FDS Week 3 Homework

Definitions File

theory Defs
  imports "HOL-Library.Tree"
begin

fun isin :: "('a::linorder) tree \<Rightarrow> 'a \<Rightarrow> bool" where
"isin Leaf x = False" |
"isin (Node l a r) x =
  (if x < a then isin l x else
   if x > a then isin r x
   else True)"

fun ins :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
"ins x Leaf = Node Leaf x Leaf" |
"ins x (Node l a r) =
  (if x < a then Node (ins x l) a r else
   if x > a then Node l a (ins x r)
   else Node l a r)"

end

Template File

theory Template
  imports Defs
begin

abbreviation bst_eq :: "('a::linorder) tree \<Rightarrow> bool" where
"bst_eq \<equiv> undefined"


lemma isin_bst_eq: "bst_eq t \<Longrightarrow> isin t x = (x \<in> set_tree t)"
  sorry



lemma bst_eq_ins: "bst_eq t \<Longrightarrow> bst_eq (ins x t)"
  sorry

fun ins_eq :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
  where
"ins_eq _ _= undefined"


lemma bst_eq_ins_eq: "bst_eq t \<Longrightarrow> bst_eq (ins_eq x t)"
  sorry

fun count_tree :: "'a \<Rightarrow> 'a tree \<Rightarrow> nat" 
  where
  "count_tree _ _ = undefined"
  
lemma count_tree_ins_eq: "count_tree x (ins_eq x t) = Suc (count_tree x t)"  
  sorry

lemma count_tree_ins_eq_diff: "x\<noteq>y \<Longrightarrow> count_tree y (ins_eq x t) = count_tree y t"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma isin_bst_eq: "bst_eq t \<Longrightarrow> isin t x = (x \<in> set_tree t)"
  by (rule isin_bst_eq)

lemma bst_eq_ins: "bst_eq t \<Longrightarrow> bst_eq (ins x t)"
  by(rule bst_eq_ins)

lemma bst_eq_ins_eq: "bst_eq t \<Longrightarrow> bst_eq (ins_eq x t)"
  by(rule bst_eq_ins_eq)

lemma count_tree_ins_eq: "count_tree x (ins_eq x t) = Suc (count_tree x t)"  
  by (rule count_tree_ins_eq)

lemma "x\<noteq>y \<Longrightarrow> count_tree y (ins_eq x t) = count_tree y t"
  by (rule count_tree_ins_eq_diff)

end