Homework 8

Definitions File

theory Defs
  imports "HOL-Library.Tree"
begin

fun avl :: "nat tree \<Rightarrow> bool" where
  "avl \<langle>\<rangle> = True"
| "avl \<langle>l, n, r\<rangle> = (abs(int(height l) - int(height r)) \<le> 1 \<and>
     n = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"

fun ht :: "nat tree \<Rightarrow> nat" where
  "ht \<langle>\<rangle> = 0"
| "ht \<langle>l, n, r\<rangle> = n"

lemma ht_height[simp]: "avl t \<Longrightarrow> ht t = height t"
  by (induction t) auto

declare [[names_short]]

fun fib_tree :: "nat \<Rightarrow> nat tree" where
 "fib_tree 0 = \<langle>\<rangle>" |
 "fib_tree (Suc 0) = \<langle>\<langle>\<rangle>, 1, \<langle>\<rangle>\<rangle>" |
 "fib_tree (Suc(Suc n)) = \<langle>fib_tree (Suc n), Suc (Suc n), fib_tree n\<rangle>"

datatype 'a itree = iLeaf | iNode "'a itree" "'a \<times> 'a" "'a itree"

fun set_itree2:: "'a::ord itree \<Rightarrow> 'a set" where
  "set_itree2 iLeaf = {}"
| "set_itree2 (iNode l (low, high) r) = {low .. high} \<union> ((set_itree2 l) \<union> (set_itree2 r))"

fun set_itree3:: "'a itree \<Rightarrow> ('a \<times> 'a) set" where
  "set_itree3 iLeaf = {}"
| "set_itree3 (iNode l (low, high) r) = {(low, high)} \<union> ((set_itree3 l) \<union> (set_itree3 r))"

consts ibst :: "'a::linorder itree \<Rightarrow> bool"

consts delete :: "int \<Rightarrow> int itree \<Rightarrow> int itree"


end

Template File

theory Submission
  imports Defs
begin

lemma fib_tree_minimal: "avl t \<Longrightarrow> size1 (fib_tree (ht t)) \<le> size1 t"
  sorry

fun ibst :: "'a::linorder itree \<Rightarrow> bool"  where
  "ibst _ = undefined"

fun delete :: "int \<Rightarrow> int itree \<Rightarrow> int itree"  where
  "delete _ = undefined"

theorem delete_set_minus: "ibst t \<Longrightarrow> set_itree2 (delete x t) = (set_itree2 t) - {x}"
  sorry

theorem delete_ibst: "ibst t \<Longrightarrow> ibst (delete x t)"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma fib_tree_minimal: "avl t \<Longrightarrow> size1 (fib_tree (ht t)) \<le> size1 t"
  by (rule Submission.fib_tree_minimal)

theorem delete_set_minus: "ibst t \<Longrightarrow> set_itree2 (delete x t) = (set_itree2 t) - {x}"
  by (rule Submission.delete_set_minus)

theorem delete_ibst: "ibst t \<Longrightarrow> ibst (delete x t)"
  by (rule Submission.delete_ibst)

end