157 case True |
157 case True |
158 then show ?thesis using f1 f2 apply - |
158 then show ?thesis using f1 f2 apply - |
159 apply (simp add: memb_def) |
159 apply (simp add: memb_def) |
160 apply clarify |
160 apply clarify |
161 by metis |
161 by metis |
|
162 next |
162 case False |
163 case False |
163 then have ?thesis using f1 f2 apply - |
164 then show ?thesis using f1 f2 apply - |
164 apply (rule_tac x="a" in exI) |
165 apply (rule_tac x="a" in exI) |
165 apply (rule_tac x="xs" in exI) |
166 apply (rule_tac x="xs" in exI) |
166 apply (simp add: memb_def) |
167 apply (simp add: memb_def) |
167 done |
168 done |
168 qed |
169 qed |
169 qed |
170 qed |
170 qed |
|
171 |
171 |
172 lemma singleton_fcard_1: "set a = {b} \<Longrightarrow> fcard_raw a = Suc 0" |
172 lemma singleton_fcard_1: "set a = {b} \<Longrightarrow> fcard_raw a = Suc 0" |
173 apply (induct a) |
173 apply (induct a) |
174 apply simp_all |
174 apply simp_all |
175 apply auto |
175 apply auto |
342 apply (simp_all add: memb_delete_raw) |
342 apply (simp_all add: memb_delete_raw) |
343 apply (simp add: memb_cons_iff) |
343 apply (simp add: memb_cons_iff) |
344 apply (simp add: not_memb_delete_raw_ident) |
344 apply (simp add: not_memb_delete_raw_ident) |
345 apply (simp add: memb_cons_iff rsp_fold_def) |
345 apply (simp add: memb_cons_iff rsp_fold_def) |
346 done |
346 done |
|
347 |
|
348 lemma ffold_raw_rsp_pre: |
|
349 "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b" |
|
350 apply (induct a arbitrary: b) |
|
351 apply (simp add: hd_in_set memb_absorb memb_def none_mem_nil) |
|
352 apply (simp add: ffold_raw.simps) |
|
353 apply (rule conjI) |
|
354 apply (rule_tac [!] impI) |
|
355 apply (rule_tac [!] conjI) |
|
356 apply (rule_tac [!] impI) |
|
357 apply (simp add: in_set_code memb_cons_iff memb_def) |
|
358 apply (metis) |
|
359 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2)) |
|
360 defer |
|
361 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2)) |
|
362 apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))") |
|
363 apply (simp only:) |
|
364 apply (rule_tac f="f a1" in arg_cong) |
|
365 apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)") |
|
366 apply simp |
|
367 apply (simp add: memb_delete_raw) |
|
368 apply (metis memb_cons_iff) |
|
369 apply (erule memb_commute_ffold_raw) |
|
370 apply (drule_tac x="a1" in spec) |
|
371 apply (simp add: memb_cons_iff) |
|
372 done |
|
373 |
|
374 lemma [quot_respect]: |
|
375 "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
|
376 by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |
347 |
377 |
348 primrec |
378 primrec |
349 finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
379 finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
350 where |
380 where |
351 "finter_raw [] l = []" |
381 "finter_raw [] l = []" |
631 |
661 |
632 lemma fin_finter: |
662 lemma fin_finter: |
633 "(e |\<in>| (l |\<inter>| r)) = (e |\<in>| l \<and> e |\<in>| r)" |
663 "(e |\<in>| (l |\<inter>| r)) = (e |\<in>| l \<and> e |\<in>| r)" |
634 by (lifting memb_finter_raw) |
664 by (lifting memb_finter_raw) |
635 |
665 |
|
666 lemma expand_fset_eq: |
|
667 "(xs = ys) = (\<forall>x. (x |\<in>| xs) = (x |\<in>| ys))" |
|
668 by (lifting list_eq.simps[simplified memb_def[symmetric]]) |
|
669 |
|
670 |
636 ML {* |
671 ML {* |
637 fun dest_fsetT (Type ("FSet.fset", [T])) = T |
672 fun dest_fsetT (Type ("FSet.fset", [T])) = T |
638 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
673 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
639 *} |
674 *} |
640 |
675 |