# HG changeset patch
# User wenzelm
# Date 1473545605 -7200
# Node ID a400b127853cbb6771e727ef5189b65896944d7a
# Parent  ea7471c921f58c93af5ba5be45ba6f4892dd7f45
misc tuning and modernization;

diff -r ea7471c921f5 -r a400b127853c src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sat Sep 10 14:11:04 2016 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Sun Sep 11 00:13:25 2016 +0200
@@ -6,7 +6,7 @@
 section \<open>Divisibility in monoids and rings\<close>
 
 theory Divisibility
-imports "~~/src/HOL/Library/Permutation" Coset Group
+  imports "~~/src/HOL/Library/Permutation" Coset Group
 begin
 
 section \<open>Factorial Monoids\<close>
@@ -14,22 +14,16 @@
 subsection \<open>Monoids with Cancellation Law\<close>
 
 locale monoid_cancel = monoid +
-  assumes l_cancel: 
-          "\<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
-      and r_cancel: 
-          "\<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
+  assumes l_cancel: "\<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
+    and r_cancel: "\<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
 
 lemma (in monoid) monoid_cancelI:
-  assumes l_cancel: 
-          "\<And>a b c. \<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
-      and r_cancel: 
-          "\<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"
+  assumes l_cancel: "\<And>a b c. \<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
+    and r_cancel: "\<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"
   shows "monoid_cancel G"
     by standard fact+
 
-lemma (in monoid_cancel) is_monoid_cancel:
-  "monoid_cancel G"
-  ..
+lemma (in monoid_cancel) is_monoid_cancel: "monoid_cancel G" ..
 
 sublocale group \<subseteq> monoid_cancel
   by standard simp_all
@@ -40,8 +34,7 @@
 lemma comm_monoid_cancelI:
   fixes G (structure)
   assumes "comm_monoid G"
-  assumes cancel: 
-          "\<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"
+  assumes cancel: "\<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"
   shows "comm_monoid_cancel G"
 proof -
   interpret comm_monoid G by fact
@@ -49,50 +42,51 @@
     by unfold_locales (metis assms(2) m_ac(2))+
 qed
 
-lemma (in comm_monoid_cancel) is_comm_monoid_cancel:
-  "comm_monoid_cancel G"
+lemma (in comm_monoid_cancel) is_comm_monoid_cancel: "comm_monoid_cancel G"
   by intro_locales
 
-sublocale comm_group \<subseteq> comm_monoid_cancel
-  ..
+sublocale comm_group \<subseteq> comm_monoid_cancel ..
 
 
 subsection \<open>Products of Units in Monoids\<close>
 
 lemma (in monoid) Units_m_closed[simp, intro]:
-  assumes h1unit: "h1 \<in> Units G" and h2unit: "h2 \<in> Units G"
+  assumes h1unit: "h1 \<in> Units G"
+    and h2unit: "h2 \<in> Units G"
   shows "h1 \<otimes> h2 \<in> Units G"
-unfolding Units_def
-using assms
-by auto (metis Units_inv_closed Units_l_inv Units_m_closed Units_r_inv)
+  unfolding Units_def
+  using assms
+  by auto (metis Units_inv_closed Units_l_inv Units_m_closed Units_r_inv)
 
 lemma (in monoid) prod_unit_l:
-  assumes abunit[simp]: "a \<otimes> b \<in> Units G" and aunit[simp]: "a \<in> Units G"
+  assumes abunit[simp]: "a \<otimes> b \<in> Units G"
+    and aunit[simp]: "a \<in> Units G"
     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
   shows "b \<in> Units G"
 proof -
   have c: "inv (a \<otimes> b) \<otimes> a \<in> carrier G" by simp
 
-  have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)" by (simp add: m_assoc)
+  have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)"
+    by (simp add: m_assoc)
   also have "\<dots> = \<one>" by simp
   finally have li: "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = \<one>" .
 
   have "\<one> = inv a \<otimes> a" by (simp add: Units_l_inv[symmetric])
   also have "\<dots> = inv a \<otimes> \<one> \<otimes> a" by simp
   also have "\<dots> = inv a \<otimes> ((a \<otimes> b) \<otimes> inv (a \<otimes> b)) \<otimes> a"
-       by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv)
+    by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv)
   also have "\<dots> = ((inv a \<otimes> a) \<otimes> b) \<otimes> inv (a \<otimes> b) \<otimes> a"
     by (simp add: m_assoc del: Units_l_inv)
   also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp
   also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> a)" by (simp add: m_assoc)
   finally have ri: "b \<otimes> (inv (a \<otimes> b) \<otimes> a) = \<one> " by simp
 
-  from c li ri
-      show "b \<in> Units G" by (simp add: Units_def, fast)
+  from c li ri show "b \<in> Units G" by (auto simp: Units_def)
 qed
 
 lemma (in monoid) prod_unit_r:
-  assumes abunit[simp]: "a \<otimes> b \<in> Units G" and bunit[simp]: "b \<in> Units G"
+  assumes abunit[simp]: "a \<otimes> b \<in> Units G"
+    and bunit[simp]: "b \<in> Units G"
     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
   shows "a \<in> Units G"
 proof -
@@ -105,42 +99,39 @@
 
   have "\<one> = b \<otimes> inv b" by (simp add: Units_r_inv[symmetric])
   also have "\<dots> = b \<otimes> \<one> \<otimes> inv b" by simp
-  also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> (a \<otimes> b)) \<otimes> inv b" 
-       by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv)
+  also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> (a \<otimes> b)) \<otimes> inv b"
+    by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv)
   also have "\<dots> = (b \<otimes> inv (a \<otimes> b) \<otimes> a) \<otimes> (b \<otimes> inv b)"
     by (simp add: m_assoc del: Units_l_inv)
   also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp
   finally have ri: "(b \<otimes> inv (a \<otimes> b)) \<otimes> a = \<one> " by simp
 
-  from c li ri
-      show "a \<in> Units G" by (simp add: Units_def, fast)
+  from c li ri show "a \<in> Units G" by (auto simp: Units_def)
 qed
 
 lemma (in comm_monoid) unit_factor:
   assumes abunit: "a \<otimes> b \<in> Units G"
     and [simp]: "a \<in> carrier G"  "b \<in> carrier G"
   shows "a \<in> Units G"
-using abunit[simplified Units_def]
+  using abunit[simplified Units_def]
 proof clarsimp
   fix i
   assume [simp]: "i \<in> carrier G"
-    and li: "i \<otimes> (a \<otimes> b) = \<one>"
-    and ri: "a \<otimes> b \<otimes> i = \<one>"
 
   have carr': "b \<otimes> i \<in> carrier G" by simp
 
   have "(b \<otimes> i) \<otimes> a = (i \<otimes> b) \<otimes> a" by (simp add: m_comm)
   also have "\<dots> = i \<otimes> (b \<otimes> a)" by (simp add: m_assoc)
   also have "\<dots> = i \<otimes> (a \<otimes> b)" by (simp add: m_comm)
-  also note li
+  also assume "i \<otimes> (a \<otimes> b) = \<one>"
   finally have li': "(b \<otimes> i) \<otimes> a = \<one>" .
 
   have "a \<otimes> (b \<otimes> i) = a \<otimes> b \<otimes> i" by (simp add: m_assoc)
-  also note ri
+  also assume "a \<otimes> b \<otimes> i = \<one>"
   finally have ri': "a \<otimes> (b \<otimes> i) = \<one>" .
 
   from carr' li' ri'
-      show "a \<in> Units G" by (simp add: Units_def, fast)
+  show "a \<in> Units G" by (simp add: Units_def, fast)
 qed
 
 
@@ -148,29 +139,23 @@
 
 subsubsection \<open>Function definitions\<close>
 
-definition
-  factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)
+definition factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)
   where "a divides\<^bsub>G\<^esub> b \<longleftrightarrow> (\<exists>c\<in>carrier G. b = a \<otimes>\<^bsub>G\<^esub> c)"
 
-definition
-  associated :: "[_, 'a, 'a] => bool" (infix "\<sim>\<index>" 55)
+definition associated :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "\<sim>\<index>" 55)
   where "a \<sim>\<^bsub>G\<^esub> b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"
 
-abbreviation
-  "division_rel G == \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>"
-
-definition
-  properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"
+abbreviation "division_rel G \<equiv> \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>"
+
+definition properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"
   where "properfactor G a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"
 
-definition
-  irreducible :: "[_, 'a] \<Rightarrow> bool"
+definition irreducible :: "[_, 'a] \<Rightarrow> bool"
   where "irreducible G a \<longleftrightarrow> a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
 
-definition
-  prime :: "[_, 'a] \<Rightarrow> bool" where
-  "prime G p \<longleftrightarrow>
-    p \<notin> Units G \<and> 
+definition prime :: "[_, 'a] \<Rightarrow> bool"
+  where "prime G p \<longleftrightarrow>
+    p \<notin> Units G \<and>
     (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides\<^bsub>G\<^esub> (a \<otimes>\<^bsub>G\<^esub> b) \<longrightarrow> p divides\<^bsub>G\<^esub> a \<or> p divides\<^bsub>G\<^esub> b)"
 
 
@@ -181,24 +166,20 @@
   assumes carr: "c \<in> carrier G"
     and p: "b = a \<otimes> c"
   shows "a divides b"
-unfolding factor_def
-using assms by fast
+  unfolding factor_def using assms by fast
 
 lemma dividesI' [intro]:
-   fixes G (structure)
+  fixes G (structure)
   assumes p: "b = a \<otimes> c"
     and carr: "c \<in> carrier G"
   shows "a divides b"
-using assms
-by (fast intro: dividesI)
+  using assms by (fast intro: dividesI)
 
 lemma dividesD:
   fixes G (structure)
   assumes "a divides b"
   shows "\<exists>c\<in>carrier G. b = a \<otimes> c"
-using assms
-unfolding factor_def
-by fast
+  using assms unfolding factor_def by fast
 
 lemma dividesE [elim]:
   fixes G (structure)
@@ -207,106 +188,93 @@
   shows "P"
 proof -
   from dividesD[OF d]
-      obtain c
-      where "c\<in>carrier G"
-      and "b = a \<otimes> c"
-      by auto
-  thus "P" by (elim elim)
+  obtain c where "c \<in> carrier G" and "b = a \<otimes> c" by auto
+  then show P by (elim elim)
 qed
 
 lemma (in monoid) divides_refl[simp, intro!]:
   assumes carr: "a \<in> carrier G"
   shows "a divides a"
-apply (intro dividesI[of "\<one>"])
-apply (simp, simp add: carr)
-done
+  by (intro dividesI[of "\<one>"]) (simp_all add: carr)
 
 lemma (in monoid) divides_trans [trans]:
   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)
+  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"
   shows "(c \<otimes> a) divides (c \<otimes> b)"
-using ab
-apply (elim dividesE, simp add: m_assoc[symmetric] carr)
-apply (fast intro: dividesI)
-done
+  using ab
+  apply (elim dividesE)
+  apply (simp add: m_assoc[symmetric] carr)
+  apply (fast intro: dividesI)
+  done
 
 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
+  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
 
 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
+  apply (simp add: m_comm[of a c] m_comm[of b c])
+  apply (rule divides_mult_lI, assumption+)
+  done
 
 lemma (in comm_monoid_cancel) divides_mult_r [simp]:
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "(a \<otimes> c) divides (b \<otimes> c) = a divides b"
-using carr
-by (simp add: m_comm[of a c] m_comm[of b c])
+  using carr by (simp add: m_comm[of a c] m_comm[of b c])
 
 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"
   shows "a divides (b \<otimes> c)"
-using ab carr
-by (fast intro: m_assoc)
+  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"
   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 ab carr
+  apply (simp add: m_comm[of c b])
+  apply (fast intro: divides_prod_r)
+  done
 
 lemma (in monoid) unit_divides:
   assumes uunit: "u \<in> Units G"
-      and acarr: "a \<in> carrier G"
+    and acarr: "a \<in> carrier G"
   shows "u divides a"
 proof (intro dividesI[of "(inv u) \<otimes> a"], fast intro: uunit acarr)
-  from uunit acarr
-      have xcarr: "inv u \<otimes> a \<in> carrier G" by fast
-
-  from uunit acarr
-       have "u \<otimes> (inv u \<otimes> a) = (u \<otimes> inv u) \<otimes> a" by (fast intro: m_assoc[symmetric])
+  from uunit acarr have xcarr: "inv u \<otimes> a \<in> carrier G" by fast
+  from uunit acarr have "u \<otimes> (inv u \<otimes> a) = (u \<otimes> inv u) \<otimes> a"
+    by (fast intro: m_assoc[symmetric])
   also have "\<dots> = \<one> \<otimes> a" by (simp add: Units_r_inv[OF uunit])
-  also from acarr 
-       have "\<dots> = a" by simp
-  finally
-       show "a = u \<otimes> (inv u \<otimes> a)" ..
+  also from acarr have "\<dots> = a" by simp
+  finally show "a = u \<otimes> (inv u \<otimes> a)" ..
 qed
 
 lemma (in comm_monoid) divides_unit:
   assumes udvd: "a divides u"
-      and  carr: "a \<in> carrier G"  "u \<in> Units G"
+    and  carr: "a \<in> carrier G"  "u \<in> Units G"
   shows "a \<in> Units G"
-using udvd carr
-by (blast intro: unit_factor)
+  using udvd carr by (blast intro: unit_factor)
 
 lemma (in comm_monoid) Unit_eq_dividesone:
   assumes ucarr: "u \<in> carrier G"
   shows "u \<in> Units G = u divides \<one>"
-using ucarr
-by (fast dest: divides_unit intro: unit_divides)
+  using ucarr by (fast dest: divides_unit intro: unit_divides)
 
 
 subsubsection \<open>Association\<close>
@@ -315,83 +283,71 @@
   fixes G (structure)
   assumes "a divides b"  "b divides a"
   shows "a \<sim> b"
-using assms
-by (simp add: associated_def)
+  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"
   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
+  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
 
 lemma (in monoid) associatedI2':
-  assumes a: "a = b \<otimes> u"
-    and uunit: "u \<in> Units G"
-    and bcarr: "b \<in> carrier G"
+  assumes "a = b \<otimes> u"
+    and "u \<in> Units G"
+    and "b \<in> carrier G"
   shows "a \<sim> b"
-using assms by (intro associatedI2)
+  using assms by (intro associatedI2)
 
 lemma associatedD:
   fixes G (structure)
   assumes "a \<sim> b"
   shows "a divides b"
-using assms by (simp add: associated_def)
+  using assms by (simp add: associated_def)
 
 lemma (in monoid_cancel) associatedD2:
   assumes assoc: "a \<sim> b"
     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
+  using assoc
+  unfolding associated_def
 proof clarify
   assume "b divides a"
-  hence "\<exists>u\<in>carrier G. a = b \<otimes> u" by (rule dividesD)
-  from this obtain u
-      where ucarr: "u \<in> carrier G" and a: "a = b \<otimes> u"
-      by auto
+  then have "\<exists>u\<in>carrier G. a = b \<otimes> u" by (rule dividesD)
+  then obtain u where ucarr: "u \<in> carrier G" and a: "a = b \<otimes> u"
+    by auto
 
   assume "a divides b"
-  hence "\<exists>u'\<in>carrier G. b = a \<otimes> u'" by (rule dividesD)
-  from this obtain u'
-      where u'carr: "u' \<in> carrier G" and b: "b = a \<otimes> u'"
-      by auto
+  then have "\<exists>u'\<in>carrier G. b = a \<otimes> u'" by (rule dividesD)
+  then obtain u' where u'carr: "u' \<in> carrier G" and b: "b = a \<otimes> u'"
+    by auto
   note carr = carr ucarr u'carr
 
-  from carr
-       have "a \<otimes> \<one> = a" by simp
+  from carr have "a \<otimes> \<one> = a" by simp
   also have "\<dots> = b \<otimes> u" by (simp add: a)
   also have "\<dots> = a \<otimes> u' \<otimes> u" by (simp add: b)
-  also from carr
-       have "\<dots> = a \<otimes> (u' \<otimes> u)" by (simp add: m_assoc)
-  finally
-       have "a \<otimes> \<one> = a \<otimes> (u' \<otimes> u)" .
-  with carr
-      have u1: "\<one> = u' \<otimes> u" by (fast dest: l_cancel)
-
-  from carr
-       have "b \<otimes> \<one> = b" by simp
+  also from carr have "\<dots> = a \<otimes> (u' \<otimes> u)" by (simp add: m_assoc)
+  finally have "a \<otimes> \<one> = a \<otimes> (u' \<otimes> u)" .
+  with carr have u1: "\<one> = u' \<otimes> u" by (fast dest: l_cancel)
+
+  from carr have "b \<otimes> \<one> = b" by simp
   also have "\<dots> = a \<otimes> u'" by (simp add: b)
   also have "\<dots> = b \<otimes> u \<otimes> u'" by (simp add: a)
-  also from carr
-       have "\<dots> = b \<otimes> (u \<otimes> u')" by (simp add: m_assoc)
-  finally
-       have "b \<otimes> \<one> = b \<otimes> (u \<otimes> u')" .
-  with carr
-      have u2: "\<one> = u \<otimes> u'" by (fast dest: l_cancel)
-
-  from u'carr u1[symmetric] u2[symmetric]
-      have "\<exists>u'\<in>carrier G. u' \<otimes> u = \<one> \<and> u \<otimes> u' = \<one>" by fast
-  hence "u \<in> Units G" by (simp add: Units_def ucarr)
-
-  from ucarr this a
-      show "\<exists>u\<in>Units G. a = b \<otimes> u" by fast
+  also from carr have "\<dots> = b \<otimes> (u \<otimes> u')" by (simp add: m_assoc)
+  finally have "b \<otimes> \<one> = b \<otimes> (u \<otimes> u')" .
+  with carr have u2: "\<one> = u \<otimes> u'" by (fast dest: l_cancel)
+
+  from u'carr u1[symmetric] u2[symmetric] have "\<exists>u'\<in>carrier G. u' \<otimes> u = \<one> \<and> u \<otimes> u' = \<one>"
+    by fast
+  then have "u \<in> Units G"
+    by (simp add: Units_def ucarr)
+  with ucarr a show "\<exists>u\<in>Units G. a = b \<otimes> u" by fast
 qed
 
 lemma associatedE:
@@ -400,10 +356,9 @@
     and e: "\<lbrakk>a divides b; b divides a\<rbrakk> \<Longrightarrow> P"
   shows "P"
 proof -
-  from assoc
-      have "a divides b"  "b divides a"
-      by (simp add: associated_def)+
-  thus "P" by (elim e)
+  from assoc have "a divides b" "b divides a"
+    by (simp_all add: associated_def)
+  then show P by (elim e)
 qed
 
 lemma (in monoid_cancel) associatedE2:
@@ -412,39 +367,34 @@
     and carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "P"
 proof -
-  from assoc and carr
-      have "\<exists>u\<in>Units G. a = b \<otimes> u" by (rule associatedD2)
-  from this obtain u
-      where "u \<in> Units G"  "a = b \<otimes> u"
-      by auto
-  thus "P" by (elim e)
+  from assoc and carr have "\<exists>u\<in>Units G. a = b \<otimes> u"
+    by (rule associatedD2)
+  then obtain u where "u \<in> Units G"  "a = b \<otimes> u"
+    by auto
+  then show P by (elim e)
 qed
 
 lemma (in monoid) associated_refl [simp, intro!]:
   assumes "a \<in> carrier G"
   shows "a \<sim> a"
-using assms
-by (fast intro: associatedI)
+  using assms by (fast intro: associatedI)
 
 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)
+  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"
   shows "a \<sim> c"
-using assms
-by (iprover intro: associatedI divides_trans elim: associatedE)
-
-lemma (in monoid) division_equiv [intro, simp]:
-  "equivalence (division_rel G)"
+  using assms by (iprover intro: associatedI divides_trans elim: associatedE)
+
+lemma (in monoid) division_equiv [intro, simp]: "equivalence (division_rel G)"
   apply unfold_locales
-  apply simp_all
-  apply (metis associated_def)
+    apply simp_all
+   apply (metis associated_def)
   apply (iprover intro: associated_trans)
   done
 
@@ -456,152 +406,143 @@
   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)
+  using assms by (fast intro: associatedI)
 
 lemma (in monoid) divides_cong_l [trans]:
-  assumes xx': "x \<sim> x'"
-    and xdvdy: "x' divides y"
-    and carr [simp]: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
+  assumes "x \<sim> x'"
+    and "x' divides y"
+    and [simp]: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   shows "x divides y"
 proof -
-  from xx'
-       have "x divides x'" by (simp add: associatedD)
-  also note xdvdy
-  finally
-       show "x divides y" by simp
+  from assms(1) have "x divides x'" by (simp add: associatedD)
+  also note assms(2)
+  finally show "x divides y" by simp
 qed
 
 lemma (in monoid) divides_cong_r [trans]:
-  assumes xdvdy: "x divides y"
-    and yy': "y \<sim> y'"
-    and carr[simp]: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
+  assumes "x divides y"
+    and "y \<sim> y'"
+    and [simp]: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
   shows "x divides y'"
 proof -
-  note xdvdy
-  also from yy'
-       have "y divides y'" by (simp add: associatedD)
-  finally
-       show "x divides y'" by simp
+  note assms(1)
+  also from assms(2) have "y divides y'" by (simp add: associatedD)
+  finally show "x divides y'" by simp
 qed
 
 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 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
 
-    
+
 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"
   shows "a \<otimes> b \<sim> a \<otimes> b'"
-using assms
-apply (elim associatedE2, intro associatedI2)
-apply (auto intro: m_assoc[symmetric])
-done
+  using assms
+  apply (elim associatedE2, intro associatedI2)
+      apply (auto intro: m_assoc[symmetric])
+  done
 
 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"
   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+
