Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Homework 10

This is the task corresponding to homework 10.

## Resources

### Definitions File

```theory Defs
imports "HOL-Data_Structures.Leftist_Heap"
begin

consts merge_adjacent :: "'a::ord lheap list \<Rightarrow> 'a lheap list"

consts merge_forest :: "'a::ord lheap list \<Rightarrow> 'a lheap"

consts heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"

end```

### Template File

```theory Submission
imports Defs
begin

fun merge_adjacent :: "'a::ord lheap list \<Rightarrow> 'a lheap list"  where

lemma length_merge_adjacent[simp]: "length (merge_adjacent ts) = (length ts + 1) div 2"
sorry

fun merge_forest :: "'a::ord lheap list \<Rightarrow> 'a lheap"  where
"merge_forest _ = undefined"

definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
where
"heap_of_list _ = undefined"

lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
sorry

lemma heap_heap_of_list: "heap (heap_of_list xs)"
sorry

lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
sorry

end```

### Check File

```theory Check
imports Submission
begin

lemma length_merge_adjacent: "length (merge_adjacent ts) = (length ts + 1) div 2"