Week 12 homework

Definitions File

theory Defs
  imports
  "HOL-Data_Structures.Base_FDS"
  "HOL-Data_Structures.Tree2"
  "HOL-Data_Structures.Priority_Queue_Specs"
  Complex_Main
begin

fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where
"mset_tree Leaf = {#}" |
"mset_tree (Node l a _ r) = {#a#} + mset_tree l + mset_tree r"

type_synonym 'a lheap = "('a,nat)tree"

fun ltree :: "('a,nat)tree \<Rightarrow> bool" where
"ltree Leaf = True" |
"ltree (Node l a n r) =
 (n = size l + 1 + size r \<and> size l \<ge> size r \<and> ltree l \<and> ltree r)"

unbundle pattern_aliases
end

Template File

theory Submission
  imports Defs
begin

fun (in linorder) heap :: "('a,'b) tree \<Rightarrow> bool" where
"heap _ = undefined"

fun get_min :: "'a lheap \<Rightarrow> 'a" where
"get_min(Node l a n r) = a"


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

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

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

interpretation lheap: Priority_Queue_Merge
where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
and insert = insert and del_min = del_min
and get_min = get_min and merge = merge
and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
  sorry

fun t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
  "t_merge _ = undefined"

lemma t_merge_log: assumes "ltree l" "ltree r"
shows "t_merge l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"
  sorry

definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
"t_insert _ = undefined"

lemma t_insert_log: "ltree t \<Longrightarrow> t_insert x t \<le> log 2 (size1 t) + 2"
  sorry

fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where
"t_del_min _ = undefined"

lemma t_del_min_log: assumes "ltree t"
  shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"
  sorry

end

Check File

theory Check
  imports "Submission"
begin

interpretation lheap: Priority_Queue_Merge
where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
and insert = insert and del_min = del_min
and get_min = get_min and merge = merge
and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
  by(rule lheap.Priority_Queue_Merge_axioms)

lemma t_merge_log: assumes "ltree l" "ltree r"
  shows "t_merge l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"
  by (rule t_merge_log[OF assms])

lemma t_insert_log: "ltree t \<Longrightarrow> t_insert x t \<le> log 2 (size1 t) + 2"
  by (rule t_insert_log)

lemma t_del_min_log: assumes "ltree t"
  shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"
  by (rule t_del_min_log[OF assms])

end