# HG changeset patch
# User wenzelm
# Date 1468488858 -7200
# Node ID cd540c8031a41b33e7961c92a901a86377ab4f81
# Parent  a7c5074a025155b5c2e832038359bdb9341f8d2a
misc tuning and modernization;

diff -r a7c5074a0251 -r cd540c8031a4 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Wed Jul 13 21:30:41 2016 +0200
+++ b/src/HOL/Archimedean_Field.thy	Thu Jul 14 11:34:18 2016 +0200
@@ -9,62 +9,69 @@
 begin
 
 lemma cInf_abs_ge:
-  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
-  assumes "S \<noteq> {}" and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a"
+  fixes S :: "'a::{linordered_idom,conditionally_complete_linorder} set"
+  assumes "S \<noteq> {}"
+    and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a"
   shows "\<bar>Inf S\<bar> \<le> a"
 proof -
   have "Sup (uminus ` S) = - (Inf S)"
   proof (rule antisym)
-    show "- (Inf S) \<le> Sup(uminus ` S)"
+    show "- (Inf S) \<le> Sup (uminus ` S)"
       apply (subst minus_le_iff)
       apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
       apply (subst minus_le_iff)
-      apply (rule cSup_upper, force)
-      using bdd apply (force simp add: abs_le_iff bdd_above_def)
+      apply (rule cSup_upper)
+       apply force
+      using bdd
+      apply (force simp: abs_le_iff bdd_above_def)
       done
   next
     show "Sup (uminus ` S) \<le> - Inf S"
       apply (rule cSup_least)
-       using \<open>S \<noteq> {}\<close> apply (force simp add: )
+      using \<open>S \<noteq> {}\<close>
+       apply force
       apply clarsimp
       apply (rule cInf_lower)
-      apply assumption
-      using bdd apply (simp add: bdd_below_def)
-      apply (rule_tac x="-a" in exI)
+       apply assumption
+      using bdd
+      apply (simp add: bdd_below_def)
+      apply (rule_tac x = "- a" in exI)
       apply force
       done
   qed
-  with cSup_abs_le [of "uminus ` S"] assms show ?thesis by fastforce
+  with cSup_abs_le [of "uminus ` S"] assms show ?thesis
+    by fastforce
 qed
 
 lemma cSup_asclose:
-  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
+  fixes S :: "'a::{linordered_idom,conditionally_complete_linorder} set"
   assumes S: "S \<noteq> {}"
     and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
   shows "\<bar>Sup S - l\<bar> \<le> e"
 proof -
-  have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
+  have *: "\<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" for x l e :: 'a
     by arith
   have "bdd_above S"
     using b by (auto intro!: bdd_aboveI[of _ "l + e"])
   with S b show ?thesis
-    unfolding th by (auto intro!: cSup_upper2 cSup_least)
+    unfolding * by (auto intro!: cSup_upper2 cSup_least)
 qed
 
 lemma cInf_asclose:
-  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
+  fixes S :: "'a::{linordered_idom,conditionally_complete_linorder} set"
   assumes S: "S \<noteq> {}"
     and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
   shows "\<bar>Inf S - l\<bar> \<le> e"
 proof -
-  have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
+  have *: "\<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" for x l e :: 'a
     by arith
   have "bdd_below S"
     using b by (auto intro!: bdd_belowI[of _ "l - e"])
   with S b show ?thesis
-    unfolding th by (auto intro!: cInf_lower2 cInf_greatest)
+    unfolding * by (auto intro!: cInf_lower2 cInf_greatest)
 qed
 
+
 subsection \<open>Class of Archimedean fields\<close>
 
 text \<open>Archimedean fields have no infinite elements.\<close>
@@ -72,36 +79,41 @@
 class archimedean_field = linordered_field +
   assumes ex_le_of_int: "\<exists>z. x \<le> of_int z"
 
-lemma ex_less_of_int:
-  fixes x :: "'a::archimedean_field" shows "\<exists>z. x < of_int z"
+lemma ex_less_of_int: "\<exists>z. x < of_int z"
+  for x :: "'a::archimedean_field"
 proof -
   from ex_le_of_int obtain z where "x \<le> of_int z" ..
   then have "x < of_int (z + 1)" by simp
   then show ?thesis ..
 qed
 
-lemma ex_of_int_less:
-  fixes x :: "'a::archimedean_field" shows "\<exists>z. of_int z < x"
+lemma ex_of_int_less: "\<exists>z. of_int z < x"
+  for x :: "'a::archimedean_field"
 proof -
   from ex_less_of_int obtain z where "- x < of_int z" ..
   then have "of_int (- z) < x" by simp
   then show ?thesis ..
 qed
 
-lemma reals_Archimedean2:
-  fixes x :: "'a::archimedean_field" shows "\<exists>n. x < of_nat n"
+lemma reals_Archimedean2: "\<exists>n. x < of_nat n"
+  for x :: "'a::archimedean_field"
 proof -
-  obtain z where "x < of_int z" using ex_less_of_int ..
-  also have "\<dots> \<le> of_int (int (nat z))" by simp
-  also have "\<dots> = of_nat (nat z)" by (simp only: of_int_of_nat_eq)
+  obtain z where "x < of_int z"
+    using ex_less_of_int ..
+  also have "\<dots> \<le> of_int (int (nat z))"
+    by simp
+  also have "\<dots> = of_nat (nat z)"
+    by (simp only: of_int_of_nat_eq)
   finally show ?thesis ..
 qed
 
-lemma real_arch_simple:
-  fixes x :: "'a::archimedean_field" shows "\<exists>n. x \<le> of_nat n"
+lemma real_arch_simple: "\<exists>n. x \<le> of_nat n"
+  for x :: "'a::archimedean_field"
 proof -
-  obtain n where "x < of_nat n" using reals_Archimedean2 ..
-  then have "x \<le> of_nat n" by simp
+  obtain n where "x < of_nat n"
+    using reals_Archimedean2 ..
+  then have "x \<le> of_nat n"
+    by simp
   then show ?thesis ..
 qed
 
@@ -109,7 +121,8 @@
 
 lemma reals_Archimedean:
   fixes x :: "'a::archimedean_field"
-  assumes "0 < x" shows "\<exists>n. inverse (of_nat (Suc n)) < x"
+  assumes "0 < x"
+  shows "\<exists>n. inverse (of_nat (Suc n)) < x"
 proof -
   from \<open>0 < x\<close> have "0 < inverse x"
     by (rule positive_imp_inverse_positive)
@@ -126,15 +139,19 @@
 
 lemma ex_inverse_of_nat_less:
   fixes x :: "'a::archimedean_field"
-  assumes "0 < x" shows "\<exists>n>0. inverse (of_nat n) < x"
+  assumes "0 < x"
+  shows "\<exists>n>0. inverse (of_nat n) < x"
   using reals_Archimedean [OF \<open>0 < x\<close>] by auto
 
 lemma ex_less_of_nat_mult:
   fixes x :: "'a::archimedean_field"
-  assumes "0 < x" shows "\<exists>n. y < of_nat n * x"
+  assumes "0 < x"
+  shows "\<exists>n. y < of_nat n * x"
 proof -
-  obtain n where "y / x < of_nat n" using reals_Archimedean2 ..
-  with \<open>0 < x\<close> have "y < of_nat n * x" by (simp add: pos_divide_less_eq)
+  obtain n where "y / x < of_nat n"
+    using reals_Archimedean2 ..
+  with \<open>0 < x\<close> have "y < of_nat n * x"
+    by (simp add: pos_divide_less_eq)
   then show ?thesis ..
 qed
 
@@ -145,11 +162,14 @@
   assumes "\<not> P 0" and "\<exists>n. P n"
   shows "\<exists>n. \<not> P n \<and> P (Suc n)"
 proof -
-  from \<open>\<exists>n. P n\<close> have "P (Least P)" by (rule LeastI_ex)
+  from \<open>\<exists>n. P n\<close> have "P (Least P)"
+    by (rule LeastI_ex)
   with \<open>\<not> P 0\<close> obtain n where "Least P = Suc n"
     by (cases "Least P") auto
-  then have "n < Least P" by simp
-  then have "\<not> P n" by (rule not_less_Least)
+  then have "n < Least P"
+    by simp
+  then have "\<not> P n"
+    by (rule not_less_Least)
   then have "\<not> P n \<and> P (Suc n)"
     using \<open>P (Least P)\<close> \<open>Least P = Suc n\<close> by simp
   then show ?thesis ..
@@ -158,37 +178,40 @@
 lemma floor_exists:
   fixes x :: "'a::archimedean_field"
   shows "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)"
-proof (cases)
-  assume "0 \<le> x"
-  then have "\<not> x < of_nat 0" by simp
+proof (cases "0 \<le> x")
+  case True
+  then have "\<not> x < of_nat 0"
+    by simp
   then have "\<exists>n. \<not> x < of_nat n \<and> x < of_nat (Suc n)"
     using reals_Archimedean2 by (rule exists_least_lemma)
   then obtain n where "\<not> x < of_nat n \<and> x < of_nat (Suc n)" ..
-  then have "of_int (int n) \<le> x \<and> x < of_int (int n + 1)" by simp
+  then have "of_int (int n) \<le> x \<and> x < of_int (int n + 1)"
+    by simp
   then show ?thesis ..
 next
-  assume "\<not> 0 \<le> x"
-  then have "\<not> - x \<le> of_nat 0" by simp
+  case False
+  then have "\<not> - x \<le> of_nat 0"
+    by simp
   then have "\<exists>n. \<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)"
     using real_arch_simple by (rule exists_least_lemma)
   then obtain n where "\<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" ..
-  then have "of_int (- int n - 1) \<le> x \<and> x < of_int (- int n - 1 + 1)" by simp
+  then have "of_int (- int n - 1) \<le> x \<and> x < of_int (- int n - 1 + 1)"
+    by simp
   then show ?thesis ..
 qed
 
-lemma floor_exists1:
-  fixes x :: "'a::archimedean_field"
-  shows "\<exists>!z. of_int z \<le> x \<and> x < of_int (z + 1)"
+lemma floor_exists1: "\<exists>!z. of_int z \<le> x \<and> x < of_int (z + 1)"
+  for x :: "'a::archimedean_field"
 proof (rule ex_ex1I)
   show "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)"
     by (rule floor_exists)
 next
-  fix y z assume
-    "of_int y \<le> x \<and> x < of_int (y + 1)"
-    "of_int z \<le> x \<and> x < of_int (z + 1)"
+  fix y z
+  assume "of_int y \<le> x \<and> x < of_int (y + 1)"
+    and "of_int z \<le> x \<and> x < of_int (z + 1)"
   with le_less_trans [of "of_int y" "x" "of_int (z + 1)"]
-       le_less_trans [of "of_int z" "x" "of_int (y + 1)"]
-  show "y = z" by (simp del: of_int_add)
+       le_less_trans [of "of_int z" "x" "of_int (y + 1)"] show "y = z"
+    by (simp del: of_int_add)
 qed
 
 
@@ -198,13 +221,12 @@
   fixes floor :: "'a \<Rightarrow> int"  ("\<lfloor>_\<rfloor>")
   assumes floor_correct: "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)"
 
-lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> \<lfloor>x\<rfloor> = z"
+lemma floor_unique: "of_int z \<le> x \<Longrightarrow> x < of_int z + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = z"
   using floor_correct [of x] floor_exists1 [of x] by auto
 
-lemma floor_unique_iff:
-  fixes x :: "'a::floor_ceiling"
-  shows  "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
-using floor_correct floor_unique by auto
+lemma floor_unique_iff: "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
+  for x :: "'a::floor_ceiling"
+  using floor_correct floor_unique by auto
 
 lemma of_int_floor_le [simp]: "of_int \<lfloor>x\<rfloor> \<le> x"
   using floor_correct ..
@@ -254,7 +276,8 @@
 lemma le_floor_add: "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> \<le> \<lfloor>x + y\<rfloor>"
   by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le)
 
-text \<open>Floor with numerals\<close>
+
+text \<open>Floor with numerals.\<close>
 
 lemma floor_zero [simp]: "\<lfloor>0\<rfloor> = 0"
   using floor_of_int [of 0] by simp
@@ -274,12 +297,10 @@
 lemma one_le_floor [simp]: "1 \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> 1 \<le> x"
   by (simp add: le_floor_iff)
 
-lemma numeral_le_floor [simp]:
-  "numeral v \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> numeral v \<le> x"
+lemma numeral_le_floor [simp]: "numeral v \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> numeral v \<le> x"
   by (simp add: le_floor_iff)
 
-lemma neg_numeral_le_floor [simp]:
-  "- numeral v \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> - numeral v \<le> x"
+lemma neg_numeral_le_floor [simp]: "- numeral v \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> - numeral v \<le> x"
   by (simp add: le_floor_iff)
 
 lemma zero_less_floor [simp]: "0 < \<lfloor>x\<rfloor> \<longleftrightarrow> 1 \<le> x"
@@ -288,12 +309,10 @@
 lemma one_less_floor [simp]: "1 < \<lfloor>x\<rfloor> \<longleftrightarrow> 2 \<le> x"
   by (simp add: less_floor_iff)
 
-lemma numeral_less_floor [simp]:
-  "numeral v < \<lfloor>x\<rfloor> \<longleftrightarrow> numeral v + 1 \<le> x"
+lemma numeral_less_floor [simp]: "numeral v < \<lfloor>x\<rfloor> \<longleftrightarrow> numeral v + 1 \<le> x"
   by (simp add: less_floor_iff)
 
-lemma neg_numeral_less_floor [simp]:
-  "- numeral v < \<lfloor>x\<rfloor> \<longleftrightarrow> - numeral v + 1 \<le> x"
+lemma neg_numeral_less_floor [simp]: "- numeral v < \<lfloor>x\<rfloor> \<longleftrightarrow> - numeral v + 1 \<le> x"
   by (simp add: less_floor_iff)
 
 lemma floor_le_zero [simp]: "\<lfloor>x\<rfloor> \<le> 0 \<longleftrightarrow> x < 1"
@@ -302,12 +321,10 @@
 lemma floor_le_one [simp]: "\<lfloor>x\<rfloor> \<le> 1 \<longleftrightarrow> x < 2"
   by (simp add: floor_le_iff)
 
-lemma floor_le_numeral [simp]:
-  "\<lfloor>x\<rfloor> \<le> numeral v \<longleftrightarrow> x < numeral v + 1"
+lemma floor_le_numeral [simp]: "\<lfloor>x\<rfloor> \<le> numeral v \<longleftrightarrow> x < numeral v + 1"
   by (simp add: floor_le_iff)
 
-lemma floor_le_neg_numeral [simp]:
-  "\<lfloor>x\<rfloor> \<le> - numeral v \<longleftrightarrow> x < - numeral v + 1"
+lemma floor_le_neg_numeral [simp]: "\<lfloor>x\<rfloor> \<le> - numeral v \<longleftrightarrow> x < - numeral v + 1"
   by (simp add: floor_le_iff)
 
 lemma floor_less_zero [simp]: "\<lfloor>x\<rfloor> < 0 \<longleftrightarrow> x < 0"
@@ -316,21 +333,19 @@
 lemma floor_less_one [simp]: "\<lfloor>x\<rfloor> < 1 \<longleftrightarrow> x < 1"
   by (simp add: floor_less_iff)
 
-lemma floor_less_numeral [simp]:
-  "\<lfloor>x\<rfloor> < numeral v \<longleftrightarrow> x < numeral v"
+lemma floor_less_numeral [simp]: "\<lfloor>x\<rfloor> < numeral v \<longleftrightarrow> x < numeral v"
   by (simp add: floor_less_iff)
 
-lemma floor_less_neg_numeral [simp]:
-  "\<lfloor>x\<rfloor> < - numeral v \<longleftrightarrow> x < - numeral v"
+lemma floor_less_neg_numeral [simp]: "\<lfloor>x\<rfloor> < - numeral v \<longleftrightarrow> x < - numeral v"
   by (simp add: floor_less_iff)
 
-text \<open>Addition and subtraction of integers\<close>
+
+text \<open>Addition and subtraction of integers.\<close>
 
 lemma floor_add_of_int [simp]: "\<lfloor>x + of_int z\<rfloor> = \<lfloor>x\<rfloor> + z"
   using floor_correct [of x] by (simp add: floor_unique)
 
-lemma floor_add_numeral [simp]:
-    "\<lfloor>x + numeral v\<rfloor> = \<lfloor>x\<rfloor> + numeral v"
+lemma floor_add_numeral [simp]: "\<lfloor>x + numeral v\<rfloor> = \<lfloor>x\<rfloor> + numeral v"
   using floor_add_of_int [of x "numeral v"] by simp
 
 lemma floor_add_one [simp]: "\<lfloor>x + 1\<rfloor> = \<lfloor>x\<rfloor> + 1"
@@ -342,8 +357,7 @@
 lemma floor_uminus_of_int [simp]: "\<lfloor>- (of_int z)\<rfloor> = - z"
   by (metis floor_diff_of_int [of 0] diff_0 floor_zero)
 
-lemma floor_diff_numeral [simp]:
-  "\<lfloor>x - numeral v\<rfloor> = \<lfloor>x\<rfloor> - numeral v"
+lemma floor_diff_numeral [simp]: "\<lfloor>x - numeral v\<rfloor> = \<lfloor>x\<rfloor> - numeral v"
   using floor_diff_of_int [of x "numeral v"] by simp
 
 lemma floor_diff_one [simp]: "\<lfloor>x - 1\<rfloor> = \<lfloor>x\<rfloor> - 1"
@@ -353,32 +367,38 @@
   assumes "0 \<le> a" and "0 \<le> b"
   shows "\<lfloor>a\<rfloor> * \<lfloor>b\<rfloor> \<le> \<lfloor>a * b\<rfloor>"
 proof -
-  have "of_int \<lfloor>a\<rfloor> \<le> a"
-    and "of_int \<lfloor>b\<rfloor> \<le> b" by (auto intro: of_int_floor_le)
-  hence "of_int (\<lfloor>a\<rfloor> * \<lfloor>b\<rfloor>) \<le> a * b"
+  have "of_int \<lfloor>a\<rfloor> \<le> a" and "of_int \<lfloor>b\<rfloor> \<le> b"
+    by (auto intro: of_int_floor_le)
+  then have "of_int (\<lfloor>a\<rfloor> * \<lfloor>b\<rfloor>) \<le> a * b"
     using assms by (auto intro!: mult_mono)
   also have "a * b < of_int (\<lfloor>a * b\<rfloor> + 1)"
     using floor_correct[of "a * b"] by auto
-  finally show ?thesis unfolding of_int_less_iff by simp
+  finally show ?thesis
+    unfolding of_int_less_iff by simp
 qed
 
