# HG changeset patch
# User wenzelm
# Date 1501618777 -7200
# Node ID 7454317f883cd73f15cd2a47bc6c81458e35ea8a
# Parent  cde6ceffcbc7a0517b4eb283bf64ebb59de0f90b
misc tuning and modernization;

diff -r cde6ceffcbc7 -r 7454317f883c src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Tue Aug 01 17:33:04 2017 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy	Tue Aug 01 22:19:37 2017 +0200
@@ -8,186 +8,223 @@
 imports Residues
 begin
 
-subsection\<open>Lemmas about previously defined terms\<close>
+subsection \<open>Lemmas about previously defined terms\<close>
 
-lemma prime_nat_iff'':
-  "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
+lemma prime_nat_iff'': "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
   unfolding prime_nat_iff
 proof safe
-  fix m assume p: "p > 0" "p \<noteq> 1" and m: "m dvd p" "m \<noteq> p" 
-           and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
+  fix m
+  assume p: "p > 0" "p \<noteq> 1"
+    and m: "m dvd p" "m \<noteq> p"
+    and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
   from p m have "m \<noteq> 0" by (intro notI) auto
   moreover from p m have "m < p" by (auto dest: dvd_imp_le)
-  ultimately have "coprime p m" using * by blast
+  ultimately have "coprime p m"
+    using * by blast
   with m show "m = 1" by simp
-qed (auto simp: prime_nat_iff simp del: One_nat_def 
-          intro!: prime_imp_coprime dest: dvd_imp_le)
+qed (auto simp: prime_nat_iff simp del: One_nat_def intro!: prime_imp_coprime dest: dvd_imp_le)
 
 lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
-proof-
+proof -
   have "{ m. 0 < m \<and> m < n } = {1..<n}" by auto
-  thus ?thesis by simp
+  then show ?thesis by simp
 qed
 
 
-subsection\<open>Some basic theorems about solving congruences\<close>
+subsection \<open>Some basic theorems about solving congruences\<close>
 
-lemma cong_solve: 
-  fixes n::nat assumes an: "coprime a n" shows "\<exists>x. [a * x = b] (mod n)"
-proof-
-  {assume "a=0" hence ?thesis using an by (simp add: cong_nat_def)}
-  moreover
-  {assume az: "a\<noteq>0"
-  from bezout_add_strong_nat[OF az, of n]
-  obtain d x y where dxy: "d dvd a" "d dvd n" "a*x = n*y + d" by blast
+lemma cong_solve:
+  fixes n :: nat
+  assumes an: "coprime a n"
+  shows "\<exists>x. [a * x = b] (mod n)"
+proof (cases "a = 0")
+  case True
+  with an show ?thesis
+    by (simp add: cong_nat_def)
+next
+  case False
+  from bezout_add_strong_nat [OF this]
+  obtain d x y where dxy: "d dvd a" "d dvd n" "a * x = n * y + d" by blast
   from dxy(1,2) have d1: "d = 1"
-    by (metis assms coprime_nat) 
-  hence "a*x*b = (n*y + 1)*b" using dxy(3) by simp
-  hence "a*(x*b) = n*(y*b) + b" 
-    by (auto simp add: algebra_simps)
-  hence "a*(x*b) mod n = (n*(y*b) + b) mod n" by simp
-  hence "a*(x*b) mod n = b mod n" by (simp add: mod_add_left_eq)
-  hence "[a*(x*b) = b] (mod n)" unfolding cong_nat_def .
-  hence ?thesis by blast}
-ultimately  show ?thesis by blast
+    by (metis assms coprime_nat)
+  with dxy(3) have "a * x * b = (n * y + 1) * b"
+    by simp
+  then have "a * (x * b) = n * (y * b) + b"
+    by (auto simp: algebra_simps)
+  then have "a * (x * b) mod n = (n * (y * b) + b) mod n"
+    by simp
+  then have "a * (x * b) mod n = b mod n"
+    by (simp add: mod_add_left_eq)
+  then have "[a * (x * b) = b] (mod n)"
+    by (simp only: cong_nat_def)
+  then show ?thesis by blast
 qed
 
-lemma cong_solve_unique: 
-  fixes n::nat assumes an: "coprime a n" and nz: "n \<noteq> 0"
+lemma cong_solve_unique:
+  fixes n :: nat
+  assumes an: "coprime a n" and nz: "n \<noteq> 0"
   shows "\<exists>!x. x < n \<and> [a * x = b] (mod n)"
-proof-
+proof -
+  from cong_solve[OF an] obtain x where x: "[a * x = b] (mod n)"
+    by blast
   let ?P = "\<lambda>x. x < n \<and> [a * x = b] (mod n)"
-  from cong_solve[OF an] obtain x where x: "[a*x = b] (mod n)" by blast
   let ?x = "x mod n"
-  from x have th: "[a * ?x = b] (mod n)"
+  from x have *: "[a * ?x = b] (mod n)"
     by (simp add: cong_nat_def mod_mult_right_eq[of a x n])
-  from mod_less_divisor[ of n x] nz th have Px: "?P ?x" by simp
-  {fix y assume Py: "y < n" "[a * y = b] (mod n)"
-    from Py(2) th have "[a * y = a*?x] (mod n)" by (simp add: cong_nat_def)
-    hence "[y = ?x] (mod n)"
-      by (metis an cong_mult_lcancel_nat) 
+  from mod_less_divisor[ of n x] nz * have Px: "?P ?x" by simp
+  have "y = ?x" if Py: "y < n" "[a * y = b] (mod n)" for y
+  proof -
+    from Py(2) * have "[a * y = a * ?x] (mod n)"
+      by (simp add: cong_nat_def)
+    then have "[y = ?x] (mod n)"
+      by (metis an cong_mult_lcancel_nat)
     with mod_less[OF Py(1)] mod_less_divisor[ of n x] nz
-    have "y = ?x" by (simp add: cong_nat_def)}
+    show ?thesis
+      by (simp add: cong_nat_def)
+  qed
   with Px show ?thesis by blast
 qed
 
 lemma cong_solve_unique_nontrivial:
-  assumes p: "prime (p::nat)" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p"
+  fixes p :: nat
+  assumes p: "prime p"
+    and pa: "coprime p a"
+    and x0: "0 < x"
+    and xp: "x < p"
   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
-proof-
+proof -
   from pa have ap: "coprime a p"
-    by (metis gcd.commute) 
-  have px:"coprime x p"
+    by (metis gcd.commute)
+  have px: "coprime x p"
     by (metis gcd.commute p prime_nat_iff'' x0 xp)
   obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y"
     by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
-  {assume y0: "y = 0"
-    with y(2) have th: "p dvd a"
+  have "y \<noteq> 0"
+  proof
+    assume "y = 0"
+    with y(2) have "p dvd a"
       by (auto dest: cong_dvd_eq_nat)
-    have False
-      by (metis gcd_nat.absorb1 not_prime_1 p pa th)}
-  with y show ?thesis unfolding Ex1_def using neq0_conv by blast
+    then show False
+      by (metis gcd_nat.absorb1 not_prime_1 p pa)
+  qed
+  with y show ?thesis
+    by blast
 qed
 
 lemma cong_unique_inverse_prime:
-  assumes "prime (p::nat)" and "0 < x" and "x < p"
+  fixes p :: nat
+  assumes "prime p" and "0 < x" and "x < p"
   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
-  by (rule cong_solve_unique_nontrivial) (insert assms, simp_all)
+  by (rule cong_solve_unique_nontrivial) (use assms in simp_all)
 
 lemma chinese_remainder_coprime_unique:
-  fixes a::nat 
+  fixes a :: nat
   assumes ab: "coprime a b" and az: "a \<noteq> 0" and bz: "b \<noteq> 0"
-  and ma: "coprime m a" and nb: "coprime n b"
+    and ma: "coprime m a" and nb: "coprime n b"
   shows "\<exists>!x. coprime x (a * b) \<and> x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
-proof-
+proof -
   let ?P = "\<lambda>x. x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
   from binary_chinese_remainder_unique_nat[OF ab az bz]
-  obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)"
-    "\<forall>y. ?P y \<longrightarrow> y = x" by blast
-  from ma nb x
-  have "coprime x a" "coprime x b"
+  obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)" "\<forall>y. ?P y \<longrightarrow> y = x"
+    by blast
+  from ma nb x have "coprime x a" "coprime x b"
     by (metis cong_gcd_eq_nat)+
   then have "coprime x (a*b)"
     by (metis coprime_mul_eq)
-  with x show ?thesis by blast
+  with x show ?thesis
+    by blast
 qed
 
 
