# HG changeset patch
# User wenzelm
# Date 1466451648 -7200
# Node ID 1086d56cde866bd89f3bc11e9197707eb5162405
# Parent  1e98146f3581ce9215180895604249eed992b1ab
misc tuning and modernization;

diff -r 1e98146f3581 -r 1086d56cde86 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Mon Jun 20 17:51:47 2016 +0200
+++ b/src/HOL/Groups.thy	Mon Jun 20 21:40:48 2016 +0200
@@ -13,22 +13,26 @@
 named_theorems ac_simps "associativity and commutativity simplification rules"
 
 
-text\<open>The rewrites accumulated in \<open>algebra_simps\<close> deal with the
-classical algebraic structures of groups, rings and family. They simplify
-terms by multiplying everything out (in case of a ring) and bringing sums and
-products into a canonical form (by ordered rewriting). As a result it decides
-group and ring equalities but also helps with inequalities.
+text \<open>
+  The rewrites accumulated in \<open>algebra_simps\<close> deal with the
+  classical algebraic structures of groups, rings and family. They simplify
+  terms by multiplying everything out (in case of a ring) and bringing sums and
+  products into a canonical form (by ordered rewriting). As a result it decides
+  group and ring equalities but also helps with inequalities.
 
-Of course it also works for fields, but it knows nothing about multiplicative
-inverses or division. This is catered for by \<open>field_simps\<close>.\<close>
+  Of course it also works for fields, but it knows nothing about multiplicative
+  inverses or division. This is catered for by \<open>field_simps\<close>.
+\<close>
 
 named_theorems algebra_simps "algebra simplification rules"
 
 
-text\<open>Lemmas \<open>field_simps\<close> multiply with denominators in (in)equations
-if they can be proved to be non-zero (for equations) or positive/negative
-(for inequations). Can be too aggressive and is therefore separate from the
-more benign \<open>algebra_simps\<close>.\<close>
+text \<open>
+  Lemmas \<open>field_simps\<close> multiply with denominators in (in)equations
+  if they can be proved to be non-zero (for equations) or positive/negative
+  (for inequations). Can be too aggressive and is therefore separate from the
+  more benign \<open>algebra_simps\<close>.
+\<close>
 
 named_theorems field_simps "algebra simplification rules for fields"
 
@@ -42,15 +46,14 @@
 \<close>
 
 locale semigroup =
-  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^bold>*" 70)
+  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^bold>*" 70)
   assumes assoc [ac_simps]: "a \<^bold>* b \<^bold>* c = a \<^bold>* (b \<^bold>* c)"
 
 locale abel_semigroup = semigroup +
   assumes commute [ac_simps]: "a \<^bold>* b = b \<^bold>* a"
 begin
 
-lemma left_commute [ac_simps]:
-  "b \<^bold>* (a \<^bold>* c) = a \<^bold>* (b \<^bold>* c)"
+lemma left_commute [ac_simps]: "b \<^bold>* (a \<^bold>* c) = a \<^bold>* (b \<^bold>* c)"
 proof -
   have "(b \<^bold>* a) \<^bold>* c = (a \<^bold>* b) \<^bold>* c"
     by (simp only: commute)
@@ -238,13 +241,11 @@
   assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
 begin
 
-lemma add_left_cancel [simp]:
-  "a + b = a + c \<longleftrightarrow> b = c"
-by (blast dest: add_left_imp_eq)
+lemma add_left_cancel [simp]: "a + b = a + c \<longleftrightarrow> b = c"
+  by (blast dest: add_left_imp_eq)
 
-lemma add_right_cancel [simp]:
-  "b + a = c + a \<longleftrightarrow> b = c"
-by (blast dest: add_right_imp_eq)
+lemma add_right_cancel [simp]: "b + a = c + a \<longleftrightarrow> b = c"
+  by (blast dest: add_right_imp_eq)
 
 end
 
@@ -253,8 +254,7 @@
   assumes diff_diff_add [algebra_simps, field_simps]: "a - b - c = a - (b + c)"
 begin
 
-lemma add_diff_cancel_right' [simp]:
-  "(a + b) - b = a"
+lemma add_diff_cancel_right' [simp]: "(a + b) - b = a"
   using add_diff_cancel_left' [of b a] by (simp add: ac_simps)
 
 subclass cancel_semigroup_add
@@ -274,16 +274,13 @@
     by simp
 qed
 
-lemma add_diff_cancel_left [simp]:
-  "(c + a) - (c + b) = a - b"
+lemma add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b"
   unfolding diff_diff_add [symmetric] by simp
 
-lemma add_diff_cancel_right [simp]:
-  "(a + c) - (b + c) = a - b"
+lemma add_diff_cancel_right [simp]: "(a + c) - (b + c) = a - b"
   using add_diff_cancel_left [symmetric] by (simp add: ac_simps)
 
-lemma diff_right_commute:
-  "a - c - b = a - b - c"
+lemma diff_right_commute: "a - c - b = a - b - c"
   by (simp add: diff_diff_add add.commute)
 
 end
@@ -291,14 +288,13 @@
 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
 begin
 
-lemma diff_zero [simp]:
-  "a - 0 = a"
+lemma diff_zero [simp]: "a - 0 = a"
   using add_diff_cancel_right' [of a 0] by simp
 
-lemma diff_cancel [simp]:
-  "a - a = 0"
+lemma diff_cancel [simp]: "a - a = 0"
 proof -
-  have "(a + 0) - (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero)
+  have "(a + 0) - (a + 0) = 0"
+    by (simp only: add_diff_cancel_left diff_zero)
   then show ?thesis by simp
 qed
 
@@ -306,29 +302,29 @@
   assumes "c + b = a"
   shows "c = a - b"
 proof -
-  from assms have "(b + c) - (b + 0) = a - b" by (simp add: add.commute)
+  from assms have "(b + c) - (b + 0) = a - b"
+    by (simp add: add.commute)
   then show "c = a - b" by simp
 qed
 
-lemma add_cancel_right_right [simp]:
-  "a = a + b \<longleftrightarrow> b = 0" (is "?P \<longleftrightarrow> ?Q")
+lemma add_cancel_right_right [simp]: "a = a + b \<longleftrightarrow> b = 0"
+  (is "?P \<longleftrightarrow> ?Q")
 proof
-  assume ?Q then show ?P by simp
+  assume ?Q
+  then show ?P by simp
 next
-  assume ?P then have "a - a = a + b - a" by simp
+  assume ?P
+  then have "a - a = a + b - a" by simp
   then show ?Q by simp
 qed
 
-lemma add_cancel_right_left [simp]:
-  "a = b + a \<longleftrightarrow> b = 0"
+lemma add_cancel_right_left [simp]: "a = b + a \<longleftrightarrow> b = 0"
   using add_cancel_right_right [of a b] by (simp add: ac_simps)
 
-lemma add_cancel_left_right [simp]:
-  "a + b = a \<longleftrightarrow> b = 0"
+lemma add_cancel_left_right [simp]: "a + b = a \<longleftrightarrow> b = 0"
   by (auto dest: sym)
 
-lemma add_cancel_left_left [simp]:
-  "b + a = a \<longleftrightarrow> b = 0"
+lemma add_cancel_left_left [simp]: "b + a = a \<longleftrightarrow> b = 0"
   by (auto dest: sym)
 
 end
@@ -337,11 +333,12 @@
   assumes zero_diff [simp]: "0 - a = 0"
 begin
 
-lemma diff_add_zero [simp]:
-  "a - (a + b) = 0"
+lemma diff_add_zero [simp]: "a - (a + b) = 0"
 proof -
-  have "a - (a + b) = (a + 0) - (a + b)" by simp
-  also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff)
+  have "a - (a + b) = (a + 0) - (a + b)"
+    by simp
+  also have "\<dots> = 0"
+    by (simp only: add_diff_cancel_left zero_diff)
   finally show ?thesis .
 qed
 
@@ -355,14 +352,14 @@
   assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"
 begin
 
-lemma diff_conv_add_uminus:
-  "a - b = a + (- b)"
+lemma diff_conv_add_uminus: "a - b = a + (- b)"
   by simp
 
 lemma minus_unique:
-  assumes "a + b = 0" shows "- a = b"
+  assumes "a + b = 0"
+  shows "- a = b"
 proof -
-  have "- a = - a + (a + b)" using assms by simp
+  from assms have "- a = - a + (a + b)" by simp
   also have "\<dots> = b" by (simp add: add.assoc [symmetric])
   finally show ?thesis .
 qed
@@ -370,13 +367,13 @@
 lemma minus_zero [simp]: "- 0 = 0"
 proof -
   have "0 + 0 = 0" by (rule add_0_right)
-  thus "- 0 = 0" by (rule minus_unique)
+  then show "- 0 = 0" by (rule minus_unique)
 qed
 
 lemma minus_minus [simp]: "- (- a) = a"
 proof -
   have "- a + a = 0" by (rule left_minus)
-  thus "- (- a) = a" by (rule minus_unique)
+  then show "- (- a) = a" by (rule minus_unique)
 qed
 
 lemma right_minus: "a + - a = 0"
@@ -386,8 +383,7 @@
   finally show ?thesis .
 qed
 
-lemma diff_self [simp]:
-  "a - a = 0"
+lemma diff_self [simp]: "a - a = 0"
   using right_minus [of a] by simp
 
 subclass cancel_semigroup_add
@@ -404,24 +400,19 @@
   then show "b = c" unfolding add.assoc by simp
 qed
 
-lemma minus_add_cancel [simp]:
-  "- a + (a + b) = b"
+lemma minus_add_cancel [simp]: "- a + (a + b) = b"
   by (simp add: add.assoc [symmetric])
 
-lemma add_minus_cancel [simp]:
-  "a + (- a + b) = b"
+lemma add_minus_cancel [simp]: "a + (- a + b) = b"
   by (simp add: add.assoc [symmetric])
 
-lemma diff_add_cancel [simp]:
-  "a - b + b = a"
+lemma diff_add_cancel [simp]: "a - b + b = a"
   by (simp only: diff_conv_add_uminus add.assoc) simp
 
-lemma add_diff_cancel [simp]:
-  "a + b - b = a"
+lemma add_diff_cancel [simp]: "a + b - b = a"
   by (simp only: diff_conv_add_uminus add.assoc) simp
 
-lemma minus_add:
-  "- (a + b) = - b + - a"
+lemma minus_add: "- (a + b) = - b + - a"
 proof -
   have "(a + b) + (- b + - a) = 0"
     by (simp only: add.assoc add_minus_cancel) simp
@@ -429,117 +420,103 @@
     by (rule minus_unique)
 qed
 
-lemma right_minus_eq [simp]:
-  "a - b = 0 \<longleftrightarrow> a = b"
+lemma right_minus_eq [simp]: "a - b = 0 \<longleftrightarrow> a = b"
 proof
   assume "a - b = 0"
   have "a = (a - b) + b" by (simp add: add.assoc)
   also have "\<dots> = b" using \<open>a - b = 0\<close> by simp
   finally show "a = b" .
 next
-  assume "a = b" thus "a - b = 0" by simp
+  assume "a = b"
+  then show "a - b = 0" by simp
 qed
 
-lemma eq_iff_diff_eq_0:
-  "a = b \<longleftrightarrow> a - b = 0"
+lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
   by (fact right_minus_eq [symmetric])
 
-lemma diff_0 [simp]:
-  "0 - a = - a"
+lemma diff_0 [simp]: "0 - a = - a"
   by (simp only: diff_conv_add_uminus add_0_left)
 
-lemma diff_0_right [simp]:
-  "a - 0 = a"
+lemma diff_0_right [simp]: "a - 0 = a"
   by (simp only: diff_conv_add_uminus minus_zero add_0_right)
 
-lemma diff_minus_eq_add [simp]:
-  "a - - b = a + b"
+lemma diff_minus_eq_add [simp]: "a - - b = a + b"
   by (simp only: diff_conv_add_uminus minus_minus)
 
-lemma neg_equal_iff_equal [simp]:
-  "- a = - b \<longleftrightarrow> a = b"
+lemma neg_equal_iff_equal [simp]: "- a = - b \<longleftrightarrow> a = b"
 proof
   assume "- a = - b"
-  hence "- (- a) = - (- b)" by simp
-  thus "a = b" by simp
+  then have "- (- a) = - (- b)" by simp
+  then show "a = b" by simp
 next
   assume "a = b"
-  thus "- a = - b" by simp
+  then show "- a = - b" by simp
 qed
 
-lemma neg_equal_0_iff_equal [simp]:
-  "- a = 0 \<longleftrightarrow> a = 0"
+lemma neg_equal_0_iff_equal [simp]: "- a = 0 \<longleftrightarrow> a = 0"
   by (subst neg_equal_iff_equal [symmetric]) simp
 
-lemma neg_0_equal_iff_equal [simp]:
-  "0 = - a \<longleftrightarrow> 0 = a"
+lemma neg_0_equal_iff_equal [simp]: "0 = - a \<longleftrightarrow> 0 = a"
   by (subst neg_equal_iff_equal [symmetric]) simp
 
-text\<open>The next two equations can make the simplifier loop!\<close>
+text \<open>The next two equations can make the simplifier loop!\<close>
 
-lemma equation_minus_iff:
-  "a = - b \<longleftrightarrow> b = - a"
+lemma equation_minus_iff: "a = - b \<longleftrightarrow> b = - a"
 proof -
-  have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
-  thus ?thesis by (simp add: eq_commute)
+  have "- (- a) = - b \<longleftrightarrow> - a = b"
+    by (rule neg_equal_iff_equal)
+  then show ?thesis
+    by (simp add: eq_commute)
 qed
 
-lemma minus_equation_iff:
-  "- a = b \<longleftrightarrow> - b = a"
+lemma minus_equation_iff: "- a = b \<longleftrightarrow> - b = a"
 proof -
-  have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
-  thus ?thesis by (simp add: eq_commute)
+  have "- a = - (- b) \<longleftrightarrow> a = -b"
+    by (rule neg_equal_iff_equal)
+  then show ?thesis
+    by (simp add: eq_commute)
 qed
 
-lemma eq_neg_iff_add_eq_0:
-  "a = - b \<longleftrightarrow> a + b = 0"
+lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
 proof
-  assume "a = - b" then show "a + b = 0" by simp
+  assume "a = - b"
+  then show "a + b = 0" by simp
 next
   assume "a + b = 0"
   moreover have "a + (b + - b) = (a + b) + - b"
     by (simp only: add.assoc)
-  ultimately show "a = - b" by simp
+  ultimately show "a = - b"
+    by simp
 qed
 
-lemma add_eq_0_iff2:
-  "a + b = 0 \<longleftrightarrow> a = - b"
+lemma add_eq_0_iff2: "a + b = 0 \<longleftrightarrow> a = - b"
   by (fact eq_neg_iff_add_eq_0 [symmetric])
 
-lemma neg_eq_iff_add_eq_0:
-  "- a = b \<longleftrightarrow> a + b = 0"
+lemma neg_eq_iff_add_eq_0: "- a = b \<longleftrightarrow> a + b = 0"
   by (auto simp add: add_eq_0_iff2)
 
-lemma add_eq_0_iff:
-  "a + b = 0 \<longleftrightarrow> b = - a"
+lemma add_eq_0_iff: "a + b = 0 \<longleftrightarrow> b = - a"
   by (auto simp add: neg_eq_iff_add_eq_0 [symmetric])
 