-lemma floor_divide_of_int_eq:
-  fixes k l :: int
-  shows "\<lfloor>of_int k / of_int l\<rfloor> = k div l"
+lemma floor_divide_of_int_eq: "\<lfloor>of_int k / of_int l\<rfloor> = k div l"
+  for k l :: int
 proof (cases "l = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
   case False
   have *: "\<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> = 0"
   proof (cases "l > 0")
-    case True then show ?thesis
+    case True
+    then show ?thesis
       by (auto intro: floor_unique)
   next
     case False
-    obtain r where "r = - l" by blast
-    then have l: "l = - r" by simp
-    moreover with \<open>l \<noteq> 0\<close> False have "r > 0" by simp
-    ultimately show ?thesis using pos_mod_bound [of r]
+    obtain r where "r = - l"
+      by blast
+    then have l: "l = - r"
+      by simp
+    moreover with \<open>l \<noteq> 0\<close> False have "r > 0"
+      by simp
+    ultimately show ?thesis
+      using pos_mod_bound [of r]
       by (auto simp add: zmod_zminus2_eq_if less_le field_simps intro: floor_unique)
   qed
   have "(of_int k :: 'a) = of_int (k div l * l + k mod l)"
@@ -395,14 +415,15 @@
     by (simp add: ac_simps)
   then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> + k div l"
     by simp
-  with * show ?thesis by simp
+  with * show ?thesis
+    by simp
 qed
 
-lemma floor_divide_of_nat_eq:
-  fixes m n :: nat
-  shows "\<lfloor>of_nat m / of_nat n\<rfloor> = of_nat (m div n)"
+lemma floor_divide_of_nat_eq: "\<lfloor>of_nat m / of_nat n\<rfloor> = of_nat (m div n)"
+  for m n :: nat
 proof (cases "n = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
   case False
   then have *: "\<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> = 0"
@@ -410,7 +431,7 @@
   have "(of_nat m :: 'a) = of_nat (m div n * n + m mod n)"
     by simp
   also have "\<dots> = (of_nat (m div n) + of_nat (m mod n) / of_nat n) * of_nat n"
-    using False by (simp only: of_nat_add) (simp add: field_simps of_nat_mult)
+    using False by (simp only: of_nat_add) (simp add: field_simps)
   finally have "(of_nat m / of_nat n :: 'a) = \<dots> / of_nat n"
     by simp
   then have "(of_nat m / of_nat n :: 'a) = of_nat (m div n) + of_nat (m mod n) / of_nat n"
@@ -421,9 +442,11 @@
     by (simp add: ac_simps)
   moreover have "(of_nat (m div n) :: 'a) = of_int (of_nat (m div n))"
     by simp
-  ultimately have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> + of_nat (m div n)"
+  ultimately have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> =
+      \<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> + of_nat (m div n)"
     by (simp only: floor_add_of_int)
-  with * show ?thesis by simp
+  with * show ?thesis
+    by simp
 qed
 
 
@@ -433,9 +456,10 @@
   where "\<lceil>x\<rceil> = - \<lfloor>- x\<rfloor>"
 
 lemma ceiling_correct: "of_int \<lceil>x\<rceil> - 1 < x \<and> x \<le> of_int \<lceil>x\<rceil>"
-  unfolding ceiling_def using floor_correct [of "- x"] by (simp add: le_minus_iff)
+  unfolding ceiling_def using floor_correct [of "- x"]
+  by (simp add: le_minus_iff)
 
-lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> \<lceil>x\<rceil> = z"
+lemma ceiling_unique: "of_int z - 1 < x \<Longrightarrow> x \<le> of_int z \<Longrightarrow> \<lceil>x\<rceil> = z"
   unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp
 
 lemma le_of_int_ceiling [simp]: "x \<le> of_int \<lceil>x\<rceil>"
@@ -468,7 +492,8 @@
 lemma ceiling_add_le: "\<lceil>x + y\<rceil> \<le> \<lceil>x\<rceil> + \<lceil>y\<rceil>"
   by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)
 
-text \<open>Ceiling with numerals\<close>
+
+text \<open>Ceiling with numerals.\<close>
 
 lemma ceiling_zero [simp]: "\<lceil>0\<rceil> = 0"
   using ceiling_of_int [of 0] by simp
@@ -488,12 +513,10 @@
 lemma ceiling_le_one [simp]: "\<lceil>x\<rceil> \<le> 1 \<longleftrightarrow> x \<le> 1"
   by (simp add: ceiling_le_iff)
 
-lemma ceiling_le_numeral [simp]:
-  "\<lceil>x\<rceil> \<le> numeral v \<longleftrightarrow> x \<le> numeral v"
+lemma ceiling_le_numeral [simp]: "\<lceil>x\<rceil> \<le> numeral v \<longleftrightarrow> x \<le> numeral v"
   by (simp add: ceiling_le_iff)
 
-lemma ceiling_le_neg_numeral [simp]:
-  "\<lceil>x\<rceil> \<le> - numeral v \<longleftrightarrow> x \<le> - numeral v"
+lemma ceiling_le_neg_numeral [simp]: "\<lceil>x\<rceil> \<le> - numeral v \<longleftrightarrow> x \<le> - numeral v"
   by (simp add: ceiling_le_iff)
 
 lemma ceiling_less_zero [simp]: "\<lceil>x\<rceil> < 0 \<longleftrightarrow> x \<le> -1"
@@ -502,12 +525,10 @@
 lemma ceiling_less_one [simp]: "\<lceil>x\<rceil> < 1 \<longleftrightarrow> x \<le> 0"
   by (simp add: ceiling_less_iff)
 
-lemma ceiling_less_numeral [simp]:
-  "\<lceil>x\<rceil> < numeral v \<longleftrightarrow> x \<le> numeral v - 1"
+lemma ceiling_less_numeral [simp]: "\<lceil>x\<rceil> < numeral v \<longleftrightarrow> x \<le> numeral v - 1"
   by (simp add: ceiling_less_iff)
 
-lemma ceiling_less_neg_numeral [simp]:
-  "\<lceil>x\<rceil> < - numeral v \<longleftrightarrow> x \<le> - numeral v - 1"
+lemma ceiling_less_neg_numeral [simp]: "\<lceil>x\<rceil> < - numeral v \<longleftrightarrow> x \<le> - numeral v - 1"
   by (simp add: ceiling_less_iff)
 
 lemma zero_le_ceiling [simp]: "0 \<le> \<lceil>x\<rceil> \<longleftrightarrow> -1 < x"
@@ -516,12 +537,10 @@
 lemma one_le_ceiling [simp]: "1 \<le> \<lceil>x\<rceil> \<longleftrightarrow> 0 < x"
   by (simp add: le_ceiling_iff)
 
-lemma numeral_le_ceiling [simp]:
-  "numeral v \<le> \<lceil>x\<rceil> \<longleftrightarrow> numeral v - 1 < x"
+lemma numeral_le_ceiling [simp]: "numeral v \<le> \<lceil>x\<rceil> \<longleftrightarrow> numeral v - 1 < x"
   by (simp add: le_ceiling_iff)
 
-lemma neg_numeral_le_ceiling [simp]:
-  "- numeral v \<le> \<lceil>x\<rceil> \<longleftrightarrow> - numeral v - 1 < x"
+lemma neg_numeral_le_ceiling [simp]: "- numeral v \<le> \<lceil>x\<rceil> \<longleftrightarrow> - numeral v - 1 < x"
   by (simp add: le_ceiling_iff)
 
 lemma zero_less_ceiling [simp]: "0 < \<lceil>x\<rceil> \<longleftrightarrow> 0 < x"
@@ -530,21 +549,20 @@
 lemma one_less_ceiling [simp]: "1 < \<lceil>x\<rceil> \<longleftrightarrow> 1 < x"
   by (simp add: less_ceiling_iff)
 
-lemma numeral_less_ceiling [simp]:
-  "numeral v < \<lceil>x\<rceil> \<longleftrightarrow> numeral v < x"
+lemma numeral_less_ceiling [simp]: "numeral v < \<lceil>x\<rceil> \<longleftrightarrow> numeral v < x"
   by (simp add: less_ceiling_iff)
 
-lemma neg_numeral_less_ceiling [simp]:
-  "- numeral v < \<lceil>x\<rceil> \<longleftrightarrow> - numeral v < x"
+lemma neg_numeral_less_ceiling [simp]: "- numeral v < \<lceil>x\<rceil> \<longleftrightarrow> - numeral v < x"
   by (simp add: less_ceiling_iff)
 
 lemma ceiling_altdef: "\<lceil>x\<rceil> = (if x = of_int \<lfloor>x\<rfloor> then \<lfloor>x\<rfloor> else \<lfloor>x\<rfloor> + 1)"
-  by (intro ceiling_unique, (simp, linarith?)+)
+  by (intro ceiling_unique; simp, linarith?)
 
 lemma floor_le_ceiling [simp]: "\<lfloor>x\<rfloor> \<le> \<lceil>x\<rceil>"
   by (simp add: ceiling_altdef)
 
-text \<open>Addition and subtraction of integers\<close>
+
+text \<open>Addition and subtraction of integers.\<close>
 
 lemma ceiling_add_of_int [simp]: "\<lceil>x + of_int z\<rceil> = \<lceil>x\<rceil> + z"
   using ceiling_correct [of x] by (simp add: ceiling_def)
@@ -579,6 +597,7 @@
     unfolding of_int_less_iff by simp
 qed
 
+
 subsection \<open>Negation\<close>
 
 lemma floor_minus: "\<lfloor>- x\<rfloor> = - \<lceil>x\<rceil>"
@@ -590,18 +609,17 @@
 
 subsection \<open>Frac Function\<close>
 
-definition frac :: "'a \<Rightarrow> 'a::floor_ceiling" where
-  "frac x \<equiv> x - of_int \<lfloor>x\<rfloor>"
+definition frac :: "'a \<Rightarrow> 'a::floor_ceiling"
+  where "frac x \<equiv> x - of_int \<lfloor>x\<rfloor>"
 
 lemma frac_lt_1: "frac x < 1"
-  by  (simp add: frac_def) linarith
+  by (simp add: frac_def) linarith
 
 lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> \<int>"
   by (simp add: frac_def) (metis Ints_cases Ints_of_int floor_of_int )
 
 lemma frac_ge_0 [simp]: "frac x \<ge> 0"
-  unfolding frac_def
-  by linarith
+  unfolding frac_def by linarith
 
 lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> \<int>"
   by (metis frac_eq_0_iff frac_ge_0 le_less less_irrefl)
@@ -611,57 +629,60 @@
 
 lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)"
 proof -
-  {assume "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
-   then have "\<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
-     by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
-   }
+  have "\<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>" if "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
+    using that by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
   moreover
-  { assume "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
-    then have "\<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)"
-      apply (simp add: floor_unique_iff)
-      apply (auto simp add: algebra_simps)
-      by linarith
-  }
+  have "\<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)" if "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
+    using that
+    apply (simp add: floor_unique_iff)
+    apply (auto simp add: algebra_simps)
+    apply linarith
+    done
   ultimately show ?thesis
     by (auto simp add: frac_def algebra_simps)
 qed
 
-lemma frac_add: "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y
-                                 else (frac x + frac y) - 1)"
+lemma frac_add:
+  "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y else (frac x + frac y) - 1)"
   by (simp add: frac_def floor_add)
 
-lemma frac_unique_iff:
-  fixes x :: "'a::floor_ceiling"
-  shows  "frac x = a \<longleftrightarrow> x - a \<in> \<int> \<and> 0 \<le> a \<and> a < 1"
+lemma frac_unique_iff: "frac x = a \<longleftrightarrow> x - a \<in> \<int> \<and> 0 \<le> a \<and> a < 1"
+  for x :: "'a::floor_ceiling"
   apply (auto simp: Ints_def frac_def algebra_simps floor_unique)
-  apply linarith+
+   apply linarith+
   done
 
-lemma frac_eq: "(frac x) = x \<longleftrightarrow> 0 \<le> x \<and> x < 1"
+lemma frac_eq: "frac x = x \<longleftrightarrow> 0 \<le> x \<and> x < 1"
   by (simp add: frac_unique_iff)
 
-lemma frac_neg:
-  fixes x :: "'a::floor_ceiling"
-  shows  "frac (-x) = (if x \<in> \<int> then 0 else 1 - frac x)"
+lemma frac_neg: "frac (- x) = (if x \<in> \<int> then 0 else 1 - frac x)"
+  for x :: "'a::floor_ceiling"
   apply (auto simp add: frac_unique_iff)
-  apply (simp add: frac_def)
-  by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
+   apply (simp add: frac_def)
+  apply (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
+  done
 
 
 subsection \<open>Rounding to the nearest integer\<close>
 
-definition round where "round x = \<lfloor>x + 1/2\<rfloor>"
+definition round :: "'a::floor_ceiling \<Rightarrow> int"
+  where "round x = \<lfloor>x + 1/2\<rfloor>"
 
-lemma of_int_round_ge:     "of_int (round x) \<ge> x - 1/2"
-  and of_int_round_le:     "of_int (round x) \<le> x + 1/2"
+lemma of_int_round_ge: "of_int (round x) \<ge> x - 1/2"
+  and of_int_round_le: "of_int (round x) \<le> x + 1/2"
   and of_int_round_abs_le: "\<bar>of_int (round x) - x\<bar> \<le> 1/2"
-  and of_int_round_gt:     "of_int (round x) > x - 1/2"
+  and of_int_round_gt: "of_int (round x) > x - 1/2"
 proof -
-  from floor_correct[of "x + 1/2"] have "x + 1/2 < of_int (round x) + 1" by (simp add: round_def)
-  from add_strict_right_mono[OF this, of "-1"] show A: "of_int (round x) > x - 1/2" by simp
-  thus "of_int (round x) \<ge> x - 1/2" by simp
-  from floor_correct[of "x + 1/2"] show "of_int (round x) \<le> x + 1/2" by (simp add: round_def)
-  with A show "\<bar>of_int (round x) - x\<bar> \<le> 1/2" by linarith
+  from floor_correct[of "x + 1/2"] have "x + 1/2 < of_int (round x) + 1"
+    by (simp add: round_def)
+  from add_strict_right_mono[OF this, of "-1"] show A: "of_int (round x) > x - 1/2"
+    by simp
+  then show "of_int (round x) \<ge> x - 1/2"
+    by simp
+  from floor_correct[of "x + 1/2"] show "of_int (round x) \<le> x + 1/2"
+    by (simp add: round_def)
+  with A show "\<bar>of_int (round x) - x\<bar> \<le> 1/2"
+    by linarith
 qed
 
 lemma round_of_int [simp]: "round (of_int n) = n"
@@ -686,37 +707,40 @@
   unfolding round_def by (intro floor_mono) simp
 
 lemma round_unique: "of_int y > x - 1/2 \<Longrightarrow> of_int y \<le> x + 1/2 \<Longrightarrow> round x = y"
-unfolding round_def
+  unfolding round_def
 proof (rule floor_unique)
   assume "x - 1 / 2 < of_int y"
-  from add_strict_left_mono[OF this, of 1] show "x + 1 / 2 < of_int y + 1" by simp
+  from add_strict_left_mono[OF this, of 1] show "x + 1 / 2 < of_int y + 1"
+    by simp
 qed
 
 lemma round_altdef: "round x = (if frac x \<ge> 1/2 then \<lceil>x\<rceil> else \<lfloor>x\<rfloor>)"
   by (cases "frac x \<ge> 1/2")
-     (rule round_unique, ((simp add: frac_def field_simps ceiling_altdef, linarith?)+)[2])+
+    (rule round_unique, ((simp add: frac_def field_simps ceiling_altdef; linarith)+)[2])+
 
 lemma floor_le_round: "\<lfloor>x\<rfloor> \<le> round x"
   unfolding round_def by (intro floor_mono) simp
 
-lemma ceiling_ge_round: "\<lceil>x\<rceil> \<ge> round x" unfolding round_altdef by simp
+lemma ceiling_ge_round: "\<lceil>x\<rceil> \<ge> round x"
+  unfolding round_altdef by simp
 
-lemma round_diff_minimal:
-  fixes z :: "'a :: floor_ceiling"
-  shows "\<bar>z - of_int (round z)\<bar> \<le> \<bar>z - of_int m\<bar>"
+lemma round_diff_minimal: "\<bar>z - of_int (round z)\<bar> \<le> \<bar>z - of_int m\<bar>"
+  for z :: "'a::floor_ceiling"
 proof (cases "of_int m \<ge> z")
   case True
-  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int \<lceil>z\<rceil> - z\<bar>"
-    unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith?
-  also have "of_int \<lceil>z\<rceil> - z \<ge> 0" by linarith
+  then have "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int \<lceil>z\<rceil> - z\<bar>"
+    unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith
+  also have "of_int \<lceil>z\<rceil> - z \<ge> 0"
+    by linarith
   with True have "\<bar>of_int \<lceil>z\<rceil> - z\<bar> \<le> \<bar>z - of_int m\<bar>"
     by (simp add: ceiling_le_iff)
   finally show ?thesis .
 next
   case False
-  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int \<lfloor>z\<rfloor> - z\<bar>"
-    unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith?
-  also have "z - of_int \<lfloor>z\<rfloor> \<ge> 0" by linarith
+  then have "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int \<lfloor>z\<rfloor> - z\<bar>"
+    unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith
+  also have "z - of_int \<lfloor>z\<rfloor> \<ge> 0"
+    by linarith
   with False have "\<bar>of_int \<lfloor>z\<rfloor> - z\<bar> \<le> \<bar>z - of_int m\<bar>"
     by (simp add: le_floor_iff)
   finally show ?thesis .
diff -r a7c5074a0251 -r cd540c8031a4 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Jul 13 21:30:41 2016 +0200
+++ b/src/HOL/GCD.thy	Thu Jul 14 11:34:18 2016 +0200
@@ -1,6 +1,10 @@
-(*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
-                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
-
+(*  Title:      HOL/GCD.thy
+    Author:     Christophe Tabacznyj
+    Author:     Lawrence C. Paulson
+    Author:     Amine Chaieb
+    Author:     Thomas M. Rasmussen
+    Author:     Jeremy Avigad
+    Author:     Tobias Nipkow
 
 This file deals with the functions gcd and lcm.  Definitions and
 lemmas are proved uniformly for the natural numbers and integers.
@@ -24,13 +28,13 @@
 Tobias Nipkow cleaned up a lot.
 *)
 
-
 section \<open>Greatest common divisor and least common multiple\<close>
 
 theory GCD
-imports Main
+  imports Main
 begin
 
+
 subsection \<open>Abstract GCD and LCM\<close>
 
 class gcd = zero + one + dvd +
@@ -49,12 +53,10 @@
 begin
 
 abbreviation GREATEST_COMMON_DIVISOR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-where
-  "GREATEST_COMMON_DIVISOR A f \<equiv> Gcd (f ` A)"
+  where "GREATEST_COMMON_DIVISOR A f \<equiv> Gcd (f ` A)"
 
 abbreviation LEAST_COMMON_MULTIPLE :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-where
-  "LEAST_COMMON_MULTIPLE A f \<equiv> Lcm (f ` A)"
+  where "LEAST_COMMON_MULTIPLE A f \<equiv> Lcm (f ` A)"
 
 end
 
@@ -63,7 +65,6 @@
   "_GCD"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3GCD _\<in>_./ _)" [0, 0, 10] 10)
   "_LCM1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3LCM _./ _)" [0, 10] 10)
   "_LCM"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3LCM _\<in>_./ _)" [0, 0, 10] 10)
