43 "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" |
43 "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" |
44 shows "comm_monoid_cancel G" |
44 shows "comm_monoid_cancel G" |
45 proof - |
45 proof - |
46 interpret comm_monoid G by fact |
46 interpret comm_monoid G by fact |
47 show "comm_monoid_cancel G" |
47 show "comm_monoid_cancel G" |
48 apply unfold_locales |
48 by unfold_locales (metis assms(2) m_ac(2))+ |
49 apply (subgoal_tac "a \<otimes> c = b \<otimes> c") |
|
50 apply (iprover intro: cancel) |
|
51 apply (simp add: m_comm) |
|
52 apply (iprover intro: cancel) |
|
53 done |
|
54 qed |
49 qed |
55 |
50 |
56 lemma (in comm_monoid_cancel) is_comm_monoid_cancel: |
51 lemma (in comm_monoid_cancel) is_comm_monoid_cancel: |
57 "comm_monoid_cancel G" |
52 "comm_monoid_cancel G" |
58 by intro_locales |
53 by intro_locales |
66 lemma (in monoid) Units_m_closed[simp, intro]: |
61 lemma (in monoid) Units_m_closed[simp, intro]: |
67 assumes h1unit: "h1 \<in> Units G" and h2unit: "h2 \<in> Units G" |
62 assumes h1unit: "h1 \<in> Units G" and h2unit: "h2 \<in> Units G" |
68 shows "h1 \<otimes> h2 \<in> Units G" |
63 shows "h1 \<otimes> h2 \<in> Units G" |
69 unfolding Units_def |
64 unfolding Units_def |
70 using assms |
65 using assms |
71 apply safe |
66 by auto (metis Units_inv_closed Units_l_inv Units_m_closed Units_r_inv) |
72 apply fast |
|
73 apply (intro bexI[of _ "inv h2 \<otimes> inv h1"], safe) |
|
74 apply (simp add: m_assoc Units_closed) |
|
75 apply (simp add: m_assoc[symmetric] Units_closed Units_l_inv) |
|
76 apply (simp add: m_assoc Units_closed) |
|
77 apply (simp add: m_assoc[symmetric] Units_closed Units_r_inv) |
|
78 apply fast |
|
79 done |
|
80 |
67 |
81 lemma (in monoid) prod_unit_l: |
68 lemma (in monoid) prod_unit_l: |
82 assumes abunit[simp]: "a \<otimes> b \<in> Units G" and aunit[simp]: "a \<in> Units G" |
69 assumes abunit[simp]: "a \<otimes> b \<in> Units G" and aunit[simp]: "a \<in> Units G" |
83 and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" |
70 and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" |
84 shows "b \<in> Units G" |
71 shows "b \<in> Units G" |
611 apply clarsimp |
597 apply clarsimp |
612 apply (rule unit_divides) |
598 apply (rule unit_divides) |
613 apply (unfold Units_def, fast) |
599 apply (unfold Units_def, fast) |
614 apply assumption |
600 apply assumption |
615 apply clarsimp |
601 apply clarsimp |
616 proof - |
602 apply (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed) |
617 fix x |
603 done |
618 assume xcarr: "x \<in> carrier G" |
|
619 assume r[rule_format]: "\<forall>y. y \<in> carrier G \<longrightarrow> x divides y" |
|
620 have "\<one> \<in> carrier G" by simp |
|
621 hence "x divides \<one>" by (rule r) |
|
622 hence "\<exists>x'\<in>carrier G. \<one> = x \<otimes> x'" by (rule dividesE, fast) |
|
623 from this obtain x' |
|
624 where x'carr: "x' \<in> carrier G" |
|
625 and xx': "\<one> = x \<otimes> x'" |
|
626 by auto |
|
627 |
|
628 note xx' |
|
629 also with xcarr x'carr |
|
630 have "\<dots> = x' \<otimes> x" by (simp add: m_comm) |
|
631 finally |
|
632 have "\<one> = x' \<otimes> x" . |
|
633 |
|
634 from x'carr xx'[symmetric] this[symmetric] |
|
635 show "\<exists>y\<in>carrier G. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast |
|
636 qed |
|
637 |
604 |
638 |
605 |
639 subsubsection {* Proper factors *} |
606 subsubsection {* Proper factors *} |
640 |
607 |
641 lemma properfactorI: |
608 lemma properfactorI: |
854 and carr[simp]: "a \<in> carrier G" "a' \<in> carrier G" |
821 and carr[simp]: "a \<in> carrier G" "a' \<in> carrier G" |
855 shows "irreducible G a'" |
822 shows "irreducible G a'" |
856 using assms |
823 using assms |
857 apply (elim irreducibleE, intro irreducibleI) |
824 apply (elim irreducibleE, intro irreducibleI) |
858 apply simp_all |
825 apply simp_all |
859 proof clarify |
826 apply (metis assms(2) assms(3) assoc_unit_l) |
860 assume "a' \<in> Units G" |
827 apply (metis assms(2) assms(3) assms(4) associated_sym properfactor_cong_r) |
861 also note aa'[symmetric] |
828 done |
862 finally have aunit: "a \<in> Units G" by simp |
|
863 |
|
864 assume "a \<notin> Units G" |
|
865 with aunit |
|
866 show "False" by fast |
|
867 next |
|
868 fix b |
|
869 assume r[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G" |
|
870 and bcarr[simp]: "b \<in> carrier G" |
|
871 assume "properfactor G b a'" |
|
872 also note aa'[symmetric] |
|
873 finally |
|
874 have "properfactor G b a" by simp |
|
875 |
|
876 with bcarr |
|
877 show "b \<in> Units G" by (fast intro: r) |
|
878 qed |
|
879 |
|
880 |
829 |
881 lemma (in monoid) irreducible_prod_rI: |
830 lemma (in monoid) irreducible_prod_rI: |
882 assumes airr: "irreducible G a" |
831 assumes airr: "irreducible G a" |
883 and bunit: "b \<in> Units G" |
832 and bunit: "b \<in> Units G" |
884 and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" |
833 and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" |
885 shows "irreducible G (a \<otimes> b)" |
834 shows "irreducible G (a \<otimes> b)" |
886 using airr carr bunit |
835 using airr carr bunit |
887 apply (elim irreducibleE, intro irreducibleI, clarify) |
836 apply (elim irreducibleE, intro irreducibleI, clarify) |
888 apply (subgoal_tac "a \<in> Units G", simp) |
837 apply (subgoal_tac "a \<in> Units G", simp) |
889 apply (intro prod_unit_r[of a b] carr bunit, assumption) |
838 apply (intro prod_unit_r[of a b] carr bunit, assumption) |
890 proof - |
839 apply (metis assms associatedI2 m_closed properfactor_cong_r) |
891 fix c |
840 done |
892 assume [simp]: "c \<in> carrier G" |
|
893 and r[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G" |
|
894 assume "properfactor G c (a \<otimes> b)" |
|
895 also have "a \<otimes> b \<sim> a" by (intro associatedI2[OF bunit], simp+) |
|
896 finally |
|
897 have pfa: "properfactor G c a" by simp |
|
898 show "c \<in> Units G" by (rule r, simp add: pfa) |
|
899 qed |
|
900 |
841 |
901 lemma (in comm_monoid) irreducible_prod_lI: |
842 lemma (in comm_monoid) irreducible_prod_lI: |
902 assumes birr: "irreducible G b" |
843 assumes birr: "irreducible G b" |
903 and aunit: "a \<in> Units G" |
844 and aunit: "a \<in> Units G" |
904 and carr [simp]: "a \<in> carrier G" "b \<in> carrier G" |
845 and carr [simp]: "a \<in> carrier G" "b \<in> carrier G" |
919 and isunit[rule_format]: "\<forall>ba. ba \<in> carrier G \<and> properfactor G ba (a \<otimes> b) \<longrightarrow> ba \<in> Units G" |
860 and isunit[rule_format]: "\<forall>ba. ba \<in> carrier G \<and> properfactor G ba (a \<otimes> b) \<longrightarrow> ba \<in> Units G" |
920 |
861 |
921 show "P" |
862 show "P" |
922 proof (cases "a \<in> Units G") |
863 proof (cases "a \<in> Units G") |
923 assume aunit: "a \<in> Units G" |
864 assume aunit: "a \<in> Units G" |
924 |
|
925 have "irreducible G b" |
865 have "irreducible G b" |
926 apply (rule irreducibleI) |
866 apply (rule irreducibleI) |
927 proof (rule ccontr, simp) |
867 proof (rule ccontr, simp) |
928 assume "b \<in> Units G" |
868 assume "b \<in> Units G" |
929 with aunit have "(a \<otimes> b) \<in> Units G" by fast |
869 with aunit have "(a \<otimes> b) \<in> Units G" by fast |
996 and pp': "p \<sim> p'" |
936 and pp': "p \<sim> p'" |
997 and carr[simp]: "p \<in> carrier G" "p' \<in> carrier G" |
937 and carr[simp]: "p \<in> carrier G" "p' \<in> carrier G" |
998 shows "prime G p'" |
938 shows "prime G p'" |
999 using pprime |
939 using pprime |
1000 apply (elim primeE, intro primeI) |
940 apply (elim primeE, intro primeI) |
1001 proof clarify |
941 apply (metis assms(2) assms(3) assoc_unit_l) |
1002 assume pnunit: "p \<notin> Units G" |
942 apply (metis assms(2) assms(3) assms(4) associated_sym divides_cong_l m_closed) |
1003 assume "p' \<in> Units G" |
943 done |
1004 also note pp'[symmetric] |
|
1005 finally |
|
1006 have "p \<in> Units G" by simp |
|
1007 with pnunit |
|
1008 show False .. |
|
1009 next |
|
1010 fix a b |
|
1011 assume r[rule_format]: |
|
1012 "\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b" |
|
1013 assume p'dvd: "p' divides a \<otimes> b" |
|
1014 and carr'[simp]: "a \<in> carrier G" "b \<in> carrier G" |
|
1015 |
|
1016 note pp' |
|
1017 also note p'dvd |
|
1018 finally |
|
1019 have "p divides a \<otimes> b" by simp |
|
1020 hence "p divides a \<or> p divides b" by (intro r, simp+) |
|
1021 moreover { |
|
1022 note pp'[symmetric] |
|
1023 also assume "p divides a" |
|
1024 finally |
|
1025 have "p' divides a" by simp |
|
1026 hence "p' divides a \<or> p' divides b" by simp |
|
1027 } |
|
1028 moreover { |
|
1029 note pp'[symmetric] |
|
1030 also assume "p divides b" |
|
1031 finally |
|
1032 have "p' divides b" by simp |
|
1033 hence "p' divides a \<or> p' divides b" by simp |
|
1034 } |
|
1035 ultimately |
|
1036 show "p' divides a \<or> p' divides b" by fast |
|
1037 qed |
|
1038 |
|
1039 |
944 |
1040 subsection {* Factorization and Factorial Monoids *} |
945 subsection {* Factorization and Factorial Monoids *} |
1041 |
946 |
1042 subsubsection {* Function definitions *} |
947 subsubsection {* Function definitions *} |
1043 |
948 |
1259 apply (induct fs) |
1164 apply (induct fs) |
1260 apply simp |
1165 apply simp |
1261 apply (case_tac "f = a", simp) |
1166 apply (case_tac "f = a", simp) |
1262 apply (fast intro: dividesI) |
1167 apply (fast intro: dividesI) |
1263 apply clarsimp |
1168 apply clarsimp |
1264 apply (elim dividesE, intro dividesI) |
1169 apply (metis assms(2) divides_prod_l multlist_closed) |
1265 defer 1 |
|
1266 apply (simp add: m_comm) |
|
1267 apply (simp add: m_assoc[symmetric]) |
|
1268 apply (simp add: m_comm) |
|
1269 apply simp |
|
1270 done |
1170 done |
1271 |
1171 |
1272 lemma (in comm_monoid_cancel) multlist_listassoc_cong: |
1172 lemma (in comm_monoid_cancel) multlist_listassoc_cong: |
1273 assumes "fs [\<sim>] fs'" |
1173 assumes "fs [\<sim>] fs'" |
1274 and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G" |
1174 and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G" |
1381 lemma (in monoid) nunit_factors: |
1281 lemma (in monoid) nunit_factors: |
1382 assumes anunit: "a \<notin> Units G" |
1282 assumes anunit: "a \<notin> Units G" |
1383 and fs: "factors G as a" |
1283 and fs: "factors G as a" |
1384 shows "length as > 0" |
1284 shows "length as > 0" |
1385 apply (insert fs, elim factorsE) |
1285 apply (insert fs, elim factorsE) |
1386 proof (cases "length as = 0") |
1286 apply (metis Units_one_closed assms(1) foldr.simps(1) length_greater_0_conv) |
1387 assume "length as = 0" |
1287 done |
1388 hence fold: "foldr op \<otimes> as \<one> = \<one>" by force |
|
1389 |
|
1390 assume "foldr op \<otimes> as \<one> = a" |
|
1391 with fold |
|
1392 have "a = \<one>" by simp |
|
1393 then have "a \<in> Units G" by fast |
|
1394 with anunit |
|
1395 have "False" by simp |
|
1396 thus ?thesis .. |
|
1397 qed simp |
|
1398 |
1288 |
1399 lemma (in monoid) unit_wfactors [simp]: |
1289 lemma (in monoid) unit_wfactors [simp]: |
1400 assumes aunit: "a \<in> Units G" |
1290 assumes aunit: "a \<in> Units G" |
1401 shows "wfactors G [] a" |
1291 shows "wfactors G [] a" |
1402 using aunit |
1292 using aunit |
1443 and asc: "fs [\<sim>] fs'" |
1333 and asc: "fs [\<sim>] fs'" |
1444 and carr: "a \<in> carrier G" "set fs \<subseteq> carrier G" "set fs' \<subseteq> carrier G" |
1334 and carr: "a \<in> carrier G" "set fs \<subseteq> carrier G" "set fs' \<subseteq> carrier G" |
1445 shows "wfactors G fs' a" |
1335 shows "wfactors G fs' a" |
1446 using fact |
1336 using fact |
1447 apply (elim wfactorsE, intro wfactorsI) |
1337 apply (elim wfactorsE, intro wfactorsI) |
1448 proof - |
1338 apply (metis assms(2) assms(4) assms(5) irrlist_listassoc_cong) |
1449 assume "\<forall>f\<in>set fs. irreducible G f" |
1339 proof - |
1450 also note asc |
|
1451 finally (irrlist_listassoc_cong) |
|
1452 show "\<forall>f\<in>set fs'. irreducible G f" by (simp add: carr) |
|
1453 next |
|
1454 from asc[symmetric] |
1340 from asc[symmetric] |
1455 have "foldr op \<otimes> fs' \<one> \<sim> foldr op \<otimes> fs \<one>" |
1341 have "foldr op \<otimes> fs' \<one> \<sim> foldr op \<otimes> fs \<one>" |
1456 by (simp add: multlist_listassoc_cong carr) |
1342 by (simp add: multlist_listassoc_cong carr) |
1457 also assume "foldr op \<otimes> fs \<one> \<sim> a" |
1343 also assume "foldr op \<otimes> fs \<one> \<sim> a" |
1458 finally |
1344 finally |
2359 using pf |
2245 using pf |
2360 apply (elim properfactorE) |
2246 apply (elim properfactorE) |
2361 apply rule |
2247 apply rule |
2362 apply (intro divides_fmsubset, assumption) |
2248 apply (intro divides_fmsubset, assumption) |
2363 apply (rule assms)+ |
2249 apply (rule assms)+ |
2364 proof |
2250 apply (metis assms divides_fmsubset fmsubset_divides) |
2365 assume bna: "\<not> b divides a" |
2251 done |
2366 assume "fmset G as = fmset G bs" |
|
2367 then have "essentially_equal G as bs" by (rule fmset_ee) fact+ |
|
2368 hence "a \<sim> b" by (rule ee_wfactorsD[of as bs]) fact+ |
|
2369 hence "b divides a" by (elim associatedE) |
|
2370 with bna |
|
2371 show "False" .. |
|
2372 qed |
|
2373 |
|
2374 |
2252 |
2375 subsection {* Irreducible Elements are Prime *} |
2253 subsection {* Irreducible Elements are Prime *} |
2376 |
2254 |
2377 lemma (in factorial_monoid) irreducible_is_prime: |
2255 lemma (in factorial_monoid) irreducible_is_prime: |
2378 assumes pirr: "irreducible G p" |
2256 assumes pirr: "irreducible G p" |
3427 |
3305 |
3428 lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct: |
3306 lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct: |
3429 "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and> |
3307 "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and> |
3430 wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'" |
3308 wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'" |
3431 apply (induct as) |
3309 apply (induct as) |
3432 apply clarsimp defer 1 |
3310 apply (metis Units_one_closed essentially_equal_def foldr.simps(1) is_monoid_cancel listassoc_refl monoid_cancel.assoc_unit_r perm_refl unit_wfactors_empty wfactorsE) |
3433 apply clarsimp defer 1 |
3311 apply clarsimp |
3434 proof - |
3312 proof - |
3435 fix a as' |
3313 fix a as ah as' |
3436 assume acarr: "a \<in> carrier G" |
|
3437 and "wfactors G [] a" |
|
3438 hence aunit: "a \<in> Units G" |
|
3439 apply (elim wfactorsE) |
|
3440 apply (simp, rule assoc_unit_r[of "\<one>"], simp+) |
|
3441 done |
|
3442 |
|
3443 assume "set as' \<subseteq> carrier G" "wfactors G as' a" |
|
3444 with aunit |
|
3445 have "as' = []" |
|
3446 by (intro unit_wfactors_empty[of a]) |
|
3447 thus "essentially_equal G [] as'" by simp |
|
3448 next |
|
3449 fix a as ah as' |
|
3450 assume ih[rule_format]: |
3314 assume ih[rule_format]: |
3451 "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> |
3315 "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> |
3452 wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'" |
3316 wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'" |
3453 and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G" |
3317 and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G" |
3454 and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G" |
3318 and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G" |
3640 |
3504 |
3641 lemma (in monoid) ee_length: |
3505 lemma (in monoid) ee_length: |
3642 assumes ee: "essentially_equal G as bs" |
3506 assumes ee: "essentially_equal G as bs" |
3643 shows "length as = length bs" |
3507 shows "length as = length bs" |
3644 apply (rule essentially_equalE[OF ee]) |
3508 apply (rule essentially_equalE[OF ee]) |
3645 apply (subgoal_tac "length as = length fs1'") |
3509 apply (metis list_all2_conv_all_nth perm_length) |
3646 apply (simp add: list_all2_lengthD) |
|
3647 apply (simp add: perm_length) |
|
3648 done |
3510 done |
3649 |
3511 |
3650 lemma (in factorial_monoid) factorcount_exists: |
3512 lemma (in factorial_monoid) factorcount_exists: |
3651 assumes carr[simp]: "a \<in> carrier G" |
3513 assumes carr[simp]: "a \<in> carrier G" |
3652 shows "EX c. ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as" |
3514 shows "EX c. ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as" |
3656 where ascarr[simp]: "set as \<subseteq> carrier G" |
3518 where ascarr[simp]: "set as \<subseteq> carrier G" |
3657 and afs: "wfactors G as a" |
3519 and afs: "wfactors G as a" |
3658 by (auto simp del: carr) |
3520 by (auto simp del: carr) |
3659 |
3521 |
3660 have "ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'" |
3522 have "ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'" |
3661 proof clarify |
3523 by (metis afs ascarr assms ee_length wfactors_unique) |
3662 fix as' |
|
3663 assume [simp]: "set as' \<subseteq> carrier G" |
|
3664 and bfs: "wfactors G as' a" |
|
3665 from afs bfs |
|
3666 have "essentially_equal G as as'" |
|
3667 by (intro ee_wfactorsI[of a a as as'], simp+) |
|
3668 thus "length as = length as'" by (rule ee_length) |
|
3669 qed |
|
3670 thus "EX c. ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" .. |
3524 thus "EX c. ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" .. |
3671 qed |
3525 qed |
3672 |
3526 |
3673 lemma (in factorial_monoid) factorcount_unique: |
3527 lemma (in factorial_monoid) factorcount_unique: |
3674 assumes afs: "wfactors G as a" |
3528 assumes afs: "wfactors G as a" |
3782 have "b divides a" by (fast intro: dividesI[of "inv c"]) |
3636 have "b divides a" by (fast intro: dividesI[of "inv c"]) |
3783 with nbdvda show False by simp |
3637 with nbdvda show False by simp |
3784 qed |
3638 qed |
3785 |
3639 |
3786 with cfs have "length cs > 0" |
3640 with cfs have "length cs > 0" |
3787 apply - |
3641 apply - |
3788 apply (rule ccontr, simp) |
3642 apply (rule ccontr, simp) |
3789 proof - |
3643 apply (metis Units_one_closed ccarr cscarr l_one one_closed properfactorI3 properfactor_fmset unit_wfactors) |
3790 assume "wfactors G [] c" |
3644 done |
3791 hence "\<one> \<sim> c" by (elim wfactorsE, simp) |
|
3792 with ccarr |
|
3793 have cunit: "c \<in> Units G" by (intro assoc_unit_r[of "\<one>" "c"], simp+) |
|
3794 assume "c \<notin> Units G" |
|
3795 with cunit show "False" by simp |
|
3796 qed |
|
3797 |
|
3798 with fca fcb show ?thesis by simp |
3645 with fca fcb show ?thesis by simp |
3799 qed |
3646 qed |
3800 |
3647 |
3801 sublocale factorial_monoid \<subseteq> divisor_chain_condition_monoid |
3648 sublocale factorial_monoid \<subseteq> divisor_chain_condition_monoid |
3802 apply unfold_locales |
3649 apply unfold_locales |
3803 apply (rule wfUNIVI) |
3650 apply (rule wfUNIVI) |
3804 apply (rule measure_induct[of "factorcount G"]) |
3651 apply (rule measure_induct[of "factorcount G"]) |
3805 apply simp (* slow *) (* |
3652 apply simp |
3806 [1]Applying congruence rule: |
3653 apply (metis properfactor_fcount) |
3807 \<lbrakk>factorcount G y < factorcount G xa \<equiv> ?P'; ?P' \<Longrightarrow> P y \<equiv> ?Q'\<rbrakk> \<Longrightarrow> factorcount G y < factorcount G xa \<longrightarrow> P y \<equiv> ?P' \<longrightarrow> ?Q' |
3654 done |
3808 |
|
3809 trace_simp_depth_limit exceeded! |
|
3810 *) |
|
3811 proof - |
|
3812 fix P x |
|
3813 assume r1[rule_format]: |
|
3814 "\<forall>y. (\<forall>z. z \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G z y \<longrightarrow> P z) \<longrightarrow> P y" |
|
3815 and r2[rule_format]: "\<forall>y. factorcount G y < factorcount G x \<longrightarrow> P y" |
|
3816 show "P x" |
|
3817 apply (rule r1) |
|
3818 apply (rule r2) |
|
3819 apply (rule properfactor_fcount, simp+) |
|
3820 done |
|
3821 qed |
|
3822 |
3655 |
3823 sublocale factorial_monoid \<subseteq> primeness_condition_monoid |
3656 sublocale factorial_monoid \<subseteq> primeness_condition_monoid |
3824 proof qed (rule irreducible_is_prime) |
3657 proof qed (rule irreducible_is_prime) |
3825 |
3658 |
3826 |
3659 |