-done
+  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
 
 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'"
   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
+  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
 
 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"
   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
+  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
 
 
 subsubsection \<open>Units\<close>
 
 lemma (in monoid_cancel) assoc_unit_l [trans]:
-  assumes asc: "a \<sim> b" and bunit: "b \<in> Units G"
-    and carr: "a \<in> carrier G" 
+  assumes "a \<sim> b"
+    and "b \<in> Units G"
+    and "a \<in> carrier G"
   shows "a \<in> Units G"
-using assms
-by (fast elim: associatedE2)
+  using assms by (fast elim: associatedE2)
 
 lemma (in monoid_cancel) assoc_unit_r [trans]:
-  assumes aunit: "a \<in> Units G" and asc: "a \<sim> b"
+  assumes aunit: "a \<in> Units G"
+    and asc: "a \<sim> b"
     and bcarr: "b \<in> carrier G"
   shows "b \<in> Units G"
-using aunit bcarr associated_sym[OF asc]
-by (blast intro: assoc_unit_l)
+  using aunit bcarr associated_sym[OF asc] by (blast intro: assoc_unit_l)
 
 lemma (in comm_monoid) Units_cong:
   assumes aunit: "a \<in> Units G" and asc: "a \<sim> b"
     and bcarr: "b \<in> carrier G"
   shows "b \<in> Units G"
-using assms
-by (blast intro: divides_unit elim: associatedE)
+  using assms by (blast intro: divides_unit elim: associatedE)
 
 lemma (in monoid) Units_assoc:
   assumes units: "a \<in> Units G"  "b \<in> Units G"
   shows "a \<sim> b"
-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)
+  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
+    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
 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 (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed)
-done
+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 (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed)
+  done
 
 
 subsubsection \<open>Proper factors\<close>
@@ -611,16 +552,14 @@
   assumes "a divides b"
     and "\<not>(b divides a)"
   shows "properfactor G a b"
-using assms
-unfolding properfactor_def
-by simp
+  using assms unfolding properfactor_def by simp
 
 lemma properfactorI2:
   fixes G (structure)
   assumes advdb: "a divides b"
     and neq: "\<not>(a \<sim> b)"
   shows "properfactor G a b"
-apply (rule properfactorI, rule advdb)
+  apply (rule properfactorI, rule advdb)
 proof (rule ccontr, simp)
   assume "b divides a"
   with advdb have "a \<sim> b" by (rule associatedI)
@@ -632,9 +571,9 @@
     and nunit: "b \<notin> Units G"
     and carr: "a \<in> carrier G"  "b \<in> carrier G"  "p \<in> carrier G"
   shows "properfactor G a p"
-unfolding p
-using carr
-apply (intro properfactorI, fast)
+  unfolding p
+  using carr
+  apply (intro properfactorI, fast)
 proof (clarsimp, elim dividesE)
   fix c
   assume ccarr: "c \<in> carrier G"
@@ -645,14 +584,13 @@
   also have "\<dots> = a \<otimes> (b \<otimes> c)" by (simp add: m_assoc)
   finally have "a \<otimes> \<one> = a \<otimes> (b \<otimes> c)" .
 
-  hence rinv: "\<one> = b \<otimes> c" by (intro l_cancel[of "a" "\<one>" "b \<otimes> c"], simp+)
+  then have rinv: "\<one> = b \<otimes> c" by (intro l_cancel[of "a" "\<one>" "b \<otimes> c"], simp+)
   also have "\<dots> = c \<otimes> b" by (simp add: m_comm)
   finally have linv: "\<one> = c \<otimes> b" .
 
-  from ccarr linv[symmetric] rinv[symmetric]
-  have "b \<in> Units G" unfolding Units_def by fastforce
-  with nunit
-      show "False" ..
+  from ccarr linv[symmetric] rinv[symmetric] have "b \<in> Units G"
+    unfolding Units_def by fastforce
+  with nunit show False ..
 qed
 
 lemma properfactorE:
@@ -660,74 +598,67 @@
   assumes pf: "properfactor G a b"
     and r: "\<lbrakk>a divides b; \<not>(b divides a)\<rbrakk> \<Longrightarrow> P"
   shows "P"
-using pf
-unfolding properfactor_def
-by (fast intro: r)
+  using pf unfolding properfactor_def by (fast intro: r)
 
 lemma properfactorE2:
   fixes G (structure)
   assumes pf: "properfactor G a b"
     and elim: "\<lbrakk>a divides b; \<not>(a \<sim> b)\<rbrakk> \<Longrightarrow> P"
   shows "P"
-using pf
-unfolding properfactor_def
-by (fast elim: elim associatedE)
+  using pf unfolding properfactor_def by (fast elim: elim associatedE)
 
 lemma (in monoid) properfactor_unitE:
   assumes uunit: "u \<in> Units G"
     and pf: "properfactor G a u"
     and acarr: "a \<in> carrier G"
   shows "P"
-using pf unit_divides[OF uunit acarr]
-by (fast elim: properfactorE)
-
+  using pf unit_divides[OF uunit acarr] by (fast elim: properfactorE)
 
 lemma (in monoid) properfactor_divides:
   assumes pf: "properfactor G a b"
   shows "a divides b"
-using pf
-by (elim properfactorE)
+  using pf by (elim properfactorE)
 
 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"
   shows "properfactor G a c"
-using dvds carr
-apply (elim properfactorE, intro properfactorI)
- apply (iprover intro: divides_trans)+
-done
+  using dvds carr
+  apply (elim properfactorE, intro properfactorI)
+   apply (iprover intro: divides_trans)+
+  done
 
 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"
   shows "properfactor G a c"
-using dvds carr
-apply (elim properfactorE, intro properfactorI)
- apply (iprover intro: divides_trans)+
-done
+  using dvds carr
+  apply (elim properfactorE, intro properfactorI)
+   apply (iprover intro: divides_trans)+
+  done
 
 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
+  apply (rule ext)
+  apply (rule ext)
+  apply rule
+   apply (fastforce elim: properfactorE2 intro: weak_llessI)
+  apply (fastforce elim: weak_llessE intro: properfactorI2)
+  done
 
 lemma (in monoid) properfactor_cong_l [trans]:
   assumes x'x: "x' \<sim> x"
     and pf: "properfactor G x y"
     and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   shows "properfactor G x' y"
-using pf
-unfolding properfactor_lless
+  using pf
+  unfolding properfactor_lless
 proof -
   interpret weak_partial_order "division_rel G" ..
-  from x'x
-       have "x' .=\<^bsub>division_rel G\<^esub> x" by simp
+  from x'x have "x' .=\<^bsub>division_rel G\<^esub> x" by simp
   also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
-  finally
-       show "x' \<sqsubset>\<^bsub>division_rel G\<^esub> y" by (simp add: carr)
+  finally show "x' \<sqsubset>\<^bsub>division_rel G\<^esub> y" by (simp add: carr)
 qed
 
 lemma (in monoid) properfactor_cong_r [trans]:
@@ -735,54 +666,49 @@
     and yy': "y \<sim> y'"
     and carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
   shows "properfactor G x y'"
-using pf
-unfolding properfactor_lless
+  using pf
+  unfolding properfactor_lless
 proof -
   interpret weak_partial_order "division_rel G" ..
   assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
   also from yy'
-       have "y .=\<^bsub>division_rel G\<^esub> y'" by simp
-  finally
-       show "x \<sqsubset>\<^bsub>division_rel G\<^esub> y'" by (simp add: carr)
+  have "y .=\<^bsub>division_rel G\<^esub> y'" by simp
+  finally show "x \<sqsubset>\<^bsub>division_rel G\<^esub> y'" by (simp add: carr)
 qed
 
 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"
   shows "properfactor G (c \<otimes> a) (c \<otimes> b)"
-using ab carr
-by (fastforce elim: properfactorE intro: properfactorI)
+  using ab carr by (fastforce elim: properfactorE intro: properfactorI)
 
 lemma (in monoid_cancel) properfactor_mult_l [simp]:
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "properfactor G (c \<otimes> a) (c \<otimes> b) = properfactor G a b"
-using carr
-by (fastforce elim: properfactorE intro: properfactorI)
+  using carr by (fastforce elim: properfactorE intro: properfactorI)
 
 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"
   shows "properfactor G (a \<otimes> c) (b \<otimes> c)"
-using ab carr
-by (fastforce elim: properfactorE intro: properfactorI)
+  using ab carr by (fastforce elim: properfactorE intro: properfactorI)
 
 lemma (in comm_monoid_cancel) properfactor_mult_r [simp]:
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "properfactor G (a \<otimes> c) (b \<otimes> c) = properfactor G a b"
-using carr
-by (fastforce elim: properfactorE intro: properfactorI)
+  using carr by (fastforce elim: properfactorE intro: properfactorI)
 
 lemma (in monoid) properfactor_prod_r:
   assumes ab: "properfactor G a b"
     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "properfactor G a (b \<otimes> c)"
-by (intro properfactor_trans2[OF ab] divides_prod_r, simp+)
+  by (intro properfactor_trans2[OF ab] divides_prod_r) simp_all
 
 lemma (in comm_monoid) properfactor_prod_l:
   assumes ab: "properfactor G a b"
     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "properfactor G a (c \<otimes> b)"
-by (intro properfactor_trans2[OF ab] divides_prod_l, simp+)
+  by (intro properfactor_trans2[OF ab] divides_prod_l) simp_all
 
 
 subsection \<open>Irreducible Elements and Primes\<close>
@@ -794,77 +720,71 @@
   assumes "a \<notin> Units G"
     and "\<And>b. \<lbrakk>b \<in> carrier G; properfactor G b a\<rbrakk> \<Longrightarrow> b \<in> Units G"
   shows "irreducible G a"
-using assms 
-unfolding irreducible_def
-by blast
+  using assms unfolding irreducible_def by blast
 
 lemma irreducibleE:
   fixes G (structure)
   assumes irr: "irreducible G a"
-     and elim: "\<lbrakk>a \<notin> Units G; \<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G\<rbrakk> \<Longrightarrow> P"
+    and elim: "\<lbrakk>a \<notin> Units G; \<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G\<rbrakk> \<Longrightarrow> P"
   shows "P"
-using assms
-unfolding irreducible_def
-by blast
+  using assms unfolding irreducible_def by blast
 
 lemma irreducibleD:
   fixes G (structure)
   assumes irr: "irreducible G a"
-     and pf: "properfactor G b a"
-     and bcarr: "b \<in> carrier G"
+    and pf: "properfactor G b a"
+    and bcarr: "b \<in> carrier G"
   shows "b \<in> Units G"
-using assms
-by (fast elim: irreducibleE)
+  using assms by (fast elim: irreducibleE)
 
 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"
   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)
-done
+  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)
+  done
 
 lemma (in monoid) irreducible_prod_rI:
   assumes airr: "irreducible G a"
     and bunit: "b \<in> Units G"
     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 associatedI2 m_closed properfactor_cong_r)
-done
+  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 associatedI2 m_closed properfactor_cong_r)
+  done
 
 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
+  apply (subst m_comm, simp+)
+  apply (intro irreducible_prod_rI assms)
+  done
 
 lemma (in comm_monoid_cancel) irreducible_prodE [elim]:
   assumes irr: "irreducible G (a \<otimes> b)"
     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
     and e1: "\<lbrakk>irreducible G a; b \<in> Units G\<rbrakk> \<Longrightarrow> P"
     and e2: "\<lbrakk>a \<in> Units G; irreducible G b\<rbrakk> \<Longrightarrow> P"
-  shows "P"
-using irr
+  shows P
+  using irr
 proof (elim irreducibleE)
   assume abnunit: "a \<otimes> b \<notin> Units G"
     and isunit[rule_format]: "\<forall>ba. ba \<in> carrier G \<and> properfactor G ba (a \<otimes> b) \<longrightarrow> ba \<in> Units G"
-
-  show "P"
+  show P
   proof (cases "a \<in> Units G")
-    assume aunit: "a \<in>  Units G"
+    case aunit: True
     have "irreducible G b"
-    apply (rule irreducibleI)
+      apply (rule irreducibleI)
     proof (rule ccontr, simp)
       assume "b \<in> Units G"
       with aunit have "(a \<otimes> b) \<in> Units G" by fast
@@ -873,19 +793,18 @@
       fix c
       assume ccarr: "c \<in> carrier G"
         and "properfactor G c b"
-      hence "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_l[of c b a])
-      from ccarr this show "c \<in> Units G" by (fast intro: isunit)
+      then have "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_l[of c b a])
+      with ccarr show "c \<in> Units G" by (fast intro: isunit)
     qed
-
-    from aunit this show "P" by (rule e2)
+    with aunit show "P" by (rule e2)
   next
-    assume anunit: "a \<notin> Units G"
+    case anunit: False
     with carr have "properfactor G b (b \<otimes> a)" by (fast intro: properfactorI3)
-    hence bf: "properfactor G b (a \<otimes> b)" by (subst m_comm[of a b], simp+)
-    hence bunit: "b \<in> Units G" by (intro isunit, simp)
+    then have bf: "properfactor G b (a \<otimes> b)" by (subst m_comm[of a b], simp+)
+    then have bunit: "b \<in> Units G" by (intro isunit, simp)
 
     have "irreducible G a"
-    apply (rule irreducibleI)
+      apply (rule irreducibleI)
     proof (rule ccontr, simp)
       assume "a \<in> Units G"
       with bunit have "(a \<otimes> b) \<in> Units G" by fast
@@ -894,10 +813,10 @@
       fix c
       assume ccarr: "c \<in> carrier G"
         and "properfactor G c a"
-      hence "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_r[of c a b])
-      from ccarr this show "c \<in> Units G" by (fast intro: isunit)
+      then have "properfactor G c (a \<otimes> b)"
+        by (simp add: properfactor_prod_r[of c a b])
+      with ccarr show "c \<in> Units G" by (fast intro: isunit)
     qed
-
     from this bunit show "P" by (rule e1)
   qed
 qed
@@ -910,66 +829,57 @@
   assumes "p \<notin> Units G"
     and "\<And>a b. \<lbrakk>a \<in> carrier G; b \<in> carrier G; p divides (a \<otimes> b)\<rbrakk> \<Longrightarrow> p divides a \<or> p divides b"
   shows "prime G p"
-using assms
-unfolding prime_def
-by blast
+  using assms unfolding prime_def by blast
 
 lemma primeE:
   fixes G (structure)
   assumes pprime: "prime G p"
     and e: "\<lbrakk>p \<notin> Units G; \<forall>a\<in>carrier G. \<forall>b\<in>carrier G.
-                          p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b\<rbrakk> \<Longrightarrow> P"
+      p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b\<rbrakk> \<Longrightarrow> P"
   shows "P"
-using pprime
-unfolding prime_def
-by (blast dest: e)
+  using pprime unfolding prime_def by (blast dest: e)
 
 lemma (in comm_monoid_cancel) prime_divides:
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
     and pprime: "prime G p"
     and pdvd: "p divides a \<otimes> b"
   shows "p divides a \<or> p divides b"
-using assms
-by (blast elim: primeE)
+  using assms by (blast elim: primeE)
 
 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"
   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)
-done
+  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)
+  done
+
 
 subsection \<open>Factorization and Factorial Monoids\<close>
 
 subsubsection \<open>Function definitions\<close>
 
-definition
-  factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
+definition factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
   where "factors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> = a"
 
-definition
-  wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool"
+definition wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool"
   where "wfactors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> \<sim>\<^bsub>G\<^esub> a"
 
-abbreviation
-  list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44)
-  where "list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)"
-
-definition
-  essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool"
+abbreviation list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44)
+  where "list_assoc G \<equiv> list_all2 (op \<sim>\<^bsub>G\<^esub>)"
+
+definition essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool"
   where "essentially_equal G fs1 fs2 \<longleftrightarrow> (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)"
 
 
 locale factorial_monoid = comm_monoid_cancel +
-  assumes factors_exist: 
-          "\<lbrakk>a \<in> carrier G; a \<notin> Units G\<rbrakk> \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a"
-      and factors_unique: 
-          "\<lbrakk>factors G fs a; factors G fs' a; a \<in> carrier G; a \<notin> Units G; 
-            set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
+  assumes factors_exist: "\<lbrakk>a \<in> carrier G; a \<notin> Units G\<rbrakk> \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a"
+    and factors_unique:
+      "\<lbrakk>factors G fs a; factors G fs' a; a \<in> carrier G; a \<notin> Units G;
+        set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
 
 
 subsubsection \<open>Comparing lists of elements\<close>
@@ -979,44 +889,45 @@
 lemma (in monoid) listassoc_refl [simp, intro]:
   assumes "set as \<subseteq> carrier G"
   shows "as [\<sim>] as"
-using assms
-by (induct as) simp+
+  using assms by (induct as) simp_all
 
 lemma (in monoid) listassoc_sym [sym]:
   assumes "as [\<sim>] bs"
-    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
+    and "set as \<subseteq> carrier G"
+    and "set bs \<subseteq> carrier G"
   shows "bs [\<sim>] as"
-using assms
+  using assms
 proof (induct as arbitrary: bs, simp)
   case Cons
-  thus ?case
-    apply (induct bs, simp)
+  then show ?case
+    apply (induct bs)
+     apply simp
     apply clarsimp
     apply (iprover intro: associated_sym)
-  done
+    done
 qed
 
 lemma (in monoid) listassoc_trans [trans]:
   assumes "as [\<sim>] bs" and "bs [\<sim>] cs"
     and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" and "set cs \<subseteq> carrier G"
   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
+  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
 
 lemma (in monoid_cancel) irrlist_listassoc_cong:
   assumes "\<forall>a\<in>set as. irreducible G a"
     and "as [\<sim>] bs"
     and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
   shows "\<forall>a\<in>set bs. irreducible G a"
-using assms
-apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)
-apply (blast intro: irreducible_cong)
-done
+  using assms
+  apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)
+  apply (blast intro: irreducible_cong)
+  done
 
 
 text \<open>Permutations\<close>
@@ -1024,36 +935,34 @@
 lemma perm_map [intro]:
   assumes p: "a <~~> b"
   shows "map f a <~~> map f b"
-using p
-by induct auto
+  using p by induct auto
 
 lemma perm_map_switch:
   assumes m: "map f a = map f b" and p: "b <~~> c"
   shows "\<exists>d. a <~~> d \<and> map f d = map f c"
-using p m
-by (induct arbitrary: a) (simp, force, force, blast)
+  using p m by (induct arbitrary: a) (simp, force, force, blast)
 
 lemma (in monoid) perm_assoc_switch:
-   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
+  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
 
 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
+  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
 
 declare perm_sym [sym]
 
@@ -1062,19 +971,17 @@
     and as: "P (set as)"
   shows "P (set bs)"
 proof -
-  from perm
-      have "mset as = mset bs"
-      by (simp add: mset_eq_perm)
-  hence "set as = set bs" by (rule mset_eq_setD)
-  with as
-      show "P (set bs)" by simp
+  from perm have "mset as = mset bs"
+    by (simp add: mset_eq_perm)
+  then have "set as = set bs"
+    by (rule mset_eq_setD)
+  with as show "P (set bs)"
+    by simp
 qed
 
-lemmas (in monoid) perm_closed =
-    perm_setP[of _ _ "\<lambda>as. as \<subseteq> carrier G"]
-
-lemmas (in monoid) irrlist_perm_cong =
-    perm_setP[of _ _ "\<lambda>as. \<forall>a\<in>as. irreducible G a"]
+lemmas (in monoid) perm_closed = perm_setP[of _ _ "\<lambda>as. as \<subseteq> carrier G"]
+
+lemmas (in monoid) irrlist_perm_cong = perm_setP[of _ _ "\<lambda>as. \<forall>a\<in>as. irreducible G a"]
 
 
 text \<open>Essentially equal factorizations\<close>
@@ -1082,70 +989,61 @@
 lemma (in monoid) essentially_equalI:
   assumes ex: "fs1 <~~> fs1'"  "fs1' [\<sim>] fs2"
   shows "essentially_equal G fs1 fs2"
-using ex
-unfolding essentially_equal_def
-by fast
+  using ex unfolding essentially_equal_def by fast
 
 lemma (in monoid) essentially_equalE:
   assumes ee: "essentially_equal G fs1 fs2"
     and e: "\<And>fs1'. \<lbrakk>fs1 <~~> fs1'; fs1' [\<sim>] fs2\<rbrakk> \<Longrightarrow> P"
   shows "P"
-using ee
-unfolding essentially_equal_def
-by (fast intro: e)
+  using ee unfolding essentially_equal_def by (fast intro: e)
 
 lemma (in monoid) ee_refl [simp,intro]:
   assumes carr: "set as \<subseteq> carrier G"
   shows "essentially_equal G as as"
-using carr
-by (fast intro: essentially_equalI)
+  using carr by (fast intro: essentially_equalI)
 
 lemma (in monoid) ee_sym [sym]:
   assumes ee: "essentially_equal G as bs"
     and carr: "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
   shows "essentially_equal G bs as"
-using ee
+  using ee
 proof (elim essentially_equalE)
   fix fs
   assume "as <~~> fs"  "fs [\<sim>] bs"
-  hence "\<exists>fs'. as [\<sim>] fs' \<and> fs' <~~> bs" by (rule perm_assoc_switch_r)
-  from this obtain fs'
-      where a: "as [\<sim>] fs'" and p: "fs' <~~> bs"
-      by auto
+  then have "\<exists>fs'. as [\<sim>] fs' \<and> fs' <~~> bs"
+    by (rule perm_assoc_switch_r)
+  then obtain fs' where a: "as [\<sim>] fs'" and p: "fs' <~~> bs"
+    by auto
   from p have "bs <~~> fs'" by (rule perm_sym)
