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