author | nipkow |
Thu, 07 Jul 2016 18:08:02 +0200 | |
changeset 63411 | e051eea34990 |
parent 62390 | 842917225d56 |
child 67965 | aaa31cd0caef |
permissions | -rw-r--r-- |
61232 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
section \<open>Function \textit{lookup} for Tree2\<close> |
|
4 |
||
5 |
theory Lookup2 |
|
6 |
imports |
|
7 |
Tree2 |
|
61693 | 8 |
Cmp |
61232 | 9 |
Map_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 lookup :: "('a::linorder * 'b, 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where |
61232 | 13 |
"lookup Leaf x = None" | |
14 |
"lookup (Node _ l (a,b) r) x = |
|
61693 | 15 |
(case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)" |
61232 | 16 |
|
61790 | 17 |
lemma lookup_map_of: |
18 |
"sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" |
|
61232 | 19 |
by(induction t) (auto simp: map_of_simps split: option.split) |
20 |
||
62390 | 21 |
end |