-
 translations
   "GCD x y. B"   \<rightleftharpoons> "GCD x. GCD y. B"
   "GCD x. B"     \<rightleftharpoons> "CONST GREATEST_COMMON_DIVISOR CONST UNIV (\<lambda>x. B)"
@@ -85,50 +86,49 @@
     and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
     and normalize_gcd [simp]: "normalize (gcd a b) = gcd a b"
     and lcm_gcd: "lcm a b = normalize (a * b) div gcd a b"
-begin    
-
-lemma gcd_greatest_iff [simp]:
-  "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c"
+begin
+
+lemma gcd_greatest_iff [simp]: "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c"
   by (blast intro!: gcd_greatest intro: dvd_trans)
 
-lemma gcd_dvdI1:
-  "a dvd c \<Longrightarrow> gcd a b dvd c"
+lemma gcd_dvdI1: "a dvd c \<Longrightarrow> gcd a b dvd c"
   by (rule dvd_trans) (rule gcd_dvd1)
 
-lemma gcd_dvdI2:
-  "b dvd c \<Longrightarrow> gcd a b dvd c"
+lemma gcd_dvdI2: "b dvd c \<Longrightarrow> gcd a b dvd c"
   by (rule dvd_trans) (rule gcd_dvd2)
 
-lemma dvd_gcdD1:
-  "a dvd gcd b c \<Longrightarrow> a dvd b"
+lemma dvd_gcdD1: "a dvd gcd b c \<Longrightarrow> a dvd b"
   using gcd_dvd1 [of b c] by (blast intro: dvd_trans)
 
-lemma dvd_gcdD2:
-  "a dvd gcd b c \<Longrightarrow> a dvd c"
+lemma dvd_gcdD2: "a dvd gcd b c \<Longrightarrow> a dvd c"
   using gcd_dvd2 [of b c] by (blast intro: dvd_trans)
 
-lemma gcd_0_left [simp]:
-  "gcd 0 a = normalize a"
+lemma gcd_0_left [simp]: "gcd 0 a = normalize a"
   by (rule associated_eqI) simp_all
 
-lemma gcd_0_right [simp]:
-  "gcd a 0 = normalize a"
+lemma gcd_0_right [simp]: "gcd a 0 = normalize a"
   by (rule associated_eqI) simp_all
-  
-lemma gcd_eq_0_iff [simp]:
-  "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" (is "?P \<longleftrightarrow> ?Q")
+
+lemma gcd_eq_0_iff [simp]: "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
+  (is "?P \<longleftrightarrow> ?Q")
 proof
-  assume ?P then have "0 dvd gcd a b" by simp
-  then have "0 dvd a" and "0 dvd b" by (blast intro: dvd_trans)+
-  then show ?Q by simp
+  assume ?P
+  then have "0 dvd gcd a b"
+    by simp
+  then have "0 dvd a" and "0 dvd b"
+    by (blast intro: dvd_trans)+
+  then show ?Q
+    by simp
 next
-  assume ?Q then show ?P by simp
+  assume ?Q
+  then show ?P
+    by simp
 qed
 
-lemma unit_factor_gcd:
-  "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)"
+lemma unit_factor_gcd: "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)"
 proof (cases "gcd a b = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
   case False
   have "unit_factor (gcd a b) * normalize (gcd a b) = gcd a b"
@@ -137,11 +137,11 @@
     by simp
   then have "unit_factor (gcd a b) * gcd a b div gcd a b = gcd a b div gcd a b"
     by simp
-  with False show ?thesis by simp
+  with False show ?thesis
+    by simp
 qed
 
-lemma is_unit_gcd [simp]:
-  "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
+lemma is_unit_gcd [simp]: "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
   by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
 
 sublocale gcd: abel_semigroup gcd
@@ -165,8 +165,7 @@
     by (rule associated_eqI) simp_all
 qed
 
-lemma gcd_self [simp]:
-  "gcd a a = normalize a"
+lemma gcd_self [simp]: "gcd a a = normalize a"
 proof -
   have "a dvd gcd a a"
     by (rule gcd_greatest) simp_all
@@ -174,60 +173,52 @@
     by (auto intro: associated_eqI)
 qed
 
-lemma gcd_left_idem [simp]:
-  "gcd a (gcd a b) = gcd a b"
+lemma gcd_left_idem [simp]: "gcd a (gcd a b) = gcd a b"
   by (auto intro: associated_eqI)
 
-lemma gcd_right_idem [simp]:
-  "gcd (gcd a b) b = gcd a b"
+lemma gcd_right_idem [simp]: "gcd (gcd a b) b = gcd a b"
   unfolding gcd.commute [of a] gcd.commute [of "gcd b a"] by simp
 
-lemma coprime_1_left [simp]:
-  "coprime 1 a"
+lemma coprime_1_left [simp]: "coprime 1 a"
   by (rule associated_eqI) simp_all
 
-lemma coprime_1_right [simp]:
-  "coprime a 1"
+lemma coprime_1_right [simp]: "coprime a 1"
   using coprime_1_left [of a] by (simp add: ac_simps)
 
-lemma gcd_mult_left:
-  "gcd (c * a) (c * b) = normalize c * gcd a b"
+lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
 proof (cases "c = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
   case False
-  then have "c * gcd a b dvd gcd (c * a) (c * b)"
+  then have *: "c * gcd a b dvd gcd (c * a) (c * b)"
     by (auto intro: gcd_greatest)
-  moreover from calculation False have "gcd (c * a) (c * b) dvd c * gcd a b"
+  moreover from False * have "gcd (c * a) (c * b) dvd c * gcd a b"
     by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
   ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
     by (auto intro: associated_eqI)
-  then show ?thesis by (simp add: normalize_mult)
+  then show ?thesis
+    by (simp add: normalize_mult)
 qed
 
-lemma gcd_mult_right:
-  "gcd (a * c) (b * c) = gcd b a * normalize c"
+lemma gcd_mult_right: "gcd (a * c) (b * c) = gcd b a * normalize c"
   using gcd_mult_left [of c a b] by (simp add: ac_simps)
 
-lemma mult_gcd_left:
-  "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
+lemma mult_gcd_left: "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
   by (simp add: gcd_mult_left mult.assoc [symmetric])
 
-lemma mult_gcd_right:
-  "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
+lemma mult_gcd_right: "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
   using mult_gcd_left [of c a b] by (simp add: ac_simps)
 
-lemma dvd_lcm1 [iff]:
-  "a dvd lcm a b"
+lemma dvd_lcm1 [iff]: "a dvd lcm a b"
 proof -
   have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)"
     by (simp add: lcm_gcd normalize_mult div_mult_swap)
   then show ?thesis
     by (simp add: lcm_gcd)
 qed
-  
-lemma dvd_lcm2 [iff]:
-  "b dvd lcm a b"
+
+lemma dvd_lcm2 [iff]: "b dvd lcm a b"
 proof -
   have "normalize (a * b) div gcd a b = normalize b * (normalize a div gcd a b)"
     by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps)
@@ -235,85 +226,87 @@
     by (simp add: lcm_gcd)
 qed
 
-lemma dvd_lcmI1:
-  "a dvd b \<Longrightarrow> a dvd lcm b c"
-  by (rule dvd_trans) (assumption, blast) 
-
-lemma dvd_lcmI2:
-  "a dvd c \<Longrightarrow> a dvd lcm b c"
+lemma dvd_lcmI1: "a dvd b \<Longrightarrow> a dvd lcm b c"
+  by (rule dvd_trans) (assumption, blast)
+
+lemma dvd_lcmI2: "a dvd c \<Longrightarrow> a dvd lcm b c"
   by (rule dvd_trans) (assumption, blast)
 
-lemma lcm_dvdD1:
-  "lcm a b dvd c \<Longrightarrow> a dvd c"
+lemma lcm_dvdD1: "lcm a b dvd c \<Longrightarrow> a dvd c"
   using dvd_lcm1 [of a b] by (blast intro: dvd_trans)
 
-lemma lcm_dvdD2:
-  "lcm a b dvd c \<Longrightarrow> b dvd c"
+lemma lcm_dvdD2: "lcm a b dvd c \<Longrightarrow> b dvd c"
   using dvd_lcm2 [of a b] by (blast intro: dvd_trans)
 
 lemma lcm_least:
   assumes "a dvd c" and "b dvd c"
   shows "lcm a b dvd c"
 proof (cases "c = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
-  case False then have U: "is_unit (unit_factor c)" by simp
+  case False
+  then have *: "is_unit (unit_factor c)"
+    by simp
   show ?thesis
   proof (cases "gcd a b = 0")
-    case True with assms show ?thesis by simp
+    case True
+    with assms show ?thesis by simp
   next
-    case False then have "a \<noteq> 0 \<or> b \<noteq> 0" by simp
+    case False
+    then have "a \<noteq> 0 \<or> b \<noteq> 0"
+      by simp
     with \<open>c \<noteq> 0\<close> assms have "a * b dvd a * c" "a * b dvd c * b"
       by (simp_all add: mult_dvd_mono)
     then have "normalize (a * b) dvd gcd (a * c) (b * c)"
       by (auto intro: gcd_greatest simp add: ac_simps)
     then have "normalize (a * b) dvd gcd (a * c) (b * c) * unit_factor c"
-      using U by (simp add: dvd_mult_unit_iff)
+      using * by (simp add: dvd_mult_unit_iff)
     then have "normalize (a * b) dvd gcd a b * c"
       by (simp add: mult_gcd_right [of a b c])
     then have "normalize (a * b) div gcd a b dvd c"
       using False by (simp add: div_dvd_iff_mult ac_simps)
-    then show ?thesis by (simp add: lcm_gcd)
+    then show ?thesis
+      by (simp add: lcm_gcd)
   qed
 qed
 
-lemma lcm_least_iff [simp]:
-  "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
+lemma lcm_least_iff [simp]: "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
   by (blast intro!: lcm_least intro: dvd_trans)
 
-lemma normalize_lcm [simp]:
-  "normalize (lcm a b) = lcm a b"
+lemma normalize_lcm [simp]: "normalize (lcm a b) = lcm a b"
   by (simp add: lcm_gcd dvd_normalize_div)
 
-lemma lcm_0_left [simp]:
-  "lcm 0 a = 0"
+lemma lcm_0_left [simp]: "lcm 0 a = 0"
+  by (simp add: lcm_gcd)
+
+lemma lcm_0_right [simp]: "lcm a 0 = 0"
   by (simp add: lcm_gcd)
-  
-lemma lcm_0_right [simp]:
-  "lcm a 0 = 0"
-  by (simp add: lcm_gcd)
-
-lemma lcm_eq_0_iff:
-  "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" (is "?P \<longleftrightarrow> ?Q")
+
+lemma lcm_eq_0_iff: "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
+  (is "?P \<longleftrightarrow> ?Q")
 proof
-  assume ?P then have "0 dvd lcm a b" by simp
+  assume ?P
+  then have "0 dvd lcm a b"
+    by simp
   then have "0 dvd normalize (a * b) div gcd a b"
     by (simp add: lcm_gcd)
   then have "0 * gcd a b dvd normalize (a * b)"
     using dvd_div_iff_mult [of "gcd a b" _ 0] by (cases "gcd a b = 0") simp_all
   then have "normalize (a * b) = 0"
     by simp
-  then show ?Q by simp
+  then show ?Q
+    by simp
 next
-  assume ?Q then show ?P by auto
+  assume ?Q
+  then show ?P
+    by auto
 qed
 
-lemma lcm_eq_1_iff [simp]:
-  "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
+lemma lcm_eq_1_iff [simp]: "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
   by (auto intro: associated_eqI)
 
-lemma unit_factor_lcm :
-  "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
+lemma unit_factor_lcm: "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
   by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
 
 sublocale lcm: abel_semigroup lcm
@@ -332,8 +325,7 @@
     by (rule associated_eqI) simp_all
 qed
 
-lemma lcm_self [simp]:
-  "lcm a a = normalize a"
+lemma lcm_self [simp]: "lcm a a = normalize a"
 proof -
   have "lcm a a dvd a"
     by (rule lcm_least) simp_all
@@ -341,21 +333,17 @@
     by (auto intro: associated_eqI)
 qed
 
-lemma lcm_left_idem [simp]:
-  "lcm a (lcm a b) = lcm a b"
+lemma lcm_left_idem [simp]: "lcm a (lcm a b) = lcm a b"
   by (auto intro: associated_eqI)
 
-lemma lcm_right_idem [simp]:
-  "lcm (lcm a b) b = lcm a b"
+lemma lcm_right_idem [simp]: "lcm (lcm a b) b = lcm a b"
   unfolding lcm.commute [of a] lcm.commute [of "lcm b a"] by simp
 
-lemma gcd_mult_lcm [simp]:
-  "gcd a b * lcm a b = normalize a * normalize b"
+lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b"
   by (simp add: lcm_gcd normalize_mult)
 
-lemma lcm_mult_gcd [simp]:
-  "lcm a b * gcd a b = normalize a * normalize b"
-  using gcd_mult_lcm [of a b] by (simp add: ac_simps) 
+lemma lcm_mult_gcd [simp]: "lcm a b * gcd a b = normalize a * normalize b"
+  using gcd_mult_lcm [of a b] by (simp add: ac_simps)
 
 lemma gcd_lcm:
   assumes "a \<noteq> 0" and "b \<noteq> 0"
@@ -363,48 +351,43 @@
 proof -
   from assms have "lcm a b \<noteq> 0"
     by (simp add: lcm_eq_0_iff)
-  have "gcd a b * lcm a b = normalize a * normalize b" by simp
+  have "gcd a b * lcm a b = normalize a * normalize b"
+    by simp
   then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
     by (simp_all add: normalize_mult)
   with \<open>lcm a b \<noteq> 0\<close> show ?thesis
     using nonzero_mult_divide_cancel_right [of "lcm a b" "gcd a b"] by simp
 qed
 
-lemma lcm_1_left [simp]:
-  "lcm 1 a = normalize a"
+lemma lcm_1_left [simp]: "lcm 1 a = normalize a"
   by (simp add: lcm_gcd)
 
-lemma lcm_1_right [simp]:
-  "lcm a 1 = normalize a"
+lemma lcm_1_right [simp]: "lcm a 1 = normalize a"
   by (simp add: lcm_gcd)
-  
-lemma lcm_mult_left:
-  "lcm (c * a) (c * b) = normalize c * lcm a b"
+
+lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize c * lcm a b"
   by (cases "c = 0")
     (simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps,
       simp add: dvd_div_mult2_eq mult.left_commute [of "normalize c", symmetric])
 
-lemma lcm_mult_right:
-  "lcm (a * c) (b * c) = lcm b a * normalize c"
+lemma lcm_mult_right: "lcm (a * c) (b * c) = lcm b a * normalize c"
   using lcm_mult_left [of c a b] by (simp add: ac_simps)
 
-lemma mult_lcm_left:
-  "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
+lemma mult_lcm_left: "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
   by (simp add: lcm_mult_left mult.assoc [symmetric])
 
-lemma mult_lcm_right:
-  "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
+lemma mult_lcm_right: "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
   using mult_lcm_left [of c a b] by (simp add: ac_simps)
 
 lemma gcdI:
-  assumes "c dvd a" and "c dvd b" and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
+  assumes "c dvd a" and "c dvd b"
+    and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
     and "normalize c = c"
   shows "c = gcd a b"
   by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
 
-lemma gcd_unique: "d dvd a \<and> d dvd b \<and> 
-    normalize d = d \<and>
-    (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
+lemma gcd_unique:
+  "d dvd a \<and> d dvd b \<and> normalize d = d \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   by rule (auto intro: gcdI simp: gcd_greatest)
 
 lemma gcd_dvd_prod: "gcd a b dvd k * b"
@@ -418,27 +401,31 @@
 
 lemma gcd_proj1_iff: "gcd m n = normalize m \<longleftrightarrow> m dvd n"
 proof
-  assume A: "gcd m n = normalize m"
+  assume *: "gcd m n = normalize m"
   show "m dvd n"
   proof (cases "m = 0")
-    assume [simp]: "m \<noteq> 0"
-    from A have B: "m = gcd m n * unit_factor m"
+    case True
+    with * show ?thesis by simp
+  next
+    case [simp]: False
+    from * have **: "m = gcd m n * unit_factor m"
       by (simp add: unit_eq_div2)
-    show ?thesis by (subst B, simp add: mult_unit_dvd_iff)
-  qed (insert A, simp)
+    show ?thesis
+      by (subst **) (simp add: mult_unit_dvd_iff)
+  qed
 next
   assume "m dvd n"
-  then show "gcd m n = normalize m" by (rule gcd_proj1_if_dvd)
+  then show "gcd m n = normalize m"
+    by (rule gcd_proj1_if_dvd)
 qed
-  
+
 lemma gcd_proj2_iff: "gcd m n = normalize n \<longleftrightarrow> n dvd m"
   using gcd_proj1_iff [of n m] by (simp add: ac_simps)
 
 lemma gcd_mult_distrib': "normalize c * gcd a b = gcd (c * a) (c * b)"
   by (rule gcdI) (auto simp: normalize_mult gcd_greatest mult_dvd_mono gcd_mult_left[symmetric])
 
-lemma gcd_mult_distrib:
-  "k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
+lemma gcd_mult_distrib: "k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
 proof-
   have "normalize k * gcd a b = gcd (k * a) (k * b)"
     by (simp add: gcd_mult_distrib')
@@ -450,29 +437,27 @@
     by simp
 qed
 
-lemma lcm_mult_unit1:
-  "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
+lemma lcm_mult_unit1: "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
   by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)
 
-lemma lcm_mult_unit2:
-  "is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c"
+lemma lcm_mult_unit2: "is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c"
   using lcm_mult_unit1 [of a c b] by (simp add: ac_simps)
 
 lemma lcm_div_unit1:
   "is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c"
-  by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1) 
-
-lemma lcm_div_unit2:
-  "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
+  by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1)
+
+lemma lcm_div_unit2: "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
   by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)
 
-lemma normalize_lcm_left [simp]:
-  "lcm (normalize a) b = lcm a b"
+lemma normalize_lcm_left [simp]: "lcm (normalize a) b = lcm a b"
 proof (cases "a = 0")
