| author | Manuel Eberl <eberlm@in.tum.de> |
| Mon, 26 Mar 2018 16:12:55 +0200 | |
| changeset 67950 | 99eaa5cedbb7 |
| parent 67929 | 30486b96274d |
| child 67964 | 08cc5ab18c84 |
| 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 |
| 61224 | 9 |
Set_by_Ordered |
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 |
|
| 67929 | 20 |
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set(inorder t))" |
21 |
by (induction t) (auto simp: isin_simps) |
|
| 61224 | 22 |
|
| 62390 | 23 |
end |