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