# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1529446260 -3600
# Node ID 7ddcce75c3ee5a63a48eaaa0329517d9c354bd9c
# Parent  ae42b0f6885d9988c1513958fcac78416629d1d1
Partial de-apply of Divisibility

diff -r ae42b0f6885d -r 7ddcce75c3ee src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Tue Jun 19 12:14:31 2018 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Tue Jun 19 23:11:00 2018 +0100
@@ -189,39 +189,31 @@
   by (intro dividesI[of "\<one>"]) (simp_all add: carr)
 
 lemma (in monoid) divides_trans [trans]:
-  assumes dvds: "a divides b"  "b divides c"
+  assumes dvds: "a divides b" "b divides c"
     and acarr: "a \<in> carrier G"
   shows "a divides c"
   using dvds[THEN dividesD] by (blast intro: dividesI m_assoc acarr)
 
 lemma (in monoid) divides_mult_lI [intro]:
-  assumes ab: "a divides b"
-    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  assumes  "a divides b" "a \<in> carrier G" "c \<in> carrier G"
   shows "(c \<otimes> a) divides (c \<otimes> b)"
-  using ab
-  apply (elim dividesE)
-  apply (simp add: m_assoc[symmetric] carr)
-  apply (fast intro: dividesI)
-  done
+  by (metis assms factor_def m_assoc)
 
 lemma (in monoid_cancel) divides_mult_l [simp]:
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "(c \<otimes> a) divides (c \<otimes> b) = a divides b"
-  apply safe
-   apply (elim dividesE, intro dividesI, assumption)
-   apply (rule l_cancel[of c])
-      apply (simp add: m_assoc carr)+
-  apply (fast intro: carr)
-  done
+proof
+  show "c \<otimes> a divides c \<otimes> b \<Longrightarrow> a divides b"
+    using carr monoid.m_assoc monoid_axioms monoid_cancel.l_cancel monoid_cancel_axioms by fastforce
+  show "a divides b \<Longrightarrow> c \<otimes> a divides c \<otimes> b"
+  using carr(1) carr(3) by blast
+qed
 
 lemma (in comm_monoid) divides_mult_rI [intro]:
   assumes ab: "a divides b"
     and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "(a \<otimes> c) divides (b \<otimes> c)"
-  using carr ab
-  apply (simp add: m_comm[of a c] m_comm[of b c])
-  apply (rule divides_mult_lI, assumption+)
-  done
+  using carr ab by (metis divides_mult_lI m_comm)
 
 lemma (in comm_monoid_cancel) divides_mult_r [simp]:
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
@@ -230,18 +222,14 @@
 
 lemma (in monoid) divides_prod_r:
   assumes ab: "a divides b"
-    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+    and carr: "a \<in> carrier G" "c \<in> carrier G"
   shows "a divides (b \<otimes> c)"
   using ab carr by (fast intro: m_assoc)
 
 lemma (in comm_monoid) divides_prod_l:
-  assumes carr[intro]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
-    and ab: "a divides b"
+  assumes "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" "a divides b"
   shows "a divides (c \<otimes> b)"
-  using ab carr
-  apply (simp add: m_comm[of c b])
-  apply (fast intro: divides_prod_r)
-  done
+  using assms  by (simp add: divides_prod_r m_comm)
 
 lemma (in monoid) unit_divides:
   assumes uunit: "u \<in> Units G"
@@ -272,22 +260,20 @@
 
 lemma associatedI:
   fixes G (structure)
-  assumes "a divides b"  "b divides a"
+  assumes "a divides b" "b divides a"
   shows "a \<sim> b"
   using assms by (simp add: associated_def)
 
 lemma (in monoid) associatedI2:
   assumes uunit[simp]: "u \<in> Units G"
     and a: "a = b \<otimes> u"
-    and bcarr[simp]: "b \<in> carrier G"
+    and bcarr: "b \<in> carrier G"
   shows "a \<sim> b"
   using uunit bcarr
   unfolding a
   apply (intro associatedI)
