49 code_datatype Set Coset |
49 code_datatype Set Coset |
50 |
50 |
51 lemma member_code [code]: |
51 lemma member_code [code]: |
52 "member (Set xs) = List.member xs" |
52 "member (Set xs) = List.member xs" |
53 "member (Coset xs) = Not \<circ> List.member xs" |
53 "member (Coset xs) = Not \<circ> List.member xs" |
54 by (simp_all add: expand_fun_eq mem_iff fun_Compl_def bool_Compl_def) |
54 by (simp_all add: expand_fun_eq member_def fun_Compl_def bool_Compl_def) |
55 |
55 |
56 lemma member_image_UNIV [simp]: |
56 lemma member_image_UNIV [simp]: |
57 "member ` UNIV = UNIV" |
57 "member ` UNIV = UNIV" |
58 proof - |
58 proof - |
59 have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a fset. A = member B" |
59 have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a fset. A = member B" |
139 |
139 |
140 definition is_empty :: "'a fset \<Rightarrow> bool" where |
140 definition is_empty :: "'a fset \<Rightarrow> bool" where |
141 [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)" |
141 [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)" |
142 |
142 |
143 lemma is_empty_Set [code]: |
143 lemma is_empty_Set [code]: |
144 "is_empty (Set xs) \<longleftrightarrow> null xs" |
144 "is_empty (Set xs) \<longleftrightarrow> List.null xs" |
145 by (simp add: is_empty_set) |
145 by (simp add: is_empty_set) |
146 |
146 |
147 lemma empty_Set [code]: |
147 lemma empty_Set [code]: |
148 "bot = Set []" |
148 "bot = Set []" |
149 by (simp add: Set_def) |
149 by (simp add: Set_def) |
186 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
186 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
187 [simp]: "forall P A \<longleftrightarrow> Ball (member A) P" |
187 [simp]: "forall P A \<longleftrightarrow> Ball (member A) P" |
188 |
188 |
189 lemma forall_Set [code]: |
189 lemma forall_Set [code]: |
190 "forall P (Set xs) \<longleftrightarrow> list_all P xs" |
190 "forall P (Set xs) \<longleftrightarrow> list_all P xs" |
191 by (simp add: Set_def ball_set) |
191 by (simp add: Set_def list_all_iff) |
192 |
192 |
193 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
193 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
194 [simp]: "exists P A \<longleftrightarrow> Bex (member A) P" |
194 [simp]: "exists P A \<longleftrightarrow> Bex (member A) P" |
195 |
195 |
196 lemma exists_Set [code]: |
196 lemma exists_Set [code]: |
197 "exists P (Set xs) \<longleftrightarrow> list_ex P xs" |
197 "exists P (Set xs) \<longleftrightarrow> list_ex P xs" |
198 by (simp add: Set_def bex_set) |
198 by (simp add: Set_def list_ex_iff) |
199 |
199 |
200 definition card :: "'a fset \<Rightarrow> nat" where |
200 definition card :: "'a fset \<Rightarrow> nat" where |
201 [simp]: "card A = Finite_Set.card (member A)" |
201 [simp]: "card A = Finite_Set.card (member A)" |
202 |
202 |
203 lemma card_Set [code]: |
203 lemma card_Set [code]: |