1(* Author: Tobias Nipkow *) 2 3section \<open>Function \textit{isin} for Tree2\<close> 4 5theory Isin2 6imports 7 Tree2 8 Cmp 9 Set_Specs 10begin 11 12fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where 13"isin Leaf x = False" | 14"isin (Node l a _ r) x = 15 (case cmp x a of 16 LT \<Rightarrow> isin l x | 17 EQ \<Rightarrow> True | 18 GT \<Rightarrow> isin r x)" 19 20lemma isin_set_inorder: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set(inorder t))" 21by (induction t) (auto simp: isin_simps) 22 23lemma isin_set_tree: "bst t \<Longrightarrow> isin t x \<longleftrightarrow> x \<in> set_tree t" 24by(induction t) auto 25 26end 27