-   apply (rule dividesI[of "inv u"], simp)
-   apply (simp add: m_assoc Units_closed)
-  apply fast
-  done
+  apply (metis Units_closed divides_mult_lI one_closed r_one unit_divides)
+  by blast
 
 lemma (in monoid) associatedI2':
   assumes "a = b \<otimes> u"
@@ -304,7 +290,7 @@
 
 lemma (in monoid_cancel) associatedD2:
   assumes assoc: "a \<sim> b"
-    and carr: "a \<in> carrier G"  "b \<in> carrier G"
+    and carr: "a \<in> carrier G" "b \<in> carrier G"
   shows "\<exists>u\<in>Units G. a = b \<otimes> u"
   using assoc
   unfolding associated_def
@@ -370,13 +356,12 @@
 
 lemma (in monoid) associated_sym [sym]:
   assumes "a \<sim> b"
-    and "a \<in> carrier G"  "b \<in> carrier G"
   shows "b \<sim> a"
   using assms by (iprover intro: associatedI elim: associatedE)
 
 lemma (in monoid) associated_trans [trans]:
   assumes "a \<sim> b"  "b \<sim> c"
-    and "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+    and "a \<in> carrier G" "c \<in> carrier G"
   shows "a \<sim> c"
   using assms by (iprover intro: associatedI divides_trans elim: associatedE)
 
@@ -390,93 +375,48 @@
 
 subsubsection \<open>Division and associativity\<close>
 
-lemma divides_antisym:
-  fixes G (structure)
-  assumes "a divides b"  "b divides a"
-    and "a \<in> carrier G"  "b \<in> carrier G"
-  shows "a \<sim> b"
-  using assms by (fast intro: associatedI)
+lemmas divides_antisym = associatedI
 
 lemma (in monoid) divides_cong_l [trans]:
-  assumes "x \<sim> x'"
-    and "x' divides y"
-    and [simp]: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
+  assumes "x \<sim> x'" "x' divides y" "x \<in> carrier G" 
   shows "x divides y"
-proof -
-  from assms(1) have "x divides x'" by (simp add: associatedD)
-  also note assms(2)
-  finally show "x divides y" by simp
-qed
+  by (meson assms associatedD divides_trans)
 
 lemma (in monoid) divides_cong_r [trans]:
-  assumes "x divides y"
-    and "y \<sim> y'"
-    and [simp]: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
+  assumes "x divides y" "y \<sim> y'" "x \<in> carrier G" 
   shows "x divides y'"
-proof -
-  note assms(1)
-  also from assms(2) have "y divides y'" by (simp add: associatedD)
-  finally show "x divides y'" by simp
-qed
+  by (meson assms associatedD divides_trans)
 
 lemma (in monoid) division_weak_partial_order [simp, intro!]:
   "weak_partial_order (division_rel G)"
   apply unfold_locales
-        apply simp_all
-      apply (simp add: associated_sym)
-     apply (blast intro: associated_trans)
-    apply (simp add: divides_antisym)
-   apply (blast intro: divides_trans)
-  apply (blast intro: divides_cong_l divides_cong_r associated_sym)
-  done
+      apply (simp_all add: associated_sym divides_antisym)
+     apply (metis associated_trans)
+   apply (metis divides_trans)
+  by (meson associated_def divides_trans)
 
 
 subsubsection \<open>Multiplication and associativity\<close>
 
 lemma (in monoid_cancel) mult_cong_r:
-  assumes "b \<sim> b'"
-    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"
+  assumes "b \<sim> b'" "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"
   shows "a \<otimes> b \<sim> a \<otimes> b'"
-  using assms
-  apply (elim associatedE2, intro associatedI2)
-      apply (auto intro: m_assoc[symmetric])
-  done
+  by (meson assms associated_def divides_mult_lI)
 
 lemma (in comm_monoid_cancel) mult_cong_l:
-  assumes "a \<sim> a'"
-    and carr: "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
+  assumes "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
   shows "a \<otimes> b \<sim> a' \<otimes> b"
