|
61224
|
1 |
(* Author: Tobias Nipkow *)
|
|
|
2 |
|
|
|
3 |
section \<open>Function \textit{isin} for Tree2\<close>
|
|
|
4 |
|
|
|
5 |
theory Isin2
|
|
|
6 |
imports
|
|
|
7 |
Tree2
|
|
|
8 |
Set_by_Ordered
|
|
|
9 |
begin
|
|
|
10 |
|
|
|
11 |
fun isin :: "('a,'b) tree \<Rightarrow> ('a::order) \<Rightarrow> bool" where
|
|
|
12 |
"isin Leaf x = False" |
|
|
|
13 |
"isin (Node _ l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)"
|
|
|
14 |
|
|
|
15 |
lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
|
|
61229
|
16 |
by (induction t) (auto simp: elems_simps1)
|
|
61224
|
17 |
|
|
|
18 |
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
|
|
61229
|
19 |
by (induction t) (auto simp: elems_simps2)
|
|
61224
|
20 |
|
|
|
21 |
end |