-lemma minus_diff_eq [simp]:
-  "- (a - b) = b - a"
+lemma minus_diff_eq [simp]: "- (a - b) = b - a"
   by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add.assoc minus_add_cancel) simp
 
-lemma add_diff_eq [algebra_simps, field_simps]:
-  "a + (b - c) = (a + b) - c"
+lemma add_diff_eq [algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
   by (simp only: diff_conv_add_uminus add.assoc)
 
-lemma diff_add_eq_diff_diff_swap:
-  "a - (b + c) = a - c - b"
+lemma diff_add_eq_diff_diff_swap: "a - (b + c) = a - c - b"
   by (simp only: diff_conv_add_uminus add.assoc minus_add)
 
-lemma diff_eq_eq [algebra_simps, field_simps]:
-  "a - b = c \<longleftrightarrow> a = c + b"
+lemma diff_eq_eq [algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
   by auto
 
-lemma eq_diff_eq [algebra_simps, field_simps]:
-  "a = c - b \<longleftrightarrow> a + b = c"
+lemma eq_diff_eq [algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
   by auto
 
-lemma diff_diff_eq2 [algebra_simps, field_simps]:
-  "a - (b - c) = (a + c) - b"
+lemma diff_diff_eq2 [algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
   by (simp only: diff_conv_add_uminus add.assoc) simp
 
-lemma diff_eq_diff_eq:
-  "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
+lemma diff_eq_diff_eq: "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
   by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
 
 end
@@ -550,7 +527,7 @@
 begin
 
 subclass group_add
-  proof qed (simp_all add: ab_left_minus ab_diff_conv_add_uminus)
+  by standard (simp_all add: ab_left_minus ab_diff_conv_add_uminus)
 
 subclass cancel_comm_monoid_add
 proof
@@ -563,16 +540,13 @@
     by (simp add: algebra_simps)
 qed
 
-lemma uminus_add_conv_diff [simp]:
-  "- a + b = b - a"
+lemma uminus_add_conv_diff [simp]: "- a + b = b - a"
   by (simp add: add.commute)
 
-lemma minus_add_distrib [simp]:
-  "- (a + b) = - a + - b"
+lemma minus_add_distrib [simp]: "- (a + b) = - a + - b"
   by (simp add: algebra_simps)
 
-lemma diff_add_eq [algebra_simps, field_simps]:
-  "(a - b) + c = (a + c) - b"
+lemma diff_add_eq [algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
   by (simp add: algebra_simps)
 
 end
@@ -582,35 +556,31 @@
 
 text \<open>
   The theory of partially ordered groups is taken from the books:
-  \begin{itemize}
-  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
-  \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
-  \end{itemize}
+
+    \<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979
+    \<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
+
   Most of the used notions can also be looked up in
-  \begin{itemize}
-  \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
-  \item \emph{Algebra I} by van der Waerden, Springer.
-  \end{itemize}
+    \<^item> @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
+    \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
 \<close>
 
 class ordered_ab_semigroup_add = order + ab_semigroup_add +
   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
 begin
 
-lemma add_right_mono:
-  "a \<le> b \<Longrightarrow> a + c \<le> b + c"
-by (simp add: add.commute [of _ c] add_left_mono)
+lemma add_right_mono: "a \<le> b \<Longrightarrow> a + c \<le> b + c"
+  by (simp add: add.commute [of _ c] add_left_mono)
 
 text \<open>non-strict, in both arguments\<close>
-lemma add_mono:
-  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
+lemma add_mono: "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   apply (erule add_right_mono [THEN order_trans])
   apply (simp add: add.commute add_left_mono)
   done
 
 end
 
-text\<open>Strict monotonicity in both arguments\<close>
+text \<open>Strict monotonicity in both arguments\<close>
 class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add +
   assumes add_strict_mono: "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
 
@@ -618,13 +588,11 @@
   ordered_ab_semigroup_add + cancel_ab_semigroup_add
 begin
 
-lemma add_strict_left_mono:
-  "a < b \<Longrightarrow> c + a < c + b"
-by (auto simp add: less_le add_left_mono)
+lemma add_strict_left_mono: "a < b \<Longrightarrow> c + a < c + b"
+  by (auto simp add: less_le add_left_mono)
 
-lemma add_strict_right_mono:
-  "a < b \<Longrightarrow> a + c < b + c"
-by (simp add: add.commute [of _ c] add_strict_left_mono)
+lemma add_strict_right_mono: "a < b \<Longrightarrow> a + c < b + c"
+  by (simp add: add.commute [of _ c] add_strict_left_mono)
 
 subclass strict_ordered_ab_semigroup_add
   apply standard
@@ -632,17 +600,15 @@
   apply (erule add_strict_left_mono)
   done
 
-lemma add_less_le_mono:
-  "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
-apply (erule add_strict_right_mono [THEN less_le_trans])
-apply (erule add_left_mono)
-done
+lemma add_less_le_mono: "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
+  apply (erule add_strict_right_mono [THEN less_le_trans])
+  apply (erule add_left_mono)
+  done
 
-lemma add_le_less_mono:
-  "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
-apply (erule add_right_mono [THEN le_less_trans])
-apply (erule add_strict_left_mono)
-done
+lemma add_le_less_mono: "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
+  apply (erule add_right_mono [THEN le_less_trans])
+  apply (erule add_strict_left_mono)
+  done
 
 end
 
@@ -651,63 +617,60 @@
 begin
 
 lemma add_less_imp_less_left:
-  assumes less: "c + a < c + b" shows "a < b"
+  assumes less: "c + a < c + b"
+  shows "a < b"
 proof -
-  from less have le: "c + a <= c + b" by (simp add: order_le_less)
-  have "a <= b"
+  from less have le: "c + a \<le> c + b"
+    by (simp add: order_le_less)
+  have "a \<le> b"
     apply (insert le)
     apply (drule add_le_imp_le_left)
-    by (insert le, drule add_le_imp_le_left, assumption)
+    apply (insert le)
+    apply (drule add_le_imp_le_left)
+    apply assumption
+    done
   moreover have "a \<noteq> b"
   proof (rule ccontr)
-    assume "~(a \<noteq> b)"
+    assume "\<not> ?thesis"
     then have "a = b" by simp
     then have "c + a = c + b" by simp
-    with less show "False"by simp
+    with less show "False" by simp
   qed
-  ultimately show "a < b" by (simp add: order_le_less)
+  ultimately show "a < b"
+    by (simp add: order_le_less)
 qed
 
-lemma add_less_imp_less_right:
-  "a + c < b + c \<Longrightarrow> a < b"
-apply (rule add_less_imp_less_left [of c])
-apply (simp add: add.commute)
-done
+lemma add_less_imp_less_right: "a + c < b + c \<Longrightarrow> a < b"
+  by (rule add_less_imp_less_left [of c]) (simp add: add.commute)
 
-lemma add_less_cancel_left [simp]:
-  "c + a < c + b \<longleftrightarrow> a < b"
+lemma add_less_cancel_left [simp]: "c + a < c + b \<longleftrightarrow> a < b"
   by (blast intro: add_less_imp_less_left add_strict_left_mono)
 
-lemma add_less_cancel_right [simp]:
-  "a + c < b + c \<longleftrightarrow> a < b"
+lemma add_less_cancel_right [simp]: "a + c < b + c \<longleftrightarrow> a < b"
   by (blast intro: add_less_imp_less_right add_strict_right_mono)
 
-lemma add_le_cancel_left [simp]:
-  "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
-  by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)
+lemma add_le_cancel_left [simp]: "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
+  apply auto
+  apply (drule add_le_imp_le_left)
+  apply (simp_all add: add_left_mono)
+  done
 
-lemma add_le_cancel_right [simp]:
-  "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
+lemma add_le_cancel_right [simp]: "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   by (simp add: add.commute [of a c] add.commute [of b c])
 
-lemma add_le_imp_le_right:
-  "a + c \<le> b + c \<Longrightarrow> a \<le> b"
-by simp
+lemma add_le_imp_le_right: "a + c \<le> b + c \<Longrightarrow> a \<le> b"
+  by simp
 
-lemma max_add_distrib_left:
-  "max x y + z = max (x + z) (y + z)"
+lemma max_add_distrib_left: "max x y + z = max (x + z) (y + z)"
   unfolding max_def by auto
 
-lemma min_add_distrib_left:
-  "min x y + z = min (x + z) (y + z)"
+lemma min_add_distrib_left: "min x y + z = min (x + z) (y + z)"
   unfolding min_def by auto
 
-lemma max_add_distrib_right:
-  "x + max y z = max (x + y) (x + z)"
+lemma max_add_distrib_right: "x + max y z = max (x + y) (x + z)"
   unfolding max_def by auto
 
-lemma min_add_distrib_right:
-  "x + min y z = min (x + y) (x + z)"
+lemma min_add_distrib_right: "x + min y z = min (x + y) (x + z)"
   unfolding min_def by auto
 
 end
@@ -717,36 +680,28 @@
 class ordered_comm_monoid_add = comm_monoid_add + ordered_ab_semigroup_add
 begin
 
-lemma add_nonneg_nonneg [simp]:
-  "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
+lemma add_nonneg_nonneg [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
   using add_mono[of 0 a 0 b] by simp
 
-lemma add_nonpos_nonpos:
-  "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b \<le> 0"
+lemma add_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b \<le> 0"
   using add_mono[of a 0 b 0] by simp
 
-lemma add_nonneg_eq_0_iff:
-  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+lemma add_nonneg_eq_0_iff: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   using add_left_mono[of 0 y x] add_right_mono[of 0 x y] by auto
 
-lemma add_nonpos_eq_0_iff:
-  "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+lemma add_nonpos_eq_0_iff: "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   using add_left_mono[of y 0 x] add_right_mono[of x 0 y] by auto
 
-lemma add_increasing:
-  "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
-  by (insert add_mono [of 0 a b c], simp)
+lemma add_increasing: "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
+  using add_mono [of 0 a b c] by simp
 
-lemma add_increasing2:
-  "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
+lemma add_increasing2: "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
   by (simp add: add_increasing add.commute [of a])
 
-lemma add_decreasing:
-  "a \<le> 0 \<Longrightarrow> c \<le> b \<Longrightarrow> a + c \<le> b"
-  using add_mono[of a 0 c b] by simp
+lemma add_decreasing: "a \<le> 0 \<Longrightarrow> c \<le> b \<Longrightarrow> a + c \<le> b"
+  using add_mono [of a 0 c b] by simp
 
-lemma add_decreasing2:
-  "c \<le> 0 \<Longrightarrow> a \<le> b \<Longrightarrow> a + c \<le> b"
+lemma add_decreasing2: "c \<le> 0 \<Longrightarrow> a \<le> b \<Longrightarrow> a + c \<le> b"
   using add_mono[of a b c 0] by simp
 
 lemma add_pos_nonneg: "0 < a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < a + b"
@@ -776,8 +731,7 @@
 class strict_ordered_comm_monoid_add = comm_monoid_add + strict_ordered_ab_semigroup_add
 begin
 
-lemma pos_add_strict:
-  shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
+lemma pos_add_strict: "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   using add_strict_mono [of 0 a b c] by simp
 
 end
@@ -788,13 +742,11 @@
 subclass ordered_cancel_ab_semigroup_add ..
 subclass strict_ordered_comm_monoid_add ..
 
-lemma add_strict_increasing:
-  "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
-  by (insert add_less_le_mono [of 0 a b c], simp)
+lemma add_strict_increasing: "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
+  using add_less_le_mono [of 0 a b c] by simp
 
-lemma add_strict_increasing2:
-  "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
-  by (insert add_le_less_mono [of 0 a b c], simp)
+lemma add_strict_increasing2: "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
+  using add_le_less_mono [of 0 a b c] by simp
 
 end
 
@@ -807,105 +759,108 @@
 proof
   fix a b c :: 'a
   assume "c + a \<le> c + b"
-  hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
-  hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add.assoc)
-  thus "a \<le> b" by simp
+  then have "(-c) + (c + a) \<le> (-c) + (c + b)"
+    by (rule add_left_mono)
+  then have "((-c) + c) + a \<le> ((-c) + c) + b"
+    by (simp only: add.assoc)
+  then show "a \<le> b" by simp
 qed
 
 subclass ordered_cancel_comm_monoid_add ..
 
-lemma add_less_same_cancel1 [simp]:
-  "b + a < b \<longleftrightarrow> a < 0"
+lemma add_less_same_cancel1 [simp]: "b + a < b \<longleftrightarrow> a < 0"
   using add_less_cancel_left [of _ _ 0] by simp
 
-lemma add_less_same_cancel2 [simp]:
-  "a + b < b \<longleftrightarrow> a < 0"
+lemma add_less_same_cancel2 [simp]: "a + b < b \<longleftrightarrow> a < 0"
   using add_less_cancel_right [of _ _ 0] by simp
 
-lemma less_add_same_cancel1 [simp]:
-  "a < a + b \<longleftrightarrow> 0 < b"
+lemma less_add_same_cancel1 [simp]: "a < a + b \<longleftrightarrow> 0 < b"
   using add_less_cancel_left [of _ 0] by simp
 
-lemma less_add_same_cancel2 [simp]:
-  "a < b + a \<longleftrightarrow> 0 < b"
+lemma less_add_same_cancel2 [simp]: "a < b + a \<longleftrightarrow> 0 < b"
   using add_less_cancel_right [of 0] by simp
 
-lemma add_le_same_cancel1 [simp]:
-  "b + a \<le> b \<longleftrightarrow> a \<le> 0"
+lemma add_le_same_cancel1 [simp]: "b + a \<le> b \<longleftrightarrow> a \<le> 0"
   using add_le_cancel_left [of _ _ 0] by simp
 
-lemma add_le_same_cancel2 [simp]:
-  "a + b \<le> b \<longleftrightarrow> a \<le> 0"
+lemma add_le_same_cancel2 [simp]: "a + b \<le> b \<longleftrightarrow> a \<le> 0"
   using add_le_cancel_right [of _ _ 0] by simp
 
-lemma le_add_same_cancel1 [simp]:
-  "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
+lemma le_add_same_cancel1 [simp]: "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
   using add_le_cancel_left [of _ 0] by simp
 
-lemma le_add_same_cancel2 [simp]:
-  "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
+lemma le_add_same_cancel2 [simp]: "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
   using add_le_cancel_right [of 0] by simp
 
-lemma max_diff_distrib_left:
-  shows "max x y - z = max (x - z) (y - z)"
+lemma max_diff_distrib_left: "max x y - z = max (x - z) (y - z)"
   using max_add_distrib_left [of x y "- z"] by simp
 
-lemma min_diff_distrib_left:
-  shows "min x y - z = min (x - z) (y - z)"
+lemma min_diff_distrib_left: "min x y - z = min (x - z) (y - z)"
   using min_add_distrib_left [of x y "- z"] by simp
 
 lemma le_imp_neg_le:
-  assumes "a \<le> b" shows "-b \<le> -a"
+  assumes "a \<le> b"
+  shows "- b \<le> - a"
 proof -
-  have "-a+a \<le> -a+b" using \<open>a \<le> b\<close> by (rule add_left_mono)
-  then have "0 \<le> -a+b" by simp
-  then have "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)
-  then show ?thesis by (simp add: algebra_simps)
+  from assms have "- a + a \<le> - a + b"
+    by (rule add_left_mono)
+  then have "0 \<le> - a + b"
+    by simp
+  then have "0 + (- b) \<le> (- a + b) + (- b)"
+    by (rule add_right_mono)
+  then show ?thesis
+    by (simp add: algebra_simps)
 qed
 
 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
 proof
   assume "- b \<le> - a"
-  hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
-  thus "a\<le>b" by simp
+  then have "- (- a) \<le> - (- b)"
+    by (rule le_imp_neg_le)
+  then show "a \<le> b"
+    by simp
 next
-  assume "a\<le>b"
-  thus "-b \<le> -a" by (rule le_imp_neg_le)
+  assume "a \<le> b"
+  then show "- b \<le> - a"
+    by (rule le_imp_neg_le)
 qed
 
 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
-by (subst neg_le_iff_le [symmetric], simp)
+  by (subst neg_le_iff_le [symmetric]) simp
 
 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
-by (subst neg_le_iff_le [symmetric], simp)
+  by (subst neg_le_iff_le [symmetric]) simp
 
 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
-by (force simp add: less_le)
+  by (auto simp add: less_le)
 
 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
-by (subst neg_less_iff_less [symmetric], simp)
+  by (subst neg_less_iff_less [symmetric]) simp
 
 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
-by (subst neg_less_iff_less [symmetric], simp)
+  by (subst neg_less_iff_less [symmetric]) simp
 
-text\<open>The next several equations can make the simplifier loop!\<close>
+text \<open>The next several equations can make the simplifier loop!\<close>
 
 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
 proof -
-  have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
-  thus ?thesis by simp
+  have "- (-a) < - b \<longleftrightarrow> b < - a"
+    by (rule neg_less_iff_less)
+  then show ?thesis by simp
 qed
 
 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
 proof -
-  have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
-  thus ?thesis by simp
+  have "- a < - (- b) \<longleftrightarrow> - b < a"
+    by (rule neg_less_iff_less)
+  then show ?thesis by simp
 qed
 
 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
 proof -
-  have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
-  have "(- (- a) <= -b) = (b <= - a)"
+  have mm: "- (- a) < -b \<Longrightarrow> - (- b) < -a" for a b :: 'a
+    by (simp only: minus_less_iff)
+  have "- (- a) \<le> -b \<longleftrightarrow> b \<le> - a"
     apply (auto simp only: le_less)
     apply (drule mm)
     apply (simp_all)
@@ -915,60 +870,52 @@
 qed
 
 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
-by (auto simp add: le_less minus_less_iff)
+  by (auto simp add: le_less minus_less_iff)
 
-lemma diff_less_0_iff_less [simp]:
-  "a - b < 0 \<longleftrightarrow> a < b"
+lemma diff_less_0_iff_less [simp]: "a - b < 0 \<longleftrightarrow> a < b"
 proof -
-  have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by simp
-  also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
+  have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)"
+    by simp
+  also have "\<dots> \<longleftrightarrow> a < b"
+    by (simp only: add_less_cancel_right)
   finally show ?thesis .
 qed
 
 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
 
-lemma diff_less_eq [algebra_simps, field_simps]:
-  "a - b < c \<longleftrightarrow> a < c + b"
-apply (subst less_iff_diff_less_0 [of a])
-apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
-apply (simp add: algebra_simps)
-done
+lemma diff_less_eq [algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
+  apply (subst less_iff_diff_less_0 [of a])
+  apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
+  apply (simp add: algebra_simps)
+  done
 
-lemma less_diff_eq[algebra_simps, field_simps]:
-  "a < c - b \<longleftrightarrow> a + b < c"
-apply (subst less_iff_diff_less_0 [of "a + b"])
-apply (subst less_iff_diff_less_0 [of a])
-apply (simp add: algebra_simps)
-done
+lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"
+  apply (subst less_iff_diff_less_0 [of "a + b"])
+  apply (subst less_iff_diff_less_0 [of a])
+  apply (simp add: algebra_simps)
+  done
 
-lemma diff_gt_0_iff_gt [simp]:
-  "a - b > 0 \<longleftrightarrow> a > b"
+lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \<longleftrightarrow> a > b"
   by (simp add: less_diff_eq)
 
-lemma diff_le_eq [algebra_simps, field_simps]:
-  "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
+lemma diff_le_eq [algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   by (auto simp add: le_less diff_less_eq )
 
-lemma le_diff_eq [algebra_simps, field_simps]:
-  "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
+lemma le_diff_eq [algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   by (auto simp add: le_less less_diff_eq)
 
-lemma diff_le_0_iff_le [simp]:
-  "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
+lemma diff_le_0_iff_le [simp]: "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
   by (simp add: algebra_simps)
 
 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
 
-lemma diff_ge_0_iff_ge [simp]:
-  "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
+lemma diff_ge_0_iff_ge [simp]: "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
   by (simp add: le_diff_eq)
 
-lemma diff_eq_diff_less:
-  "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
+lemma diff_eq_diff_less: "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
 
-lemma diff_eq_diff_less_eq:
-  "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
+lemma diff_eq_diff_less_eq: "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
 
 lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d"
@@ -1020,18 +967,18 @@
 subclass ordered_ab_semigroup_add_imp_le
 proof
   fix a b c :: 'a
-  assume le: "c + a <= c + b"
-  show "a <= b"
+  assume le1: "c + a \<le> c + b"
+  show "a \<le> b"
   proof (rule ccontr)
-    assume w: "~ a \<le> b"
-    hence "b <= a" by (simp add: linorder_not_le)
-    hence le2: "c + b <= c + a" by (rule add_left_mono)
+    assume *: "\<not> ?thesis"
+    then have "b \<le> a" by (simp add: linorder_not_le)
+    then have le2: "c + b \<le> c + a" by (rule add_left_mono)
     have "a = b"
-      apply (insert le)
-      apply (insert le2)
-      apply (drule antisym, simp_all)
+      apply (insert le1 le2)
+      apply (drule antisym)
+      apply simp_all
       done
-    with w show False
+    with * show False
       by (simp add: linorder_not_le [symmetric])
   qed
 qed
@@ -1043,72 +990,71 @@
 
 subclass linordered_cancel_ab_semigroup_add ..
 
-lemma equal_neg_zero [simp]:
-  "a = - a \<longleftrightarrow> a = 0"
+lemma equal_neg_zero [simp]: "a = - a \<longleftrightarrow> a = 0"
 proof
-  assume "a = 0" then show "a = - a" by simp
+  assume "a = 0"
+  then show "a = - a" by simp
 next
-  assume A: "a = - a" show "a = 0"
+  assume A: "a = - a"
+  show "a = 0"
   proof (cases "0 \<le> a")
-    case True with A have "0 \<le> - a" by auto
+    case True
+    with A have "0 \<le> - a" by auto
     with le_minus_iff have "a \<le> 0" by simp
     with True show ?thesis by (auto intro: order_trans)
   next
-    case False then have B: "a \<le> 0" by auto
+    case False
+    then have B: "a \<le> 0" by auto
     with A have "- a \<le> 0" by auto
     with B show ?thesis by (auto intro: order_trans)
   qed
 qed
 
-lemma neg_equal_zero [simp]:
-  "- a = a \<longleftrightarrow> a = 0"
+lemma neg_equal_zero [simp]: "- a = a \<longleftrightarrow> a = 0"
   by (auto dest: sym)
 
-lemma neg_less_eq_nonneg [simp]:
-  "- a \<le> a \<longleftrightarrow> 0 \<le> a"
+lemma neg_less_eq_nonneg [simp]: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
 proof
-  assume A: "- a \<le> a" show "0 \<le> a"
+  assume *: "- a \<le> a"
+  show "0 \<le> a"
   proof (rule classical)
-    assume "\<not> 0 \<le> a"
+    assume "\<not> ?thesis"
     then have "a < 0" by auto
-    with A have "- a < 0" by (rule le_less_trans)
+    with * have "- a < 0" by (rule le_less_trans)
     then show ?thesis by auto
   qed
 next
-  assume A: "0 \<le> a" show "- a \<le> a"
-  proof (rule order_trans)
-    show "- a \<le> 0" using A by (simp add: minus_le_iff)
-  next
-    show "0 \<le> a" using A .
-  qed
+  assume *: "0 \<le> a"
+  then have "- a \<le> 0" by (simp add: minus_le_iff)
+  from this * show "- a \<le> a" by (rule order_trans)
 qed
 
-lemma neg_less_pos [simp]:
-  "- a < a \<longleftrightarrow> 0 < a"
+lemma neg_less_pos [simp]: "- a < a \<longleftrightarrow> 0 < a"
   by (auto simp add: less_le)
 
-lemma less_eq_neg_nonpos [simp]:
-  "a \<le> - a \<longleftrightarrow> a \<le> 0"
+lemma less_eq_neg_nonpos [simp]: "a \<le> - a \<longleftrightarrow> a \<le> 0"
   using neg_less_eq_nonneg [of "- a"] by simp
 
-lemma less_neg_neg [simp]:
-  "a < - a \<longleftrightarrow> a < 0"
+lemma less_neg_neg [simp]: "a < - a \<longleftrightarrow> a < 0"
   using neg_less_pos [of "- a"] by simp
 
-lemma double_zero [simp]:
-  "a + a = 0 \<longleftrightarrow> a = 0"
+lemma double_zero [simp]: "a + a = 0 \<longleftrightarrow> a = 0"
 proof
-  assume assm: "a + a = 0"
+  assume "a + a = 0"
   then have a: "- a = a" by (rule minus_unique)
   then show "a = 0" by (simp only: neg_equal_zero)
-qed simp
+next
+  assume "a = 0"
+  then show "a + a = 0" by simp
+qed
 
-lemma double_zero_sym [simp]:
-  "0 = a + a \<longleftrightarrow> a = 0"
-  by (rule, drule sym) simp_all
+lemma double_zero_sym [simp]: "0 = a + a \<longleftrightarrow> a = 0"
+  apply (rule iffI)
+  apply (drule sym)
+  apply simp_all
+  done
 
-lemma zero_less_double_add_iff_zero_less_single_add [simp]:
-  "0 < a + a \<longleftrightarrow> 0 < a"
+lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a"
 proof
   assume "0 < a + a"
   then have "0 - a < a" by (simp only: diff_less_eq)
@@ -1121,32 +1067,27 @@
   then show "0 < a + a" by simp
 qed
 
-lemma zero_le_double_add_iff_zero_le_single_add [simp]:
-  "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
+lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   by (auto simp add: le_less)
 
-lemma double_add_less_zero_iff_single_add_less_zero [simp]:
-  "a + a < 0 \<longleftrightarrow> a < 0"
+lemma double_add_less_zero_iff_single_add_less_zero [simp]: "a + a < 0 \<longleftrightarrow> a < 0"
 proof -
   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
     by (simp add: not_less)
   then show ?thesis by simp
 qed
 
-lemma double_add_le_zero_iff_single_add_le_zero [simp]:
-  "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
+lemma double_add_le_zero_iff_single_add_le_zero [simp]: "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
 proof -
   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
     by (simp add: not_le)
   then show ?thesis by simp
 qed
 
-lemma minus_max_eq_min:
-  "- max x y = min (-x) (-y)"
+lemma minus_max_eq_min: "- max x y = min (- x) (- y)"
   by (auto simp add: max_def min_def)
 
-lemma minus_min_eq_max:
-  "- min x y = max (-x) (-y)"
+lemma minus_min_eq_max: "- min x y = max (- x) (- y)"
   by (auto simp add: max_def min_def)
 
 end
@@ -1181,16 +1122,17 @@
   unfolding neg_le_0_iff_le by simp
 
 lemma abs_of_nonneg [simp]:
-  assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
+  assumes nonneg: "0 \<le> a"
+  shows "\<bar>a\<bar> = a"
 proof (rule antisym)
+  show "a \<le> \<bar>a\<bar>" by (rule abs_ge_self)
   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
   from this nonneg have "- a \<le> a" by (rule order_trans)
   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
-qed (rule abs_ge_self)
+qed
 
 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
-by (rule antisym)
-   (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
+  by (rule antisym) (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
 
 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
 proof -
@@ -1206,27 +1148,27 @@
 qed
 
 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
-by simp
+  by simp
 
 lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
 proof -
   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
-  thus ?thesis by simp
+  then show ?thesis by simp
 qed
 
 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
 proof
   assume "\<bar>a\<bar> \<le> 0"
   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
-  thus "a = 0" by simp
+  then show "a = 0" by simp
 next
   assume "a = 0"
-  thus "\<bar>a\<bar> \<le> 0" by simp
+  then show "\<bar>a\<bar> \<le> 0" by simp
 qed
 
 lemma abs_le_self_iff [simp]: "\<bar>a\<bar> \<le> a \<longleftrightarrow> 0 \<le> a"
 proof -
-  have "\<forall>a. (0::'a) \<le> \<bar>a\<bar>"
+  have "0 \<le> \<bar>a\<bar>"
     using abs_ge_zero by blast
   then have "\<bar>a\<bar> \<le> a \<Longrightarrow> 0 \<le> a"
     using order.trans by blast
@@ -1235,12 +1177,12 @@
 qed
 
 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
-by (simp add: less_le)
+  by (simp add: less_le)
 
 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
 proof -
-  have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
-  show ?thesis by (simp add: a)
+  have "x \<le> y \<Longrightarrow> \<not> y < x" for x y by auto
+  then show ?thesis by simp
 qed
 
 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
@@ -1249,39 +1191,40 @@
   then show ?thesis by simp
 qed
 
-lemma abs_minus_commute:
-  "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
+lemma abs_minus_commute: "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
 proof -
-  have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
-  also have "... = \<bar>b - a\<bar>" by simp
+  have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>"
+    by (simp only: abs_minus_cancel)
+  also have "\<dots> = \<bar>b - a\<bar>" by simp
   finally show ?thesis .
 qed
 
 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
-by (rule abs_of_nonneg, rule less_imp_le)
+  by (rule abs_of_nonneg) (rule less_imp_le)
 
 lemma abs_of_nonpos [simp]:
-  assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
+  assumes "a \<le> 0"
+  shows "\<bar>a\<bar> = - a"
 proof -
   let ?b = "- a"
   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
-  unfolding abs_minus_cancel [of "?b"]
-  unfolding neg_le_0_iff_le [of "?b"]
-  unfolding minus_minus by (erule abs_of_nonneg)
+    unfolding abs_minus_cancel [of ?b]
+    unfolding neg_le_0_iff_le [of ?b]
+    unfolding minus_minus by (erule abs_of_nonneg)
   then show ?thesis using assms by auto
 qed
 
 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
-by (rule abs_of_nonpos, rule less_imp_le)
+  by (rule abs_of_nonpos) (rule less_imp_le)
 
 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
-by (insert abs_ge_self, blast intro: order_trans)
+  using abs_ge_self by (blast intro: order_trans)
 
 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
-by (insert abs_le_D1 [of "- a"], simp)
+  using abs_le_D1 [of "- a"] by simp
 
 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
-by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
+  by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
 
 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
 proof -
@@ -1301,24 +1244,27 @@
 
 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
 proof -
-  have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (simp add: algebra_simps)
-  also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
+  have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>"
+    by (simp add: algebra_simps)
+  also have "\<dots> \<le> \<bar>a\<bar> + \<bar>- b\<bar>"
+    by (rule abs_triangle_ineq)
   finally show ?thesis by simp
 qed
 
 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
 proof -
-  have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: algebra_simps)
-  also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
+  have "\<bar>a + b - (c + d)\<bar> = \<bar>(a - c) + (b - d)\<bar>"
+    by (simp add: algebra_simps)
+  also have "\<dots> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
+    by (rule abs_triangle_ineq)
   finally show ?thesis .
 qed
 
-lemma abs_add_abs [simp]:
-  "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
+lemma abs_add_abs [simp]: "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>"
+  (is "?L = ?R")
 proof (rule antisym)
-  show "?L \<ge> ?R" by(rule abs_ge_self)
-next
-  have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
+  show "?L \<ge> ?R" by (rule abs_ge_self)
+  have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by (rule abs_triangle_ineq)
   also have "\<dots> = ?R" by simp
   finally show "?L \<le> ?R" .
 qed
@@ -1327,8 +1273,9 @@
 
 lemma dense_eq0_I:
   fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
-  shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
-  apply (cases "\<bar>x\<bar> = 0", simp)
+  shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) \<Longrightarrow> x = 0"
+  apply (cases "\<bar>x\<bar> = 0")
+  apply simp
   apply (simp only: zero_less_abs_iff [symmetric])
   apply (drule dense)
   apply (auto simp add: not_less [symmetric])
@@ -1336,10 +1283,11 @@
 
 hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
 
-lemmas add_0 = add_0_left \<comment> \<open>FIXME duplicate\<close>
-lemmas mult_1 = mult_1_left \<comment> \<open>FIXME duplicate\<close>
-lemmas ab_left_minus = left_minus \<comment> \<open>FIXME duplicate\<close>
-lemmas diff_diff_eq = diff_diff_add \<comment> \<open>FIXME duplicate\<close>
+lemmas add_0 = add_0_left (* FIXME duplicate *)
+lemmas mult_1 = mult_1_left (* FIXME duplicate *)
+lemmas ab_left_minus = left_minus (* FIXME duplicate *)
+lemmas diff_diff_eq = diff_diff_add (* FIXME duplicate *)
+
 
 subsection \<open>Canonically ordered monoids\<close>
 
@@ -1358,14 +1306,14 @@
 lemma not_less_zero[simp]: "\<not> n < 0"
   by (auto simp: less_le)
 
-lemma zero_less_iff_neq_zero: "(0 < n) \<longleftrightarrow> (n \<noteq> 0)"
+lemma zero_less_iff_neq_zero: "0 < n \<longleftrightarrow> n \<noteq> 0"
   by (auto simp: less_le)
 
 text \<open>This theorem is useful with \<open>blast\<close>\<close>
 lemma gr_zeroI: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n"
   by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover
 
-lemma not_gr_zero[simp]: "(\<not> (0 < n)) \<longleftrightarrow> (n = 0)"
+lemma not_gr_zero[simp]: "\<not> 0 < n \<longleftrightarrow> n = 0"
   by (simp add: zero_less_iff_neq_zero)
 
 subclass ordered_comm_monoid_add
@@ -1388,54 +1336,48 @@
 
 context
   fixes a b
-  assumes "a \<le> b"
+  assumes le: "a \<le> b"
 begin
 
-lemma add_diff_inverse:
-  "a + (b - a) = b"
-  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add)
+lemma add_diff_inverse: "a + (b - a) = b"
+  using le by (auto simp add: le_iff_add)
 
-lemma add_diff_assoc:
-  "c + (b - a) = c + b - a"
-  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.left_commute [of c])
+lemma add_diff_assoc: "c + (b - a) = c + b - a"
+  using le by (auto simp add: le_iff_add add.left_commute [of c])
 
-lemma add_diff_assoc2:
-  "b - a + c = b + c - a"
-  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.assoc)
+lemma add_diff_assoc2: "b - a + c = b + c - a"
+  using le by (auto simp add: le_iff_add add.assoc)
 
-lemma diff_add_assoc:
-  "c + b - a = c + (b - a)"
-  using \<open>a \<le> b\<close> by (simp add: add.commute add_diff_assoc)
+lemma diff_add_assoc: "c + b - a = c + (b - a)"
+  using le by (simp add: add.commute add_diff_assoc)
 
-lemma diff_add_assoc2:
-  "b + c - a = b - a + c"
-  using \<open>a \<le> b\<close>by (simp add: add.commute add_diff_assoc)
+lemma diff_add_assoc2: "b + c - a = b - a + c"
+  using le by (simp add: add.commute add_diff_assoc)
 
-lemma diff_diff_right:
-  "c - (b - a) = c + a - b"
+lemma diff_diff_right: "c - (b - a) = c + a - b"
   by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)
 
-lemma diff_add:
-  "b - a + a = b"
+lemma diff_add: "b - a + a = b"
   by (simp add: add.commute add_diff_inverse)
 
-lemma le_add_diff:
-  "c \<le> b + c - a"
+lemma le_add_diff: "c \<le> b + c - a"
   by (auto simp add: add.commute diff_add_assoc2 le_iff_add)
 
-lemma le_imp_diff_is_add:
-  "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
+lemma le_imp_diff_is_add: "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
   by (auto simp add: add.commute add_diff_inverse)
 
-lemma le_diff_conv2:
-  "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
+lemma le_diff_conv2: "c \<le> b - a \<longleftrightarrow> c + a \<le> b"
+  (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?P
-  then have "c + a \<le> b - a + a" by (rule add_right_mono)
-  then show ?Q by (simp add: add_diff_inverse add.commute)
+  then have "c + a \<le> b - a + a"
+    by (rule add_right_mono)
+  then show ?Q
+    by (simp add: add_diff_inverse add.commute)
 next
   assume ?Q
-  then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add.commute)
+  then have "a + c \<le> a + (b - a)"
+    by (simp add: add_diff_inverse add.commute)
   then show ?P by simp
 qed
 
@@ -1443,6 +1385,7 @@
 
 end
 
+
 subsection \<open>Tools setup\<close>
 
 lemma add_mono_thms_linordered_semiring:
@@ -1451,7 +1394,7 @@
     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
-by (rule add_mono, clarify+)+
+  by (rule add_mono, clarify+)+
 
 lemma add_mono_thms_linordered_field:
   fixes i j k :: "'a::ordered_cancel_ab_semigroup_add"
@@ -1460,8 +1403,8 @@
     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
-by (auto intro: add_strict_right_mono add_strict_left_mono
-  add_less_le_mono add_le_less_mono add_strict_mono)
+  by (auto intro: add_strict_right_mono add_strict_left_mono
+      add_less_le_mono add_le_less_mono add_strict_mono)
 
 code_identifier
   code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
diff -r 1e98146f3581 -r 1086d56cde86 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Mon Jun 20 17:51:47 2016 +0200
+++ b/src/HOL/Rings.thy	Mon Jun 20 21:40:48 2016 +0200
@@ -18,10 +18,9 @@
   assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"
 begin
 
-text\<open>For the \<open>combine_numerals\<close> simproc\<close>
-lemma combine_common_factor:
-  "a * e + (b * e + c) = (a + b) * e + c"
-by (simp add: distrib_right ac_simps)
+text \<open>For the \<open>combine_numerals\<close> simproc\<close>
+lemma combine_common_factor: "a * e + (b * e + c) = (a + b) * e + c"
+  by (simp add: distrib_right ac_simps)
 
 end
 
@@ -30,8 +29,7 @@
   assumes mult_zero_right [simp]: "a * 0 = 0"
 begin
 
-lemma mult_not_zero:
-  "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0"
+lemma mult_not_zero: "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0"
   by auto
 
 end
@@ -45,11 +43,9 @@
 proof
   fix a :: 'a
   have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric])
