|
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 |
|
|
61693
|
12 |
fun lookup :: "('a::cmp * '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 |
|
|
61693
|
17 |
lemma lookup_eq: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
|
|
61232
|
18 |
by(induction t) (auto simp: map_of_simps split: option.split)
|
|
|
19 |
|
|
|
20 |
end |