-  with a[symmetric] carr
-      show ?thesis
-      by (iprover intro: essentially_equalI perm_closed)
+  with a[symmetric] carr show ?thesis
+    by (iprover intro: essentially_equalI perm_closed)
 qed
 
 lemma (in monoid) ee_trans [trans]:
   assumes ab: "essentially_equal G as bs" and bc: "essentially_equal G bs cs"
-    and ascarr: "set as \<subseteq> carrier G" 
+    and ascarr: "set as \<subseteq> carrier G"
     and bscarr: "set bs \<subseteq> carrier G"
     and cscarr: "set cs \<subseteq> carrier G"
   shows "essentially_equal G as cs"
-using ab bc
+  using ab bc
 proof (elim essentially_equalE)
   fix abs bcs
   assume  "abs [\<sim>] bs" and pb: "bs <~~> bcs"
-  hence "\<exists>bs'. abs <~~> bs' \<and> bs' [\<sim>] bcs" by (rule perm_assoc_switch)
-  from this obtain bs'
-      where p: "abs <~~> bs'" and a: "bs' [\<sim>] bcs"
-      by auto
+  then have "\<exists>bs'. abs <~~> bs' \<and> bs' [\<sim>] bcs"
+    by (rule perm_assoc_switch)
+  then obtain bs' where p: "abs <~~> bs'" and a: "bs' [\<sim>] bcs"
+    by auto
 
   assume "as <~~> abs"
-  with p
-      have pp: "as <~~> bs'" by fast
+  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)
-
-  with pp
-      show ?thesis
-      by (rule essentially_equalI)
+  finally (listassoc_trans) have "bs' [\<sim>] cs" by (simp add: c1 c2 cscarr)
+  with pp show ?thesis
+    by (rule essentially_equalI)
 qed
 
 
@@ -1156,47 +1054,46 @@
 lemma (in monoid) multlist_closed [simp, intro]:
   assumes ascarr: "set fs \<subseteq> carrier G"
   shows "foldr (op \<otimes>) fs \<one> \<in> carrier G"
-by (insert ascarr, induct fs, simp+)
+  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"
   shows "f divides (foldr (op \<otimes>) fs \<one>)"
-using assms
-apply (induct fs)
- apply simp
-apply (case_tac "f = a", simp)
- apply (fast intro: dividesI)
-apply clarsimp
-apply (metis assms(2) divides_prod_l multlist_closed)
-done
+  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
 
 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 (op \<otimes>) fs \<one> \<sim> foldr (op \<otimes>) fs' \<one>"