-subsection\<open>Lucas's theorem\<close>
+subsection \<open>Lucas's theorem\<close>
 
 lemma lucas_coprime_lemma:
-  fixes n::nat 
-  assumes m: "m\<noteq>0" and am: "[a^m = 1] (mod n)"
+  fixes n :: nat
+  assumes m: "m \<noteq> 0" and am: "[a^m = 1] (mod n)"
   shows "coprime a n"
-proof-
-  {assume "n=1" hence ?thesis by simp}
-  moreover
-  {assume "n = 0" hence ?thesis using am m 
-     by (metis am cong_0_nat gcd_nat.right_neutral power_eq_one_eq_nat)}
-  moreover
-  {assume n: "n\<noteq>0" "n\<noteq>1"
-    from m obtain m' where m': "m = Suc m'" by (cases m, blast+)
-    {fix d
-      assume d: "d dvd a" "d dvd n"
-      from n have n1: "1 < n" by arith
-      from am mod_less[OF n1] have am1: "a^m mod n = 1" unfolding cong_nat_def by simp
-      from dvd_mult2[OF d(1), of "a^m'"] have dam:"d dvd a^m" by (simp add: m')
-      from dvd_mod_iff[OF d(2), of "a^m"] dam am1
-      have "d = 1" by simp }
-    hence ?thesis by auto
-  }
-  ultimately show ?thesis by blast
+proof -
+  consider "n = 1" | "n = 0" | "n > 1" by arith
+  then show ?thesis
+  proof cases
+    case 1
+    then show ?thesis by simp
+  next
+    case 2
+    with am m show ?thesis
+      by (metis am cong_0_nat gcd_nat.right_neutral power_eq_one_eq_nat)
+  next
+    case 3
+    from m obtain m' where m': "m = Suc m'" by (cases m) blast+
+    have "d = 1" if d: "d dvd a" "d dvd n" for d
+    proof -
+      from am mod_less[OF \<open>n > 1\<close>] have am1: "a^m mod n = 1"
+        by (simp add: cong_nat_def)
+      from dvd_mult2[OF d(1), of "a^m'"] have dam: "d dvd a^m"
+        by (simp add: m')
+      from dvd_mod_iff[OF d(2), of "a^m"] dam am1 show ?thesis
+        by simp
+    qed
+    then show ?thesis by blast
+  qed
 qed
 
 lemma lucas_weak:
-  fixes n::nat 
-  assumes n: "n \<ge> 2" and an: "[a ^ (n - 1) = 1] (mod n)"
-  and nm: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)"
+  fixes n :: nat
+  assumes n: "n \<ge> 2"
+    and an: "[a ^ (n - 1) = 1] (mod n)"
+    and nm: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)"
   shows "prime n"
 proof (rule totient_imp_prime)
   show "totient n = n - 1"
   proof (rule ccontr)
     have "[a ^ totient n = 1] (mod n)"
-      by (rule euler_theorem, rule lucas_coprime_lemma [of "n - 1"])
-        (use n an in auto)
+      by (rule euler_theorem, rule lucas_coprime_lemma [of "n - 1"]) (use n an in auto)
     moreover assume "totient n \<noteq> n - 1"
-    then have "totient n > 0 \<and> totient n < n - 1"
-      using \<open>n \<ge> 2\<close> and totient_less[of n] by simp
+    then have "totient n > 0" "totient n < n - 1"
+      using \<open>n \<ge> 2\<close> and totient_less[of n] by simp_all
     ultimately show False
       using nm by auto
   qed
-qed (insert n, auto)
+qed (use n in auto)
 
 lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"
   by (metis ex_least_nat_le not_less0)
 
-lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> (P (Least P) \<and> (\<forall>m < (Least P). \<not> P m))"
+lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> P (Least P) \<and> (\<forall>m < (Least P). \<not> P m)"
   (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
-  {assume ?rhs hence ?lhs by blast}
-  moreover
-  { assume H: ?lhs then obtain n where n: "P n" by blast
+proof
+  show ?lhs if ?rhs
+    using that by blast
+  show ?rhs if ?lhs
+  proof -
+    from \<open>?lhs\<close> obtain n where n: "P n" by blast
     let ?x = "Least P"
-    {fix m assume m: "m < ?x"
-      from not_less_Least[OF m] have "\<not> P m" .}
-    with LeastI_ex[OF H] have ?rhs by blast}
-  ultimately show ?thesis by blast
+    have "\<not> P m" if "m < ?x" for m
+      by (rule not_less_Least[OF that])
+    with LeastI_ex[OF \<open>?lhs\<close>] show ?thesis
+      by blast
+  qed
 qed
 
 theorem lucas:
   assumes n2: "n \<ge> 2" and an1: "[a^(n - 1) = 1] (mod n)"
-  and pn: "\<forall>p. prime p \<and> p dvd n - 1 \<longrightarrow> [a^((n - 1) div p) \<noteq> 1] (mod n)"
+    and pn: "\<forall>p. prime p \<and> p dvd n - 1 \<longrightarrow> [a^((n - 1) div p) \<noteq> 1] (mod n)"
   shows "prime n"
 proof-
-  from n2 have n01: "n\<noteq>0" "n\<noteq>1" "n - 1 \<noteq> 0" by arith+
-  from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1" by simp
+  from n2 have n01: "n \<noteq> 0" "n \<noteq> 1" "n - 1 \<noteq> 0"
+    by arith+
+  from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1"
+    by simp
   from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1
   have an: "coprime a n" "coprime (a^(n - 1)) n"
     by (auto simp add: coprime_exp gcd.commute)
-  {assume H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
+  have False if H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
+  proof -
     from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
-      m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k" by blast
-    {assume nm1: "(n - 1) mod m > 0"
+      m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k"
+      by blast
+    have False if nm1: "(n - 1) mod m > 0"
+    proof -
       from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast
       let ?y = "a^ ((n - 1) div m * m)"
       note mdeq = div_mult_mod_eq[of "(n - 1)" m]
@@ -199,53 +236,62 @@
         using power_mod[of "a^m" n "(n - 1) div m"] by simp
       also have "\<dots> = 1" using m(3)[unfolded cong_nat_def onen] onen
         by (metis power_one)
-      finally have th3: "?y mod n = 1"  .
-      have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
+      finally have *: "?y mod n = 1"  .
+      have **: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
         using an1[unfolded cong_nat_def onen] onen
           div_mult_mod_eq[of "(n - 1)" m, symmetric]
-        by (simp add:power_add[symmetric] cong_nat_def th3 del: One_nat_def)
-      have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)"
-        by (metis cong_mult_rcancel_nat mult.commute th2 yn)
-      from m(4)[rule_format, OF th0] nm1
-        less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] th1
-      have False by blast }
-    hence "(n - 1) mod m = 0" by auto
+        by (simp add:power_add[symmetric] cong_nat_def * del: One_nat_def)
+      have "[a ^ ((n - 1) mod m) = 1] (mod n)"
+        by (metis cong_mult_rcancel_nat mult.commute ** yn)
+      with m(4)[rule_format, OF th0] nm1
+        less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] show ?thesis
+        by blast
+    qed
+    then have "(n - 1) mod m = 0" by auto
     then have mn: "m dvd n - 1" by presburger
-    then obtain r where r: "n - 1 = m*r" unfolding dvd_def by blast
-    from n01 r m(2) have r01: "r\<noteq>0" "r\<noteq>1" by - (rule ccontr, simp)+
+    then obtain r where r: "n - 1 = m * r"
+      unfolding dvd_def by blast
+    from n01 r m(2) have r01: "r \<noteq> 0" "r \<noteq> 1" by auto
     obtain p where p: "prime p" "p dvd r"
       by (metis prime_factor_nat r01(2))
-    hence th: "prime p \<and> p dvd n - 1" unfolding r by (auto intro: dvd_mult)
-    have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r
+    then have th: "prime p \<and> p dvd n - 1"
+      unfolding r by (auto intro: dvd_mult)
+    from r have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n"
       by (simp add: power_mult)
-    also have "\<dots> = (a^(m*(r div p))) mod n" 
-      using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] 
-      by simp
-    also have "\<dots> = ((a^m)^(r div p)) mod n" by (simp add: power_mult)
-    also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod ..
-    also have "\<dots> = 1" using m(3) onen by (simp add: cong_nat_def)
+    also have "\<dots> = (a^(m*(r div p))) mod n"
+      using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] by simp
+    also have "\<dots> = ((a^m)^(r div p)) mod n"
+      by (simp add: power_mult)
+    also have "\<dots> = ((a^m mod n)^(r div p)) mod n"
+      using power_mod ..
+    also from m(3) onen have "\<dots> = 1"
+      by (simp add: cong_nat_def)
     finally have "[(a ^ ((n - 1) div p))= 1] (mod n)"
       using onen by (simp add: cong_nat_def)
