author | paulson <lp15@cam.ac.uk> |
Mon, 30 Nov 2020 22:00:23 +0000 | |
changeset 72797 | 402afc68f2f9 |
parent 70755 | 3fb16bed5d6c |
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 |
||
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
68413
diff
changeset
|
12 |
fun isin :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where |
61224 | 13 |
"isin Leaf x = False" | |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
68413
diff
changeset
|
14 |
"isin (Node l (a,_) r) x = |
61692
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))" |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
68413
diff
changeset
|
21 |
by (induction t rule: tree2_induct) (auto simp: isin_simps) |
61224 | 22 |
|
67967 | 23 |
lemma isin_set_tree: "bst t \<Longrightarrow> isin t x \<longleftrightarrow> x \<in> set_tree t" |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
68413
diff
changeset
|
24 |
by(induction t rule: tree2_induct) auto |
67967 | 25 |
|
62390 | 26 |
end |