-  thus "0 * a = 0" by (simp only: add_left_cancel)
-next
-  fix a :: 'a
+  then show "0 * a = 0" by (simp only: add_left_cancel)
   have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric])
-  thus "a * 0 = 0" by (simp only: add_left_cancel)
+  then show "a * 0 = 0" by (simp only: add_left_cancel)
 qed
 
 end
@@ -63,8 +59,8 @@
   fix a b c :: 'a
   show "(a + b) * c = a * c + b * c" by (simp add: distrib)
   have "a * (b + c) = (b + c) * a" by (simp add: ac_simps)
-  also have "... = b * a + c * a" by (simp only: distrib)
-  also have "... = a * b + a * c" by (simp add: ac_simps)
+  also have "\<dots> = b * a + c * a" by (simp only: distrib)
+  also have "\<dots> = a * b + a * c" by (simp add: ac_simps)
   finally show "a * (b + c) = a * b + a * c" by blast
 qed
 
@@ -91,27 +87,23 @@
 begin
 
 lemma one_neq_zero [simp]: "1 \<noteq> 0"
-by (rule not_sym) (rule zero_neq_one)
+  by (rule not_sym) (rule zero_neq_one)
 
 definition of_bool :: "bool \<Rightarrow> 'a"
-where
-  "of_bool p = (if p then 1 else 0)"
+  where "of_bool p = (if p then 1 else 0)"
 
 lemma of_bool_eq [simp, code]:
   "of_bool False = 0"
   "of_bool True = 1"
   by (simp_all add: of_bool_def)
 