-    with pn th have False by blast}
-  hence th: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" by blast
-  from lucas_weak[OF n2 an1 th] show ?thesis .
+    with pn th show ?thesis by blast
+  qed
+  then have "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)"
+    by blast
+  then show ?thesis by (rule lucas_weak[OF n2 an1])
 qed
 
 
-subsection\<open>Definition of the order of a number mod n (0 in non-coprime case)\<close>
+subsection \<open>Definition of the order of a number mod n (0 in non-coprime case)\<close>
 
 definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)"
 
-(* This has the expected properties.                                         *)
+text \<open>This has the expected properties.\<close>
 
 lemma coprime_ord:
-  fixes n::nat 
+  fixes n::nat
   assumes "coprime n a"
   shows "ord n a > 0 \<and> [a ^(ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> [a^ m \<noteq> 1] (mod n))"
 proof-
   let ?P = "\<lambda>d. 0 < d \<and> [a ^ d = 1] (mod n)"
-  from bigger_prime[of a] obtain p where p: "prime p" "a < p" by blast
-  from assms have o: "ord n a = Least ?P" by (simp add: ord_def)
+  from bigger_prime[of a] obtain p where p: "prime p" "a < p"
+    by blast
+  from assms have o: "ord n a = Least ?P"
+    by (simp add: ord_def)
   have ex: "\<exists>m>0. ?P m"
   proof (cases "n \<ge> 2")
     case True
@@ -266,136 +312,143 @@
     unfolding o[symmetric] by auto
 qed
 
-(* With the special value 0 for non-coprime case, it's more convenient.      *)
-lemma ord_works:
-  fixes n::nat
-  shows "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> ~[a^ m = 1] (mod n))"
-apply (cases "coprime n a")
-using coprime_ord[of n a]
-by (auto simp add: ord_def cong_nat_def)
+text \<open>With the special value \<open>0\<close> for non-coprime case, it's more convenient.\<close>
+lemma ord_works: "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> \<not> [a^ m = 1] (mod n))"
+  for n :: nat
+  by (cases "coprime n a") (use coprime_ord[of n a] in \<open>auto simp add: ord_def cong_nat_def\<close>)
 
-lemma ord:
-  fixes n::nat
-  shows "[a^(ord n a) = 1] (mod n)" using ord_works by blast
+lemma ord: "[a^(ord n a) = 1] (mod n)"
+  for n :: nat
+  using ord_works by blast
 
-lemma ord_minimal:
-  fixes n::nat
-  shows "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> ~[a^m = 1] (mod n)"
+lemma ord_minimal: "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> \<not> [a^m = 1] (mod n)"
+  for n :: nat
   using ord_works by blast
 
-lemma ord_eq_0:
-  fixes n::nat
-  shows "ord n a = 0 \<longleftrightarrow> ~coprime n a"
-by (cases "coprime n a", simp add: coprime_ord, simp add: ord_def)
+lemma ord_eq_0: "ord n a = 0 \<longleftrightarrow> \<not> coprime n a"
+  for n :: nat
+  by (cases "coprime n a") (simp add: coprime_ord, simp add: ord_def)
 
-lemma divides_rexp: 
-  "x dvd y \<Longrightarrow> (x::nat) dvd (y^(Suc n))" 
+lemma divides_rexp: "x dvd y \<Longrightarrow> x dvd (y ^ Suc n)"
+  for x y :: nat
   by (simp add: dvd_mult2[of x y])
 
-lemma ord_divides:
-  fixes n::nat
-  shows "[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d" (is "?lhs \<longleftrightarrow> ?rhs")
+lemma ord_divides:"[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d"
+  (is "?lhs \<longleftrightarrow> ?rhs")
+  for n :: nat
 proof
-  assume rh: ?rhs
-  then obtain k where "d = ord n a * k" unfolding dvd_def by blast
-  hence "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)"
+  assume ?rhs
+  then obtain k where "d = ord n a * k"
+    unfolding dvd_def by blast
+  then have "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)"
     by (simp add : cong_nat_def power_mult power_mod)
   also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)"
     using ord[of a n, unfolded cong_nat_def]
     by (simp add: cong_nat_def power_mod)
-  finally  show ?lhs .
+  finally show ?lhs .
 next
-  assume lh: ?lhs
-  { assume H: "\<not> coprime n a"
-    hence o: "ord n a = 0" by (simp add: ord_def)
-    {assume d: "d=0" with o H have ?rhs by (simp add: cong_nat_def)}
-    moreover
-    {assume d0: "d\<noteq>0" then obtain d' where d': "d = Suc d'" by (cases d, auto)
-      from H
-      obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
-      from lh
-      obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2"
-        by (metis H d0 gcd.commute lucas_coprime_lemma) 
-      hence "a ^ d + n * q1 - n * q2 = 1" by simp
-      with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2  d' p
-      have "p dvd 1"
+  assume ?lhs
+  show ?rhs
+  proof (cases "coprime n a")
+    case prem: False
+    then have o: "ord n a = 0" by (simp add: ord_def)
+    show ?thesis
+    proof (cases d)
+      case 0
+      with o prem show ?thesis by (simp add: cong_nat_def)
+    next
+      case (Suc d')
+      then have d0: "d \<noteq> 0" by simp
+      from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
+      from \<open>?lhs\<close> obtain q1 q2 where q12: "a ^ d + n * q1 = 1 + n * q2"
+        by (metis prem d0 gcd.commute lucas_coprime_lemma)
+      then have "a ^ d + n * q1 - n * q2 = 1" by simp
+      with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2 Suc p have "p dvd 1"
         by metis
       with p(3) have False by simp
-      hence ?rhs ..}
-    ultimately have ?rhs by blast}
-  moreover
-  {assume H: "coprime n a"
+      then show ?thesis ..
+    qed
+  next
+    case H: True
     let ?o = "ord n a"
     let ?q = "d div ord n a"
     let ?r = "d mod ord n a"
     have eqo: "[(a^?o)^?q = 1] (mod n)"
       by (metis cong_exp_nat ord power_one)
     from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
-    hence op: "?o > 0" by simp
-    from div_mult_mod_eq[of d "ord n a"] lh
-    have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: cong_nat_def mult.commute)
-    hence "[(a^?o)^?q * (a^?r) = 1] (mod n)"
+    then have op: "?o > 0" by simp
+    from div_mult_mod_eq[of d "ord n a"] \<open>?lhs\<close>
+    have "[a^(?o*?q + ?r) = 1] (mod n)"
+      by (simp add: cong_nat_def mult.commute)
+    then have "[(a^?o)^?q * (a^?r) = 1] (mod n)"
       by (simp add: cong_nat_def power_mult[symmetric] power_add[symmetric])
-    hence th: "[a^?r = 1] (mod n)"
+    then have th: "[a^?r = 1] (mod n)"
       using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
-      apply (simp add: cong_nat_def del: One_nat_def)
-      by (metis mod_mult_left_eq nat_mult_1)
-    {assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)}
-    moreover
-    {assume r: "?r \<noteq> 0"
+      by (simp add: cong_nat_def del: One_nat_def) (metis mod_mult_left_eq nat_mult_1)
+    show ?thesis
+    proof (cases "?r = 0")
+      case True
+      then show ?thesis by (simp add: dvd_eq_mod_eq_0)
+    next
+      case False
       with mod_less_divisor[OF op, of d] have r0o:"?r >0 \<and> ?r < ?o" by simp
       from conjunct2[OF ord_works[of a n], rule_format, OF r0o] th
-      have ?rhs by blast}
-    ultimately have ?rhs by blast}
-  ultimately  show ?rhs by blast
+      show ?thesis by blast
+    qed
+  qed
 qed
 
-lemma order_divides_totient:
-  "ord n a dvd totient n" if "coprime n a"
+lemma order_divides_totient: "ord n a dvd totient n" if "coprime n a"
   by (metis euler_theorem gcd.commute ord_divides that)
 
 lemma order_divides_expdiff:
   fixes n::nat and a::nat assumes na: "coprime n a"
   shows "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
