equal
deleted
inserted
replaced
32 "(op = ===> op \<approx> ===> op =) (op mem) (op mem)" |
32 "(op = ===> op \<approx> ===> op =) (op mem) (op mem)" |
33 *) |
33 *) |
34 |
34 |
35 |
35 |
36 lemma no_mem_nil: |
36 lemma no_mem_nil: |
37 "(\<forall>a. \<not>(a \<in> set A)) = (A = [])" |
37 "(\<forall>a. a \<notin> set A) = (A = [])" |
38 by (induct A) (auto) |
38 by (induct A) (auto) |
39 |
39 |
40 lemma none_mem_nil: |
40 lemma none_mem_nil: |
41 "(\<forall>a. \<not>(a \<in> set A)) = (A \<approx> [])" |
41 "(\<forall>a. a \<notin> set A) = (A \<approx> [])" |
42 by simp |
42 by simp |
43 |
43 |
44 lemma mem_cons: |
44 lemma mem_cons: |
45 "a \<in> set A \<Longrightarrow> a # A \<approx> A" |
45 "a \<in> set A \<Longrightarrow> a # A \<approx> A" |
46 by auto |
46 by auto |
233 quotient_def |
233 quotient_def |
234 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
234 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
235 as "delete_raw" |
235 as "delete_raw" |
236 |
236 |
237 quotient_def |
237 quotient_def |
238 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<in>f _" [50, 51] 50) |
238 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [50, 51] 50) |
239 as "op @" |
239 as "op @" |
240 |
240 |
241 quotient_def |
241 quotient_def |
242 "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70) |
242 "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70) |
243 as "inter_raw" |
243 as "inter_raw" |
265 |
265 |
266 (* thm MEM: |
266 (* thm MEM: |
267 MEM x [] = F |
267 MEM x [] = F |
268 MEM x (h::t) = (x=h) \/ MEM x t *) |
268 MEM x (h::t) = (x=h) \/ MEM x t *) |
269 thm none_mem_nil |
269 thm none_mem_nil |
|
270 (*lemma "(\<forall>a. a \<notin>f A) = (A = fempty)"*) |
|
271 |
270 thm mem_cons |
272 thm mem_cons |
271 thm finite_set_raw_strong_cases |
273 thm finite_set_raw_strong_cases |
272 thm card_raw.simps |
274 thm card_raw.simps |
273 thm not_mem_card_raw |
275 thm not_mem_card_raw |
274 thm card_raw_suc |
276 thm card_raw_suc |