# HG changeset patch
# User nipkow
# Date 1523178352 -7200
# Node ID aaa31cd0caef7904aa21b16e625f704d86be0ba2
# Parent  08cc5ab18c84ee4726e67eb8293b445687389514
more name tuning

diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Brother12_Map.thy
--- a/src/HOL/Data_Structures/Brother12_Map.thy	Sun Apr 08 09:46:33 2018 +0200
+++ b/src/HOL/Data_Structures/Brother12_Map.thy	Sun Apr 08 11:05:52 2018 +0200
@@ -5,7 +5,7 @@
 theory Brother12_Map
 imports
   Brother12_Set
-  Map_by_Ordered
+  Map_Specs
 begin
 
 fun lookup :: "('a \<times> 'b) bro \<Rightarrow> 'a::linorder \<Rightarrow> 'b option" where
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Brother12_Set.thy
--- a/src/HOL/Data_Structures/Brother12_Set.thy	Sun Apr 08 09:46:33 2018 +0200
+++ b/src/HOL/Data_Structures/Brother12_Set.thy	Sun Apr 08 11:05:52 2018 +0200
@@ -5,7 +5,7 @@
 theory Brother12_Set
 imports
   Cmp
-  Set_Interfaces
+  Set_Specs
   "HOL-Number_Theory.Fib"
 begin
 
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Isin2.thy
--- a/src/HOL/Data_Structures/Isin2.thy	Sun Apr 08 09:46:33 2018 +0200
+++ b/src/HOL/Data_Structures/Isin2.thy	Sun Apr 08 11:05:52 2018 +0200
@@ -6,7 +6,7 @@
 imports
   Tree2
   Cmp
-  Set_Interfaces
+  Set_Specs
 begin
 
 fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Lookup2.thy
--- a/src/HOL/Data_Structures/Lookup2.thy	Sun Apr 08 09:46:33 2018 +0200
+++ b/src/HOL/Data_Structures/Lookup2.thy	Sun Apr 08 11:05:52 2018 +0200
@@ -6,7 +6,7 @@
 imports
   Tree2
   Cmp
-  Map_by_Ordered
+  Map_Specs
 begin
 
 fun lookup :: "('a::linorder * 'b, 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Map_Specs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Map_Specs.thy	Sun Apr 08 11:05:52 2018 +0200