-proof-
-  {fix n::nat and a::nat and d::nat and e::nat
-    assume na: "coprime n a" and ed: "(e::nat) \<le> d"
-    hence "\<exists>c. d = e + c" by presburger
-    then obtain c where c: "d = e + c" by presburger
+proof -
+  have th: "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
+    if na: "coprime n a" and ed: "(e::nat) \<le> d"
+    for n a d e :: nat
+  proof -
+    from na ed have "\<exists>c. d = e + c" by presburger
+    then obtain c where c: "d = e + c" ..
     from na have an: "coprime a n"
       by (metis gcd.commute)
     have aen: "coprime (a^e) n"
-      by (metis coprime_exp gcd.commute na)      
+      by (metis coprime_exp gcd.commute na)
     have acn: "coprime (a^c) n"
-      by (metis coprime_exp gcd.commute na) 
-    have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
-      using c by simp
+      by (metis coprime_exp gcd.commute na)
+    from c have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
+      by simp
     also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
     also have  "\<dots> \<longleftrightarrow> [a ^ c = 1] (mod n)"
       using cong_mult_lcancel_nat [OF aen, of "a^c" "a^0"] by simp
-    also  have "\<dots> \<longleftrightarrow> ord n a dvd c" by (simp only: ord_divides)
+    also have "\<dots> \<longleftrightarrow> ord n a dvd c"
+      by (simp only: ord_divides)
     also have "\<dots> \<longleftrightarrow> [e + c = e + 0] (mod ord n a)"
-      using cong_add_lcancel_nat 
+      using cong_add_lcancel_nat
       by (metis cong_dvd_eq_nat dvd_0_right cong_dvd_modulus_nat cong_mult_self_nat nat_mult_1)
-    finally have "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
-      using c by simp }
-  note th = this
-  have "e \<le> d \<or> d \<le> e" by arith
-  moreover
-  {assume ed: "e \<le> d" from th[OF na ed] have ?thesis .}
-  moreover
-  {assume de: "d \<le> e"
-    from th[OF na de] have ?thesis
-    by (metis cong_sym_nat)}
-  ultimately show ?thesis by blast
+    finally show ?thesis
+      using c by simp
+  qed
+  consider "e \<le> d" | "d \<le> e" by arith
+  then show ?thesis
+  proof cases
+    case 1
+    with na show ?thesis by (rule th)
+  next
+    case 2
+    from th[OF na this] show ?thesis
+      by (metis cong_sym_nat)
+  qed
 qed
 
-subsection\<open>Another trivial primality characterization\<close>
+
+subsection \<open>Another trivial primality characterization\<close>
 
-lemma prime_prime_factor:
-  "prime (n::nat) \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)" 
+lemma prime_prime_factor: "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)"
   (is "?lhs \<longleftrightarrow> ?rhs")
-proof (cases "n=0 \<or> n=1")
+  for n :: nat
+proof (cases "n = 0 \<or> n = 1")
   case True
   then show ?thesis
      by (metis bigger_prime dvd_0_right not_prime_1 not_prime_0)
@@ -405,7 +458,7 @@
   proof
     assume "prime n"
     then show ?rhs
-      by (metis  not_prime_1 prime_nat_iff)
+      by (metis not_prime_1 prime_nat_iff)
   next
     assume ?rhs
     with False show "prime n"
@@ -413,322 +466,402 @@
   qed
 qed
 
-lemma prime_divisor_sqrt:
-  "prime (n::nat) \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
+lemma prime_divisor_sqrt: "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
+  for n :: nat
 proof -
-  {assume "n=0 \<or> n=1" hence ?thesis
-    by auto}
-  moreover
-  {assume n: "n\<noteq>0" "n\<noteq>1"
-    hence np: "n > 1" by arith
-    {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" and H: "\<forall>m. m dvd n \<longrightarrow> m=1 \<or> m=n"
-      from H d have d1n: "d = 1 \<or> d=n" by blast
-      {assume dn: "d=n"
-        have "n\<^sup>2 > n*1" using n by (simp add: power2_eq_square)
-        with dn d(2) have "d=1" by simp}
-      with d1n have "d = 1" by blast  }
+  consider "n = 0" | "n = 1" | "n \<noteq> 0" "n \<noteq> 1" by blast
+  then show ?thesis
+  proof cases
+    case 1
+    then show ?thesis by simp
+  next
+    case 2
+    then show ?thesis by simp
+  next
+    case n: 3
+    then have np: "n > 1" by arith
+    {
+      fix d
+      assume d: "d dvd n" "d\<^sup>2 \<le> n"
+        and H: "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
+      from H d have d1n: "d = 1 \<or> d = n" by blast
+      then have "d = 1"
+      proof
+        assume dn: "d = n"
+        from n have "n\<^sup>2 > n * 1"
+          by (simp add: power2_eq_square)
+        with dn d(2) show ?thesis by simp
+      qed
+    }
     moreover
-    {fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1"
+    {
+      fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1"
       from d n have "d \<noteq> 0"
         by (metis dvd_0_left_iff)
-      hence dp: "d > 0" by simp
+      then have dp: "d > 0" by simp
       from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast
       from n dp e have ep:"e > 0" by simp
-      have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n" using dp ep
+      from dp ep have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n"
         by (auto simp add: e power2_eq_square mult_le_cancel_left)
-      moreover
-      {assume h: "d\<^sup>2 \<le> n"
-        from H[rule_format, of d] h d have "d = 1" by blast}
-      moreover
-      {assume h: "e\<^sup>2 \<le> n"
-        from e have "e dvd n" unfolding dvd_def by (simp add: mult.commute)
-        with H[rule_format, of e] h have "e=1" by simp
-        with e have "d = n" by simp}
-      ultimately have "d=1 \<or> d=n"  by blast}
-    ultimately have ?thesis unfolding prime_nat_iff using np n(2) by blast}
-  ultimately show ?thesis by auto
+      then have "d = 1 \<or> d = n"
+      proof
+        assume "d\<^sup>2 \<le> n"
+        with H[rule_format, of d] d have "d = 1" by blast
+        then show ?thesis ..
+      next
+        assume h: "e\<^sup>2 \<le> n"
+        from e have "e dvd n" by (simp add: dvd_def mult.commute)
+        with H[rule_format, of e] h have "e = 1" by simp
+        with e have "d = n" by simp
+        then show ?thesis ..
+      qed
+    }
+    ultimately show ?thesis
+      unfolding prime_nat_iff using np n(2) by blast
+  qed
 qed
 
 lemma prime_prime_factor_sqrt:
-  "prime (n::nat) \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
+  "prime (n::nat) \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> (\<nexists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
   (is "?lhs \<longleftrightarrow>?rhs")
-proof-
-  {assume "n=0 \<or> n=1" 
-   hence ?thesis
-     by (metis not_prime_0 not_prime_1)}
-  moreover
-  {assume n: "n\<noteq>0" "n\<noteq>1"
-    {assume H: ?lhs
-      from H[unfolded prime_divisor_sqrt] n
-      have ?rhs
-        by (metis prime_prime_factor) }
-    moreover
-    {assume H: ?rhs
-      {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1"
+proof -
+  consider "n = 0" | "n = 1" | "n \<noteq> 0" "n \<noteq> 1"
+    by blast
+  then show ?thesis
+  proof cases
+    case 1
+    then show ?thesis by (metis not_prime_0)
+  next
+    case 2
+    then show ?thesis by (metis not_prime_1)
+  next
+    case n: 3
+    show ?thesis
+    proof
+      assume ?lhs
+      from this[unfolded prime_divisor_sqrt] n show ?rhs
+        by (metis prime_prime_factor)
+    next
+      assume ?rhs
+      {
+        fix d
+        assume d: "d dvd n" "d\<^sup>2 \<le> n" "d \<noteq> 1"
         then obtain p where p: "prime p" "p dvd d"
-          by (metis prime_factor_nat) 
+          by (metis prime_factor_nat)
         from d(1) n have dp: "d > 0"
-          by (metis dvd_0_left neq0_conv) 
+          by (metis dvd_0_left neq0_conv)
         from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)
         have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith
-        with H n p(1) dvd_trans[OF p(2) d(1)] have False  by blast}
-      with n prime_divisor_sqrt  have ?lhs by auto}
-    ultimately have ?thesis by blast }
-  ultimately show ?thesis by (cases "n=0 \<or> n=1", auto)
+        with \<open>?rhs\<close> n p(1) dvd_trans[OF p(2) d(1)] have False
+          by blast
+      }
+      with n prime_divisor_sqrt show ?lhs by auto
+    qed
+  qed
 qed
 
 
-subsection\<open>Pocklington theorem\<close>
+subsection \<open>Pocklington theorem\<close>
 
 lemma pocklington_lemma:
-  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and an: "[a^ (n - 1) = 1] (mod n)"
-  and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
-  and pp: "prime (p::nat)" and pn: "p dvd n"
+  fixes p :: nat
+  assumes n: "n \<ge> 2" and nqr: "n - 1 = q * r"
+    and an: "[a^ (n - 1) = 1] (mod n)"
+    and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n"
+    and pp: "prime p" and pn: "p dvd n"
   shows "[p = 1] (mod q)"
 proof -
