# HG changeset patch
# User nipkow
# Date 1447685987 -3600
# Node ID d04b1b4fb01548d425f1d7a24d871e4275cd0ed9
# Parent  95a57e288fd4b6d2315385ee463b4e494ebc5194
corrected inefficient implementation

diff -r 95a57e288fd4 -r d04b1b4fb015 src/HOL/Data_Structures/Map_by_Ordered.thy
--- a/src/HOL/Data_Structures/Map_by_Ordered.thy	Mon Nov 16 14:27:10 2015 +0100
+++ b/src/HOL/Data_Structures/Map_by_Ordered.thy	Mon Nov 16 15:59:47 2015 +0100
@@ -34,22 +34,24 @@
 and delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
   inorder(delete a t) = del_list a (inorder t)"
 and inv_empty:  "inv empty"
-and inv_insert: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(update a b t)"
+and inv_update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(update a b t)"
 and inv_delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(delete a t)"
 begin
 
 sublocale Map
-  empty update delete "map_of o inorder" "\<lambda>t. inv t \<and> sorted1 (inorder t)"
+  empty update delete lookup "\<lambda>t. inv t \<and> sorted1 (inorder t)"
 proof(standard, goal_cases)
-  case 1 show ?case by (auto simp: empty)
+  case 1 show ?case by (auto simp: lookup empty inv_empty)
 next
-  case 2 thus ?case by(simp add: update map_of_ins_list)
+  case 2 thus ?case
+    by(simp add: fun_eq_iff update inv_update map_of_ins_list lookup sorted_upd_list)
 next
-  case 3 thus ?case by(simp add: delete map_of_del_list)
+  case 3 thus ?case
+    by(simp add: fun_eq_iff delete inv_delete map_of_del_list lookup sorted_del_list)
 next
   case 4 thus ?case by(simp add: empty inv_empty)
 next
-  case 5 thus ?case by(simp add: update inv_insert sorted_upd_list)
+  case 5 thus ?case by(simp add: update inv_update sorted_upd_list)
 next
   case 6 thus ?case by (auto simp: delete inv_delete sorted_del_list)
 qed