I agree 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.
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
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
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