-using assms
+  using assms
 proof (induct fs arbitrary: fs', simp)
   case (Cons a as fs')
-  thus ?case
-  apply (induct fs', simp)
+  then show ?case
+    apply (induct fs', simp)
   proof clarsimp
     fix b bs
-    assume "a \<sim> b" 
+    assume "a \<sim> b"
       and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
       and ascarr: "set as \<subseteq> carrier G"
-    hence p: "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> as \<one>"
-        by (fast intro: mult_cong_l)
+    then have p: "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<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 op \<otimes> as \<one> \<sim> foldr op \<otimes> fs' \<one>"
-      hence "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by simp
-      with ascarr bscarr bcarr
-          have "b \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>"
-          by (fast intro: mult_cong_r)
-   finally
-       show "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>"
-       by (simp add: ascarr bscarr acarr bcarr)
+    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 op \<otimes> as \<one> \<sim> foldr op \<otimes> fs' \<one>"
+    then have "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by simp
+    with ascarr bscarr bcarr have "b \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>"
+      by (fast intro: mult_cong_r)
+    finally show "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>"
+      by (simp add: ascarr bscarr acarr bcarr)
   qed
 qed
 
@@ -1204,12 +1101,12 @@
   assumes prm: "as <~~> bs"
     and ascarr: "set as \<subseteq> carrier G"
   shows "foldr (op \<otimes>) as \<one> = foldr (op \<otimes>) bs \<one>"
-using prm ascarr
-apply (induct, simp, clarsimp simp add: m_ac, clarsimp)
+  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"
-  hence "set ys \<subseteq> carrier G" by (rule perm_closed)
+  then have "set ys \<subseteq> carrier G" by (rule perm_closed)
   moreover assume "set ys \<subseteq> carrier G \<Longrightarrow> foldr op \<otimes> ys \<one> = foldr op \<otimes> zs \<one>"
   ultimately show "foldr op \<otimes> ys \<one> = foldr op \<otimes> zs \<one>" by simp
 qed
@@ -1218,10 +1115,10 @@
   assumes "essentially_equal G fs fs'"
     and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
   shows "foldr (op \<otimes>) fs \<one> \<sim> foldr (op \<otimes>) fs' \<one>"
-using assms
-apply (elim essentially_equalE)
-apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)
-done
+  using assms
+  apply (elim essentially_equalE)
+  apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)
+  done
 
 
 subsubsection \<open>Factorization in irreducible elements\<close>
@@ -1231,53 +1128,42 @@
   assumes "\<forall>f\<in>set fs. irreducible G f"
     and "foldr (op \<otimes>) fs \<one> \<sim> a"
   shows "wfactors G fs a"
-using assms
-unfolding wfactors_def
-by simp
+  using assms unfolding wfactors_def by simp
 
 lemma wfactorsE:
   fixes G (structure)
   assumes wf: "wfactors G fs a"
     and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> \<sim> a\<rbrakk> \<Longrightarrow> P"
   shows "P"
-using wf
-unfolding wfactors_def
-by (fast dest: e)
+  using wf unfolding wfactors_def by (fast dest: e)
 
 lemma (in monoid) factorsI:
   assumes "\<forall>f\<in>set fs. irreducible G f"
     and "foldr (op \<otimes>) fs \<one> = a"
   shows "factors G fs a"
-using assms
-unfolding factors_def
-by simp
+  using assms unfolding factors_def by simp
 
 lemma factorsE:
   fixes G (structure)
   assumes f: "factors G fs a"
     and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> = a\<rbrakk> \<Longrightarrow> P"
   shows "P"
-using f
-unfolding factors_def
-by (simp add: e)
+  using f unfolding factors_def by (simp add: e)
 
 lemma (in monoid) factors_wfactors:
   assumes "factors G as a" and "set as \<subseteq> carrier G"
   shows "wfactors G as a"
-using assms
-by (blast elim: factorsE intro: wfactorsI)
+  using assms by (blast elim: factorsE intro: wfactorsI)
 
 lemma (in monoid) wfactors_factors:
   assumes "wfactors G as a" and "set as \<subseteq> carrier G"
   shows "\<exists>a'. factors G as a' \<and> a' \<sim> a"
-using assms
-by (blast elim: wfactorsE intro: factorsI)
+  using assms by (blast elim: wfactorsE intro: factorsI)
 
 lemma (in monoid) factors_closed [dest]:
   assumes "factors G fs a" and "set fs \<subseteq> carrier G"
   shows "a \<in> carrier G"
-using assms
-by (elim factorsE, clarsimp)
+  using assms by (elim factorsE, clarsimp)
 
 lemma (in monoid) nunit_factors:
   assumes anunit: "a \<notin> Units G"
@@ -1291,8 +1177,7 @@
 lemma (in monoid) unit_wfactors [simp]:
   assumes aunit: "a \<in> Units G"
   shows "wfactors G [] a"
-using aunit
-by (intro wfactorsI) (simp, simp add: Units_assoc)
+  using aunit by (intro wfactorsI) (simp, simp add: Units_assoc)
 
 lemma (in comm_monoid_cancel) unit_wfactors_empty:
   assumes aunit: "a \<in> Units G"
@@ -1303,27 +1188,21 @@
   fix f fs'
   assume fs: "fs = f # fs'"
 
-  from carr
-      have fcarr[simp]: "f \<in> carrier G"
-      and carr'[simp]: "set fs' \<subseteq> carrier G"
-      by (simp add: fs)+
-
-  from fs wf
-      have "irreducible G f" by (simp add: wfactors_def)
-  hence fnunit: "f \<notin> Units G" by (fast elim: irreducibleE)
-
-  from fs wf
-      have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
+  from carr have fcarr[simp]: "f \<in> carrier G" and carr'[simp]: "set fs' \<subseteq> carrier G"
+    by (simp_all add: fs)
+
+  from fs wf have "irreducible G f" by (simp add: wfactors_def)
+  then have fnunit: "f \<notin> Units G" by (fast elim: irreducibleE)
+
+  from fs wf have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
 
   note aunit
   also from fs wf
-       have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
-       have "a \<sim> f \<otimes> foldr (op \<otimes>) fs' \<one>" 
-       by (simp add: Units_closed[OF aunit] a[symmetric])
-  finally
-       have "f \<otimes> foldr (op \<otimes>) fs' \<one> \<in> Units G" by simp
-  hence "f \<in> Units G" by (intro unit_factor[of f], simp+)
-
+  have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
+  have "a \<sim> f \<otimes> foldr (op \<otimes>) fs' \<one>"
+    by (simp add: Units_closed[OF aunit] a[symmetric])
+  finally have "f \<otimes> foldr (op \<otimes>) fs' \<one> \<in> Units G" by simp
+  then have "f \<in> Units G" by (intro unit_factor[of f], simp+)
   with fnunit show "False" by simp
 qed
 
@@ -1335,16 +1214,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"
-using fact
-apply (elim wfactorsE, intro wfactorsI)
-apply (metis assms(2) assms(4) assms(5) irrlist_listassoc_cong)
+  using fact
+  apply (elim wfactorsE, intro wfactorsI)
+   apply (metis assms(2) assms(4) assms(5) irrlist_listassoc_cong)
 proof -
-  from asc[symmetric]
-       have "foldr op \<otimes> fs' \<one> \<sim> foldr op \<otimes> fs \<one>" 
-       by (simp add: multlist_listassoc_cong carr)
+  from asc[symmetric] have "foldr op \<otimes> fs' \<one> \<sim> foldr op \<otimes> fs \<one>"
+    by (simp add: multlist_listassoc_cong carr)
   also assume "foldr op \<otimes> fs \<one> \<sim> a"
-  finally
-       show "foldr op \<otimes> fs' \<one> \<sim> a" by (simp add: carr)
+  finally show "foldr op \<otimes> fs' \<one> \<sim> a" by (simp add: carr)
 qed
 
 lemma (in comm_monoid) wfactors_perm_cong_l:
@@ -1352,37 +1229,36 @@
     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
+  apply (elim wfactorsE, intro wfactorsI)
+   apply (rule irrlist_perm_cong, assumption+)
+  apply (simp add: multlist_perm_cong[symmetric])
+  done
 
 lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]:
   assumes ee: "essentially_equal G as bs"
     and bfs: "wfactors G bs b"
     and carr: "b \<in> carrier G"  "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
   shows "wfactors G as b"
-using ee
+  using ee
 proof (elim essentially_equalE)
   fix fs
   assume prm: "as <~~> fs"
-  with carr
-       have fscarr: "set fs \<subseteq> carrier G" by (simp add: perm_closed)
+  with carr have fscarr: "set fs \<subseteq> carrier G" by (simp add: perm_closed)
 
   note bfs
   also assume [symmetric]: "fs [\<sim>] bs"
   also (wfactors_listassoc_cong_l)
-       note prm[symmetric]
+  note prm[symmetric]
   finally (wfactors_perm_cong_l)
-       show "wfactors G as b" by (simp add: carr fscarr)
+  show "wfactors G as b" by (simp add: carr fscarr)
 qed
 
 lemma (in monoid) wfactors_cong_r [trans]:
   assumes fac: "wfactors G fs a" and aa': "a \<sim> a'"
     and carr[simp]: "a \<in> carrier G"  "a' \<in> carrier G"  "set fs \<subseteq> carrier G"
   shows "wfactors G fs a'"
-using fac
+  using fac
 proof (elim wfactorsE, intro wfactorsI)
   assume "foldr op \<otimes> fs \<one> \<sim> a" also note aa'
   finally show "foldr op \<otimes> fs \<one> \<sim> a'" by simp
@@ -1394,61 +1270,64 @@
 lemma (in comm_monoid_cancel) unitfactor_ee:
   assumes uunit: "u \<in> Units G"
     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
+  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
 
 lemma (in comm_monoid_cancel) factors_cong_unit:
-  assumes uunit: "u \<in> Units G" and anunit: "a \<notin> Units G"
+  assumes uunit: "u \<in> Units G"
+    and anunit: "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
+  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
 
 lemma (in comm_monoid) perm_wfactorsD:
   assumes prm: "as <~~> bs"
-    and afs: "wfactors G as a" and bfs: "wfactors G bs b"
+    and afs: "wfactors G as a"
+    and bfs: "wfactors G bs b"
     and [simp]: "a \<in> carrier G"  "b \<in> carrier G"
-    and ascarr[simp]: "set as \<subseteq> carrier G"
+    and ascarr [simp]: "set as \<subseteq> carrier G"
   shows "a \<sim> b"
-using afs bfs
+  using afs bfs
 proof (elim wfactorsE)
   from prm have [simp]: "set bs \<subseteq> carrier G" by (simp add: perm_closed)
   assume "foldr op \<otimes> as \<one> \<sim> a"
-  hence "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+)
+  then have "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+)
   also from prm
-       have "foldr op \<otimes> as \<one> = foldr op \<otimes> bs \<one>" by (rule multlist_perm_cong, simp)
+  have "foldr op \<otimes> as \<one> = foldr op \<otimes> bs \<one>" by (rule multlist_perm_cong, simp)
   also assume "foldr op \<otimes> bs \<one> \<sim> b"
-  finally
-       show "a \<sim> b" by simp
+  finally show "a \<sim> b" by simp
 qed
 
 lemma (in comm_monoid_cancel) listassoc_wfactorsD:
   assumes assoc: "as [\<sim>] bs"
-    and afs: "wfactors G as a" and bfs: "wfactors G bs b"
+    and afs: "wfactors G as a"
+    and bfs: "wfactors G bs b"
     and [simp]: "a \<in> carrier G"  "b \<in> carrier G"
     and [simp]: "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
   shows "a \<sim> b"
-using afs bfs
+  using afs bfs
 proof (elim wfactorsE)
   assume "foldr op \<otimes> as \<one> \<sim> a"
-  hence "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+)
+  then have "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+)
   also from assoc
-       have "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by (rule multlist_listassoc_cong, simp+)
+  have "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by (rule multlist_listassoc_cong, simp+)
   also assume "foldr op \<otimes> bs \<one> \<sim> b"
-  finally
-       show "a \<sim> b" by simp
+  finally show "a \<sim> b" by simp
 qed
 
 lemma (in comm_monoid_cancel) ee_wfactorsD:
@@ -1457,16 +1336,17 @@
     and [simp]: "a \<in> carrier G"  "b \<in> carrier G"
     and ascarr[simp]: "set as \<subseteq> carrier G" and bscarr[simp]: "set bs \<subseteq> carrier G"
   shows "a \<sim> b"
-using ee
+  using ee
 proof (elim essentially_equalE)
   fix fs
   assume prm: "as <~~> fs"
-  hence as'carr[simp]: "set fs \<subseteq> carrier G" by (simp add: perm_closed)
-  from afs prm
-      have afs': "wfactors G fs a" by (rule wfactors_perm_cong_l, simp)
+  then have as'carr[simp]: "set fs \<subseteq> carrier G"
+    by (simp add: perm_closed)
+  from afs prm have afs': "wfactors G fs a"
+    by (rule wfactors_perm_cong_l) simp
   assume "fs [\<sim>] bs"
-  from this afs' bfs
-      show "a \<sim> b" by (rule listassoc_wfactorsD, simp+)
+  from this afs' bfs show "a \<sim> b"
+    by (rule listassoc_wfactorsD) simp_all
 qed
 
 lemma (in comm_monoid_cancel) ee_factorsD:
@@ -1474,8 +1354,7 @@
     and afs: "factors G as a" and bfs:"factors G bs b"
     and "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
   shows "a \<sim> b"
-using assms
-by (blast intro: factors_wfactors dest: ee_wfactorsD)
+  using assms by (blast intro: factors_wfactors dest: ee_wfactorsD)
 
 lemma (in factorial_monoid) ee_factorsI:
   assumes ab: "a \<sim> b"
@@ -1485,33 +1364,29 @@
   shows "essentially_equal G as bs"
 proof -
   note carr[simp] = factors_closed[OF afs ascarr] ascarr[THEN subsetD]
-                    factors_closed[OF bfs bscarr] bscarr[THEN subsetD]
-
-  from ab carr
-      have "\<exists>u\<in>Units G. a = b \<otimes> u" by (fast elim: associatedE2)
-  from this obtain u
-      where uunit: "u \<in> Units G"
-      and a: "a = b \<otimes> u" by auto
-
-  from uunit bscarr
-      have ee: "essentially_equal G (bs[0 := (bs!0 \<otimes> u)]) bs" 
-                (is "essentially_equal G ?bs' bs")
-      by (rule unitfactor_ee)
-
-  from bscarr uunit
-      have bs'carr: "set ?bs' \<subseteq> carrier G"
-      by (cases bs) (simp add: Units_closed)+
-
-  from uunit bnunit bfs bscarr
-      have fac: "factors G ?bs' (b \<otimes> u)"
-      by (rule factors_cong_unit)
+    factors_closed[OF bfs bscarr] bscarr[THEN subsetD]
+
+  from ab carr have "\<exists>u\<in>Units G. a = b \<otimes> u"
+    by (fast elim: associatedE2)
+  then obtain u where uunit: "u \<in> Units G" and a: "a = b \<otimes> u"
+    by auto
+
+  from uunit bscarr have ee: "essentially_equal G (bs[0 := (bs!0 \<otimes> u)]) bs"
+    (is "essentially_equal G ?bs' bs")
+    by (rule unitfactor_ee)
+
+  from bscarr uunit have bs'carr: "set ?bs' \<subseteq> carrier G"
+    by (cases bs) (simp_all add: Units_closed)
+
+  from uunit bnunit bfs bscarr have fac: "factors G ?bs' (b \<otimes> u)"
+    by (rule factors_cong_unit)
 
   from afs fac[simplified a[symmetric]] ascarr bs'carr anunit
-       have "essentially_equal G as ?bs'"
-       by (blast intro: factors_unique)
+  have "essentially_equal G as ?bs'"
+    by (blast intro: factors_unique)
   also note ee
-  finally
-      show "essentially_equal G as bs" by (simp add: ascarr bscarr bs'carr)
+  finally show "essentially_equal G as bs"
+    by (simp add: ascarr bscarr bs'carr)
 qed
 
 lemma (in factorial_monoid) ee_wfactorsI:
@@ -1520,74 +1395,68 @@
     and acarr[simp]: "a \<in> carrier G" and bcarr[simp]: "b \<in> carrier G"
     and ascarr[simp]: "set as \<subseteq> carrier G" and bscarr[simp]: "set bs \<subseteq> carrier G"
   shows "essentially_equal G as bs"
-using assms
+  using assms
 proof (cases "a \<in> Units G")
-  assume aunit: "a \<in> Units G"
+  case aunit: True
   also note asc
   finally have bunit: "b \<in> Units G" by simp
 
-  from aunit asf ascarr
-      have e: "as = []" by (rule unit_wfactors_empty)
-  from bunit bsf bscarr
-      have e': "bs = []" by (rule unit_wfactors_empty)
+  from aunit asf ascarr have e: "as = []"
+    by (rule unit_wfactors_empty)
+  from bunit bsf bscarr have e': "bs = []"
+    by (rule unit_wfactors_empty)
 
   have "essentially_equal G [] []"
-      by (fast intro: essentially_equalI)
-  thus ?thesis by (simp add: e e')
+    by (fast intro: essentially_equalI)
+  then show ?thesis
+    by (simp add: e e')
 next
-  assume anunit: "a \<notin> Units G"
+  case anunit: False
   have bnunit: "b \<notin> Units G"
   proof clarify
     assume "b \<in> Units G"
     also note asc[symmetric]
     finally have "a \<in> Units G" by simp
-    with anunit
-         show "False" ..
+    with anunit show False ..
   qed
 
-  have "\<exists>a'. factors G as a' \<and> a' \<sim> a" by (rule wfactors_factors[OF asf ascarr])
-  from this obtain a'
-      where fa': "factors G as a'"
-      and a': "a' \<sim> a"
-      by auto
-  from fa' ascarr
-      have a'carr[simp]: "a' \<in> carrier G" by fast
+  have "\<exists>a'. factors G as a' \<and> a' \<sim> a"
+    by (rule wfactors_factors[OF asf ascarr])
+  then obtain a' where fa': "factors G as a'" and a': "a' \<sim> a"
+    by auto
+  from fa' ascarr have a'carr[simp]: "a' \<in> carrier G"
+    by fast
 
   have a'nunit: "a' \<notin> Units G"
-  proof (clarify)
+  proof clarify
     assume "a' \<in> Units G"
     also note a'
     finally have "a \<in> Units G" by simp
     with anunit
-         show "False" ..
+    show "False" ..
   qed
 
-  have "\<exists>b'. factors G bs b' \<and> b' \<sim> b" by (rule wfactors_factors[OF bsf bscarr])
-  from this obtain b'
-      where fb': "factors G bs b'"
-      and b': "b' \<sim> b"
-      by auto
-  from fb' bscarr
-      have b'carr[simp]: "b' \<in> carrier G" by fast
+  have "\<exists>b'. factors G bs b' \<and> b' \<sim> b"
+    by (rule wfactors_factors[OF bsf bscarr])
+  then obtain b' where fb': "factors G bs b'" and b': "b' \<sim> b"
+    by auto
+  from fb' bscarr have b'carr[simp]: "b' \<in> carrier G"
+    by fast
 
   have b'nunit: "b' \<notin> Units G"
-  proof (clarify)
+  proof clarify
     assume "b' \<in> Units G"
     also note b'
     finally have "b \<in> Units G" by simp
-    with bnunit
-        show "False" ..
+    with bnunit show False ..
   qed
 
   note a'
   also note asc
   also note b'[symmetric]
-  finally
-       have "a' \<sim> b'" by simp
-
-  from this fa' a'nunit fb' b'nunit ascarr bscarr
-  show "essentially_equal G as bs"
-      by (rule ee_factorsI)
+  finally have "a' \<sim> b'" by simp
+  from this fa' a'nunit fb' b'nunit ascarr bscarr show "essentially_equal G as bs"
+    by (rule ee_factorsI)
 qed
 
 lemma (in factorial_monoid) ee_wfactors:
@@ -1596,189 +1465,168 @@
     and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
     and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
   shows asc: "a \<sim> b = essentially_equal G as bs"
-using assms
-by (fast intro: ee_wfactorsI ee_wfactorsD)
+  using assms by (fast intro: ee_wfactorsI ee_wfactorsD)
 
 lemma (in factorial_monoid) wfactors_exist [intro, simp]:
   assumes acarr[simp]: "a \<in> carrier G"
   shows "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a"
 proof (cases "a \<in> Units G")
-  assume "a \<in> Units G"
-  hence "wfactors G [] a" by (rule unit_wfactors)
-  thus ?thesis by (intro exI) force
+  case True
+  then have "wfactors G [] a" by (rule unit_wfactors)
+  then show ?thesis by (intro exI) force
 next
-  assume "a \<notin> Units G"
-  hence "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" by (intro factors_exist acarr)
-  from this obtain fs
-      where fscarr: "set fs \<subseteq> carrier G"
-      and f: "factors G fs a"
-      by auto
+  case False
+  then have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a"
+    by (intro factors_exist acarr)
+  then obtain fs where fscarr: "set fs \<subseteq> carrier G" and f: "factors G fs a"
+    by auto
   from f have "wfactors G fs a" by (rule factors_wfactors) fact
-  from fscarr this
-      show ?thesis by fast
+  with fscarr show ?thesis by fast
 qed
 
 lemma (in monoid) wfactors_prod_exists [intro, simp]:
   assumes "\<forall>a \<in> set as. irreducible G a" and "set as \<subseteq> carrier G"
   shows "\<exists>a. a \<in> carrier G \<and> wfactors G as a"
-unfolding wfactors_def
-using assms
-by blast
+  unfolding wfactors_def using assms by blast
 
 lemma (in factorial_monoid) wfactors_unique:
-  assumes "wfactors G fs a" and "wfactors G fs' a"
+  assumes "wfactors G fs a"
+    and "wfactors G fs' a"
     and "a \<in> carrier G"
-    and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
+    and "set fs \<subseteq> carrier G"
+    and "set fs' \<subseteq> carrier G"
   shows "essentially_equal G fs fs'"
-using assms
-by (fast intro: ee_wfactorsI[of a a])
+  using assms by (fast intro: ee_wfactorsI[of a a])
 
 lemma (in monoid) factors_mult_single:
   assumes "irreducible G a" and "factors G fb b" and "a \<in> carrier G"
   shows "factors G (a # fb) (a \<otimes> b)"
-using assms
-unfolding factors_def
-by simp
+  using assms unfolding factors_def by simp
 
 lemma (in monoid_cancel) wfactors_mult_single:
   assumes f: "irreducible G a"  "wfactors G fb b"
-        "a \<in> carrier G"  "b \<in> carrier G"  "set fb \<subseteq> carrier G"
+    "a \<in> carrier G"  "b \<in> carrier G"  "set fb \<subseteq> carrier G"
   shows "wfactors G (a # fb) (a \<otimes> b)"
-using assms
-unfolding wfactors_def
-by (simp add: mult_cong_r)
+  using assms unfolding wfactors_def by (simp add: mult_cong_r)
 
 lemma (in monoid) factors_mult:
   assumes factors: "factors G fa a"  "factors G fb b"
-    and ascarr: "set fa \<subseteq> carrier G" and bscarr:"set fb \<subseteq> carrier G"
+    and ascarr: "set fa \<subseteq> carrier G"
+    and bscarr: "set fb \<subseteq> carrier G"
   shows "factors G (fa @ fb) (a \<otimes> b)"
-using assms
-unfolding factors_def
-apply (safe, force)
-apply hypsubst_thin
-apply (induct fa)
- apply simp
-apply (simp add: m_assoc)
-done
+  using assms
+  unfolding factors_def
+  apply safe
+   apply force
+  apply hypsubst_thin
+  apply (induct fa)
+   apply simp
+  apply (simp add: m_assoc)
+  done
 
 lemma (in comm_monoid_cancel) wfactors_mult [intro]:
   assumes asf: "wfactors G as a" and bsf:"wfactors G bs b"
     and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
     and ascarr: "set as \<subseteq> carrier G" and bscarr:"set bs \<subseteq> carrier G"
   shows "wfactors G (as @ bs) (a \<otimes> b)"
-apply (insert wfactors_factors[OF asf ascarr])
-apply (insert wfactors_factors[OF bsf bscarr])
-proof (clarsimp)
+  using wfactors_factors[OF asf ascarr] and wfactors_factors[OF bsf bscarr]
+proof clarsimp
   fix a' b'
   assume asf': "factors G as a'" and a'a: "a' \<sim> a"
-     and bsf': "factors G bs b'" and b'b: "b' \<sim> b"
+    and bsf': "factors G bs b'" and b'b: "b' \<sim> b"
   from asf' have a'carr: "a' \<in> carrier G" by (rule factors_closed) fact
   from bsf' have b'carr: "b' \<in> carrier G" by (rule factors_closed) fact
 
   note carr = acarr bcarr a'carr b'carr ascarr bscarr
 
-  from asf' bsf'
-      have "factors G (as @ bs) (a' \<otimes> b')" by (rule factors_mult) fact+
-
-  with carr
-       have abf': "wfactors G (as @ bs) (a' \<otimes> b')" by (intro factors_wfactors) simp+
-  also from b'b carr
-       have trb: "a' \<otimes> b' \<sim> a' \<otimes> b" by (intro mult_cong_r)
-  also from a'a carr
-       have tra: "a' \<otimes> b \<sim> a \<otimes> b" by (intro mult_cong_l)
-  finally
-       show "wfactors G (as @ bs) (a \<otimes> b)"
-       by (simp add: carr)
+  from asf' bsf' have "factors G (as @ bs) (a' \<otimes> b')"
+    by (rule factors_mult) fact+
+
+  with carr have abf': "wfactors G (as @ bs) (a' \<otimes> b')"
+    by (intro factors_wfactors) simp_all
+  also from b'b carr have trb: "a' \<otimes> b' \<sim> a' \<otimes> b"
+    by (intro mult_cong_r)
+  also from a'a carr have tra: "a' \<otimes> b \<sim> a \<otimes> b"
+    by (intro mult_cong_l)
+  finally show "wfactors G (as @ bs) (a \<otimes> b)"
+    by (simp add: carr)
 qed
 
 lemma (in comm_monoid) factors_dividesI:
-  assumes "factors G fs a" and "f \<in> set fs"
+  assumes "factors G fs a"
+    and "f \<in> set fs"
     and "set fs \<subseteq> carrier G"
   shows "f divides a"
-using assms
-by (fast elim: factorsE intro: multlist_dividesI)
+  using assms by (fast elim: factorsE intro: multlist_dividesI)
 
 lemma (in comm_monoid) wfactors_dividesI:
   assumes p: "wfactors G fs a"
     and fscarr: "set fs \<subseteq> carrier G" and acarr: "a \<in> carrier G"
     and f: "f \<in> set fs"
   shows "f divides a"
-apply (insert wfactors_factors[OF p fscarr], clarsimp)
-proof -
+  using wfactors_factors[OF p fscarr]
+proof clarsimp
   fix a'
-  assume fsa': "factors G fs a'"
-    and a'a: "a' \<sim> a"
-  with fscarr
-      have a'carr: "a' \<in> carrier G" by (simp add: factors_closed)
-
-  from fsa' fscarr f
-       have "f divides a'" by (fast intro: factors_dividesI)
+  assume fsa': "factors G fs a'" and a'a: "a' \<sim> a"
+  with fscarr have a'carr: "a' \<in> carrier G"
+    by (simp add: factors_closed)
+
+  from fsa' fscarr f have "f divides a'"
+    by (fast intro: factors_dividesI)
   also note a'a
-  finally
-       show "f divides a" by (simp add: f fscarr[THEN subsetD] acarr a'carr)
+  finally show "f divides a"
+    by (simp add: f fscarr[THEN subsetD] acarr a'carr)
 qed
 
 
 subsubsection \<open>Factorial monoids and wfactors\<close>
 
 lemma (in comm_monoid_cancel) factorial_monoidI:
-  assumes wfactors_exists: 
-          "\<And>a. a \<in> carrier G \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a"
-      and wfactors_unique: 
-          "\<And>a fs fs'. \<lbrakk>a \<in> carrier G; set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G; 
-                       wfactors G fs a; wfactors G fs' a\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
+  assumes wfactors_exists: "\<And>a. a \<in> carrier G \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a"
+    and wfactors_unique:
+      "\<And>a fs fs'. \<lbrakk>a \<in> carrier G; set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G;
+        wfactors G fs a; wfactors G fs' a\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
   shows "factorial_monoid G"
 proof
   fix a
   assume acarr: "a \<in> carrier G" and anunit: "a \<notin> Units G"
 
   from wfactors_exists[OF acarr]
-  obtain as
-      where ascarr: "set as \<subseteq> carrier G"
-      and afs: "wfactors G as a"
-      by auto
-  from afs ascarr
-      have "\<exists>a'. factors G as a' \<and> a' \<sim> a" by (rule wfactors_factors)
-  from this obtain a'
-      where afs': "factors G as a'"
-      and a'a: "a' \<sim> a"
-      by auto
-  from afs' ascarr
-      have a'carr: "a' \<in> carrier G" by fast
+  obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
+    by auto
+  from afs ascarr have "\<exists>a'. factors G as a' \<and> a' \<sim> a"
+    by (rule wfactors_factors)
+  then obtain a' where afs': "factors G as a'" and a'a: "a' \<sim> a"
+    by auto
+  from afs' ascarr have a'carr: "a' \<in> carrier G"
+    by fast
   have a'nunit: "a' \<notin> Units G"
   proof clarify
     assume "a' \<in> Units G"
     also note a'a
     finally have "a \<in> Units G" by (simp add: acarr)
-    with anunit
-        show "False" ..
+    with anunit show False ..
   qed
 
-  from a'carr acarr a'a
-      have "\<exists>u. u \<in> Units G \<and> a' = a \<otimes> u" by (blast elim: associatedE2)
-  from this obtain  u
-      where uunit: "u \<in> Units G"
-      and a': "a' = a \<otimes> u"
-      by auto
+  from a'carr acarr a'a have "\<exists>u. u \<in> Units G \<and> a' = a \<otimes> u"
+    by (blast elim: associatedE2)
+  then obtain u where uunit: "u \<in> Units G" and a': "a' = a \<otimes> u"
+    by auto
 
   note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit]
 
   have "a = a \<otimes> \<one>" by simp
   also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: uunit)
   also have "\<dots> = a' \<otimes> inv u" by (simp add: m_assoc[symmetric] a'[symmetric])
-  finally
-       have a: "a = a' \<otimes> inv u" .
-
-  from ascarr uunit
-      have cr: "set (as[0:=(as!0 \<otimes> inv u)]) \<subseteq> carrier G"
-      by (cases as, clarsimp+)
-
-  from afs' uunit a'nunit acarr ascarr
-      have "factors G (as[0:=(as!0 \<otimes> inv u)]) a"
-      by (simp add: a factors_cong_unit)
-
-  with cr
-      show "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" by fast
+  finally have a: "a = a' \<otimes> inv u" .
+
+  from ascarr uunit have cr: "set (as[0:=(as!0 \<otimes> inv u)]) \<subseteq> carrier G"
+    by (cases as) auto
+
+  from afs' uunit a'nunit acarr ascarr have "factors G (as[0:=(as!0 \<otimes> inv u)]) a"
+    by (simp add: a factors_cong_unit)
+  with cr show "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a"
+    by fast
 qed (blast intro: factors_wfactors wfactors_unique)
 
 
@@ -1788,11 +1636,9 @@
 
 (* FIXME: use class_of x instead of closure_of {x} *)
 
-abbreviation
-  "assocs G x == eq_closure_of (division_rel G) {x}"
-
-definition
-  "fmset G as = mset (map (\<lambda>a. assocs G a) as)"
+abbreviation "assocs G x \<equiv> eq_closure_of (division_rel G) {x}"
+
+definition "fmset G as = mset (map (\<lambda>a. assocs G a) as)"
 
 
 text \<open>Helper lemmas\<close>
@@ -1801,37 +1647,32 @@
   assumes "y \<in> assocs G x"
     and "x \<in> carrier G"
   shows "assocs G x = assocs G y"
-using assms
-apply safe
- apply (elim closure_ofE2, intro closure_ofI2[of _ _ y])
-   apply (clarsimp, iprover intro: associated_trans associated_sym, simp+)
-apply (elim closure_ofE2, intro closure_ofI2[of _ _ x])
-  apply (clarsimp, iprover intro: associated_trans, simp+)
-done
+  using assms
+  apply safe
+   apply (elim closure_ofE2, intro closure_ofI2[of _ _ y])
+     apply (clarsimp, iprover intro: associated_trans associated_sym, simp+)
+  apply (elim closure_ofE2, intro closure_ofI2[of _ _ x])
+    apply (clarsimp, iprover intro: associated_trans, simp+)
+  done
 
 lemma (in monoid) assocs_self:
   assumes "x \<in> carrier G"
   shows "x \<in> assocs G x"
-using assms
-by (fastforce intro: closure_ofI2)
+  using assms by (fastforce intro: closure_ofI2)
 
 lemma (in monoid) assocs_repr_independenceD:
   assumes repr: "assocs G x = assocs G y"
     and ycarr: "y \<in> carrier G"
   shows "y \<in> assocs G x"
-unfolding repr
-using ycarr
-by (intro assocs_self)
+  unfolding repr using ycarr by (intro assocs_self)
 
 lemma (in comm_monoid) assocs_assoc:
   assumes "a \<in> assocs G b"
     and "b \<in> carrier G"
   shows "a \<sim> b"
-using assms
-by (elim closure_ofE2, simp)
-
-lemmas (in comm_monoid) assocs_eqD =
-    assocs_repr_independenceD[THEN assocs_assoc]
+  using assms by (elim closure_ofE2) simp
+
+lemmas (in comm_monoid) assocs_eqD = assocs_repr_independenceD[THEN assocs_assoc]
 
 
 subsubsection \<open>Comparing multisets\<close>
@@ -1839,137 +1680,119 @@
 lemma (in monoid) fmset_perm_cong:
   assumes prm: "as <~~> bs"
   shows "fmset G as = fmset G bs"
-using perm_map[OF prm] unfolding mset_eq_perm fmset_def by blast
+  using perm_map[OF prm] unfolding mset_eq_perm fmset_def by blast
 
 lemma (in comm_monoid_cancel) eqc_listassoc_cong:
   assumes "as [\<sim>] bs"
     and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
   shows "map (assocs G) as = map (assocs G) bs"
-using assms
-apply (induct as arbitrary: bs, simp)
-apply (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1, safe)
- apply (clarsimp elim!: closure_ofE2) defer 1
- apply (clarsimp elim!: closure_ofE2) defer 1
+  using assms
+  apply (induct as arbitrary: bs, simp)
+  apply (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1, safe)
+   apply (clarsimp elim!: closure_ofE2) defer 1
+   apply (clarsimp elim!: closure_ofE2) defer 1
 proof -
   fix a x z
   assume carr[simp]: "a \<in> carrier G"  "x \<in> carrier G"  "z \<in> carrier G"
   assume "x \<sim> a"
   also assume "a \<sim> z"
   finally have "x \<sim> z" by simp
-  with carr
-      show "x \<in> assocs G z"
-      by (intro closure_ofI2) simp+
+  with carr show "x \<in> assocs G z"
+    by (intro closure_ofI2) simp_all
 next
   fix a x z
   assume carr[simp]: "a \<in> carrier G"  "x \<in> carrier G"  "z \<in> carrier G"
   assume "x \<sim> z"
   also assume [symmetric]: "a \<sim> z"
   finally have "x \<sim> a" by simp
-  with carr
-      show "x \<in> assocs G a"
-      by (intro closure_ofI2) simp+
+  with carr show "x \<in> assocs G a"
+    by (intro closure_ofI2) simp_all
 qed
 
 lemma (in comm_monoid_cancel) fmset_listassoc_cong:
-  assumes "as [\<sim>] bs" 
+  assumes "as [\<sim>] bs"
     and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
   shows "fmset G as = fmset G bs"
-using assms
-unfolding fmset_def
-by (simp add: eqc_listassoc_cong)
+  using assms unfolding fmset_def by (simp add: eqc_listassoc_cong)
 
 lemma (in comm_monoid_cancel) ee_fmset:
-  assumes ee: "essentially_equal G as bs" 
+  assumes ee: "essentially_equal G as bs"
     and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
   shows "fmset G as = fmset G bs"
-using ee
+  using ee
 proof (elim essentially_equalE)
   fix as'
   assume prm: "as <~~> as'"
-  from prm ascarr
-      have as'carr: "set as' \<subseteq> carrier G" by (rule perm_closed)
-
-  from prm
-       have "fmset G as = fmset G as'" by (rule fmset_perm_cong)
+  from prm ascarr have as'carr: "set as' \<subseteq> carrier G"
+    by (rule perm_closed)
+
+  from prm have "fmset G as = fmset G as'"
+    by (rule fmset_perm_cong)
   also assume "as' [\<sim>] bs"
-       with as'carr bscarr
-       have "fmset G as' = fmset G bs" by (simp add: fmset_listassoc_cong)
-  finally
-       show "fmset G as = fmset G bs" .
+  with as'carr bscarr have "fmset G as' = fmset G bs"
+    by (simp add: fmset_listassoc_cong)
+  finally show "fmset G as = fmset G bs" .
 qed
 
 lemma (in monoid_cancel) fmset_ee__hlp_induct:
   assumes prm: "cas <~~> cbs"
     and cdef: "cas = map (assocs G) as"  "cbs = map (assocs G) bs"
-  shows "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and> 
-                 cbs = map (assocs G) bs) \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)"
-apply (rule perm.induct[of cas cbs], rule prm)
-apply safe apply (simp_all del: mset_map)
-  apply (simp add: map_eq_Cons_conv, blast)
- apply force
+  shows "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and>
+    cbs = map (assocs G) bs) \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)"
+  apply (rule perm.induct[of cas cbs], rule prm)
+     apply safe
+     apply (simp_all del: mset_map)
+    apply (simp add: map_eq_Cons_conv)
+    apply blast
+   apply force
 proof -
   fix ys as bs
   assume p1: "map (assocs G) as <~~> ys"
     and r1[rule_format]:
-        "\<forall>asa bs. map (assocs G) as = map (assocs G) asa \<and>
-                  ys = map (assocs G) bs
-                  \<longrightarrow> (\<exists>as'. asa <~~> as' \<and> map (assocs G) as' = map (assocs G) bs)"
+      "\<forall>asa bs. map (assocs G) as = map (assocs G) asa \<and> ys = map (assocs G) bs
+        \<longrightarrow> (\<exists>as'. asa <~~> as' \<and> map (assocs G) as' = map (assocs G) bs)"
     and p2: "ys <~~> map (assocs G) bs"
-    and r2[rule_format]:
-        "\<forall>as bsa. ys = map (assocs G) as \<and>
-                  map (assocs G) bs = map (assocs G) bsa
-                  \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bsa)"
+    and r2[rule_format]: "\<forall>as bsa. ys = map (assocs G) as \<and> map (assocs G) bs = map (assocs G) bsa
+      \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bsa)"
     and p3: "map (assocs G) as <~~> map (assocs G) bs"
 
-  from p1
-      have "mset (map (assocs G) as) = mset ys"
-      by (simp add: mset_eq_perm del: mset_map)
-  hence setys: "set (map (assocs G) as) = set ys" by (rule mset_eq_setD)
-
-  have "set (map (assocs G) as) = { assocs G x | x. x \<in> set as}" by clarsimp fast
+  from p1 have "mset (map (assocs G) as) = mset ys"
+    by (simp add: mset_eq_perm del: mset_map)
+  then have setys: "set (map (assocs G) as) = set ys"
+    by (rule mset_eq_setD)
+
+  have "set (map (assocs G) as) = {assocs G x | x. x \<in> set as}" by auto
   with setys have "set ys \<subseteq> { assocs G x | x. x \<in> set as}" by simp
-  hence "\<exists>yy. ys = map (assocs G) yy"
-    apply (induct ys, simp, clarsimp)
+  then have "\<exists>yy. ys = map (assocs G) yy"
+    apply (induct ys)
+     apply simp
+    apply clarsimp
   proof -
     fix yy x
-    show "\<exists>yya. (assocs G x) # map (assocs G) yy =
-                map (assocs G) yya"
-    by (rule exI[of _ "x#yy"], simp)
+    show "\<exists>yya. (assocs G x) # map (assocs G) yy = map (assocs G) yya"
+      by (rule exI[of _ "x#yy"]) simp
   qed
-  from this obtain yy
-      where ys: "ys = map (assocs G) yy"
-      by auto
-
-  from p1 ys
-      have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) yy"
-      by (intro r1, simp)
-  from this obtain as'
-      where asas': "as <~~> as'"
-      and as'yy: "map (assocs G) as' = map (assocs G) yy"
-      by auto
-
-  from p2 ys
-      have "\<exists>as'. yy <~~> as' \<and> map (assocs G) as' = map (assocs G) bs"
-      by (intro r2, simp)
-  from this 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 "\<exists>cs. as' <~~> cs \<and> map (assocs G) cs = map (assocs G) as''"
-      by (rule perm_map_switch)
-  from this 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
-  from ascs and this
-  show "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs" by fast
+  then obtain yy where ys: "ys = map (assocs G) yy"
+    by auto
+
+  from p1 ys have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) yy"
+    by (intro r1) simp
+  then obtain as' where asas': "as <~~> as'" and as'yy: "map (assocs G) as' = map (assocs G) yy"
+    by auto
+
+  from p2 ys have "\<exists>as'. yy <~~> as' \<and> map (assocs G) as' = map (assocs G) bs"
+    by (intro r2) simp
+  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 "\<exists>cs. as' <~~> cs \<and> 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 "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs" by fast
 qed
 
 lemma (in comm_monoid_cancel) fmset_ee:
