better name; added binary operations
authornipkow
Sun Apr 08 09:46:33 2018 +0200 (13 months ago)
changeset 6796408cc5ab18c84
parent 67963 9541f2c5ce8d
child 67965 aaa31cd0caef
better name; added binary operations
src/HOL/Data_Structures/AVL_Set.thy
src/HOL/Data_Structures/Brother12_Set.thy
src/HOL/Data_Structures/Isin2.thy
src/HOL/Data_Structures/Set_Interfaces.thy
src/HOL/Data_Structures/Set_by_Ordered.thy
src/HOL/Data_Structures/Tree234_Set.thy
src/HOL/Data_Structures/Tree23_Set.thy
src/HOL/Data_Structures/Tree_Set.thy
     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Sat Apr 07 22:09:57 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Sun Apr 08 09:46:33 2018 +0200
     1.3 @@ -7,8 +7,8 @@
     1.4  
     1.5  theory AVL_Set
     1.6  imports
     1.7 - Cmp
     1.8 - Isin2
     1.9 +  Cmp
    1.10 +  Isin2
    1.11    "HOL-Number_Theory.Fib"
    1.12  begin
    1.13  
     2.1 --- a/src/HOL/Data_Structures/Brother12_Set.thy	Sat Apr 07 22:09:57 2018 +0200
     2.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Sun Apr 08 09:46:33 2018 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  theory Brother12_Set
     2.5  imports
     2.6    Cmp
     2.7 -  Set_by_Ordered
     2.8 +  Set_Interfaces
     2.9    "HOL-Number_Theory.Fib"
    2.10  begin
    2.11  
     3.1 --- a/src/HOL/Data_Structures/Isin2.thy	Sat Apr 07 22:09:57 2018 +0200
     3.2 +++ b/src/HOL/Data_Structures/Isin2.thy	Sun Apr 08 09:46:33 2018 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  imports
     3.5    Tree2
     3.6    Cmp
     3.7 -  Set_by_Ordered
     3.8 +  Set_Interfaces
     3.9  begin
    3.10  
    3.11  fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Data_Structures/Set_Interfaces.thy	Sun Apr 08 09:46:33 2018 +0200
     4.3 @@ -0,0 +1,86 @@
     4.4 +(* Author: Tobias Nipkow *)
     4.5 +
     4.6 +section \<open>Interfaces for Set ADT\<close>
     4.7 +
     4.8 +theory Set_Interfaces
     4.9 +imports List_Ins_Del
    4.10 +begin
    4.11 +
    4.12 +text \<open>The basic set interface with traditional specification (based on \<open>set\<close> and \<open>bst\<close>):\<close>
    4.13 +
    4.14 +locale Set =
    4.15 +fixes empty :: "'s"
    4.16 +fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    4.17 +fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    4.18 +fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
    4.19 +fixes set :: "'s \<Rightarrow> 'a set"
    4.20 +fixes invar :: "'s \<Rightarrow> bool"
    4.21 +assumes set_empty:    "set empty = {}"
    4.22 +assumes set_isin:     "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
    4.23 +assumes set_insert:   "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
    4.24 +assumes set_delete:   "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
    4.25 +assumes invar_empty:  "invar empty"
    4.26 +assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
    4.27 +assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
    4.28 +
    4.29 +
    4.30 +text \<open>The basic set interface with \<open>inorder\<close>-based specification:\<close>
    4.31 +
    4.32 +locale Set_by_Ordered =
    4.33 +fixes empty :: "'t"
    4.34 +fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
    4.35 +fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
    4.36 +fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
    4.37 +fixes inorder :: "'t \<Rightarrow> 'a list"
    4.38 +fixes inv :: "'t \<Rightarrow> bool"
    4.39 +assumes empty: "inorder empty = []"
    4.40 +assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    4.41 +  isin t x = (x \<in> set (inorder t))"
    4.42 +assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    4.43 +  inorder(insert x t) = ins_list x (inorder t)"
    4.44 +assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    4.45 +  inorder(delete x t) = del_list x (inorder t)"
    4.46 +assumes inv_empty:  "inv empty"
    4.47 +assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
    4.48 +assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
    4.49 +begin
    4.50 +
    4.51 +text \<open>It implements the traditional specification:\<close>
    4.52 +
    4.53 +sublocale Set
    4.54 +  empty insert delete isin "set o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
    4.55 +proof(standard, goal_cases)
    4.56 +  case 1 show ?case by (auto simp: empty)
    4.57 +next
    4.58 +  case 2 thus ?case by(simp add: isin)
    4.59 +next
    4.60 +  case 3 thus ?case by(simp add: insert set_ins_list)
    4.61 +next
    4.62 +  case (4 s x) thus ?case
    4.63 +    using delete[OF 4, of x] by (auto simp: distinct_if_sorted set_del_list_eq)
    4.64 +next
    4.65 +  case 5 thus ?case by(simp add: empty inv_empty)
    4.66 +next
    4.67 +  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
    4.68 +next
    4.69 +  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
    4.70 +qed
    4.71 +
    4.72 +end
    4.73 +
    4.74 +
    4.75 +text \<open>Set2 = Set with binary operations:\<close>
    4.76 +
    4.77 +locale Set2 = Set
    4.78 +  where insert = insert for insert :: "'a \<Rightarrow> 's \<Rightarrow> 's" (*for typing purposes only*) +
    4.79 +fixes union :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    4.80 +fixes inter :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    4.81 +fixes diff  :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    4.82 +assumes set_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(union s1 s2) = set s1 \<union> set s2"
    4.83 +assumes set_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(inter s1 s2) = set s1 \<inter> set s2"
    4.84 +assumes set_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(diff s1 s2) = set s1 - set s2"
    4.85 +assumes invar_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(union s1 s2)"
    4.86 +assumes invar_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(inter s1 s2)"
    4.87 +assumes invar_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(diff s1 s2)"
    4.88 +
    4.89 +end
     5.1 --- a/src/HOL/Data_Structures/Set_by_Ordered.thy	Sat Apr 07 22:09:57 2018 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,64 +0,0 @@
     5.4 -(* Author: Tobias Nipkow *)
     5.5 -
     5.6 -section \<open>Implementing Ordered Sets\<close>
     5.7 -
     5.8 -theory Set_by_Ordered
     5.9 -imports List_Ins_Del
    5.10 -begin
    5.11 -
    5.12 -locale Set =
    5.13 -fixes empty :: "'s"
    5.14 -fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    5.15 -fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    5.16 -fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
    5.17 -fixes set :: "'s \<Rightarrow> 'a set"
    5.18 -fixes invar :: "'s \<Rightarrow> bool"
    5.19 -assumes set_empty:    "set empty = {}"
    5.20 -assumes set_isin:     "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
    5.21 -assumes set_insert:   "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
    5.22 -assumes set_delete:   "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
    5.23 -assumes invar_empty:  "invar empty"
    5.24 -assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
    5.25 -assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
    5.26 -
    5.27 -locale Set_by_Ordered =
    5.28 -fixes empty :: "'t"
    5.29 -fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
    5.30 -fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
    5.31 -fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
    5.32 -fixes inorder :: "'t \<Rightarrow> 'a list"
    5.33 -fixes inv :: "'t \<Rightarrow> bool"
    5.34 -assumes empty: "inorder empty = []"
    5.35 -assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    5.36 -  isin t x = (x \<in> set (inorder t))"
    5.37 -assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    5.38 -  inorder(insert x t) = ins_list x (inorder t)"
    5.39 -assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    5.40 -  inorder(delete x t) = del_list x (inorder t)"
    5.41 -assumes inv_empty:  "inv empty"
    5.42 -assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
    5.43 -assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
    5.44 -begin
    5.45 -
    5.46 -sublocale Set
    5.47 -  empty insert delete isin "set o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
    5.48 -proof(standard, goal_cases)
    5.49 -  case 1 show ?case by (auto simp: empty)
    5.50 -next
    5.51 -  case 2 thus ?case by(simp add: isin)
    5.52 -next
    5.53 -  case 3 thus ?case by(simp add: insert set_ins_list)
    5.54 -next
    5.55 -  case (4 s x) thus ?case
    5.56 -    using delete[OF 4, of x] by (auto simp: distinct_if_sorted set_del_list_eq)
    5.57 -next
    5.58 -  case 5 thus ?case by(simp add: empty inv_empty)
    5.59 -next
    5.60 -  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
    5.61 -next
    5.62 -  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
    5.63 -qed
    5.64 -
    5.65 -end
    5.66 -
    5.67 -end
     6.1 --- a/src/HOL/Data_Structures/Tree234_Set.thy	Sat Apr 07 22:09:57 2018 +0200
     6.2 +++ b/src/HOL/Data_Structures/Tree234_Set.thy	Sun Apr 08 09:46:33 2018 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  imports
     6.5    Tree234
     6.6    Cmp
     6.7 -  "../Data_Structures/Set_by_Ordered"
     6.8 +  "Set_Interfaces"
     6.9  begin
    6.10  
    6.11  subsection \<open>Set operations on 2-3-4 trees\<close>
     7.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Sat Apr 07 22:09:57 2018 +0200
     7.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Sun Apr 08 09:46:33 2018 +0200
     7.3 @@ -6,7 +6,7 @@
     7.4  imports
     7.5    Tree23
     7.6    Cmp
     7.7 -  Set_by_Ordered
     7.8 +  Set_Interfaces
     7.9  begin
    7.10  
    7.11  fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
     8.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Sat Apr 07 22:09:57 2018 +0200
     8.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Sun Apr 08 09:46:33 2018 +0200
     8.3 @@ -6,7 +6,7 @@
     8.4  imports
     8.5    "HOL-Library.Tree"
     8.6    Cmp
     8.7 -  Set_by_Ordered
     8.8 +  Set_Interfaces
     8.9  begin
    8.10  
    8.11  fun isin :: "'a::linorder tree \<Rightarrow> 'a \<Rightarrow> bool" where