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.

# FDS Week 12 Homework

Week 12 homework.

## Resources

### Definitions File

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

### Template File

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

### Check File

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

Terms and Conditions