-  have p01: "p \<noteq> 0" "p \<noteq> 1" using pp by (auto intro: prime_gt_0_nat)
-  obtain k where k: "a ^ (q * r) - 1 = n*k"
+  have p01: "p \<noteq> 0" "p \<noteq> 1"
+    using pp by (auto intro: prime_gt_0_nat)
+  obtain k where k: "a ^ (q * r) - 1 = n * k"
     by (metis an cong_to_1_nat dvd_def nqr)
-  from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast
-  {assume a0: "a = 0"
-    hence "a^ (n - 1) = 0" using n by (simp add: power_0_left)
-    with n an mod_less[of 1 n]  have False by (simp add: power_0_left cong_nat_def)}
-  hence a0: "a\<noteq>0" ..
-  from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp
-  hence "(a ^ (q * r) - 1) + 1  = a ^ (q * r)" by simp
-  with k l have "a ^ (q * r) = p*l*k + 1" by simp
-  hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: ac_simps)
-  hence odq: "ord p (a^r) dvd q"
+  from pn[unfolded dvd_def] obtain l where l: "n = p * l"
+    by blast
+  have a0: "a \<noteq> 0"
+  proof
+    assume "a = 0"
+    with n have "a^ (n - 1) = 0"
+      by (simp add: power_0_left)
+    with n an mod_less[of 1 n] show False
+      by (simp add: power_0_left cong_nat_def)
+  qed
+  with n nqr have aqr0: "a ^ (q * r) \<noteq> 0"
+    by simp
+  then have "(a ^ (q * r) - 1) + 1  = a ^ (q * r)"
+    by simp
+  with k l have "a ^ (q * r) = p * l * k + 1"
+    by simp
+  then have "a ^ (r * q) + p * 0 = 1 + p * (l * k)"
+    by (simp add: ac_simps)
+  then have odq: "ord p (a^r) dvd q"
     unfolding ord_divides[symmetric] power_mult[symmetric]
-    by (metis an cong_dvd_modulus_nat mult.commute nqr pn) 
-  from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d" by blast
-  {assume d1: "d \<noteq> 1"
+    by (metis an cong_dvd_modulus_nat mult.commute nqr pn)
+  from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d"
+    by blast
+  have d1: "d = 1"
+  proof (rule ccontr)
+    assume d1: "d \<noteq> 1"
     obtain P where P: "prime P" "P dvd d"
-      by (metis d1 prime_factor_nat) 
+      by (metis d1 prime_factor_nat)
     from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp
     from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast
     from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast
-    have P0: "P \<noteq> 0" using P(1)
-      by (metis not_prime_0) 
+    from P(1) have P0: "P \<noteq> 0"
+      by (metis not_prime_0)
     from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast
     from d s t P0  have s': "ord p (a^r) * t = s"
-      by (metis mult.commute mult_cancel1 mult.assoc) 
+      by (metis mult.commute mult_cancel1 mult.assoc)
     have "ord p (a^r) * t*r = r * ord p (a^r) * t"
       by (metis mult.assoc mult.commute)
-    hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"
+    then have exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"
       by (simp only: power_mult)
-    then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"
+    then have "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"
       by (metis cong_exp_nat ord power_one)
-    have pd0: "p dvd a^(ord p (a^r) * t*r) - 1"
-      by (metis cong_to_1_nat exps th)
-    from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" using P0 by simp
+    then have pd0: "p dvd a^(ord p (a^r) * t*r) - 1"
+      by (metis cong_to_1_nat exps)
+    from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r"
+      using P0 by simp
     with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp
-    with p01 pn pd0 coprime_common_divisor_nat have False 
-      by auto}
-  hence d1: "d = 1" by blast
-  hence o: "ord p (a^r) = q" using d by simp
-  from pp totient_prime [of p]
-  have totient_eq: "totient p = p - 1" by simp
-  {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
+    with p01 pn pd0 coprime_common_divisor_nat show False
+      by auto
+  qed
+  with d have o: "ord p (a^r) = q" by simp
+  from pp totient_prime [of p] have totient_eq: "totient p = p - 1"
+    by simp
+  {
+    fix d
+    assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
     from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast
     from n have "n \<noteq> 0" by simp
     then have False using d dp pn
-      by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)} 
-  hence cpa: "coprime p a" by auto
+      by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)
+  }
+  then have cpa: "coprime p a" by auto
   have arp: "coprime (a^r) p"
-    by (metis coprime_exp cpa gcd.commute) 
-  from euler_theorem [OF arp, simplified ord_divides] o totient_eq
-  have "q dvd (p - 1)" by simp
-  then obtain d where d:"p - 1 = q * d" 
+    by (metis coprime_exp cpa gcd.commute)
+  from euler_theorem [OF arp, simplified ord_divides] o totient_eq have "q dvd (p - 1)"
+    by simp
+  then obtain d where d:"p - 1 = q * d"
     unfolding dvd_def by blast
-  have p0:"p \<noteq> 0"
-    by (metis p01(1)) 
-  from p0 d have "p + q * 0 = 1 + q * d" by simp
+  have "p \<noteq> 0"
+    by (metis p01(1))
+  with d have "p + q * 0 = 1 + q * d" by simp
   then show ?thesis
     by (metis cong_iff_lin_nat mult.commute)
 qed
 
 theorem pocklington:
-  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
-  and an: "[a^ (n - 1) = 1] (mod n)"
-  and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
+  assumes n: "n \<ge> 2" and nqr: "n - 1 = q * r" and sqr: "n \<le> q\<^sup>2"
+    and an: "[a^ (n - 1) = 1] (mod n)"
+    and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
   shows "prime n"
-unfolding prime_prime_factor_sqrt[of n]
-proof-
-  let ?ths = "n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
-  from n have n01: "n\<noteq>0" "n\<noteq>1" by arith+
-  {fix p assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n"
-    from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)" by (simp add: power2_eq_square)
-    hence pq: "p \<le> q"
-      by (metis le0 power_le_imp_le_base) 
-    from pocklington_lemma[OF n nqr an aq p(1,2)] 
-    have th: "q dvd p - 1"
-      by (metis cong_to_1_nat) 
-    have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
-    with pq th have False
-      by (simp add: nat_dvd_not_less)}
+  unfolding prime_prime_factor_sqrt[of n]
+proof -
+  let ?ths = "n \<noteq> 0 \<and> n \<noteq> 1 \<and> (\<nexists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
+  from n have n01: "n \<noteq> 0" "n \<noteq> 1" by arith+
+  {
+    fix p
+    assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n"
+    from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)"
+      by (simp add: power2_eq_square)
+    then have pq: "p \<le> q"
+      by (metis le0 power_le_imp_le_base)
+    from pocklington_lemma[OF n nqr an aq p(1,2)] have *: "q dvd p - 1"
+      by (metis cong_to_1_nat)
+    have "p - 1 \<noteq> 0"
+      using prime_ge_2_nat [OF p(1)] by arith
+    with pq * have False
+      by (simp add: nat_dvd_not_less)
+  }
   with n01 show ?ths by blast
 qed
 
-(* Variant for application, to separate the exponentiation.                  *)
+text \<open>Variant for application, to separate the exponentiation.\<close>
 lemma pocklington_alt:
-  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
-  and an: "[a^ (n - 1) = 1] (mod n)"
-  and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> (\<exists>b. [a^((n - 1) div p) = b] (mod n) \<and> coprime (b - 1) n)"
+  assumes n: "n \<ge> 2" and nqr: "n - 1 = q * r" and sqr: "n \<le> q\<^sup>2"
+    and an: "[a^ (n - 1) = 1] (mod n)"
+    and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> (\<exists>b. [a^((n - 1) div p) = b] (mod n) \<and> coprime (b - 1) n)"
   shows "prime n"