@@ -1977,48 +1800,42 @@
     and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
   shows "essentially_equal G as bs"
 proof -
-  from mset
-      have mpp: "map (assocs G) as <~~> map (assocs G) bs"
-      by (simp add: fmset_def mset_eq_perm del: mset_map)
+  from mset have mpp: "map (assocs G) as <~~> map (assocs G) bs"
+    by (simp add: fmset_def mset_eq_perm del: mset_map)
 
   have "\<exists>cas. cas = map (assocs G) as" by simp
-  from this obtain cas where cas: "cas = map (assocs G) as" by simp
+  then obtain cas where cas: "cas = map (assocs G) as" by simp
 
   have "\<exists>cbs. cbs = map (assocs G) bs" by simp
-  from this obtain cbs where cbs: "cbs = map (assocs G) bs" by simp
-
-  from cas cbs mpp
-      have [rule_format]:
-           "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and> 
-                     cbs = map (assocs G) bs) 
-                     \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)"
-      by (intro fmset_ee__hlp_induct, simp+)
-  with mpp cas cbs
-      have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs"
-      by simp
-
-  from this obtain as'
-      where tp: "as <~~> as'"
-      and tm: "map (assocs G) as' = map (assocs G) bs"
-      by auto
-  from tm have lene: "length as' = length bs" by (rule map_eq_imp_length_eq)
-  from tp have "set as = set as'" by (simp add: mset_eq_perm mset_eq_setD)
-  with ascarr
-      have as'carr: "set as' \<subseteq> carrier G" by simp
+  then obtain cbs where cbs: "cbs = map (assocs G) bs" by simp
+
+  from cas cbs mpp have [rule_format]:
+    "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and> cbs = map (assocs G) bs)
+      \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)"
+    by (intro fmset_ee__hlp_induct, simp+)
+  with mpp cas cbs have "\<exists>as'. as <~~> as' \<and> 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"
+    by auto
+  from tm have lene: "length as' = length bs"
+    by (rule map_eq_imp_length_eq)
+  from tp have "set as = set as'"
+    by (simp add: mset_eq_perm mset_eq_setD)
+  with ascarr have as'carr: "set as' \<subseteq> carrier G"
+    by simp
 
   from tm as'carr[THEN subsetD] bscarr[THEN subsetD]
   have "as' [\<sim>] bs"
     by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym])
-
-  from tp and this
-    show "essentially_equal G as bs" by (fast intro: essentially_equalI)
+  with tp show "essentially_equal G as bs"
+    by (fast intro: essentially_equalI)
 qed
 
 lemma (in comm_monoid_cancel) ee_is_fmset:
   assumes "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
   shows "essentially_equal G as bs = (fmset G as = fmset G bs)"
-using assms
-by (fast intro: ee_fmset fmset_ee)
+  using assms by (fast intro: ee_fmset fmset_ee)
 
 
 subsubsection \<open>Interpreting multisets as factorizations\<close>
@@ -2028,105 +1845,90 @@
   shows "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> fmset G cs = Cs"
 proof -
   have "\<exists>Cs'. Cs = mset Cs'"
-      by (rule surjE[OF surj_mset], fast)
-  from this obtain Cs'
-      where Cs: "Cs = mset Cs'"
-      by auto
+    by (rule surjE[OF surj_mset], fast)
+  then obtain Cs' where Cs: "Cs = mset Cs'"
+    by auto
 
   have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> mset (map (assocs G) cs) = Cs"
-  using elems
-  unfolding Cs
+    using elems
+    unfolding Cs
     apply (induct Cs', simp)
   proof (clarsimp simp del: mset_map)
-    fix a Cs' cs 
+    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
-        have "\<exists>x. P x \<and> a = assocs G x" by fast
-    from this 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" by simp
-    from mset a
-    have "mset (map (assocs G) (c#cs)) = add_mset a (mset Cs')" by simp
-    from tP this
-    show "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and>
-               mset (map (assocs G) cs) =
-               add_mset a (mset Cs')" by fast
+    from ih have "\<exists>x. P x \<and> 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: "\<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
-  thus ?thesis by (simp add: fmset_def)
+  then show ?thesis by (simp add: fmset_def)
 qed
 
 lemma (in monoid) mset_wfactorsEx:
-  assumes elems: "\<And>X. X \<in> set_mset Cs 
-                      \<Longrightarrow> \<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"
+  assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"
   shows "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = Cs"
 proof -
   have "\<exists>cs. (\<forall>c\<in>set cs. c \<in> carrier G \<and> irreducible G c) \<and> fmset G cs = Cs"
-      by (intro mset_fmsetEx, rule elems)
-  from this obtain cs
-      where p[rule_format]: "\<forall>c\<in>set cs. c \<in> carrier G \<and> irreducible G c"
-      and Cs[symmetric]: "fmset G cs = Cs"
-      by auto
-
-  from p
-      have cscarr: "set cs \<subseteq> carrier G" by fast
-
-  from p
-      have "\<exists>c. c \<in> carrier G \<and> wfactors G cs c"
-      by (intro wfactors_prod_exists) fast+
-  from this obtain c
-      where ccarr: "c \<in> carrier G"
-      and cfs: "wfactors G cs c"
-      by auto
-
-  with cscarr Cs
-      show ?thesis by fast
+    by (intro mset_fmsetEx, rule elems)
+  then obtain cs where p[rule_format]: "\<forall>c\<in>set cs. c \<in> carrier G \<and> irreducible G c"
+    and Cs[symmetric]: "fmset G cs = Cs" by auto
+
+  from p have cscarr: "set cs \<subseteq> carrier G" by fast
+  from p have "\<exists>c. c \<in> carrier G \<and> wfactors G cs c"
+    by (intro wfactors_prod_exists) auto
+  then obtain c where ccarr: "c \<in> carrier G" and cfs: "wfactors G cs c" by auto
+  with cscarr Cs show ?thesis by fast
 qed
 
 
 subsubsection \<open>Multiplication on multisets\<close>
 
 lemma (in factorial_monoid) mult_wfactors_fmset:
-  assumes afs: "wfactors G as a" and bfs: "wfactors G bs b" and cfs: "wfactors G cs (a \<otimes> b)"
+  assumes afs: "wfactors G as a"
+    and bfs: "wfactors G bs b"
+    and cfs: "wfactors G cs (a \<otimes> b)"
     and carr: "a \<in> carrier G"  "b \<in> carrier G"
               "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"  "set cs \<subseteq> carrier G"
   shows "fmset G cs = fmset G as + fmset G bs"
 proof -
-  from assms
-       have "wfactors G (as @ bs) (a \<otimes> b)" by (intro wfactors_mult)
-  with carr cfs
-       have "essentially_equal G cs (as@bs)" by (intro ee_wfactorsI[of "a\<otimes>b" "a\<otimes>b"], simp+)
-  with carr
-       have "fmset G cs = fmset G (as@bs)" by (intro ee_fmset, simp+)
-  also have "fmset G (as@bs) = fmset G as + fmset G bs" by (simp add: fmset_def)
+  from assms have "wfactors G (as @ bs) (a \<otimes> b)"
+    by (intro wfactors_mult)
+  with carr cfs have "essentially_equal G cs (as@bs)"
+    by (intro ee_wfactorsI[of "a\<otimes>b" "a\<otimes>b"]) simp_all
+  with carr have "fmset G cs = fmset G (as@bs)"
+    by (intro ee_fmset) simp_all
+  also have "fmset G (as@bs) = fmset G as + fmset G bs"
+    by (simp add: fmset_def)
   finally show "fmset G cs = fmset G as + fmset G bs" .
 qed
 
 lemma (in factorial_monoid) mult_factors_fmset:
-  assumes afs: "factors G as a" and bfs: "factors G bs b" and cfs: "factors G cs (a \<otimes> b)"
+  assumes afs: "factors G as a"
+    and bfs: "factors G bs b"
+    and cfs: "factors G cs (a \<otimes> b)"
     and "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"  "set cs \<subseteq> carrier G"
   shows "fmset G cs = fmset G as + fmset G bs"
-using assms
-by (blast intro: factors_wfactors mult_wfactors_fmset)
+  using assms by (blast intro: factors_wfactors mult_wfactors_fmset)
 
 lemma (in comm_monoid_cancel) fmset_wfactors_mult:
   assumes mset: "fmset G cs = fmset G as + fmset G bs"
     and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
-          "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"  "set cs \<subseteq> carrier G"
+      "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"  "set cs \<subseteq> carrier G"
     and fs: "wfactors G as a"  "wfactors G bs b"  "wfactors G cs c"
   shows "c \<sim> a \<otimes> b"
 proof -
-  from carr fs
-       have m: "wfactors G (as @ bs) (a \<otimes> b)" by (intro wfactors_mult)
-
-  from mset
-       have "fmset G cs = fmset G (as@bs)" by (simp add: fmset_def)
-  then have "essentially_equal G cs (as@bs)" by (rule fmset_ee) (simp add: carr)+
-  then show "c \<sim> a \<otimes> b" by (rule ee_wfactorsD[of "cs" "as@bs"]) (simp add: assms m)+
+  from carr fs have m: "wfactors G (as @ bs) (a \<otimes> b)"
+    by (intro wfactors_mult)
+
+  from mset have "fmset G cs = fmset G (as@bs)"
+    by (simp add: fmset_def)
+  then have "essentially_equal G cs (as@bs)"
+    by (rule fmset_ee) (simp_all add: carr)
+  then show "c \<sim> a \<otimes> b"
+    by (rule ee_wfactorsD[of "cs" "as@bs"]) (simp_all add: assms m)
 qed
 
 
@@ -2134,32 +1936,34 @@
 
 lemma (in factorial_monoid) divides_fmsubset:
   assumes ab: "a divides b"
-    and afs: "wfactors G as a" and bfs: "wfactors G bs b"
+    and afs: "wfactors G as a"
+    and bfs: "wfactors G bs b"
     and carr: "a \<in> carrier G"  "b \<in> carrier G"  "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
   shows "fmset G as \<le># fmset G bs"
-using ab
+  using ab
 proof (elim dividesE)
   fix c
   assume ccarr: "c \<in> carrier G"
-  hence "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" by (rule wfactors_exist)
-  from this obtain cs 
-      where cscarr: "set cs \<subseteq> carrier G"
-      and cfs: "wfactors G cs c" by auto
+  then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c"
+    by (rule wfactors_exist)
+  then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"
+    by auto
   note carr = carr ccarr cscarr
 
   assume "b = a \<otimes> c"
-  with afs bfs cfs carr
-      have "fmset G bs = fmset G as + fmset G cs"
-      by (intro mult_wfactors_fmset[OF afs cfs]) simp+
-
-  thus ?thesis by simp
+  with afs bfs cfs carr have "fmset G bs = fmset G as + fmset G cs"
+    by (intro mult_wfactors_fmset[OF afs cfs]) simp_all
+  then show ?thesis by simp
 qed
 
 lemma (in comm_monoid_cancel) fmsubset_divides:
   assumes msubset: "fmset G as \<le># fmset G bs"
-    and afs: "wfactors G as a" and bfs: "wfactors G bs b"
-    and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
-    and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
+    and afs: "wfactors G as a"
+    and bfs: "wfactors G bs b"
+    and acarr: "a \<in> carrier G"
+    and bcarr: "b \<in> carrier G"
+    and ascarr: "set as \<subseteq> carrier G"
+    and bscarr: "set bs \<subseteq> carrier G"
   shows "a divides b"
 proof -
   from afs have airr: "\<forall>a \<in> set as. irreducible G a" by (fast elim: wfactorsE)
@@ -2169,48 +1973,46 @@
   proof (intro mset_wfactorsEx, simp)
     fix X
     assume "X \<in># fmset G bs - fmset G as"
-    hence "X \<in># fmset G bs" by (rule in_diffD)
-    hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
-    hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct bs) auto
-    from this obtain x
-        where xbs: "x \<in> set bs"
-        and X: "X = assocs G x"
-        by auto
-
+    then have "X \<in># fmset G bs" by (rule in_diffD)
+    then have "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
+    then have "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct bs) auto
+    then obtain x where xbs: "x \<in> set bs" and X: "X = assocs G x" by auto
     with bscarr have xcarr: "x \<in> carrier G" by fast
     from xbs birr have xirr: "irreducible G x" by simp
 
-    from xcarr and xirr and X
-        show "\<exists>x. x \<in> carrier G \<and> irreducible G x \<and> X = assocs G x" by fast
+    from xcarr and xirr and X show "\<exists>x. x \<in> carrier G \<and> irreducible G x \<and> X = assocs G x"
+      by fast
   qed
-  from this obtain c cs
-      where ccarr: "c \<in> carrier G"
-      and cscarr: "set cs \<subseteq> carrier G" 
+  then obtain c cs
+    where ccarr: "c \<in> carrier G"
+      and cscarr: "set cs \<subseteq> carrier G"
       and csf: "wfactors G cs c"
       and csmset: "fmset G cs = fmset G bs - fmset G as" by auto
 
   from csmset msubset
-      have "fmset G bs = fmset G as + fmset G cs"
-      by (simp add: multiset_eq_iff subseteq_mset_def)
-  hence basc: "b \<sim> a \<otimes> c"
-      by (rule fmset_wfactors_mult) fact+
-
-  thus ?thesis
+  have "fmset G bs = fmset G as + fmset G cs"
+    by (simp add: multiset_eq_iff subseteq_mset_def)
+  then have basc: "b \<sim> a \<otimes> c"
+    by (rule fmset_wfactors_mult) fact+
+  then show ?thesis
   proof (elim associatedE2)
     fix u
     assume "u \<in> Units G"  "b = a \<otimes> c \<otimes> u"
-    with acarr ccarr
-        show "a divides b" by (fast intro: dividesI[of "c \<otimes> u"] m_assoc)
-  qed (simp add: acarr bcarr ccarr)+
+    with acarr ccarr show "a divides b"
+      by (fast intro: dividesI[of "c \<otimes> u"] m_assoc)
+  qed (simp_all add: acarr bcarr ccarr)
 qed
 
 lemma (in factorial_monoid) divides_as_fmsubset:
-  assumes "wfactors G as a" and "wfactors G bs b"
-    and "a \<in> carrier G" and "b \<in> carrier G" 
-    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
+  assumes "wfactors G as a"
+    and "wfactors G bs b"
+    and "a \<in> carrier G"
+    and "b \<in> carrier G"
+    and "set as \<subseteq> carrier G"
+    and "set bs \<subseteq> carrier G"
   shows "a divides b = (fmset G as \<le># fmset G bs)"
-using assms
-by (blast intro: divides_fmsubset fmsubset_divides)
+  using assms
+  by (blast intro: divides_fmsubset fmsubset_divides)
 
 
 text \<open>Proper factors on multisets\<close>
@@ -2218,35 +2020,41 @@
 lemma (in factorial_monoid) fmset_properfactor:
   assumes asubb: "fmset G as \<le># fmset G bs"
     and anb: "fmset G as \<noteq> fmset G bs"
-    and "wfactors G as a" and "wfactors G bs b"
-    and "a \<in> carrier G" and "b \<in> carrier G"
-    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
+    and "wfactors G as a"
+    and "wfactors G bs b"
+    and "a \<in> carrier G"
+    and "b \<in> carrier G"
+    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+)
+  apply (rule properfactorI)
+   apply (rule fmsubset_divides[of as bs], fact+)
 proof
   assume "b divides a"
-  hence "fmset G bs \<le># 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" ..
+  then have "fmset G bs \<le># 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 ..
 qed
 
 lemma (in factorial_monoid) properfactor_fmset:
   assumes pf: "properfactor G a b"
-    and "wfactors G as a" and "wfactors G bs b"
-    and "a \<in> carrier G" and "b \<in> carrier G"
-    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
+    and "wfactors G as a"
+    and "wfactors G bs b"
+    and "a \<in> carrier G"
+    and "b \<in> carrier G"
+    and "set as \<subseteq> carrier G"
+    and "set bs \<subseteq> carrier G"
   shows "fmset G as \<le># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
-using pf
-apply (elim properfactorE)
-apply rule
- apply (intro divides_fmsubset, assumption)
-  apply (rule assms)+
-apply (metis assms divides_fmsubset fmsubset_divides)
-done
+  using pf
+  apply (elim properfactorE)
+  apply rule
+   apply (intro divides_fmsubset, assumption)
+        apply (rule assms)+
+  using assms(2,3,4,6,7) divides_as_fmsubset
+  apply auto
+  done
 
 subsection \<open>Irreducible Elements are Prime\<close>
 
@@ -2254,88 +2062,78 @@
   assumes pirr: "irreducible G p"
     and pcarr: "p \<in> carrier G"
   shows "prime G p"
-using pirr
+  using pirr
 proof (elim irreducibleE, intro primeI)
   fix a b
   assume acarr: "a \<in> carrier G"  and bcarr: "b \<in> carrier G"
     and pdvdab: "p divides (a \<otimes> b)"
     and pnunit: "p \<notin> Units G"
   assume irreduc[rule_format]:
-         "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"
+    "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"
   from pdvdab
-      have "\<exists>c\<in>carrier G. a \<otimes> b = p \<otimes> c" by (rule dividesD)
-  from this obtain c
-      where ccarr: "c \<in> carrier G"
-      and abpc: "a \<otimes> b = p \<otimes> c"
-      by auto
-
-  from acarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a" by (rule wfactors_exist)
-  from this obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a" by auto
-
-  from bcarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs b" by (rule wfactors_exist)
-  from this obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b" by auto
-
-  from ccarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs c" by (rule wfactors_exist)
-  from this obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c" by auto
+  have "\<exists>c\<in>carrier G. a \<otimes> b = p \<otimes> c" by (rule dividesD)
+  then obtain c where ccarr: "c \<in> carrier G" and abpc: "a \<otimes> b = p \<otimes> c"
+    by auto
+
+  from acarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a"
+    by (rule wfactors_exist)
+  then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
+    by auto
+
+  from bcarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs b"
+    by (rule wfactors_exist)
+  then obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b"
+    by auto
+
+  from ccarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs c"
+    by (rule wfactors_exist)
+  then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"
+    by auto
 
   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)"
-      by (rule wfactors_unique) simp+
-
-  hence "\<exists>ds. p # cs <~~> ds \<and> ds [\<sim>] (as @ bs)"
-      by (fast elim: essentially_equalE)
-  from this obtain ds
-      where "p # cs <~~> ds"
-      and dsassoc: "ds [\<sim>] (as @ bs)"
-      by auto
-
+  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)"
+    by (rule wfactors_unique) simp+
+
+  then have "\<exists>ds. p # cs <~~> ds \<and> ds [\<sim>] (as @ bs)"
+    by (fast elim: essentially_equalE)
+  then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)"
+    by auto
   then have "p \<in> set ds"
-       by (simp add: perm_set_eq[symmetric])
-  with dsassoc
-       have "\<exists>p'. p' \<in> set (as@bs) \<and> p \<sim> p'"
-       unfolding list_all2_conv_all_nth set_conv_nth
-       by force
-
-  from this obtain p'
-       where "p' \<in> set (as@bs)"
-       and pp': "p \<sim> p'"
-       by auto
-
-  hence "p' \<in> set as \<or> p' \<in> set bs" by simp
-  moreover
-  {
-    assume p'elem: "p' \<in> set as"
+    by (simp add: perm_set_eq[symmetric])
+  with dsassoc have "\<exists>p'. p' \<in> set (as@bs) \<and> p \<sim> p'"
+    unfolding list_all2_conv_all_nth set_conv_nth by force
+  then obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'"
+    by auto
+  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
-  }
-  moreover
-  {
-    assume p'elem: "p' \<in> set bs"
+    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
-  }
-  ultimately
-      show "p divides a \<or> p divides b" by fast
+    have "p' divides b" by (rule wfactors_dividesI) fact+
+    finally have "p divides b" by simp
+    then show ?thesis ..
+  qed
 qed
 
 
@@ -2344,145 +2142,121 @@
   assumes pirr: "irreducible G p"
     and pcarr: "p \<in> carrier G"
   shows "prime G p"
-using pirr
-apply (elim irreducibleE, intro primeI)
- apply assumption
+  using pirr
+  apply (elim irreducibleE, intro primeI)
+   apply assumption
 proof -
   fix a b