-  using assms
-  apply (elim associatedE2, intro associatedI2)
-      apply assumption
-     apply (simp add: m_assoc Units_closed)
-     apply (simp add: m_comm Units_closed)
-    apply simp_all
-  done
+  using assms m_comm mult_cong_r by auto
 
 lemma (in monoid_cancel) assoc_l_cancel:
-  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"
-    and "a \<otimes> b \<sim> a \<otimes> b'"
+  assumes "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G" "a \<otimes> b \<sim> a \<otimes> b'"
   shows "b \<sim> b'"
-  using assms
-  apply (elim associatedE2, intro associatedI2)
-      apply assumption
-     apply (rule l_cancel[of a])
-        apply (simp add: m_assoc Units_closed)
-       apply fast+
-  done
+  by (meson assms associated_def divides_mult_l)
 
 lemma (in comm_monoid_cancel) assoc_r_cancel:
-  assumes "a \<otimes> b \<sim> a' \<otimes> b"
-    and carr: "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
+  assumes "a \<otimes> b \<sim> a' \<otimes> b" "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
   shows "a \<sim> a'"
-  using assms
-  apply (elim associatedE2, intro associatedI2)
-      apply assumption
-     apply (rule r_cancel[of a b])
-        apply (metis Units_closed assms(3) assms(4) m_ac)
-       apply fast+
-  done
+  using assms assoc_l_cancel m_comm by presburger
 
 
 subsubsection \<open>Units\<close>
@@ -507,29 +447,23 @@
   using units by (fast intro: associatedI unit_divides)
 
 lemma (in monoid) Units_are_ones: "Units G {.=}\<^bsub>(division_rel G)\<^esub> {\<one>}"
-  apply (simp add: set_eq_def elem_def, rule, simp_all)
-proof clarsimp
-  fix a
-  assume aunit: "a \<in> Units G"
-  show "a \<sim> \<one>"
-    apply (rule associatedI)
-     apply (fast intro: dividesI[of "inv a"] aunit Units_r_inv[symmetric])
-    apply (fast intro: dividesI[of "a"] l_one[symmetric] Units_closed[OF aunit])
-    done
-next
-  have "\<one> \<in> Units G" by simp
-  moreover have "\<one> \<sim> \<one>" by simp
-  ultimately show "\<exists>a \<in> Units G. \<one> \<sim> a" by fast
+proof -
+  have "a .\<in>\<^bsub>division_rel G\<^esub> {\<one>}" if "a \<in> Units G" for a
+  proof -
+    have "a \<sim> \<one>"
+      by (rule associatedI) (simp_all add: Units_closed that unit_divides)
+    then show ?thesis
+      by (simp add: elem_def)
+  qed
+  moreover have "\<one> .\<in>\<^bsub>division_rel G\<^esub> Units G"
+    by (simp add: equivalence.mem_imp_elem)
+  ultimately show ?thesis
+    by (auto simp: set_eq_def)
 qed
 
 lemma (in comm_monoid) Units_Lower: "Units G = Lower (division_rel G) (carrier G)"
-  apply (simp add: Units_def Lower_def)
-  apply (rule, rule)
-   apply clarsimp
-   apply (rule unit_divides)
-    apply (unfold Units_def, fast)
-   apply assumption
-  apply clarsimp
+  apply (auto simp add: Units_def Lower_def)
+   apply (metis Units_one_closed unit_divides unit_factor)
   apply (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed)
   done
 
@@ -557,7 +491,7 @@
 lemma (in comm_monoid_cancel) properfactorI3:
   assumes p: "p = a \<otimes> b"
     and nunit: "b \<notin> Units G"
-    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "p \<in> carrier G"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G" 
   shows "properfactor G a p"
   unfolding p
   using carr
@@ -609,7 +543,7 @@
 
 lemma (in monoid) properfactor_trans1 [trans]:
   assumes dvds: "a divides b"  "properfactor G b c"
-    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+    and carr: "a \<in> carrier G"  "c \<in> carrier G"
   shows "properfactor G a c"
   using dvds carr
   apply (elim properfactorE, intro properfactorI)
@@ -618,7 +552,7 @@
 
 lemma (in monoid) properfactor_trans2 [trans]:
   assumes dvds: "properfactor G a b"  "b divides c"