-proof-
-  {fix p assume p: "prime p" "p dvd q"
-    from aq[rule_format] p obtain b where
-      b: "[a^((n - 1) div p) = b] (mod n)" "coprime (b - 1) n" by blast
-    {assume a0: "a=0"
-      from n an have "[0 = 1] (mod n)" unfolding a0 power_0_left by auto
-      hence False using n by (simp add: cong_nat_def dvd_eq_mod_eq_0[symmetric])}
-    hence a0: "a\<noteq> 0" ..
-    hence a1: "a \<ge> 1" by arith
+proof -
+  {
+    fix p
+    assume p: "prime p" "p dvd q"
+    from aq[rule_format] p obtain b where b: "[a^((n - 1) div p) = b] (mod n)" "coprime (b - 1) n"
+      by blast
+    have a0: "a \<noteq> 0"
+    proof
+      assume a0: "a = 0"
+      from n an have "[0 = 1] (mod n)"
+        unfolding a0 power_0_left by auto
+      then show False
+        using n by (simp add: cong_nat_def dvd_eq_mod_eq_0[symmetric])
+    qed
+    then have a1: "a \<ge> 1" by arith
     from one_le_power[OF a1] have ath: "1 \<le> a ^ ((n - 1) div p)" .
-    {assume b0: "b = 0"
+    have b0: "b \<noteq> 0"
+    proof
+      assume b0: "b = 0"
       from p(2) nqr have "(n - 1) mod p = 0"
         by (metis mod_0 mod_mod_cancel mod_mult_self1_is_0)
       with div_mult_mod_eq[of "n - 1" p]
       have "(n - 1) div p * p= n - 1" by auto
-      hence eq: "(a^((n - 1) div p))^p = a^(n - 1)"
+      then have eq: "(a^((n - 1) div p))^p = a^(n - 1)"
         by (simp only: power_mult[symmetric])
-      have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
+      have "p - 1 \<noteq> 0"
+        using prime_ge_2_nat [OF p(1)] by arith
       then have pS: "Suc (p - 1) = p" by arith
-      from b have d: "n dvd a^((n - 1) div p)" unfolding b0
-        by auto
-      from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n
-      have False
-        by simp}
-    then have b0: "b \<noteq> 0" ..
-    hence b1: "b \<ge> 1" by arith 
-    from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]] 
-         ath b1 b nqr
+      from b have d: "n dvd a^((n - 1) div p)"
+        unfolding b0 by auto
+      from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n show False
+        by simp
+    qed
+    then have b1: "b \<ge> 1" by arith
+    from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]]
+      ath b1 b nqr
     have "coprime (a ^ ((n - 1) div p) - 1) n"
-      by simp}
-  hence th: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n "
+      by simp
+  }
+  then have "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n "
     by blast
-  from pocklington[OF n nqr sqr an th] show ?thesis .
+  then show ?thesis by (rule pocklington[OF n nqr sqr an])
 qed
 
 
