Homework 10

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
  "merge_adjacent _ = undefined"

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"
  by (rule Submission.length_merge_adjacent)

lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
  by (rule Submission.mset_heap_of_list)

lemma heap_heap_of_list: "heap (heap_of_list xs)"
  by (rule Submission.heap_heap_of_list)

lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
  by (rule Submission.ltree_ltree_of_list)

end