-    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "properfactor G a c"
   using dvds carr
   apply (elim properfactorE, intro properfactorI)
@@ -628,12 +562,7 @@
 lemma properfactor_lless:
   fixes G (structure)
   shows "properfactor G = lless (division_rel G)"
-  apply (rule ext)
-  apply (rule ext)
-  apply rule
-   apply (fastforce elim: properfactorE2 intro: weak_llessI)
-  apply (fastforce elim: weak_llessE intro: properfactorI2)
-  done
+  by (force simp: lless_def properfactor_def associated_def)
 
 lemma (in monoid) properfactor_cong_l [trans]:
   assumes x'x: "x' \<sim> x"
@@ -666,7 +595,7 @@
 
 lemma (in monoid_cancel) properfactor_mult_lI [intro]:
   assumes ab: "properfactor G a b"
-    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+    and carr: "a \<in> carrier G" "c \<in> carrier G"
   shows "properfactor G (c \<otimes> a) (c \<otimes> b)"
   using ab carr by (fastforce elim: properfactorE intro: properfactorI)
 
@@ -677,7 +606,7 @@
 
 lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:
   assumes ab: "properfactor G a b"
-    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+    and carr: "a \<in> carrier G" "c \<in> carrier G"
   shows "properfactor G (a \<otimes> c) (b \<otimes> c)"
   using ab carr by (fastforce elim: properfactorE intro: properfactorI)
 
@@ -727,14 +656,13 @@
 
 lemma (in monoid_cancel) irreducible_cong [trans]:
   assumes irred: "irreducible G a"
