FDS Week 8 homework

Definitions File

theory Defs
  imports Main  "~~/src/HOL/Data_Structures/AVL_Set"
begin

 fun fib_tree :: "nat \<Rightarrow> unit avl_tree" where
 "fib_tree 0 = Leaf" |
 "fib_tree (Suc 0) = Node Leaf () 1 Leaf" |
 "fib_tree (Suc(Suc n)) = Node (fib_tree (Suc n)) () (Suc(Suc(n))) (fib_tree n)"

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

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"

value "delete 3 (iNode (iNode (iNode iLeaf (Interval 0 0) iLeaf) (Interval 1 1) (iNode iLeaf (Interval 2 4) iLeaf)) (Interval (5::nat) 6) (iLeaf))
       = iNode (iNode (iNode iLeaf (Interval 0 0) iLeaf) (Interval 1 1) (iNode iLeaf (Interval 2 2) (iNode iLeaf (Interval 4 4) iLeaf))) (Interval 5 6) iLeaf"

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

lemma 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 fib_tree_minimal)

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

lemma delete_ibst: "ibst t \<Longrightarrow> ibst (delete x t)"
  by(rule delete_ibst)

end