1.1 --- a/src/HOL/IsaMakefile Mon Jun 29 12:18:54 2009 +0200
1.2 +++ b/src/HOL/IsaMakefile Mon Jun 29 12:18:55 2009 +0200
1.3 @@ -319,7 +319,7 @@
1.4 Library/Abstract_Rat.thy \
1.5 Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy \
1.6 Library/Euclidean_Space.thy Library/Sum_Of_Squares.thy Library/positivstellensatz.ML \
1.7 - Library/Code_Set.thy Library/Convex_Euclidean_Space.thy \
1.8 + Library/Fset.thy Library/Convex_Euclidean_Space.thy \
1.9 Library/sum_of_squares.ML Library/Glbs.thy Library/normarith.ML \
1.10 Library/Executable_Set.thy Library/Infinite_Set.thy \
1.11 Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
2.1 --- a/src/HOL/Library/Code_Set.thy Mon Jun 29 12:18:54 2009 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,224 +0,0 @@
2.4 -
2.5 -(* Author: Florian Haftmann, TU Muenchen *)
2.6 -
2.7 -header {* Executable finite sets *}
2.8 -
2.9 -theory Code_Set
2.10 -imports List_Set
2.11 -begin
2.12 -
2.13 -lemma foldl_apply_inv:
2.14 - assumes "\<And>x. g (h x) = x"
2.15 - shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
2.16 - by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
2.17 -
2.18 -declare mem_def [simp]
2.19 -
2.20 -subsection {* Lifting *}
2.21 -
2.22 -datatype 'a fset = Fset "'a set"
2.23 -
2.24 -primrec member :: "'a fset \<Rightarrow> 'a set" where
2.25 - "member (Fset A) = A"
2.26 -
2.27 -lemma Fset_member [simp]:
2.28 - "Fset (member A) = A"
2.29 - by (cases A) simp
2.30 -
2.31 -definition Set :: "'a list \<Rightarrow> 'a fset" where
2.32 - "Set xs = Fset (set xs)"
2.33 -
2.34 -lemma member_Set [simp]:
2.35 - "member (Set xs) = set xs"
2.36 - by (simp add: Set_def)
2.37 -
2.38 -code_datatype Set
2.39 -
2.40 -
2.41 -subsection {* Basic operations *}
2.42 -
2.43 -definition is_empty :: "'a fset \<Rightarrow> bool" where
2.44 - [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
2.45 -
2.46 -lemma is_empty_Set [code]:
2.47 - "is_empty (Set xs) \<longleftrightarrow> null xs"
2.48 - by (simp add: is_empty_set)
2.49 -
2.50 -definition empty :: "'a fset" where
2.51 - [simp]: "empty = Fset {}"
2.52 -
2.53 -lemma empty_Set [code]:
2.54 - "empty = Set []"
2.55 - by (simp add: Set_def)
2.56 -
2.57 -definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
2.58 - [simp]: "insert x A = Fset (Set.insert x (member A))"
2.59 -
2.60 -lemma insert_Set [code]:
2.61 - "insert x (Set xs) = Set (List_Set.insert x xs)"
2.62 - by (simp add: Set_def insert_set)
2.63 -
2.64 -definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
2.65 - [simp]: "remove x A = Fset (List_Set.remove x (member A))"
2.66 -
2.67 -lemma remove_Set [code]:
2.68 - "remove x (Set xs) = Set (remove_all x xs)"
2.69 - by (simp add: Set_def remove_set)
2.70 -
2.71 -definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
2.72 - [simp]: "map f A = Fset (image f (member A))"
2.73 -
2.74 -lemma map_Set [code]:
2.75 - "map f (Set xs) = Set (remdups (List.map f xs))"
2.76 - by (simp add: Set_def)
2.77 -
2.78 -definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
2.79 - [simp]: "filter P A = Fset (List_Set.project P (member A))"
2.80 -
2.81 -lemma filter_Set [code]:
2.82 - "filter P (Set xs) = Set (List.filter P xs)"
2.83 - by (simp add: Set_def project_set)
2.84 -
2.85 -definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
2.86 - [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
2.87 -
2.88 -lemma forall_Set [code]:
2.89 - "forall P (Set xs) \<longleftrightarrow> list_all P xs"
2.90 - by (simp add: Set_def ball_set)
2.91 -
2.92 -definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
2.93 - [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
2.94 -
2.95 -lemma exists_Set [code]:
2.96 - "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
2.97 - by (simp add: Set_def bex_set)
2.98 -
2.99 -
2.100 -subsection {* Derived operations *}
2.101 -
2.102 -lemma member_exists [code]:
2.103 - "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A"
2.104 - by simp
2.105 -
2.106 -definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
2.107 - [simp]: "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B"
2.108 -
2.109 -lemma subfset_eq_forall [code]:
2.110 - "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A"
2.111 - by (simp add: subset_eq)
2.112 -
2.113 -definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
2.114 - [simp]: "subfset A B \<longleftrightarrow> member A \<subset> member B"
2.115 -
2.116 -lemma subfset_subfset_eq [code]:
2.117 - "subfset A B \<longleftrightarrow> subfset_eq A B \<and> \<not> subfset_eq B A"
2.118 - by (simp add: subset)
2.119 -
2.120 -lemma eq_fset_subfset_eq [code]:
2.121 - "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A"
2.122 - by (cases A, cases B) (simp add: eq set_eq)
2.123 -
2.124 -definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
2.125 - [simp]: "inter A B = Fset (project (member A) (member B))"
2.126 -
2.127 -lemma inter_project [code]:
2.128 - "inter A B = filter (member A) B"
2.129 - by (simp add: inter)
2.130 -
2.131 -
2.132 -subsection {* Functorial operations *}
2.133 -
2.134 -definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
2.135 - [simp]: "union A B = Fset (member A \<union> member B)"
2.136 -
2.137 -lemma union_insert [code]:
2.138 - "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
2.139 -proof -
2.140 - have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
2.141 - member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
2.142 - by (rule foldl_apply_inv) simp
2.143 - then show ?thesis by (simp add: union_set)
2.144 -qed
2.145 -
2.146 -definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
2.147 - [simp]: "subtract A B = Fset (member B - member A)"
2.148 -
2.149 -lemma subtract_remove [code]:
2.150 - "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
2.151 -proof -
2.152 - have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
2.153 - member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
2.154 - by (rule foldl_apply_inv) simp
2.155 - then show ?thesis by (simp add: minus_set)
2.156 -qed
2.157 -
2.158 -definition Inter :: "'a fset fset \<Rightarrow> 'a fset" where
2.159 - [simp]: "Inter A = Fset (Set.Inter (member ` member A))"
2.160 -
2.161 -lemma Inter_inter [code]:
2.162 - "Inter (Set (A # As)) = foldl inter A As"
2.163 -proof -
2.164 - note Inter_image_eq [simp del] set_map [simp del] set.simps [simp del]
2.165 - have "foldl (op \<inter>) (member A) (List.map member As) =
2.166 - member (foldl (\<lambda>B A. Fset (member B \<inter> A)) A (List.map member As))"
2.167 - by (rule foldl_apply_inv) simp
2.168 - then show ?thesis
2.169 - by (simp add: Inter_set image_set inter_def_raw inter foldl_map)
2.170 -qed
2.171 -
2.172 -definition Union :: "'a fset fset \<Rightarrow> 'a fset" where
2.173 - [simp]: "Union A = Fset (Set.Union (member ` member A))"
2.174 -
2.175 -lemma Union_union [code]:
2.176 - "Union (Set As) = foldl union empty As"
2.177 -proof -
2.178 - note Union_image_eq [simp del] set_map [simp del]
2.179 - have "foldl (op \<union>) (member empty) (List.map member As) =
2.180 - member (foldl (\<lambda>B A. Fset (member B \<union> A)) empty (List.map member As))"
2.181 - by (rule foldl_apply_inv) simp
2.182 - then show ?thesis
2.183 - by (simp add: Union_set image_set union_def_raw foldl_map)
2.184 -qed
2.185 -
2.186 -
2.187 -subsection {* Misc operations *}
2.188 -
2.189 -lemma size_fset [code]:
2.190 - "fset_size f A = 0"
2.191 - "size A = 0"
2.192 - by (cases A, simp) (cases A, simp)
2.193 -
2.194 -lemma fset_case_code [code]:
2.195 - "fset_case f A = f (member A)"
2.196 - by (cases A) simp
2.197 -
2.198 -lemma fset_rec_code [code]:
2.199 - "fset_rec f A = f (member A)"
2.200 - by (cases A) simp
2.201 -
2.202 -
2.203 -subsection {* Simplified simprules *}
2.204 -
2.205 -lemma is_empty_simp [simp]:
2.206 - "is_empty A \<longleftrightarrow> member A = {}"
2.207 - by (simp add: List_Set.is_empty_def)
2.208 -declare is_empty_def [simp del]
2.209 -
2.210 -lemma remove_simp [simp]:
2.211 - "remove x A = Fset (member A - {x})"
2.212 - by (simp add: List_Set.remove_def)
2.213 -declare remove_def [simp del]
2.214 -
2.215 -lemma filter_simp [simp]:
2.216 - "filter P A = Fset {x \<in> member A. P x}"
2.217 - by (simp add: List_Set.project_def)
2.218 -declare filter_def [simp del]
2.219 -
2.220 -lemma inter_simp [simp]:
2.221 - "inter A B = Fset (member A \<inter> member B)"
2.222 - by (simp add: inter)
2.223 -declare inter_def [simp del]
2.224 -
2.225 -declare mem_def [simp del]
2.226 -
2.227 -end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Library/Fset.thy Mon Jun 29 12:18:55 2009 +0200
3.3 @@ -0,0 +1,240 @@
3.4 +
3.5 +(* Author: Florian Haftmann, TU Muenchen *)
3.6 +
3.7 +header {* Executable finite sets *}
3.8 +
3.9 +theory Fset
3.10 +imports List_Set
3.11 +begin
3.12 +
3.13 +lemma foldl_apply_inv:
3.14 + assumes "\<And>x. g (h x) = x"
3.15 + shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
3.16 + by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
3.17 +
3.18 +declare mem_def [simp]
3.19 +
3.20 +
3.21 +subsection {* Lifting *}
3.22 +
3.23 +datatype 'a fset = Fset "'a set"
3.24 +
3.25 +primrec member :: "'a fset \<Rightarrow> 'a set" where
3.26 + "member (Fset A) = A"
3.27 +
3.28 +lemma Fset_member [simp]:
3.29 + "Fset (member A) = A"
3.30 + by (cases A) simp
3.31 +
3.32 +definition Set :: "'a list \<Rightarrow> 'a fset" where
3.33 + "Set xs = Fset (set xs)"
3.34 +
3.35 +lemma member_Set [simp]:
3.36 + "member (Set xs) = set xs"
3.37 + by (simp add: Set_def)
3.38 +
3.39 +code_datatype Set
3.40 +
3.41 +
3.42 +subsection {* Basic operations *}
3.43 +
3.44 +definition is_empty :: "'a fset \<Rightarrow> bool" where
3.45 + [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
3.46 +
3.47 +lemma is_empty_Set [code]:
3.48 + "is_empty (Set xs) \<longleftrightarrow> null xs"
3.49 + by (simp add: is_empty_set)
3.50 +
3.51 +definition empty :: "'a fset" where
3.52 + [simp]: "empty = Fset {}"
3.53 +
3.54 +lemma empty_Set [code]:
3.55 + "empty = Set []"
3.56 + by (simp add: Set_def)
3.57 +
3.58 +definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
3.59 + [simp]: "insert x A = Fset (Set.insert x (member A))"
3.60 +
3.61 +lemma insert_Set [code]:
3.62 + "insert x (Set xs) = Set (List_Set.insert x xs)"
3.63 + by (simp add: Set_def insert_set)
3.64 +
3.65 +definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
3.66 + [simp]: "remove x A = Fset (List_Set.remove x (member A))"
3.67 +
3.68 +lemma remove_Set [code]:
3.69 + "remove x (Set xs) = Set (remove_all x xs)"
3.70 + by (simp add: Set_def remove_set)
3.71 +
3.72 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
3.73 + [simp]: "map f A = Fset (image f (member A))"
3.74 +
3.75 +lemma map_Set [code]:
3.76 + "map f (Set xs) = Set (remdups (List.map f xs))"
3.77 + by (simp add: Set_def)
3.78 +
3.79 +definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
3.80 + [simp]: "filter P A = Fset (List_Set.project P (member A))"
3.81 +
3.82 +lemma filter_Set [code]:
3.83 + "filter P (Set xs) = Set (List.filter P xs)"
3.84 + by (simp add: Set_def project_set)
3.85 +
3.86 +definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
3.87 + [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
3.88 +
3.89 +lemma forall_Set [code]:
3.90 + "forall P (Set xs) \<longleftrightarrow> list_all P xs"
3.91 + by (simp add: Set_def ball_set)
3.92 +
3.93 +definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
3.94 + [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
3.95 +
3.96 +lemma exists_Set [code]:
3.97 + "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
3.98 + by (simp add: Set_def bex_set)
3.99 +
3.100 +definition card :: "'a fset \<Rightarrow> nat" where
3.101 + [simp]: "card A = Finite_Set.card (member A)"
3.102 +
3.103 +lemma card_Set [code]:
3.104 + "card (Set xs) = length (remdups xs)"
3.105 +proof -
3.106 + have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
3.107 + by (rule distinct_card) simp
3.108 + then show ?thesis by (simp add: Set_def card_def)
3.109 +qed
3.110 +
3.111 +
3.112 +subsection {* Derived operations *}
3.113 +
3.114 +lemma member_exists [code]:
3.115 + "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A"
3.116 + by simp
3.117 +
3.118 +definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
3.119 + [simp]: "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B"
3.120 +
3.121 +lemma subfset_eq_forall [code]:
3.122 + "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A"
3.123 + by (simp add: subset_eq)
3.124 +
3.125 +definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
3.126 + [simp]: "subfset A B \<longleftrightarrow> member A \<subset> member B"
3.127 +
3.128 +lemma subfset_subfset_eq [code]:
3.129 + "subfset A B \<longleftrightarrow> subfset_eq A B \<and> \<not> subfset_eq B A"
3.130 + by (simp add: subset)
3.131 +
3.132 +lemma eq_fset_subfset_eq [code]:
3.133 + "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A"
3.134 + by (cases A, cases B) (simp add: eq set_eq)
3.135 +
3.136 +definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
3.137 + [simp]: "inter A B = Fset (project (member A) (member B))"
3.138 +
3.139 +lemma inter_project [code]:
3.140 + "inter A B = filter (member A) B"
3.141 + by (simp add: inter)
3.142 +
3.143 +
3.144 +subsection {* Functorial operations *}
3.145 +
3.146 +definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
3.147 + [simp]: "union A B = Fset (member A \<union> member B)"
3.148 +
3.149 +lemma union_insert [code]:
3.150 + "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
3.151 +proof -
3.152 + have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
3.153 + member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
3.154 + by (rule foldl_apply_inv) simp
3.155 + then show ?thesis by (simp add: union_set)
3.156 +qed
3.157 +
3.158 +definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
3.159 + [simp]: "subtract A B = Fset (member B - member A)"
3.160 +
3.161 +lemma subtract_remove [code]:
3.162 + "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
3.163 +proof -
3.164 + have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
3.165 + member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
3.166 + by (rule foldl_apply_inv) simp
3.167 + then show ?thesis by (simp add: minus_set)
3.168 +qed
3.169 +
3.170 +definition Inter :: "'a fset fset \<Rightarrow> 'a fset" where
3.171 + [simp]: "Inter A = Fset (Set.Inter (member ` member A))"
3.172 +
3.173 +lemma Inter_inter [code]:
3.174 + "Inter (Set (A # As)) = foldl inter A As"
3.175 +proof -
3.176 + note Inter_image_eq [simp del] set_map [simp del] set.simps [simp del]
3.177 + have "foldl (op \<inter>) (member A) (List.map member As) =
3.178 + member (foldl (\<lambda>B A. Fset (member B \<inter> A)) A (List.map member As))"
3.179 + by (rule foldl_apply_inv) simp
3.180 + then show ?thesis
3.181 + by (simp add: Inter_set image_set inter_def_raw inter foldl_map)
3.182 +qed
3.183 +
3.184 +definition Union :: "'a fset fset \<Rightarrow> 'a fset" where
3.185 + [simp]: "Union A = Fset (Set.Union (member ` member A))"
3.186 +
3.187 +lemma Union_union [code]:
3.188 + "Union (Set As) = foldl union empty As"
3.189 +proof -
3.190 + note Union_image_eq [simp del] set_map [simp del]
3.191 + have "foldl (op \<union>) (member empty) (List.map member As) =
3.192 + member (foldl (\<lambda>B A. Fset (member B \<union> A)) empty (List.map member As))"
3.193 + by (rule foldl_apply_inv) simp
3.194 + then show ?thesis
3.195 + by (simp add: Union_set image_set union_def_raw foldl_map)
3.196 +qed
3.197 +
3.198 +
3.199 +subsection {* Misc operations *}
3.200 +
3.201 +lemma size_fset [code]:
3.202 + "fset_size f A = 0"
3.203 + "size A = 0"
3.204 + by (cases A, simp) (cases A, simp)
3.205 +
3.206 +lemma fset_case_code [code]:
3.207 + "fset_case f A = f (member A)"
3.208 + by (cases A) simp
3.209 +
3.210 +lemma fset_rec_code [code]:
3.211 + "fset_rec f A = f (member A)"
3.212 + by (cases A) simp
3.213 +
3.214 +
3.215 +subsection {* Simplified simprules *}
3.216 +
3.217 +lemma is_empty_simp [simp]:
3.218 + "is_empty A \<longleftrightarrow> member A = {}"
3.219 + by (simp add: List_Set.is_empty_def)
3.220 +declare is_empty_def [simp del]
3.221 +
3.222 +lemma remove_simp [simp]:
3.223 + "remove x A = Fset (member A - {x})"
3.224 + by (simp add: List_Set.remove_def)
3.225 +declare remove_def [simp del]
3.226 +
3.227 +lemma filter_simp [simp]:
3.228 + "filter P A = Fset {x \<in> member A. P x}"
3.229 + by (simp add: List_Set.project_def)
3.230 +declare filter_def [simp del]
3.231 +
3.232 +lemma inter_simp [simp]:
3.233 + "inter A B = Fset (member A \<inter> member B)"
3.234 + by (simp add: inter)
3.235 +declare inter_def [simp del]
3.236 +
3.237 +declare mem_def [simp del]
3.238 +
3.239 +
3.240 +hide (open) const is_empty empty insert remove map filter forall exists card
3.241 + subfset_eq subfset inter union subtract Inter Union
3.242 +
3.243 +end
4.1 --- a/src/HOL/Library/Library.thy Mon Jun 29 12:18:54 2009 +0200
4.2 +++ b/src/HOL/Library/Library.thy Mon Jun 29 12:18:55 2009 +0200
4.3 @@ -10,7 +10,6 @@
4.4 Char_ord
4.5 Code_Char_chr
4.6 Code_Integer
4.7 - Code_Set
4.8 Coinductive_List
4.9 Commutative_Ring
4.10 Continuity
4.11 @@ -28,6 +27,7 @@
4.12 Formal_Power_Series
4.13 Fraction_Field
4.14 FrechetDeriv
4.15 + Fset
4.16 FuncSet
4.17 Fundamental_Theorem_Algebra
4.18 Infinite_Set
5.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy Mon Jun 29 12:18:54 2009 +0200
5.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy Mon Jun 29 12:18:55 2009 +0200
5.3 @@ -8,7 +8,7 @@
5.4 Complex_Main
5.5 AssocList
5.6 Binomial
5.7 - Code_Set
5.8 + Fset
5.9 Commutative_Ring
5.10 Enum
5.11 List_Prefix