-  assume acarr: "a \<in> carrier G" 
+  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
-      have "\<exists>c\<in>carrier G. a \<otimes> b = p \<otimes> c" by (rule dividesD)
-  from this obtain c
-      where ccarr: "c \<in> carrier G"
-      and abpc: "a \<otimes> b = p \<otimes> c"
-      by auto
+  assume irreduc[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"
+  from pdvdab have "\<exists>c\<in>carrier G. a \<otimes> b = p \<otimes> c"
+    by (rule dividesD)
+  then obtain c where ccarr: "c \<in> carrier G" and abpc: "a \<otimes> b = p \<otimes> c"
+    by auto
   note [simp] = pcarr acarr bcarr ccarr
 
   show "p divides a \<or> p divides b"
   proof (cases "a \<in> Units G")
-    assume aunit: "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
-    thus "p divides a \<or> p divides b" ..
+    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
-    assume anunit: "a \<notin> Units G"
-
-    show "p divides a \<or> p divides b"
+    case anunit: False
+    show ?thesis
     proof (cases "b \<in> Units G")
-      assume bunit: "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
-      thus "p divides a \<or> p divides b" ..
+      have baa: "a \<otimes> b \<sim> a"
+        by (intro associatedI2[of "b"], simp+)
+      finally have "p divides a" by simp
+      then show ?thesis ..
     next
-      assume bnunit: "b \<notin> Units G"
-
+      case bnunit: False
       have cnunit: "c \<notin> Units G"
       proof (rule ccontr, simp)
         assume cunit: "c \<in> Units G"
-        from bnunit
-             have "properfactor G a (a \<otimes> b)"
-             by (intro properfactorI3[of _ _ b], simp+)
+        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" ..
+        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 abunit: "a \<otimes> b \<in> Units G"
-        hence "a \<in> Units G" by (rule unit_factor) fact+
-        with anunit
-             show "False" ..
+        assume "a \<otimes> b \<in> Units G"
+        then have "a \<in> Units G" by (rule unit_factor) fact+
+        with anunit show False ..
       qed
 
-      from acarr anunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" by (rule factors_exist)
-      then obtain as where ascarr: "set as \<subseteq> carrier G" and afac: "factors G as a" by auto
-
-      from bcarr bnunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs b" by (rule factors_exist)
-      then obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfac: "factors G bs b" by auto
-
-      from ccarr cnunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs c" by (rule factors_exist)
-      then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfac: "factors G cs c" by auto
+      from acarr anunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a"
+        by (rule factors_exist)
+      then obtain as where ascarr: "set as \<subseteq> carrier G" and afac: "factors G as a"
+        by auto
+
+      from bcarr bnunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs b"
+        by (rule factors_exist)
+      then obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfac: "factors G bs b"
+        by auto
+
+      from ccarr cnunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs c"
+        by (rule factors_exist)
+      then 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)+
-
-      hence "\<exists>ds. p # cs <~~> ds \<and> ds [\<sim>] (as @ bs)"
-          by (fast elim: essentially_equalE)
-      from this obtain ds
-          where "p # cs <~~> ds"
-          and dsassoc: "ds [\<sim>] (as @ bs)"
-          by auto
-
+      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 have "\<exists>ds. p # cs <~~> ds \<and> ds [\<sim>] (as @ bs)"
+        by (fast elim: essentially_equalE)
+      then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)"
+        by auto
       then have "p \<in> set ds"
-           by (simp add: perm_set_eq[symmetric])
-      with dsassoc
-           have "\<exists>p'. p' \<in> set (as@bs) \<and> p \<sim> p'"
-           unfolding list_all2_conv_all_nth set_conv_nth
-           by force
-
-      from this obtain p'
-          where "p' \<in> set (as@bs)"
-          and pp': "p \<sim> p'" by auto
-
-      hence "p' \<in> set as \<or> p' \<in> set bs" by simp
-      moreover
-      {
-        assume p'elem: "p' \<in> set as"
+        by (simp add: perm_set_eq[symmetric])
+      with dsassoc have "\<exists>p'. p' \<in> set (as@bs) \<and> p \<sim> p'"
+        unfolding list_all2_conv_all_nth set_conv_nth by force
+      then obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'"
+        by auto
+      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 p'elem
-             have "p' divides a" by (rule factors_dividesI) fact+
-        finally
-             have "p divides a" by simp
-      }
-      moreover
-      {
-        assume p'elem: "p' \<in> set bs"
+        also from afac 1 have "p' divides a" by (rule factors_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 bfac
-             have "p' divides b" by (rule factors_dividesI) fact+
+        have "p' divides b" by (rule factors_dividesI) fact+
         finally have "p divides b" by simp
-      }
-      ultimately
-          show "p divides a \<or> p divides b" by fast
+        then show ?thesis ..
+      qed
     qed
   qed
 qed
@@ -2492,39 +2266,31 @@
 
 subsubsection \<open>Definitions\<close>
 
-definition
-  isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ gcdof\<index> _ _)" [81,81,81] 80)
+definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ gcdof\<index> _ _)" [81,81,81] 80)
   where "x gcdof\<^bsub>G\<^esub> a b \<longleftrightarrow> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and>
     (\<forall>y\<in>carrier G. (y divides\<^bsub>G\<^esub> a \<and> y divides\<^bsub>G\<^esub> b \<longrightarrow> y divides\<^bsub>G\<^esub> x))"
 
-definition
-  islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ lcmof\<index> _ _)" [81,81,81] 80)
+definition islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ lcmof\<index> _ _)" [81,81,81] 80)
   where "x lcmof\<^bsub>G\<^esub> a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and>
     (\<forall>y\<in>carrier G. (a divides\<^bsub>G\<^esub> y \<and> b divides\<^bsub>G\<^esub> y \<longrightarrow> x divides\<^bsub>G\<^esub> y))"
 
-definition
-  somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+definition somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   where "somegcd G a b = (SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b)"
 
-definition
-  somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+definition somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   where "somelcm G a b = (SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b)"
 
-definition
-  "SomeGcd G A = inf (division_rel G) A"
+definition "SomeGcd G A = inf (division_rel G) A"
 
 
 locale gcd_condition_monoid = comm_monoid_cancel +
-  assumes gcdof_exists:
-          "\<lbrakk>a \<in> carrier G; b \<in> carrier G\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> carrier G \<and> c gcdof a b"
+  assumes gcdof_exists: "\<lbrakk>a \<in> carrier G; b \<in> carrier G\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> carrier G \<and> c gcdof a b"
 
 locale primeness_condition_monoid = comm_monoid_cancel +
-  assumes irreducible_prime:
-          "\<lbrakk>a \<in> carrier G; irreducible G a\<rbrakk> \<Longrightarrow> prime G a"
+  assumes irreducible_prime: "\<lbrakk>a \<in> carrier G; irreducible G a\<rbrakk> \<Longrightarrow> prime G a"
 
 locale divisor_chain_condition_monoid = comm_monoid_cancel +
-  assumes division_wellfounded:
-          "wf {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}"
+  assumes division_wellfounded: "wf {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}"
 
 
 subsubsection \<open>Connections to \texttt{Lattice.thy}\<close>
@@ -2532,222 +2298,208 @@
 lemma gcdof_greatestLower:
   fixes G (structure)
   assumes carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
-  shows "(x \<in> carrier G \<and> x gcdof a b) =
-         greatest (division_rel G) x (Lower (division_rel G) {a, b})"
-unfolding isgcd_def greatest_def Lower_def elem_def
-by auto
+  shows "(x \<in> carrier G \<and> x gcdof a b) = greatest (division_rel G) x (Lower (division_rel G) {a, b})"
+  by (auto simp: isgcd_def greatest_def Lower_def elem_def)
 
 lemma lcmof_leastUpper:
   fixes G (structure)
   assumes carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
-  shows "(x \<in> carrier G \<and> x lcmof a b) =
-         least (division_rel G) x (Upper (division_rel G) {a, b})"
-unfolding islcm_def least_def Upper_def elem_def
-by auto
+  shows "(x \<in> carrier G \<and> x lcmof a b) = least (division_rel G) x (Upper (division_rel G) {a, b})"
+  by (auto simp: islcm_def least_def Upper_def elem_def)
 
 lemma somegcd_meet:
   fixes G (structure)
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "somegcd G a b = meet (division_rel G) a b"
-unfolding somegcd_def meet_def inf_def
-by (simp add: gcdof_greatestLower[OF carr])
+  by (simp add: somegcd_def meet_def inf_def gcdof_greatestLower[OF carr])
 
 lemma (in monoid) isgcd_divides_l:
   assumes "a divides b"
     and "a \<in> carrier G"  "b \<in> carrier G"
   shows "a gcdof a b"
-using assms
-unfolding isgcd_def
-by fast
+  using assms unfolding isgcd_def by fast
 
 lemma (in monoid) isgcd_divides_r:
   assumes "b divides a"
     and "a \<in> carrier G"  "b \<in> carrier G"
   shows "b gcdof a b"
-using assms
-unfolding isgcd_def
-by fast
+  using assms unfolding isgcd_def by fast
 
 
 subsubsection \<open>Existence of gcd and lcm\<close>
 
 lemma (in factorial_monoid) gcdof_exists:
-  assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
+  assumes acarr: "a \<in> carrier G"
+    and bcarr: "b \<in> carrier G"
   shows "\<exists>c. c \<in> carrier G \<and> c gcdof a b"
 proof -
   from acarr have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by (rule wfactors_exist)
-  from this obtain as
-      where ascarr: "set as \<subseteq> carrier G"
-      and afs: "wfactors G as a"
-      by auto
-  from afs have airr: "\<forall>a \<in> set as. irreducible G a" by (fast elim: wfactorsE)
-
-  from bcarr have "\<exists>bs. set bs \<subseteq> carrier G \<and> wfactors G bs b" by (rule wfactors_exist)
-  from this obtain bs
-      where bscarr: "set bs \<subseteq> carrier G"
-      and bfs: "wfactors G bs b"
-      by auto
-  from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" by (fast elim: wfactorsE)
-
-  have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> 
-               fmset G cs = fmset G as #\<inter> fmset G bs"
+  then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
+    by auto
+  from afs have airr: "\<forall>a \<in> set as. irreducible G a"
+    by (fast elim: wfactorsE)
+
+  from bcarr have "\<exists>bs. set bs \<subseteq> carrier G \<and> wfactors G bs b"
+    by (rule wfactors_exist)
+  then obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b"
+    by auto
+  from bfs have birr: "\<forall>b \<in> set bs. irreducible G b"
+    by (fast elim: wfactorsE)
+
+  have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and>
+    fmset G cs = fmset G as #\<inter> fmset G bs"
   proof (intro mset_wfactorsEx)
     fix X
     assume "X \<in># fmset G as #\<inter> fmset G bs"
-    hence "X \<in># fmset G as" by simp
-    hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
-    hence "\<exists>x. X = assocs G x \<and> x \<in> set as" by (induct as) auto
-    from this obtain x
-        where X: "X = assocs G x"
-        and xas: "x \<in> set as"
-        by auto
-    with ascarr have xcarr: "x \<in> carrier G" by fast
-    from xas airr have xirr: "irreducible G x" by simp
- 
-    from xcarr and xirr and X
-        show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast
+    then have "X \<in># fmset G as" by simp
+    then have "X \<in> set (map (assocs G) as)"
+      by (simp add: fmset_def)
+    then have "\<exists>x. X = assocs G x \<and> x \<in> set as"
+      by (induct as) auto
+    then obtain x where X: "X = assocs G x" and xas: "x \<in> set as"
+      by auto
+    with ascarr have xcarr: "x \<in> carrier G"
+      by fast
+    from xas airr have xirr: "irreducible G x"
+      by simp
+    from xcarr and xirr and X show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"
+      by fast
   qed
-
-  from this obtain c cs
-      where ccarr: "c \<in> carrier G"
-      and cscarr: "set cs \<subseteq> carrier G" 
+  then obtain c cs
+    where ccarr: "c \<in> carrier G"
+      and cscarr: "set cs \<subseteq> carrier G"
       and csirr: "wfactors G cs c"
-      and csmset: "fmset G cs = fmset G as #\<inter> fmset G bs" by auto
+      and csmset: "fmset G cs = fmset G as #\<inter> fmset G bs"
+    by auto
 
   have "c gcdof a b"
   proof (simp add: isgcd_def, safe)
     from csmset
-        have "fmset G cs \<le># fmset G as"
-        by (simp add: multiset_inter_def subset_mset_def)
-    thus "c divides a" by (rule fmsubset_divides) fact+
+    have "fmset G cs \<le># fmset G as"
+      by (simp add: multiset_inter_def subset_mset_def)
+    then show "c divides a" by (rule fmsubset_divides) fact+
   next
-    from csmset
-        have "fmset G cs \<le># fmset G bs"
-        by (simp add: multiset_inter_def subseteq_mset_def, force)
-    thus "c divides b" by (rule fmsubset_divides) fact+
+    from csmset have "fmset G cs \<le># fmset G bs"
+      by (simp add: multiset_inter_def subseteq_mset_def, force)
+    then show "c divides b"
+      by (rule fmsubset_divides) fact+
   next
     fix y
     assume ycarr: "y \<in> carrier G"
-    hence "\<exists>ys. set ys \<subseteq> carrier G \<and> wfactors G ys y" by (rule wfactors_exist)
-    from this obtain ys
-        where yscarr: "set ys \<subseteq> carrier G"
-        and yfs: "wfactors G ys y"
-        by auto
+    then have "\<exists>ys. set ys \<subseteq> carrier G \<and> wfactors G ys y"
+      by (rule wfactors_exist)
+    then obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"
+      by auto
 
     assume "y divides a"
-    hence ya: "fmset G ys \<le># fmset G as" by (rule divides_fmsubset) fact+
+    then have ya: "fmset G ys \<le># fmset G as"
+      by (rule divides_fmsubset) fact+
 
     assume "y divides b"
-    hence yb: "fmset G ys \<le># fmset G bs" by (rule divides_fmsubset) fact+
-
-    from ya yb csmset
-    have "fmset G ys \<le># fmset G cs" by (simp add: subset_mset_def)
-    thus "y divides c" by (rule fmsubset_divides) fact+
+    then have yb: "fmset G ys \<le># fmset G bs"
+      by (rule divides_fmsubset) fact+
+
+    from ya yb csmset have "fmset G ys \<le># fmset G cs"
+      by (simp add: subset_mset_def)
+    then show "y divides c"
+      by (rule fmsubset_divides) fact+
   qed
-
-  with ccarr
-      show "\<exists>c. c \<in> carrier G \<and> c gcdof a b" by fast
+  with ccarr show "\<exists>c. c \<in> carrier G \<and> c gcdof a b"
+    by fast
 qed
 
 lemma (in factorial_monoid) lcmof_exists:
-  assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
+  assumes acarr: "a \<in> carrier G"
+    and bcarr: "b \<in> carrier G"
   shows "\<exists>c. c \<in> carrier G \<and> c lcmof a b"
 proof -
-  from acarr have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by (rule wfactors_exist)
-  from this obtain as
-      where ascarr: "set as \<subseteq> carrier G"
-      and afs: "wfactors G as a"
-      by auto
-  from afs have airr: "\<forall>a \<in> set as. irreducible G a" by (fast elim: wfactorsE)
-
-  from bcarr have "\<exists>bs. set bs \<subseteq> carrier G \<and> wfactors G bs b" by (rule wfactors_exist)
-  from this obtain bs
-      where bscarr: "set bs \<subseteq> carrier G"
-      and bfs: "wfactors G bs b"
-      by auto
-  from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" by (fast elim: wfactorsE)
-
-  have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> 
-               fmset G cs = (fmset G as - fmset G bs) + fmset G bs"
+  from acarr have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"
+    by (rule wfactors_exist)
+  then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
+    by auto
+  from afs have airr: "\<forall>a \<in> set as. irreducible G a"
+    by (fast elim: wfactorsE)
+
+  from bcarr have "\<exists>bs. set bs \<subseteq> carrier G \<and> wfactors G bs b"
+    by (rule wfactors_exist)
+  then obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b"
+    by auto
+  from bfs have birr: "\<forall>b \<in> set bs. irreducible G b"
+    by (fast elim: wfactorsE)
+
+  have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and>
+    fmset G cs = (fmset G as - fmset G bs) + fmset G bs"
   proof (intro mset_wfactorsEx)
     fix X
     assume "X \<in># (fmset G as - fmset G bs) + fmset G bs"
-    hence "X \<in># fmset G as \<or> X \<in># fmset G bs"
+    then have "X \<in># fmset G as \<or> X \<in># fmset G bs"
       by (auto dest: in_diffD)
-    moreover
-    {
-      assume "X \<in> set_mset (fmset G as)"
-      hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
-      hence "\<exists>x. x \<in> set as \<and> X = assocs G x" by (induct as) auto
-      from this obtain x
-          where xas: "x \<in> set as"
-          and X: "X = assocs G x" by auto
-
+    then consider "X \<in> set_mset (fmset G as)" | "X \<in> set_mset (fmset G bs)"
+      by fast
+    then show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"
+    proof cases
+      case 1
+      then have "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
+      then have "\<exists>x. x \<in> set as \<and> X = assocs G x" by (induct as) auto
+      then obtain x where xas: "x \<in> set as" and X: "X = assocs G x" by auto
       with ascarr have xcarr: "x \<in> carrier G" by fast
       from xas airr have xirr: "irreducible G x" by simp
-
-      from xcarr and xirr and X
-          have "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast
-    }
-    moreover
-    {
-      assume "X \<in> set_mset (fmset G bs)"
-      hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
-      hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct as) auto
-      from this obtain x
-          where xbs: "x \<in> set bs"
-          and X: "X = assocs G x" by auto
-
+      from xcarr and xirr and X show ?thesis by fast
+    next
+      case 2
+      then have "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
+      then have "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct as) auto
+      then obtain x where xbs: "x \<in> set bs" and X: "X = assocs G x" by auto
       with bscarr have xcarr: "x \<in> carrier G" by fast
       from xbs birr have xirr: "irreducible G x" by simp
-
-      from xcarr and xirr and X
-          have "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast
-    }
-    ultimately
-    show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast
+      from xcarr and xirr and X show ?thesis by fast
+    qed
   qed
-
-  from this obtain c cs
-      where ccarr: "c \<in> carrier G"
-      and cscarr: "set cs \<subseteq> carrier G" 
+  then obtain c cs
+    where ccarr: "c \<in> carrier G"
+      and cscarr: "set cs \<subseteq> carrier G"
       and csirr: "wfactors G cs c"
-      and csmset: "fmset G cs = fmset G as - fmset G bs + fmset G bs" by auto
+      and csmset: "fmset G cs = fmset G as - fmset G bs + fmset G bs"
+    by auto
 
   have "c lcmof a b"
   proof (simp add: islcm_def, safe)
-    from csmset have "fmset G as \<le># fmset G cs" by (simp add: subseteq_mset_def, force)
-    thus "a divides c" by (rule fmsubset_divides) fact+
+    from csmset have "fmset G as \<le># fmset G cs"
+      by (simp add: subseteq_mset_def, force)
+    then show "a divides c"
+      by (rule fmsubset_divides) fact+
   next
-    from csmset have "fmset G bs \<le># fmset G cs" by (simp add: subset_mset_def)
-    thus "b divides c" by (rule fmsubset_divides) fact+
+    from csmset have "fmset G bs \<le># fmset G cs"
+      by (simp add: subset_mset_def)
+    then show "b divides c"
+      by (rule fmsubset_divides) fact+
   next
     fix y
     assume ycarr: "y \<in> carrier G"
-    hence "\<exists>ys. set ys \<subseteq> carrier G \<and> wfactors G ys y" by (rule wfactors_exist)
-    from this obtain ys
-        where yscarr: "set ys \<subseteq> carrier G"
-        and yfs: "wfactors G ys y"
-        by auto
+    then have "\<exists>ys. set ys \<subseteq> carrier G \<and> wfactors G ys y"
+      by (rule wfactors_exist)
+    then obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"
+      by auto
 
     assume "a divides y"
-    hence ya: "fmset G as \<le># fmset G ys" by (rule divides_fmsubset) fact+
+    then have ya: "fmset G as \<le># fmset G ys"
+      by (rule divides_fmsubset) fact+
 
     assume "b divides y"
-    hence yb: "fmset G bs \<le># fmset G ys" by (rule divides_fmsubset) fact+
-
-    from ya yb csmset
-    have "fmset G cs \<le># fmset G ys"
+    then have yb: "fmset G bs \<le># fmset G ys"
+      by (rule divides_fmsubset) fact+
+
+    from ya yb csmset have "fmset G cs \<le># fmset G ys"
       apply (simp add: subseteq_mset_def, clarify)
       apply (case_tac "count (fmset G as) a < count (fmset G bs) a")
        apply simp
       apply simp
-    done
-    thus "c divides y" by (rule fmsubset_divides) fact+
+      done
+    then show "c divides y"
+      by (rule fmsubset_divides) fact+
   qed
-
-  with ccarr
-      show "\<exists>c. c \<in> carrier G \<and> c lcmof a b" by fast
+  with ccarr show "\<exists>c. c \<in> carrier G \<and> c lcmof a b"
+    by fast
 qed
 
 
@@ -2756,23 +2508,21 @@
 subsubsection \<open>Gcd condition\<close>
 
 lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
-  shows "weak_lower_semilattice (division_rel G)"
+  "weak_lower_semilattice (division_rel G)"
 proof -
   interpret weak_partial_order "division_rel G" ..
   show ?thesis
-  apply (unfold_locales, simp_all)
+    apply (unfold_locales, simp_all)
   proof -
     fix x y
     assume carr: "x \<in> carrier G"  "y \<in> carrier G"