@@ -0,0 +1,68 @@
+(* Author: Tobias Nipkow *)
+
+section \<open>Specifications of Map ADT\<close>
+
+theory Map_Specs
+imports AList_Upd_Del
+begin
+
+text \<open>The basic map interface with traditional \<open>set\<close>-based specification:\<close>
+
+locale Map =
+fixes empty :: "'m"
+fixes update :: "'a \<Rightarrow> 'b \<Rightarrow> 'm \<Rightarrow> 'm"
+fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm"
+fixes lookup :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
+fixes invar :: "'m \<Rightarrow> bool"
+assumes map_empty: "lookup empty = (\<lambda>_. None)"
+and map_update: "invar m \<Longrightarrow> lookup(update a b m) = (lookup m)(a := Some b)"
+and map_delete: "invar m \<Longrightarrow> lookup(delete a m) = (lookup 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)"
+
+
+text \<open>The basic map interface with \<open>inorder\<close>-based specification:\<close>
+
+locale Map_by_Ordered =
+fixes empty :: "'t"
+fixes update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> 't \<Rightarrow> 't"
+fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
+fixes lookup :: "'t \<Rightarrow> 'a \<Rightarrow> 'b option"
+fixes inorder :: "'t \<Rightarrow> ('a * 'b) list"
+fixes inv :: "'t \<Rightarrow> bool"
+assumes empty: "inorder empty = []"
+and lookup: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
+  lookup t a = map_of (inorder t) a"
+and update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
+  inorder(update a b t) = upd_list a b (inorder t)"
+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_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
+
+text \<open>It implements the traditional specification:\<close>
+
+sublocale Map
+  empty update delete lookup "\<lambda>t. inv t \<and> sorted1 (inorder t)"
+proof(standard, goal_cases)
+  case 1 show ?case by (auto simp: lookup empty inv_empty)
+next
+  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: 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_update sorted_upd_list)
+next
+  case 6 thus ?case by (auto simp: delete inv_delete sorted_del_list)
+qed
+
+end
+
+end
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Map_by_Ordered.thy
--- a/src/HOL/Data_Structures/Map_by_Ordered.thy	Sun Apr 08 09:46:33 2018 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-section \<open>Implementing Ordered Maps\<close>
-
-theory Map_by_Ordered
-imports AList_Upd_Del
-begin
-
-locale Map =
-fixes empty :: "'m"
-fixes update :: "'a \<Rightarrow> 'b \<Rightarrow> 'm \<Rightarrow> 'm"
-fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm"
-fixes lookup :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
-fixes invar :: "'m \<Rightarrow> bool"
-assumes map_empty: "lookup empty = (\<lambda>_. None)"
-and map_update: "invar m \<Longrightarrow> lookup(update a b m) = (lookup m)(a := Some b)"
-and map_delete: "invar m \<Longrightarrow> lookup(delete a m) = (lookup 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"
-fixes update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> 't \<Rightarrow> 't"
-fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
-fixes lookup :: "'t \<Rightarrow> 'a \<Rightarrow> 'b option"
-fixes inorder :: "'t \<Rightarrow> ('a * 'b) list"
-fixes inv :: "'t \<Rightarrow> bool"
-assumes empty: "inorder empty = []"
-and lookup: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
-  lookup t a = map_of (inorder t) a"
-and update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
-  inorder(update a b t) = upd_list a b (inorder t)"
-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_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 lookup "\<lambda>t. inv t \<and> sorted1 (inorder t)"
-proof(standard, goal_cases)
-  case 1 show ?case by (auto simp: lookup empty inv_empty)
-next
-  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: 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_update sorted_upd_list)
-next
-  case 6 thus ?case by (auto simp: delete inv_delete sorted_del_list)
-qed
-
-end
-
-end
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Set_Interfaces.thy
--- a/src/HOL/Data_Structures/Set_Interfaces.thy	Sun Apr 08 09:46:33 2018 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,86 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-section \<open>Interfaces for Set ADT\<close>
-
-theory Set_Interfaces
-imports List_Ins_Del
-begin
-
-text \<open>The basic set interface with traditional specification (based on \<open>set\<close> and \<open>bst\<close>):\<close>
-
-locale Set =
-fixes empty :: "'s"
-fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
-fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
-fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
-fixes set :: "'s \<Rightarrow> 'a set"
-fixes invar :: "'s \<Rightarrow> bool"
-assumes set_empty:    "set empty = {}"
-assumes set_isin:     "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
-assumes set_insert:   "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
-assumes set_delete:   "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
-assumes invar_empty:  "invar empty"
-assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
-assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
-
-
-text \<open>The basic set interface with \<open>inorder\<close>-based specification:\<close>
-
-locale Set_by_Ordered =
-fixes empty :: "'t"
-fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
-fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
-fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
-fixes inorder :: "'t \<Rightarrow> 'a list"
-fixes inv :: "'t \<Rightarrow> bool"
-assumes empty: "inorder empty = []"
-assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
-  isin t x = (x \<in> set (inorder t))"
-assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
-  inorder(insert x t) = ins_list x (inorder t)"
-assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
-  inorder(delete x t) = del_list x (inorder t)"
-assumes inv_empty:  "inv empty"
-assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
-assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
-begin
-
-text \<open>It implements the traditional specification:\<close>
-
-sublocale Set
-  empty insert delete isin "set o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
-proof(standard, goal_cases)
-  case 1 show ?case by (auto simp: empty)
-next
-  case 2 thus ?case by(simp add: isin)
-next
-  case 3 thus ?case by(simp add: insert set_ins_list)
-next
-  case (4 s x) thus ?case
-    using delete[OF 4, of x] by (auto simp: distinct_if_sorted set_del_list_eq)
-next
-  case 5 thus ?case by(simp add: empty inv_empty)
-next
-  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
-next
-  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
-qed
-
-end
-
-
-text \<open>Set2 = Set with binary operations:\<close>
-
-locale Set2 = Set
-  where insert = insert for insert :: "'a \<Rightarrow> 's \<Rightarrow> 's" (*for typing purposes only*) +
-fixes union :: "'s \<Rightarrow> 's \<Rightarrow> 's"
-fixes inter :: "'s \<Rightarrow> 's \<Rightarrow> 's"
-fixes diff  :: "'s \<Rightarrow> 's \<Rightarrow> 's"
-assumes set_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(union s1 s2) = set s1 \<union> set s2"
-assumes set_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(inter s1 s2) = set s1 \<inter> set s2"
-assumes set_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(diff s1 s2) = set s1 - set s2"
-assumes invar_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(union s1 s2)"
-assumes invar_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(inter s1 s2)"
-assumes invar_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(diff s1 s2)"
-
-end
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Set_Specs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Set_Specs.thy	Sun Apr 08 11:05:52 2018 +0200
@@ -0,0 +1,86 @@
+(* Author: Tobias Nipkow *)
+
+section \<open>Specifications of Set ADT\<close>
+
+theory Set_Specs
+imports List_Ins_Del
+begin
+
+text \<open>The basic set interface with traditional \<open>set\<close>-based specification:\<close>
+
+locale Set =
+fixes empty :: "'s"
+fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
+fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
+fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
+fixes set :: "'s \<Rightarrow> 'a set"
+fixes invar :: "'s \<Rightarrow> bool"
+assumes set_empty:    "set empty = {}"
+assumes set_isin:     "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
+assumes set_insert:   "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
+assumes set_delete:   "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
+assumes invar_empty:  "invar empty"
+assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
+assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
+
+
+text \<open>The basic set interface with \<open>inorder\<close>-based specification:\<close>
+
+locale Set_by_Ordered =
+fixes empty :: "'t"
+fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
+fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
+fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
+fixes inorder :: "'t \<Rightarrow> 'a list"
+fixes inv :: "'t \<Rightarrow> bool"
+assumes empty: "inorder empty = []"
+assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
+  isin t x = (x \<in> set (inorder t))"
+assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
+  inorder(insert x t) = ins_list x (inorder t)"
+assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
+  inorder(delete x t) = del_list x (inorder t)"
+assumes inv_empty:  "inv empty"
+assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
+assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
+begin
+
+text \<open>It implements the traditional specification:\<close>
+
+sublocale Set
+  empty insert delete isin "set o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
+proof(standard, goal_cases)
+  case 1 show ?case by (auto simp: empty)
+next
+  case 2 thus ?case by(simp add: isin)
+next
+  case 3 thus ?case by(simp add: insert set_ins_list)
+next
+  case (4 s x) thus ?case
+    using delete[OF 4, of x] by (auto simp: distinct_if_sorted set_del_list_eq)
+next
+  case 5 thus ?case by(simp add: empty inv_empty)
+next
+  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
+next
+  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
+qed
+
+end
+
+
+text \<open>Set2 = Set with binary operations:\<close>
+
+locale Set2 = Set
+  where insert = insert for insert :: "'a \<Rightarrow> 's \<Rightarrow> 's" (*for typing purposes only*) +
+fixes union :: "'s \<Rightarrow> 's \<Rightarrow> 's"
+fixes inter :: "'s \<Rightarrow> 's \<Rightarrow> 's"
+fixes diff  :: "'s \<Rightarrow> 's \<Rightarrow> 's"
+assumes set_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(union s1 s2) = set s1 \<union> set s2"
+assumes set_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(inter s1 s2) = set s1 \<inter> set s2"
+assumes set_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(diff s1 s2) = set s1 - set s2"
+assumes invar_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(union s1 s2)"
+assumes invar_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(inter s1 s2)"
+assumes invar_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(diff s1 s2)"
+
+end
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Tree234_Map.thy
--- a/src/HOL/Data_Structures/Tree234_Map.thy	Sun Apr 08 09:46:33 2018 +0200
+++ b/src/HOL/Data_Structures/Tree234_Map.thy	Sun Apr 08 11:05:52 2018 +0200
@@ -5,7 +5,7 @@
 theory Tree234_Map
 imports
   Tree234_Set
