equal
deleted
inserted
replaced
76 and "\<not> (x # xs \<approx> [])" |
76 and "\<not> (x # xs \<approx> [])" |
77 by auto |
77 by auto |
78 |
78 |
79 lemma not_memb_nil: |
79 lemma not_memb_nil: |
80 shows "\<not> memb x []" |
80 shows "\<not> memb x []" |
|
81 by (simp add: memb_def) |
|
82 |
|
83 lemma no_memb_nil: |
|
84 "(\<forall>x. \<not> memb x xs) = (xs = [])" |
|
85 by (simp add: memb_def) |
|
86 |
|
87 lemma none_memb_nil: |
|
88 "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])" |
81 by (simp add: memb_def) |
89 by (simp add: memb_def) |
82 |
90 |
83 lemma memb_cons_iff: |
91 lemma memb_cons_iff: |
84 shows "memb x (y # xs) = (x = y \<or> memb x xs)" |
92 shows "memb x (y # xs) = (x = y \<or> memb x xs)" |
85 by (induct xs) (auto simp add: memb_def) |
93 by (induct xs) (auto simp add: memb_def) |
159 done |
167 done |
160 |
168 |
161 lemma fcard_raw_delete_one: |
169 lemma fcard_raw_delete_one: |
162 shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" |
170 shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" |
163 by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def) |
171 by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def) |
|
172 |
|
173 lemma fcard_raw_suc_memb: |
|
174 assumes a: "fcard_raw A = Suc n" |
|
175 shows "\<exists>a. memb a A" |
|
176 using a |
|
177 apply (induct A) |
|
178 apply simp |
|
179 apply (rule_tac x="a" in exI) |
|
180 apply (simp add: memb_def) |
|
181 done |
|
182 |
|
183 lemma mem_card_not_0: |
|
184 assumes a: "memb a A" |
|
185 shows "\<not>(fcard_raw A = 0)" |
|
186 by (metis a fcard_raw_0 none_memb_nil) |
164 |
187 |
165 lemma fcard_raw_rsp_aux: |
188 lemma fcard_raw_rsp_aux: |
166 assumes a: "xs \<approx> ys" |
189 assumes a: "xs \<approx> ys" |
167 shows "fcard_raw xs = fcard_raw ys" |
190 shows "fcard_raw xs = fcard_raw ys" |
168 using a |
191 using a |
205 by auto |
228 by auto |
206 |
229 |
207 lemma cons_left_idem: |
230 lemma cons_left_idem: |
208 "x # x # xs \<approx> x # xs" |
231 "x # x # xs \<approx> x # xs" |
209 by auto |
232 by auto |
210 |
|
211 lemma none_memb_nil: |
|
212 "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])" |
|
213 by (simp add: memb_def) |
|
214 |
233 |
215 lemma fset_raw_strong_cases: |
234 lemma fset_raw_strong_cases: |
216 "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))" |
235 "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))" |
217 apply (induct xs) |
236 apply (induct xs) |
218 apply (simp) |
237 apply (simp) |
490 |
509 |
491 lemma fcard_delete: |
510 lemma fcard_delete: |
492 "fcard (fdelete S y) = (if y |\<in>| S then fcard S - 1 else fcard S)" |
511 "fcard (fdelete S y) = (if y |\<in>| S then fcard S - 1 else fcard S)" |
493 by (lifting fcard_raw_delete) |
512 by (lifting fcard_raw_delete) |
494 |
513 |
|
514 lemma fcard_suc_memb: "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A" |
|
515 by (lifting fcard_raw_suc_memb) |
|
516 |
|
517 lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0" |
|
518 by (lifting mem_card_not_0) |
|
519 |
495 text {* funion *} |
520 text {* funion *} |
496 |
521 |
497 lemma funion_simps[simp]: |
522 lemma funion_simps[simp]: |
498 shows "{||} |\<union>| S = S" |
523 shows "{||} |\<union>| S = S" |
499 and "finsert x S |\<union>| T = finsert x (S |\<union>| T)" |
524 and "finsert x S |\<union>| T = finsert x (S |\<union>| T)" |