# HG changeset patch
# User nipkow
# Date 1447675732 -3600
# Node ID e6784939d6455712a74b282eca596d2c67c6ec60
# Parent  2b3772ecfdec32a5c70e1cad1dbd404d164c4223
tuned names

diff -r 2b3772ecfdec -r e6784939d645 src/HOL/Data_Structures/AVL_Map.thy
--- 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
diff -r 2b3772ecfdec -r e6784939d645 src/HOL/Data_Structures/Map_by_Ordered.thy
--- 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
diff -r 2b3772ecfdec -r e6784939d645 src/HOL/Data_Structures/RBT_Map.thy
--- 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
diff -r 2b3772ecfdec -r e6784939d645 src/HOL/Data_Structures/Splay_Map.thy
--- 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
diff -r 2b3772ecfdec -r e6784939d645 src/HOL/Data_Structures/Tree234_Map.thy
--- 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
diff -r 2b3772ecfdec -r e6784939d645 src/HOL/Data_Structures/Tree23_Map.thy
--- 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
diff -r 2b3772ecfdec -r e6784939d645 src/HOL/Data_Structures/Tree_Map.thy
--- 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