diff -r c5232e6fb10b -r 3fb16bed5d6c src/HOL/Data_Structures/Lookup2.thy --- a/src/HOL/Data_Structures/Lookup2.thy Tue Sep 24 17:36:14 2019 +0200 +++ b/src/HOL/Data_Structures/Lookup2.thy Wed Sep 25 17:22:57 2019 +0200 @@ -9,13 +9,13 @@ Map_Specs begin -fun lookup :: "('a::linorder * 'b, 'c) tree \ 'a \ 'b option" where +fun lookup :: "(('a::linorder * 'b) * 'c) tree \ 'a \ 'b option" where "lookup Leaf x = None" | -"lookup (Node l (a,b) _ r) x = +"lookup (Node l ((a,b), _) r) x = (case cmp x a of LT \ lookup l x | GT \ lookup r x | EQ \ Some b)" lemma lookup_map_of: "sorted1(inorder t) \ lookup t x = map_of (inorder t) x" -by(induction t) (auto simp: map_of_simps split: option.split) +by(induction t rule: tree2_induct) (auto simp: map_of_simps split: option.split) end