-  "../Data_Structures/Map_by_Ordered"
+  Map_Specs
 begin
 
 subsection \<open>Map operations on 2-3-4 trees\<close>
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Tree234_Set.thy
--- a/src/HOL/Data_Structures/Tree234_Set.thy	Sun Apr 08 09:46:33 2018 +0200
+++ b/src/HOL/Data_Structures/Tree234_Set.thy	Sun Apr 08 11:05:52 2018 +0200
@@ -6,7 +6,7 @@
 imports
   Tree234
   Cmp
-  "Set_Interfaces"
+  Set_Specs
 begin
 
 subsection \<open>Set operations on 2-3-4 trees\<close>
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Tree23_Map.thy
--- a/src/HOL/Data_Structures/Tree23_Map.thy	Sun Apr 08 09:46:33 2018 +0200
+++ b/src/HOL/Data_Structures/Tree23_Map.thy	Sun Apr 08 11:05:52 2018 +0200
@@ -5,7 +5,7 @@
 theory Tree23_Map
 imports
   Tree23_Set
-  Map_by_Ordered
+  Map_Specs
 begin
 
 fun lookup :: "('a::linorder * 'b) tree23 \<Rightarrow> 'a \<Rightarrow> 'b option" where
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Sun Apr 08 09:46:33 2018 +0200
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Sun Apr 08 11:05:52 2018 +0200
@@ -6,7 +6,7 @@
 imports
   Tree23
   Cmp
-  Set_Interfaces
+  Set_Specs
 begin
 
 fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Tree_Map.thy
--- a/src/HOL/Data_Structures/Tree_Map.thy	Sun Apr 08 09:46:33 2018 +0200
+++ b/src/HOL/Data_Structures/Tree_Map.thy	Sun Apr 08 11:05:52 2018 +0200
@@ -5,7 +5,7 @@
 theory Tree_Map
 imports
   Tree_Set
-  Map_by_Ordered
+  Map_Specs
 begin
 
 fun lookup :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/Data_Structures/Tree_Set.thy
--- a/src/HOL/Data_Structures/Tree_Set.thy	Sun Apr 08 09:46:33 2018 +0200
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Sun Apr 08 11:05:52 2018 +0200
@@ -6,7 +6,7 @@
 imports
   "HOL-Library.Tree"
   Cmp
-  Set_Interfaces
+  Set_Specs
 begin
 
 fun isin :: "'a::linorder tree \<Rightarrow> 'a \<Rightarrow> bool" where
diff -r 08cc5ab18c84 -r aaa31cd0caef src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Apr 08 09:46:33 2018 +0200
+++ b/src/HOL/ROOT	Sun Apr 08 11:05:52 2018 +0200
@@ -201,6 +201,8 @@
     Tree234_Map
     Brother12_Map
     AA_Map
+    Set2_BST_Join
+    Set2_BST2_Join_RBT
     Leftist_Heap
     Binomial_Heap
   document_files "root.tex" "root.bib"