more name tuning
authornipkow
Sun Apr 08 11:05:52 2018 +0200 (13 months ago)
changeset 67965aaa31cd0caef
parent 67964 08cc5ab18c84
child 67966 f13796496e82
more name tuning
src/HOL/Data_Structures/Brother12_Map.thy
src/HOL/Data_Structures/Brother12_Set.thy
src/HOL/Data_Structures/Isin2.thy
src/HOL/Data_Structures/Lookup2.thy
src/HOL/Data_Structures/Map_Specs.thy
src/HOL/Data_Structures/Map_by_Ordered.thy
src/HOL/Data_Structures/Set_Interfaces.thy
src/HOL/Data_Structures/Set_Specs.thy
src/HOL/Data_Structures/Tree234_Map.thy
src/HOL/Data_Structures/Tree234_Set.thy
src/HOL/Data_Structures/Tree23_Map.thy
src/HOL/Data_Structures/Tree23_Set.thy
src/HOL/Data_Structures/Tree_Map.thy
src/HOL/Data_Structures/Tree_Set.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Data_Structures/Brother12_Map.thy	Sun Apr 08 09:46:33 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Brother12_Map.thy	Sun Apr 08 11:05:52 2018 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  theory Brother12_Map
     1.5  imports
     1.6    Brother12_Set
     1.7 -  Map_by_Ordered
     1.8 +  Map_Specs
     1.9  begin
    1.10  
    1.11  fun lookup :: "('a \<times> 'b) bro \<Rightarrow> 'a::linorder \<Rightarrow> 'b option" where
     2.1 --- a/src/HOL/Data_Structures/Brother12_Set.thy	Sun Apr 08 09:46:33 2018 +0200
     2.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Sun Apr 08 11:05:52 2018 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  theory Brother12_Set
     2.5  imports
     2.6    Cmp
     2.7 -  Set_Interfaces
     2.8 +  Set_Specs
     2.9    "HOL-Number_Theory.Fib"
    2.10  begin
    2.11  
     3.1 --- a/src/HOL/Data_Structures/Isin2.thy	Sun Apr 08 09:46:33 2018 +0200
     3.2 +++ b/src/HOL/Data_Structures/Isin2.thy	Sun Apr 08 11:05:52 2018 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  imports
     3.5    Tree2
     3.6    Cmp
     3.7 -  Set_Interfaces
     3.8 +  Set_Specs
     3.9  begin
    3.10  
    3.11  fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where
     4.1 --- a/src/HOL/Data_Structures/Lookup2.thy	Sun Apr 08 09:46:33 2018 +0200
     4.2 +++ b/src/HOL/Data_Structures/Lookup2.thy	Sun Apr 08 11:05:52 2018 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  imports
     4.5    Tree2
     4.6    Cmp
     4.7 -  Map_by_Ordered
     4.8 +  Map_Specs
     4.9  begin
    4.10  
    4.11  fun lookup :: "('a::linorder * 'b, 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Data_Structures/Map_Specs.thy	Sun Apr 08 11:05:52 2018 +0200
     5.3 @@ -0,0 +1,68 @@
     5.4 +(* Author: Tobias Nipkow *)
     5.5 +
     5.6 +section \<open>Specifications of Map ADT\<close>
     5.7 +
     5.8 +theory Map_Specs
     5.9 +imports AList_Upd_Del
    5.10 +begin
    5.11 +
    5.12 +text \<open>The basic map interface with traditional \<open>set\<close>-based specification:\<close>
    5.13 +
    5.14 +locale Map =
    5.15 +fixes empty :: "'m"
    5.16 +fixes update :: "'a \<Rightarrow> 'b \<Rightarrow> 'm \<Rightarrow> 'm"
    5.17 +fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm"
    5.18 +fixes lookup :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
    5.19 +fixes invar :: "'m \<Rightarrow> bool"
    5.20 +assumes map_empty: "lookup empty = (\<lambda>_. None)"
    5.21 +and map_update: "invar m \<Longrightarrow> lookup(update a b m) = (lookup m)(a := Some b)"
    5.22 +and map_delete: "invar m \<Longrightarrow> lookup(delete a m) = (lookup m)(a := None)"
    5.23 +and invar_empty: "invar empty"
    5.24 +and invar_update: "invar m \<Longrightarrow> invar(update a b m)"
    5.25 +and invar_delete: "invar m \<Longrightarrow> invar(delete a m)"
    5.26 +
    5.27 +
    5.28 +text \<open>The basic map interface with \<open>inorder\<close>-based specification:\<close>
    5.29 +
    5.30 +locale Map_by_Ordered =
    5.31 +fixes empty :: "'t"
    5.32 +fixes update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> 't \<Rightarrow> 't"
    5.33 +fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
    5.34 +fixes lookup :: "'t \<Rightarrow> 'a \<Rightarrow> 'b option"
    5.35 +fixes inorder :: "'t \<Rightarrow> ('a * 'b) list"
    5.36 +fixes inv :: "'t \<Rightarrow> bool"
    5.37 +assumes empty: "inorder empty = []"
    5.38 +and lookup: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    5.39 +  lookup t a = map_of (inorder t) a"
    5.40 +and update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    5.41 +  inorder(update a b t) = upd_list a b (inorder t)"
    5.42 +and delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    5.43 +  inorder(delete a t) = del_list a (inorder t)"
    5.44 +and inv_empty:  "inv empty"
    5.45 +and inv_update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(update a b t)"
    5.46 +and inv_delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(delete a t)"
    5.47 +begin
    5.48 +
    5.49 +text \<open>It implements the traditional specification:\<close>
    5.50 +
    5.51 +sublocale Map
    5.52 +  empty update delete lookup "\<lambda>t. inv t \<and> sorted1 (inorder t)"
    5.53 +proof(standard, goal_cases)
    5.54 +  case 1 show ?case by (auto simp: lookup empty inv_empty)
    5.55 +next
    5.56 +  case 2 thus ?case
    5.57 +    by(simp add: fun_eq_iff update inv_update map_of_ins_list lookup sorted_upd_list)
    5.58 +next
    5.59 +  case 3 thus ?case
    5.60 +    by(simp add: fun_eq_iff delete inv_delete map_of_del_list lookup sorted_del_list)
    5.61 +next
    5.62 +  case 4 thus ?case by(simp add: empty inv_empty)
    5.63 +next
    5.64 +  case 5 thus ?case by(simp add: update inv_update sorted_upd_list)
    5.65 +next
    5.66 +  case 6 thus ?case by (auto simp: delete inv_delete sorted_del_list)
    5.67 +qed
    5.68 +
    5.69 +end
    5.70 +
    5.71 +end
     6.1 --- a/src/HOL/Data_Structures/Map_by_Ordered.thy	Sun Apr 08 09:46:33 2018 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,61 +0,0 @@
     6.4 -(* Author: Tobias Nipkow *)
     6.5 -
     6.6 -section \<open>Implementing Ordered Maps\<close>
     6.7 -
     6.8 -theory Map_by_Ordered
     6.9 -imports AList_Upd_Del
    6.10 -begin
    6.11 -
    6.12 -locale Map =
    6.13 -fixes empty :: "'m"
    6.14 -fixes update :: "'a \<Rightarrow> 'b \<Rightarrow> 'm \<Rightarrow> 'm"
    6.15 -fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm"
    6.16 -fixes lookup :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
    6.17 -fixes invar :: "'m \<Rightarrow> bool"
    6.18 -assumes map_empty: "lookup empty = (\<lambda>_. None)"
    6.19 -and map_update: "invar m \<Longrightarrow> lookup(update a b m) = (lookup m)(a := Some b)"
    6.20 -and map_delete: "invar m \<Longrightarrow> lookup(delete a m) = (lookup m)(a := None)"
    6.21 -and invar_empty: "invar empty"
    6.22 -and invar_update: "invar m \<Longrightarrow> invar(update a b m)"
    6.23 -and invar_delete: "invar m \<Longrightarrow> invar(delete a m)"
    6.24 -
    6.25 -locale Map_by_Ordered =
    6.26 -fixes empty :: "'t"
    6.27 -fixes update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> 't \<Rightarrow> 't"
    6.28 -fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
    6.29 -fixes lookup :: "'t \<Rightarrow> 'a \<Rightarrow> 'b option"
    6.30 -fixes inorder :: "'t \<Rightarrow> ('a * 'b) list"
    6.31 -fixes inv :: "'t \<Rightarrow> bool"
    6.32 -assumes empty: "inorder empty = []"
    6.33 -and lookup: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    6.34 -  lookup t a = map_of (inorder t) a"
    6.35 -and update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    6.36 -  inorder(update a b t) = upd_list a b (inorder t)"
    6.37 -and delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    6.38 -  inorder(delete a t) = del_list a (inorder t)"
    6.39 -and inv_empty:  "inv empty"
    6.40 -and inv_update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(update a b t)"
    6.41 -and inv_delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(delete a t)"
    6.42 -begin
    6.43 -
    6.44 -sublocale Map
    6.45 -  empty update delete lookup "\<lambda>t. inv t \<and> sorted1 (inorder t)"
    6.46 -proof(standard, goal_cases)
    6.47 -  case 1 show ?case by (auto simp: lookup empty inv_empty)
    6.48 -next
    6.49 -  case 2 thus ?case
    6.50 -    by(simp add: fun_eq_iff update inv_update map_of_ins_list lookup sorted_upd_list)
    6.51 -next
    6.52 -  case 3 thus ?case
    6.53 -    by(simp add: fun_eq_iff delete inv_delete map_of_del_list lookup sorted_del_list)
    6.54 -next
    6.55 -  case 4 thus ?case by(simp add: empty inv_empty)
    6.56 -next
    6.57 -  case 5 thus ?case by(simp add: update inv_update sorted_upd_list)
    6.58 -next
    6.59 -  case 6 thus ?case by (auto simp: delete inv_delete sorted_del_list)
    6.60 -qed
    6.61 -
    6.62 -end
    6.63 -
    6.64 -end
     7.1 --- a/src/HOL/Data_Structures/Set_Interfaces.thy	Sun Apr 08 09:46:33 2018 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,86 +0,0 @@
     7.4 -(* Author: Tobias Nipkow *)
     7.5 -
     7.6 -section \<open>Interfaces for Set ADT\<close>
     7.7 -
     7.8 -theory Set_Interfaces
     7.9 -imports List_Ins_Del
    7.10 -begin
    7.11 -
    7.12 -text \<open>The basic set interface with traditional specification (based on \<open>set\<close> and \<open>bst\<close>):\<close>
    7.13 -
    7.14 -locale Set =
    7.15 -fixes empty :: "'s"
    7.16 -fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    7.17 -fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    7.18 -fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
    7.19 -fixes set :: "'s \<Rightarrow> 'a set"
    7.20 -fixes invar :: "'s \<Rightarrow> bool"
    7.21 -assumes set_empty:    "set empty = {}"
    7.22 -assumes set_isin:     "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
    7.23 -assumes set_insert:   "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
    7.24 -assumes set_delete:   "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
    7.25 -assumes invar_empty:  "invar empty"
    7.26 -assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
    7.27 -assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
    7.28 -
    7.29 -
    7.30 -text \<open>The basic set interface with \<open>inorder\<close>-based specification:\<close>
    7.31 -
    7.32 -locale Set_by_Ordered =
    7.33 -fixes empty :: "'t"
    7.34 -fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
    7.35 -fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
    7.36 -fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
    7.37 -fixes inorder :: "'t \<Rightarrow> 'a list"
    7.38 -fixes inv :: "'t \<Rightarrow> bool"
    7.39 -assumes empty: "inorder empty = []"
    7.40 -assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    7.41 -  isin t x = (x \<in> set (inorder t))"
    7.42 -assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    7.43 -  inorder(insert x t) = ins_list x (inorder t)"
    7.44 -assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    7.45 -  inorder(delete x t) = del_list x (inorder t)"
    7.46 -assumes inv_empty:  "inv empty"
    7.47 -assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
    7.48 -assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
    7.49 -begin
    7.50 -
    7.51 -text \<open>It implements the traditional specification:\<close>
    7.52 -
    7.53 -sublocale Set
    7.54 -  empty insert delete isin "set o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
    7.55 -proof(standard, goal_cases)
    7.56 -  case 1 show ?case by (auto simp: empty)
    7.57 -next
    7.58 -  case 2 thus ?case by(simp add: isin)
    7.59 -next
    7.60 -  case 3 thus ?case by(simp add: insert set_ins_list)
    7.61 -next
    7.62 -  case (4 s x) thus ?case
    7.63 -    using delete[OF 4, of x] by (auto simp: distinct_if_sorted set_del_list_eq)
    7.64 -next
    7.65 -  case 5 thus ?case by(simp add: empty inv_empty)
    7.66 -next
    7.67 -  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
    7.68 -next
    7.69 -  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
    7.70 -qed
    7.71 -
    7.72 -end
    7.73 -
    7.74 -
    7.75 -text \<open>Set2 = Set with binary operations:\<close>
    7.76 -
    7.77 -locale Set2 = Set
    7.78 -  where insert = insert for insert :: "'a \<Rightarrow> 's \<Rightarrow> 's" (*for typing purposes only*) +
    7.79 -fixes union :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    7.80 -fixes inter :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    7.81 -fixes diff  :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    7.82 -assumes set_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(union s1 s2) = set s1 \<union> set s2"
    7.83 -assumes set_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(inter s1 s2) = set s1 \<inter> set s2"
    7.84 -assumes set_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(diff s1 s2) = set s1 - set s2"
    7.85 -assumes invar_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(union s1 s2)"
    7.86 -assumes invar_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(inter s1 s2)"
    7.87 -assumes invar_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(diff s1 s2)"
    7.88 -
    7.89 -end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Data_Structures/Set_Specs.thy	Sun Apr 08 11:05:52 2018 +0200
     8.3 @@ -0,0 +1,86 @@
     8.4 +(* Author: Tobias Nipkow *)
     8.5 +
     8.6 +section \<open>Specifications of Set ADT\<close>
     8.7 +
     8.8 +theory Set_Specs
     8.9 +imports List_Ins_Del
    8.10 +begin
    8.11 +
    8.12 +text \<open>The basic set interface with traditional \<open>set\<close>-based specification:\<close>
    8.13 +
    8.14 +locale Set =
    8.15 +fixes empty :: "'s"
    8.16 +fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    8.17 +fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    8.18 +fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
    8.19 +fixes set :: "'s \<Rightarrow> 'a set"
    8.20 +fixes invar :: "'s \<Rightarrow> bool"
    8.21 +assumes set_empty:    "set empty = {}"
    8.22 +assumes set_isin:     "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
    8.23 +assumes set_insert:   "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
    8.24 +assumes set_delete:   "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
    8.25 +assumes invar_empty:  "invar empty"
    8.26 +assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
    8.27 +assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
    8.28 +
    8.29 +
    8.30 +text \<open>The basic set interface with \<open>inorder\<close>-based specification:\<close>
    8.31 +
    8.32 +locale Set_by_Ordered =
    8.33 +fixes empty :: "'t"
    8.34 +fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
    8.35 +fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
    8.36 +fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
    8.37 +fixes inorder :: "'t \<Rightarrow> 'a list"
    8.38 +fixes inv :: "'t \<Rightarrow> bool"
    8.39 +assumes empty: "inorder empty = []"
    8.40 +assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    8.41 +  isin t x = (x \<in> set (inorder t))"
    8.42 +assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    8.43 +  inorder(insert x t) = ins_list x (inorder t)"
    8.44 +assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    8.45 +  inorder(delete x t) = del_list x (inorder t)"
    8.46 +assumes inv_empty:  "inv empty"
    8.47 +assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
    8.48 +assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
    8.49 +begin
    8.50 +
    8.51 +text \<open>It implements the traditional specification:\<close>
    8.52 +
    8.53 +sublocale Set
    8.54 +  empty insert delete isin "set o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
    8.55 +proof(standard, goal_cases)
    8.56 +  case 1 show ?case by (auto simp: empty)
    8.57 +next
    8.58 +  case 2 thus ?case by(simp add: isin)
    8.59 +next
    8.60 +  case 3 thus ?case by(simp add: insert set_ins_list)
    8.61 +next
    8.62 +  case (4 s x) thus ?case
    8.63 +    using delete[OF 4, of x] by (auto simp: distinct_if_sorted set_del_list_eq)
    8.64 +next
    8.65 +  case 5 thus ?case by(simp add: empty inv_empty)
    8.66 +next
    8.67 +  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
    8.68 +next
    8.69 +  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
    8.70 +qed
    8.71 +
    8.72 +end
    8.73 +
    8.74 +
    8.75 +text \<open>Set2 = Set with binary operations:\<close>
    8.76 +
    8.77 +locale Set2 = Set
    8.78 +  where insert = insert for insert :: "'a \<Rightarrow> 's \<Rightarrow> 's" (*for typing purposes only*) +
    8.79 +fixes union :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    8.80 +fixes inter :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    8.81 +fixes diff  :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    8.82 +assumes set_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(union s1 s2) = set s1 \<union> set s2"
    8.83 +assumes set_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(inter s1 s2) = set s1 \<inter> set s2"
    8.84 +assumes set_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(diff s1 s2) = set s1 - set s2"
    8.85 +assumes invar_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(union s1 s2)"
    8.86 +assumes invar_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(inter s1 s2)"
    8.87 +assumes invar_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(diff s1 s2)"
    8.88 +
    8.89 +end
     9.1 --- a/src/HOL/Data_Structures/Tree234_Map.thy	Sun Apr 08 09:46:33 2018 +0200
     9.2 +++ b/src/HOL/Data_Structures/Tree234_Map.thy	Sun Apr 08 11:05:52 2018 +0200
     9.3 @@ -5,7 +5,7 @@
     9.4  theory Tree234_Map
     9.5  imports
     9.6    Tree234_Set
     9.7 -  "../Data_Structures/Map_by_Ordered"
     9.8 +  Map_Specs
     9.9  begin
    9.10  
    9.11  subsection \<open>Map operations on 2-3-4 trees\<close>
    10.1 --- a/src/HOL/Data_Structures/Tree234_Set.thy	Sun Apr 08 09:46:33 2018 +0200
    10.2 +++ b/src/HOL/Data_Structures/Tree234_Set.thy	Sun Apr 08 11:05:52 2018 +0200
    10.3 @@ -6,7 +6,7 @@
    10.4  imports
    10.5    Tree234
    10.6    Cmp
    10.7 -  "Set_Interfaces"
    10.8 +  Set_Specs
    10.9  begin
   10.10  
   10.11  subsection \<open>Set operations on 2-3-4 trees\<close>
    11.1 --- a/src/HOL/Data_Structures/Tree23_Map.thy	Sun Apr 08 09:46:33 2018 +0200
    11.2 +++ b/src/HOL/Data_Structures/Tree23_Map.thy	Sun Apr 08 11:05:52 2018 +0200
    11.3 @@ -5,7 +5,7 @@
    11.4  theory Tree23_Map
    11.5  imports
    11.6    Tree23_Set
    11.7 -  Map_by_Ordered
    11.8 +  Map_Specs
    11.9  begin
   11.10  
   11.11  fun lookup :: "('a::linorder * 'b) tree23 \<Rightarrow> 'a \<Rightarrow> 'b option" where
    12.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Sun Apr 08 09:46:33 2018 +0200
    12.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Sun Apr 08 11:05:52 2018 +0200
    12.3 @@ -6,7 +6,7 @@
    12.4  imports
    12.5    Tree23
    12.6    Cmp
    12.7 -  Set_Interfaces
    12.8 +  Set_Specs
    12.9  begin
   12.10  
   12.11  fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
    13.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Sun Apr 08 09:46:33 2018 +0200
    13.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Sun Apr 08 11:05:52 2018 +0200
    13.3 @@ -5,7 +5,7 @@
    13.4  theory Tree_Map
    13.5  imports
    13.6    Tree_Set
    13.7 -  Map_by_Ordered
    13.8 +  Map_Specs
    13.9  begin
   13.10  
   13.11  fun lookup :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
    14.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Sun Apr 08 09:46:33 2018 +0200
    14.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Sun Apr 08 11:05:52 2018 +0200
    14.3 @@ -6,7 +6,7 @@
    14.4  imports
    14.5    "HOL-Library.Tree"
    14.6    Cmp
    14.7 -  Set_Interfaces
    14.8 +  Set_Specs
    14.9  begin
   14.10  
   14.11  fun isin :: "'a::linorder tree \<Rightarrow> 'a \<Rightarrow> bool" where
    15.1 --- a/src/HOL/ROOT	Sun Apr 08 09:46:33 2018 +0200
    15.2 +++ b/src/HOL/ROOT	Sun Apr 08 11:05:52 2018 +0200
    15.3 @@ -201,6 +201,8 @@
    15.4      Tree234_Map
    15.5      Brother12_Map
    15.6      AA_Map
    15.7 +    Set2_BST_Join
    15.8 +    Set2_BST2_Join_RBT
    15.9      Leftist_Heap
   15.10      Binomial_Heap
   15.11    document_files "root.tex" "root.bib"