src/HOL/Data_Structures/Tree234_Map.thy
changeset 61790 0494964bb226
parent 61686 e6784939d645
child 62130 90a3016a6c12
     1.1 --- a/src/HOL/Data_Structures/Tree234_Map.thy	Sat Dec 05 16:13:28 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/Tree234_Map.thy	Sat Dec 05 16:33:20 2015 +0100
     1.3 @@ -113,7 +113,8 @@
     1.4  
     1.5  subsection "Functional correctness"
     1.6  
     1.7 -lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
     1.8 +lemma lookup_map_of:
     1.9 +  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    1.10  by (induction t) (auto simp: map_of_simps split: option.split)
    1.11  
    1.12  
    1.13 @@ -163,11 +164,11 @@
    1.14  
    1.15  subsection \<open>Overall Correctness\<close>
    1.16  
    1.17 -interpretation T234_Map: Map_by_Ordered
    1.18 +interpretation Map_by_Ordered
    1.19  where empty = Leaf and lookup = lookup and update = update and delete = delete
    1.20  and inorder = inorder and inv = bal
    1.21  proof (standard, goal_cases)
    1.22 -  case 2 thus ?case by(simp add: lookup)
    1.23 +  case 2 thus ?case by(simp add: lookup_map_of)
    1.24  next
    1.25    case 3 thus ?case by(simp add: inorder_update)
    1.26  next