-lemma of_bool_eq_iff:
-  "of_bool p = of_bool q \<longleftrightarrow> p = q"
+lemma of_bool_eq_iff: "of_bool p = of_bool q \<longleftrightarrow> p = q"
   by (simp add: of_bool_def)
 
-lemma split_of_bool [split]:
-  "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)"
+lemma split_of_bool [split]: "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)"
   by (cases p) simp_all
 
-lemma split_of_bool_asm:
-  "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
+lemma split_of_bool_asm: "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
   by (cases p) simp_all
 
 end
@@ -123,8 +115,8 @@
 class dvd = times
 begin
 
-definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) where
-  "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
+definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50)
+  where "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
 
 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
   unfolding dvd_def ..
@@ -139,8 +131,7 @@
 
 subclass dvd .
 
-lemma dvd_refl [simp]:
-  "a dvd a"
+lemma dvd_refl [simp]: "a dvd a"
 proof
   show "a = a * 1" by simp
 qed
@@ -155,32 +146,25 @@
   then show ?thesis ..
 qed
 
-lemma subset_divisors_dvd:
-  "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
+lemma subset_divisors_dvd: "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
   by (auto simp add: subset_iff intro: dvd_trans)
 
-lemma strict_subset_divisors_dvd:
-  "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
+lemma strict_subset_divisors_dvd: "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
   by (auto simp add: subset_iff intro: dvd_trans)
 
-lemma one_dvd [simp]:
-  "1 dvd a"
+lemma one_dvd [simp]: "1 dvd a"
   by (auto intro!: dvdI)
 
-lemma dvd_mult [simp]:
-  "a dvd c \<Longrightarrow> a dvd (b * c)"
+lemma dvd_mult [simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
   by (auto intro!: mult.left_commute dvdI elim!: dvdE)
 
-lemma dvd_mult2 [simp]:
-  "a dvd b \<Longrightarrow> a dvd (b * c)"
+lemma dvd_mult2 [simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
   using dvd_mult [of a b c] by (simp add: ac_simps)
 
-lemma dvd_triv_right [simp]:
-  "a dvd b * a"
+lemma dvd_triv_right [simp]: "a dvd b * a"
   by (rule dvd_mult) (rule dvd_refl)
 
-lemma dvd_triv_left [simp]:
-  "a dvd a * b"
+lemma dvd_triv_left [simp]: "a dvd a * b"
   by (rule dvd_mult2) (rule dvd_refl)
 
 lemma mult_dvd_mono:
@@ -194,12 +178,10 @@
   then show ?thesis ..
 qed
 
-lemma dvd_mult_left:
-  "a * b dvd c \<Longrightarrow> a dvd c"
+lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
   by (simp add: dvd_def mult.assoc) blast
 
-lemma dvd_mult_right:
-  "a * b dvd c \<Longrightarrow> b dvd c"
+lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
   using dvd_mult_left [of b a c] by (simp add: ac_simps)
 
 end
@@ -209,18 +191,15 @@
 
 subclass semiring_1 ..
 
-lemma dvd_0_left_iff [simp]:
-  "0 dvd a \<longleftrightarrow> a = 0"
+lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"
   by (auto intro: dvd_refl elim!: dvdE)
 
-lemma dvd_0_right [iff]:
-  "a dvd 0"
+lemma dvd_0_right [iff]: "a dvd 0"
 proof
   show "0 = a * 0" by simp
 qed
 
-lemma dvd_0_left:
-  "0 dvd a \<Longrightarrow> a = 0"
+lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
   by simp
 
 lemma dvd_add [simp]:
@@ -245,8 +224,8 @@
 
 end
 
-class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add +
-                               zero_neq_one + comm_monoid_mult +
+class comm_semiring_1_cancel =
+  comm_semiring + cancel_comm_monoid_add + zero_neq_one + comm_monoid_mult +
   assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
 begin
 
@@ -254,16 +233,15 @@
 subclass comm_semiring_0_cancel ..
 subclass comm_semiring_1 ..
 
-lemma left_diff_distrib' [algebra_simps]:
-  "(b - c) * a = b * a - c * a"
+lemma left_diff_distrib' [algebra_simps]: "(b - c) * a = b * a - c * a"
   by (simp add: algebra_simps)
 
-lemma dvd_add_times_triv_left_iff [simp]:
-  "a dvd c * a + b \<longleftrightarrow> a dvd b"
+lemma dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \<longleftrightarrow> a dvd b"
 proof -
   have "a dvd a * c + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")
   proof
-    assume ?Q then show ?P by simp
+    assume ?Q
+    then show ?P by simp
   next
     assume ?P
     then obtain d where "a * c + b = a * d" ..
@@ -275,23 +253,21 @@
   then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps)
 qed
 
-lemma dvd_add_times_triv_right_iff [simp]:
-  "a dvd b + c * a \<longleftrightarrow> a dvd b"
+lemma dvd_add_times_triv_right_iff [simp]: "a dvd b + c * a \<longleftrightarrow> a dvd b"
   using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)
 
-lemma dvd_add_triv_left_iff [simp]:
-  "a dvd a + b \<longleftrightarrow> a dvd b"
+lemma dvd_add_triv_left_iff [simp]: "a dvd a + b \<longleftrightarrow> a dvd b"
   using dvd_add_times_triv_left_iff [of a 1 b] by simp
 
-lemma dvd_add_triv_right_iff [simp]:
-  "a dvd b + a \<longleftrightarrow> a dvd b"
+lemma dvd_add_triv_right_iff [simp]: "a dvd b + a \<longleftrightarrow> a dvd b"
   using dvd_add_times_triv_right_iff [of a b 1] by simp
 
 lemma dvd_add_right_iff:
   assumes "a dvd b"
   shows "a dvd b + c \<longleftrightarrow> a dvd c" (is "?P \<longleftrightarrow> ?Q")
 proof
-  assume ?P then obtain d where "b + c = a * d" ..
+  assume ?P
+  then obtain d where "b + c = a * d" ..
   moreover from \<open>a dvd b\<close> obtain e where "b = a * e" ..
   ultimately have "a * e + c = a * d" by simp
   then have "a * e + c - a * e = a * d - a * e" by simp
@@ -299,13 +275,12 @@
   then have "c = a * (d - e)" by (simp add: algebra_simps)
   then show ?Q ..
 next
-  assume ?Q with assms show ?P by simp
+  assume ?Q
+  with assms show ?P by simp
 qed
 
-lemma dvd_add_left_iff:
-  assumes "a dvd c"
-  shows "a dvd b + c \<longleftrightarrow> a dvd b"
-  using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps)
+lemma dvd_add_left_iff: "a dvd c \<Longrightarrow> a dvd b + c \<longleftrightarrow> a dvd b"
+  using dvd_add_right_iff [of a c b] by (simp add: ac_simps)
 
 end
 