-subsection\<open>Prime factorizations\<close>
+subsection \<open>Prime factorizations\<close>
 
 (* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
 
-definition "primefact ps n = (foldr op * ps 1 = n \<and> (\<forall>p\<in> set ps. prime p))"
+definition "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> (\<forall>p\<in> set ps. prime p)"
 
-lemma primefact: 
-  assumes n: "n \<noteq> (0::nat)"
+lemma primefact:
+  fixes n :: nat
+  assumes n: "n \<noteq> 0"
   shows "\<exists>ps. primefact ps n"
 proof -
-  have "\<exists>xs. mset xs = prime_factorization n" by (rule ex_mset)
-  then guess xs .. note xs = this
-  from assms have "n = prod_mset (prime_factorization n)" 
+  obtain xs where xs: "mset xs = prime_factorization n"
+    using ex_mset [of "prime_factorization n"] by blast
+  from assms have "n = prod_mset (prime_factorization n)"
     by (simp add: prod_mset_prime_factorization)
   also have "\<dots> = prod_mset (mset xs)" by (simp add: xs)
-  also have "\<dots> = foldr op * xs 1" by (induction xs) simp_all
+  also have "\<dots> = foldr op * xs 1" by (induct xs) simp_all
   finally have "foldr op * xs 1 = n" ..
-  moreover from xs have "\<forall>p\<in>#mset xs. prime p"
-    by auto
+  moreover from xs have "\<forall>p\<in>#mset xs. prime p" by auto
   ultimately have "primefact xs n" by (auto simp: primefact_def)
-  thus ?thesis ..
+  then show ?thesis ..
 qed
 
 lemma primefact_contains:
-  assumes pf: "primefact ps n" and p: "prime p" and pn: "p dvd n"
-  shows "(p::nat) \<in> set ps"
+  fixes p :: nat
+  assumes pf: "primefact ps n"
+    and p: "prime p"
+    and pn: "p dvd n"
+  shows "p \<in> set ps"
   using pf p pn
-proof(induct ps arbitrary: p n)
-  case Nil thus ?case by (auto simp add: primefact_def)
+proof (induct ps arbitrary: p n)
+  case Nil
+  then show ?case by (auto simp: primefact_def)
 next
-  case (Cons q qs p n)
+  case (Cons q qs)
   from Cons.prems[unfolded primefact_def]
-  have q: "prime q" "q * foldr op * qs 1 = n" "\<forall>p \<in>set qs. prime p"  and p: "prime p" "p dvd q * foldr op * qs 1" by simp_all
-  {assume "p dvd q"
-    with p(1) q(1) have "p = q" unfolding prime_nat_iff by auto
-    hence ?case by simp}
-  moreover
-  { assume h: "p dvd foldr op * qs 1"
+  have q: "prime q" "q * foldr op * qs 1 = n" "\<forall>p \<in>set qs. prime p"
+    and p: "prime p" "p dvd q * foldr op * qs 1"
+    by simp_all
+  consider "p dvd q" | "p dvd foldr op * qs 1"
+    by (metis p prime_dvd_mult_eq_nat)
+  then show ?case
+  proof cases
+    case 1
+    with p(1) q(1) have "p = q"
+      unfolding prime_nat_iff by auto
+    then show ?thesis by simp
+  next
+    case prem: 2
     from q(3) have pqs: "primefact qs (foldr op * qs 1)"
       by (simp add: primefact_def)
-    from Cons.hyps[OF pqs p(1) h] have ?case by simp}
-  ultimately show ?case
-    by (metis p prime_dvd_mult_eq_nat) 
+    from Cons.hyps[OF pqs p(1) prem] show ?thesis by simp
+  qed
 qed
 
 lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps"
   by (auto simp add: primefact_def list_all_iff)
 
-(* Variant of Lucas theorem.                                                 *)
-
+text \<open>Variant of Lucas theorem.\<close>
 lemma lucas_primefact:
   assumes n: "n \<ge> 2" and an: "[a^(n - 1) = 1] (mod n)"
-  and psn: "foldr op * ps 1 = n - 1"
-  and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps"
+    and psn: "foldr op * ps 1 = n - 1"
+    and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps"
   shows "prime n"
-proof-
-  {fix p assume p: "prime p" "p dvd n - 1" "[a ^ ((n - 1) div p) = 1] (mod n)"
+proof -
+  {
+    fix p
+    assume p: "prime p" "p dvd n - 1" "[a ^ ((n - 1) div p) = 1] (mod n)"
     from psn psp have psn1: "primefact ps (n - 1)"
       by (auto simp add: list_all_iff primefact_variant)
     from p(3) primefact_contains[OF psn1 p(1,2)] psp
-    have False by (induct ps, auto)}
+    have False by (induct ps) auto
+  }
   with lucas[OF n an] show ?thesis by blast
 qed
 
-(* Variant of Pocklington theorem.                                           *)
-
+text \<open>Variant of Pocklington theorem.\<close>
 lemma pocklington_primefact:
   assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2"
-  and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q"
-  and bqn: "(b^q) mod n = 1"
-  and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
+    and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q"
+    and bqn: "(b^q) mod n = 1"
+    and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
   shows "prime n"
-proof-
+proof -
   from bqn psp qrn
   have bqn: "a ^ (n - 1) mod n = 1"
-    and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps"  
-    unfolding arnb[symmetric] power_mod 
+    and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps"
+    unfolding arnb[symmetric] power_mod
     by (simp_all add: power_mult[symmetric] algebra_simps)
-  from n  have n0: "n > 0" by arith
+  from n have n0: "n > 0" by arith
   from div_mult_mod_eq[of "a^(n - 1)" n]
     mod_less_divisor[OF n0, of "a^(n - 1)"]
   have an1: "[a ^ (n - 1) = 1] (mod n)"
     by (metis bqn cong_nat_def mod_mod_trivial)
-  {fix p assume p: "prime p" "p dvd q"
+  have "coprime (a ^ ((n - 1) div p) - 1) n" if p: "prime p" "p dvd q" for p
+  proof -
     from psp psq have pfpsq: "primefact ps q"
       by (auto simp add: primefact_variant list_all_iff)
     from psp primefact_contains[OF pfpsq p]
     have p': "coprime (a ^ (r * (q div p)) mod n - 1) n"
       by (simp add: list_all_iff)
-    from p prime_nat_iff have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)" 
+    from p prime_nat_iff have p01: "p \<noteq> 0" "p \<noteq> 1" "p = Suc (p - 1)"
       by auto
     from div_mult1_eq[of r q p] p(2)
     have eq1: "r* (q div p) = (n - 1) div p"
       unfolding qrn[symmetric] dvd_eq_mod_eq_0 by (simp add: mult.commute)
-    have ath: "\<And>a (b::nat). a <= b \<Longrightarrow> a \<noteq> 0 ==> 1 <= a \<and> 1 <= b" by arith
-    {assume "a ^ ((n - 1) div p) mod n = 0"
-      then obtain s where s: "a ^ ((n - 1) div p) = n*s"
+    have ath: "a \<le> b \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> 1 \<le> a \<and> 1 \<le> b" for a b :: nat
+      by arith
+    {
+      assume "a ^ ((n - 1) div p) mod n = 0"
+      then obtain s where s: "a ^ ((n - 1) div p) = n * s"
         unfolding mod_eq_0_iff by blast
-      hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
-      from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto
-      from dvd_trans[OF p(2) qn1]
-      have npp: "(n - 1) div p * p = n - 1" by simp
-      with eq0 have "a^ (n - 1) = (n*s)^p"
+      then have eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
+      from qrn[symmetric] have qn1: "q dvd n - 1"
+        by (auto simp: dvd_def)
+      from dvd_trans[OF p(2) qn1] have npp: "(n - 1) div p * p = n - 1"
+        by simp
+      with eq0 have "a ^ (n - 1) = (n * s) ^ p"
         by (simp add: power_mult[symmetric])
-      hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp
+      with bqn p01 have "1 = (n * s)^(Suc (p - 1)) mod n"
+        by simp
       also have "\<dots> = 0" by (simp add: mult.assoc)
-      finally have False by simp }
-      then have th11: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto
-    have th1: "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)"
-      unfolding cong_nat_def by simp
-    from  th1   ath[OF mod_less_eq_dividend th11]
-    have th: "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)"
+      finally have False by simp
+    }
+    then have *: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto
+    have "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)"
+      by (simp add: cong_nat_def)
+    with ath[OF mod_less_eq_dividend *]
+    have "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)"
       by (metis cong_diff_nat cong_refl_nat)
-    have "coprime (a ^ ((n - 1) div p) - 1) n"
-      by (metis cong_imp_coprime_nat eq1 p' th) }
-  with pocklington[OF n qrn[symmetric] nq2 an1]
-  show ?thesis by blast
+    then show ?thesis
+      by (metis cong_imp_coprime_nat eq1 p')
+  qed
+  with pocklington[OF n qrn[symmetric] nq2 an1] show ?thesis
+    by blast
 qed
 
 end
diff -r cde6ceffcbc7 -r 7454317f883c src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Tue Aug 01 17:33:04 2017 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Tue Aug 01 22:19:37 2017 +0200
@@ -17,24 +17,26 @@
   Totient
 begin
 
-definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" where
-  "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))"
+definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool"
+  where "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))"
 
-definition Legendre :: "int \<Rightarrow> int \<Rightarrow> int" where
-  "Legendre a p = (if ([a = 0] (mod p)) then 0
-    else if QuadRes p a then 1
-    else -1)"
+definition Legendre :: "int \<Rightarrow> int \<Rightarrow> int"
+  where "Legendre a p =
+    (if ([a = 0] (mod p)) then 0
+     else if QuadRes p a then 1
+     else -1)"
+
 
 subsection \<open>A locale for residue rings\<close>
 
 definition residue_ring :: "int \<Rightarrow> int ring"
-where
-  "residue_ring m =
-    \<lparr>carrier = {0..m - 1},
-     monoid.mult = \<lambda>x y. (x * y) mod m,
-     one = 1,
-     zero = 0,
-     add = \<lambda>x y. (x + y) mod m\<rparr>"
+  where
+    "residue_ring m =
+      \<lparr>carrier = {0..m - 1},
+       monoid.mult = \<lambda>x y. (x * y) mod m,
+       one = 1,
+       zero = 0,
+       add = \<lambda>x y. (x + y) mod m\<rparr>"
 
 locale residues =
   fixes m :: int and R (structure)
@@ -88,37 +90,37 @@
 \<close>
 
 lemma res_carrier_eq: "carrier R = {0..m - 1}"
-  unfolding R_def residue_ring_def by auto
+  by (auto simp: R_def residue_ring_def)
 
 lemma res_add_eq: "x \<oplus> y = (x + y) mod m"
-  unfolding R_def residue_ring_def by auto
+  by (auto simp: R_def residue_ring_def)
 
 lemma res_mult_eq: "x \<otimes> y = (x * y) mod m"
-  unfolding R_def residue_ring_def by auto
+  by (auto simp: R_def residue_ring_def)
 
 lemma res_zero_eq: "\<zero> = 0"
-  unfolding R_def residue_ring_def by auto
+  by (auto simp: R_def residue_ring_def)
 
 lemma res_one_eq: "\<one> = 1"
-  unfolding R_def residue_ring_def units_of_def by auto
+  by (auto simp: R_def residue_ring_def units_of_def)
 
 lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
   using m_gt_one
   unfolding Units_def R_def residue_ring_def
   apply auto
-  apply (subgoal_tac "x \<noteq> 0")
-  apply auto
-  apply (metis invertible_coprime_int)
+    apply (subgoal_tac "x \<noteq> 0")
+     apply auto
+   apply (metis invertible_coprime_int)
   apply (subst (asm) coprime_iff_invertible'_int)
-  apply (auto simp add: cong_int_def mult.commute)
+   apply (auto simp add: cong_int_def mult.commute)
   done
 
 lemma res_neg_eq: "\<ominus> x = (- x) mod m"
   using m_gt_one unfolding R_def a_inv_def m_inv_def residue_ring_def
   apply simp
   apply (rule the_equality)
-  apply (simp add: mod_add_right_eq)
-  apply (simp add: add.commute mod_add_right_eq)
+   apply (simp add: mod_add_right_eq)
+   apply (simp add: add.commute mod_add_right_eq)
   apply (metis add.right_neutral minus_add_cancel mod_add_right_eq mod_pos_pos_trivial)
   done
 
@@ -139,18 +141,16 @@
   using insert m_gt_one by auto
 
 lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
-  unfolding R_def residue_ring_def
-  by (auto simp add: mod_simps)
+  by (auto simp: R_def residue_ring_def mod_simps)
 
 lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
-  unfolding R_def residue_ring_def
-  by (auto simp add: mod_simps)
+  by (auto simp: R_def residue_ring_def mod_simps)
 
 lemma zero_cong: "\<zero> = 0"
-  unfolding R_def residue_ring_def by auto
+  by (auto simp: R_def residue_ring_def)
 
 lemma one_cong: "\<one> = 1 mod m"
-  using m_gt_one unfolding R_def residue_ring_def by auto
+  using m_gt_one by (auto simp: R_def residue_ring_def)
 
 (* FIXME revise algebra library to use 1? *)
 lemma pow_cong: "(x mod m) (^) n = x^n mod m"
@@ -173,24 +173,26 @@
   assumes "1 < m" and "coprime a m"
   shows "a mod m \<in> Units R"
 proof (cases "a mod m = 0")
-  case True with assms show ?thesis
+  case True
+  with assms show ?thesis
     by (auto simp add: res_units_eq gcd_red_int [symmetric])
 next
   case False
   from assms have "0 < m" by simp
-  with pos_mod_sign [of m a] have "0 \<le> a mod m" .
+  then have "0 \<le> a mod m" by (rule pos_mod_sign [of m a])
   with False have "0 < a mod m" by simp
   with assms show ?thesis
     by (auto simp add: res_units_eq gcd_red_int [symmetric] ac_simps)
 qed
 
 lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)"
-  unfolding cong_int_def by auto
+  by (auto simp: cong_int_def)
 
 
 text \<open>Simplifying with these will translate a ring equation in R to a congruence.\<close>
-lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong
-    prod_cong sum_cong neg_cong res_eq_to_cong
+lemmas res_to_cong_simps =
+  add_cong mult_cong pow_cong one_cong
+  prod_cong sum_cong neg_cong res_eq_to_cong
 
 text \<open>Other useful facts about the residue ring.\<close>
 lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2"
@@ -220,11 +222,11 @@
 
 lemma is_field: "field R"
 proof -
-  have "\<And>x. \<lbrakk>gcd x (int p) \<noteq> 1; 0 \<le> x; x < int p\<rbrakk> \<Longrightarrow> x = 0"
+  have "gcd x (int p) \<noteq> 1 \<Longrightarrow> 0 \<le> x \<Longrightarrow> x < int p \<Longrightarrow> x = 0" for x
     by (metis dual_order.order_iff_strict gcd.commute less_le_not_le p_prime prime_imp_coprime prime_nat_int_transfer zdvd_imp_le)
   then show ?thesis
-  apply (intro cring.field_intro2 cring)
-  apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
+    apply (intro cring.field_intro2 cring)
+     apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
     done
 qed
 
@@ -245,23 +247,26 @@
 
 subsection \<open>Euler's theorem\<close>
 
-lemma (in residues) totient_eq:
-  "totient (nat m) = card (Units R)"
+lemma (in residues) totient_eq: "totient (nat m) = card (Units R)"
 proof -
   have *: "inj_on nat (Units R)"
     by (rule inj_onI) (auto simp add: res_units_eq)
   define m' where "m' = nat m"
-  from m_gt_one have m: "m = int m'" "m' > 1" by (simp_all add: m'_def)
-  from m have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
+  from m_gt_one have "m = int m'" "m' > 1"
+    by (simp_all add: m'_def)
+  then have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
     unfolding res_units_eq
     by (cases x; cases "x = m") (auto simp: totatives_def transfer_int_nat_gcd)
-  hence "Units R = int ` totatives m'" by blast
-  hence "totatives m' = nat ` Units R" by (simp add: image_image)
+  then have "Units R = int ` totatives m'"
+    by blast
+  then have "totatives m' = nat ` Units R"
+    by (simp add: image_image)
   then have "card (totatives (nat m)) = card (nat ` Units R)"
     by (simp add: m'_def)
   also have "\<dots> = card (Units R)"
     using * card_image [of nat "Units R"] by auto
-  finally show ?thesis by (simp add: totient_def)
+  finally show ?thesis
+    by (simp add: totient_def)
 qed
 
 lemma (in residues_prime) totient_eq: "totient p = p - 1"
@@ -324,26 +329,26 @@
   have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i\<in>\<Union>?Inverse_Pairs. i)"
     apply (subst UR)
     apply (subst finprod_Un_disjoint)
-    apply (auto intro: funcsetI)
+         apply (auto intro: funcsetI)
     using inv_one apply auto[1]
     using inv_eq_neg_one_eq apply auto
     done
   also have "(\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"
     apply (subst finprod_insert)
-    apply auto
+        apply auto
     apply (frule one_eq_neg_one)
     using a apply force
     done
   also have "(\<Otimes>i\<in>(\<Union>?Inverse_Pairs). i) = (\<Otimes>A\<in>?Inverse_Pairs. (\<Otimes>y\<in>A. y))"
     apply (subst finprod_Union_disjoint)
-    apply auto
-    apply (metis Units_inv_inv)+
+       apply auto
+     apply (metis Units_inv_inv)+
     done
   also have "\<dots> = \<one>"
     apply (rule finprod_one)
-    apply auto
+     apply auto
     apply (subst finprod_insert)
-    apply auto
+        apply auto
     apply (metis inv_eq_self)
     done
   finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>"
@@ -361,7 +366,7 @@
   finally have "fact (p - 1) mod p = \<ominus> \<one>" .
   then show ?thesis
     by (metis of_nat_fact Divides.transfer_int_nat_functions(2)
-      cong_int_def res_neg_eq res_one_eq)
+        cong_int_def res_neg_eq res_one_eq)
 qed
 
 lemma wilson_theorem:
@@ -380,13 +385,11 @@
 
 text \<open>
   This result can be transferred to the multiplicative group of
-  $\mathbb{Z}/p\mathbb{Z}$ for $p$ prime.\<close>
+  \<open>\<int>/p\<int>\<close> for \<open>p\<close> prime.\<close>
 
 lemma mod_nat_int_pow_eq:
   fixes n :: nat and p a :: int
-  assumes "a \<ge> 0" "p \<ge> 0"
-  shows "(nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
-  using assms
+  shows "a \<ge> 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow> (nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
   by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric])
 
 theorem residue_prime_mult_group_has_gen :
@@ -394,43 +397,55 @@
  assumes prime_p : "prime p"
  shows "\<exists>a \<in> {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \<in> UNIV}"
 proof -
-  have "p\<ge>2" using prime_gt_1_nat[OF prime_p] by simp
-  interpret R:residues_prime "p" "residue_ring p" unfolding residues_prime_def
-    by (simp add: prime_p)
-  have car: "carrier (residue_ring (int p)) - {\<zero>\<^bsub>residue_ring (int p)\<^esub>} =  {1 .. int p - 1}"
+  have "p \<ge> 2"
+    using prime_gt_1_nat[OF prime_p] by simp
+  interpret R: residues_prime p "residue_ring p"
+    by (simp add: residues_prime_def prime_p)
+  have car: "carrier (residue_ring (int p)) - {\<zero>\<^bsub>residue_ring (int p)\<^esub>} = {1 .. int p - 1}"
     by (auto simp add: R.zero_cong R.res_carrier_eq)
-  obtain a where a:"a \<in> {1 .. int p - 1}"
-         and a_gen:"{1 .. int p - 1} = {a(^)\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \<in> UNIV}"
-    apply atomize_elim using field.finite_field_mult_group_has_gen[OF R.is_field]
+
+  have "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)"
+    if "x \<in> {1 .. int p - 1}" for x and i :: nat
+    using that R.pow_cong[of x i] by auto
+  moreover
+  obtain a where a: "a \<in> {1 .. int p - 1}"
+    and a_gen: "{1 .. int p - 1} = {a(^)\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \<in> UNIV}"
+    using field.finite_field_mult_group_has_gen[OF R.is_field]
     by (auto simp add: car[symmetric] carrier_mult_of)
-  { fix x fix i :: nat assume x: "x \<in> {1 .. int p - 1}"
-    hence "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)" using R.pow_cong[of x i] by auto}
-  note * = this
-  have **:"nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
+  moreover
+  have "nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
   proof
-    { fix n assume n: "n \<in> ?L"
-      then have "n \<in> ?R" using \<open>p\<ge>2\<close> by force
-    } thus "?L \<subseteq> ?R" by blast
-    { fix n assume n: "n \<in> ?R"
-      then have "n \<in> ?L" using \<open>p\<ge>2\<close> Set_Interval.transfer_nat_int_set_functions(2) by fastforce
-    } thus "?R \<subseteq> ?L" by blast
+    have "n \<in> ?R" if "n \<in> ?L" for n
+      using that \<open>p\<ge>2\<close> by force
+    then show "?L \<subseteq> ?R" by blast
+    have "n \<in> ?L" if "n \<in> ?R" for n
+      using that \<open>p\<ge>2\<close> Set_Interval.transfer_nat_int_set_functions(2) by fastforce
+    then show "?R \<subseteq> ?L" by blast
   qed
+  moreover
   have "nat ` {a^i mod (int p) | i::nat. i \<in> UNIV} = {nat a^i mod p | i . i \<in> UNIV}" (is "?L = ?R")
   proof
-    { fix x assume x: "x \<in> ?L"
-      then obtain i where i:"x = nat (a^i mod (int p))" by blast
-      hence "x = nat a ^ i mod p" using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
-      hence "x \<in> ?R" using i by blast
-    } thus "?L \<subseteq> ?R" by blast
-    { fix x assume x: "x \<in> ?R"
-      then obtain i where i:"x = nat a^i mod p" by blast
-      hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
-    } thus "?R \<subseteq> ?L" by blast
+    have "x \<in> ?R" if "x \<in> ?L" for x
+    proof -
+      from that obtain i where i: "x = nat (a^i mod (int p))"
+        by blast
+      then have "x = nat a ^ i mod p"
+        using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
+      with i show ?thesis by blast
+    qed
+    then show "?L \<subseteq> ?R" by blast
+    have "x \<in> ?L" if "x \<in> ?R" for x
+    proof -
+      from that obtain i where i: "x = nat a^i mod p"
+        by blast
+      with mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> show ?thesis
+        by auto
+    qed
+    then show "?R \<subseteq> ?L" by blast
   qed
-  hence "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"
-    using * a a_gen ** by presburger
-  moreover
-  have "nat a \<in> {1 .. p - 1}" using a by force
+  ultimately have "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"
+    by presburger
+  moreover from a have "nat a \<in> {1 .. p - 1}" by force
   ultimately show ?thesis ..
 qed
 
diff -r cde6ceffcbc7 -r 7454317f883c src/HOL/Number_Theory/Totient.thy
--- a/src/HOL/Number_Theory/Totient.thy	Tue Aug 01 17:33:04 2017 +0200
+++ b/src/HOL/Number_Theory/Totient.thy	Tue Aug 01 22:19:37 2017 +0200
@@ -177,7 +177,7 @@
   
 lemma totient_less: 
   assumes "n > 1"
-  shows   "totient n < n"
+  shows "totient n < n"
 proof -
   from assms have "card (totatives n) \<le> card {0<..<n}"
     using totatives_less[of _ n] totatives_subset[of n] by (intro card_mono) auto