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-Library.Pattern_Aliases" Complex_Main "HOL-Data_Structures.Priority_Queue_Specs"
begin
lemma size_list_size[simp]:
"(a, b) \<in> set (zip (rev [0..<r]) ts) \<Longrightarrow> size b < Suc (size_list size ts)"
apply(induction ts)
apply simp
apply (metis in_set_zipE nat_neq_iff not_less_eq size_list_estimation)
done
datatype 'a tree = Node (root: 'a) (children: "'a tree list")
type_synonym 'a heap = "(nat*'a tree) list"
fun btree :: "nat \<Rightarrow> 'a::linorder tree \<Rightarrow> bool" where
"btree r (Node x ts) \<longleftrightarrow>
length ts = r \<and> (\<forall>(r',t)\<in>set (zip (rev [0..<r]) ts). btree r' t)"
definition bheap :: "'a::linorder heap \<Rightarrow> bool" where
"bheap ts \<longleftrightarrow> (\<forall>(r,t)\<in>set ts. btree r t) \<and> (sorted_wrt (<) (map fst ts))"
fun heap :: "'a::linorder tree \<Rightarrow> bool" where
"heap (Node x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. heap t \<and> x \<le> root t)"
definition heaps :: "'a::linorder tree list \<Rightarrow> bool" where
"heaps ts \<longleftrightarrow> (\<forall>t\<in>set ts. heap t)"
definition invar :: "'a::linorder heap \<Rightarrow> bool" where
"invar ts \<longleftrightarrow> bheap ts \<and> heaps (map snd ts)"
fun mset_tree :: "'a::linorder tree \<Rightarrow> 'a multiset" where
"mset_tree (Node a ts) = {#a#} + (\<Sum>t\<in>#mset ts. mset_tree t)"
definition mset_heap :: "'a::linorder heap \<Rightarrow> 'a multiset" where
"mset_heap ts = (\<Sum>(r,t)\<in>#mset ts. mset_tree t)"
consts insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap"
consts merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap"
end
theory Submission
imports Defs
begin
type_synonym 'a heap = "(nat*'a tree) list"
definition insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
"insert _ = undefined"
lemma invar_insert[simp]: "invar t \<Longrightarrow> invar (insert x t)"
sorry
lemma mset_heap_insert[simp]: "mset_heap (insert x t) = {#x#} + mset_heap t"
sorry
fun merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
"merge _ = undefined"
lemma invar_merge[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)"
sorry
lemma mset_heap_merge[simp]: "mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2"
sorry
end
theory Check
imports Submission
begin
lemma invar_insert: "invar t \<Longrightarrow> invar (insert x t)"
by (rule Submission.invar_insert)
lemma mset_heap_insert: "mset_heap (insert x t) = {#x#} + mset_heap t"
by (rule Submission.mset_heap_insert)
lemma invar_merge: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)"
by (rule Submission.invar_merge)
lemma mset_heap_merge: "mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2"
by (rule Submission.mset_heap_merge)
end