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
datatype 'a tree = Node (root: 'a) (children: "'a tree list")
type_synonym 'a heap = "(nat*'a tree) list"
lemma [simp]:
"(a, b) \<in> set (zip (rev [0..<r]) ts) \<Longrightarrow> size b \<le> (size_list size ts)"
by (induction "[0..<r]")
(auto elim: in_set_zipE intro!: size_list_estimation')
fun invar_btree :: "nat \<Rightarrow> 'a::linorder tree \<Rightarrow> bool" where
"invar_btree r (Node x ts) \<longleftrightarrow>
length ts = r \<and> (\<forall>(r',t)\<in>set (zip (rev [0..<r]) ts). invar_btree r' t)"
definition invar_bheap :: "'a::linorder heap \<Rightarrow> bool" where
"invar_bheap ts
\<longleftrightarrow> (\<forall>(r,t)\<in>set ts. invar_btree r t) \<and> (sorted_wrt (<) (map fst ts))"
fun invar_otree :: "'a::linorder tree \<Rightarrow> bool" where
"invar_otree (Node x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t \<and> x \<le> root t)"
definition invar_oheap :: "'a::linorder tree list \<Rightarrow> bool" where
"invar_oheap ts \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t)"
definition invar :: "'a::linorder heap \<Rightarrow> bool" where
"invar ts \<longleftrightarrow> invar_bheap ts \<and> invar_oheap (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)"
end
theory Template
imports Defs
begin
definition insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
"insert _ _ = undefined"
fun merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
"merge _ _ = 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
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 Template
begin
abbreviation "ins \<equiv> Template.insert"
lemma invar_insert[simp]: "Defs.invar t \<Longrightarrow> Defs.invar (ins x t)"
by(rule invar_insert)
lemma mset_heap_insert[simp]: "Defs.mset_heap (ins x t) = {#x#} + Defs.mset_heap t"
by(rule mset_heap_insert)
lemma invar_merge[simp]: "\<lbrakk> Defs.invar ts\<^sub>1; Defs.invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> Defs.invar (merge ts\<^sub>1 ts\<^sub>2)"
by(rule invar_merge)
lemma mset_heap_merge[simp]: "Defs.mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2"
by(rule mset_heap_merge)
end