# HG changeset patch
# User paulson
# Date 1529618772 -3600
# Node ID f839ce4af873343accf5428d0a78d4aaf8c7d27b
# Parent  f090b313fdc891ed592a7a99c8dea4f91abb4e25# Parent  f75a7d2be8c55a6ea508e8bb678a2c6a12b02945
merged

diff -r f090b313fdc8 -r f839ce4af873 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Thu Jun 21 12:39:52 2018 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Thu Jun 21 23:06:12 2018 +0100
@@ -659,9 +659,7 @@
     and aa': "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"
   shows "irreducible G a'"
   using assms
-  apply (elim irreducibleE, intro irreducibleI)
-   apply simp_all
-   apply (metis assms(2) assms(3) assoc_unit_l)
+  apply (auto simp: irreducible_def assoc_unit_l)
   apply (metis aa' associated_sym properfactor_cong_r)
   done
 
@@ -757,12 +755,11 @@
   using assms by (blast elim: primeE)
 
 lemma (in monoid_cancel) prime_cong [trans]:
-  assumes pprime: "prime G p"
+  assumes "prime G p"
     and pp': "p \<sim> p'" "p \<in> carrier G"  "p' \<in> carrier G"
   shows "prime G p'"
-  using pprime
-  apply (elim primeE, intro primeI)
-   apply (metis assms(2) assms(3) assoc_unit_l)
+  using assms
+  apply (auto simp: prime_def assoc_unit_l)
   apply (metis pp' associated_sym divides_cong_l)
   done
 
@@ -1015,14 +1012,13 @@
     and ascarr: "set as \<subseteq> carrier G"
   shows "foldr (\<otimes>) as \<one> = foldr (\<otimes>) bs \<one>"
   using prm ascarr
-  apply (induct, simp, clarsimp simp add: m_ac, clarsimp)
-proof clarsimp
-  fix xs ys zs
-  assume "xs <~~> ys"  "set xs \<subseteq> carrier G"
-  then have "set ys \<subseteq> carrier G" by (rule perm_closed)
-  moreover assume "set ys \<subseteq> carrier G \<Longrightarrow> foldr (\<otimes>) ys \<one> = foldr (\<otimes>) zs \<one>"
-  ultimately show "foldr (\<otimes>) ys \<one> = foldr (\<otimes>) zs \<one>" by simp
-qed
+proof induction
+  case (swap y x l) then show ?case
+    by (simp add: m_lcomm)
+next
+  case (trans xs ys zs) then show ?case
+    using perm_closed by auto
+qed auto
 
 lemma (in comm_monoid_cancel) multlist_ee_cong:
   assumes "essentially_equal G fs fs'"
@@ -1673,23 +1669,17 @@
   from surjE[OF surj_mset] obtain Cs' where Cs: "Cs = mset Cs'"
     by blast
   have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> mset (map (assocs G) cs) = Cs"
-    using elems
-    unfolding Cs
-    apply (induct Cs', simp)
-  proof (clarsimp simp del: mset_map)
-    fix a Cs' cs
-    assume ih: "\<And>X. X = a \<or> X \<in> set Cs' \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
-      and csP: "\<forall>x\<in>set cs. P x"
-      and mset: "mset (map (assocs G) cs) = mset Cs'"
-    from ih obtain c where cP: "P c" and a: "a = assocs G c"
-      by auto
-    from cP csP have tP: "\<forall>x\<in>set (c#cs). P x"
+    using elems unfolding Cs
+  proof (induction Cs')
+    case (Cons a Cs')
+    then obtain c cs where csP: "\<forall>x\<in>set cs. P x" and mset: "mset (map (assocs G) cs) = mset Cs'"
+            and cP: "P c" and a: "a = assocs G c"
+      by force
+    then have tP: "\<forall>x\<in>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 "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and> mset (map (assocs G) cs) = add_mset a (mset Cs')"
-      by fast
-  qed
+    show ?case
+      using tP mset a by fastforce
+  qed auto
   then show ?thesis by (simp add: fmset_def)
 qed
 
@@ -1851,15 +1841,11 @@
     and "set as \<subseteq> carrier G"
     and "set bs \<subseteq> carrier G"
   shows "properfactor G a b"
-  apply (rule properfactorI)
-   apply (rule fmsubset_divides[of as bs], fact+)
-proof
-  assume "b divides a"
-  then have "fmset G bs \<subseteq># fmset G as"
-    by (rule divides_fmsubset) fact+
-  with asubb have "fmset G as = fmset G bs"
-    by (rule subset_mset.antisym)
-  with anb show False ..
+proof (rule properfactorI)
+  show "a divides b"
+    using assms asubb fmsubset_divides by blast
+  show "\<not> b divides a"
+    by (meson anb assms asubb factorial_monoid.divides_fmsubset factorial_monoid_axioms subset_mset.antisym)
 qed
 
 lemma (in factorial_monoid) properfactor_fmset:
@@ -1879,8 +1865,7 @@
 subsection \<open>Irreducible Elements are Prime\<close>
 
 lemma (in factorial_monoid) irreducible_prime:
-  assumes pirr: "irreducible G p"
-    and pcarr: "p \<in> carrier G"
+  assumes pirr: "irreducible G p" and pcarr: "p \<in> carrier G"
   shows "prime G p"
   using pirr
 proof (elim irreducibleE, intro primeI)
@@ -1892,32 +1877,19 @@
     "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"
   from pdvdab obtain c where ccarr: "c \<in> carrier G" and abpc: "a \<otimes> b = p \<otimes> c"
     by (rule dividesE)
-
-  from wfactors_exist [OF acarr]
   obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
-    by blast
-
-  from wfactors_exist [OF bcarr]
+    using wfactors_exist [OF acarr] by blast
   obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b"
-    by auto
-
-  from wfactors_exist [OF ccarr]
+    using wfactors_exist [OF bcarr] by blast
   obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"
-    by auto
-
+    using wfactors_exist [OF ccarr] by blast
   note carr[simp] = pcarr acarr bcarr ccarr ascarr bscarr cscarr
-
-  from afs and bfs have abfs: "wfactors G (as @ bs) (a \<otimes> b)"
-    by (rule wfactors_mult) fact+
-
-  from pirr cfs have pcfs: "wfactors G (p # cs) (p \<otimes> c)"
-    by (rule wfactors_mult_single) fact+
-  with abpc have abfs': "wfactors G (p # cs) (a \<otimes> b)"
-    by simp
-
-  from abfs' abfs have "essentially_equal G (p # cs) (as @ bs)"
+  from pirr cfs  abpc have "wfactors G (p # cs) (a \<otimes> b)"
+    by (simp add: wfactors_mult_single)
+  moreover have  "wfactors G (as @ bs) (a \<otimes> b)"
+    by (rule wfactors_mult [OF afs bfs]) fact+
+  ultimately have "essentially_equal G (p # cs) (as @ bs)"
     by (rule wfactors_unique) simp+
-
   then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)"
     by (fast elim: essentially_equalE)
   then have "p \<in> set ds"
@@ -1926,138 +1898,69 @@
     unfolding list_all2_conv_all_nth set_conv_nth by force
   then consider "p' \<in> set as" | "p' \<in> set bs" by auto
   then show "p divides a \<or> p divides b"
-  proof cases
-    case 1
-    with ascarr have [simp]: "p' \<in> carrier G" by fast
-
-    note pp'
-    also from afs
-    have "p' divides a" by (rule wfactors_dividesI) fact+
-    finally have "p divides a" by simp
-    then show ?thesis ..
-  next
-    case 2
-    with bscarr have [simp]: "p' \<in> carrier G" by fast
-
-    note pp'
-    also from bfs
-    have "p' divides b" by (rule wfactors_dividesI) fact+
-    finally have "p divides b" by simp
-    then show ?thesis ..
-  qed
+    using afs bfs divides_cong_l pp' wfactors_dividesI
+    by (meson acarr ascarr bcarr bscarr pcarr)
 qed
 
 
 \<comment> \<open>A version using @{const factors}, more complicated\<close>
 lemma (in factorial_monoid) factors_irreducible_prime:
-  assumes pirr: "irreducible G p"
-    and pcarr: "p \<in> carrier G"
+  assumes pirr: "irreducible G p" and pcarr: "p \<in> carrier G"
   shows "prime G p"
-  using pirr
-  apply (elim irreducibleE, intro primeI)
-   apply assumption
-proof -
-  fix a b
-  assume acarr: "a \<in> carrier G"
-    and bcarr: "b \<in> carrier G"
-    and pdvdab: "p divides (a \<otimes> b)"
-  assume irreduc[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"
-  from pdvdab obtain c where ccarr: "c \<in> carrier G" and abpc: "a \<otimes> b = p \<otimes> c"
-    by (rule dividesE)
-  note [simp] = pcarr acarr bcarr ccarr
-
-  show "p divides a \<or> p divides b"
-  proof (cases "a \<in> Units G")
-    case aunit: True
-
-    note pdvdab
-    also have "a \<otimes> b = b \<otimes> a" by (simp add: m_comm)
-    also from aunit have bab: "b \<otimes> a \<sim> b"
-      by (intro associatedI2[of "a"], simp+)
-    finally have "p divides b" by simp
-    then show ?thesis ..
-  next
-    case anunit: False
-    show ?thesis
-    proof (cases "b \<in> Units G")
-      case bunit: True
-      note pdvdab
-      also from bunit
-      have baa: "a \<otimes> b \<sim> a"
-        by (intro associatedI2[of "b"], simp+)
-      finally have "p divides a" by simp
+proof (rule primeI)
+  show "p \<notin> Units G"
+    by (meson irreducibleE pirr)
+  have irreduc: "\<And>b. \<lbrakk>b \<in> carrier G; properfactor G b p\<rbrakk> \<Longrightarrow> b \<in> Units G"
+    using pirr by (auto simp: irreducible_def)
+  show "p divides a \<or> p divides b" 
+    if acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and pdvdab: "p divides (a \<otimes> b)" for a b
+  proof -
+    from pdvdab obtain c where ccarr: "c \<in> carrier G" and abpc: "a \<otimes> b = p \<otimes> c"
+      by (rule dividesE)
+    note [simp] = pcarr acarr bcarr ccarr
+
+    show "p divides a \<or> p divides b"
+    proof (cases "a \<in> Units G")
+      case True
+      then have "p divides b"
+        by (metis acarr associatedI2' associated_def bcarr divides_trans m_comm pcarr pdvdab) 
       then show ?thesis ..
     next
-      case bnunit: False
-      have cnunit: "c \<notin> Units G"
-      proof
-        assume cunit: "c \<in> Units G"
-        from bnunit have "properfactor G a (a \<otimes> b)"
-          by (intro properfactorI3[of _ _ b], simp+)
-        also note abpc
-        also from cunit have "p \<otimes> c \<sim> p"
-          by (intro associatedI2[of c], simp+)
-        finally have "properfactor G a p" by simp
-        with acarr have "a \<in> Units G" by (fast intro: irreduc)
-        with anunit show False ..
-      qed
-
-      have abnunit: "a \<otimes> b \<notin> Units G"
-      proof clarsimp
-        assume "a \<otimes> b \<in> Units G"
-        then have "a \<in> Units G" by (rule unit_factor) fact+
-        with anunit show False ..
-      qed
-
-      from factors_exist [OF acarr anunit]
-      obtain as where ascarr: "set as \<subseteq> carrier G" and afac: "factors G as a"
-        by blast
-
-      from factors_exist [OF bcarr bnunit]
-      obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfac: "factors G bs b"
-        by blast
-
-      from factors_exist [OF ccarr cnunit]
-      obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfac: "factors G cs c"
-        by auto
-
-      note [simp] = ascarr bscarr cscarr
-
-      from afac and bfac have abfac: "factors G (as @ bs) (a \<otimes> b)"
-        by (rule factors_mult) fact+
-
-      from pirr cfac have pcfac: "factors G (p # cs) (p \<otimes> c)"
-        by (rule factors_mult_single) fact+
-      with abpc have abfac': "factors G (p # cs) (a \<otimes> b)"
-        by simp
-
-      from abfac' abfac have "essentially_equal G (p # cs) (as @ bs)"
-        by (rule factors_unique) (fact | simp)+
-      then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)"
-        by (fast elim: essentially_equalE)
-      then have "p \<in> set ds"
-        by (simp add: perm_set_eq[symmetric])
-      with dsassoc obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'"
-        unfolding list_all2_conv_all_nth set_conv_nth by force
-      then consider "p' \<in> set as" | "p' \<in> set bs" by auto
-      then show "p divides a \<or> p divides b"
-      proof cases
-        case 1
-        with ascarr have [simp]: "p' \<in> carrier G" by fast
-
-        note pp'
-        also from afac 1 have "p' divides a" by (rule factors_dividesI) fact+
-        finally have "p divides a" by simp
+      case anunit: False
+      show ?thesis
+      proof (cases "b \<in> Units G")
+        case True 
+        then have "p divides a"
+          by (meson acarr bcarr divides_unit irreducible_prime pcarr pdvdab pirr prime_def)
         then show ?thesis ..
       next
-        case 2
-        with bscarr have [simp]: "p' \<in> carrier G" by fast
-
-        note pp'
-        also from bfac
-        have "p' divides b" by (rule factors_dividesI) fact+
-        finally have "p divides b" by simp
-        then show ?thesis ..
+        case bnunit: False
+        then have cnunit: "c \<notin> Units G"
+          by (metis abpc acarr anunit bcarr ccarr irreducible_prodE irreducible_prod_rI pcarr pirr)
+        then have abnunit: "a \<otimes> b \<notin> Units G"
+          using acarr anunit bcarr unit_factor by blast
+        obtain as where ascarr: "set as \<subseteq> carrier G" and afac: "factors G as a"
+          using factors_exist [OF acarr anunit] by blast
+        obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfac: "factors G bs b"
+          using factors_exist [OF bcarr bnunit] by blast
+        obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfac: "factors G cs c"
+          using factors_exist [OF ccarr cnunit] by auto
+        note [simp] = ascarr bscarr cscarr
+        from pirr cfac abpc have abfac': "factors G (p # cs) (a \<otimes> b)"
+          by (simp add: factors_mult_single)
+        from afac and bfac have "factors G (as @ bs) (a \<otimes> b)"
+          by (rule factors_mult) fact+
+        with abfac' have "essentially_equal G (p # cs) (as @ bs)"
+          using abnunit factors_unique by auto
+        then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)"
+          by (fast elim: essentially_equalE)
+        then have "p \<in> set ds"
+          by (simp add: perm_set_eq[symmetric])
+        with dsassoc obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'"
+          unfolding list_all2_conv_all_nth set_conv_nth by force
+        then consider "p' \<in> set as" | "p' \<in> set bs" by auto
+        then show "p divides a \<or> p divides b"
+          by (meson afac bfac divides_cong_l factors_dividesI pp' ascarr bscarr pcarr)
       qed
     qed
   qed
@@ -2597,73 +2500,47 @@
 qed
 
 lemma (in gcd_condition_monoid) primeness_condition: "primeness_condition_monoid G"
-  apply unfold_locales
-  apply (rule primeI)
-   apply (elim irreducibleE, assumption)
 proof -
-  fix p a b
-  assume pcarr: "p \<in> carrier G" and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
-    and pirr: "irreducible G p"
-    and pdvdab: "p divides a \<otimes> b"
-  from pirr have pnunit: "p \<notin> Units G"
-    and r[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"
-    by (fast elim: irreducibleE)+
-
-  show "p divides a \<or> p divides b"
-  proof (rule ccontr, clarsimp)
-    assume npdvda: "\<not> p divides a"
-    with pcarr acarr have "\<one> \<sim> somegcd G p a"
-      apply (intro gcdI, simp, simp, simp)
-           apply (fast intro: unit_divides)
-          apply (fast intro: unit_divides)
-         apply (clarsimp simp add: Unit_eq_dividesone[symmetric])
-         apply (rule r, rule, assumption)
-         apply (rule properfactorI, assumption)
-    proof
-      fix y
-      assume ycarr: "y \<in> carrier G"
-      assume "p divides y"
-      also assume "y divides a"
-      finally have "p divides a"
-        by (simp add: pcarr ycarr acarr)
-      with npdvda show False ..
-    qed simp_all
-    with pcarr acarr have pa: "somegcd G p a \<sim> \<one>"
-      by (fast intro: associated_sym[of "\<one>"] gcd_closed)
-
-    assume npdvdb: "\<not> p divides b"
-    with pcarr bcarr have "\<one> \<sim> somegcd G p b"
-      apply (intro gcdI, simp, simp, simp)
-           apply (fast intro: unit_divides)
-          apply (fast intro: unit_divides)
-         apply (clarsimp simp add: Unit_eq_dividesone[symmetric])
-         apply (rule r, rule, assumption)
-         apply (rule properfactorI, assumption)
-    proof
-      fix y
-      assume ycarr: "y \<in> carrier G"
-      assume "p divides y"
-      also assume "y divides b"
-      finally have "p divides b" by (simp add: pcarr ycarr bcarr)
-      with npdvdb
-      show "False" ..
-    qed simp_all
-    with pcarr bcarr have pb: "somegcd G p b \<sim> \<one>"
-      by (fast intro: associated_sym[of "\<one>"] gcd_closed)
-
-    from pcarr acarr bcarr pdvdab have "p gcdof p (a \<otimes> b)"
-      by (fast intro: isgcd_divides_l)
-    with pcarr acarr bcarr have "p \<sim> somegcd G p (a \<otimes> b)"
-      by (fast intro: gcdI2)
-    also from pa pb pcarr acarr bcarr have "somegcd G p (a \<otimes> b) \<sim> \<one>"
-      by (rule relprime_mult)
-    finally have "p \<sim> \<one>"
-      by (simp add: pcarr acarr bcarr)
-    with pcarr have "p \<in> Units G"
-      by (fast intro: assoc_unit_l)
-    with pnunit show False ..
+  have *: "p divides a \<or> p divides b"
+    if pcarr[simp]: "p \<in> carrier G" and acarr[simp]: "a \<in> carrier G" and bcarr[simp]: "b \<in> carrier G"
+      and pirr: "irreducible G p" and pdvdab: "p divides a \<otimes> b"
+    for p a b
+  proof -
+    from pirr have pnunit: "p \<notin> Units G"
+      and r: "\<And>b. \<lbrakk>b \<in> carrier G; properfactor G b p\<rbrakk> \<Longrightarrow> b \<in> Units G"
+      by (fast elim: irreducibleE)+
+    show "p divides a \<or> p divides b"
+    proof (rule ccontr, clarsimp)
+      assume npdvda: "\<not> p divides a" and npdvdb: "\<not> p divides b"
+      have "\<one> \<sim> somegcd G p a"
+      proof (intro gcdI unit_divides)
+        show "\<And>y. \<lbrakk>y \<in> carrier G; y divides p; y divides a\<rbrakk> \<Longrightarrow> y \<in> Units G"
+          by (meson divides_trans npdvda pcarr properfactorI r)
+      qed auto
+      with pcarr acarr have pa: "somegcd G p a \<sim> \<one>"
+        by (fast intro: associated_sym[of "\<one>"] gcd_closed)
+      have "\<one> \<sim> somegcd G p b"
+      proof (intro gcdI unit_divides)
+        show "\<And>y. \<lbrakk>y \<in> carrier G; y divides p; y divides b\<rbrakk> \<Longrightarrow> y \<in> Units G"
+          by (meson divides_trans npdvdb pcarr properfactorI r)
+      qed auto
+      with pcarr bcarr have pb: "somegcd G p b \<sim> \<one>"
+        by (fast intro: associated_sym[of "\<one>"] gcd_closed)
+      have "p \<sim> somegcd G p (a \<otimes> b)"
+        using pdvdab by (simp add: gcdI2 isgcd_divides_l)
+      also from pa pb pcarr acarr bcarr have "somegcd G p (a \<otimes> b) \<sim> \<one>"
+        by (rule relprime_mult)
+      finally have "p \<sim> \<one>"
+        by simp
+      with pcarr have "p \<in> Units G"
+        by (fast intro: assoc_unit_l)
+      with pnunit show False ..
+    qed
   qed
-qed
+  show ?thesis
+    by unfold_locales (metis * primeI irreducibleE)
+qed    
+
 
 sublocale gcd_condition_monoid \<subseteq> primeness_condition_monoid
   by (rule primeness_condition)
@@ -2675,63 +2552,45 @@
   assumes acarr: "a \<in> carrier G"
   shows "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"
 proof -
-  have r[rule_format]: "a \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a)"
-  proof (rule wf_induct[OF division_wellfounded])
-    fix x
-    assume ih: "\<forall>y. (y, x) \<in> {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}
-                    \<longrightarrow> y \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y)"
-
-    show "x \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as x)"
-      apply clarify
-      apply (cases "x \<in> Units G")
-       apply (rule exI[of _ "[]"], simp)
-      apply (cases "irreducible G x")
-       apply (rule exI[of _ "[x]"], simp add: wfactors_def)
-    proof -
-      assume xcarr: "x \<in> carrier G"
-        and xnunit: "x \<notin> Units G"
-        and xnirr: "\<not> irreducible G x"
-      then have "\<exists>y. y \<in> carrier G \<and> properfactor G y x \<and> y \<notin> Units G"
-        apply -
-        apply (rule ccontr)
-        apply simp
-        apply (subgoal_tac "irreducible G x", simp)
-        apply (rule irreducibleI, simp, simp)
-        done
-      then obtain y where ycarr: "y \<in> carrier G" and ynunit: "y \<notin> Units G"
-        and pfyx: "properfactor G y x"
-        by blast
-
-      have ih': "\<And>y. \<lbrakk>y \<in> carrier G; properfactor G y x\<rbrakk>
-          \<Longrightarrow> \<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y"
-        by (rule ih[rule_format, simplified]) (simp add: xcarr)+
-
-      from ih' [OF ycarr pfyx]
-      obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"
-        by blast
-
-      from pfyx have "y divides x" and nyx: "\<not> y \<sim> x"
-        by (fast elim: properfactorE2)+
-      then obtain z where zcarr: "z \<in> carrier G" and x: "x = y \<otimes> z"
-        by blast
-
-      from zcarr ycarr have "properfactor G z x"
-        apply (subst x)
-        apply (intro properfactorI3[of _ _ y])
-            apply (simp add: m_comm)
-           apply (simp add: ynunit)+
-        done
-      from ih' [OF zcarr this]
-      obtain zs where zscarr: "set zs \<subseteq> carrier G" and zfs: "wfactors G zs z"
-        by blast
-      from yscarr zscarr have xscarr: "set (ys@zs) \<subseteq> carrier G"
-        by simp
-      from yfs zfs ycarr zcarr yscarr zscarr have "wfactors G (ys@zs) (y\<otimes>z)"
-        by (rule wfactors_mult)
-      then have "wfactors G (ys@zs) x"
-        by (simp add: x)
-      with xscarr show "\<exists>xs. set xs \<subseteq> carrier G \<and> wfactors G xs x"
-        by fast
+  have r: "a \<in> carrier G \<Longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a)"
+    using division_wellfounded
+  proof (induction rule: wf_induct_rule)
+    case (less x)
+    then have xcarr: "x \<in> carrier G"
+      by auto
+    show ?case
+    proof (cases "x \<in> Units G")
+      case True
+      then show ?thesis
+        by (metis bot.extremum list.set(1) unit_wfactors)
+    next
+      case xnunit: False
+      show ?thesis
+      proof (cases "irreducible G x")
+        case True
+        then show ?thesis
+          by (rule_tac x="[x]" in exI) (simp add: wfactors_def xcarr)
+      next
+        case False
+        then obtain y where ycarr: "y \<in> carrier G" and ynunit: "y \<notin> Units G" and pfyx: "properfactor G y x"
+          by (meson irreducible_def xnunit)
+        obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"
+          using less ycarr pfyx by blast
+        then obtain z where zcarr: "z \<in> carrier G" and x: "x = y \<otimes> z"
+          by (meson dividesE pfyx properfactorE2)
+        from zcarr ycarr have "properfactor G z x"
+          using m_comm properfactorI3 x ynunit by blast
+        with less zcarr obtain zs where zscarr: "set zs \<subseteq> carrier G" and zfs: "wfactors G zs z"
+          by blast
+        from yscarr zscarr have xscarr: "set (ys@zs) \<subseteq> carrier G"
+          by simp
+        have "wfactors G (ys@zs) (y\<otimes>z)"
+          using xscarr ycarr yfs zcarr zfs by auto
+        then have "wfactors G (ys@zs) x"
+          by (simp add: x)
+        with xscarr show "\<exists>xs. set xs \<subseteq> carrier G \<and> wfactors G xs x"
+          by fast
+      qed
     qed
   qed
   from acarr show ?thesis by (rule r)
@@ -2741,64 +2600,33 @@
 subsubsection \<open>Primeness condition\<close>
 
 lemma (in comm_monoid_cancel) multlist_prime_pos:
-  assumes carr: "a \<in> carrier G"  "set as \<subseteq> carrier G"
-    and aprime: "prime G a"
-    and "a divides (foldr (\<otimes>) as \<one>)"
-  shows "\<exists>i<length as. a divides (as!i)"
-proof -
-  have r[rule_format]: "set as \<subseteq> carrier G \<and> a divides (foldr (\<otimes>) as \<one>)
-    \<longrightarrow> (\<exists>i. i < length as \<and> a divides (as!i))"
-    apply (induct as)
-     apply clarsimp defer 1
-     apply clarsimp defer 1
-  proof -
-    assume "a divides \<one>"
-    with carr have "a \<in> Units G"
-      by (fast intro: divides_unit[of a \<one>])
-    with aprime show False
-      by (elim primeE, simp)
-  next
-    fix aa as
-    assume ih[rule_format]: "a divides foldr (\<otimes>) as \<one> \<longrightarrow> (\<exists>i<length as. a divides as ! i)"
-      and carr': "aa \<in> carrier G"  "set as \<subseteq> carrier G"
-      and "a divides aa \<otimes> foldr (\<otimes>) as \<one>"
-    with carr aprime have "a divides aa \<or> a divides foldr (\<otimes>) as \<one>"
-      by (intro prime_divides) simp+
-    then show "\<exists>i<Suc (length as). a divides (aa # as) ! i"
-    proof
-      assume "a divides aa"
-      then have p1: "a divides (aa#as)!0" by simp
-      have "0 < Suc (length as)" by simp
-      with p1 show ?thesis by fast
-    next
-      assume "a divides foldr (\<otimes>) as \<one>"
-      from ih [OF this] obtain i where "a divides as ! i" and len: "i < length as" by auto
-      then have p1: "a divides (aa#as) ! (Suc i)" by simp
-      from len have "Suc i < Suc (length as)" by simp
-      with p1 show ?thesis by force
-   qed
-  qed
-  from assms show ?thesis
-    by (intro r) auto
+  assumes aprime: "prime G a" and carr: "a \<in> carrier G" 
+     and as: "set as \<subseteq> carrier G" "a divides (foldr (\<otimes>) as \<one>)"
+   shows "\<exists>i<length as. a divides (as!i)"
+  using as
+proof (induction as)
+  case Nil
+  then show ?case
+    by simp (meson Units_one_closed aprime carr divides_unit primeE)
+next
+  case (Cons x as)
+  then have "x \<in> carrier G"  "set as \<subseteq> carrier G" and "a divides x \<otimes> foldr (\<otimes>) as \<one>"
+    by (auto simp: )
+  with carr aprime have "a divides x \<or> a divides foldr (\<otimes>) as \<one>"
+    by (intro prime_divides) simp+
+  then show ?case
+    using Cons.IH Cons.prems(1) by force
 qed
 
+
 lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:
   "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and>
            wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"
 proof (induct as)
   case Nil
   show ?case
-  proof auto
-    fix a as'
-    assume a: "a \<in> carrier G"
-    assume "wfactors G [] a"
-    then obtain "\<one> \<sim> a" by (auto elim: wfactorsE)
-    with a have "a \<in> Units G" by (auto intro: assoc_unit_r)
-    moreover assume "wfactors G as' a"
-    moreover assume "set as' \<subseteq> carrier G"
-    ultimately have "as' = []" by (rule unit_wfactors_empty)
-    then show "essentially_equal G [] as'" by simp
-  qed
+    apply (clarsimp simp: wfactors_def)
+    by (metis Units_one_closed assoc_unit_r list_update_nonempty unit_wfactors_empty unitfactor_ee wfactorsI)
 next
   case (Cons ah as)
   then show ?case