-    hence "\<exists>z. z \<in> carrier G \<and> z gcdof x y" by (rule gcdof_exists)
-    from this obtain z
-        where zcarr: "z \<in> carrier G"
-        and isgcd: "z gcdof x y"
-        by auto
-    with carr
-    have "greatest (division_rel G) z (Lower (division_rel G) {x, y})"
-        by (subst gcdof_greatestLower[symmetric], simp+)
-    thus "\<exists>z. greatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast
+    then have "\<exists>z. z \<in> carrier G \<and> z gcdof x y" by (rule gcdof_exists)
+    then obtain z where zcarr: "z \<in> carrier G" and isgcd: "z gcdof x y"
+      by auto
+    with carr have "greatest (division_rel G) z (Lower (division_rel G) {x, y})"
+      by (subst gcdof_greatestLower[symmetric], simp+)
+    then show "\<exists>z. greatest (division_rel G) z (Lower (division_rel G) {x, y})"
+      by fast
   qed
 qed
 
@@ -2787,13 +2537,13 @@
   have "a' \<in> carrier G \<and> a' gcdof b c"
     apply (simp add: gcdof_greatestLower carr')
     apply (subst greatest_Lower_cong_l[of _ a])
-       apply (simp add: a'a)
+        apply (simp add: a'a)
+       apply (simp add: carr)
       apply (simp add: carr)
      apply (simp add: carr)
-    apply (simp add: carr)
     apply (simp add: gcdof_greatestLower[symmetric] agcd carr)
-  done
-  thus ?thesis ..
+    done
+  then show ?thesis ..
 qed
 
 lemma (in gcd_condition_monoid) gcd_closed [simp]:
@@ -2804,28 +2554,30 @@
   show ?thesis
     apply (simp add: somegcd_meet[OF carr])
     apply (rule meet_closed[simplified], fact+)
-  done
+    done
 qed
 
 lemma (in gcd_condition_monoid) gcd_isgcd:
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "(somegcd G a b) gcdof a b"
 proof -
-  interpret weak_lower_semilattice "division_rel G" by simp
-  from carr
-  have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
+  interpret weak_lower_semilattice "division_rel G"
+    by simp
+  from carr have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
     apply (subst gcdof_greatestLower, simp, simp)
     apply (simp add: somegcd_meet[OF carr] meet_def)
     apply (rule inf_of_two_greatest[simplified], assumption+)
-  done
-  thus "(somegcd G a b) gcdof a b" by simp
+    done
+  then show "(somegcd G a b) gcdof a b"
+    by simp
 qed
 
 lemma (in gcd_condition_monoid) gcd_exists:
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "\<exists>x\<in>carrier G. x = somegcd G a b"
 proof -
-  interpret weak_lower_semilattice "division_rel G" by simp
+  interpret weak_lower_semilattice "division_rel G"
+    by simp
   show ?thesis
     by (metis carr(1) carr(2) gcd_closed)
 qed
@@ -2834,7 +2586,8 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "(somegcd G a b) divides a"
 proof -
-  interpret weak_lower_semilattice "division_rel G" by simp
+  interpret weak_lower_semilattice "division_rel G"
+    by simp
   show ?thesis
     by (metis carr(1) carr(2) gcd_isgcd isgcd_def)
 qed
@@ -2843,7 +2596,8 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "(somegcd G a b) divides b"
 proof -
-  interpret weak_lower_semilattice "division_rel G" by simp
+  interpret weak_lower_semilattice "division_rel G"
+    by simp
   show ?thesis
     by (metis carr gcd_isgcd isgcd_def)
 qed
@@ -2853,7 +2607,8 @@
     and L: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   shows "z divides (somegcd G x y)"
 proof -
-  interpret weak_lower_semilattice "division_rel G" by simp
+  interpret weak_lower_semilattice "division_rel G"
+    by simp
   show ?thesis
     by (metis gcd_isgcd isgcd_def assms)
 qed
@@ -2863,11 +2618,12 @@
     and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   shows "somegcd G x y \<sim> somegcd G x' y"
 proof -
-  interpret weak_lower_semilattice "division_rel G" by simp
+  interpret weak_lower_semilattice "division_rel G"
+    by simp
   show ?thesis
     apply (simp add: somegcd_meet carr)
     apply (rule meet_cong_l[simplified], fact+)
-  done
+    done
 qed
 
 lemma (in gcd_condition_monoid) gcd_cong_r:
@@ -2879,7 +2635,7 @@
   show ?thesis
     apply (simp add: somegcd_meet carr)
     apply (rule meet_cong_r[simplified], fact+)
-  done
+    done
 qed
 
 (*
@@ -2897,7 +2653,7 @@
 unfolding CONG_def
 by clarsimp (blast intro: gcd_cong_r)
 
-lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] = 
+lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] =
     assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r]
 *)
 
@@ -2906,43 +2662,42 @@
     and others: "\<forall>y\<in>carrier G. y divides b \<and> y divides c \<longrightarrow> y divides a"
     and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"
   shows "a \<sim> somegcd G b c"
-apply (simp add: somegcd_def)
-apply (rule someI2_ex)
- apply (rule exI[of _ a], simp add: isgcd_def)
- apply (simp add: assms)
-apply (simp add: isgcd_def assms, clarify)
-apply (insert assms, blast intro: associatedI)
-done
+  apply (simp add: somegcd_def)
+  apply (rule someI2_ex)
+   apply (rule exI[of _ a], simp add: isgcd_def)
+   apply (simp add: assms)
+  apply (simp add: isgcd_def assms, clarify)
+  apply (insert assms, blast intro: associatedI)
+  done
 
 lemma (in gcd_condition_monoid) gcdI2:
-  assumes "a gcdof b c"
-    and "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"
+  assumes "a gcdof b c" and "a \<in> carrier G" and "b \<in> carrier G" and "c \<in> carrier G"
   shows "a \<sim> somegcd G b c"
-using assms
-unfolding isgcd_def
-by (blast intro: gcdI)
+  using assms unfolding isgcd_def by (blast intro: gcdI)
 
 lemma (in gcd_condition_monoid) SomeGcd_ex:
   assumes "finite A"  "A \<subseteq> carrier G"  "A \<noteq> {}"
   shows "\<exists>x\<in> carrier G. x = SomeGcd G A"
 proof -
-  interpret weak_lower_semilattice "division_rel G" by simp
+  interpret weak_lower_semilattice "division_rel G"
+    by simp
   show ?thesis
     apply (simp add: SomeGcd_def)
     apply (rule finite_inf_closed[simplified], fact+)
-  done
+    done
 qed
 
 lemma (in gcd_condition_monoid) gcd_assoc:
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"
 proof -
-  interpret weak_lower_semilattice "division_rel G" by simp
+  interpret weak_lower_semilattice "division_rel G"
+    by simp
   show ?thesis
     apply (subst (2 3) somegcd_meet, (simp add: carr)+)
     apply (simp add: somegcd_meet carr)
     apply (rule weak_meet_assoc[simplified], fact+)
-  done
+    done
 qed
 
 lemma (in gcd_condition_monoid) gcd_mult:
@@ -2957,59 +2712,53 @@
   note carr = carr dcarr ecarr
 
   have "?d divides a" by (simp add: gcd_divides_l)
-  hence cd'ca: "c \<otimes> ?d divides (c \<otimes> a)" by (simp add: divides_mult_lI)
+  then have cd'ca: "c \<otimes> ?d divides (c \<otimes> a)" by (simp add: divides_mult_lI)
 
   have "?d divides b" by (simp add: gcd_divides_r)
-  hence cd'cb: "c \<otimes> ?d divides (c \<otimes> b)" by (simp add: divides_mult_lI)
-  
-  from cd'ca cd'cb
-      have cd'e: "c \<otimes> ?d divides ?e"
-      by (rule gcd_divides) simp+
-
-  hence "\<exists>u. u \<in> carrier G \<and> ?e = c \<otimes> ?d \<otimes> u"
-      by (elim dividesE, fast)
-  from this obtain u
-      where ucarr[simp]: "u \<in> carrier G"
-      and e_cdu: "?e = c \<otimes> ?d \<otimes> u"
-      by auto
+  then have cd'cb: "c \<otimes> ?d divides (c \<otimes> b)" by (simp add: divides_mult_lI)
+
+  from cd'ca cd'cb have cd'e: "c \<otimes> ?d divides ?e"
+    by (rule gcd_divides) simp_all
+  then have "\<exists>u. u \<in> carrier G \<and> ?e = c \<otimes> ?d \<otimes> u"
+    by (elim dividesE) fast
+  then obtain u where ucarr[simp]: "u \<in> carrier G" and e_cdu: "?e = c \<otimes> ?d \<otimes> u"
+    by auto
 
   note carr = carr ucarr
 
-  have "?e divides c \<otimes> a" by (rule gcd_divides_l) simp+
-  hence "\<exists>x. x \<in> carrier G \<and> c \<otimes> a = ?e \<otimes> x"
-      by (elim dividesE, fast)
-  from this obtain x
-      where xcarr: "x \<in> carrier G"
-      and ca_ex: "c \<otimes> a = ?e \<otimes> x"
-      by auto
-  with e_cdu
-      have ca_cdux: "c \<otimes> a = c \<otimes> ?d \<otimes> u \<otimes> x" by simp
-
-  from ca_cdux xcarr
-       have "c \<otimes> a = c \<otimes> (?d \<otimes> u \<otimes> x)" by (simp add: m_assoc)
-  then have "a = ?d \<otimes> u \<otimes> x" by (rule l_cancel[of c a]) (simp add: xcarr)+
-  hence du'a: "?d \<otimes> u divides a" by (rule dividesI[OF xcarr])
-
-  have "?e divides c \<otimes> b" by (intro gcd_divides_r, simp+)
-  hence "\<exists>x. x \<in> carrier G \<and> c \<otimes> b = ?e \<otimes> x"
-      by (elim dividesE, fast)
-  from this obtain x
-      where xcarr: "x \<in> carrier G"
-      and cb_ex: "c \<otimes> b = ?e \<otimes> x"
-      by auto
-  with e_cdu
-      have cb_cdux: "c \<otimes> b = c \<otimes> ?d \<otimes> u \<otimes> x" by simp
-
-  from cb_cdux xcarr
-      have "c \<otimes> b = c \<otimes> (?d \<otimes> u \<otimes> x)" by (simp add: m_assoc)
-  with xcarr
-      have "b = ?d \<otimes> u \<otimes> x" by (intro l_cancel[of c b], simp+)
-  hence du'b: "?d \<otimes> u divides b" by (intro dividesI[OF xcarr])
-
-  from du'a du'b carr
-      have du'd: "?d \<otimes> u divides ?d"
-      by (intro gcd_divides, simp+)
-  hence uunit: "u \<in> Units G"
+  have "?e divides c \<otimes> a" by (rule gcd_divides_l) simp_all
+  then have "\<exists>x. x \<in> carrier G \<and> c \<otimes> a = ?e \<otimes> x"
+    by (elim dividesE) fast
+  then obtain x where xcarr: "x \<in> carrier G" and ca_ex: "c \<otimes> a = ?e \<otimes> x"
+    by auto
+  with e_cdu have ca_cdux: "c \<otimes> a = c \<otimes> ?d \<otimes> u \<otimes> x"
+    by simp
+
+  from ca_cdux xcarr have "c \<otimes> a = c \<otimes> (?d \<otimes> u \<otimes> x)"
+    by (simp add: m_assoc)
+  then have "a = ?d \<otimes> u \<otimes> x"
+    by (rule l_cancel[of c a]) (simp add: xcarr)+
+  then have du'a: "?d \<otimes> u divides a"
+    by (rule dividesI[OF xcarr])
+
+  have "?e divides c \<otimes> b" by (intro gcd_divides_r) simp_all
+  then have "\<exists>x. x \<in> carrier G \<and> c \<otimes> b = ?e \<otimes> x"
+    by (elim dividesE) fast
+  then obtain x where xcarr: "x \<in> carrier G" and cb_ex: "c \<otimes> b = ?e \<otimes> x"
+    by auto
+  with e_cdu have cb_cdux: "c \<otimes> b = c \<otimes> ?d \<otimes> u \<otimes> x"
+    by simp
+
+  from cb_cdux xcarr have "c \<otimes> b = c \<otimes> (?d \<otimes> u \<otimes> x)"
+    by (simp add: m_assoc)
+  with xcarr have "b = ?d \<otimes> u \<otimes> x"
+    by (intro l_cancel[of c b]) simp_all
+  then have du'b: "?d \<otimes> u divides b"
+    by (intro dividesI[OF xcarr])
+
+  from du'a du'b carr have du'd: "?d \<otimes> u divides ?d"
+    by (intro gcd_divides) simp_all
+  then have uunit: "u \<in> Units G"
   proof (elim dividesE)
     fix v
     assume vcarr[simp]: "v \<in> carrier G"
@@ -3017,108 +2766,100 @@
     have "?d \<otimes> \<one> = ?d \<otimes> u \<otimes> v" by simp fact
     also have "?d \<otimes> u \<otimes> v = ?d \<otimes> (u \<otimes> v)" by (simp add: m_assoc)
     finally have "?d \<otimes> \<one> = ?d \<otimes> (u \<otimes> v)" .
-    hence i2: "\<one> = u \<otimes> v" by (rule l_cancel) simp+
-    hence i1: "\<one> = v \<otimes> u" by (simp add: m_comm)
-    from vcarr i1[symmetric] i2[symmetric]
-        show "u \<in> Units G"
-        by (unfold Units_def, simp, fast)
+    then have i2: "\<one> = u \<otimes> v" by (rule l_cancel) simp_all
+    then have i1: "\<one> = v \<otimes> u" by (simp add: m_comm)
+    from vcarr i1[symmetric] i2[symmetric] show "u \<in> Units G"
+      by (auto simp: Units_def)
   qed
 
-  from e_cdu uunit
-      have "somegcd G (c \<otimes> a) (c \<otimes> b) \<sim> c \<otimes> somegcd G a b"
-      by (intro associatedI2[of u], simp+)
-  from this[symmetric]
-      show "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" by simp
+  from e_cdu uunit have "somegcd G (c \<otimes> a) (c \<otimes> b) \<sim> c \<otimes> somegcd G a b"
+    by (intro associatedI2[of u]) simp_all
+  from this[symmetric] show "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"
+    by simp
 qed
 
 lemma (in monoid) assoc_subst:
   assumes ab: "a \<sim> b"
-    and cP: "ALL a b. a : carrier G & b : carrier G & a \<sim> b
-      --> f a : carrier G & f b : carrier G & f a \<sim> f b"
+    and cP: "\<forall>a b. a \<in> carrier G \<and> b \<in> carrier G \<and> a \<sim> b
+      \<longrightarrow> f a \<in> carrier G \<and> f b \<in> carrier G \<and> f a \<sim> f b"
     and carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "f a \<sim> f b"
   using assms by auto
 
 lemma (in gcd_condition_monoid) relprime_mult:
-  assumes abrelprime: "somegcd G a b \<sim> \<one>" and acrelprime: "somegcd G a c \<sim> \<one>"
+  assumes abrelprime: "somegcd G a b \<sim> \<one>"
+    and acrelprime: "somegcd G a c \<sim> \<one>"
     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "somegcd G a (b \<otimes> c) \<sim> \<one>"
 proof -
   have "c = c \<otimes> \<one>" by simp
   also from abrelprime[symmetric]
-       have "\<dots> \<sim> c \<otimes> somegcd G a b"
-         by (rule assoc_subst) (simp add: mult_cong_r)+
-  also have "\<dots> \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" by (rule gcd_mult) fact+
-  finally
-       have c: "c \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" by simp
-
-  from carr
-       have a: "a \<sim> somegcd G a (c \<otimes> a)"
-       by (fast intro: gcdI divides_prod_l)
-
-  have "somegcd G a (b \<otimes> c) \<sim> somegcd G a (c \<otimes> b)" by (simp add: m_comm)
-  also from a
-       have "\<dots> \<sim> somegcd G (somegcd G a (c \<otimes> a)) (c \<otimes> b)"
-         by (rule assoc_subst) (simp add: gcd_cong_l)+
-  also from gcd_assoc
-       have "\<dots> \<sim> somegcd G a (somegcd G (c \<otimes> a) (c \<otimes> b))"
-       by (rule assoc_subst) simp+
-  also from c[symmetric]
-       have "\<dots> \<sim> somegcd G a c"
-         by (rule assoc_subst) (simp add: gcd_cong_r)+
+  have "\<dots> \<sim> c \<otimes> somegcd G a b"
+    by (rule assoc_subst) (simp add: mult_cong_r)+
+  also have "\<dots> \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"
+    by (rule gcd_mult) fact+
+  finally have c: "c \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"
+    by simp
+
+  from carr have a: "a \<sim> somegcd G a (c \<otimes> a)"
+    by (fast intro: gcdI divides_prod_l)
+
+  have "somegcd G a (b \<otimes> c) \<sim> somegcd G a (c \<otimes> b)"
+    by (simp add: m_comm)
+  also from a have "\<dots> \<sim> somegcd G (somegcd G a (c \<otimes> a)) (c \<otimes> b)"
+    by (rule assoc_subst) (simp add: gcd_cong_l)+
+  also from gcd_assoc have "\<dots> \<sim> somegcd G a (somegcd G (c \<otimes> a) (c \<otimes> b))"
+    by (rule assoc_subst) simp+
+  also from c[symmetric] have "\<dots> \<sim> somegcd G a c"
+    by (rule assoc_subst) (simp add: gcd_cong_r)+
   also note acrelprime
-  finally
-       show "somegcd G a (b \<otimes> c) \<sim> \<one>" by simp
+  finally show "somegcd G a (b \<otimes> c) \<sim> \<one>"
+    by simp
 qed
 
-lemma (in gcd_condition_monoid) primeness_condition:
-  "primeness_condition_monoid G"
-apply unfold_locales
-apply (rule primeI)
- apply (elim irreducibleE, assumption)
+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)+
+  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)
+    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 (rule ccontr, simp)
       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+
-    with pcarr acarr
-        have pa: "somegcd G p a \<sim> \<one>" by (fast intro: associated_sym[of "\<one>"] gcd_closed)
+      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)
+    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 (rule ccontr, simp)
       fix y
       assume ycarr: "y \<in> carrier G"
@@ -3126,24 +2867,22 @@
       also assume "y divides b"
       finally have "p divides b" by (simp add: pcarr ycarr bcarr)
       with npdvdb
-          show "False" ..
-    qed simp+
-    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" ..
+      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 ..
   qed
 qed
 
@@ -3158,86 +2897,70 @@
   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)"
