104 by (rule eq_reflection) auto |
104 by (rule eq_reflection) auto |
105 |
105 |
106 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba" |
106 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba" |
107 unfolding list_eq.simps |
107 unfolding list_eq.simps |
108 by (simp only: set_map set_in_eq) |
108 by (simp only: set_map set_in_eq) |
109 |
|
110 text {* Peter *} |
|
111 ML {* Quotient_Info.quotient_rules_get @{context} *} |
|
112 |
|
113 lemma |
|
114 assumes "Quotient R1 abs1 rep1" |
|
115 and "Quotient R2 abs2 rep2" |
|
116 shows "Quotient (R1 OOO R2) (abs1 o ab2) (rep1 o rep2)" |
|
117 using assms |
|
118 sorry |
|
119 |
|
120 lemma |
|
121 assumes "Quotient R1 abs1 rep1" |
|
122 and "Quotient R2 abs2 rep2" |
|
123 shows "Quotient (R3) (abs1 o ab2) (rep1 o rep2)" |
|
124 using assms |
|
125 sorry |
|
126 |
109 |
127 lemma quotient_compose_list[quot_thm]: |
110 lemma quotient_compose_list[quot_thm]: |
128 shows "Quotient ((list_all2 op \<approx>) OOO (op \<approx>)) |
111 shows "Quotient ((list_all2 op \<approx>) OOO (op \<approx>)) |
129 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
112 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
130 unfolding Quotient_def comp_def |
113 unfolding Quotient_def comp_def |
738 shows "memb x xs \<Longrightarrow> memb x (y # xs)" |
721 shows "memb x xs \<Longrightarrow> memb x (y # xs)" |
739 by (simp add: memb_def) |
722 by (simp add: memb_def) |
740 |
723 |
741 lemma singleton_list_eq: |
724 lemma singleton_list_eq: |
742 shows "[x] \<approx> [y] \<longleftrightarrow> x = y" |
725 shows "[x] \<approx> [y] \<longleftrightarrow> x = y" |
743 by (simp add: id_simps) auto |
726 by (simp add:) auto |
744 |
727 |
745 lemma sub_list_cons: |
728 lemma sub_list_cons: |
746 "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)" |
729 "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)" |
747 by (auto simp add: memb_def sub_list_def) |
730 by (auto simp add: memb_def sub_list_def) |
748 |
731 |
762 |
745 |
763 lemma fcard_raw_suc: |
746 lemma fcard_raw_suc: |
764 assumes a: "fcard_raw xs = Suc n" |
747 assumes a: "fcard_raw xs = Suc n" |
765 shows "\<exists>x ys. \<not> (memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n" |
748 shows "\<exists>x ys. \<not> (memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n" |
766 using a |
749 using a |
767 by (induct xs) (auto simp add: memb_def split: if_splits) |
750 by (induct xs) (auto simp add: memb_def split_ifs) |
768 |
751 |
769 lemma singleton_fcard_1: |
752 lemma singleton_fcard_1: |
770 shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1" |
753 shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1" |
771 by (induct xs) (auto simp add: memb_def subset_insert) |
754 by (induct xs) (auto simp add: memb_def subset_insert) |
772 |
755 |
963 |
946 |
964 lemma sub_list_neq_set: "(sub_list xs ys \<and> \<not> list_eq xs ys) = (set xs \<subset> set ys)" |
947 lemma sub_list_neq_set: "(sub_list xs ys \<and> \<not> list_eq xs ys) = (set xs \<subset> set ys)" |
965 by (auto simp add: sub_list_set) |
948 by (auto simp add: sub_list_set) |
966 |
949 |
967 lemma fcard_raw_set: "fcard_raw xs = card (set xs)" |
950 lemma fcard_raw_set: "fcard_raw xs = card (set xs)" |
968 by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint finite_set) |
951 by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint) |
969 |
952 |
970 lemma memb_set: "memb x xs = (x \<in> set xs)" |
953 lemma memb_set: "memb x xs = (x \<in> set xs)" |
971 by (simp only: memb_def) |
954 by (simp only: memb_def) |
972 |
955 |
973 lemma filter_set: "set (filter P xs) = P \<inter> (set xs)" |
956 lemma filter_set: "set (filter P xs) = P \<inter> (set xs)" |
980 lemma inter_raw_set: "set (finter_raw xs ys) = set xs \<inter> set ys" |
963 lemma inter_raw_set: "set (finter_raw xs ys) = set xs \<inter> set ys" |
981 by (induct xs) (simp_all add: memb_def) |
964 by (induct xs) (simp_all add: memb_def) |
982 |
965 |
983 lemma fminus_raw_set: "set (fminus_raw xs ys) = set xs - set ys" |
966 lemma fminus_raw_set: "set (fminus_raw xs ys) = set xs - set ys" |
984 by (induct ys arbitrary: xs) |
967 by (induct ys arbitrary: xs) |
985 (simp_all add: fminus_raw.simps delete_raw_set, blast) |
968 (simp_all add: delete_raw_set, blast) |
986 |
969 |
987 text {* Raw theorems of ffilter *} |
970 text {* Raw theorems of ffilter *} |
988 |
971 |
989 lemma sub_list_filter: "sub_list (filter P xs) (filter Q xs) = (\<forall> x. memb x xs \<longrightarrow> P x \<longrightarrow> Q x)" |
972 lemma sub_list_filter: "sub_list (filter P xs) (filter Q xs) = (\<forall> x. memb x xs \<longrightarrow> P x \<longrightarrow> Q x)" |
990 unfolding sub_list_def memb_def by auto |
973 unfolding sub_list_def memb_def by auto |
1321 |
1304 |
1322 lemma fconcat_empty: |
1305 lemma fconcat_empty: |
1323 shows "fconcat {||} = {||}" |
1306 shows "fconcat {||} = {||}" |
1324 by (lifting concat.simps(1)) |
1307 by (lifting concat.simps(1)) |
1325 |
1308 |
1326 text {* Peter *} |
|
1327 lemma test: "equivp R ==> a = b --> R a b" |
|
1328 by (simp add: equivp_def) |
|
1329 |
|
1330 lemma |
|
1331 shows "fconcat {||} = {||}" |
|
1332 apply(lifting_setup concat.simps(1)) |
|
1333 apply(rule test) |
|
1334 apply(tactic {* resolve_tac (Quotient_Info.equiv_rules_get @{context}) 1 *}) |
|
1335 |
|
1336 sorry |
|
1337 |
|
1338 lemma fconcat_insert: |
1309 lemma fconcat_insert: |
1339 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
1310 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
1340 by (lifting concat.simps(2)) |
1311 by (lifting concat.simps(2)) |
1341 |
1312 |
1342 lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys" |
|
1343 by (lifting concat_append) |
|
1344 |
|
1345 text {* ffilter *} |
1313 text {* ffilter *} |
1346 |
1314 |
1347 lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)" |
1315 lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)" |
1348 by (lifting sub_list_filter) |
1316 by (lifting sub_list_filter) |
1349 |
1317 |
1350 lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)" |
1318 lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)" |
1351 by (lifting list_eq_filter) |
1319 by (lifting list_eq_filter) |
1352 |
1320 |
1353 lemma subset_ffilter: "(\<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" |
1321 lemma subset_ffilter: |
|
1322 "(\<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" |
1354 unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter) |
1323 unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter) |
1355 |
1324 |
1356 section {* lemmas transferred from Finite_Set theory *} |
1325 section {* lemmas transferred from Finite_Set theory *} |
1357 |
1326 |
1358 text {* finiteness for finite sets holds *} |
1327 text {* finiteness for finite sets holds *} |
1447 done |
1416 done |
1448 |
1417 |
1449 lemma list_all2_refl: |
1418 lemma list_all2_refl: |
1450 assumes q: "equivp R" |
1419 assumes q: "equivp R" |
1451 shows "(list_all2 R) r r" |
1420 shows "(list_all2 R) r r" |
1452 by (rule list_all2_refl) (metis equivp_def fset_equivp q) |
1421 by (rule list_all2_refl) (metis equivp_def q) |
1453 |
1422 |
1454 lemma compose_list_refl2: |
1423 lemma compose_list_refl2: |
1455 assumes q: "equivp R" |
1424 assumes q: "equivp R" |
1456 shows "(list_all2 R OOO op \<approx>) r r" |
1425 shows "(list_all2 R OOO op \<approx>) r r" |
1457 proof |
1426 proof |