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