-    apply (rule wf_induct[OF division_wellfounded])
-  proof -
+  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)
+      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"
-      hence "\<exists>y. y \<in> carrier G \<and> properfactor G y x \<and> y \<notin> Units G"
-        apply - apply (rule ccontr, simp)
+      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
-      from this obtain y
-          where ycarr: "y \<in> carrier G"
-          and ynunit: "y \<notin> Units G"
-          and pfyx: "properfactor G y x"
-          by auto
-
-      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 ycarr pfyx
-          have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y"
-          by (rule ih')
-      from this obtain ys
-          where yscarr: "set ys \<subseteq> carrier G"
-          and yfs: "wfactors G ys y"
-          by auto
-
-      from pfyx
-          have "y divides x"
-          and nyx: "\<not> y \<sim> x"
-          by - (fast elim: properfactorE2)+
-      hence "\<exists>z. z \<in> carrier G \<and> x = y \<otimes> z"
-          by fast
-
-      from this obtain z
-          where zcarr: "z \<in> carrier G"
-          and x: "x = y \<otimes> z"
-          by auto
-
-      from zcarr ycarr
-      have "properfactor G z x"
+        done
+      then obtain y where ycarr: "y \<in> carrier G" and ynunit: "y \<notin> Units G"
+        and pfyx: "properfactor G y x"
+        by auto
+
+      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 ycarr pfyx have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y"
+        by (rule ih')
+      then obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"
+        by auto
+
+      from pfyx have "y divides x" and nyx: "\<not> y \<sim> x"
+        by (fast elim: properfactorE2)+
+      then have "\<exists>z. z \<in> carrier G \<and> x = y \<otimes> z"
+        by fast
+      then obtain z where zcarr: "z \<in> carrier G" and x: "x = y \<otimes> z"
+        by auto
+
+      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
-      with zcarr
-          have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as z"
-          by (rule ih')
-      from this obtain zs
-          where zscarr: "set zs \<subseteq> carrier G"
-          and zfs: "wfactors G zs z"
-          by auto
-
-      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)
-      hence "wfactors G (ys@zs) x" by (simp add: x)
-
-      from xscarr this
-          show "\<exists>xs. set xs \<subseteq> carrier G \<and> wfactors G xs x" by fast
+            apply (simp add: m_comm)
+           apply (simp add: ynunit)+
+        done
+      with zcarr have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as z"
+        by (rule ih')
+      then obtain zs where zscarr: "set zs \<subseteq> carrier G" and zfs: "wfactors G zs z"
+        by auto
+
+      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
     qed
   qed
-
-  from acarr
-      show ?thesis by (rule r)
+  from acarr show ?thesis by (rule r)
 qed
 
 
@@ -3249,56 +2972,50 @@
     and "a divides (foldr (op \<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 (op \<otimes>) as \<one>)
-        \<longrightarrow> (\<exists>i. i < length as \<and> a divides (as!i))"
+  have r[rule_format]: "set as \<subseteq> carrier G \<and> a divides (foldr (op \<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)
+    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 op \<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 op \<otimes> as \<one>"
-    with carr aprime
-        have "a divides aa \<or> a divides foldr op \<otimes> as \<one>"
-        by (intro prime_divides) simp+
-    moreover {
+    with carr aprime have "a divides aa \<or> a divides foldr op \<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"
-      hence p1: "a divides (aa#as)!0" by simp
+      then have p1: "a divides (aa#as)!0" by simp
       have "0 < Suc (length as)" by simp
-      with p1 have "\<exists>i<Suc (length as). a divides (aa # as) ! i" by fast
-    }
-    moreover {
+      with p1 show ?thesis by fast
+    next
       assume "a divides foldr op \<otimes> as \<one>"
-      hence "\<exists>i. i < length as \<and> a divides as ! i" by (rule ih)
-      from this obtain i where "a divides as ! i" and len: "i < length as" by auto
-      hence p1: "a divides (aa#as) ! (Suc i)" by simp
+      then have "\<exists>i. i < length as \<and> a divides as ! i" by (rule ih)
+      then 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 have "\<exists>i<Suc (length as). a divides (aa # as) ! i" by force
-   }
-   ultimately
-      show "\<exists>i<Suc (length as). a divides (aa # as) ! i" by fast
+      with p1 show ?thesis by force
+   qed
   qed
-
-  from assms
-      show ?thesis
-      by (intro r, safe)
+  from assms show ?thesis
+    by (intro r) auto
 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> 
+  "\<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 apply auto
-  proof -
+  case Nil
+  show ?case
+  proof auto
     fix a as'
     assume a: "a \<in> carrier G"
     assume "wfactors G [] a"
@@ -3310,56 +3027,55 @@
     then show "essentially_equal G [] as'" by simp
   qed
 next
-  case (Cons ah as) then show ?case apply clarsimp 
-  proof -
+  case (Cons ah as)
+  then show ?case
+  proof clarsimp
     fix a as'
-    assume ih [rule_format]: 
+    assume ih [rule_format]:
       "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and>
         wfactors G as' a \<longrightarrow> essentially_equal G as as'"
       and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"
       and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"
       and afs: "wfactors G (ah # as) a"
       and afs': "wfactors G as' a"
-    hence ahdvda: "ah divides a"
+    then have ahdvda: "ah divides a"
       by (intro wfactors_dividesI[of "ah#as" "a"], simp+)
-    hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by fast
-    from this obtain a'
-      where a'carr: "a' \<in> carrier G"
-      and a: "a = ah \<otimes> a'"
+    then have "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by fast
+    then obtain a' where a'carr: "a' \<in> carrier G" and a: "a = ah \<otimes> a'"
       by auto
     have a'fs: "wfactors G as a'"
       apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
       apply (simp add: a, insert ascarr a'carr)
       apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)
       done
-    from afs have ahirr: "irreducible G ah" by (elim wfactorsE, simp)
-    with ascarr have ahprime: "prime G ah" by (intro irreducible_prime ahcarr)
+    from afs have ahirr: "irreducible G ah"
+      by (elim wfactorsE) simp
+    with ascarr have ahprime: "prime G ah"
+      by (intro irreducible_prime ahcarr)
 
     note carr [simp] = acarr ahcarr ascarr as'carr a'carr
 
     note ahdvda
-    also from afs'
-      have "a divides (foldr (op \<otimes>) as' \<one>)"
+    also from afs' have "a divides (foldr (op \<otimes>) as' \<one>)"
       by (elim wfactorsE associatedE, simp)
-    finally have "ah divides (foldr (op \<otimes>) as' \<one>)" by simp
-
-    with ahprime
-      have "\<exists>i<length as'. ah divides as'!i"
+    finally have "ah divides (foldr (op \<otimes>) as' \<one>)"
+      by simp
+    with ahprime have "\<exists>i<length as'. ah divides as'!i"
       by (intro multlist_prime_pos, simp+)
-    from this obtain i
-      where len: "i<length as'" and ahdvd: "ah divides as'!i"
+    then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i"
       by auto
     from afs' carr have irrasi: "irreducible G (as'!i)"
       by (fast intro: nth_mem[OF len] elim: wfactorsE)
-    from len carr
-      have asicarr[simp]: "as'!i \<in> carrier G" by (unfold set_conv_nth, force)
+    from len carr have asicarr[simp]: "as'!i \<in> carrier G"
+      unfolding set_conv_nth by force
     note carr = carr asicarr
 
-    from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by fast
-    from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto
-
-    with carr irrasi[simplified asi]
-      have asiah: "as'!i \<sim> ah" apply -
+    from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x"
+      by fast
+    then obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"
+      by auto
+    with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah"
+      apply -
       apply (elim irreducible_prodE[of "ah" "x"], assumption+)
        apply (rule associatedI2[of x], assumption+)
       apply (rule irreducibleE[OF ahirr], simp)
@@ -3371,86 +3087,78 @@
 
     have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
       apply (intro wfactors_prod_exists)
-      using setparts afs' by (fast elim: wfactorsE, simp)
-    from this obtain aa_1
-        where aa1carr: "aa_1 \<in> carrier G"
-        and aa1fs: "wfactors G (take i as') aa_1"
-        by auto
+      using setparts afs'
+       apply (fast elim: wfactorsE)
+      apply simp
+      done
+    then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"
+      by auto
 
     have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
       apply (intro wfactors_prod_exists)
-      using setparts afs' by (fast elim: wfactorsE, simp)
-    from this obtain aa_2
-        where aa2carr: "aa_2 \<in> carrier G"
-        and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
-        by auto
+      using setparts afs'
+       apply (fast elim: wfactorsE)
+      apply simp
+      done
+    then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G"
+      and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
+      by auto
 
     note carr = carr aa1carr[simp] aa2carr[simp]
 
     from aa1fs aa2fs
-      have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
+    have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
       by (intro wfactors_mult, simp+)
-    hence v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
+    then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
       apply (intro wfactors_mult_single)
       using setparts afs'
-      by (fast intro: nth_mem[OF len] elim: wfactorsE, simp+)
-
-    from aa2carr carr aa1fs aa2fs
-      have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
-        by (metis irrasi wfactors_mult_single)
+          apply (fast intro: nth_mem[OF len] elim: wfactorsE)
+         apply simp_all
+      done
+
+    from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
+      by (metis irrasi wfactors_mult_single)
     with len carr aa1carr aa2carr aa1fs
-      have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
+    have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
       apply (intro wfactors_mult)
            apply fast
           apply (simp, (fast intro: nth_mem[OF len])?)+
-    done
-
-    from len
-      have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
+      done
+
+    from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
       by (simp add: Cons_nth_drop_Suc)
-    with carr
-      have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
+    with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
       by simp
-    with v2 afs' carr aa1carr aa2carr nth_mem[OF len]
-      have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
-        by (metis as' ee_wfactorsD m_closed)
-    then
-    have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
+    with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
+      by (metis as' ee_wfactorsD m_closed)
+    then have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
       by (metis aa1carr aa2carr asicarr m_lcomm)
-    from carr asiah
-    have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
+    from carr asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
       by (metis associated_sym m_closed mult_cong_l)
     also note t1
-    finally
-      have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
-
-    with carr aa1carr aa2carr a'carr nth_mem[OF len]
-      have a': "aa_1 \<otimes> aa_2 \<sim> a'"
+    finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
+
+    with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'"
       by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])
 
     note v1
     also note a'
-    finally have "wfactors G (take i as' @ drop (Suc i) as') a'" by simp
-
-    from a'fs this carr
-      have "essentially_equal G as (take i as' @ drop (Suc i) as')"
+    finally have "wfactors G (take i as' @ drop (Suc i) as') a'"
+      by simp
+
+    from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')"
       by (intro ih[of a']) simp
-
-    hence ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
-      apply (elim essentially_equalE) apply (fastforce intro: essentially_equalI)
-    done
-
-    from carr
-    have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
+    then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
+      by (elim essentially_equalE) (fastforce intro: essentially_equalI)
+
+    from carr have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
       (as' ! i # take i as' @ drop (Suc i) as')"
     proof (intro essentially_equalI)
       show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
         by simp
     next
       show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"
-      apply (simp add: list_all2_append)
-      apply (simp add: asiah[symmetric])
-      done
+        by (simp add: list_all2_append) (simp add: asiah[symmetric])
     qed
 
     note ee1
@@ -3458,15 +3166,16 @@
     also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
       (take i as' @ as' ! i # drop (Suc i) as')"
       apply (intro essentially_equalI)
-       apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~> 
-        take i as' @ as' ! i # drop (Suc i) as'")
+       apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
+          take i as' @ as' ! i # drop (Suc i) as'")
         apply simp
        apply (rule perm_append_Cons)
       apply simp
       done
-    finally
-      have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" by simp
-    then show "essentially_equal G (ah # as) as'" by (subst as', assumption)
+    finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"
+      by simp
+    then show "essentially_equal G (ah # as) as'"
+      by (subst as')
   qed
 qed
 
@@ -3474,39 +3183,33 @@
   assumes "wfactors G as a"  "wfactors G as' a"
     and "a \<in> carrier G"  "set as \<subseteq> carrier G"  "set as' \<subseteq> carrier G"
   shows "essentially_equal G as as'"
-apply (rule wfactors_unique__hlp_induct[rule_format, of a])
-apply (simp add: assms)
-done
+  by (rule wfactors_unique__hlp_induct[rule_format, of a]) (simp add: assms)
 
 
 subsubsection \<open>Application to factorial monoids\<close>
 
 text \<open>Number of factors for wellfoundedness\<close>
 
-definition
-  factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where
-  "factorcount G a =
-    (THE c. (ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as))"
+definition factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat"
+  where "factorcount G a =
+    (THE c. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as)"
 
 lemma (in monoid) ee_length:
   assumes ee: "essentially_equal G as bs"
   shows "length as = length bs"
-apply (rule essentially_equalE[OF ee])
-apply (metis list_all2_conv_all_nth perm_length)
-done
+  by (rule essentially_equalE[OF ee]) (metis list_all2_conv_all_nth perm_length)
 
 lemma (in factorial_monoid) factorcount_exists:
   assumes carr[simp]: "a \<in> carrier G"
-  shows "EX c. ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as"
+  shows "\<exists>c. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as"
 proof -
-  have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by (intro wfactors_exist, simp)
-  from this obtain as
-      where ascarr[simp]: "set as \<subseteq> carrier G"
-      and afs: "wfactors G as a"
-      by (auto simp del: carr)
-  have "ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'"
+  have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"
+    by (intro wfactors_exist) simp
+  then obtain as where ascarr[simp]: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
+    by (auto simp del: carr)
+  have "\<forall>as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'"
     by (metis afs ascarr assms ee_length wfactors_unique)
-  thus "EX c. ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" ..
+  then show "\<exists>c. \<forall>as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" ..
 qed
 
 lemma (in factorial_monoid) factorcount_unique:
@@ -3514,164 +3217,158 @@
     and acarr[simp]: "a \<in> carrier G" and ascarr[simp]: "set as \<subseteq> carrier G"
   shows "factorcount G a = length as"
 proof -
-  have "EX ac. ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as" by (rule factorcount_exists, simp)
-  from this obtain ac where
-      alen: "ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"
-      by auto
+  have "\<exists>ac. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"
+    by (rule factorcount_exists) simp
+  then obtain ac where alen: "\<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"
+    by auto
   have ac: "ac = factorcount G a"
     apply (simp add: factorcount_def)
     apply (rule theI2)
       apply (rule alen)
      apply (metis afs alen ascarr)+
-  done
-
-  from ascarr afs have "ac = length as" by (iprover intro: alen[rule_format])
-  with ac show ?thesis by simp
+    done
+  from ascarr afs have "ac = length as"
+    by (iprover intro: alen[rule_format])
+  with ac show ?thesis
+    by simp
 qed
 
 lemma (in factorial_monoid) divides_fcount:
   assumes dvd: "a divides b"
-    and acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G"
-  shows "factorcount G a <= factorcount G b"
-apply (rule dividesE[OF dvd])
-proof -
+    and acarr: "a \<in> carrier G"
+    and bcarr:"b \<in> carrier G"
+  shows "factorcount G a \<le> factorcount G b"
+proof (rule dividesE[OF dvd])
   fix c
-  from assms
-      have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by fast
-  from this obtain as
-      where ascarr: "set as \<subseteq> carrier G"
-      and afs: "wfactors G as a"
-      by auto
-  with acarr have fca: "factorcount G a = length as" by (intro factorcount_unique)
+  from assms have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"
+    by fast
+  then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
+    by auto
+  with acarr have fca: "factorcount G a = length as"
+    by (intro factorcount_unique)
 
   assume ccarr: "c \<in> carrier G"
-  hence "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" by fast
-  from this obtain cs
-      where cscarr: "set cs \<subseteq> carrier G"
-      and cfs: "wfactors G cs c"
-      by auto
+  then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c"
+    by fast
+  then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"
+    by auto
 
   note [simp] = acarr bcarr ccarr ascarr cscarr
 
   assume b: "b = a \<otimes> c"
-  from afs cfs
-      have "wfactors G (as@cs) (a \<otimes> c)" by (intro wfactors_mult, simp+)
-  with b have "wfactors G (as@cs) b" by simp
-  hence "factorcount G b = length (as@cs)" by (intro factorcount_unique, simp+)
-  hence "factorcount G b = length as + length cs" by simp
-  with fca show ?thesis by simp
+  from afs cfs have "wfactors G (as@cs) (a \<otimes> c)"
+    by (intro wfactors_mult) simp_all
+  with b have "wfactors G (as@cs) b"
+    by simp
+  then have "factorcount G b = length (as@cs)"
+    by (intro factorcount_unique) simp_all
+  then have "factorcount G b = length as + length cs"
+    by simp
+  with fca show ?thesis
+    by simp
 qed
 
 lemma (in factorial_monoid) associated_fcount:
-  assumes acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G"
+  assumes acarr: "a \<in> carrier G"
+    and bcarr: "b \<in> carrier G"
     and asc: "a \<sim> b"
   shows "factorcount G a = factorcount G b"
-apply (rule associatedE[OF asc])
-apply (drule divides_fcount[OF _ acarr bcarr])
-apply (drule divides_fcount[OF _ bcarr acarr])
-apply simp
-done
+  apply (rule associatedE[OF asc])
+  apply (drule divides_fcount[OF _ acarr bcarr])
+  apply (drule divides_fcount[OF _ bcarr acarr])
+  apply simp
+  done
 
 lemma (in factorial_monoid) properfactor_fcount:
   assumes acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G"
     and pf: "properfactor G a b"
   shows "factorcount G a < factorcount G b"
-apply (rule properfactorE[OF pf], elim dividesE)
-proof -
+proof (rule properfactorE[OF pf], elim dividesE)
   fix c
-  from assms
-  have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by fast
-  from this obtain as
-      where ascarr: "set as \<subseteq> carrier G"
-      and afs: "wfactors G as a"
-      by auto
-  with acarr have fca: "factorcount G a = length as" by (intro factorcount_unique)
+  from assms have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"
+    by fast
+  then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
+    by auto
+  with acarr have fca: "factorcount G a = length as"
+    by (intro factorcount_unique)
 
   assume ccarr: "c \<in> carrier G"
-  hence "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" by fast
-  from this obtain cs
-      where cscarr: "set cs \<subseteq> carrier G"
-      and cfs: "wfactors G cs c"
-      by auto
+  then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c"
+    by fast
+  then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"
+    by auto
 
   assume b: "b = a \<otimes> c"
 
-  have "wfactors G (as@cs) (a \<otimes> c)" by (rule wfactors_mult) fact+
-  with b
-      have "wfactors G (as@cs) b" by simp
-  with ascarr cscarr bcarr
-      have "factorcount G b = length (as@cs)" by (simp add: factorcount_unique)
-  hence fcb: "factorcount G b = length as + length cs" by simp
+  have "wfactors G (as@cs) (a \<otimes> c)"
+    by (rule wfactors_mult) fact+
+  with b have "wfactors G (as@cs) b"
+    by simp
+  with ascarr cscarr bcarr have "factorcount G b = length (as@cs)"
+    by (simp add: factorcount_unique)
+  then have fcb: "factorcount G b = length as + length cs"
+    by simp
 
   assume nbdvda: "\<not> b divides a"
   have "c \<notin> Units G"
   proof (rule ccontr, simp)
     assume cunit:"c \<in> Units G"
-
-    have "b \<otimes> inv c = a \<otimes> c \<otimes> inv c" by (simp add: b)
-    also from ccarr acarr cunit
-        have "\<dots> = a \<otimes> (c \<otimes> inv c)" by (fast intro: m_assoc)
-    also from ccarr cunit
-        have "\<dots> = a \<otimes> \<one>" by simp
-    also from acarr
-        have "\<dots> = a" by simp
+    have "b \<otimes> inv c = a \<otimes> c \<otimes> inv c"
+      by (simp add: b)
+    also from ccarr acarr cunit have "\<dots> = a \<otimes> (c \<otimes> inv c)"
+      by (fast intro: m_assoc)
+    also from ccarr cunit have "\<dots> = a \<otimes> \<one>" by simp
+    also from acarr have "\<dots> = a" by simp
     finally have "a = b \<otimes> inv c" by simp
-    with ccarr cunit
-    have "b divides a" by (fast intro: dividesI[of "inv c"])
+    with ccarr cunit have "b divides a"
+      by (fast intro: dividesI[of "inv c"])
     with nbdvda show False by simp
   qed
-
   with cfs have "length cs > 0"
     apply -
     apply (rule ccontr, simp)
     apply (metis Units_one_closed ccarr cscarr l_one one_closed properfactorI3 properfactor_fmset unit_wfactors)
     done
-  with fca fcb show ?thesis by simp
+  with fca fcb show ?thesis
+    by simp
 qed
 
 sublocale factorial_monoid \<subseteq> divisor_chain_condition_monoid
-apply unfold_locales
-apply (rule wfUNIVI)
-apply (rule measure_induct[of "factorcount G"])
-apply simp
-apply (metis properfactor_fcount)
-done
+  apply unfold_locales
+  apply (rule wfUNIVI)
+  apply (rule measure_induct[of "factorcount G"])
+  apply simp
+  apply (metis properfactor_fcount)
+  done
 
 sublocale factorial_monoid \<subseteq> primeness_condition_monoid
   by standard (rule irreducible_prime)
 
 
-lemma (in factorial_monoid) primeness_condition:
-  shows "primeness_condition_monoid G"
-  ..
-
-lemma (in factorial_monoid) gcd_condition [simp]:
-  shows "gcd_condition_monoid G"
+lemma (in factorial_monoid) primeness_condition: "primeness_condition_monoid G" ..
+
+lemma (in factorial_monoid) gcd_condition [simp]: "gcd_condition_monoid G"
   by standard (rule gcdof_exists)
 
 sublocale factorial_monoid \<subseteq> gcd_condition_monoid
   by standard (rule gcdof_exists)
 
-lemma (in factorial_monoid) division_weak_lattice [simp]:
-  shows "weak_lattice (division_rel G)"
+lemma (in factorial_monoid) division_weak_lattice [simp]: "weak_lattice (division_rel G)"
 proof -
-  interpret weak_lower_semilattice "division_rel G" by simp
-
+  interpret weak_lower_semilattice "division_rel G"
+    by simp
   show "weak_lattice (division_rel G)"
-  apply (unfold_locales, simp_all)
-  proof -
+  proof (unfold_locales, simp_all)
     fix x y
     assume carr: "x \<in> carrier G"  "y \<in> carrier G"
-
-    hence "\<exists>z. z \<in> carrier G \<and> z lcmof x y" by (rule lcmof_exists)
-    from this obtain z
-        where zcarr: "z \<in> carrier G"
-        and isgcd: "z lcmof x y"
-        by auto
-    with carr
-    have "least (division_rel G) z (Upper (division_rel G) {x, y})"
-        by (simp add: lcmof_leastUpper[symmetric])
-    thus "\<exists>z. least (division_rel G) z (Upper (division_rel G) {x, y})" by fast
+    then have "\<exists>z. z \<in> carrier G \<and> z lcmof x y"
+      by (rule lcmof_exists)
+    then obtain z where zcarr: "z \<in> carrier G" and isgcd: "z lcmof x y"
+      by auto
+    with carr have "least (division_rel G) z (Upper (division_rel G) {x, y})"
+      by (simp add: lcmof_leastUpper[symmetric])
+    then show "\<exists>z. least (division_rel G) z (Upper (division_rel G) {x, y})"
+      by fast
   qed
 qed
 
@@ -3679,39 +3376,37 @@
 subsection \<open>Factoriality Theorems\<close>
 
 theorem factorial_condition_one: (* Jacobson theorem 2.21 *)
-  shows "(divisor_chain_condition_monoid G \<and> primeness_condition_monoid G) = 
-         factorial_monoid G"
-apply rule
+  "(divisor_chain_condition_monoid G \<and> primeness_condition_monoid G) = factorial_monoid G"
+  apply rule
 proof clarify
   assume dcc: "divisor_chain_condition_monoid G"
-     and pc: "primeness_condition_monoid G"
+    and pc: "primeness_condition_monoid G"
   interpret divisor_chain_condition_monoid "G" by (rule dcc)
   interpret primeness_condition_monoid "G" by (rule pc)
-
   show "factorial_monoid G"
-      by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)
+    by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)
 next
   assume fm: "factorial_monoid G"
   interpret factorial_monoid "G" by (rule fm)
   show "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G"
-      by rule unfold_locales
+    by rule unfold_locales
 qed
 
 theorem factorial_condition_two: (* Jacobson theorem 2.22 *)
   shows "(divisor_chain_condition_monoid G \<and> gcd_condition_monoid G) = factorial_monoid G"
-apply rule
+  apply rule
 proof clarify
   assume dcc: "divisor_chain_condition_monoid G"
-     and gc: "gcd_condition_monoid G"
+    and gc: "gcd_condition_monoid G"
   interpret divisor_chain_condition_monoid "G" by (rule dcc)
   interpret gcd_condition_monoid "G" by (rule gc)
   show "factorial_monoid G"
-      by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)
+    by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)
 next
   assume fm: "factorial_monoid G"
   interpret factorial_monoid "G" by (rule fm)
   show "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G"
-      by rule unfold_locales
+    by rule unfold_locales
 qed
 
 end