# HG changeset patch # User wenzelm # Date 1473631890 -7200 # Node ID c948738d31aa49dbcda042a6d3dfe73a78547c08 # Parent 61a03e429cbdf7d552e3897b63f8b0d378463365# Parent 34dccc2dd6db3d9733ea58e990a2619e05caf274 merged diff -r 61a03e429cbd -r c948738d31aa src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Sun Sep 11 23:32:45 2016 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Mon Sep 12 00:11:30 2016 +0200 @@ -187,8 +187,7 @@ and elim: "\c. \b = a \ c; c \ carrier G\ \ P" shows "P" proof - - from dividesD[OF d] - obtain c where "c \ carrier G" and "b = a \ c" by auto + from dividesD[OF d] obtain c where "c \ carrier G" and "b = a \ c" by auto then show P by (elim elim) qed @@ -319,14 +318,12 @@ unfolding associated_def proof clarify assume "b divides a" - then have "\u\carrier G. a = b \ u" by (rule dividesD) then obtain u where ucarr: "u \ carrier G" and a: "a = b \ u" - by auto + by (rule dividesE) assume "a divides b" - then have "\u'\carrier G. b = a \ u'" by (rule dividesD) then obtain u' where u'carr: "u' \ carrier G" and b: "b = a \ u'" - by auto + by (rule dividesE) note carr = carr ucarr u'carr from carr have "a \ \ = a" by simp @@ -559,8 +556,7 @@ assumes advdb: "a divides b" and neq: "\(a \ b)" shows "properfactor G a b" - apply (rule properfactorI, rule advdb) -proof (rule ccontr, simp) +proof (rule properfactorI, rule advdb, rule notI) assume "b divides a" with advdb have "a \ b" by (rule associatedI) with neq show "False" by fast @@ -758,7 +754,7 @@ apply (elim irreducibleE, intro irreducibleI, clarify) apply (subgoal_tac "a \ Units G", simp) apply (intro prod_unit_r[of a b] carr bunit, assumption) - apply (metis assms associatedI2 m_closed properfactor_cong_r) + apply (metis assms(2,3) associatedI2 m_closed properfactor_cong_r) done lemma (in comm_monoid) irreducible_prod_lI: @@ -784,8 +780,7 @@ proof (cases "a \ Units G") case aunit: True have "irreducible G b" - apply (rule irreducibleI) - proof (rule ccontr, simp) + proof (rule irreducibleI, rule notI) assume "b \ Units G" with aunit have "(a \ b) \ Units G" by fast with abnunit show "False" .. @@ -804,8 +799,7 @@ then have bunit: "b \ Units G" by (intro isunit, simp) have "irreducible G a" - apply (rule irreducibleI) - proof (rule ccontr, simp) + proof (rule irreducibleI, rule notI) assume "a \ Units G" with bunit have "(a \ b) \ Units G" by fast with abnunit show "False" .. @@ -1010,10 +1004,8 @@ proof (elim essentially_equalE) fix fs assume "as <~~> fs" "fs [\] bs" - then have "\fs'. as [\] fs' \ fs' <~~> bs" - by (rule perm_assoc_switch_r) - then obtain fs' where a: "as [\] fs'" and p: "fs' <~~> bs" - by auto + from perm_assoc_switch_r [OF this] obtain fs' where a: "as [\] fs'" and p: "fs' <~~> bs" + by blast from p have "bs <~~> fs'" by (rule perm_sym) with a[symmetric] carr show ?thesis by (iprover intro: essentially_equalI perm_closed) @@ -1028,11 +1020,9 @@ using ab bc proof (elim essentially_equalE) fix abs bcs - assume "abs [\] bs" and pb: "bs <~~> bcs" - then have "\bs'. abs <~~> bs' \ bs' [\] bcs" - by (rule perm_assoc_switch) - then obtain bs' where p: "abs <~~> bs'" and a: "bs' [\] bcs" - by auto + assume "abs [\] bs" and pb: "bs <~~> bcs" + from perm_assoc_switch [OF this] obtain bs' where p: "abs <~~> bs'" and a: "bs' [\] bcs" + by blast assume "as <~~> abs" with p have pp: "as <~~> bs'" by fast @@ -1184,10 +1174,11 @@ and wf: "wfactors G fs a" and carr[simp]: "set fs \ carrier G" shows "fs = []" -proof (rule ccontr, cases fs, simp) - fix f fs' - assume fs: "fs = f # fs'" - +proof (cases fs) + case Nil + then show ?thesis . +next + case fs: (Cons f fs') from carr have fcarr[simp]: "f \ carrier G" and carr'[simp]: "set fs' \ carrier G" by (simp_all add: fs) @@ -1203,7 +1194,7 @@ by (simp add: Units_closed[OF aunit] a[symmetric]) finally have "f \ foldr (op \) fs' \ \ Units G" by simp then have "f \ Units G" by (intro unit_factor[of f], simp+) - with fnunit show "False" by simp + with fnunit show ?thesis by contradiction qed @@ -1366,10 +1357,8 @@ note carr[simp] = factors_closed[OF afs ascarr] ascarr[THEN subsetD] factors_closed[OF bfs bscarr] bscarr[THEN subsetD] - from ab carr have "\u\Units G. a = b \ u" - by (fast elim: associatedE2) - then obtain u where uunit: "u \ Units G" and a: "a = b \ u" - by auto + from ab carr obtain u where uunit: "u \ Units G" and a: "a = b \ u" + by (elim associatedE2) from uunit bscarr have ee: "essentially_equal G (bs[0 := (bs!0 \ u)]) bs" (is "essentially_equal G ?bs' bs") @@ -1420,10 +1409,8 @@ with anunit show False .. qed - have "\a'. factors G as a' \ a' \ a" - by (rule wfactors_factors[OF asf ascarr]) - then obtain a' where fa': "factors G as a'" and a': "a' \ a" - by auto + from wfactors_factors[OF asf ascarr] obtain a' where fa': "factors G as a'" and a': "a' \ a" + by blast from fa' ascarr have a'carr[simp]: "a' \ carrier G" by fast @@ -1436,10 +1423,8 @@ show "False" .. qed - have "\b'. factors G bs b' \ b' \ b" - by (rule wfactors_factors[OF bsf bscarr]) - then obtain b' where fb': "factors G bs b'" and b': "b' \ b" - by auto + from wfactors_factors[OF bsf bscarr] obtain b' where fb': "factors G bs b'" and b': "b' \ b" + by blast from fb' bscarr have b'carr[simp]: "b' \ carrier G" by fast @@ -1476,10 +1461,8 @@ then show ?thesis by (intro exI) force next case False - then have "\fs. set fs \ carrier G \ factors G fs a" - by (intro factors_exist acarr) - then obtain fs where fscarr: "set fs \ carrier G" and f: "factors G fs a" - by auto + with factors_exist [OF acarr] obtain fs where fscarr: "set fs \ carrier G" and f: "factors G fs a" + by blast from f have "wfactors G fs a" by (rule factors_wfactors) fact with fscarr show ?thesis by fast qed @@ -1593,11 +1576,9 @@ from wfactors_exists[OF acarr] obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" - by auto - from afs ascarr have "\a'. factors G as a' \ a' \ a" - by (rule wfactors_factors) - then obtain a' where afs': "factors G as a'" and a'a: "a' \ a" - by auto + by blast + from wfactors_factors [OF afs ascarr] obtain a' where afs': "factors G as a'" and a'a: "a' \ a" + by blast from afs' ascarr have a'carr: "a' \ carrier G" by fast have a'nunit: "a' \ Units G" @@ -1608,10 +1589,8 @@ with anunit show False .. qed - from a'carr acarr a'a have "\u. u \ Units G \ a' = a \ u" + from a'carr acarr a'a obtain u where uunit: "u \ Units G" and a': "a' = a \ u" by (blast elim: associatedE2) - then obtain u where uunit: "u \ Units G" and a': "a' = a \ u" - by auto note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit] @@ -1764,16 +1743,19 @@ have "set (map (assocs G) as) = {assocs G x | x. x \ set as}" by auto with setys have "set ys \ { assocs G x | x. x \ set as}" by simp then have "\yy. ys = map (assocs G) yy" - apply (induct ys) - apply simp - apply clarsimp - proof - - fix yy x - show "\yya. (assocs G x) # map (assocs G) yy = map (assocs G) yya" - by (rule exI[of _ "x#yy"]) simp + proof (induct ys) + case Nil + then show ?case by simp + next + case Cons + then show ?case + proof clarsimp + fix yy x + show "\yya. assocs G x # map (assocs G) yy = map (assocs G) yya" + by (rule exI[of _ "x#yy"]) simp + qed qed - then obtain yy where ys: "ys = map (assocs G) yy" - by auto + then obtain yy where ys: "ys = map (assocs G) yy" .. from p1 ys have "\as'. as <~~> as' \ map (assocs G) as' = map (assocs G) yy" by (intro r1) simp @@ -1785,14 +1767,16 @@ then obtain as'' where yyas'': "yy <~~> as''" and as''bs: "map (assocs G) as'' = map (assocs G) bs" by auto - from as'yy and yyas'' have "\cs. as' <~~> cs \ map (assocs G) cs = map (assocs G) as''" - by (rule perm_map_switch) - then obtain cs where as'cs: "as' <~~> cs" and csas'': "map (assocs G) cs = map (assocs G) as''" - by auto - - from asas' and as'cs have ascs: "as <~~> cs" by fast - from csas'' and as''bs have "map (assocs G) cs = map (assocs G) bs" by simp - with ascs show "\as'. as <~~> as' \ map (assocs G) as' = map (assocs G) bs" by fast + from perm_map_switch [OF as'yy yyas''] + obtain cs where as'cs: "as' <~~> cs" and csas'': "map (assocs G) cs = map (assocs G) as''" + by blast + + from asas' and as'cs have ascs: "as <~~> cs" + by fast + from csas'' and as''bs have "map (assocs G) cs = map (assocs G) bs" + by simp + with ascs show "\as'. as <~~> as' \ map (assocs G) as' = map (assocs G) bs" + by fast qed lemma (in comm_monoid_cancel) fmset_ee: @@ -1803,17 +1787,14 @@ from mset have mpp: "map (assocs G) as <~~> map (assocs G) bs" by (simp add: fmset_def mset_eq_perm del: mset_map) - have "\cas. cas = map (assocs G) as" by simp - then obtain cas where cas: "cas = map (assocs G) as" by simp - - have "\cbs. cbs = map (assocs G) bs" by simp - then obtain cbs where cbs: "cbs = map (assocs G) bs" by simp - - from cas cbs mpp have [rule_format]: + define cas where "cas = map (assocs G) as" + define cbs where "cbs = map (assocs G) bs" + + from cas_def cbs_def mpp have [rule_format]: "\as bs. (cas <~~> cbs \ cas = map (assocs G) as \ cbs = map (assocs G) bs) \ (\as'. as <~~> as' \ map (assocs G) as' = cbs)" by (intro fmset_ee__hlp_induct, simp+) - with mpp cas cbs have "\as'. as <~~> as' \ map (assocs G) as' = map (assocs G) bs" + with mpp cas_def cbs_def have "\as'. as <~~> as' \ map (assocs G) as' = map (assocs G) bs" by simp then obtain as' where tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs" @@ -1825,8 +1806,7 @@ with ascarr have as'carr: "set as' \ carrier G" by simp - from tm as'carr[THEN subsetD] bscarr[THEN subsetD] - have "as' [\] bs" + from tm as'carr[THEN subsetD] bscarr[THEN subsetD] have "as' [\] bs" by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym]) with tp show "essentially_equal G as bs" by (fast intro: essentially_equalI) @@ -1844,11 +1824,8 @@ assumes elems: "\X. X \ set_mset Cs \ \x. P x \ X = assocs G x" shows "\cs. (\c \ set cs. P c) \ fmset G cs = Cs" proof - - have "\Cs'. Cs = mset Cs'" - by (rule surjE[OF surj_mset], fast) - then obtain Cs' where Cs: "Cs = mset Cs'" - by auto - + from surjE[OF surj_mset] obtain Cs' where Cs: "Cs = mset Cs'" + by blast have "\cs. (\c \ set cs. P c) \ mset (map (assocs G) cs) = Cs" using elems unfolding Cs @@ -1858,11 +1835,14 @@ assume ih: "\X. X = a \ X \ set Cs' \ \x. P x \ X = assocs G x" and csP: "\x\set cs. P x" and mset: "mset (map (assocs G) cs) = mset Cs'" - from ih have "\x. P x \ a = assocs G x" by fast - then obtain c where cP: "P c" and a: "a = assocs G c" by auto - from cP csP have tP: "\x\set (c#cs). P x" by simp - from mset a have "mset (map (assocs G) (c#cs)) = add_mset a (mset Cs')" by simp - with tP show "\cs. (\x\set cs. P x) \ mset (map (assocs G) cs) = add_mset a (mset Cs')" by fast + from ih obtain c where cP: "P c" and a: "a = assocs G c" + by auto + from cP csP have tP: "\x\set (c#cs). P x" + by simp + from mset a have "mset (map (assocs G) (c#cs)) = add_mset a (mset Cs')" + by simp + with tP show "\cs. (\x\set cs. P x) \ mset (map (assocs G) cs) = add_mset a (mset Cs')" + by fast qed then show ?thesis by (simp add: fmset_def) qed @@ -1875,7 +1855,6 @@ by (intro mset_fmsetEx, rule elems) then obtain cs where p[rule_format]: "\c\set cs. c \ carrier G \ irreducible G c" and Cs[symmetric]: "fmset G cs = Cs" by auto - from p have cscarr: "set cs \ carrier G" by fast from p have "\c. c \ carrier G \ wfactors G cs c" by (intro wfactors_prod_exists) auto @@ -1944,10 +1923,9 @@ proof (elim dividesE) fix c assume ccarr: "c \ carrier G" - then have "\cs. set cs \ carrier G \ wfactors G cs c" - by (rule wfactors_exist) - then obtain cs where cscarr: "set cs \ carrier G" and cfs: "wfactors G cs c" - by auto + from wfactors_exist [OF this] + obtain cs where cscarr: "set cs \ carrier G" and cfs: "wfactors G cs c" + by blast note carr = carr ccarr cscarr assume "b = a \ c" @@ -2070,24 +2048,19 @@ and pnunit: "p \ Units G" assume irreduc[rule_format]: "\b. b \ carrier G \ properfactor G b p \ b \ Units G" - from pdvdab - have "\c\carrier G. a \ b = p \ c" by (rule dividesD) - then obtain c where ccarr: "c \ carrier G" and abpc: "a \ b = p \ c" - by auto - - from acarr have "\fs. set fs \ carrier G \ wfactors G fs a" - by (rule wfactors_exist) - then obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" + from pdvdab obtain c where ccarr: "c \ carrier G" and abpc: "a \ b = p \ c" + by (rule dividesE) + + from wfactors_exist [OF acarr] + obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" + by blast + + from wfactors_exist [OF bcarr] + obtain bs where bscarr: "set bs \ carrier G" and bfs: "wfactors G bs b" by auto - from bcarr have "\fs. set fs \ carrier G \ wfactors G fs b" - by (rule wfactors_exist) - then obtain bs where bscarr: "set bs \ carrier G" and bfs: "wfactors G bs b" - by auto - - from ccarr have "\fs. set fs \ carrier G \ wfactors G fs c" - by (rule wfactors_exist) - then obtain cs where cscarr: "set cs \ carrier G" and cfs: "wfactors G cs c" + from wfactors_exist [OF ccarr] + obtain cs where cscarr: "set cs \ carrier G" and cfs: "wfactors G cs c" by auto note carr[simp] = pcarr acarr bcarr ccarr ascarr bscarr cscarr @@ -2103,16 +2076,12 @@ from abfs' abfs have "essentially_equal G (p # cs) (as @ bs)" by (rule wfactors_unique) simp+ - then have "\ds. p # cs <~~> ds \ ds [\] (as @ bs)" + then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\] (as @ bs)" by (fast elim: essentially_equalE) - then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\] (as @ bs)" - by auto then have "p \ set ds" by (simp add: perm_set_eq[symmetric]) - with dsassoc have "\p'. p' \ set (as@bs) \ p \ p'" + with dsassoc obtain p' where "p' \ set (as@bs)" and pp': "p \ p'" unfolding list_all2_conv_all_nth set_conv_nth by force - then obtain p' where "p' \ set (as@bs)" and pp': "p \ p'" - by auto then consider "p' \ set as" | "p' \ set bs" by auto then show "p divides a \ p divides b" proof cases @@ -2151,10 +2120,8 @@ and bcarr: "b \ carrier G" and pdvdab: "p divides (a \ b)" assume irreduc[rule_format]: "\b. b \ carrier G \ properfactor G b p \ b \ Units G" - from pdvdab have "\c\carrier G. a \ b = p \ c" - by (rule dividesD) - then obtain c where ccarr: "c \ carrier G" and abpc: "a \ b = p \ c" - by auto + from pdvdab obtain c where ccarr: "c \ carrier G" and abpc: "a \ b = p \ c" + by (rule dividesE) note [simp] = pcarr acarr bcarr ccarr show "p divides a \ p divides b" @@ -2181,7 +2148,7 @@ next case bnunit: False have cnunit: "c \ Units G" - proof (rule ccontr, simp) + proof assume cunit: "c \ Units G" from bnunit have "properfactor G a (a \ b)" by (intro properfactorI3[of _ _ b], simp+) @@ -2200,19 +2167,16 @@ with anunit show False .. qed - from acarr anunit have "\fs. set fs \ carrier G \ factors G fs a" - by (rule factors_exist) - then obtain as where ascarr: "set as \ carrier G" and afac: "factors G as a" - by auto - - from bcarr bnunit have "\fs. set fs \ carrier G \ factors G fs b" - by (rule factors_exist) - then obtain bs where bscarr: "set bs \ carrier G" and bfac: "factors G bs b" - by auto - - from ccarr cnunit have "\fs. set fs \ carrier G \ factors G fs c" - by (rule factors_exist) - then obtain cs where cscarr: "set cs \ carrier G" and cfac: "factors G cs c" + from factors_exist [OF acarr anunit] + obtain as where ascarr: "set as \ carrier G" and afac: "factors G as a" + by blast + + from factors_exist [OF bcarr bnunit] + obtain bs where bscarr: "set bs \ carrier G" and bfac: "factors G bs b" + by blast + + from factors_exist [OF ccarr cnunit] + obtain cs where cscarr: "set cs \ carrier G" and cfac: "factors G cs c" by auto note [simp] = ascarr bscarr cscarr @@ -2227,16 +2191,12 @@ from abfac' abfac have "essentially_equal G (p # cs) (as @ bs)" by (rule factors_unique) (fact | simp)+ - then have "\ds. p # cs <~~> ds \ ds [\] (as @ bs)" + then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\] (as @ bs)" by (fast elim: essentially_equalE) - then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\] (as @ bs)" - by auto then have "p \ set ds" by (simp add: perm_set_eq[symmetric]) - with dsassoc have "\p'. p' \ set (as@bs) \ p \ p'" + with dsassoc obtain p' where "p' \ set (as@bs)" and pp': "p \ p'" unfolding list_all2_conv_all_nth set_conv_nth by force - then obtain p' where "p' \ set (as@bs)" and pp': "p \ p'" - by auto then consider "p' \ set as" | "p' \ set bs" by auto then show "p divides a \ p divides b" proof cases @@ -2333,16 +2293,15 @@ and bcarr: "b \ carrier G" shows "\c. c \ carrier G \ c gcdof a b" proof - - from acarr have "\as. set as \ carrier G \ wfactors G as a" by (rule wfactors_exist) - then obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" - by auto + from wfactors_exist [OF acarr] + obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" + by blast from afs have airr: "\a \ set as. irreducible G a" by (fast elim: wfactorsE) - from bcarr have "\bs. set bs \ carrier G \ wfactors G bs b" - by (rule wfactors_exist) - then obtain bs where bscarr: "set bs \ carrier G" and bfs: "wfactors G bs b" - by auto + from wfactors_exist [OF bcarr] + obtain bs where bscarr: "set bs \ carrier G" and bfs: "wfactors G bs b" + by blast from bfs have birr: "\b \ set bs. irreducible G b" by (fast elim: wfactorsE) @@ -2357,13 +2316,13 @@ then have "\x. X = assocs G x \ x \ set as" by (induct as) auto then obtain x where X: "X = assocs G x" and xas: "x \ set as" - by auto + by blast with ascarr have xcarr: "x \ carrier G" - by fast + by blast from xas airr have xirr: "irreducible G x" by simp from xcarr and xirr and X show "\x. (x \ carrier G \ irreducible G x) \ X = assocs G x" - by fast + by blast qed then obtain c cs where ccarr: "c \ carrier G" @@ -2385,11 +2344,10 @@ by (rule fmsubset_divides) fact+ next fix y - assume ycarr: "y \ carrier G" - then have "\ys. set ys \ carrier G \ wfactors G ys y" - by (rule wfactors_exist) - then obtain ys where yscarr: "set ys \ carrier G" and yfs: "wfactors G ys y" - by auto + assume "y \ carrier G" + from wfactors_exist [OF this] + obtain ys where yscarr: "set ys \ carrier G" and yfs: "wfactors G ys y" + by blast assume "y divides a" then have ya: "fmset G ys \# fmset G as" @@ -2413,17 +2371,15 @@ and bcarr: "b \ carrier G" shows "\c. c \ carrier G \ c lcmof a b" proof - - from acarr have "\as. set as \ carrier G \ wfactors G as a" - by (rule wfactors_exist) - then obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" - by auto + from wfactors_exist [OF acarr] + obtain as where ascarr: "set as \ carrier G" and afs: "wfactors G as a" + by blast from afs have airr: "\a \ set as. irreducible G a" by (fast elim: wfactorsE) - from bcarr have "\bs. set bs \ carrier G \ wfactors G bs b" - by (rule wfactors_exist) - then obtain bs where bscarr: "set bs \ carrier G" and bfs: "wfactors G bs b" - by auto + from wfactors_exist [OF bcarr] + obtain bs where bscarr: "set bs \ carrier G" and bfs: "wfactors G bs b" + by blast from bfs have birr: "\b \ set bs. irreducible G b" by (fast elim: wfactorsE) @@ -2475,11 +2431,10 @@ by (rule fmsubset_divides) fact+ next fix y - assume ycarr: "y \ carrier G" - then have "\ys. set ys \ carrier G \ wfactors G ys y" - by (rule wfactors_exist) - then obtain ys where yscarr: "set ys \ carrier G" and yfs: "wfactors G ys y" - by auto + assume "y \ carrier G" + from wfactors_exist [OF this] + obtain ys where yscarr: "set ys \ carrier G" and yfs: "wfactors G ys y" + by blast assume "a divides y" then have ya: "fmset G as \# fmset G ys" @@ -2516,9 +2471,8 @@ proof - fix x y assume carr: "x \ carrier G" "y \ carrier G" - then have "\z. z \ carrier G \ z gcdof x y" by (rule gcdof_exists) - then obtain z where zcarr: "z \ carrier G" and isgcd: "z gcdof x y" - by auto + from gcdof_exists [OF this] obtain z where zcarr: "z \ carrier G" and isgcd: "z gcdof x y" + by blast with carr have "greatest (division_rel G) z (Lower (division_rel G) {x, y})" by (subst gcdof_greatestLower[symmetric], simp+) then show "\z. greatest (division_rel G) z (Lower (division_rel G) {x, y})" @@ -2719,18 +2673,14 @@ from cd'ca cd'cb have cd'e: "c \ ?d divides ?e" by (rule gcd_divides) simp_all - then have "\u. u \ carrier G \ ?e = c \ ?d \ u" - by (elim dividesE) fast then obtain u where ucarr[simp]: "u \ carrier G" and e_cdu: "?e = c \ ?d \ u" - by auto + by blast note carr = carr ucarr have "?e divides c \ a" by (rule gcd_divides_l) simp_all - then have "\x. x \ carrier G \ c \ a = ?e \ x" - by (elim dividesE) fast then obtain x where xcarr: "x \ carrier G" and ca_ex: "c \ a = ?e \ x" - by auto + by blast with e_cdu have ca_cdux: "c \ a = c \ ?d \ u \ x" by simp @@ -2742,10 +2692,8 @@ by (rule dividesI[OF xcarr]) have "?e divides c \ b" by (intro gcd_divides_r) simp_all - then have "\x. x \ carrier G \ c \ b = ?e \ x" - by (elim dividesE) fast then obtain x where xcarr: "x \ carrier G" and cb_ex: "c \ b = ?e \ x" - by auto + by blast with e_cdu have cb_cdux: "c \ b = c \ ?d \ u \ x" by simp @@ -2840,7 +2788,7 @@ apply (clarsimp simp add: Unit_eq_dividesone[symmetric]) apply (rule r, rule, assumption) apply (rule properfactorI, assumption) - proof (rule ccontr, simp) + proof fix y assume ycarr: "y \ carrier G" assume "p divides y" @@ -2860,7 +2808,7 @@ apply (clarsimp simp add: Unit_eq_dividesone[symmetric]) apply (rule r, rule, assumption) apply (rule properfactorI, assumption) - proof (rule ccontr, simp) + proof fix y assume ycarr: "y \ carrier G" assume "p divides y" @@ -2921,23 +2869,20 @@ done then obtain y where ycarr: "y \ carrier G" and ynunit: "y \ Units G" and pfyx: "properfactor G y x" - by auto + by blast have ih': "\y. \y \ carrier G; properfactor G y x\ \ \as. set as \ carrier G \ wfactors G as y" by (rule ih[rule_format, simplified]) (simp add: xcarr)+ - from ycarr pfyx have "\as. set as \ carrier G \ wfactors G as y" - by (rule ih') - then obtain ys where yscarr: "set ys \ carrier G" and yfs: "wfactors G ys y" - by auto + from ih' [OF ycarr pfyx] + obtain ys where yscarr: "set ys \ carrier G" and yfs: "wfactors G ys y" + by blast from pfyx have "y divides x" and nyx: "\ y \