--- a/src/HOL/Data_Structures/AVL_Map.thy Mon Nov 16 12:37:46 2015 +0100
+++ b/src/HOL/Data_Structures/AVL_Map.thy Mon Nov 16 13:08:52 2015 +0100
@@ -38,7 +38,7 @@
interpretation Map_by_Ordered
where empty = Leaf and lookup = lookup and update = update and delete = delete
-and inorder = inorder and wf = "\<lambda>_. True"
+and inorder = inorder and inv = "\<lambda>_. True"
proof (standard, goal_cases)
case 1 show ?case by simp
next
@@ -47,6 +47,6 @@
case 3 thus ?case by(simp add: inorder_update)
next
case 4 thus ?case by(simp add: inorder_delete)
-qed (rule TrueI)+
+qed auto
end
--- a/src/HOL/Data_Structures/Map_by_Ordered.thy Mon Nov 16 12:37:46 2015 +0100
+++ b/src/HOL/Data_Structures/Map_by_Ordered.thy Mon Nov 16 13:08:52 2015 +0100
@@ -12,12 +12,12 @@
fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm"
fixes map_of :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
fixes invar :: "'m \<Rightarrow> bool"
-assumes "map_of empty = (\<lambda>_. None)"
-assumes "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)"
-assumes "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)"
-assumes "invar empty"
-assumes "invar m \<Longrightarrow> invar(update a b m)"
-assumes "invar m \<Longrightarrow> invar(delete a m)"
+assumes map_empty: "map_of empty = (\<lambda>_. None)"
+and map_update: "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)"
+and map_delete: "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)"
+and invar_empty: "invar empty"
+and invar_update: "invar m \<Longrightarrow> invar(update a b m)"
+and invar_delete: "invar m \<Longrightarrow> invar(delete a m)"
locale Map_by_Ordered =
fixes empty :: "'t"
@@ -25,21 +25,21 @@
fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
fixes lookup :: "'t \<Rightarrow> 'a \<Rightarrow> 'b option"
fixes inorder :: "'t \<Rightarrow> ('a * 'b) list"
-fixes wf :: "'t \<Rightarrow> bool"
+fixes inv :: "'t \<Rightarrow> bool"
assumes empty: "inorder empty = []"
-assumes lookup: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
+and lookup: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
lookup t a = map_of (inorder t) a"
-assumes update: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
+and update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
inorder(update a b t) = upd_list a b (inorder t)"
-assumes delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
+and delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
inorder(delete a t) = del_list a (inorder t)"
-assumes wf_empty: "wf empty"
-assumes wf_insert: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(update a b t)"
-assumes wf_delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(delete a t)"
+and inv_empty: "inv empty"
+and inv_insert: "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. wf t \<and> sorted1 (inorder t)"
+ empty update delete "map_of o inorder" "\<lambda>t. inv t \<and> sorted1 (inorder t)"
proof(standard, goal_cases)
case 1 show ?case by (auto simp: empty)
next
@@ -47,11 +47,11 @@
next
case 3 thus ?case by(simp add: delete map_of_del_list)
next
- case 4 thus ?case by(simp add: empty wf_empty)
+ case 4 thus ?case by(simp add: empty inv_empty)
next
- case 5 thus ?case by(simp add: update wf_insert sorted_upd_list)
+ case 5 thus ?case by(simp add: update inv_insert sorted_upd_list)
next
- case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list)
+ case 6 thus ?case by (auto simp: delete inv_delete sorted_del_list)
qed
end
--- a/src/HOL/Data_Structures/RBT_Map.thy Mon Nov 16 12:37:46 2015 +0100
+++ b/src/HOL/Data_Structures/RBT_Map.thy Mon Nov 16 13:08:52 2015 +0100
@@ -53,7 +53,7 @@
interpretation Map_by_Ordered
where empty = Leaf and lookup = lookup and update = update and delete = delete
-and inorder = inorder and wf = "\<lambda>_. True"
+and inorder = inorder and inv = "\<lambda>_. True"
proof (standard, goal_cases)
case 1 show ?case by simp
next
@@ -62,6 +62,6 @@
case 3 thus ?case by(simp add: inorder_update)
next
case 4 thus ?case by(simp add: inorder_delete)
-qed (rule TrueI)+
+qed auto
end
--- a/src/HOL/Data_Structures/Splay_Map.thy Mon Nov 16 12:37:46 2015 +0100
+++ b/src/HOL/Data_Structures/Splay_Map.thy Mon Nov 16 13:08:52 2015 +0100
@@ -163,7 +163,7 @@
interpretation Map_by_Ordered
where empty = Leaf and lookup = lookup and update = update
-and delete = delete and inorder = inorder and wf = "\<lambda>_. True"
+and delete = delete and inorder = inorder and inv = "\<lambda>_. True"
proof (standard, goal_cases)
case 2 thus ?case by(simp add: lookup_eq)
next
--- a/src/HOL/Data_Structures/Tree234_Map.thy Mon Nov 16 12:37:46 2015 +0100
+++ b/src/HOL/Data_Structures/Tree234_Map.thy Mon Nov 16 13:08:52 2015 +0100
@@ -165,7 +165,7 @@
interpretation T234_Map: Map_by_Ordered
where empty = Leaf and lookup = lookup and update = update and delete = delete
-and inorder = inorder and wf = bal
+and inorder = inorder and inv = bal
proof (standard, goal_cases)
case 2 thus ?case by(simp add: lookup)
next
--- a/src/HOL/Data_Structures/Tree23_Map.thy Mon Nov 16 12:37:46 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Map.thy Mon Nov 16 13:08:52 2015 +0100
@@ -120,7 +120,7 @@
interpretation T23_Map: Map_by_Ordered
where empty = Leaf and lookup = lookup and update = update and delete = delete
-and inorder = inorder and wf = bal
+and inorder = inorder and inv = bal
proof (standard, goal_cases)
case 2 thus ?case by(simp add: lookup)
next
--- a/src/HOL/Data_Structures/Tree_Map.thy Mon Nov 16 12:37:46 2015 +0100
+++ b/src/HOL/Data_Structures/Tree_Map.thy Mon Nov 16 13:08:52 2015 +0100
@@ -44,7 +44,7 @@
interpretation Map_by_Ordered
where empty = Leaf and lookup = lookup and update = update and delete = delete
-and inorder = inorder and wf = "\<lambda>_. True"
+and inorder = inorder and inv = "\<lambda>_. True"
proof (standard, goal_cases)
case 1 show ?case by simp
next
@@ -53,6 +53,6 @@
case 3 thus ?case by(simp add: inorder_update)
next
case 4 thus ?case by(simp add: inorder_delete)
-qed (rule TrueI)+
+qed auto
end