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