equal
deleted
inserted
replaced
254 by (metis List.set.simps(2) emptyE ffold_raw.simps(2) in_listsp_conv_set listsp.simps mem_def) |
254 by (metis List.set.simps(2) emptyE ffold_raw.simps(2) in_listsp_conv_set listsp.simps mem_def) |
255 |
255 |
256 lemma ffold_raw_rsp[quot_respect]: |
256 lemma ffold_raw_rsp[quot_respect]: |
257 shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
257 shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
258 unfolding fun_rel_def |
258 unfolding fun_rel_def |
259 apply(auto intro: ffold_raw_rsp_pre) |
259 by(auto intro: ffold_raw_rsp_pre) |
260 done |
|
261 |
260 |
262 lemma concat_rsp_pre: |
261 lemma concat_rsp_pre: |
263 assumes a: "list_all2 op \<approx> x x'" |
262 assumes a: "list_all2 op \<approx> x x'" |
264 and b: "x' \<approx> y'" |
263 and b: "x' \<approx> y'" |
265 and c: "list_all2 op \<approx> y' y" |
264 and c: "list_all2 op \<approx> y' y" |
298 qed |
297 qed |
299 then show "concat a \<approx> concat b" by auto |
298 then show "concat a \<approx> concat b" by auto |
300 qed |
299 qed |
301 |
300 |
302 |
301 |
303 lemma concat_rsp_unfolded: |
302 |
304 "\<lbrakk>list_all2 op \<approx> a ba; ba \<approx> bb; list_all2 op \<approx> bb b\<rbrakk> \<Longrightarrow> concat a \<approx> concat b" |
|
305 proof - |
|
306 fix a b ba bb |
|
307 assume a: "list_all2 op \<approx> a ba" |
|
308 assume b: "ba \<approx> bb" |
|
309 assume c: "list_all2 op \<approx> bb b" |
|
310 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
|
311 fix x |
|
312 show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
|
313 assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
|
314 show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
|
315 next |
|
316 assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
|
317 have a': "list_all2 op \<approx> ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a]) |
|
318 have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) |
|
319 have c': "list_all2 op \<approx> b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c]) |
|
320 show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
|
321 qed |
|
322 qed |
|
323 then show "concat a \<approx> concat b" by auto |
|
324 qed |
|
325 |
303 |
326 lemma [quot_respect]: |
304 lemma [quot_respect]: |
327 shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter" |
305 shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter" |
328 by auto |
306 by auto |
329 |
307 |
503 |
481 |
504 section {* Other constants on the Quotient Type *} |
482 section {* Other constants on the Quotient Type *} |
505 |
483 |
506 quotient_definition |
484 quotient_definition |
507 "fcard :: 'a fset \<Rightarrow> nat" |
485 "fcard :: 'a fset \<Rightarrow> nat" |
508 is fcard_raw |
486 is |
|
487 fcard_raw |
509 |
488 |
510 quotient_definition |
489 quotient_definition |
511 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
490 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
512 is map |
491 is |
|
492 map |
513 |
493 |
514 quotient_definition |
494 quotient_definition |
515 "fdelete :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
495 "fdelete :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
516 is removeAll |
496 is removeAll |
517 |
497 |
676 by simp |
656 by simp |
677 |
657 |
678 lemma memb_append: |
658 lemma memb_append: |
679 "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys" |
659 "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys" |
680 by (induct xs) (simp_all add: not_memb_nil memb_cons_iff) |
660 by (induct xs) (simp_all add: not_memb_nil memb_cons_iff) |
681 |
|
682 lemma cons_left_comm: |
|
683 "x # y # xs \<approx> y # x # xs" |
|
684 by auto |
|
685 |
|
686 lemma cons_left_idem: |
|
687 "x # x # xs \<approx> x # xs" |
|
688 by auto |
|
689 |
661 |
690 lemma fset_raw_strong_cases: |
662 lemma fset_raw_strong_cases: |
691 obtains "xs = []" |
663 obtains "xs = []" |
692 | x ys where "\<not> memb x ys" and "xs \<approx> x # ys" |
664 | x ys where "\<not> memb x ys" and "xs \<approx> x # ys" |
693 proof (induct xs arbitrary: x ys) |
665 proof (induct xs arbitrary: x ys) |
717 show thesis using b f g by simp |
689 show thesis using b f g by simp |
718 qed |
690 qed |
719 qed |
691 qed |
720 then show thesis using a c by blast |
692 then show thesis using a c by blast |
721 qed |
693 qed |
722 |
|
723 |
694 |
724 section {* deletion *} |
695 section {* deletion *} |
725 |
696 |
726 |
697 |
727 lemma fset_raw_removeAll_cases: |
698 lemma fset_raw_removeAll_cases: |
825 qed |
796 qed |
826 |
797 |
827 text {* Lifted theorems *} |
798 text {* Lifted theorems *} |
828 |
799 |
829 lemma not_fin_fnil: "x |\<notin>| {||}" |
800 lemma not_fin_fnil: "x |\<notin>| {||}" |
830 by (lifting not_memb_nil) |
801 by (descending) (simp add: memb_def) |
831 |
802 |
832 lemma fin_finsert_iff[simp]: |
803 lemma fin_finsert_iff[simp]: |
833 "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S" |
804 "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S" |
834 by (descending) (simp add: memb_def) |
805 by (descending) (simp add: memb_def) |
835 |
806 |
1023 lemma fmap_set_image: |
994 lemma fmap_set_image: |
1024 "fset (fmap f S) = f ` (fset S)" |
995 "fset (fmap f S) = f ` (fset S)" |
1025 by (induct S) simp_all |
996 by (induct S) simp_all |
1026 |
997 |
1027 lemma inj_fmap_eq_iff: |
998 lemma inj_fmap_eq_iff: |
1028 "inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)" |
999 "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T" |
1029 by (lifting inj_map_eq_iff) |
1000 by (lifting inj_map_eq_iff) |
1030 |
1001 |
1031 lemma fmap_funion: |
1002 lemma fmap_funion: |
1032 shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T" |
1003 shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T" |
1033 by (lifting map_append) |
1004 by (lifting map_append) |
1213 by (descending) (auto simp add: memb_def sub_list_def) |
1184 by (descending) (auto simp add: memb_def sub_list_def) |
1214 |
1185 |
1215 lemma eq_ffilter: |
1186 lemma eq_ffilter: |
1216 shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)" |
1187 shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)" |
1217 by (descending) (auto simp add: memb_def) |
1188 by (descending) (auto simp add: memb_def) |
1218 |
1189 |
1219 lemma subset_ffilter: |
1190 lemma subset_ffilter: |
1220 "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs" |
1191 shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs" |
1221 unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter) |
1192 unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter) |
1222 |
1193 |
1223 |
1194 |
1224 section {* lemmas transferred from Finite_Set theory *} |
1195 section {* lemmas transferred from Finite_Set theory *} |
1225 |
1196 |
1226 text {* finiteness for finite sets holds *} |
1197 text {* finiteness for finite sets holds *} |
1408 *} |
1379 *} |
1409 |
1380 |
1410 no_notation |
1381 no_notation |
1411 list_eq (infix "\<approx>" 50) |
1382 list_eq (infix "\<approx>" 50) |
1412 |
1383 |
1413 |
|
1414 end |
1384 end |