|
61232
|
1 |
(* Author: Tobias Nipkow *)
|
|
|
2 |
|
|
|
3 |
section \<open>Function \textit{lookup} for Tree2\<close>
|
|
|
4 |
|
|
|
5 |
theory Lookup2
|
|
|
6 |
imports
|
|
|
7 |
Tree2
|
|
|
8 |
Map_by_Ordered
|
|
|
9 |
begin
|
|
|
10 |
|
|
|
11 |
fun lookup :: "('a::linorder * 'b, 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
|
|
|
12 |
"lookup Leaf x = None" |
|
|
|
13 |
"lookup (Node _ l (a,b) r) x =
|
|
|
14 |
(if x < a then lookup l x else
|
|
|
15 |
if x > a then lookup r x else Some b)"
|
|
|
16 |
|
|
|
17 |
lemma lookup_eq:
|
|
|
18 |
"sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
|
|
|
19 |
by(induction t) (auto simp: map_of_simps split: option.split)
|
|
|
20 |
|
|
|
21 |
end |