-    and aa': "a \<sim> a'"
-    and carr[simp]: "a \<in> carrier G"  "a' \<in> carrier G"
+    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 (metis assms(2) assms(3) assms(4) associated_sym properfactor_cong_r)
+  apply (metis aa' associated_sym properfactor_cong_r)
   done
 
 lemma (in monoid) irreducible_prod_rI:
@@ -743,20 +671,16 @@
     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
   shows "irreducible G (a \<otimes> b)"
   using airr carr bunit
-  apply (elim irreducibleE, intro irreducibleI, clarify)
-   apply (subgoal_tac "a \<in> Units G", simp)
-   apply (intro prod_unit_r[of a b] carr bunit, assumption)
-  apply (metis assms(2,3) associatedI2 m_closed properfactor_cong_r)
-  done
+  apply (elim irreducibleE, intro irreducibleI)
+  using prod_unit_r apply blast
+  using associatedI2' properfactor_cong_r by auto
 
 lemma (in comm_monoid) irreducible_prod_lI:
   assumes birr: "irreducible G b"
     and aunit: "a \<in> Units G"
     and carr [simp]: "a \<in> carrier G"  "b \<in> carrier G"
   shows "irreducible G (a \<otimes> b)"
-  apply (subst m_comm, simp+)
-  apply (intro irreducible_prod_rI assms)
-  done
+  by (metis aunit birr carr irreducible_prod_rI m_comm)
 
 lemma (in comm_monoid_cancel) irreducible_prodE [elim]:
   assumes irr: "irreducible G (a \<otimes> b)"
@@ -834,13 +758,12 @@
 
 lemma (in monoid_cancel) prime_cong [trans]:
   assumes pprime: "prime G p"
-    and pp': "p \<sim> p'"
-    and carr[simp]: "p \<in> carrier G"  "p' \<in> carrier G"
+    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)
-  apply (metis assms(2) assms(3) assms(4) associated_sym divides_cong_l m_closed)
+  apply (metis pp' associated_sym divides_cong_l)
   done
 
 
@@ -883,15 +806,11 @@
     and "set bs \<subseteq> carrier G"
   shows "bs [\<sim>] as"
   using assms
-proof (induct as arbitrary: bs, simp)
+proof (induction as arbitrary: bs)
   case Cons
   then show ?case
-    apply (induct bs)
-     apply simp
-    apply clarsimp
-    apply (iprover intro: associated_sym)
-    done
-qed
+    by (induction bs) (use associated_sym in auto)
+qed auto
 
 lemma (in monoid) listassoc_trans [trans]:
   assumes "as [\<sim>] bs" and "bs [\<sim>] cs"
@@ -899,11 +818,7 @@
   shows "as [\<sim>] cs"
   using assms
   apply (simp add: list_all2_conv_all_nth set_conv_nth, safe)
-  apply (rule associated_trans)
-      apply (subgoal_tac "as ! i \<sim> bs ! i", assumption)
-      apply (simp, simp)
-    apply blast+
-  done
+  by (metis (mono_tags, lifting) associated_trans nth_mem subsetCE)
 
 lemma (in monoid_cancel) irrlist_listassoc_cong:
   assumes "\<forall>a\<in>set as. irreducible G a"
@@ -932,23 +847,41 @@
   assumes a:"as [\<sim>] bs" and p: "bs <~~> cs"
   shows "\<exists>bs'. as <~~> bs' \<and> bs' [\<sim>] cs"
   using p a
-  apply (induct bs cs arbitrary: as, simp)
-    apply (clarsimp simp add: list_all2_Cons2, blast)
-   apply (clarsimp simp add: list_all2_Cons2)
-   apply blast
-  apply blast
-  done
+proof (induction bs cs arbitrary: as)
+  case (swap y x l)
+  then show ?case
+    by (metis (no_types, hide_lams) list_all2_Cons2 perm.swap)
+next
+case (Cons xs ys z)
+  then show ?case
+    by (metis list_all2_Cons2 perm.Cons)
+next
+  case (trans xs ys zs)
+  then show ?case
+    by (meson perm.trans)
+qed auto
 
 lemma (in monoid) perm_assoc_switch_r:
   assumes p: "as <~~> bs" and a:"bs [\<sim>] cs"
   shows "\<exists>bs'. as [\<sim>] bs' \<and> bs' <~~> cs"
   using p a
-  apply (induct as bs arbitrary: cs, simp)
-    apply (clarsimp simp add: list_all2_Cons1, blast)
-   apply (clarsimp simp add: list_all2_Cons1)
-   apply blast
-  apply blast
-  done
+proof (induction as bs arbitrary: cs)
+  case Nil
+  then show ?case
+    by auto
+next
+  case (swap y x l)
+  then show ?case
+    by (metis (no_types, hide_lams) list_all2_Cons1 perm.swap)
+next
+  case (Cons xs ys z)
+  then show ?case
+    by (metis list_all2_Cons1 perm.Cons)
+next
+  case (trans xs ys zs)
+  then show ?case
+    by (blast intro:  elim: )
+qed
 
 declare perm_sym [sym]
 
@@ -1015,15 +948,13 @@
   assume "abs [\<sim>] bs" and pb: "bs <~~> bcs"
   from perm_assoc_switch [OF this] obtain bs' where p: "abs <~~> bs'" and a: "bs' [\<sim>] bcs"
     by blast
-
   assume "as <~~> abs"
   with p have pp: "as <~~> bs'" by fast
-
   from pp ascarr have c1: "set bs' \<subseteq> carrier G" by (rule perm_closed)
   from pb bscarr have c2: "set bcs \<subseteq> carrier G" by (rule perm_closed)
-  note a
-  also assume "bcs [\<sim>] cs"
-  finally (listassoc_trans) have "bs' [\<sim>] cs" by (simp add: c1 c2 cscarr)
+  assume "bcs [\<sim>] cs"
+  then have "bs' [\<sim>] cs"
+    using a c1 c2 cscarr listassoc_trans by blast
   with pp show ?thesis
     by (rule essentially_equalI)
 qed
@@ -1038,46 +969,46 @@
   shows "foldr (\<otimes>) fs \<one> \<in> carrier G"
   using ascarr by (induct fs) simp_all
 
-lemma  (in comm_monoid) multlist_dividesI (*[intro]*):
-  assumes "f \<in> set fs" and "f \<in> carrier G" and "set fs \<subseteq> carrier G"
+lemma  (in comm_monoid) multlist_dividesI:
+  assumes "f \<in> set fs" and "set fs \<subseteq> carrier G"
   shows "f divides (foldr (\<otimes>) fs \<one>)"
   using assms
-  apply (induct fs)
-   apply simp
-  apply (case_tac "f = a")
-   apply simp
-   apply (fast intro: dividesI)
-  apply clarsimp
-  apply (metis assms(2) divides_prod_l multlist_closed)
-  done
+proof (induction fs)
+  case (Cons a fs)
+  then have f: "f \<in> carrier G"
+    by blast
+  show ?case
+  proof (cases "f = a")
+    case True
+    then show ?thesis
+      using Cons.prems by auto
+  next
+    case False
+    with Cons show ?thesis
+      by clarsimp (metis f divides_prod_l multlist_closed)
+  qed
+qed auto
 
 lemma (in comm_monoid_cancel) multlist_listassoc_cong:
   assumes "fs [\<sim>] fs'"
     and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
   shows "foldr (\<otimes>) fs \<one> \<sim> foldr (\<otimes>) fs' \<one>"
   using assms
-proof (induct fs arbitrary: fs', simp)
+proof (induct fs arbitrary: fs')
   case (Cons a as fs')
   then show ?case
-    apply (induct fs', simp)
-  proof clarsimp
-    fix b bs
-    assume "a \<sim> b"
-      and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
-      and ascarr: "set as \<subseteq> carrier G"
+  proof (induction fs')
+    case (Cons b bs)
     then have p: "a \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) as \<one>"
-      by (fast intro: mult_cong_l)
-    also
-    assume "as [\<sim>] bs"
-      and bscarr: "set bs \<subseteq> carrier G"
-      and "\<And>fs'. \<lbrakk>as [\<sim>] fs'; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) fs' \<one>"
-    then have "foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) bs \<one>" by simp
-    with ascarr bscarr bcarr have "b \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) bs \<one>"
-      by (fast intro: mult_cong_r)
-    finally show "a \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) bs \<one>"
-      by (simp add: ascarr bscarr acarr bcarr)
-  qed
-qed
+      by (simp add: mult_cong_l)
+    then have "foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) bs \<one>"
+      using Cons by auto
+    with Cons have "b \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) bs \<one>"
+      by (simp add: mult_cong_r)
+    then show ?case
+      using Cons.prems(3) Cons.prems(4) monoid.associated_trans monoid_axioms p by force
+  qed auto
+qed auto
 
 lemma (in comm_monoid) multlist_perm_cong:
   assumes prm: "as <~~> bs"
@@ -1197,14 +1128,14 @@
     and asc: "fs [\<sim>] fs'"
     and carr: "a \<in> carrier G"  "set fs \<subseteq> carrier G"  "set fs' \<subseteq> carrier G"
   shows "wfactors G fs' a"
+proof -
+  { from asc[symmetric] have "foldr (\<otimes>) fs' \<one> \<sim> foldr (\<otimes>) fs \<one>"
+      by (simp add: multlist_listassoc_cong carr)
+    also assume "foldr (\<otimes>) fs \<one> \<sim> a"
+    finally have "foldr (\<otimes>) fs' \<one> \<sim> a" by (simp add: carr) }
+  then show ?thesis
   using fact
-  apply (elim wfactorsE, intro wfactorsI)
-   apply (metis assms(2) assms(4) assms(5) irrlist_listassoc_cong)
-proof -
-  from asc[symmetric] have "foldr (\<otimes>) fs' \<one> \<sim> foldr (\<otimes>) fs \<one>"
-    by (simp add: multlist_listassoc_cong carr)
-  also assume "foldr (\<otimes>) fs \<one> \<sim> a"
-  finally show "foldr (\<otimes>) fs' \<one> \<sim> a" by (simp add: carr)
+  by (meson asc carr(2) carr(3) irrlist_listassoc_cong wfactors_def)
 qed
 
 lemma (in comm_monoid) wfactors_perm_cong_l:
@@ -1212,11 +1143,7 @@
     and "fs <~~> fs'"
     and "set fs \<subseteq> carrier G"
   shows "wfactors G fs' a"
-  using assms
-  apply (elim wfactorsE, intro wfactorsI)
-   apply (rule irrlist_perm_cong, assumption+)
-  apply (simp add: multlist_perm_cong[symmetric])
-  done
+  using assms irrlist_perm_cong multlist_perm_cong wfactors_def by fastforce
 
 lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]:
   assumes ee: "essentially_equal G as bs"
@@ -1255,28 +1182,40 @@
     and carr: "set as \<subseteq> carrier G"
   shows "essentially_equal G (as[0 := (as!0 \<otimes> u)]) as"
     (is "essentially_equal G ?as' as")
-  using assms
-  apply (intro essentially_equalI[of _ ?as'], simp)
-  apply (cases as, simp)
-  apply (clarsimp, fast intro: associatedI2[of u])
-  done
+proof -
+  have "as[0 := as ! 0 \<otimes> u] [\<sim>] as"
+  proof (cases as)
+    case (Cons a as')
+    then show ?thesis
+      using associatedI2 carr uunit by auto
+  qed auto
+  then show ?thesis
+    using essentially_equal_def by blast
+qed
 
 lemma (in comm_monoid_cancel) factors_cong_unit:
-  assumes uunit: "u \<in> Units G"
-    and anunit: "a \<notin> Units G"
+  assumes u: "u \<in> Units G"
+    and a: "a \<notin> Units G"
     and afs: "factors G as a"
     and ascarr: "set as \<subseteq> carrier G"
   shows "factors G (as[0 := (as!0 \<otimes> u)]) (a \<otimes> u)"
     (is "factors G ?as' ?a'")
-  using assms
-  apply (elim factorsE, clarify)
-  apply (cases as)
-   apply (simp add: nunit_factors)
-  apply clarsimp
-  apply (elim factorsE, intro factorsI)
-   apply (clarsimp, fast intro: irreducible_prod_rI)
-  apply (simp add: m_ac Units_closed)
-  done
+proof (cases as)
+  case Nil
+  then show ?thesis
+    using afs a nunit_factors by auto
+next
+  case (Cons b bs)
+  have *: "\<forall>f\<in>set as. irreducible G f" "foldr (\<otimes>) as \<one> = a"
+    using afs  by (auto simp: factors_def)
+  show ?thesis
+  proof (intro factorsI)
+    show "foldr (\<otimes>) (as[0 := as ! 0 \<otimes> u]) \<one> = a \<otimes> u"
+      using Cons u ascarr * by (auto simp add: m_ac Units_closed)
+    show "\<forall>f\<in>set (as[0 := as ! 0 \<otimes> u]). irreducible G f"
+      using Cons u ascarr * by (force intro: irreducible_prod_rI)
+  qed 
+qed
 
 lemma (in comm_monoid) perm_wfactorsD:
   assumes prm: "as <~~> bs"
@@ -1289,7 +1228,8 @@
 proof (elim wfactorsE)
   from prm have [simp]: "set bs \<subseteq> carrier G" by (simp add: perm_closed)
   assume "foldr (\<otimes>) as \<one> \<sim> a"
-  then have "a \<sim> foldr (\<otimes>) as \<one>" by (rule associated_sym, simp+)
+  then have "a \<sim> foldr (\<otimes>) as \<one>"
+    by (simp add: associated_sym)
   also from prm
   have "foldr (\<otimes>) as \<one> = foldr (\<otimes>) bs \<one>" by (rule multlist_perm_cong, simp)
   also assume "foldr (\<otimes>) bs \<one> \<sim> b"
@@ -1306,7 +1246,7 @@
   using afs bfs
 proof (elim wfactorsE)
   assume "foldr (\<otimes>) as \<one> \<sim> a"
-  then have "a \<sim> foldr (\<otimes>) as \<one>" by (rule associated_sym, simp+)
+  then have "a \<sim> foldr (\<otimes>) as \<one>" by (simp add: associated_sym)
   also from assoc
   have "foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) bs \<one>" by (rule multlist_listassoc_cong, simp+)
   also assume "foldr (\<otimes>) bs \<one> \<sim> b"