Cookies disclaimer

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.

FDS Week 12 Homework

Week 12 homework.


Download Files

Definitions File

theory Defs


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)"


Template File

theory Template
  imports Defs

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)"

lemma mset_heap_insert[simp]: "mset_heap (insert x t) = {#x#} + mset_heap t"

lemma invar_merge[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)"

lemma mset_heap_merge[simp]: "mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2"


Check File

theory Check
  imports Template

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)


Terms and Conditions