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.

# Week 12 homework

FDS week 12

## Resources

### Definitions File

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

### Template File

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

### Check File

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

Terms and Conditions