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.

# Homework 12

This is the task corresponding to homework 12.

## Resources

### Definitions File

```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```

### Template File

```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```

### Check File

```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```

Terms and Conditions