-  case True then show ?thesis
+  case True
+  then show ?thesis
     by simp
 next
-  case False then have "is_unit (unit_factor a)"
+  case False
+  then have "is_unit (unit_factor a)"
     by simp
   moreover have "normalize a = a div unit_factor a"
     by simp
@@ -480,18 +465,23 @@
     by (simp only: lcm_div_unit1)
 qed
 
-lemma normalize_lcm_right [simp]:
-  "lcm a (normalize b) = lcm a b"
+lemma normalize_lcm_right [simp]: "lcm a (normalize b) = lcm a b"
   using normalize_lcm_left [of b a] by (simp add: ac_simps)
 
 lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
   apply (rule gcdI)
-  apply simp_all
-  apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps)
+     apply simp_all
+  apply (rule dvd_trans)
+   apply (rule gcd_dvd1)
+  apply (simp add: unit_simps)
   done
 
 lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
-  by (subst gcd.commute, subst gcd_mult_unit1, assumption, rule gcd.commute)
+  apply (subst gcd.commute)
+  apply (subst gcd_mult_unit1)
+   apply assumption
+  apply (rule gcd.commute)
+  done
 
 lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
   by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
@@ -499,13 +489,14 @@
 lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
   by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
 
-lemma normalize_gcd_left [simp]:
-  "gcd (normalize a) b = gcd a b"
+lemma normalize_gcd_left [simp]: "gcd (normalize a) b = gcd a b"
 proof (cases "a = 0")
-  case True then show ?thesis
+  case True
+  then show ?thesis
     by simp
 next
-  case False then have "is_unit (unit_factor a)"
+  case False
+  then have "is_unit (unit_factor a)"
     by simp
   moreover have "normalize a = a div unit_factor a"
     by simp
@@ -513,8 +504,7 @@
     by (simp only: gcd_div_unit1)
 qed
 
-lemma normalize_gcd_right [simp]:
-  "gcd a (normalize b) = gcd a b"
+lemma normalize_gcd_right [simp]: "gcd a (normalize b) = gcd a b"
   using normalize_gcd_left [of b a] by (simp add: ac_simps)
 
 lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
@@ -523,58 +513,66 @@
 lemma comp_fun_idem_lcm: "comp_fun_idem lcm"
   by standard (simp_all add: fun_eq_iff ac_simps)
 
-lemma gcd_dvd_antisym:
-  "gcd a b dvd gcd c d \<Longrightarrow> gcd c d dvd gcd a b \<Longrightarrow> gcd a b = gcd c d"
+lemma gcd_dvd_antisym: "gcd a b dvd gcd c d \<Longrightarrow> gcd c d dvd gcd a b \<Longrightarrow> gcd a b = gcd c d"
 proof (rule gcdI)
-  assume A: "gcd a b dvd gcd c d" and B: "gcd c d dvd gcd a b"
-  have "gcd c d dvd c" by simp
-  with A show "gcd a b dvd c" by (rule dvd_trans)
-  have "gcd c d dvd d" by simp
-  with A show "gcd a b dvd d" by (rule dvd_trans)
+  assume *: "gcd a b dvd gcd c d"
+    and **: "gcd c d dvd gcd a b"
+  have "gcd c d dvd c"
+    by simp
+  with * show "gcd a b dvd c"
+    by (rule dvd_trans)
+  have "gcd c d dvd d"
+    by simp
+  with * show "gcd a b dvd d"
+    by (rule dvd_trans)
   show "normalize (gcd a b) = gcd a b"
     by simp
   fix l assume "l dvd c" and "l dvd d"
-  hence "l dvd gcd c d" by (rule gcd_greatest)
-  from this and B show "l dvd gcd a b" by (rule dvd_trans)
+  then have "l dvd gcd c d"
+    by (rule gcd_greatest)
+  from this and ** show "l dvd gcd a b"
+    by (rule dvd_trans)
 qed
 
 lemma coprime_dvd_mult:
   assumes "coprime a b" and "a dvd c * b"
   shows "a dvd c"
 proof (cases "c = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
   case False
-  then have unit: "is_unit (unit_factor c)" by simp
+  then have unit: "is_unit (unit_factor c)"
+    by simp
   from \<open>coprime a b\<close> mult_gcd_left [of c a b]
   have "gcd (c * a) (c * b) * unit_factor c = c"
     by (simp add: ac_simps)
   moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
     by (simp add: dvd_mult_unit_iff unit)
-  ultimately show ?thesis by simp
+  ultimately show ?thesis
+    by simp
 qed
 
-lemma coprime_dvd_mult_iff:
-  assumes "coprime a c"
-  shows "a dvd b * c \<longleftrightarrow> a dvd b"
-  using assms by (auto intro: coprime_dvd_mult)
-
-lemma gcd_mult_cancel:
-  "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
+lemma coprime_dvd_mult_iff: "coprime a c \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd b"
+  by (auto intro: coprime_dvd_mult)
+
+lemma gcd_mult_cancel: "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
   apply (rule associated_eqI)
-  apply (rule gcd_greatest)
-  apply (rule_tac b = c in coprime_dvd_mult)
-  apply (simp add: gcd.assoc)
-  apply (simp_all add: ac_simps)
+     apply (rule gcd_greatest)
+      apply (rule_tac b = c in coprime_dvd_mult)
+       apply (simp add: gcd.assoc)
+       apply (simp_all add: ac_simps)
   done
 
 lemma coprime_crossproduct:
-  fixes a b c d
+  fixes a b c d :: 'a
   assumes "coprime a d" and "coprime b c"
-  shows "normalize a * normalize c = normalize b * normalize d
-    \<longleftrightarrow> normalize a = normalize b \<and> normalize c = normalize d" (is "?lhs \<longleftrightarrow> ?rhs")
+  shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
+    normalize a = normalize b \<and> normalize c = normalize d"
+    (is "?lhs \<longleftrightarrow> ?rhs")
 proof
-  assume ?rhs then show ?lhs by simp
+  assume ?rhs
+  then show ?lhs by simp
 next
   assume ?lhs
   from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
@@ -609,8 +607,8 @@
 lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
   by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
 
-lemma coprimeI: "(\<And>l. \<lbrakk>l dvd a; l dvd b\<rbrakk> \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
-  by (rule sym, rule gcdI, simp_all)
+lemma coprimeI: "(\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
+  by (rule sym, rule gcdI) simp_all
 
 lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
   by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
@@ -623,27 +621,29 @@
   let ?a' = "a div ?g"
   let ?b' = "b div ?g"
   let ?g' = "gcd ?a' ?b'"
-  have dvdg: "?g dvd a" "?g dvd b" by simp_all
-  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
+  have dvdg: "?g dvd a" "?g dvd b"
+    by simp_all
+  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
+    by simp_all
   from dvdg dvdg' obtain ka kb ka' kb' where
-      kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
+    kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
     unfolding dvd_def by blast
   from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
     by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
-    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
-      dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
-  have "?g \<noteq> 0" using nz by simp
+    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
+  have "?g \<noteq> 0"
+    using nz by simp
   moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
-  thm dvd_mult_cancel_left
-  ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
+  ultimately show ?thesis
+    using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
 qed
 
 
 lemma divides_mult:
   assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
   shows "a * b dvd c"
-proof-
+proof -
   from \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
   with \<open>a dvd c\<close> have "a dvd b' * b"
     by (simp add: ac_simps)
@@ -656,70 +656,88 @@
 qed
 
 lemma coprime_lmult:
-  assumes dab: "gcd d (a * b) = 1" 
+  assumes dab: "gcd d (a * b) = 1"
   shows "gcd d a = 1"
 proof (rule coprimeI)
-  fix l assume "l dvd d" and "l dvd a"
-  hence "l dvd a * b" by simp
-  with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest)
+  fix l
+  assume "l dvd d" and "l dvd a"
+  then have "l dvd a * b"
+    by simp
+  with \<open>l dvd d\<close> and dab show "l dvd 1"
+    by (auto intro: gcd_greatest)
 qed
 
 lemma coprime_rmult:
   assumes dab: "gcd d (a * b) = 1"
   shows "gcd d b = 1"
 proof (rule coprimeI)
-  fix l assume "l dvd d" and "l dvd b"
-  hence "l dvd a * b" by simp
-  with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest)
+  fix l
+  assume "l dvd d" and "l dvd b"
+  then have "l dvd a * b"
+    by simp
+  with \<open>l dvd d\<close> and dab show "l dvd 1"
+    by (auto intro: gcd_greatest)
 qed
 
 lemma coprime_mult:
-  assumes da: "coprime d a" and db: "coprime d b"
+  assumes "coprime d a"
+    and "coprime d b"
   shows "coprime d (a * b)"
   apply (subst gcd.commute)
-  using da apply (subst gcd_mult_cancel)
-  apply (subst gcd.commute, assumption)
-  apply (subst gcd.commute, rule db)
+  using assms(1) apply (subst gcd_mult_cancel)
+   apply (subst gcd.commute)
+   apply assumption
+  apply (subst gcd.commute)
+  apply (rule assms(2))
   done
 
 lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1"
-  using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b] by blast
+  using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b]
+  by blast
 
 lemma gcd_coprime:
-  assumes c: "gcd a b \<noteq> 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b"
+  assumes c: "gcd a b \<noteq> 0"
+    and a: "a = a' * gcd a b"
+    and b: "b = b' * gcd a b"
   shows "gcd a' b' = 1"
 proof -
-  from c have "a \<noteq> 0 \<or> b \<noteq> 0" by simp
+  from c have "a \<noteq> 0 \<or> b \<noteq> 0"
+    by simp
   with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" .
-  also from assms have "a div gcd a b = a'" using dvd_div_eq_mult local.gcd_dvd1 by blast
-  also from assms have "b div gcd a b = b'" using dvd_div_eq_mult local.gcd_dvd1 by blast
+  also from assms have "a div gcd a b = a'"
+    using dvd_div_eq_mult local.gcd_dvd1 by blast
+  also from assms have "b div gcd a b = b'"
+    using dvd_div_eq_mult local.gcd_dvd1 by blast
   finally show ?thesis .
 qed
 
 lemma coprime_power:
   assumes "0 < n"
   shows "gcd a (b ^ n) = 1 \<longleftrightarrow> gcd a b = 1"
-using assms proof (induct n)
-  case (Suc n) then show ?case
+  using assms
+proof (induct n)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  then show ?case
     by (cases n) (simp_all add: coprime_mul_eq)
-qed simp
+qed
 
 lemma gcd_coprime_exists:
-  assumes nz: "gcd a b \<noteq> 0"
+  assumes "gcd a b \<noteq> 0"
   shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1"
   apply (rule_tac x = "a div gcd a b" in exI)
   apply (rule_tac x = "b div gcd a b" in exI)
-  apply (insert nz, auto intro: div_gcd_coprime)
+  using assms
+  apply (auto intro: div_gcd_coprime)
   done
 
-lemma coprime_exp:
-  "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1"
-  by (induct n, simp_all add: coprime_mult)
-
-lemma coprime_exp_left:
-  assumes "coprime a b"
-  shows "coprime (a ^ n) b"
-  using assms by (induct n) (simp_all add: gcd_mult_cancel)
+lemma coprime_exp: "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1"
+  by (induct n) (simp_all add: coprime_mult)
+
+lemma coprime_exp_left: "coprime a b \<Longrightarrow> coprime (a ^ n) b"
+  by (induct n) (simp_all add: gcd_mult_cancel)
 
 lemma coprime_exp2:
   assumes "coprime a b"
@@ -729,55 +747,75 @@
     by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
 qed
 
-lemma gcd_exp:
-  "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
+lemma gcd_exp: "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
 proof (cases "a = 0 \<and> b = 0")
   case True
-  then show ?thesis by (cases n) simp_all
+  then show ?thesis
+    by (cases n) simp_all
 next
   case False
   then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
     using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp
-  then have "gcd a b ^ n = gcd a b ^ n * ..." by simp
+  then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
+    by simp
   also note gcd_mult_distrib
   also have "unit_factor (gcd a b ^ n) = 1"
     using False by (auto simp add: unit_factor_power unit_factor_gcd)
   also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
-    by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp)
+    apply (subst ac_simps)
+    apply (subst div_power)
+     apply simp
+    apply (rule dvd_div_mult_self)
+    apply (rule dvd_power_same)
+    apply simp
+    done
   also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
-    by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp)
+    apply (subst ac_simps)
+    apply (subst div_power)
+     apply simp
+    apply (rule dvd_div_mult_self)
+    apply (rule dvd_power_same)
+    apply simp
+    done
   finally show ?thesis by simp
 qed
 
-lemma coprime_common_divisor: 
-  "gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
+lemma coprime_common_divisor: "gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
   apply (subgoal_tac "a dvd gcd a b")
-  apply simp
+   apply simp
   apply (erule (1) gcd_greatest)
   done
 
-lemma division_decomp: 
-  assumes dc: "a dvd b * c"
+lemma division_decomp:
+  assumes "a dvd b * c"
   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
 proof (cases "gcd a b = 0")
-  assume "gcd a b = 0"
-  hence "a = 0 \<and> b = 0" by simp
-  hence "a = 0 * c \<and> 0 dvd b \<and> c dvd c" by simp
+  case True
+  then have "a = 0 \<and> b = 0"
+    by simp
+  then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
+    by simp
   then show ?thesis by blast
 next
+  case False
   let ?d = "gcd a b"
-  assume "?d \<noteq> 0"
-  from gcd_coprime_exists[OF this]
+  from gcd_coprime_exists [OF False]
     obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
     by blast
-  from ab'(1) have "a' dvd a" unfolding dvd_def by blast
-  with dc have "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
-  from dc ab'(1,2) have "a'*?d dvd (b'*?d) * c" by simp
-  hence "?d * a' dvd ?d * (b' * c)" by (simp add: mult_ac)
-  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c" by simp
-  with coprime_dvd_mult[OF ab'(3)] 
-    have "a' dvd c" by (subst (asm) ac_simps, blast)
-  with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c" by (simp add: mult_ac)
+  from ab'(1) have "a' dvd a"
+    unfolding dvd_def by blast
+  with assms have "a' dvd b * c"
+    using dvd_trans[of a' a "b*c"] by simp
+  from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
+    by simp
+  then have "?d * a' dvd ?d * (b' * c)"
+    by (simp add: mult_ac)
+  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
+    by simp
+  with coprime_dvd_mult[OF ab'(3)] have "a' dvd c"
+    by (subst (asm) ac_simps) blast
+  with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
+    by (simp add: mult_ac)
   then show ?thesis by blast
 qed
 
@@ -785,62 +823,70 @@
   assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0"
   shows "a dvd b"
 proof (cases "gcd a b = 0")
-  assume "gcd a b = 0"
+  case True
   then show ?thesis by simp
 next
+  case False
   let ?d = "gcd a b"
-  assume "?d \<noteq> 0"
-  from n obtain m where m: "n = Suc m" by (cases n, simp_all)
-  from \<open>?d \<noteq> 0\<close> have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero)
-  from gcd_coprime_exists[OF \<open>?d \<noteq> 0\<close>]
-    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
+  from n obtain m where m: "n = Suc m"
+    by (cases n) simp_all
+  from False have zn: "?d ^ n \<noteq> 0"
+    by (rule power_not_zero)
+  from gcd_coprime_exists [OF False]
+  obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
     by blast
   from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
     by (simp add: ab'(1,2)[symmetric])
-  hence "?d^n * a'^n dvd ?d^n * b'^n"
+  then have "?d^n * a'^n dvd ?d^n * b'^n"
     by (simp only: power_mult_distrib ac_simps)
-  with zn have "a'^n dvd b'^n" by simp
-  hence "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
-  hence "a' dvd b'^m * b'" by (simp add: m ac_simps)
+  with zn have "a'^n dvd b'^n"
+    by simp
+  then have "a' dvd b'^n"
+    using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
+  then have "a' dvd b'^m * b'"
+    by (simp add: m ac_simps)
   with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]]
-    have "a' dvd b'" by (subst (asm) ac_simps, blast)
-  hence "a'*?d dvd b'*?d" by (rule mult_dvd_mono, simp)
-  with ab'(1,2) show ?thesis by simp
+  have "a' dvd b'" by (subst (asm) ac_simps) blast
+  then have "a' * ?d dvd b' * ?d"
+    by (rule mult_dvd_mono) simp
+  with ab'(1,2) show ?thesis
+    by simp
 qed
 
-lemma pow_divs_eq [simp]:
-  "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
+lemma pow_divs_eq [simp]: "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
   by (auto intro: pow_divs_pow dvd_power_same)
 
 lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
-  by (subst add_commute, simp)
-
-lemma setprod_coprime [rule_format]:
-  "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
+  by (subst add_commute) simp
+
+lemma setprod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
   apply (cases "finite A")
-  apply (induct set: finite)
-  apply (auto simp add: gcd_mult_cancel)
+   apply (induct set: finite)
+    apply (auto simp add: gcd_mult_cancel)
   done
-  
-lemma listprod_coprime:
-  "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (listprod xs) y" 
-  by (induction xs) (simp_all add: gcd_mult_cancel)
-
-lemma coprime_divisors: 
+
+lemma listprod_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (listprod xs) y"
+  by (induct xs) (simp_all add: gcd_mult_cancel)
+
+lemma coprime_divisors:
   assumes "d dvd a" "e dvd b" "gcd a b = 1"
-  shows "gcd d e = 1" 
+  shows "gcd d e = 1"
 proof -
   from assms obtain k l where "a = d * k" "b = e * l"
     unfolding dvd_def by blast
-  with assms have "gcd (d * k) (e * l) = 1" by simp
-  hence "gcd (d * k) e = 1" by (rule coprime_lmult)
-  also have "gcd (d * k) e = gcd e (d * k)" by (simp add: ac_simps)
-  finally have "gcd e d = 1" by (rule coprime_lmult)
-  then show ?thesis by (simp add: ac_simps)
+  with assms have "gcd (d * k) (e * l) = 1"
+    by simp
+  then have "gcd (d * k) e = 1"
+    by (rule coprime_lmult)
+  also have "gcd (d * k) e = gcd e (d * k)"
+    by (simp add: ac_simps)
+  finally have "gcd e d = 1"
+    by (rule coprime_lmult)
+  then show ?thesis
+    by (simp add: ac_simps)
 qed
 
-lemma lcm_gcd_prod:
-  "lcm a b * gcd a b = normalize (a * b)"
+lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
   by (simp add: lcm_gcd)
 
 declare unit_factor_lcm [simp]
@@ -851,48 +897,49 @@
   shows "c = lcm a b"
   by (rule associated_eqI) (auto simp: assms intro: lcm_least)
 
-lemma gcd_dvd_lcm [simp]:
-  "gcd a b dvd lcm a b"
+lemma gcd_dvd_lcm [simp]: "gcd a b dvd lcm a b"
   using gcd_dvd2 by (rule dvd_lcmI2)
 
 lemmas lcm_0 = lcm_0_right
 
 lemma lcm_unique:
-  "a dvd d \<and> b dvd d \<and> 
-  normalize d = d \<and>
-  (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
+  "a dvd d \<and> b dvd d \<and> normalize d = d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)
 
-lemma lcm_coprime:
-  "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
+lemma lcm_coprime: "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
   by (subst lcm_gcd) simp
 
-lemma lcm_proj1_if_dvd: 
-  "b dvd a \<Longrightarrow> lcm a b = normalize a"
-  by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all)
-
-lemma lcm_proj2_if_dvd: 
-  "a dvd b \<Longrightarrow> lcm a b = normalize b"
+lemma lcm_proj1_if_dvd: "b dvd a \<Longrightarrow> lcm a b = normalize a"
+  apply (cases "a = 0")
+   apply simp
+  apply (rule sym)
+  apply (rule lcmI)
+     apply simp_all
+  done
+
+lemma lcm_proj2_if_dvd: "a dvd b \<Longrightarrow> lcm a b = normalize b"
   using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)
 
-lemma lcm_proj1_iff:
-  "lcm m n = normalize m \<longleftrightarrow> n dvd m"
+lemma lcm_proj1_iff: "lcm m n = normalize m \<longleftrightarrow> n dvd m"
 proof
-  assume A: "lcm m n = normalize m"
+  assume *: "lcm m n = normalize m"
   show "n dvd m"
   proof (cases "m = 0")
-    assume [simp]: "m \<noteq> 0"
-    from A have B: "m = lcm m n * unit_factor m"
+    case True
+    then show ?thesis by simp
+  next
+    case [simp]: False
+    from * have **: "m = lcm m n * unit_factor m"
       by (simp add: unit_eq_div2)
-    show ?thesis by (subst B, simp)
-  qed simp
+    show ?thesis by (subst **) simp
+  qed
 next
   assume "n dvd m"
-  then show "lcm m n = normalize m" by (rule lcm_proj1_if_dvd)
+  then show "lcm m n = normalize m"
+    by (rule lcm_proj1_if_dvd)
 qed
 
-lemma lcm_proj2_iff:
-  "lcm m n = normalize n \<longleftrightarrow> m dvd n"
+lemma lcm_proj2_iff: "lcm m n = normalize n \<longleftrightarrow> m dvd n"
   using lcm_proj1_iff [of n m] by (simp add: ac_simps)
 
 end
@@ -903,33 +950,29 @@
 lemma coprime_minus_one: "coprime (n - 1) n"
   using coprime_plus_one[of "n - 1"] by (simp add: gcd.commute)
 
-lemma gcd_neg1 [simp]:
-  "gcd (-a) b = gcd a b"
-  by (rule sym, rule gcdI, simp_all add: gcd_greatest)
-
-lemma gcd_neg2 [simp]:
-  "gcd a (-b) = gcd a b"
-  by (rule sym, rule gcdI, simp_all add: gcd_greatest)
-
-lemma gcd_neg_numeral_1 [simp]:
-  "gcd (- numeral n) a = gcd (numeral n) a"
+lemma gcd_neg1 [simp]: "gcd (-a) b = gcd a b"
+  by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
+
+lemma gcd_neg2 [simp]: "gcd a (-b) = gcd a b"
+  by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
+
+lemma gcd_neg_numeral_1 [simp]: "gcd (- numeral n) a = gcd (numeral n) a"
   by (fact gcd_neg1)
 
-lemma gcd_neg_numeral_2 [simp]:
-  "gcd a (- numeral n) = gcd a (numeral n)"
+lemma gcd_neg_numeral_2 [simp]: "gcd a (- numeral n) = gcd a (numeral n)"
   by (fact gcd_neg2)
 
 lemma gcd_diff1: "gcd (m - n) n = gcd m n"
-  by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric],  subst gcd_add1, simp)
+  by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric], subst gcd_add1, simp)
 
 lemma gcd_diff2: "gcd (n - m) n = gcd m n"