@@ -317,44 +292,38 @@
 text \<open>Distribution rules\<close>
 
 lemma minus_mult_left: "- (a * b) = - a * b"
-by (rule minus_unique) (simp add: distrib_right [symmetric])
+  by (rule minus_unique) (simp add: distrib_right [symmetric])
 
 lemma minus_mult_right: "- (a * b) = a * - b"
-by (rule minus_unique) (simp add: distrib_left [symmetric])
+  by (rule minus_unique) (simp add: distrib_left [symmetric])
 
-text\<open>Extract signs from products\<close>
+text \<open>Extract signs from products\<close>
 lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
 lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
 
 lemma minus_mult_minus [simp]: "- a * - b = a * b"
-by simp
+  by simp
 
 lemma minus_mult_commute: "- a * b = a * - b"
-by simp
+  by simp
 
-lemma right_diff_distrib [algebra_simps]:
-  "a * (b - c) = a * b - a * c"
+lemma right_diff_distrib [algebra_simps]: "a * (b - c) = a * b - a * c"
   using distrib_left [of a b "-c "] by simp
 
-lemma left_diff_distrib [algebra_simps]:
-  "(a - b) * c = a * c - b * c"
+lemma left_diff_distrib [algebra_simps]: "(a - b) * c = a * c - b * c"
   using distrib_right [of a "- b" c] by simp
 
-lemmas ring_distribs =
-  distrib_left distrib_right left_diff_distrib right_diff_distrib
+lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib
 
-lemma eq_add_iff1:
-  "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
-by (simp add: algebra_simps)
+lemma eq_add_iff1: "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
+  by (simp add: algebra_simps)
 
-lemma eq_add_iff2:
-  "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
-by (simp add: algebra_simps)
+lemma eq_add_iff2: "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
+  by (simp add: algebra_simps)
 
 end
 
-lemmas ring_distribs =
-  distrib_left distrib_right left_diff_distrib right_diff_distrib
+lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib
 
 class comm_ring = comm_semiring + ab_group_add
 begin
@@ -362,8 +331,7 @@
 subclass ring ..
 subclass comm_semiring_0_cancel ..
 
-lemma square_diff_square_factored:
-  "x * x - y * y = (x + y) * (x - y)"
+lemma square_diff_square_factored: "x * x - y * y = (x + y) * (x - y)"
   by (simp add: algebra_simps)
 
 end
@@ -373,8 +341,7 @@
 
 subclass semiring_1_cancel ..
 
-lemma square_diff_one_factored:
-  "x * x - 1 = (x + 1) * (x - 1)"
+lemma square_diff_one_factored: "x * x - 1 = (x + 1) * (x - 1)"
   by (simp add: algebra_simps)
 
 end
@@ -410,8 +377,7 @@
   then show "- x dvd y" ..
 qed
 
