| author | nipkow |
| Sun, 13 May 2018 13:15:50 +0200 | |
| changeset 68159 | 620ca44d8b7d |
| parent 67967 | 5a4280946a25 |
| child 68413 | b56ed5010e69 |
| permissions | -rw-r--r-- |
| 61224 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
section \<open>Function \textit{isin} for Tree2\<close>
|
|
4 |
||
5 |
theory Isin2 |
|
6 |
imports |
|
7 |
Tree2 |
|
|
61692
cb595e12451d
removed lemmas that were only needed for old version of isin.
nipkow
parents:
61229
diff
changeset
|
8 |
Cmp |
| 67965 | 9 |
Set_Specs |
| 61224 | 10 |
begin |
11 |
||
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62390
diff
changeset
|
12 |
fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where
|
| 61224 | 13 |
"isin Leaf x = False" | |
|
61692
cb595e12451d
removed lemmas that were only needed for old version of isin.
nipkow
parents:
61229
diff
changeset
|
14 |
"isin (Node _ l a r) x = |
|
cb595e12451d
removed lemmas that were only needed for old version of isin.
nipkow
parents:
61229
diff
changeset
|
15 |
(case cmp x a of |
|
cb595e12451d
removed lemmas that were only needed for old version of isin.
nipkow
parents:
61229
diff
changeset
|
16 |
LT \<Rightarrow> isin l x | |
|
cb595e12451d
removed lemmas that were only needed for old version of isin.
nipkow
parents:
61229
diff
changeset
|
17 |
EQ \<Rightarrow> True | |
|
cb595e12451d
removed lemmas that were only needed for old version of isin.
nipkow
parents:
61229
diff
changeset
|
18 |
GT \<Rightarrow> isin r x)" |
| 61224 | 19 |
|
| 67967 | 20 |
lemma isin_set_inorder: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set(inorder t))" |
| 67929 | 21 |
by (induction t) (auto simp: isin_simps) |
| 61224 | 22 |
|
| 67967 | 23 |
lemma isin_set_tree: "bst t \<Longrightarrow> isin t x \<longleftrightarrow> x \<in> set_tree t" |
24 |
by(induction t) auto |
|
25 |
||
| 62390 | 26 |
end |