-  by (subst gcd_neg1[symmetric], simp only: minus_diff_eq gcd_diff1)
+  by (subst gcd_neg1[symmetric]) (simp only: minus_diff_eq gcd_diff1)
 
 lemma lcm_neg1 [simp]: "lcm (-a) b = lcm a b"
-  by (rule sym, rule lcmI, simp_all add: lcm_least lcm_eq_0_iff)
+  by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff)
 
 lemma lcm_neg2 [simp]: "lcm a (-b) = lcm a b"
-  by (rule sym, rule lcmI, simp_all add: lcm_least lcm_eq_0_iff)
+  by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff)
 
 lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) a = lcm (numeral n) a"
   by (fact lcm_neg1)
@@ -948,24 +991,19 @@
     and normalize_Lcm [simp]: "normalize (Lcm A) = Lcm A"
 begin
 
-lemma Lcm_Gcd:
-  "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
+lemma Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
   by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
 
-lemma Gcd_Lcm:
-  "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
+lemma Gcd_Lcm: "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
   by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
 
-lemma Gcd_empty [simp]:
-  "Gcd {} = 0"
+lemma Gcd_empty [simp]: "Gcd {} = 0"
   by (rule dvd_0_left, rule Gcd_greatest) simp
 
-lemma Lcm_empty [simp]:
-  "Lcm {} = 1"
+lemma Lcm_empty [simp]: "Lcm {} = 1"
   by (auto intro: associated_eqI Lcm_least)
 
-lemma Gcd_insert [simp]:
-  "Gcd (insert a A) = gcd a (Gcd A)"
+lemma Gcd_insert [simp]: "Gcd (insert a A) = gcd a (Gcd A)"
 proof -
   have "Gcd (insert a A) dvd gcd a (Gcd A)"
     by (auto intro: Gcd_dvd Gcd_greatest)
@@ -975,20 +1013,24 @@
     assume "b \<in> insert a A"
     then show "gcd a (Gcd A) dvd b"
     proof
-      assume "b = a" then show ?thesis by simp
+      assume "b = a"
+      then show ?thesis
+        by simp
     next
       assume "b \<in> A"
-      then have "Gcd A dvd b" by (rule Gcd_dvd)
-      moreover have "gcd a (Gcd A) dvd Gcd A" by simp
-      ultimately show ?thesis by (blast intro: dvd_trans)
+      then have "Gcd A dvd b"
+        by (rule Gcd_dvd)
+      moreover have "gcd a (Gcd A) dvd Gcd A"
+        by simp
+      ultimately show ?thesis
+        by (blast intro: dvd_trans)
     qed
   qed
   ultimately show ?thesis
     by (auto intro: associated_eqI)
 qed
 
-lemma Lcm_insert [simp]:
-  "Lcm (insert a A) = lcm a (Lcm A)"
+lemma Lcm_insert [simp]: "Lcm (insert a A) = lcm a (Lcm A)"
 proof (rule sym)
   have "lcm a (Lcm A) dvd Lcm (insert a A)"
     by (auto intro: dvd_Lcm Lcm_least)
@@ -998,12 +1040,16 @@
     assume "b \<in> insert a A"
     then show "b dvd lcm a (Lcm A)"
     proof
-      assume "b = a" then show ?thesis by simp
+      assume "b = a"
+      then show ?thesis by simp
     next
       assume "b \<in> A"
-      then have "b dvd Lcm A" by (rule dvd_Lcm)
-      moreover have "Lcm A dvd lcm a (Lcm A)" by simp
-      ultimately show ?thesis by (blast intro: dvd_trans)
+      then have "b dvd Lcm A"
+        by (rule dvd_Lcm)
+      moreover have "Lcm A dvd lcm a (Lcm A)"
+        by simp
+      ultimately show ?thesis
+        by (blast intro: dvd_trans)
     qed
   qed
   ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
@@ -1011,37 +1057,39 @@
 qed
 
 lemma LcmI:
-  assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c"
-    and "normalize b = b" shows "b = Lcm A"
+  assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b"
+    and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c"
+    and "normalize b = b"
+  shows "b = Lcm A"
   by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least)
 
-lemma Lcm_subset:
-  "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
+lemma Lcm_subset: "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
   by (blast intro: Lcm_least dvd_Lcm)
 
-lemma Lcm_Un:
-  "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)"
+lemma Lcm_Un: "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)"
   apply (rule lcmI)
-  apply (blast intro: Lcm_subset)
-  apply (blast intro: Lcm_subset)
-  apply (intro Lcm_least ballI, elim UnE)
-  apply (rule dvd_trans, erule dvd_Lcm, assumption)
-  apply (rule dvd_trans, erule dvd_Lcm, assumption)
+     apply (blast intro: Lcm_subset)
+    apply (blast intro: Lcm_subset)
+   apply (intro Lcm_least ballI, elim UnE)
+    apply (rule dvd_trans, erule dvd_Lcm, assumption)
+   apply (rule dvd_trans, erule dvd_Lcm, assumption)
   apply simp
   done
-  
-
-lemma Gcd_0_iff [simp]:
-  "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q")
+
+lemma Gcd_0_iff [simp]: "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}"
+  (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?P
   show ?Q
   proof
     fix a
     assume "a \<in> A"
-    then have "Gcd A dvd a" by (rule Gcd_dvd)
-    with \<open>?P\<close> have "a = 0" by simp
-    then show "a \<in> {0}" by simp
+    then have "Gcd A dvd a"
+      by (rule Gcd_dvd)
+    with \<open>?P\<close> have "a = 0"
+      by simp
+    then show "a \<in> {0}"
+      by simp
   qed
 next
   assume ?Q
@@ -1049,14 +1097,17 @@
   proof (rule Gcd_greatest)
     fix a
     assume "a \<in> A"
-    with \<open>?Q\<close> have "a = 0" by auto
-    then show "0 dvd a" by simp
+    with \<open>?Q\<close> have "a = 0"
+      by auto
+    then show "0 dvd a"
+      by simp
   qed
-  then show ?P by simp
+  then show ?P
+    by simp
 qed
 
-lemma Lcm_1_iff [simp]:
-  "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)" (is "?P \<longleftrightarrow> ?Q")
+lemma Lcm_1_iff [simp]: "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)"
+  (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?P
   show ?Q
@@ -1078,10 +1129,11 @@
     by simp
 qed
 
-lemma unit_factor_Lcm:
-  "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
+lemma unit_factor_Lcm: "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
 proof (cases "Lcm A = 0")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis
+    by simp
 next
   case False
   with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
@@ -1091,13 +1143,11 @@
 qed
 
 lemma unit_factor_Gcd: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
-proof -
-  show "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
-    by (simp add: Gcd_Lcm unit_factor_Lcm)
-qed
+  by (simp add: Gcd_Lcm unit_factor_Lcm)
 
 lemma GcdI:
-  assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b"
+  assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a"
+    and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b"
     and "normalize b = b"
   shows "b = Gcd A"
   by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest)
@@ -1124,52 +1174,50 @@
     by simp
 qed
 
-lemma Gcd_UNIV [simp]:
-  "Gcd UNIV = 1"
+lemma Gcd_UNIV [simp]: "Gcd UNIV = 1"
   using dvd_refl by (rule Gcd_eq_1_I) simp
 
-lemma Lcm_UNIV [simp]:
-  "Lcm UNIV = 0"
+lemma Lcm_UNIV [simp]: "Lcm UNIV = 0"
   by (rule Lcm_eq_0_I) simp
 
 lemma Lcm_0_iff:
   assumes "finite A"
   shows "Lcm A = 0 \<longleftrightarrow> 0 \<in> A"
 proof (cases "A = {}")
-  case True then show ?thesis by simp
+  case True
+  then show ?thesis by simp
 next
-  case False with assms show ?thesis
-    by (induct A rule: finite_ne_induct)
-      (auto simp add: lcm_eq_0_iff)
+  case False
+  with assms show ?thesis
+    by (induct A rule: finite_ne_induct) (auto simp add: lcm_eq_0_iff)
 qed
 
 lemma Gcd_finite:
   assumes "finite A"
   shows "Gcd A = Finite_Set.fold gcd 0 A"
   by (induct rule: finite.induct[OF \<open>finite A\<close>])
-     (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
+    (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
 
 lemma Gcd_set [code_unfold]: "Gcd (set as) = foldl gcd 0 as"
-  by (simp add: Gcd_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] 
-                foldl_conv_fold gcd.commute)
+  by (simp add: Gcd_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd]
+      foldl_conv_fold gcd.commute)
 
 lemma Lcm_finite:
   assumes "finite A"
   shows "Lcm A = Finite_Set.fold lcm 1 A"
   by (induct rule: finite.induct[OF \<open>finite A\<close>])
-     (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
-
-lemma Lcm_set [code_unfold]:
-  "Lcm (set as) = foldl lcm 1 as"
-  by (simp add: Lcm_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] 
-                foldl_conv_fold lcm.commute)
-
-lemma Gcd_image_normalize [simp]:
-  "Gcd (normalize ` A) = Gcd A"
+    (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
+
+lemma Lcm_set [code_unfold]: "Lcm (set as) = foldl lcm 1 as"
+  by (simp add: Lcm_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm]
+      foldl_conv_fold lcm.commute)
+
+lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A"
 proof -
   have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
   proof -
-    from that obtain B where "A = insert a B" by blast
+    from that obtain B where "A = insert a B"
+      by blast
     moreover have "gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
       by (rule gcd_dvd1)
     ultimately show "Gcd (normalize ` A) dvd a"
@@ -1188,22 +1236,22 @@
   shows "Gcd A = a"
   using assms by (blast intro: associated_eqI Gcd_greatest Gcd_dvd normalize_Gcd)
 
-lemma dvd_GcdD:
-  assumes "x dvd Gcd A" "y \<in> A"
-  shows   "x dvd y"
-  using assms Gcd_dvd dvd_trans by blast
-
-lemma dvd_Gcd_iff:
-  "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
+lemma dvd_GcdD: "x dvd Gcd A \<Longrightarrow> y \<in> A \<Longrightarrow> x dvd y"
+  using Gcd_dvd dvd_trans by blast
+
+lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
   by (blast dest: dvd_GcdD intro: Gcd_greatest)
 
 lemma Gcd_mult: "Gcd (op * c ` A) = normalize c * Gcd A"
 proof (cases "c = 0")
+  case True
+  then show ?thesis by auto
+next
   case [simp]: False
   have "Gcd (op * c ` A) div c dvd Gcd A"
     by (intro Gcd_greatest, subst div_dvd_iff_mult)
        (auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
-  hence "Gcd (op * c ` A) dvd c * Gcd A"
+  then have "Gcd (op * c ` A) dvd c * Gcd A"
     by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
   also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c"
     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
@@ -1214,43 +1262,45 @@
     by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
   ultimately have "normalize (Gcd (op * c ` A)) = normalize (normalize c * Gcd A)"
     by (rule associatedI)
-  thus ?thesis by (simp add: normalize_mult)
-qed auto
+  then show ?thesis
+    by (simp add: normalize_mult)
+qed
 
 lemma Lcm_eqI:
   assumes "normalize a = a"
-  assumes "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
+    and "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
     and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> b dvd c) \<Longrightarrow> a dvd c"
   shows "Lcm A = a"
   using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm)
 
-lemma Lcm_dvdD:
-  assumes "Lcm A dvd x" "y \<in> A"
-  shows   "y dvd x"
-  using assms dvd_Lcm dvd_trans by blast
-
-lemma Lcm_dvd_iff:
-  "Lcm A dvd x \<longleftrightarrow> (\<forall>y\<in>A. y dvd x)"
+lemma Lcm_dvdD: "Lcm A dvd x \<Longrightarrow> y \<in> A \<Longrightarrow> y dvd x"
+  using dvd_Lcm dvd_trans by blast
+
+lemma Lcm_dvd_iff: "Lcm A dvd x \<longleftrightarrow> (\<forall>y\<in>A. y dvd x)"
   by (blast dest: Lcm_dvdD intro: Lcm_least)
 
-lemma Lcm_mult: 
+lemma Lcm_mult:
   assumes "A \<noteq> {}"
-  shows   "Lcm (op * c ` A) = normalize c * Lcm A"
+  shows "Lcm (op * c ` A) = normalize c * Lcm A"
 proof (cases "c = 0")
   case True
-  moreover from assms this have "op * c ` A = {0}" by auto
-  ultimately show ?thesis by auto
+  with assms have "op * c ` A = {0}"
+    by auto
+  with True show ?thesis by auto
 next
   case [simp]: False
-  from assms obtain x where x: "x \<in> A" by blast
-  have "c dvd c * x" by simp
-  also from x have "c * x dvd Lcm (op * c ` A)" by (intro dvd_Lcm) auto
+  from assms obtain x where x: "x \<in> A"
+    by blast
+  have "c dvd c * x"
+    by simp
+  also from x have "c * x dvd Lcm (op * c ` A)"
+    by (intro dvd_Lcm) auto
   finally have dvd: "c dvd Lcm (op * c ` A)" .
 
   have "Lcm A dvd Lcm (op * c ` A) div c"
     by (intro Lcm_least dvd_mult_imp_div)