-lemma dvd_diff [simp]:
-  "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
+lemma dvd_diff [simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
   using dvd_add [of x y "- z"] by simp
 
 end
@@ -424,19 +390,20 @@
   assumes "a * b = 0"
   shows "a = 0 \<or> b = 0"
 proof (rule classical)
-  assume "\<not> (a = 0 \<or> b = 0)"
+  assume "\<not> ?thesis"
   then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   with no_zero_divisors have "a * b \<noteq> 0" by blast
   with assms show ?thesis by simp
 qed
 
-lemma mult_eq_0_iff [simp]:
-  shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
+lemma mult_eq_0_iff [simp]: "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
 proof (cases "a = 0 \<or> b = 0")
-  case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
+  case False
+  then have "a \<noteq> 0" and "b \<noteq> 0" by auto
     then show ?thesis using no_zero_divisors by simp
 next
-  case True then show ?thesis by auto
+  case True
+  then show ?thesis by auto
 qed
 
 end
@@ -448,12 +415,10 @@
     and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
 begin
 
-lemma mult_left_cancel:
-  "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
+lemma mult_left_cancel: "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
   by simp
 
-lemma mult_right_cancel:
-  "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"
+lemma mult_right_cancel: "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"
   by simp
 
 end
@@ -483,32 +448,27 @@
 
 subclass semiring_1_no_zero_divisors ..
 
-lemma square_eq_1_iff:
-  "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
+lemma square_eq_1_iff: "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
 proof -
   have "(x - 1) * (x + 1) = x * x - 1"
     by (simp add: algebra_simps)
-  hence "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
+  then have "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
     by simp
-  thus ?thesis
+  then show ?thesis
     by (simp add: eq_neg_iff_add_eq_0)
 qed
 
-lemma mult_cancel_right1 [simp]:
-  "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
-by (insert mult_cancel_right [of 1 c b], force)
+lemma mult_cancel_right1 [simp]: "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
+  using mult_cancel_right [of 1 c b] by auto
 
-lemma mult_cancel_right2 [simp]:
-  "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
-by (insert mult_cancel_right [of a c 1], simp)
+lemma mult_cancel_right2 [simp]: "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
+  using mult_cancel_right [of a c 1] by simp
 
-lemma mult_cancel_left1 [simp]:
-  "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
-by (insert mult_cancel_left [of c 1 b], force)
+lemma mult_cancel_left1 [simp]: "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
+  using mult_cancel_left [of c 1 b] by force
 
-lemma mult_cancel_left2 [simp]:
-  "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
-by (insert mult_cancel_left [of c a 1], simp)
+lemma mult_cancel_left2 [simp]: "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
+  using mult_cancel_left [of c a 1] by simp
 
 end
 
@@ -526,8 +486,7 @@
 
 subclass ring_1_no_zero_divisors ..
 
-lemma dvd_mult_cancel_right [simp]:
-  "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
+lemma dvd_mult_cancel_right [simp]: "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
 proof -
   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
     unfolding dvd_def by (simp add: ac_simps)
@@ -536,8 +495,7 @@
   finally show ?thesis .
 qed
 
-lemma dvd_mult_cancel_left [simp]:
-  "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
+lemma dvd_mult_cancel_left [simp]: "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
 proof -
   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
     unfolding dvd_def by (simp add: ac_simps)
@@ -562,15 +520,12 @@
 
 text \<open>
   The theory of partially ordered rings is taken from the books:
-  \begin{itemize}
-  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
-  \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
-  \end{itemize}
+    \<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979
+    \<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
+
   Most of the used notions can also be looked up in
-  \begin{itemize}
-  \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
-  \item \emph{Algebra I} by van der Waerden, Springer.
-  \end{itemize}
+    \<^item> @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
+    \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
 \<close>
 
 class divide =
@@ -605,49 +560,45 @@
   assumes divide_zero [simp]: "a div 0 = 0"
 begin
 
-lemma nonzero_mult_divide_cancel_left [simp]:
-  "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
+lemma nonzero_mult_divide_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
   using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
 
 subclass semiring_no_zero_divisors_cancel
 proof
-  fix a b c
-  { fix a b c
-    show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
-    proof (cases "c = 0")
-      case True then show ?thesis by simp
-    next
-      case False
-      { assume "a * c = b * c"
-        then have "a * c div c = b * c div c"
-          by simp
-        with False have "a = b"
-          by simp
-      } then show ?thesis by auto
-    qed
-  }
-  from this [of a c b]
-  show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
-    by (simp add: ac_simps)
+  show *: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" for a b c
+  proof (cases "c = 0")
+    case True
+    then show ?thesis by simp
+  next
+    case False
+    {
+      assume "a * c = b * c"
+      then have "a * c div c = b * c div c"
+        by simp
+      with False have "a = b"
+        by simp
+    }
+    then show ?thesis by auto
+  qed
+  show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" for a b c
+    using * [of a c b] by (simp add: ac_simps)
 qed
 
-lemma div_self [simp]:
-  assumes "a \<noteq> 0"
-  shows "a div a = 1"
-  using assms nonzero_mult_divide_cancel_left [of a 1] by simp
+lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
+  using nonzero_mult_divide_cancel_left [of a 1] by simp
 
-lemma divide_zero_left [simp]:
-  "0 div a = 0"
+lemma divide_zero_left [simp]: "0 div a = 0"
 proof (cases "a = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
-  case False then have "a * 0 div a = 0"
+  case False
+  then have "a * 0 div a = 0"
     by (rule nonzero_mult_divide_cancel_left)
   then show ?thesis by simp
 qed
 
-lemma divide_1 [simp]:
-  "a div 1 = a"
+lemma divide_1 [simp]: "a div 1 = a"
   using nonzero_mult_divide_cancel_left [of 1 a] by simp
 
 end
@@ -668,11 +619,13 @@
   assumes "a \<noteq> 0"
   shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
 proof
-  assume ?P then obtain d where "a * c = a * b * d" ..
+  assume ?P
+  then obtain d where "a * c = a * b * d" ..
   with assms have "c = b * d" by (simp add: ac_simps)
   then show ?Q ..
 next
-  assume ?Q then obtain d where "c = b * d" ..
+  assume ?Q
+  then obtain d where "c = b * d" ..
   then have "a * c = a * b * d" by (simp add: ac_simps)
   then show ?P ..
 qed
@@ -680,7 +633,7 @@
 lemma dvd_times_right_cancel_iff [simp]:
   assumes "a \<noteq> 0"
   shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
-using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
+  using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
 
 lemma div_dvd_iff_mult:
   assumes "b \<noteq> 0" and "b dvd a"
@@ -702,7 +655,8 @@
   assumes "a dvd b" and "a dvd c"
   shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
 proof (cases "a = 0")
-  case True with assms show ?thesis by simp
+  case True
+  with assms show ?thesis by simp
 next
   case False
   moreover from assms obtain k l where "b = a * k" and "c = a * l"
@@ -714,7 +668,8 @@
   assumes "c dvd a" and "c dvd b"
   shows "(a + b) div c = a div c + b div c"
 proof (cases "c = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
   case False
   moreover from assms obtain k l where "a = c * k" and "b = c * l"
@@ -729,7 +684,8 @@
   assumes "b dvd a" and "d dvd c"
   shows "(a div b) * (c div d) = (a * c) div (b * d)"
 proof (cases "b = 0 \<or> c = 0")
-  case True with assms show ?thesis by auto
+  case True
+  with assms show ?thesis by auto
 next
   case False
   moreover from assms obtain k l where "a = b * k" and "c = d * l"
@@ -748,42 +704,39 @@
 next
   assume "b div a = c"
   then have "b div a * a = c * a" by simp
-  moreover from \<open>a \<noteq> 0\<close> \<open>a dvd b\<close> have "b div a * a = b"
+  moreover from assms have "b div a * a = b"
     by (auto elim!: dvdE simp add: ac_simps)
   ultimately show "b = c * a" by simp
 qed
 
-lemma dvd_div_mult_self [simp]:
-  "a dvd b \<Longrightarrow> b div a * a = b"
+lemma dvd_div_mult_self [simp]: "a dvd b \<Longrightarrow> b div a * a = b"
   by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
 
-lemma dvd_mult_div_cancel [simp]:
-  "a dvd b \<Longrightarrow> a * (b div a) = b"
+lemma dvd_mult_div_cancel [simp]: "a dvd b \<Longrightarrow> a * (b div a) = b"
   using dvd_div_mult_self [of a b] by (simp add: ac_simps)
 
 lemma div_mult_swap:
   assumes "c dvd b"
   shows "a * (b div c) = (a * b) div c"
 proof (cases "c = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
-  case False from assms obtain d where "b = c * d" ..
+  case False
+  from assms obtain d where "b = c * d" ..
   moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"
     by simp
   ultimately show ?thesis by (simp add: ac_simps)
 qed
 
-lemma dvd_div_mult:
-  assumes "c dvd b"
-  shows "b div c * a = (b * a) div c"
-  using assms div_mult_swap [of c b a] by (simp add: ac_simps)
+lemma dvd_div_mult: "c dvd b \<Longrightarrow> b div c * a = (b * a) div c"
+  using div_mult_swap [of c b a] by (simp add: ac_simps)
 
 lemma dvd_div_mult2_eq:
   assumes "b * c dvd a"
   shows "a div (b * c) = a div b div c"
-using assms proof
-  fix k
-  assume "a = b * c * k"
+proof -
+  from assms obtain k where "a = b * c * k" ..
   then show ?thesis
     by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
 qed
@@ -808,15 +761,12 @@
 text \<open>Units: invertible elements in a ring\<close>
 
 abbreviation is_unit :: "'a \<Rightarrow> bool"
-where
-  "is_unit a \<equiv> a dvd 1"
+  where "is_unit a \<equiv> a dvd 1"
 
-lemma not_is_unit_0 [simp]:
-  "\<not> is_unit 0"
+lemma not_is_unit_0 [simp]: "\<not> is_unit 0"
   by simp
 
-lemma unit_imp_dvd [dest]:
-  "is_unit b \<Longrightarrow> b dvd a"
+lemma unit_imp_dvd [dest]: "is_unit b \<Longrightarrow> b dvd a"
   by (rule dvd_trans [of _ 1]) simp_all
 
 lemma unit_dvdE:
@@ -829,8 +779,7 @@
   ultimately show thesis using that by blast
 qed
 
-lemma dvd_unit_imp_unit:
-  "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
+lemma dvd_unit_imp_unit: "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
   by (rule dvd_trans)
 
 lemma unit_div_1_unit [simp, intro]:
@@ -849,27 +798,24 @@
 proof (rule that)
   define b where "b = 1 div a"
   then show "1 div a = b" by simp
-  from b_def \<open>is_unit a\<close> show "is_unit b" by simp
-  from \<open>is_unit a\<close> and \<open>is_unit b\<close> show "a \<noteq> 0" and "b \<noteq> 0" by auto
-  from b_def \<open>is_unit a\<close> show "a * b = 1" by simp
+  from assms b_def show "is_unit b" by simp
+  with assms show "a \<noteq> 0" and "b \<noteq> 0" by auto
+  from assms b_def show "a * b = 1" by simp
   then have "1 = a * b" ..
   with b_def \<open>b \<noteq> 0\<close> show "1 div b = a" by simp
-  from \<open>is_unit a\<close> have "a dvd c" ..
+  from assms have "a dvd c" ..
   then obtain d where "c = a * d" ..
   with \<open>a \<noteq> 0\<close> \<open>a * b = 1\<close> show "c div a = c * b"
     by (simp add: mult.assoc mult.left_commute [of a])
 qed
 
-lemma unit_prod [intro]:
-  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
+lemma unit_prod [intro]: "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
   by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
 
-lemma is_unit_mult_iff:
-  "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" (is "?P \<longleftrightarrow> ?Q")
+lemma is_unit_mult_iff: "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b"
   by (auto dest: dvd_mult_left dvd_mult_right)
 
-lemma unit_div [intro]:
-  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
+lemma unit_div [intro]: "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
   by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
 
 lemma mult_unit_dvd_iff:
@@ -894,7 +840,8 @@
   assume "a dvd c * b"
   with assms have "c * b dvd c * (b * (1 div b))"
     by (subst mult_assoc [symmetric]) simp
-  also from \<open>is_unit b\<close> have "b * (1 div b) = 1" by (rule is_unitE) simp
+  also from assms have "b * (1 div b) = 1"
+    by (rule is_unitE) simp
   finally have "c * b dvd c" by simp
   with \<open>a dvd c * b\<close> show "a dvd c" by (rule dvd_trans)
 next
@@ -902,52 +849,40 @@
   then show "a dvd c * b" by simp
 qed
 
-lemma div_unit_dvd_iff:
-  "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
+lemma div_unit_dvd_iff: "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
   by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
 
-lemma dvd_div_unit_iff:
-  "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
+lemma dvd_div_unit_iff: "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
   by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
 
 lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
-  dvd_mult_unit_iff dvd_div_unit_iff \<comment> \<open>FIXME consider fact collection\<close>
+  dvd_mult_unit_iff dvd_div_unit_iff  (* FIXME consider named_theorems *)
 
-lemma unit_mult_div_div [simp]:
-  "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
+lemma unit_mult_div_div [simp]: "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
   by (erule is_unitE [of _ b]) simp
 
-lemma unit_div_mult_self [simp]:
-  "is_unit a \<Longrightarrow> b div a * a = b"
+lemma unit_div_mult_self [simp]: "is_unit a \<Longrightarrow> b div a * a = b"
   by (rule dvd_div_mult_self) auto
 
-lemma unit_div_1_div_1 [simp]:
-  "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
+lemma unit_div_1_div_1 [simp]: "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
   by (erule is_unitE) simp
 
-lemma unit_div_mult_swap:
-  "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"
+lemma unit_div_mult_swap: "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"
   by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])
 
-lemma unit_div_commute:
-  "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"
+lemma unit_div_commute: "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"
   using unit_div_mult_swap [of b c a] by (simp add: ac_simps)
 
-lemma unit_eq_div1:
-  "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
+lemma unit_eq_div1: "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
   by (auto elim: is_unitE)
 
-lemma unit_eq_div2:
-  "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
+lemma unit_eq_div2: "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
   using unit_eq_div1 [of b c a] by auto
 
-lemma unit_mult_left_cancel:
-  assumes "is_unit a"
-  shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
-  using assms mult_cancel_left [of a b c] by auto
+lemma unit_mult_left_cancel: "is_unit a \<Longrightarrow> a * b = a * c \<longleftrightarrow> b = c"
+  using mult_cancel_left [of a b c] by auto
 
-lemma unit_mult_right_cancel:
-  "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
+lemma unit_mult_right_cancel: "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
   using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)
 
 lemma unit_div_cancel:
@@ -964,7 +899,8 @@
   assumes "is_unit b" and "is_unit c"
   shows "a div (b * c) = a div b div c"
 proof -
-  from assms have "is_unit (b * c)" by (simp add: unit_prod)
+  from assms have "is_unit (b * c)"
+    by (simp add: unit_prod)
   then have "b * c dvd a"
     by (rule unit_imp_dvd)
   then show ?thesis
@@ -1015,58 +951,57 @@
   values rather than associated elements.
 \<close>
 
-lemma unit_factor_dvd [simp]:
-  "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
+lemma unit_factor_dvd [simp]: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
   by (rule unit_imp_dvd) simp
 
-lemma unit_factor_self [simp]:
-  "unit_factor a dvd a"
+lemma unit_factor_self [simp]: "unit_factor a dvd a"
   by (cases "a = 0") simp_all
 
-lemma normalize_mult_unit_factor [simp]:
-  "normalize a * unit_factor a = a"
+lemma normalize_mult_unit_factor [simp]: "normalize a * unit_factor a = a"
   using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
 
-lemma normalize_eq_0_iff [simp]:
-  "normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
+lemma normalize_eq_0_iff [simp]: "normalize a = 0 \<longleftrightarrow> a = 0"
+  (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?P
   moreover have "unit_factor a * normalize a = a" by simp
   ultimately show ?Q by simp
 next
-  assume ?Q then show ?P by simp
+  assume ?Q
+  then show ?P by simp
 qed
 
-lemma unit_factor_eq_0_iff [simp]:
-  "unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
+lemma unit_factor_eq_0_iff [simp]: "unit_factor a = 0 \<longleftrightarrow> a = 0"
+  (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?P
   moreover have "unit_factor a * normalize a = a" by simp
   ultimately show ?Q by simp
 next
-  assume ?Q then show ?P by simp
+  assume ?Q
+  then show ?P by simp
 qed
 
 lemma is_unit_unit_factor:
-  assumes "is_unit a" shows "unit_factor a = a"
+  assumes "is_unit a"
+  shows "unit_factor a = a"
 proof -
   from assms have "normalize a = 1" by (rule is_unit_normalize)
   moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
   ultimately show ?thesis by simp
 qed
 
-lemma unit_factor_1 [simp]:
-  "unit_factor 1 = 1"
+lemma unit_factor_1 [simp]: "unit_factor 1 = 1"
   by (rule is_unit_unit_factor) simp
 
-lemma normalize_1 [simp]:
-  "normalize 1 = 1"
+lemma normalize_1 [simp]: "normalize 1 = 1"
   by (rule is_unit_normalize) simp
 
-lemma normalize_1_iff:
-  "normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
+lemma normalize_1_iff: "normalize a = 1 \<longleftrightarrow> is_unit a"
+  (is "?P \<longleftrightarrow> ?Q")
 proof
-  assume ?Q then show ?P by (rule is_unit_normalize)
+  assume ?Q
+  then show ?P by (rule is_unit_normalize)
 next
   assume ?P
   then have "a \<noteq> 0" by auto
@@ -1079,32 +1014,34 @@
   ultimately show ?Q by simp
 qed
 
-lemma div_normalize [simp]:
-  "a div normalize a = unit_factor a"
+lemma div_normalize [simp]: "a div normalize a = unit_factor a"
 proof (cases "a = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
-  case False then have "normalize a \<noteq> 0" by simp
+  case False
+  then have "normalize a \<noteq> 0" by simp
   with nonzero_mult_divide_cancel_right
   have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
   then show ?thesis by simp
 qed
 
-lemma div_unit_factor [simp]:
-  "a div unit_factor a = normalize a"
+lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
 proof (cases "a = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
-  case False then have "unit_factor a \<noteq> 0" by simp
+  case False
+  then have "unit_factor a \<noteq> 0" by simp
   with nonzero_mult_divide_cancel_left
   have "unit_factor a * normalize a div unit_factor a = normalize a" by blast
   then show ?thesis by simp
 qed
 
-lemma normalize_div [simp]:
-  "normalize a div a = 1 div unit_factor a"
+lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
 proof (cases "a = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
   case False
   have "normalize a div a = normalize a div (unit_factor a * normalize a)"
@@ -1114,62 +1051,64 @@
   finally show ?thesis .
 qed
 
-lemma mult_one_div_unit_factor [simp]:
-  "a * (1 div unit_factor b) = a div unit_factor b"
+lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
   by (cases "b = 0") simp_all
 
-lemma normalize_mult:
-  "normalize (a * b) = normalize a * normalize b"
+lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
 proof (cases "a = 0 \<or> b = 0")
-  case True then show ?thesis by auto
+  case True
+  then show ?thesis by auto
 next
   case False
   from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" .
-  then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp
-  also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps)
+  then have "normalize (a * b) = a * b div unit_factor (a * b)"
+    by simp
+  also have "\<dots> = a * b div unit_factor (b * a)"
+    by (simp add: ac_simps)
   also have "\<dots> = a * b div unit_factor b div unit_factor a"
     using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
   also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
     using False by (subst unit_div_mult_swap) simp_all
   also have "\<dots> = normalize a * normalize b"
-    using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
+    using False
+    by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
   finally show ?thesis .
 qed
 
-lemma unit_factor_idem [simp]:
-  "unit_factor (unit_factor a) = unit_factor a"
+lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a"
   by (cases "a = 0") (auto intro: is_unit_unit_factor)
 
-lemma normalize_unit_factor [simp]:
-  "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
+lemma normalize_unit_factor [simp]: "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
   by (rule is_unit_normalize) simp
 
-lemma normalize_idem [simp]:
-  "normalize (normalize a) = normalize a"
+lemma normalize_idem [simp]: "normalize (normalize a) = normalize a"
 proof (cases "a = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
   case False
-  have "normalize a = normalize (unit_factor a * normalize a)" by simp
+  have "normalize a = normalize (unit_factor a * normalize a)"
+    by simp
   also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
     by (simp only: normalize_mult)
-  finally show ?thesis using False by simp_all
+  finally show ?thesis
+    using False by simp_all
 qed
 
 lemma unit_factor_normalize [simp]:
   assumes "a \<noteq> 0"
   shows "unit_factor (normalize a) = 1"
 proof -
-  from assms have "normalize a \<noteq> 0" by simp
+  from assms have *: "normalize a \<noteq> 0"
+    by simp
   have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
     by (simp only: unit_factor_mult_normalize)
   then have "unit_factor (normalize a) * normalize a = normalize a"
     by simp
-  with \<open>normalize a \<noteq> 0\<close>
-  have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
+  with * have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
     by simp
-  with \<open>normalize a \<noteq> 0\<close>
-  show ?thesis by simp
+  with * show ?thesis
+    by simp
 qed
 
 lemma dvd_unit_factor_div:
@@ -1196,8 +1135,7 @@
     by (cases "b = 0") (simp_all add: normalize_mult)
 qed
 
-lemma normalize_dvd_iff [simp]:
-  "normalize a dvd b \<longleftrightarrow> a dvd b"
+lemma normalize_dvd_iff [simp]: "normalize a dvd b \<longleftrightarrow> a dvd b"
 proof -
   have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
     using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
@@ -1205,8 +1143,7 @@
   then show ?thesis by simp
 qed
 
-lemma dvd_normalize_iff [simp]:
-  "a dvd normalize b \<longleftrightarrow> a dvd b"
+lemma dvd_normalize_iff [simp]: "a dvd normalize b \<longleftrightarrow> a dvd b"
 proof -
   have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
     using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
@@ -1226,36 +1163,38 @@
   assumes "a dvd b" and "b dvd a"
   shows "normalize a = normalize b"
 proof (cases "a = 0 \<or> b = 0")
-  case True with assms show ?thesis by auto
+  case True
+  with assms show ?thesis by auto
 next
   case False
   from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..
   moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..
-  ultimately have "b * 1 = b * (c * d)" by (simp add: ac_simps)
+  ultimately have "b * 1 = b * (c * d)"
+    by (simp add: ac_simps)
   with False have "1 = c * d"
     unfolding mult_cancel_left by simp
-  then have "is_unit c" and "is_unit d" by auto
-  with a b show ?thesis by (simp add: normalize_mult is_unit_normalize)
+  then have "is_unit c" and "is_unit d"
+    by auto
+  with a b show ?thesis
+    by (simp add: normalize_mult is_unit_normalize)
 qed
 
-lemma associatedD1:
-  "normalize a = normalize b \<Longrightarrow> a dvd b"
+lemma associatedD1: "normalize a = normalize b \<Longrightarrow> a dvd b"
   using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]
   by simp
 
-lemma associatedD2:
-  "normalize a = normalize b \<Longrightarrow> b dvd a"
+lemma associatedD2: "normalize a = normalize b \<Longrightarrow> b dvd a"
   using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]
   by simp
 
-lemma associated_unit:
-  "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
+lemma associated_unit: "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
   using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
 
-lemma associated_iff_dvd:
-  "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a" (is "?P \<longleftrightarrow> ?Q")
+lemma associated_iff_dvd: "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a"
+  (is "?P \<longleftrightarrow> ?Q")
 proof
-  assume ?Q then show ?P by (auto intro!: associatedI)
+  assume ?Q
+  then show ?P by (auto intro!: associatedI)
 next
   assume ?P
   then have "unit_factor a * normalize a = unit_factor a * normalize b"
@@ -1264,7 +1203,8 @@
     by (simp add: ac_simps)
   show ?Q
   proof (cases "a = 0 \<or> b = 0")
-    case True with \<open>?P\<close> show ?thesis by auto
+    case True
+    with \<open>?P\<close> show ?thesis by auto
   next
     case False
     then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
@@ -1291,38 +1231,38 @@
   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
 begin
 
-lemma mult_mono:
-  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
-apply (erule mult_right_mono [THEN order_trans], assumption)
-apply (erule mult_left_mono, assumption)
-done
+lemma mult_mono: "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
+  apply (erule (1) mult_right_mono [THEN order_trans])
+  apply (erule (1) mult_left_mono)
+  done
 
-lemma mult_mono':
-  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
-apply (rule mult_mono)
-apply (fast intro: order_trans)+
-done
+lemma mult_mono': "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
+  apply (rule mult_mono)
+  apply (fast intro: order_trans)+
+  done
 
 end
 
 class ordered_semiring_0 = semiring_0 + ordered_semiring
 begin
 
-lemma mult_nonneg_nonneg[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
-using mult_left_mono [of 0 b a] by simp
+lemma mult_nonneg_nonneg [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
+  using mult_left_mono [of 0 b a] by simp
 
 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
-using mult_left_mono [of b 0 a] by simp
+  using mult_left_mono [of b 0 a] by simp
 
 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
-using mult_right_mono [of a 0 b] by simp
+  using mult_right_mono [of a 0 b] by simp
 
 text \<open>Legacy - use \<open>mult_nonpos_nonneg\<close>\<close>
 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
-by (drule mult_right_mono [of b 0], auto)
+  apply (drule mult_right_mono [of b 0])
+  apply auto
+  done
 
 lemma split_mult_neg_le: "(0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
-by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
+  by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
 
 end
 
@@ -1341,44 +1281,34 @@
 
 subclass ordered_cancel_comm_monoid_add ..
 
-lemma mult_left_less_imp_less:
-  "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
-by (force simp add: mult_left_mono not_le [symmetric])
+lemma mult_left_less_imp_less: "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
+  by (force simp add: mult_left_mono not_le [symmetric])
 
-lemma mult_right_less_imp_less:
-  "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
-by (force simp add: mult_right_mono not_le [symmetric])
+lemma mult_right_less_imp_less: "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
+  by (force simp add: mult_right_mono not_le [symmetric])
 
-lemma less_eq_add_cancel_left_greater_eq_zero [simp]:
-  "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
+lemma less_eq_add_cancel_left_greater_eq_zero [simp]: "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
   using add_le_cancel_left [of a 0 b] by simp
 
-lemma less_eq_add_cancel_left_less_eq_zero [simp]:
-  "a + b \<le> a \<longleftrightarrow> b \<le> 0"
+lemma less_eq_add_cancel_left_less_eq_zero [simp]: "a + b \<le> a \<longleftrightarrow> b \<le> 0"
   using add_le_cancel_left [of a b 0] by simp
 
-lemma less_eq_add_cancel_right_greater_eq_zero [simp]:
-  "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
+lemma less_eq_add_cancel_right_greater_eq_zero [simp]: "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
   using add_le_cancel_right [of 0 a b] by simp
 
-lemma less_eq_add_cancel_right_less_eq_zero [simp]:
-  "b + a \<le> a \<longleftrightarrow> b \<le> 0"
+lemma less_eq_add_cancel_right_less_eq_zero [simp]: "b + a \<le> a \<longleftrightarrow> b \<le> 0"
   using add_le_cancel_right [of b a 0] by simp
 
-lemma less_add_cancel_left_greater_zero [simp]:
-  "a < a + b \<longleftrightarrow> 0 < b"
+lemma less_add_cancel_left_greater_zero [simp]: "a < a + b \<longleftrightarrow> 0 < b"
   using add_less_cancel_left [of a 0 b] by simp
 
-lemma less_add_cancel_left_less_zero [simp]:
-  "a + b < a \<longleftrightarrow> b < 0"
+lemma less_add_cancel_left_less_zero [simp]: "a + b < a \<longleftrightarrow> b < 0"
   using add_less_cancel_left [of a b 0] by simp
 
-lemma less_add_cancel_right_greater_zero [simp]:
-  "a < b + a \<longleftrightarrow> 0 < b"
+lemma less_add_cancel_right_greater_zero [simp]: "a < b + a \<longleftrightarrow> 0 < b"
   using add_less_cancel_right [of 0 a b] by simp
 
-lemma less_add_cancel_right_less_zero [simp]:
-  "b + a < a \<longleftrightarrow> b < 0"
+lemma less_add_cancel_right_less_zero [simp]: "b + a < a \<longleftrightarrow> b < 0"
   using add_less_cancel_right [of b a 0] by simp
 
 end
@@ -1392,7 +1322,8 @@
 proof-
   from assms have "u * x + v * y \<le> u * a + v * a"
     by (simp add: add_mono mult_left_mono)
-  thus ?thesis using assms unfolding distrib_right[symmetric] by simp
+  with assms show ?thesis
+    unfolding distrib_right[symmetric] by simp
 qed
 
 end
@@ -1416,80 +1347,79 @@
     using mult_strict_right_mono by (cases "c = 0") auto
 qed
 
-lemma mult_left_le_imp_le:
-  "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
-by (force simp add: mult_strict_left_mono _not_less [symmetric])
+lemma mult_left_le_imp_le: "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
+  by (auto simp add: mult_strict_left_mono _not_less [symmetric])
 
-lemma mult_right_le_imp_le:
-  "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
-by (force simp add: mult_strict_right_mono not_less [symmetric])
+lemma mult_right_le_imp_le: "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
+  by (auto simp add: mult_strict_right_mono not_less [symmetric])
 
 lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
-using mult_strict_left_mono [of 0 b a] by simp
+  using mult_strict_left_mono [of 0 b a] by simp
 
 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
-using mult_strict_left_mono [of b 0 a] by simp
+  using mult_strict_left_mono [of b 0 a] by simp
 
 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
-using mult_strict_right_mono [of a 0 b] by simp
+  using mult_strict_right_mono [of a 0 b] by simp
 
 text \<open>Legacy - use \<open>mult_neg_pos\<close>\<close>
 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
-by (drule mult_strict_right_mono [of b 0], auto)
-
-lemma zero_less_mult_pos:
-  "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
-apply (cases "b\<le>0")
- apply (auto simp add: le_less not_less)
-apply (drule_tac mult_pos_neg [of a b])
- apply (auto dest: less_not_sym)
-done
+  apply (drule mult_strict_right_mono [of b 0])
+  apply auto
+  done
 
-lemma zero_less_mult_pos2:
-  "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
-apply (cases "b\<le>0")
- apply (auto simp add: le_less not_less)
-apply (drule_tac mult_pos_neg2 [of a b])
- apply (auto dest: less_not_sym)
-done
+lemma zero_less_mult_pos: "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
+  apply (cases "b \<le> 0")
+   apply (auto simp add: le_less not_less)
+  apply (drule_tac mult_pos_neg [of a b])
+   apply (auto dest: less_not_sym)
+  done
 
-text\<open>Strict monotonicity in both arguments\<close>
+lemma zero_less_mult_pos2: "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
+  apply (cases "b \<le> 0")
+   apply (auto simp add: le_less not_less)
+  apply (drule_tac mult_pos_neg2 [of a b])
+   apply (auto dest: less_not_sym)
+  done
+
+text \<open>Strict monotonicity in both arguments\<close>
 lemma mult_strict_mono:
   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
   shows "a * c < b * d"
-  using assms apply (cases "c=0")
-  apply (simp)
+  using assms
+  apply (cases "c = 0")
+  apply simp
   apply (erule mult_strict_right_mono [THEN less_trans])
-  apply (force simp add: le_less)
-  apply (erule mult_strict_left_mono, assumption)
+  apply (auto simp add: le_less)
+  apply (erule (1) mult_strict_left_mono)
   done
 
-text\<open>This weaker variant has more natural premises\<close>
+text \<open>This weaker variant has more natural premises\<close>
 lemma mult_strict_mono':
   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
   shows "a * c < b * d"
-by (rule mult_strict_mono) (insert assms, auto)
+  by (rule mult_strict_mono) (insert assms, auto)
 
 lemma mult_less_le_imp_less:
   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
   shows "a * c < b * d"
-  using assms apply (subgoal_tac "a * c < b * c")
+  using assms
+  apply (subgoal_tac "a * c < b * c")
   apply (erule less_le_trans)
   apply (erule mult_left_mono)
   apply simp
-  apply (erule mult_strict_right_mono)
-  apply assumption
+  apply (erule (1) mult_strict_right_mono)
   done
 
 lemma mult_le_less_imp_less:
   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
   shows "a * c < b * d"
-  using assms apply (subgoal_tac "a * c \<le> b * c")
+  using assms
+  apply (subgoal_tac "a * c \<le> b * c")
   apply (erule le_less_trans)
   apply (erule mult_strict_left_mono)
   apply simp
-  apply (erule mult_right_mono)
-  apply simp
+  apply (erule (1) mult_right_mono)
   done
 
 end
@@ -1504,9 +1434,9 @@
   shows "u * x + v * y < a"
 proof -
   from assms have "u * x + v * y < u * a + v * a"
-    by (cases "u = 0")
-       (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
-  thus ?thesis using assms unfolding distrib_right[symmetric] by simp
+    by (cases "u = 0") (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
+  with assms show ?thesis
+    unfolding distrib_right[symmetric] by simp
 qed
 
 end
@@ -1519,8 +1449,8 @@
 proof
   fix a b c :: 'a
   assume "a \<le> b" "0 \<le> c"
-  thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
-  thus "a * c \<le> b * c" by (simp only: mult.commute)
+  then show "c * a \<le> c * b" by (rule comm_mult_left_mono)
+  then show "a * c \<le> b * c" by (simp only: mult.commute)
 qed
 
 end
@@ -1542,15 +1472,15 @@
 proof
   fix a b c :: 'a
   assume "a < b" "0 < c"
-  thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
-  thus "a * c < b * c" by (simp only: mult.commute)
+  then show "c * a < c * b" by (rule comm_mult_strict_left_mono)
+  then show "a * c < b * c" by (simp only: mult.commute)
 qed
 
 subclass ordered_cancel_comm_semiring
 proof
   fix a b c :: 'a
   assume "a \<le> b" "0 \<le> c"
-  thus "c * a \<le> c * b"
+  then show "c * a \<le> c * b"
     unfolding le_less
     using mult_strict_left_mono by (cases "c = 0") auto
 qed
@@ -1562,40 +1492,33 @@
 
 subclass ordered_ab_group_add ..
 
-lemma less_add_iff1:
-  "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
-by (simp add: algebra_simps)
+lemma less_add_iff1: "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
+  by (simp add: algebra_simps)
 
-lemma less_add_iff2:
-  "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
-by (simp add: algebra_simps)
+lemma less_add_iff2: "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
+  by (simp add: algebra_simps)
 
-lemma le_add_iff1:
-  "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
-by (simp add: algebra_simps)
+lemma le_add_iff1: "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
+  by (simp add: algebra_simps)
 
-lemma le_add_iff2:
-  "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
-by (simp add: algebra_simps)
+lemma le_add_iff2: "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
+  by (simp add: algebra_simps)
 
-lemma mult_left_mono_neg:
-  "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
+lemma mult_left_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
   apply (drule mult_left_mono [of _ _ "- c"])
   apply simp_all
   done
 
-lemma mult_right_mono_neg:
-  "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
+lemma mult_right_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
   apply (drule mult_right_mono [of _ _ "- c"])
   apply simp_all
   done
 
 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
-using mult_right_mono_neg [of a 0 b] by simp
+  using mult_right_mono_neg [of a 0 b] by simp
 
-lemma split_mult_pos_le:
-  "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
-by (auto simp add: mult_nonpos_nonpos)
+lemma split_mult_pos_le: "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
+  by (auto simp add: mult_nonpos_nonpos)
 
 end
 
@@ -1608,12 +1531,12 @@
 proof
   fix a b
   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
-    by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)
+    by (auto simp add: abs_if not_le not_less algebra_simps
+        simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)
 qed (auto simp add: abs_if)
 
 lemma zero_le_square [simp]: "0 \<le> a * a"
-  using linear [of 0 a]
-  by (auto simp add: mult_nonpos_nonpos)
+  using linear [of 0 a] by (auto simp add: mult_nonpos_nonpos)
 
 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   by (simp add: not_less)
@@ -1621,12 +1544,10 @@
 proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
   by (auto simp add: abs_if split: if_split_asm)
 
-lemma sum_squares_ge_zero:
-  "0 \<le> x * x + y * y"
+lemma sum_squares_ge_zero: "0 \<le> x * x + y * y"
   by (intro add_nonneg_nonneg zero_le_square)
 
-lemma not_sum_squares_lt_zero:
-  "\<not> x * x + y * y < 0"
+lemma not_sum_squares_lt_zero: "\<not> x * x + y * y < 0"
   by (simp add: not_less sum_squares_ge_zero)
 
 end
@@ -1638,40 +1559,49 @@
 subclass linordered_ring ..
 
 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
-using mult_strict_left_mono [of b a "- c"] by simp
+  using mult_strict_left_mono [of b a "- c"] by simp
 
 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
-using mult_strict_right_mono [of b a "- c"] by simp
+  using mult_strict_right_mono [of b a "- c"] by simp
 
 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
-using mult_strict_right_mono_neg [of a 0 b] by simp
+  using mult_strict_right_mono_neg [of a 0 b] by simp
 
 subclass ring_no_zero_divisors
 proof
   fix a b
-  assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
-  assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
+  assume "a \<noteq> 0"
+  then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
+  assume "b \<noteq> 0"
+  then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
   have "a * b < 0 \<or> 0 < a * b"
   proof (cases "a < 0")
-    case True note A' = this
-    show ?thesis proof (cases "b < 0")
-      case True with A'
-      show ?thesis by (auto dest: mult_neg_neg)
+    case A': True
+    show ?thesis
+    proof (cases "b < 0")
+      case True
+      with A' show ?thesis by (auto dest: mult_neg_neg)
     next
-      case False with B have "0 < b" by auto
+      case False
+      with B have "0 < b" by auto
       with A' show ?thesis by (auto dest: mult_strict_right_mono)
     qed
   next
-    case False with A have A': "0 < a" by auto
-    show ?thesis proof (cases "b < 0")
-      case True with A'
-      show ?thesis by (auto dest: mult_strict_right_mono_neg)
+    case False
+    with A have A': "0 < a" by auto
+    show ?thesis
+    proof (cases "b < 0")
+      case True
+      with A' show ?thesis
+        by (auto dest: mult_strict_right_mono_neg)
     next
-      case False with B have "0 < b" by auto
+      case False
+      with B have "0 < b" by auto
       with A' show ?thesis by auto
     qed
   qed
-  then show "a * b \<noteq> 0" by (simp add: neq_iff)
+  then show "a * b \<noteq> 0"
+    by (simp add: neq_iff)
 qed
 
 lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
@@ -1681,84 +1611,66 @@
 lemma zero_le_mult_iff: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
   by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
 
-lemma mult_less_0_iff:
-  "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
-  apply (insert zero_less_mult_iff [of "-a" b])
-  apply force
-  done
+lemma mult_less_0_iff: "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
+  using zero_less_mult_iff [of "- a" b] by auto
 
-lemma mult_le_0_iff:
-  "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
-  apply (insert zero_le_mult_iff [of "-a" b])
-  apply force
-  done
+lemma mult_le_0_iff: "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
+  using zero_le_mult_iff [of "- a" b] by auto
 
-text\<open>Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
-   also with the relations \<open>\<le>\<close> and equality.\<close>
+text \<open>
+  Cancellation laws for @{term "c * a < c * b"} and @{term "a * c < b * c"},
+  also with the relations \<open>\<le>\<close> and equality.
+\<close>
 
-text\<open>These ``disjunction'' versions produce two cases when the comparison is
- an assumption, but effectively four when the comparison is a goal.\<close>
+text \<open>
+  These ``disjunction'' versions produce two cases when the comparison is
+  an assumption, but effectively four when the comparison is a goal.
+\<close>
 
-lemma mult_less_cancel_right_disj:
-  "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
+lemma mult_less_cancel_right_disj: "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   apply (cases "c = 0")
-  apply (auto simp add: neq_iff mult_strict_right_mono
-                      mult_strict_right_mono_neg)
-  apply (auto simp add: not_less
-                      not_le [symmetric, of "a*c"]
-                      not_le [symmetric, of a])
+  apply (auto simp add: neq_iff mult_strict_right_mono mult_strict_right_mono_neg)
+  apply (auto simp add: not_less not_le [symmetric, of "a*c"] not_le [symmetric, of a])
   apply (erule_tac [!] notE)
-  apply (auto simp add: less_imp_le mult_right_mono
-                      mult_right_mono_neg)
+  apply (auto simp add: less_imp_le mult_right_mono mult_right_mono_neg)
   done
 
-lemma mult_less_cancel_left_disj:
-  "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
+lemma mult_less_cancel_left_disj: "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   apply (cases "c = 0")
-  apply (auto simp add: neq_iff mult_strict_left_mono
-                      mult_strict_left_mono_neg)
-  apply (auto simp add: not_less
-                      not_le [symmetric, of "c*a"]
-                      not_le [symmetric, of a])
+  apply (auto simp add: neq_iff mult_strict_left_mono mult_strict_left_mono_neg)
+  apply (auto simp add: not_less not_le [symmetric, of "c * a"] not_le [symmetric, of a])
   apply (erule_tac [!] notE)
-  apply (auto simp add: less_imp_le mult_left_mono
-                      mult_left_mono_neg)
+  apply (auto simp add: less_imp_le mult_left_mono mult_left_mono_neg)
   done
 
-text\<open>The ``conjunction of implication'' lemmas produce two cases when the
-comparison is a goal, but give four when the comparison is an assumption.\<close>
+text \<open>
+  The ``conjunction of implication'' lemmas produce two cases when the
+  comparison is a goal, but give four when the comparison is an assumption.
+\<close>
 
-lemma mult_less_cancel_right:
-  "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
+lemma mult_less_cancel_right: "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
   using mult_less_cancel_right_disj [of a c b] by auto
 
-lemma mult_less_cancel_left:
-  "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
+lemma mult_less_cancel_left: "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
   using mult_less_cancel_left_disj [of c a b] by auto
 
-lemma mult_le_cancel_right:
-   "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
-by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
+lemma mult_le_cancel_right: "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
+  by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
 
-lemma mult_le_cancel_left:
-  "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
-by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
+lemma mult_le_cancel_left: "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
+  by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
 
-lemma mult_le_cancel_left_pos:
-  "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
-by (auto simp: mult_le_cancel_left)
+lemma mult_le_cancel_left_pos: "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
+  by (auto simp: mult_le_cancel_left)
 
-lemma mult_le_cancel_left_neg:
-  "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
-by (auto simp: mult_le_cancel_left)
+lemma mult_le_cancel_left_neg: "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
+  by (auto simp: mult_le_cancel_left)
 
-lemma mult_less_cancel_left_pos:
-  "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
-by (auto simp: mult_less_cancel_left)
+lemma mult_less_cancel_left_pos: "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
+  by (auto simp: mult_less_cancel_left)
 
-lemma mult_less_cancel_left_neg:
-  "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
-by (auto simp: mult_less_cancel_left)
+lemma mult_less_cancel_left_neg: "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
+  by (auto simp: mult_less_cancel_left)
 
 end
 
@@ -1783,19 +1695,19 @@
 begin
 
 subclass zero_neq_one
-  proof qed (insert zero_less_one, blast)
+  by standard (insert zero_less_one, blast)
 
 subclass comm_semiring_1
-  proof qed (rule mult_1_left)
+  by standard (rule mult_1_left)
 
 lemma zero_le_one [simp]: "0 \<le> 1"
-by (rule zero_less_one [THEN less_imp_le])
+  by (rule zero_less_one [THEN less_imp_le])
 
 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
-by (simp add: not_le)
+  by (simp add: not_le)
 
 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
-by (simp add: not_less)
+  by (simp add: not_less)
 
 lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
   using mult_left_mono[of c 1 a] by simp
@@ -1812,8 +1724,7 @@
   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
 begin
 
-subclass linordered_nonzero_semiring
-  proof qed
+subclass linordered_nonzero_semiring ..
 
 text \<open>Addition is the inverse of subtraction.\<close>
 
@@ -1823,31 +1734,31 @@
 lemma add_diff_inverse: "\<not> a < b \<Longrightarrow> b + (a - b) = a"
   by simp
 
-lemma add_le_imp_le_diff:
-  shows "i + k \<le> n \<Longrightarrow> i \<le> n - k"
+lemma add_le_imp_le_diff: "i + k \<le> n \<Longrightarrow> i \<le> n - k"
   apply (subst add_le_cancel_right [where c=k, symmetric])
   apply (frule le_add_diff_inverse2)
   apply (simp only: add.assoc [symmetric])
-  using add_implies_diff by fastforce
+  using add_implies_diff apply fastforce
+  done
 
 lemma add_le_add_imp_diff_le:
-  assumes a1: "i + k \<le> n"
-      and a2: "n \<le> j + k"
-  shows "\<lbrakk>i + k \<le> n; n \<le> j + k\<rbrakk> \<Longrightarrow> n - k \<le> j"
+  assumes 1: "i + k \<le> n"
+    and 2: "n \<le> j + k"
+  shows "i + k \<le> n \<Longrightarrow> n \<le> j + k \<Longrightarrow> n - k \<le> j"
 proof -
   have "n - (i + k) + (i + k) = n"
-    using a1 by simp
+    using 1 by simp
   moreover have "n - k = n - k - i + i"
-    using a1 by (simp add: add_le_imp_le_diff)
+    using 1 by (simp add: add_le_imp_le_diff)
   ultimately show ?thesis
-    using a2
+    using 2
     apply (simp add: add.assoc [symmetric])
-    apply (rule add_le_imp_le_diff [of _ k "j+k", simplified add_diff_cancel_right'])
-    by (simp add: add.commute diff_diff_add)
+    apply (rule add_le_imp_le_diff [of _ k "j + k", simplified add_diff_cancel_right'])
+    apply (simp add: add.commute diff_diff_add)
+    done
 qed
 
-lemma less_1_mult:
-  "1 < m \<Longrightarrow> 1 < n \<Longrightarrow> 1 < m * n"
+lemma less_1_mult: "1 < m \<Longrightarrow> 1 < n \<Longrightarrow> 1 < m * n"
   using mult_strict_mono [of 1 m 1 n] by (simp add: less_trans [OF zero_less_one])
 
 end
@@ -1864,90 +1775,73 @@
 subclass linordered_semidom
 proof
   have "0 \<le> 1 * 1" by (rule zero_le_square)
-  thus "0 < 1" by (simp add: le_less)
-  show "\<And>b a. b \<le> a \<Longrightarrow> a - b + b = a"
+  then show "0 < 1" by (simp add: le_less)
+  show "b \<le> a \<Longrightarrow> a - b + b = a" for a b
     by simp
 qed
 
 lemma linorder_neqE_linordered_idom:
-  assumes "x \<noteq> y" obtains "x < y" | "y < x"
+  assumes "x \<noteq> y"
+  obtains "x < y" | "y < x"
   using assms by (rule neqE)
 
 text \<open>These cancellation simprules also produce two cases when the comparison is a goal.\<close>
 
-lemma mult_le_cancel_right1:
-  "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
-by (insert mult_le_cancel_right [of 1 c b], simp)
+lemma mult_le_cancel_right1: "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
+  using mult_le_cancel_right [of 1 c b] by simp
 
-lemma mult_le_cancel_right2:
-  "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
-by (insert mult_le_cancel_right [of a c 1], simp)
+lemma mult_le_cancel_right2: "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
+  using mult_le_cancel_right [of a c 1] by simp
 
-lemma mult_le_cancel_left1:
-  "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
-by (insert mult_le_cancel_left [of c 1 b], simp)
+lemma mult_le_cancel_left1: "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
+  using mult_le_cancel_left [of c 1 b] by simp
 
-lemma mult_le_cancel_left2:
-  "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
-by (insert mult_le_cancel_left [of c a 1], simp)
+lemma mult_le_cancel_left2: "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
+  using mult_le_cancel_left [of c a 1] by simp
 
-lemma mult_less_cancel_right1:
-  "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
-by (insert mult_less_cancel_right [of 1 c b], simp)
+lemma mult_less_cancel_right1: "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
+  using mult_less_cancel_right [of 1 c b] by simp
 
-lemma mult_less_cancel_right2:
-  "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
-by (insert mult_less_cancel_right [of a c 1], simp)
+lemma mult_less_cancel_right2: "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
+  using mult_less_cancel_right [of a c 1] by simp
 
-lemma mult_less_cancel_left1:
-  "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
-by (insert mult_less_cancel_left [of c 1 b], simp)
+lemma mult_less_cancel_left1: "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
+  using mult_less_cancel_left [of c 1 b] by simp
 
-lemma mult_less_cancel_left2:
-  "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
-by (insert mult_less_cancel_left [of c a 1], simp)
+lemma mult_less_cancel_left2: "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
+  using mult_less_cancel_left [of c a 1] by simp
 
-lemma sgn_sgn [simp]:
-  "sgn (sgn a) = sgn a"
-unfolding sgn_if by simp
+lemma sgn_sgn [simp]: "sgn (sgn a) = sgn a"
+  unfolding sgn_if by simp
 
-lemma sgn_0_0:
-  "sgn a = 0 \<longleftrightarrow> a = 0"
-unfolding sgn_if by simp
+lemma sgn_0_0: "sgn a = 0 \<longleftrightarrow> a = 0"
+  unfolding sgn_if by simp
 
-lemma sgn_1_pos:
-  "sgn a = 1 \<longleftrightarrow> a > 0"
-unfolding sgn_if by simp
+lemma sgn_1_pos: "sgn a = 1 \<longleftrightarrow> a > 0"
+  unfolding sgn_if by simp
 
-lemma sgn_1_neg:
-  "sgn a = - 1 \<longleftrightarrow> a < 0"
-unfolding sgn_if by auto
+lemma sgn_1_neg: "sgn a = - 1 \<longleftrightarrow> a < 0"
+  unfolding sgn_if by auto
 
-lemma sgn_pos [simp]:
-  "0 < a \<Longrightarrow> sgn a = 1"
-unfolding sgn_1_pos .
+lemma sgn_pos [simp]: "0 < a \<Longrightarrow> sgn a = 1"
+  by (simp only: sgn_1_pos)
 
-lemma sgn_neg [simp]:
-  "a < 0 \<Longrightarrow> sgn a = - 1"
-unfolding sgn_1_neg .
+lemma sgn_neg [simp]: "a < 0 \<Longrightarrow> sgn a = - 1"
+  by (simp only: sgn_1_neg)
 
-lemma sgn_times:
-  "sgn (a * b) = sgn a * sgn b"
-by (auto simp add: sgn_if zero_less_mult_iff)
+lemma sgn_times: "sgn (a * b) = sgn a * sgn b"
+  by (auto simp add: sgn_if zero_less_mult_iff)
 
 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
-unfolding sgn_if abs_if by auto
+  unfolding sgn_if abs_if by auto
 
-lemma sgn_greater [simp]:
-  "0 < sgn a \<longleftrightarrow> 0 < a"
+lemma sgn_greater [simp]: "0 < sgn a \<longleftrightarrow> 0 < a"
   unfolding sgn_if by auto
 
-lemma sgn_less [simp]:
-  "sgn a < 0 \<longleftrightarrow> a < 0"
+lemma sgn_less [simp]: "sgn a < 0 \<longleftrightarrow> a < 0"
   unfolding sgn_if by auto
 
-lemma abs_sgn_eq:
-  "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
+lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
   by (simp add: sgn_if)
 
 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
@@ -1956,36 +1850,31 @@
 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
   by (simp add: abs_if)
 
-lemma dvd_if_abs_eq:
-  "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
-by(subst abs_dvd_iff[symmetric]) simp
+lemma dvd_if_abs_eq: "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
+  by (subst abs_dvd_iff [symmetric]) simp
 
-text \<open>The following lemmas can be proven in more general structures, but
-are dangerous as simp rules in absence of @{thm neg_equal_zero},
-@{thm neg_less_pos}, @{thm neg_less_eq_nonneg}.\<close>
+text \<open>
+  The following lemmas can be proven in more general structures, but
+  are dangerous as simp rules in absence of @{thm neg_equal_zero},
+  @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}.
+\<close>
 
-lemma equation_minus_iff_1 [simp, no_atp]:
-  "1 = - a \<longleftrightarrow> a = - 1"
+lemma equation_minus_iff_1 [simp, no_atp]: "1 = - a \<longleftrightarrow> a = - 1"
   by (fact equation_minus_iff)
 
-lemma minus_equation_iff_1 [simp, no_atp]:
-  "- a = 1 \<longleftrightarrow> a = - 1"
+lemma minus_equation_iff_1 [simp, no_atp]: "- a = 1 \<longleftrightarrow> a = - 1"
   by (subst minus_equation_iff, auto)
 
-lemma le_minus_iff_1 [simp, no_atp]:
-  "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
+lemma le_minus_iff_1 [simp, no_atp]: "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
   by (fact le_minus_iff)
 
-lemma minus_le_iff_1 [simp, no_atp]:
-  "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
+lemma minus_le_iff_1 [simp, no_atp]: "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
   by (fact minus_le_iff)
 
-lemma less_minus_iff_1 [simp, no_atp]:
-  "1 < - b \<longleftrightarrow> b < - 1"
+lemma less_minus_iff_1 [simp, no_atp]: "1 < - b \<longleftrightarrow> b < - 1"
   by (fact less_minus_iff)
 
-lemma minus_less_iff_1 [simp, no_atp]:
-  "- a < 1 \<longleftrightarrow> - 1 < a"
+lemma minus_less_iff_1 [simp, no_atp]: "- a < 1 \<longleftrightarrow> - 1 < a"
   by (fact minus_less_iff)
 
 end
@@ -1993,15 +1882,16 @@
 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
 
 lemmas mult_compare_simps =
-    mult_le_cancel_right mult_le_cancel_left
-    mult_le_cancel_right1 mult_le_cancel_right2
-    mult_le_cancel_left1 mult_le_cancel_left2
-    mult_less_cancel_right mult_less_cancel_left
-    mult_less_cancel_right1 mult_less_cancel_right2
-    mult_less_cancel_left1 mult_less_cancel_left2
-    mult_cancel_right mult_cancel_left
-    mult_cancel_right1 mult_cancel_right2
-    mult_cancel_left1 mult_cancel_left2
+  mult_le_cancel_right mult_le_cancel_left
+  mult_le_cancel_right1 mult_le_cancel_right2
+  mult_le_cancel_left1 mult_le_cancel_left2
+  mult_less_cancel_right mult_less_cancel_left
+  mult_less_cancel_right1 mult_less_cancel_right2
+  mult_less_cancel_left1 mult_less_cancel_left2
+  mult_cancel_right mult_cancel_left
+  mult_cancel_right1 mult_cancel_right2
+  mult_cancel_left1 mult_cancel_left2
+
 
 text \<open>Reasoning about inequalities with division\<close>
 
@@ -2012,7 +1902,7 @@
 proof -
   have "a + 0 < a + 1"
     by (blast intro: zero_less_one add_strict_left_mono)
-  thus ?thesis by simp
+  then show ?thesis by simp
 qed
 
 end
@@ -2020,12 +1910,10 @@
 context linordered_idom
 begin
 
-lemma mult_right_le_one_le:
-  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
+lemma mult_right_le_one_le: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
   by (rule mult_left_le)
 
-lemma mult_left_le_one_le:
-  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
+lemma mult_left_le_one_le: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
   by (auto simp add: mult_le_cancel_right2)
 
 end
@@ -2035,12 +1923,10 @@
 context linordered_idom
 begin
 
-lemma mult_sgn_abs:
-  "sgn x * \<bar>x\<bar> = x"
+lemma mult_sgn_abs: "sgn x * \<bar>x\<bar> = x"
   unfolding abs_if sgn_if by auto
 
-lemma abs_one [simp]:
-  "\<bar>1\<bar> = 1"
+lemma abs_one [simp]: "\<bar>1\<bar> = 1"
   by (simp add: abs_if)
 
 end
@@ -2052,57 +1938,54 @@
 context linordered_idom
 begin
 
-subclass ordered_ring_abs proof
-qed (auto simp add: abs_if not_less mult_less_0_iff)
+subclass ordered_ring_abs
+  by standard (auto simp add: abs_if not_less mult_less_0_iff)
 
-lemma abs_mult:
-  "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
+lemma abs_mult: "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
   by (rule abs_eq_mult) auto
 
-lemma abs_mult_self [simp]:
-  "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
+lemma abs_mult_self [simp]: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
   by (simp add: abs_if)
 
 lemma abs_mult_less:
-  "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
+  assumes ac: "\<bar>a\<bar> < c"
+    and bd: "\<bar>b\<bar> < d"
+  shows "\<bar>a\<bar> * \<bar>b\<bar> < c * d"
 proof -
-  assume ac: "\<bar>a\<bar> < c"
-  hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
-  assume "\<bar>b\<bar> < d"
-  thus ?thesis by (simp add: ac cpos mult_strict_mono)
+  from ac have "0 < c"
+    by (blast intro: le_less_trans abs_ge_zero)
+  with bd show ?thesis by (simp add: ac mult_strict_mono)
 qed
 
-lemma abs_less_iff:
-  "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
+lemma abs_less_iff: "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
 
-lemma abs_mult_pos:
-  "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
+lemma abs_mult_pos: "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
   by (simp add: abs_mult)
 
-lemma abs_diff_less_iff:
-  "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
+lemma abs_diff_less_iff: "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
   by (auto simp add: diff_less_eq ac_simps abs_less_iff)
 
-lemma abs_diff_le_iff:
-   "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
+lemma abs_diff_le_iff: "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
   by (auto simp add: diff_le_eq ac_simps abs_le_iff)
 
 lemma abs_add_one_gt_zero: "0 < 1 + \<bar>x\<bar>"
-  by (force simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans)
+  by (auto simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans)
 
 end
 
 subsection \<open>Dioids\<close>
 
-text \<open>Dioids are the alternative extensions of semirings, a semiring can either be a ring or a dioid
-but never both.\<close>
+text \<open>
+  Dioids are the alternative extensions of semirings, a semiring can
+  either be a ring or a dioid but never both.
+\<close>
 
 class dioid = semiring_1 + canonically_ordered_monoid_add
 begin
 
 subclass ordered_semiring
-  proof qed (auto simp: le_iff_add distrib_left distrib_right)
+  by standard (auto simp: le_iff_add distrib_left distrib_right)
 
 end