-       (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
-  hence "c * Lcm A dvd Lcm (op * c ` A)"
+      (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
+  then have "c * Lcm A dvd Lcm (op * c ` A)"
     by (subst (asm) dvd_div_iff_mult) (auto intro!: Lcm_least simp: mult_ac dvd)
   also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
@@ -1261,67 +1311,76 @@
     by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
   ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm (op * c ` A))"
     by (rule associatedI)
-  thus ?thesis by (simp add: normalize_mult)
-qed
-
-
-lemma Lcm_no_units:
-  "Lcm A = Lcm (A - {a. is_unit a})"
-proof -
-  have "(A - {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A" by blast
-  hence "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
-    by (simp add: Lcm_Un [symmetric])
-  also have "Lcm {a\<in>A. is_unit a} = 1" by (simp add: Lcm_1_iff)
-  finally show ?thesis by simp
+  then show ?thesis
+    by (simp add: normalize_mult)
 qed
 
-lemma Lcm_0_iff': "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
+lemma Lcm_no_units: "Lcm A = Lcm (A - {a. is_unit a})"
+proof -
+  have "(A - {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A"
+    by blast
+  then have "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
+    by (simp add: Lcm_Un [symmetric])
+  also have "Lcm {a\<in>A. is_unit a} = 1"
+    by simp
+  finally show ?thesis
+    by simp
+qed
+
+lemma Lcm_0_iff': "Lcm A = 0 \<longleftrightarrow> (\<nexists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
   by (metis Lcm_least dvd_0_left dvd_Lcm)
 
-lemma Lcm_no_multiple: "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)) \<Longrightarrow> Lcm A = 0"
+lemma Lcm_no_multiple: "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not> a dvd m)) \<Longrightarrow> Lcm A = 0"
   by (auto simp: Lcm_0_iff')
 
-lemma Lcm_singleton [simp]:
-  "Lcm {a} = normalize a"
+lemma Lcm_singleton [simp]: "Lcm {a} = normalize a"
   by simp
 
-lemma Lcm_2 [simp]:
-  "Lcm {a,b} = lcm a b"
+lemma Lcm_2 [simp]: "Lcm {a, b} = lcm a b"
   by simp
 
 lemma Lcm_coprime:
-  assumes "finite A" and "A \<noteq> {}" 
-  assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
+  assumes "finite A"
+    and "A \<noteq> {}"
+    and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
   shows "Lcm A = normalize (\<Prod>A)"
-using assms proof (induct rule: finite_ne_induct)
+  using assms
+proof (induct rule: finite_ne_induct)
+  case singleton
+  then show ?case by simp
+next
   case (insert a A)
-  have "Lcm (insert a A) = lcm a (Lcm A)" by simp
-  also from insert have "Lcm A = normalize (\<Prod>A)" by blast
-  also have "lcm a \<dots> = lcm a (\<Prod>A)" by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
-  also from insert have "gcd a (\<Prod>A) = 1" by (subst gcd.commute, intro setprod_coprime) auto
+  have "Lcm (insert a A) = lcm a (Lcm A)"
+    by simp
+  also from insert have "Lcm A = normalize (\<Prod>A)"
+    by blast
+  also have "lcm a \<dots> = lcm a (\<Prod>A)"
+    by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
+  also from insert have "gcd a (\<Prod>A) = 1"
+    by (subst gcd.commute, intro setprod_coprime) auto
   with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
     by (simp add: lcm_coprime)
   finally show ?case .
-qed simp
-      
+qed
+
 lemma Lcm_coprime':
-  "card A \<noteq> 0 \<Longrightarrow> (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1)
-    \<Longrightarrow> Lcm A = normalize (\<Prod>A)"
+  "card A \<noteq> 0 \<Longrightarrow>
+    (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1) \<Longrightarrow>
+    Lcm A = normalize (\<Prod>A)"
   by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
 
-lemma Gcd_1:
-  "1 \<in> A \<Longrightarrow> Gcd A = 1"
+lemma Gcd_1: "1 \<in> A \<Longrightarrow> Gcd A = 1"
   by (auto intro!: Gcd_eq_1_I)
 
 lemma Gcd_singleton [simp]: "Gcd {a} = normalize a"
   by simp
 
-lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b"
+lemma Gcd_2 [simp]: "Gcd {a, b} = gcd a b"
   by simp
 
 
-definition pairwise_coprime where
-  "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
+definition pairwise_coprime
+  where "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
 
 lemma pairwise_coprimeI [intro?]:
   "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
@@ -1336,20 +1395,19 @@
 
 end
 
+
 subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
 
 instantiation nat :: gcd
 begin
 
 fun gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where "gcd_nat x y =
-  (if y = 0 then x else gcd y (x mod y))"
+  where "gcd_nat x y = (if y = 0 then x else gcd y (x mod y))"
 
 definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
-  "lcm_nat x y = x * y div (gcd x y)"
-
-instance proof qed
+  where "lcm_nat x y = x * y div (gcd x y)"
+
+instance ..
 
 end
 
@@ -1369,31 +1427,32 @@
 text \<open>Transfer setup\<close>
 
 lemma transfer_nat_int_gcd:
-  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
-  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
-  unfolding gcd_int_def lcm_int_def
-  by auto
+  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
+  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
+  for x y :: int
+  unfolding gcd_int_def lcm_int_def by auto
 
 lemma transfer_nat_int_gcd_closures:
-  "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
-  "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
+  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd x y \<ge> 0"
+  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm x y \<ge> 0"
+  for x y :: int
   by (auto simp add: gcd_int_def lcm_int_def)
 
-declare transfer_morphism_nat_int[transfer add return:
-    transfer_nat_int_gcd transfer_nat_int_gcd_closures]
+declare transfer_morphism_nat_int
+  [transfer add return: transfer_nat_int_gcd transfer_nat_int_gcd_closures]
 
 lemma transfer_int_nat_gcd:
   "gcd (int x) (int y) = int (gcd x y)"
   "lcm (int x) (int y) = int (lcm x y)"
-  by (unfold gcd_int_def lcm_int_def, auto)
+  by (auto simp: gcd_int_def lcm_int_def)
 
 lemma transfer_int_nat_gcd_closures:
   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
-  by (auto simp add: gcd_int_def lcm_int_def)
-
-declare transfer_morphism_int_nat[transfer add return:
-    transfer_int_nat_gcd transfer_int_nat_gcd_closures]
+  by (auto simp: gcd_int_def lcm_int_def)
+
+declare transfer_morphism_int_nat
+  [transfer add return: transfer_int_nat_gcd transfer_int_nat_gcd_closures]
 
 lemma gcd_nat_induct:
   fixes m n :: nat
@@ -1402,119 +1461,145 @@
   shows "P m n"
   apply (rule gcd_nat.induct)
   apply (case_tac "y = 0")
-  using assms apply simp_all
-done
-
-(* specific to int *)
-
-lemma gcd_eq_int_iff:
-  "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
+  using assms
+   apply simp_all
+  done
+
+
+text \<open>Specific to \<open>int\<close>.\<close>
+
+lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
   by (simp add: gcd_int_def)
 
-lemma lcm_eq_int_iff:
-  "lcm k l = int n \<longleftrightarrow> lcm (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
+lemma lcm_eq_int_iff: "lcm k l = int n \<longleftrightarrow> lcm (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
   by (simp add: lcm_int_def)
 
-lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
+lemma gcd_neg1_int [simp]: "gcd (- x) y = gcd x y"
+  for x y :: int
   by (simp add: gcd_int_def)
 
-lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
+lemma gcd_neg2_int [simp]: "gcd x (- y) = gcd x y"
+  for x y :: int
+  by (simp add: gcd_int_def)
+
+lemma abs_gcd_int [simp]: "\<bar>gcd x y\<bar> = gcd x y"
+  for x y :: int
   by (simp add: gcd_int_def)
 
-lemma abs_gcd_int [simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
-by(simp add: gcd_int_def)
-
-lemma gcd_abs_int: "gcd (x::int) y = gcd \<bar>x\<bar> \<bar>y\<bar>"
-by (simp add: gcd_int_def)
-
-lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
-by (metis abs_idempotent gcd_abs_int)
-
-lemma gcd_abs2_int [simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
-by (metis abs_idempotent gcd_abs_int)
+lemma gcd_abs_int: "gcd x y = gcd \<bar>x\<bar> \<bar>y\<bar>"
+  for x y :: int
+  by (simp add: gcd_int_def)
+
+lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> y = gcd x y"
+  for x y :: int
+  by (metis abs_idempotent gcd_abs_int)
+
+lemma gcd_abs2_int [simp]: "gcd x \<bar>y\<bar> = gcd x y"
+  for x y :: int
+  by (metis abs_idempotent gcd_abs_int)
 
 lemma gcd_cases_int:
-  fixes x :: int and y
-  assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
-      and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
-      and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
-      and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
+  fixes x y :: int
+  assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd x y)"
+    and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd x (- y))"
+    and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd (- x) y)"
+    and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd (- x) (- y))"
   shows "P (gcd x y)"
-  by (insert assms, auto, arith)
+  using assms by auto arith
 
 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
+  for x y :: int
   by (simp add: gcd_int_def)
 
-lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
+lemma lcm_neg1_int: "lcm (- x) y = lcm x y"
+  for x y :: int
   by (simp add: lcm_int_def)
 
-lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
+lemma lcm_neg2_int: "lcm x (- y) = lcm x y"
+  for x y :: int
   by (simp add: lcm_int_def)
 
-lemma lcm_abs_int: "lcm (x::int) y = lcm \<bar>x\<bar> \<bar>y\<bar>"
+lemma lcm_abs_int: "lcm x y = lcm \<bar>x\<bar> \<bar>y\<bar>"
+  for x y :: int
   by (simp add: lcm_int_def)
 
-lemma abs_lcm_int [simp]: "\<bar>lcm i j::int\<bar> = lcm i j"
+lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
+  for i j :: int
   by (simp add:lcm_int_def)
 
-lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
+lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> y = lcm x y"
+  for x y :: int
   by (metis abs_idempotent lcm_int_def)
 
-lemma lcm_abs2_int [simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
+lemma lcm_abs2_int [simp]: "lcm x \<bar>y\<bar> = lcm x y"
+  for x y :: int
   by (metis abs_idempotent lcm_int_def)
 
 lemma lcm_cases_int:
-  fixes x :: int and y
-  assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
-      and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
-      and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
-      and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
+  fixes x y :: int
+  assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm x y)"
+    and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm x (- y))"
+    and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm (- x) y)"
+    and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm (- x) (- y))"
   shows "P (lcm x y)"
   using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
 
-lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
+lemma lcm_ge_0_int [simp]: "lcm x y \<ge> 0"
+  for x y :: int
   by (simp add: lcm_int_def)
 
-lemma gcd_0_nat: "gcd (x::nat) 0 = x"
+lemma gcd_0_nat: "gcd x 0 = x"
+  for x :: nat
   by simp
 
-lemma gcd_0_int [simp]: "gcd (x::int) 0 = \<bar>x\<bar>"
-  by (unfold gcd_int_def, auto)
-
-lemma gcd_0_left_nat: "gcd 0 (x::nat) = x"
+lemma gcd_0_int [simp]: "gcd x 0 = \<bar>x\<bar>"
+  for x :: int
+  by (auto simp: gcd_int_def)
+
+lemma gcd_0_left_nat: "gcd 0 x = x"
+  for x :: nat
   by simp
 
-lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = \<bar>x\<bar>"
-  by (unfold gcd_int_def, auto)
-
-lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
-  by (case_tac "y = 0", auto)
-
-(* weaker, but useful for the simplifier *)
-
-lemma gcd_non_0_nat: "y \<noteq> (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
-  by simp
-
-lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
+lemma gcd_0_left_int [simp]: "gcd 0 x = \<bar>x\<bar>"
+  for x :: int
+  by (auto simp:gcd_int_def)
+
+lemma gcd_red_nat: "gcd x y = gcd y (x mod y)"
+  for x y :: nat
+  by (cases "y = 0") auto
+
+
+text \<open>Weaker, but useful for the simplifier.\<close>
+
+lemma gcd_non_0_nat: "y \<noteq> 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
+  for x y :: nat
   by simp
 
-lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
+lemma gcd_1_nat [simp]: "gcd m 1 = 1"
+  for m :: nat
   by simp
 
-lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
+lemma gcd_Suc_0 [simp]: "gcd m (Suc 0) = Suc 0"
+  for m :: nat
+  by simp
+
+lemma gcd_1_int [simp]: "gcd m 1 = 1"
+  for m :: int
   by (simp add: gcd_int_def)
 
-lemma gcd_idem_nat: "gcd (x::nat) x = x"
-by simp
-
-lemma gcd_idem_int: "gcd (x::int) x = \<bar>x\<bar>"
-by (auto simp add: gcd_int_def)
+lemma gcd_idem_nat: "gcd x x = x"
+  for x :: nat
+  by simp
+
+lemma gcd_idem_int: "gcd x x = \<bar>x\<bar>"
+  for x :: int
+  by (auto simp add: gcd_int_def)
 
 declare gcd_nat.simps [simp del]
 
 text \<open>
-  \medskip @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>.  The
-  conjunctions don't seem provable separately.
+  \<^medskip> @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>.
+  The conjunctions don't seem provable separately.
 \<close>
 
 instance nat :: semiring_gcd
@@ -1523,7 +1608,8 @@
   show "gcd m n dvd m" and "gcd m n dvd n"
   proof (induct m n rule: gcd_nat_induct)
     fix m n :: nat
-    assume "gcd n (m mod n) dvd m mod n" and "gcd n (m mod n) dvd n"
+    assume "gcd n (m mod n) dvd m mod n"
+      and "gcd n (m mod n) dvd n"
     then have "gcd n (m mod n) dvd m"
       by (rule dvd_mod_imp_dvd)
     moreover assume "0 < n"
@@ -1539,71 +1625,82 @@
 
 instance int :: ring_gcd
   by standard
-    (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def lcm_int_def zdiv_int nat_abs_mult_distrib [symmetric] lcm_gcd gcd_greatest)
-
-lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
-  by (rule dvd_imp_le, auto)
-
-lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
-  by (rule dvd_imp_le, auto)
-
-lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
-  by (rule zdvd_imp_le, auto)
-
-lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
-  by (rule zdvd_imp_le, auto)
-
-lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
-  by (insert gcd_eq_0_iff [of m n], arith)
-
-lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
-  by (insert gcd_eq_0_iff [of m n], insert gcd_ge_0_int [of m n], arith)
-
-lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
-    (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
+    (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def lcm_int_def
+      zdiv_int nat_abs_mult_distrib [symmetric] lcm_gcd gcd_greatest)
+
+lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd a b \<le> a"
+  for a b :: nat
+  by (rule dvd_imp_le) auto
+
+lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd a b \<le> b"
+  for a b :: nat
+  by (rule dvd_imp_le) auto
+
+lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd a b \<le> a"
+  for a b :: int
+  by (rule zdvd_imp_le) auto
+
+lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd a b \<le> b"
+  for a b :: int
+  by (rule zdvd_imp_le) auto
+
+lemma gcd_pos_nat [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0"
+  for m n :: nat
+  using gcd_eq_0_iff [of m n] by arith
+
+lemma gcd_pos_int [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0"
+  for m n :: int
+  using gcd_eq_0_iff [of m n] gcd_ge_0_int [of m n] by arith
+
+lemma gcd_unique_nat: "d dvd a \<and> d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
+  for d a :: nat
   apply auto
   apply (rule dvd_antisym)
-  apply (erule (1) gcd_greatest)
+   apply (erule (1) gcd_greatest)
   apply auto
-done
-
-lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
-    (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
-apply (case_tac "d = 0")
- apply simp
-apply (rule iffI)
- apply (rule zdvd_antisym_nonneg)
- apply (auto intro: gcd_greatest)
-done
+  done
+
+lemma gcd_unique_int:
+  "d \<ge> 0 \<and> d dvd a \<and> d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
+  for d a :: int
+  apply (cases "d = 0")
+   apply simp
+  apply (rule iffI)
+   apply (rule zdvd_antisym_nonneg)
+      apply (auto intro: gcd_greatest)
+  done
 
 interpretation gcd_nat:
   semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n"
   by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
 
-lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = \<bar>x\<bar>"
+lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd x y = \<bar>x\<bar>"
+  for x y :: int
   by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
 
-lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = \<bar>y\<bar>"
+lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd x y = \<bar>y\<bar>"
+  for x y :: int
   by (metis gcd_proj1_if_dvd_int gcd.commute)
 
-text \<open>
-  \medskip Multiplication laws
-\<close>
-
-lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
-    \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
+
+text \<open>\<^medskip> Multiplication laws.\<close>
+
+lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)"
+  for k m n :: nat
+  \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
   apply (induct m n rule: gcd_nat_induct)
-  apply simp
-  apply (case_tac "k = 0")
-  apply (simp_all add: gcd_non_0_nat)
-done
-
-lemma gcd_mult_distrib_int: "\<bar>k::int\<bar> * gcd m n = gcd (k * m) (k * n)"
+   apply simp
+  apply (cases "k = 0")
+   apply (simp_all add: gcd_non_0_nat)
+  done
+
+lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
+  for k m n :: int
   apply (subst (1 2) gcd_abs_int)
   apply (subst (1 2) abs_mult)
   apply (rule gcd_mult_distrib_nat [transferred])
-  apply auto
-done
+    apply auto
+  done
 
 lemma coprime_crossproduct_nat:
   fixes a b c d :: nat
@@ -1617,51 +1714,54 @@
   shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>"
   using assms coprime_crossproduct [of a d b c] by simp
 
-text \<open>\medskip Addition laws\<close>
-
-(* to do: add the other variations? *)
-
-lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
+
+text \<open>\medskip Addition laws.\<close>
+
+(* TODO: add the other variations? *)
+
+lemma gcd_diff1_nat: "m \<ge> n \<Longrightarrow> gcd (m - n) n = gcd m n"
+  for m n :: nat
   by (subst gcd_add1 [symmetric]) auto
 
-lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
+lemma gcd_diff2_nat: "n \<ge> m \<Longrightarrow> gcd (n - m) n = gcd m n"
+  for m n :: nat
   apply (subst gcd.commute)
   apply (subst gcd_diff1_nat [symmetric])
-  apply auto
+   apply auto
   apply (subst gcd.commute)
   apply (subst gcd_diff1_nat)
-  apply assumption
+   apply assumption
   apply (rule gcd.commute)
   done
 
-lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
+lemma gcd_non_0_int: "y > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
+  for x y :: int
   apply (frule_tac b = y and a = x in pos_mod_sign)
   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
-  apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
-    zmod_zminus1_eq_if)
+  apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
   apply (frule_tac a = x in pos_mod_bound)
   apply (subst (1 2) gcd.commute)
-  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
-    nat_le_eq_zle)
+  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
   done
 
-lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
-  apply (case_tac "y = 0")
-  apply force
-  apply (case_tac "y > 0")
-  apply (subst gcd_non_0_int, auto)
-  apply (insert gcd_non_0_int [of "-y" "-x"])
+lemma gcd_red_int: "gcd x y = gcd y (x mod y)"
+  for x y :: int
+  apply (cases "y = 0")
+   apply force
+  apply (cases "y > 0")
+   apply (subst gcd_non_0_int, auto)
+  apply (insert gcd_non_0_int [of "- y" "- x"])
   apply auto
-done
-
-(* to do: differences, and all variations of addition rules
+  done
+
+(* TODO: differences, and all variations of addition rules
     as simplification rules for nat and int *)
 
-(* to do: add the three variations of these, and for ints? *)
-
-lemma finite_divisors_nat [simp]: \<comment> \<open>FIXME move\<close>
+(* TODO: add the three variations of these, and for ints? *)
+
+lemma finite_divisors_nat [simp]: (* FIXME move *)
   fixes m :: nat
-  assumes "m > 0" 
+  assumes "m > 0"
   shows "finite {d. d dvd m}"
 proof-
   from assms have "{d. d dvd m} \<subseteq> {d. d \<le> m}"
@@ -1677,140 +1777,143 @@
 proof -
   have "{d. \<bar>d\<bar> \<le> \<bar>i\<bar>} = {- \<bar>i\<bar>..\<bar>i\<bar>}"
     by (auto simp: abs_if)
-  then have "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}"
+  then have "finite {d. \<bar>d\<bar> \<le> \<bar>i\<bar>}"
     by simp
-  from finite_subset [OF _ this] show ?thesis using assms
-    by (simp add: dvd_imp_le_int subset_iff)
+  from finite_subset [OF _ this] show ?thesis
+    using assms by (simp add: dvd_imp_le_int subset_iff)
 qed
 
-lemma Max_divisors_self_nat [simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
-apply(rule antisym)
- apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
-apply simp
-done
-
-lemma Max_divisors_self_int [simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
-apply(rule antisym)
- apply(rule Max_le_iff [THEN iffD2])
-  apply (auto intro: abs_le_D1 dvd_imp_le_int)
-done
-
-lemma gcd_is_Max_divisors_nat:
-  "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> gcd (m::nat) n = Max {d. d dvd m \<and> d dvd n}"
-apply(rule Max_eqI[THEN sym])
-  apply (metis finite_Collect_conjI finite_divisors_nat)
- apply simp
- apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat)
-apply simp
-done
-
-lemma gcd_is_Max_divisors_int:
-  "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
-apply(rule Max_eqI[THEN sym])
-  apply (metis finite_Collect_conjI finite_divisors_int)
- apply simp
- apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le)
-apply simp
-done
-
-lemma gcd_code_int [code]:
-  "gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
+lemma Max_divisors_self_nat [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::nat. d dvd n} = n"
+  apply (rule antisym)
+   apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
+  apply simp
+  done
+
+lemma Max_divisors_self_int [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::int. d dvd n} = \<bar>n\<bar>"
+  apply (rule antisym)
+   apply (rule Max_le_iff [THEN iffD2])
+     apply (auto intro: abs_le_D1 dvd_imp_le_int)
+  done
+
+lemma gcd_is_Max_divisors_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> gcd m n = Max {d. d dvd m \<and> d dvd n}"
+  for m n :: nat
+  apply (rule Max_eqI[THEN sym])
+    apply (metis finite_Collect_conjI finite_divisors_nat)
+   apply simp
+   apply (metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat)
+  apply simp
+  done
+
+lemma gcd_is_Max_divisors_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> gcd m n = Max {d. d dvd m \<and> d dvd n}"
+  for m n :: int
+  apply (rule Max_eqI[THEN sym])
+    apply (metis finite_Collect_conjI finite_divisors_int)
+   apply simp
+   apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le)
+  apply simp
+  done
+
+lemma gcd_code_int [code]: "gcd k l = \<bar>if l = 0 then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
+  for k l :: int
   by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
 
 
 subsection \<open>Coprimality\<close>
 
-lemma coprime_nat:
-  "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
+lemma coprime_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
+  for a b :: nat
   using coprime [of a b] by simp
 
-lemma coprime_Suc_0_nat:
-  "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
+lemma coprime_Suc_0_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
+  for a b :: nat
   using coprime_nat by simp
 
-lemma coprime_int:
-  "coprime (a::int) b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
+lemma coprime_int: "coprime a b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
+  for a b :: int
   using gcd_unique_int [of 1 a b]
   apply clarsimp
   apply (erule subst)
   apply (rule iffI)
-  apply force
+   apply force
   using abs_dvd_iff abs_ge_zero apply blast
   done
 
-lemma pow_divides_eq_nat [simp]:
-  "n > 0 \<Longrightarrow> (a::nat) ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
+lemma pow_divides_eq_nat [simp]: "n > 0 \<Longrightarrow> a^n dvd b^n \<longleftrightarrow> a dvd b"
+  for a b n :: nat
   using pow_divs_eq[of n] by simp
 
 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
   using coprime_plus_one[of n] by simp
 
-lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
+lemma coprime_minus_one_nat: "n \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
+  for n :: nat
   using coprime_Suc_nat [of "n - 1"] gcd.commute [of "n - 1" n] by auto
 
-lemma coprime_common_divisor_nat: 
-  "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
+lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
+  for a b :: nat
   by (metis gcd_greatest_iff nat_dvd_1_iff_1)
 
-lemma coprime_common_divisor_int:
-  "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
+lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
+  for a b :: int
   using gcd_greatest_iff [of x a b] by auto
 
-lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
-by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat)
-
-lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
-by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int)
+lemma invertible_coprime_nat: "x * y mod m = 1 \<Longrightarrow> coprime x m"
+  for m x y :: nat
+  by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat)
+
+lemma invertible_coprime_int: "x * y mod m = 1 \<Longrightarrow> coprime x m"
+  for m x y :: int
+  by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int)
 
 
 subsection \<open>Bezout's theorem\<close>
 
-(* Function bezw returns a pair of witnesses to Bezout's theorem --
-   see the theorems that follow the definition. *)
-fun
-  bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
-where
-  "bezw x y =
-  (if y = 0 then (1, 0) else
+text \<open>
+  Function \<open>bezw\<close> returns a pair of witnesses to Bezout's theorem --
+  see the theorems that follow the definition.
+\<close>
+
+fun bezw :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
+  where "bezw x y =
+    (if y = 0 then (1, 0)
+     else
       (snd (bezw y (x mod y)),
        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
 
-lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
-
-lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
-       fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
+lemma bezw_0 [simp]: "bezw x 0 = (1, 0)"
+  by simp
+
+lemma bezw_non_0:
+  "y > 0 \<Longrightarrow> bezw x y =
+    (snd (bezw y (x mod y)), fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
   by simp
 
 declare bezw.simps [simp del]
 
-lemma bezw_aux [rule_format]:
-    "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
+lemma bezw_aux: "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
 proof (induct x y rule: gcd_nat_induct)
   fix m :: nat
   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
     by auto
-  next fix m :: nat and n
-    assume ngt0: "n > 0" and
-      ih: "fst (bezw n (m mod n)) * int n +
-        snd (bezw n (m mod n)) * int (m mod n) =
-        int (gcd n (m mod n))"
-    thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
-      apply (simp add: bezw_non_0 gcd_non_0_nat)
-      apply (erule subst)
-      apply (simp add: field_simps)
-      apply (subst mod_div_equality [of m n, symmetric])
-      (* applying simp here undoes the last substitution!
-         what is procedure cancel_div_mod? *)
-      apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
-      done
+next
+  fix m n :: nat
+  assume ngt0: "n > 0"
+    and ih: "fst (bezw n (m mod n)) * int n + snd (bezw n (m mod n)) * int (m mod n) =
+      int (gcd n (m mod n))"
+  then show "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
+    apply (simp add: bezw_non_0 gcd_non_0_nat)
+    apply (erule subst)
+    apply (simp add: field_simps)
+    apply (subst mod_div_equality [of m n, symmetric])
+      (* applying simp here undoes the last substitution! what is procedure cancel_div_mod? *)
+    apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
+    done
 qed
 
-lemma bezout_int:
-  fixes x y
-  shows "EX u v. u * (x::int) + v * y = gcd x y"
+lemma bezout_int: "\<exists>u v. u * x + v * y = gcd x y"
+  for x y :: int
 proof -
-  have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
-      EX u v. u * x + v * y = gcd x y"
+  have aux: "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> \<exists>u v. u * x + v * y = gcd x y" for x y :: int
     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
     apply (unfold gcd_int_def)
@@ -1818,77 +1921,96 @@
     apply (subst bezw_aux [symmetric])
     apply auto
     done
-  have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
-      (x \<le> 0 \<and> y \<le> 0)"
-    by auto
-  moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
-    by (erule (1) bezout_aux)
-  moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
-    apply (insert bezout_aux [of x "-y"])
-    apply auto
-    apply (rule_tac x = u in exI)
-    apply (rule_tac x = "-v" in exI)
-    apply (subst gcd_neg2_int [symmetric])
-    apply auto
-    done
-  moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
-    apply (insert bezout_aux [of "-x" y])
-    apply auto
-    apply (rule_tac x = "-u" in exI)
-    apply (rule_tac x = v in exI)
-    apply (subst gcd_neg1_int [symmetric])
-    apply auto
-    done
-  moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
-    apply (insert bezout_aux [of "-x" "-y"])
-    apply auto
-    apply (rule_tac x = "-u" in exI)
-    apply (rule_tac x = "-v" in exI)
-    apply (subst gcd_neg1_int [symmetric])
-    apply (subst gcd_neg2_int [symmetric])
-    apply auto
-    done
-  ultimately show ?thesis by blast
+  consider "x \<ge> 0" "y \<ge> 0" | "x \<ge> 0" "y \<le> 0" | "x \<le> 0" "y \<ge> 0" | "x \<le> 0" "y \<le> 0"
+    by atomize_elim auto
+  then show ?thesis
+  proof cases
+    case 1
+    then show ?thesis by (rule aux)
+  next
+    case 2
+    then show ?thesis
+      apply -
+      apply (insert aux [of x "-y"])
+      apply auto
+      apply (rule_tac x = u in exI)
+      apply (rule_tac x = "-v" in exI)
+      apply (subst gcd_neg2_int [symmetric])
+      apply auto
+      done
+  next
+    case 3
+    then show ?thesis
+      apply -
+      apply (insert aux [of "-x" y])
+      apply auto
+      apply (rule_tac x = "-u" in exI)
+      apply (rule_tac x = v in exI)
+      apply (subst gcd_neg1_int [symmetric])
+      apply auto
+      done
+  next
+    case 4
+    then show ?thesis
+      apply -
+      apply (insert aux [of "-x" "-y"])
+      apply auto
+      apply (rule_tac x = "-u" in exI)
+      apply (rule_tac x = "-v" in exI)
+      apply (subst gcd_neg1_int [symmetric])
+      apply (subst gcd_neg2_int [symmetric])
+      apply auto
+      done
+  qed
 qed
 
-text \<open>versions of Bezout for nat, by Amine Chaieb\<close>
+
+text \<open>Versions of Bezout for \<open>nat\<close>, by Amine Chaieb.\<close>
 
 lemma ind_euclid:
-  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
-  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
+  fixes P :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+  assumes c: " \<forall>a b. P a b \<longleftrightarrow> P b a"
+    and z: "\<forall>a. P a 0"
+    and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
   shows "P a b"
-proof(induct "a + b" arbitrary: a b rule: less_induct)
+proof (induct "a + b" arbitrary: a b rule: less_induct)
   case less
-  have "a = b \<or> a < b \<or> b < a" by arith
-  moreover {assume eq: "a= b"
-    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
-    by simp}
-  moreover
-  {assume lt: "a < b"
-    hence "a + b - a < a + b \<or> a = 0" by arith
-    moreover
-    {assume "a =0" with z c have "P a b" by blast }
-    moreover
-    {assume "a + b - a < a + b"
-      also have th0: "a + b - a = a + (b - a)" using lt by arith
+  consider (eq) "a = b" | (lt) "a < b" "a + b - a < a + b" | "b = 0" | "b + a - b < a + b"
+    by arith
+  show ?case
+  proof (cases a b rule: linorder_cases)
+    case equal
+    with add [rule_format, OF z [rule_format, of a]] show ?thesis by simp
+  next
+    case lt: less
+    then consider "a = 0" | "a + b - a < a + b" by arith
+    then show ?thesis
+    proof cases
+      case 1
+      with z c show ?thesis by blast
+    next
+      case 2
+      also have *: "a + b - a = a + (b - a)" using lt by arith
       finally have "a + (b - a) < a + b" .
-      then have "P a (a + (b - a))" by (rule add[rule_format, OF less])
-      then have "P a b" by (simp add: th0[symmetric])}
-    ultimately have "P a b" by blast}
-  moreover
-  {assume lt: "a > b"
-    hence "b + a - b < a + b \<or> b = 0" by arith
-    moreover
-    {assume "b =0" with z c have "P a b" by blast }
-    moreover
-    {assume "b + a - b < a + b"
-      also have th0: "b + a - b = b + (a - b)" using lt by arith
+      then have "P a (a + (b - a))" by (rule add [rule_format, OF less])
+      then show ?thesis by (simp add: *[symmetric])
+    qed
+  next
+    case gt: greater
+    then consider "b = 0" | "b + a - b < a + b" by arith
+    then show ?thesis
+    proof cases
+      case 1
+      with z c show ?thesis by blast
+    next
+      case 2
+      also have *: "b + a - b = b + (a - b)" using gt by arith
       finally have "b + (a - b) < a + b" .
-      then have "P b (b + (a - b))" by (rule add[rule_format, OF less])
-      then have "P b a" by (simp add: th0[symmetric])
-      hence "P a b" using c by blast }
-    ultimately have "P a b" by blast}
-ultimately  show "P a b" by blast
+      then have "P b (b + (a - b))" by (rule add [rule_format, OF less])
+      then have "P b a" by (simp add: *[symmetric])
+      with c show ?thesis by blast
+    qed
+  qed
 qed
 
 lemma bezout_lemma_nat:
@@ -1898,196 +2020,238 @@
     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
   using ex
   apply clarsimp
-  apply (rule_tac x="d" in exI, simp)
-  apply (case_tac "a * x = b * y + d" , simp_all)
-  apply (rule_tac x="x + y" in exI)
-  apply (rule_tac x="y" in exI)
-  apply algebra
+  apply (rule_tac x="d" in exI)
+  apply simp
+  apply (case_tac "a * x = b * y + d")
+   apply simp_all
+   apply (rule_tac x="x + y" in exI)
+   apply (rule_tac x="y" in exI)
+   apply algebra
   apply (rule_tac x="x" in exI)
   apply (rule_tac x="x + y" in exI)
   apply algebra
-done
+  done
 
 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
     (a * x = b * y + d \<or> b * x = a * y + d)"
-  apply(induct a b rule: ind_euclid)
-  apply blast
-  apply clarify
-  apply (rule_tac x="a" in exI, simp)
+  apply (induct a b rule: ind_euclid)
+    apply blast
+   apply clarify
+   apply (rule_tac x="a" in exI)
+   apply simp
   apply clarsimp
   apply (rule_tac x="d" in exI)
-  apply (case_tac "a * x = b * y + d", simp_all)
-  apply (rule_tac x="x+y" in exI)
-  apply (rule_tac x="y" in exI)
-  apply algebra
+  apply (case_tac "a * x = b * y + d")
+   apply simp_all
+   apply (rule_tac x="x+y" in exI)
+   apply (rule_tac x="y" in exI)
+   apply algebra
   apply (rule_tac x="x" in exI)
   apply (rule_tac x="x+y" in exI)
   apply algebra
-done
+  done
 
 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
     (a * x - b * y = d \<or> b * x - a * y = d)"
   using bezout_add_nat[of a b]
   apply clarsimp
-  apply (rule_tac x="d" in exI, simp)
+  apply (rule_tac x="d" in exI)
+  apply simp
   apply (rule_tac x="x" in exI)
   apply (rule_tac x="y" in exI)
   apply auto
-done
-
-lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
+  done
+
+lemma bezout_add_strong_nat:
+  fixes a b :: nat
+  assumes a: "a \<noteq> 0"
   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
-proof-
- from nz have ap: "a > 0" by simp
- from bezout_add_nat[of a b]
- have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
-   (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
- moreover
-    {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
-     from H have ?thesis by blast }
- moreover
- {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
-   {assume b0: "b = 0" with H  have ?thesis by simp}
-   moreover
-   {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
-     from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
-       by auto
-     moreover
-     {assume db: "d=b"
-       with nz H have ?thesis apply simp
-         apply (rule exI[where x = b], simp)
-         apply (rule exI[where x = b])
-        by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
-    moreover
-    {assume db: "d < b"
-        {assume "x=0" hence ?thesis using nz H by simp }
-        moreover
-        {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
-          from db have "d \<le> b - 1" by simp
-          hence "d*b \<le> b*(b - 1)" by simp
-          with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
-          have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
-          from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
+proof -
+  consider d x y where "d dvd a" "d dvd b" "a * x = b * y + d"
+    | d x y where "d dvd a" "d dvd b" "b * x = a * y + d"
+    using bezout_add_nat [of a b] by blast
+  then show ?thesis
+  proof cases
+    case 1
+    then show ?thesis by blast
+  next
+    case H: 2
+    show ?thesis
+    proof (cases "b = 0")
+      case True
+      with H show ?thesis by simp
+    next
+      case False
+      then have bp: "b > 0" by simp
+      with dvd_imp_le [OF H(2)] consider "d = b" | "d < b"
+        by atomize_elim auto
+      then show ?thesis
+      proof cases
+        case 1
+        with a H show ?thesis
+          apply simp
+          apply (rule exI[where x = b])
+          apply simp
+          apply (rule exI[where x = b])
+          apply (rule exI[where x = "a - 1"])
+          apply (simp add: diff_mult_distrib2)
+          done
+      next
+        case 2
+        show ?thesis
+        proof (cases "x = 0")
+          case True
+          with a H show ?thesis by simp
+        next
+          case x0: False
+          then have xp: "x > 0" by simp
+          from \<open>d < b\<close> have "d \<le> b - 1" by simp
+          then have "d * b \<le> b * (b - 1)" by simp
+          with xp mult_mono[of "1" "x" "d * b" "b * (b - 1)"]
+          have dble: "d * b \<le> x * b * (b - 1)" using bp by simp
+          from H(3) have "d + (b - 1) * (b * x) = d + (b - 1) * (a * y + d)"
             by simp
-          hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
+          then have "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
             by (simp only: mult.assoc distrib_left)
-          hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
+          then have "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x * b * (b - 1)"
             by algebra
-          hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
-          hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
+          then have "a * ((b - 1) * y) = d + x * b * (b - 1) - d * b"
+            using bp by simp
+          then have "a * ((b - 1) * y) = d + (x * b * (b - 1) - d * b)"
             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
-          hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
+          then have "a * ((b - 1) * y) = b * (x * (b - 1) - d) + d"
             by (simp only: diff_mult_distrib2 ac_simps)
-          hence ?thesis using H(1,2)
+          with H(1,2) show ?thesis
             apply -
-            apply (rule exI[where x=d], simp)
-            apply (rule exI[where x="(b - 1) * y"])
-            by (rule exI[where x="x*(b - 1) - d"], simp)}
-        ultimately have ?thesis by blast}
-    ultimately have ?thesis by blast}
-  ultimately have ?thesis by blast}
- ultimately show ?thesis by blast
+            apply (rule exI [where x = d])
+            apply simp
+            apply (rule exI [where x = "(b - 1) * y"])
+            apply (rule exI [where x = "x * (b - 1) - d"])
+            apply simp
+            done
+        qed
+      qed
+    qed
+  qed
 qed
 
-lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
+lemma bezout_nat:
+  fixes a :: nat
+  assumes a: "a \<noteq> 0"
   shows "\<exists>x y. a * x = b * y + gcd a b"
-proof-
-  let ?g = "gcd a b"
-  from bezout_add_strong_nat[OF a, of b]
-  obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
-  from d(1,2) have "d dvd ?g" by simp
-  then obtain k where k: "?g = d*k" unfolding dvd_def by blast
-  from d(3) have "a * x * k = (b * y + d) *k " by auto
-  hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
-  thus ?thesis by blast
+proof -
+  obtain d x y where d: "d dvd a" "d dvd b" and eq: "a * x = b * y + d"
+    using bezout_add_strong_nat [OF a, of b] by blast
+  from d have "d dvd gcd a b"
+    by simp
+  then obtain k where k: "gcd a b = d * k"
+    unfolding dvd_def by blast
+  from eq have "a * x * k = (b * y + d) * k"
+    by auto
+  then have "a * (x * k) = b * (y * k) + gcd a b"
+    by (algebra add: k)
+  then show ?thesis
+    by blast
 qed
 
 
-subsection \<open>LCM properties  on @{typ nat} and @{typ int}\<close>
-
-lemma lcm_altdef_int [code]: "lcm (a::int) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
+subsection \<open>LCM properties on @{typ nat} and @{typ int}\<close>
+
+lemma lcm_altdef_int [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
+  for a b :: int
   by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
 
-lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
+lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
+  for m n :: nat
   unfolding lcm_nat_def
   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
 
-lemma prod_gcd_lcm_int: "\<bar>m::int\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
+lemma prod_gcd_lcm_int: "\<bar>m\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
+  for m n :: int
   unfolding lcm_int_def gcd_int_def
   apply (subst of_nat_mult [symmetric])
   apply (subst prod_gcd_lcm_nat [symmetric])
   apply (subst nat_abs_mult_distrib [symmetric])
-  apply (simp, simp add: abs_mult)
-done
-
-lemma lcm_pos_nat:
-  "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
-by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
-
-lemma lcm_pos_int:
-  "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
+  apply (simp add: abs_mult)
+  done
+
+lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
+  for m n :: nat
+  by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
+
+lemma lcm_pos_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lcm m n > 0"
+  for m n :: int
   apply (subst lcm_abs_int)
   apply (rule lcm_pos_nat [transferred])
-  apply auto
+     apply auto
   done
 
-lemma dvd_pos_nat: \<comment> \<open>FIXME move\<close>
-  fixes n m :: nat
-  assumes "n > 0" and "m dvd n"
-  shows "m > 0"
-  using assms by (cases m) auto
-
-lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
-    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
+lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0"  (* FIXME move *)
+  for m n :: nat
+  by (cases m) auto
+
+lemma lcm_unique_nat:
+  "a dvd d \<and> b dvd d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
+  for a b d :: nat
   by (auto intro: dvd_antisym lcm_least)
 
-lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
-    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
+lemma lcm_unique_int:
+  "d \<ge> 0 \<and> a dvd d \<and> b dvd d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
+  for a b d :: int
   using lcm_least zdvd_antisym_nonneg by auto
 
-lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
+lemma lcm_proj2_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm x y = y"
+  for x y :: nat
   apply (rule sym)
   apply (subst lcm_unique_nat [symmetric])
   apply auto
-done
-
-lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
+  done
+
+lemma lcm_proj2_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
+  for x y :: int
   apply (rule sym)
   apply (subst lcm_unique_int [symmetric])
   apply auto
-done
-
-lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
-by (subst lcm.commute, erule lcm_proj2_if_dvd_nat)
-
-lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
-by (subst lcm.commute, erule lcm_proj2_if_dvd_int)
-
-lemma lcm_proj1_iff_nat [simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
-by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
-
-lemma lcm_proj2_iff_nat [simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
-by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
-
-lemma lcm_proj1_iff_int [simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
-by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
-
-lemma lcm_proj2_iff_int [simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
-by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
-
-lemma lcm_1_iff_nat [simp]:
-  "lcm (m::nat) n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
+  done
+
+lemma lcm_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm y x = y"
+  for x y :: nat
+  by (subst lcm.commute) (erule lcm_proj2_if_dvd_nat)
+
+lemma lcm_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
+  for x y :: int
+  by (subst lcm.commute) (erule lcm_proj2_if_dvd_int)
+
+lemma lcm_proj1_iff_nat [simp]: "lcm m n = m \<longleftrightarrow> n dvd m"
+  for m n :: nat
+  by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
+
+lemma lcm_proj2_iff_nat [simp]: "lcm m n = n \<longleftrightarrow> m dvd n"
+  for m n :: nat
+  by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
+
+lemma lcm_proj1_iff_int [simp]: "lcm m n = \<bar>m\<bar> \<longleftrightarrow> n dvd m"
+  for m n :: int
+  by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
+
+lemma lcm_proj2_iff_int [simp]: "lcm m n = \<bar>n\<bar> \<longleftrightarrow> m dvd n"
+  for m n :: int
+  by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
+
+lemma lcm_1_iff_nat [simp]: "lcm m n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
+  for m n :: nat
   using lcm_eq_1_iff [of m n] by simp
-  
-lemma lcm_1_iff_int [simp]:
-  "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
+
+lemma lcm_1_iff_int [simp]: "lcm m n = 1 \<longleftrightarrow> (m = 1 \<or> m = -1) \<and> (n = 1 \<or> n = -1)"
+  for m n :: int
   by auto
 
 
 subsection \<open>The complete divisibility lattice on @{typ nat} and @{typ int}\<close>
 
-text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
-Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
+text \<open>
+  Lifting \<open>gcd\<close> and \<open>lcm\<close> to sets (\<open>Gcd\<close> / \<open>Lcm\<close>).
+  \<open>Gcd\<close> is defined via \<open>Lcm\<close> to facilitate the proof that we have a complete lattice.
 \<close>
 
 instantiation nat :: semiring_Gcd
@@ -2096,19 +2260,15 @@
 interpretation semilattice_neutr_set lcm "1::nat"
   by standard simp_all
 
-definition
-  "Lcm (M::nat set) = (if finite M then F M else 0)"
-
-lemma Lcm_nat_empty:
-  "Lcm {} = (1::nat)"
+definition "Lcm M = (if finite M then F M else 0)" for M :: "nat set"
+
+lemma Lcm_nat_empty: "Lcm {} = (1::nat)"
   by (simp add: Lcm_nat_def del: One_nat_def)
 
-lemma Lcm_nat_insert:
-  "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
+lemma Lcm_nat_insert: "Lcm (insert n M) = lcm n (Lcm M)" for n :: nat
   by (cases "finite M") (auto simp add: Lcm_nat_def simp del: One_nat_def)
 
-lemma Lcm_nat_infinite:
-  "infinite M \<Longrightarrow> Lcm M = (0::nat)"
+lemma Lcm_nat_infinite: "infinite M \<Longrightarrow> Lcm M = 0" for M :: "nat set"
   by (simp add: Lcm_nat_def)
 
 lemma dvd_Lcm_nat [simp]:
@@ -2116,10 +2276,12 @@
   assumes "m \<in> M"
   shows "m dvd Lcm M"
 proof -
-  from assms have "insert m M = M" by auto
+  from assms have "insert m M = M"
+    by auto
   moreover have "m dvd Lcm (insert m M)"
     by (simp add: Lcm_nat_insert)
-  ultimately show ?thesis by simp
+  ultimately show ?thesis
+    by simp
 qed
 
 lemma Lcm_dvd_nat [simp]:
@@ -2127,41 +2289,46 @@
   assumes "\<forall>m\<in>M. m dvd n"
   shows "Lcm M dvd n"
 proof (cases "n > 0")
-  case False then show ?thesis by simp
+  case False
+  then show ?thesis by simp
 next
   case True
-  then have "finite {d. d dvd n}" by (rule finite_divisors_nat)
-  moreover have "M \<subseteq> {d. d dvd n}" using assms by fast
-  ultimately have "finite M" by (rule rev_finite_subset)
-  then show ?thesis using assms
-    by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
+  then have "finite {d. d dvd n}"
+    by (rule finite_divisors_nat)
+  moreover have "M \<subseteq> {d. d dvd n}"
+    using assms by fast
+  ultimately have "finite M"
+    by (rule rev_finite_subset)
+  then show ?thesis
+    using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
 qed
 
-definition
-  "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
-
-instance proof
-  show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
-  using that by (induct N rule: infinite_finite_induct)
-    (auto simp add: Gcd_nat_def)
-  show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m" for N and n :: nat
-  using that by (induct N rule: infinite_finite_induct)
-    (auto simp add: Gcd_nat_def)
-  show "n dvd Lcm N" if "n \<in> N" for N and n ::nat
-  using that by (induct N rule: infinite_finite_induct)
-    auto
-  show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n" for N and n ::nat
-  using that by (induct N rule: infinite_finite_induct)
-    auto
-qed simp_all
+definition "Gcd M = Lcm {d. \<forall>m\<in>M. d dvd m}" for M :: "nat set"
+
+instance
+proof
+  fix N :: "nat set"
+  fix n :: nat
+  show "Gcd N dvd n" if "n \<in> N"
+    using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
+  show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m"
+    using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
+  show "n dvd Lcm N" if "n \<in> N"
+    using that by (induct N rule: infinite_finite_induct) auto
+  show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n"
+    using that by (induct N rule: infinite_finite_induct) auto
+  show "normalize (Gcd N) = Gcd N" and "normalize (Lcm N) = Lcm N"
+    by simp_all
+qed
 
 end
 
-lemma Gcd_nat_eq_one:
-  "1 \<in> N \<Longrightarrow> Gcd N = (1::nat)"
+lemma Gcd_nat_eq_one: "1 \<in> N \<Longrightarrow> Gcd N = 1"
+  for N :: "nat set"
   by (rule Gcd_eq_1_I) auto
 
-text\<open>Alternative characterizations of Gcd:\<close>
+
+text \<open>Alternative characterizations of Gcd:\<close>
 
 lemma Gcd_eq_Max:
   fixes M :: "nat set"
@@ -2178,90 +2345,91 @@
     by (auto intro: Max_ge Gcd_dvd)
   from fin show "Max (\<Inter>m\<in>M. {d. d dvd m}) \<le> Gcd M"
     apply (rule Max.boundedI)
-    apply auto
+     apply auto
     apply (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
     done
 qed
 
-lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
-apply(induct pred:finite)
- apply simp
-apply(case_tac "x=0")
- apply simp
-apply(subgoal_tac "insert x F - {0} = insert x (F - {0})")
- apply simp
-apply blast
-done
+lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0})"
+  for M :: "nat set"
+  apply (induct pred: finite)
+   apply simp
+  apply (case_tac "x = 0")
+   apply simp
+  apply (subgoal_tac "insert x F - {0} = insert x (F - {0})")
+   apply simp
+  apply blast
+  done
 
 lemma Lcm_in_lcm_closed_set_nat:
-  "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M : M"
-apply(induct rule:finite_linorder_min_induct)
- apply simp
-apply simp
-apply(subgoal_tac "ALL m n :: nat. m:A \<longrightarrow> n:A \<longrightarrow> lcm m n : A")
- apply simp
- apply(case_tac "A={}")
+  "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> \<forall>m n. m \<in> M \<longrightarrow> n \<in> M \<longrightarrow> lcm m n \<in> M \<Longrightarrow> Lcm M \<in> M"
+  for M :: "nat set"
+  apply (induct rule: finite_linorder_min_induct)
+   apply simp
   apply simp
- apply simp
-apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
-done
+  apply (subgoal_tac "\<forall>m n. m \<in> A \<longrightarrow> n \<in> A \<longrightarrow> lcm m n \<in> A")
+   apply simp
+   apply(case_tac "A = {}")
+    apply simp
+   apply simp
+  apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
+  done
 
 lemma Lcm_eq_Max_nat:
-  "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M = Max M"
-apply(rule antisym)
- apply(rule Max_ge, assumption)
- apply(erule (2) Lcm_in_lcm_closed_set_nat)
-apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
-done
+  "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> \<forall>m n. m \<in> M \<longrightarrow> n \<in> M \<longrightarrow> lcm m n \<in> M \<Longrightarrow> Lcm M = Max M"
+  for M :: "nat set"
+  apply (rule antisym)
+   apply (rule Max_ge)
+    apply assumption
+   apply (erule (2) Lcm_in_lcm_closed_set_nat)
+  apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
+  done
 
 lemma mult_inj_if_coprime_nat:
-  "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
-   \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
+  "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> \<forall>a\<in>A. \<forall>b\<in>B. coprime (f a) (g b) \<Longrightarrow>
+    inj_on (\<lambda>(a, b). f a * g b) (A \<times> B)"
+  for f :: "'a \<Rightarrow> nat" and g :: "'b \<Rightarrow> nat"
   by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
 
-text\<open>Nitpick:\<close>
+
+text \<open>Nitpick:\<close>
 
 lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
-by (induct x y rule: nat_gcd.induct)
-   (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
+  by (induct x y rule: nat_gcd.induct)
+    (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
 
 lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
-by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
-
-
-subsubsection \<open>Setwise gcd and lcm for integers\<close>
+  by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
+
+
+subsubsection \<open>Setwise GCD and LCM for integers\<close>
 
 instantiation int :: semiring_Gcd
 begin
 
-definition
-  "Lcm M = int (LCM m\<in>M. (nat \<circ> abs) m)"
-
-definition
-  "Gcd M = int (GCD m\<in>M. (nat \<circ> abs) m)"
-
-instance by standard
-  (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
-    Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
+definition "Lcm M = int (LCM m\<in>M. (nat \<circ> abs) m)"
+
+definition "Gcd M = int (GCD m\<in>M. (nat \<circ> abs) m)"
+
+instance
+  by standard
+    (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
+      Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
 
 end
 
-lemma abs_Gcd [simp]:
-  fixes K :: "int set"
-  shows "\<bar>Gcd K\<bar> = Gcd K"
+lemma abs_Gcd [simp]: "\<bar>Gcd K\<bar> = Gcd K"
+  for K :: "int set"
   using normalize_Gcd [of K] by simp
 
-lemma abs_Lcm [simp]:
-  fixes K :: "int set"
-  shows "\<bar>Lcm K\<bar> = Lcm K"
+lemma abs_Lcm [simp]: "\<bar>Lcm K\<bar> = Lcm K"
+  for K :: "int set"
   using normalize_Lcm [of K] by simp
 
-lemma Gcm_eq_int_iff:
-  "Gcd K = int n \<longleftrightarrow> Gcd ((nat \<circ> abs) ` K) = n"
+lemma Gcm_eq_int_iff: "Gcd K = int n \<longleftrightarrow> Gcd ((nat \<circ> abs) ` K) = n"
   by (simp add: Gcd_int_def comp_def image_image)
 
-lemma Lcm_eq_int_iff:
-  "Lcm K = int n \<longleftrightarrow> Lcm ((nat \<circ> abs) ` K) = n"
+lemma Lcm_eq_int_iff: "Lcm K = int n \<longleftrightarrow> Lcm ((nat \<circ> abs) ` K) = n"
   by (simp add: Lcm_int_def comp_def image_image)
 
 
@@ -2274,12 +2442,12 @@
   includes integer.lifting
 begin
 
-lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
-  is gcd .
-lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
-  is lcm .
+lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is gcd .
+
+lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is lcm .
 
 end
+
 instance ..
 
 end
@@ -2291,17 +2459,18 @@
   includes integer.lifting
 begin
 
-lemma gcd_code_integer [code]:
-  "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
+lemma gcd_code_integer [code]: "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
   by transfer (fact gcd_code_int)
 
-lemma lcm_code_integer [code]: "lcm (a::integer) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
+lemma lcm_code_integer [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
+  for a b :: integer
   by transfer (fact lcm_altdef_int)
 
 end
 
-code_printing constant "gcd :: integer \<Rightarrow> _"
-  \<rightharpoonup> (OCaml) "Big'_int.gcd'_big'_int"
+code_printing
+  constant "gcd :: integer \<Rightarrow> _" \<rightharpoonup>
+    (OCaml) "Big'_int.gcd'_big'_int"
   and (Haskell) "Prelude.gcd"
   and (Scala) "_.gcd'((_)')"
   \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
@@ -2314,30 +2483,38 @@
 lemmas Gcd_set_int [code] = Gcd_set[where ?'a = int]
 
 
-text \<open>Fact aliasses\<close>
-
-lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
+text \<open>Fact aliases.\<close>
+
+lemma lcm_0_iff_nat [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
+  for m n :: nat
   by (fact lcm_eq_0_iff)
 
-lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
+lemma lcm_0_iff_int [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
+  for m n :: int
   by (fact lcm_eq_0_iff)
 
-lemma dvd_lcm_I1_nat [simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
+lemma dvd_lcm_I1_nat [simp]: "k dvd m \<Longrightarrow> k dvd lcm m n"
+  for k m n :: nat
   by (fact dvd_lcmI1)
 
-lemma dvd_lcm_I2_nat [simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
+lemma dvd_lcm_I2_nat [simp]: "k dvd n \<Longrightarrow> k dvd lcm m n"
+  for k m n :: nat
   by (fact dvd_lcmI2)
 
-lemma dvd_lcm_I1_int [simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
+lemma dvd_lcm_I1_int [simp]: "i dvd m \<Longrightarrow> i dvd lcm m n"
+  for i m n :: int
   by (fact dvd_lcmI1)
 
-lemma dvd_lcm_I2_int [simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
+lemma dvd_lcm_I2_int [simp]: "i dvd n \<Longrightarrow> i dvd lcm m n"
+  for i m n :: int
   by (fact dvd_lcmI2)
 
-lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
+lemma coprime_exp2_nat [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
+  for a b :: nat
   by (fact coprime_exp2)
 
-lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
+lemma coprime_exp2_int [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
+  for a b :: int
   by (fact coprime_exp2)
 
 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
@@ -2345,22 +2522,22 @@
 lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
 lemmas Gcd_greatest_int [simp] = Gcd_greatest [where ?'a = int]
 
-lemma dvd_Lcm_int [simp]:
-  fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
-  using assms by (fact dvd_Lcm)
-
-lemma gcd_neg_numeral_1_int [simp]:
-  "gcd (- numeral n :: int) x = gcd (numeral n) x"
+lemma dvd_Lcm_int [simp]: "m \<in> M \<Longrightarrow> m dvd Lcm M"
+  for M :: "int set"
+  by (fact dvd_Lcm)
+
+lemma gcd_neg_numeral_1_int [simp]: "gcd (- numeral n :: int) x = gcd (numeral n) x"
   by (fact gcd_neg1_int)
 
-lemma gcd_neg_numeral_2_int [simp]:
-  "gcd x (- numeral n :: int) = gcd x (numeral n)"
+lemma gcd_neg_numeral_2_int [simp]: "gcd x (- numeral n :: int) = gcd x (numeral n)"
   by (fact gcd_neg2_int)
 
-lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
+lemma gcd_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> gcd x y = x"
+  for x y :: nat
   by (fact gcd_nat.absorb1)
 
-lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
+lemma gcd_proj2_if_dvd_nat [simp]: "y dvd x \<Longrightarrow> gcd x y = y"
+  for x y :: nat
   by (fact gcd_nat.absorb2)
 
 lemmas Lcm_eq_0_I_nat [simp] = Lcm_eq_0_I [where ?'a = nat]