misc tuning and modernization;
authorwenzelm
Tue Aug 01 22:19:37 2017 +0200 (23 months ago)
changeset 663057454317f883c
parent 66304 cde6ceffcbc7
child 66306 13b051ebc6c5
child 66308 b6a0d95b94be
misc tuning and modernization;
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Number_Theory/Totient.thy
     1.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Tue Aug 01 17:33:04 2017 +0200
     1.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Tue Aug 01 22:19:37 2017 +0200
     1.3 @@ -8,186 +8,223 @@
     1.4  imports Residues
     1.5  begin
     1.6  
     1.7 -subsection\<open>Lemmas about previously defined terms\<close>
     1.8 +subsection \<open>Lemmas about previously defined terms\<close>
     1.9  
    1.10 -lemma prime_nat_iff'':
    1.11 -  "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
    1.12 +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)"
    1.13    unfolding prime_nat_iff
    1.14  proof safe
    1.15 -  fix m assume p: "p > 0" "p \<noteq> 1" and m: "m dvd p" "m \<noteq> p" 
    1.16 -           and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
    1.17 +  fix m
    1.18 +  assume p: "p > 0" "p \<noteq> 1"
    1.19 +    and m: "m dvd p" "m \<noteq> p"
    1.20 +    and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
    1.21    from p m have "m \<noteq> 0" by (intro notI) auto
    1.22    moreover from p m have "m < p" by (auto dest: dvd_imp_le)
    1.23 -  ultimately have "coprime p m" using * by blast
    1.24 +  ultimately have "coprime p m"
    1.25 +    using * by blast
    1.26    with m show "m = 1" by simp
    1.27 -qed (auto simp: prime_nat_iff simp del: One_nat_def 
    1.28 -          intro!: prime_imp_coprime dest: dvd_imp_le)
    1.29 +qed (auto simp: prime_nat_iff simp del: One_nat_def intro!: prime_imp_coprime dest: dvd_imp_le)
    1.30  
    1.31  lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
    1.32 -proof-
    1.33 +proof -
    1.34    have "{ m. 0 < m \<and> m < n } = {1..<n}" by auto
    1.35 -  thus ?thesis by simp
    1.36 +  then show ?thesis by simp
    1.37  qed
    1.38  
    1.39  
    1.40 -subsection\<open>Some basic theorems about solving congruences\<close>
    1.41 +subsection \<open>Some basic theorems about solving congruences\<close>
    1.42  
    1.43 -lemma cong_solve: 
    1.44 -  fixes n::nat assumes an: "coprime a n" shows "\<exists>x. [a * x = b] (mod n)"
    1.45 -proof-
    1.46 -  {assume "a=0" hence ?thesis using an by (simp add: cong_nat_def)}
    1.47 -  moreover
    1.48 -  {assume az: "a\<noteq>0"
    1.49 -  from bezout_add_strong_nat[OF az, of n]
    1.50 -  obtain d x y where dxy: "d dvd a" "d dvd n" "a*x = n*y + d" by blast
    1.51 +lemma cong_solve:
    1.52 +  fixes n :: nat
    1.53 +  assumes an: "coprime a n"
    1.54 +  shows "\<exists>x. [a * x = b] (mod n)"
    1.55 +proof (cases "a = 0")
    1.56 +  case True
    1.57 +  with an show ?thesis
    1.58 +    by (simp add: cong_nat_def)
    1.59 +next
    1.60 +  case False
    1.61 +  from bezout_add_strong_nat [OF this]
    1.62 +  obtain d x y where dxy: "d dvd a" "d dvd n" "a * x = n * y + d" by blast
    1.63    from dxy(1,2) have d1: "d = 1"
    1.64 -    by (metis assms coprime_nat) 
    1.65 -  hence "a*x*b = (n*y + 1)*b" using dxy(3) by simp
    1.66 -  hence "a*(x*b) = n*(y*b) + b" 
    1.67 -    by (auto simp add: algebra_simps)
    1.68 -  hence "a*(x*b) mod n = (n*(y*b) + b) mod n" by simp
    1.69 -  hence "a*(x*b) mod n = b mod n" by (simp add: mod_add_left_eq)
    1.70 -  hence "[a*(x*b) = b] (mod n)" unfolding cong_nat_def .
    1.71 -  hence ?thesis by blast}
    1.72 -ultimately  show ?thesis by blast
    1.73 +    by (metis assms coprime_nat)
    1.74 +  with dxy(3) have "a * x * b = (n * y + 1) * b"
    1.75 +    by simp
    1.76 +  then have "a * (x * b) = n * (y * b) + b"
    1.77 +    by (auto simp: algebra_simps)
    1.78 +  then have "a * (x * b) mod n = (n * (y * b) + b) mod n"
    1.79 +    by simp
    1.80 +  then have "a * (x * b) mod n = b mod n"
    1.81 +    by (simp add: mod_add_left_eq)
    1.82 +  then have "[a * (x * b) = b] (mod n)"
    1.83 +    by (simp only: cong_nat_def)
    1.84 +  then show ?thesis by blast
    1.85  qed
    1.86  
    1.87 -lemma cong_solve_unique: 
    1.88 -  fixes n::nat assumes an: "coprime a n" and nz: "n \<noteq> 0"
    1.89 +lemma cong_solve_unique:
    1.90 +  fixes n :: nat
    1.91 +  assumes an: "coprime a n" and nz: "n \<noteq> 0"
    1.92    shows "\<exists>!x. x < n \<and> [a * x = b] (mod n)"
    1.93 -proof-
    1.94 +proof -
    1.95 +  from cong_solve[OF an] obtain x where x: "[a * x = b] (mod n)"
    1.96 +    by blast
    1.97    let ?P = "\<lambda>x. x < n \<and> [a * x = b] (mod n)"
    1.98 -  from cong_solve[OF an] obtain x where x: "[a*x = b] (mod n)" by blast
    1.99    let ?x = "x mod n"
   1.100 -  from x have th: "[a * ?x = b] (mod n)"
   1.101 +  from x have *: "[a * ?x = b] (mod n)"
   1.102      by (simp add: cong_nat_def mod_mult_right_eq[of a x n])
   1.103 -  from mod_less_divisor[ of n x] nz th have Px: "?P ?x" by simp
   1.104 -  {fix y assume Py: "y < n" "[a * y = b] (mod n)"
   1.105 -    from Py(2) th have "[a * y = a*?x] (mod n)" by (simp add: cong_nat_def)
   1.106 -    hence "[y = ?x] (mod n)"
   1.107 -      by (metis an cong_mult_lcancel_nat) 
   1.108 +  from mod_less_divisor[ of n x] nz * have Px: "?P ?x" by simp
   1.109 +  have "y = ?x" if Py: "y < n" "[a * y = b] (mod n)" for y
   1.110 +  proof -
   1.111 +    from Py(2) * have "[a * y = a * ?x] (mod n)"
   1.112 +      by (simp add: cong_nat_def)
   1.113 +    then have "[y = ?x] (mod n)"
   1.114 +      by (metis an cong_mult_lcancel_nat)
   1.115      with mod_less[OF Py(1)] mod_less_divisor[ of n x] nz
   1.116 -    have "y = ?x" by (simp add: cong_nat_def)}
   1.117 +    show ?thesis
   1.118 +      by (simp add: cong_nat_def)
   1.119 +  qed
   1.120    with Px show ?thesis by blast
   1.121  qed
   1.122  
   1.123  lemma cong_solve_unique_nontrivial:
   1.124 -  assumes p: "prime (p::nat)" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p"
   1.125 +  fixes p :: nat
   1.126 +  assumes p: "prime p"
   1.127 +    and pa: "coprime p a"
   1.128 +    and x0: "0 < x"
   1.129 +    and xp: "x < p"
   1.130    shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
   1.131 -proof-
   1.132 +proof -
   1.133    from pa have ap: "coprime a p"
   1.134 -    by (metis gcd.commute) 
   1.135 -  have px:"coprime x p"
   1.136 +    by (metis gcd.commute)
   1.137 +  have px: "coprime x p"
   1.138      by (metis gcd.commute p prime_nat_iff'' x0 xp)
   1.139    obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y"
   1.140      by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
   1.141 -  {assume y0: "y = 0"
   1.142 -    with y(2) have th: "p dvd a"
   1.143 +  have "y \<noteq> 0"
   1.144 +  proof
   1.145 +    assume "y = 0"
   1.146 +    with y(2) have "p dvd a"
   1.147        by (auto dest: cong_dvd_eq_nat)
   1.148 -    have False
   1.149 -      by (metis gcd_nat.absorb1 not_prime_1 p pa th)}
   1.150 -  with y show ?thesis unfolding Ex1_def using neq0_conv by blast
   1.151 +    then show False
   1.152 +      by (metis gcd_nat.absorb1 not_prime_1 p pa)
   1.153 +  qed
   1.154 +  with y show ?thesis
   1.155 +    by blast
   1.156  qed
   1.157  
   1.158  lemma cong_unique_inverse_prime:
   1.159 -  assumes "prime (p::nat)" and "0 < x" and "x < p"
   1.160 +  fixes p :: nat
   1.161 +  assumes "prime p" and "0 < x" and "x < p"
   1.162    shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
   1.163 -  by (rule cong_solve_unique_nontrivial) (insert assms, simp_all)
   1.164 +  by (rule cong_solve_unique_nontrivial) (use assms in simp_all)
   1.165  
   1.166  lemma chinese_remainder_coprime_unique:
   1.167 -  fixes a::nat 
   1.168 +  fixes a :: nat
   1.169    assumes ab: "coprime a b" and az: "a \<noteq> 0" and bz: "b \<noteq> 0"
   1.170 -  and ma: "coprime m a" and nb: "coprime n b"
   1.171 +    and ma: "coprime m a" and nb: "coprime n b"
   1.172    shows "\<exists>!x. coprime x (a * b) \<and> x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
   1.173 -proof-
   1.174 +proof -
   1.175    let ?P = "\<lambda>x. x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
   1.176    from binary_chinese_remainder_unique_nat[OF ab az bz]
   1.177 -  obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)"
   1.178 -    "\<forall>y. ?P y \<longrightarrow> y = x" by blast
   1.179 -  from ma nb x
   1.180 -  have "coprime x a" "coprime x b"
   1.181 +  obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)" "\<forall>y. ?P y \<longrightarrow> y = x"
   1.182 +    by blast
   1.183 +  from ma nb x have "coprime x a" "coprime x b"
   1.184      by (metis cong_gcd_eq_nat)+
   1.185    then have "coprime x (a*b)"
   1.186      by (metis coprime_mul_eq)
   1.187 -  with x show ?thesis by blast
   1.188 +  with x show ?thesis
   1.189 +    by blast
   1.190  qed
   1.191  
   1.192  
   1.193 -subsection\<open>Lucas's theorem\<close>
   1.194 +subsection \<open>Lucas's theorem\<close>
   1.195  
   1.196  lemma lucas_coprime_lemma:
   1.197 -  fixes n::nat 
   1.198 -  assumes m: "m\<noteq>0" and am: "[a^m = 1] (mod n)"
   1.199 +  fixes n :: nat
   1.200 +  assumes m: "m \<noteq> 0" and am: "[a^m = 1] (mod n)"
   1.201    shows "coprime a n"
   1.202 -proof-
   1.203 -  {assume "n=1" hence ?thesis by simp}
   1.204 -  moreover
   1.205 -  {assume "n = 0" hence ?thesis using am m 
   1.206 -     by (metis am cong_0_nat gcd_nat.right_neutral power_eq_one_eq_nat)}
   1.207 -  moreover
   1.208 -  {assume n: "n\<noteq>0" "n\<noteq>1"
   1.209 -    from m obtain m' where m': "m = Suc m'" by (cases m, blast+)
   1.210 -    {fix d
   1.211 -      assume d: "d dvd a" "d dvd n"
   1.212 -      from n have n1: "1 < n" by arith
   1.213 -      from am mod_less[OF n1] have am1: "a^m mod n = 1" unfolding cong_nat_def by simp
   1.214 -      from dvd_mult2[OF d(1), of "a^m'"] have dam:"d dvd a^m" by (simp add: m')
   1.215 -      from dvd_mod_iff[OF d(2), of "a^m"] dam am1
   1.216 -      have "d = 1" by simp }
   1.217 -    hence ?thesis by auto
   1.218 -  }
   1.219 -  ultimately show ?thesis by blast
   1.220 +proof -
   1.221 +  consider "n = 1" | "n = 0" | "n > 1" by arith
   1.222 +  then show ?thesis
   1.223 +  proof cases
   1.224 +    case 1
   1.225 +    then show ?thesis by simp
   1.226 +  next
   1.227 +    case 2
   1.228 +    with am m show ?thesis
   1.229 +      by (metis am cong_0_nat gcd_nat.right_neutral power_eq_one_eq_nat)
   1.230 +  next
   1.231 +    case 3
   1.232 +    from m obtain m' where m': "m = Suc m'" by (cases m) blast+
   1.233 +    have "d = 1" if d: "d dvd a" "d dvd n" for d
   1.234 +    proof -
   1.235 +      from am mod_less[OF \<open>n > 1\<close>] have am1: "a^m mod n = 1"
   1.236 +        by (simp add: cong_nat_def)
   1.237 +      from dvd_mult2[OF d(1), of "a^m'"] have dam: "d dvd a^m"
   1.238 +        by (simp add: m')
   1.239 +      from dvd_mod_iff[OF d(2), of "a^m"] dam am1 show ?thesis
   1.240 +        by simp
   1.241 +    qed
   1.242 +    then show ?thesis by blast
   1.243 +  qed
   1.244  qed
   1.245  
   1.246  lemma lucas_weak:
   1.247 -  fixes n::nat 
   1.248 -  assumes n: "n \<ge> 2" and an: "[a ^ (n - 1) = 1] (mod n)"
   1.249 -  and nm: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)"
   1.250 +  fixes n :: nat
   1.251 +  assumes n: "n \<ge> 2"
   1.252 +    and an: "[a ^ (n - 1) = 1] (mod n)"
   1.253 +    and nm: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)"
   1.254    shows "prime n"
   1.255  proof (rule totient_imp_prime)
   1.256    show "totient n = n - 1"
   1.257    proof (rule ccontr)
   1.258      have "[a ^ totient n = 1] (mod n)"
   1.259 -      by (rule euler_theorem, rule lucas_coprime_lemma [of "n - 1"])
   1.260 -        (use n an in auto)
   1.261 +      by (rule euler_theorem, rule lucas_coprime_lemma [of "n - 1"]) (use n an in auto)
   1.262      moreover assume "totient n \<noteq> n - 1"
   1.263 -    then have "totient n > 0 \<and> totient n < n - 1"
   1.264 -      using \<open>n \<ge> 2\<close> and totient_less[of n] by simp
   1.265 +    then have "totient n > 0" "totient n < n - 1"
   1.266 +      using \<open>n \<ge> 2\<close> and totient_less[of n] by simp_all
   1.267      ultimately show False
   1.268        using nm by auto
   1.269    qed
   1.270 -qed (insert n, auto)
   1.271 +qed (use n in auto)
   1.272  
   1.273  lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"
   1.274    by (metis ex_least_nat_le not_less0)
   1.275  
   1.276 -lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> (P (Least P) \<and> (\<forall>m < (Least P). \<not> P m))"
   1.277 +lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> P (Least P) \<and> (\<forall>m < (Least P). \<not> P m)"
   1.278    (is "?lhs \<longleftrightarrow> ?rhs")
   1.279 -proof-
   1.280 -  {assume ?rhs hence ?lhs by blast}
   1.281 -  moreover
   1.282 -  { assume H: ?lhs then obtain n where n: "P n" by blast
   1.283 +proof
   1.284 +  show ?lhs if ?rhs
   1.285 +    using that by blast
   1.286 +  show ?rhs if ?lhs
   1.287 +  proof -
   1.288 +    from \<open>?lhs\<close> obtain n where n: "P n" by blast
   1.289      let ?x = "Least P"
   1.290 -    {fix m assume m: "m < ?x"
   1.291 -      from not_less_Least[OF m] have "\<not> P m" .}
   1.292 -    with LeastI_ex[OF H] have ?rhs by blast}
   1.293 -  ultimately show ?thesis by blast
   1.294 +    have "\<not> P m" if "m < ?x" for m
   1.295 +      by (rule not_less_Least[OF that])
   1.296 +    with LeastI_ex[OF \<open>?lhs\<close>] show ?thesis
   1.297 +      by blast
   1.298 +  qed
   1.299  qed
   1.300  
   1.301  theorem lucas:
   1.302    assumes n2: "n \<ge> 2" and an1: "[a^(n - 1) = 1] (mod n)"
   1.303 -  and pn: "\<forall>p. prime p \<and> p dvd n - 1 \<longrightarrow> [a^((n - 1) div p) \<noteq> 1] (mod n)"
   1.304 +    and pn: "\<forall>p. prime p \<and> p dvd n - 1 \<longrightarrow> [a^((n - 1) div p) \<noteq> 1] (mod n)"
   1.305    shows "prime n"
   1.306  proof-
   1.307 -  from n2 have n01: "n\<noteq>0" "n\<noteq>1" "n - 1 \<noteq> 0" by arith+
   1.308 -  from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1" by simp
   1.309 +  from n2 have n01: "n \<noteq> 0" "n \<noteq> 1" "n - 1 \<noteq> 0"
   1.310 +    by arith+
   1.311 +  from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1"
   1.312 +    by simp
   1.313    from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1
   1.314    have an: "coprime a n" "coprime (a^(n - 1)) n"
   1.315      by (auto simp add: coprime_exp gcd.commute)
   1.316 -  {assume H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
   1.317 +  have False if H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
   1.318 +  proof -
   1.319      from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
   1.320 -      m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k" by blast
   1.321 -    {assume nm1: "(n - 1) mod m > 0"
   1.322 +      m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k"
   1.323 +      by blast
   1.324 +    have False if nm1: "(n - 1) mod m > 0"
   1.325 +    proof -
   1.326        from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast
   1.327        let ?y = "a^ ((n - 1) div m * m)"
   1.328        note mdeq = div_mult_mod_eq[of "(n - 1)" m]
   1.329 @@ -199,53 +236,62 @@
   1.330          using power_mod[of "a^m" n "(n - 1) div m"] by simp
   1.331        also have "\<dots> = 1" using m(3)[unfolded cong_nat_def onen] onen
   1.332          by (metis power_one)
   1.333 -      finally have th3: "?y mod n = 1"  .
   1.334 -      have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
   1.335 +      finally have *: "?y mod n = 1"  .
   1.336 +      have **: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
   1.337          using an1[unfolded cong_nat_def onen] onen
   1.338            div_mult_mod_eq[of "(n - 1)" m, symmetric]
   1.339 -        by (simp add:power_add[symmetric] cong_nat_def th3 del: One_nat_def)
   1.340 -      have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)"
   1.341 -        by (metis cong_mult_rcancel_nat mult.commute th2 yn)
   1.342 -      from m(4)[rule_format, OF th0] nm1
   1.343 -        less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] th1
   1.344 -      have False by blast }
   1.345 -    hence "(n - 1) mod m = 0" by auto
   1.346 +        by (simp add:power_add[symmetric] cong_nat_def * del: One_nat_def)
   1.347 +      have "[a ^ ((n - 1) mod m) = 1] (mod n)"
   1.348 +        by (metis cong_mult_rcancel_nat mult.commute ** yn)
   1.349 +      with m(4)[rule_format, OF th0] nm1
   1.350 +        less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] show ?thesis
   1.351 +        by blast
   1.352 +    qed
   1.353 +    then have "(n - 1) mod m = 0" by auto
   1.354      then have mn: "m dvd n - 1" by presburger
   1.355 -    then obtain r where r: "n - 1 = m*r" unfolding dvd_def by blast
   1.356 -    from n01 r m(2) have r01: "r\<noteq>0" "r\<noteq>1" by - (rule ccontr, simp)+
   1.357 +    then obtain r where r: "n - 1 = m * r"
   1.358 +      unfolding dvd_def by blast
   1.359 +    from n01 r m(2) have r01: "r \<noteq> 0" "r \<noteq> 1" by auto
   1.360      obtain p where p: "prime p" "p dvd r"
   1.361        by (metis prime_factor_nat r01(2))
   1.362 -    hence th: "prime p \<and> p dvd n - 1" unfolding r by (auto intro: dvd_mult)
   1.363 -    have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r
   1.364 +    then have th: "prime p \<and> p dvd n - 1"
   1.365 +      unfolding r by (auto intro: dvd_mult)
   1.366 +    from r have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n"
   1.367        by (simp add: power_mult)
   1.368 -    also have "\<dots> = (a^(m*(r div p))) mod n" 
   1.369 -      using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] 
   1.370 -      by simp
   1.371 -    also have "\<dots> = ((a^m)^(r div p)) mod n" by (simp add: power_mult)
   1.372 -    also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod ..
   1.373 -    also have "\<dots> = 1" using m(3) onen by (simp add: cong_nat_def)
   1.374 +    also have "\<dots> = (a^(m*(r div p))) mod n"
   1.375 +      using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] by simp
   1.376 +    also have "\<dots> = ((a^m)^(r div p)) mod n"
   1.377 +      by (simp add: power_mult)
   1.378 +    also have "\<dots> = ((a^m mod n)^(r div p)) mod n"
   1.379 +      using power_mod ..
   1.380 +    also from m(3) onen have "\<dots> = 1"
   1.381 +      by (simp add: cong_nat_def)
   1.382      finally have "[(a ^ ((n - 1) div p))= 1] (mod n)"
   1.383        using onen by (simp add: cong_nat_def)
   1.384 -    with pn th have False by blast}
   1.385 -  hence th: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" by blast
   1.386 -  from lucas_weak[OF n2 an1 th] show ?thesis .
   1.387 +    with pn th show ?thesis by blast
   1.388 +  qed
   1.389 +  then have "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)"
   1.390 +    by blast
   1.391 +  then show ?thesis by (rule lucas_weak[OF n2 an1])
   1.392  qed
   1.393  
   1.394  
   1.395 -subsection\<open>Definition of the order of a number mod n (0 in non-coprime case)\<close>
   1.396 +subsection \<open>Definition of the order of a number mod n (0 in non-coprime case)\<close>
   1.397  
   1.398  definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)"
   1.399  
   1.400 -(* This has the expected properties.                                         *)
   1.401 +text \<open>This has the expected properties.\<close>
   1.402  
   1.403  lemma coprime_ord:
   1.404 -  fixes n::nat 
   1.405 +  fixes n::nat
   1.406    assumes "coprime n a"
   1.407    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))"
   1.408  proof-
   1.409    let ?P = "\<lambda>d. 0 < d \<and> [a ^ d = 1] (mod n)"
   1.410 -  from bigger_prime[of a] obtain p where p: "prime p" "a < p" by blast
   1.411 -  from assms have o: "ord n a = Least ?P" by (simp add: ord_def)
   1.412 +  from bigger_prime[of a] obtain p where p: "prime p" "a < p"
   1.413 +    by blast
   1.414 +  from assms have o: "ord n a = Least ?P"
   1.415 +    by (simp add: ord_def)
   1.416    have ex: "\<exists>m>0. ?P m"
   1.417    proof (cases "n \<ge> 2")
   1.418      case True
   1.419 @@ -266,136 +312,143 @@
   1.420      unfolding o[symmetric] by auto
   1.421  qed
   1.422  
   1.423 -(* With the special value 0 for non-coprime case, it's more convenient.      *)
   1.424 -lemma ord_works:
   1.425 -  fixes n::nat
   1.426 -  shows "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> ~[a^ m = 1] (mod n))"
   1.427 -apply (cases "coprime n a")
   1.428 -using coprime_ord[of n a]
   1.429 -by (auto simp add: ord_def cong_nat_def)
   1.430 +text \<open>With the special value \<open>0\<close> for non-coprime case, it's more convenient.\<close>
   1.431 +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))"
   1.432 +  for n :: nat
   1.433 +  by (cases "coprime n a") (use coprime_ord[of n a] in \<open>auto simp add: ord_def cong_nat_def\<close>)
   1.434  
   1.435 -lemma ord:
   1.436 -  fixes n::nat
   1.437 -  shows "[a^(ord n a) = 1] (mod n)" using ord_works by blast
   1.438 +lemma ord: "[a^(ord n a) = 1] (mod n)"
   1.439 +  for n :: nat
   1.440 +  using ord_works by blast
   1.441  
   1.442 -lemma ord_minimal:
   1.443 -  fixes n::nat
   1.444 -  shows "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> ~[a^m = 1] (mod n)"
   1.445 +lemma ord_minimal: "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> \<not> [a^m = 1] (mod n)"
   1.446 +  for n :: nat
   1.447    using ord_works by blast
   1.448  
   1.449 -lemma ord_eq_0:
   1.450 -  fixes n::nat
   1.451 -  shows "ord n a = 0 \<longleftrightarrow> ~coprime n a"
   1.452 -by (cases "coprime n a", simp add: coprime_ord, simp add: ord_def)
   1.453 +lemma ord_eq_0: "ord n a = 0 \<longleftrightarrow> \<not> coprime n a"
   1.454 +  for n :: nat
   1.455 +  by (cases "coprime n a") (simp add: coprime_ord, simp add: ord_def)
   1.456  
   1.457 -lemma divides_rexp: 
   1.458 -  "x dvd y \<Longrightarrow> (x::nat) dvd (y^(Suc n))" 
   1.459 +lemma divides_rexp: "x dvd y \<Longrightarrow> x dvd (y ^ Suc n)"
   1.460 +  for x y :: nat
   1.461    by (simp add: dvd_mult2[of x y])
   1.462  
   1.463 -lemma ord_divides:
   1.464 -  fixes n::nat
   1.465 -  shows "[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d" (is "?lhs \<longleftrightarrow> ?rhs")
   1.466 +lemma ord_divides:"[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d"
   1.467 +  (is "?lhs \<longleftrightarrow> ?rhs")
   1.468 +  for n :: nat
   1.469  proof
   1.470 -  assume rh: ?rhs
   1.471 -  then obtain k where "d = ord n a * k" unfolding dvd_def by blast
   1.472 -  hence "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)"
   1.473 +  assume ?rhs
   1.474 +  then obtain k where "d = ord n a * k"
   1.475 +    unfolding dvd_def by blast
   1.476 +  then have "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)"
   1.477      by (simp add : cong_nat_def power_mult power_mod)
   1.478    also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)"
   1.479      using ord[of a n, unfolded cong_nat_def]
   1.480      by (simp add: cong_nat_def power_mod)
   1.481 -  finally  show ?lhs .
   1.482 +  finally show ?lhs .
   1.483  next
   1.484 -  assume lh: ?lhs
   1.485 -  { assume H: "\<not> coprime n a"
   1.486 -    hence o: "ord n a = 0" by (simp add: ord_def)
   1.487 -    {assume d: "d=0" with o H have ?rhs by (simp add: cong_nat_def)}
   1.488 -    moreover
   1.489 -    {assume d0: "d\<noteq>0" then obtain d' where d': "d = Suc d'" by (cases d, auto)
   1.490 -      from H
   1.491 -      obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
   1.492 -      from lh
   1.493 -      obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2"
   1.494 -        by (metis H d0 gcd.commute lucas_coprime_lemma) 
   1.495 -      hence "a ^ d + n * q1 - n * q2 = 1" by simp
   1.496 -      with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2  d' p
   1.497 -      have "p dvd 1"
   1.498 +  assume ?lhs
   1.499 +  show ?rhs
   1.500 +  proof (cases "coprime n a")
   1.501 +    case prem: False
   1.502 +    then have o: "ord n a = 0" by (simp add: ord_def)
   1.503 +    show ?thesis
   1.504 +    proof (cases d)
   1.505 +      case 0
   1.506 +      with o prem show ?thesis by (simp add: cong_nat_def)
   1.507 +    next
   1.508 +      case (Suc d')
   1.509 +      then have d0: "d \<noteq> 0" by simp
   1.510 +      from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
   1.511 +      from \<open>?lhs\<close> obtain q1 q2 where q12: "a ^ d + n * q1 = 1 + n * q2"
   1.512 +        by (metis prem d0 gcd.commute lucas_coprime_lemma)
   1.513 +      then have "a ^ d + n * q1 - n * q2 = 1" by simp
   1.514 +      with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2 Suc p have "p dvd 1"
   1.515          by metis
   1.516        with p(3) have False by simp
   1.517 -      hence ?rhs ..}
   1.518 -    ultimately have ?rhs by blast}
   1.519 -  moreover
   1.520 -  {assume H: "coprime n a"
   1.521 +      then show ?thesis ..
   1.522 +    qed
   1.523 +  next
   1.524 +    case H: True
   1.525      let ?o = "ord n a"
   1.526      let ?q = "d div ord n a"
   1.527      let ?r = "d mod ord n a"
   1.528      have eqo: "[(a^?o)^?q = 1] (mod n)"
   1.529        by (metis cong_exp_nat ord power_one)
   1.530      from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
   1.531 -    hence op: "?o > 0" by simp
   1.532 -    from div_mult_mod_eq[of d "ord n a"] lh
   1.533 -    have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: cong_nat_def mult.commute)
   1.534 -    hence "[(a^?o)^?q * (a^?r) = 1] (mod n)"
   1.535 +    then have op: "?o > 0" by simp
   1.536 +    from div_mult_mod_eq[of d "ord n a"] \<open>?lhs\<close>
   1.537 +    have "[a^(?o*?q + ?r) = 1] (mod n)"
   1.538 +      by (simp add: cong_nat_def mult.commute)
   1.539 +    then have "[(a^?o)^?q * (a^?r) = 1] (mod n)"
   1.540        by (simp add: cong_nat_def power_mult[symmetric] power_add[symmetric])
   1.541 -    hence th: "[a^?r = 1] (mod n)"
   1.542 +    then have th: "[a^?r = 1] (mod n)"
   1.543        using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
   1.544 -      apply (simp add: cong_nat_def del: One_nat_def)
   1.545 -      by (metis mod_mult_left_eq nat_mult_1)
   1.546 -    {assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)}
   1.547 -    moreover
   1.548 -    {assume r: "?r \<noteq> 0"
   1.549 +      by (simp add: cong_nat_def del: One_nat_def) (metis mod_mult_left_eq nat_mult_1)
   1.550 +    show ?thesis
   1.551 +    proof (cases "?r = 0")
   1.552 +      case True
   1.553 +      then show ?thesis by (simp add: dvd_eq_mod_eq_0)
   1.554 +    next
   1.555 +      case False
   1.556        with mod_less_divisor[OF op, of d] have r0o:"?r >0 \<and> ?r < ?o" by simp
   1.557        from conjunct2[OF ord_works[of a n], rule_format, OF r0o] th
   1.558 -      have ?rhs by blast}
   1.559 -    ultimately have ?rhs by blast}
   1.560 -  ultimately  show ?rhs by blast
   1.561 +      show ?thesis by blast
   1.562 +    qed
   1.563 +  qed
   1.564  qed
   1.565  
   1.566 -lemma order_divides_totient:
   1.567 -  "ord n a dvd totient n" if "coprime n a"
   1.568 +lemma order_divides_totient: "ord n a dvd totient n" if "coprime n a"
   1.569    by (metis euler_theorem gcd.commute ord_divides that)
   1.570  
   1.571  lemma order_divides_expdiff:
   1.572    fixes n::nat and a::nat assumes na: "coprime n a"
   1.573    shows "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
   1.574 -proof-
   1.575 -  {fix n::nat and a::nat and d::nat and e::nat
   1.576 -    assume na: "coprime n a" and ed: "(e::nat) \<le> d"
   1.577 -    hence "\<exists>c. d = e + c" by presburger
   1.578 -    then obtain c where c: "d = e + c" by presburger
   1.579 +proof -
   1.580 +  have th: "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
   1.581 +    if na: "coprime n a" and ed: "(e::nat) \<le> d"
   1.582 +    for n a d e :: nat
   1.583 +  proof -
   1.584 +    from na ed have "\<exists>c. d = e + c" by presburger
   1.585 +    then obtain c where c: "d = e + c" ..
   1.586      from na have an: "coprime a n"
   1.587        by (metis gcd.commute)
   1.588      have aen: "coprime (a^e) n"
   1.589 -      by (metis coprime_exp gcd.commute na)      
   1.590 +      by (metis coprime_exp gcd.commute na)
   1.591      have acn: "coprime (a^c) n"
   1.592 -      by (metis coprime_exp gcd.commute na) 
   1.593 -    have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
   1.594 -      using c by simp
   1.595 +      by (metis coprime_exp gcd.commute na)
   1.596 +    from c have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
   1.597 +      by simp
   1.598      also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
   1.599      also have  "\<dots> \<longleftrightarrow> [a ^ c = 1] (mod n)"
   1.600        using cong_mult_lcancel_nat [OF aen, of "a^c" "a^0"] by simp
   1.601 -    also  have "\<dots> \<longleftrightarrow> ord n a dvd c" by (simp only: ord_divides)
   1.602 +    also have "\<dots> \<longleftrightarrow> ord n a dvd c"
   1.603 +      by (simp only: ord_divides)
   1.604      also have "\<dots> \<longleftrightarrow> [e + c = e + 0] (mod ord n a)"
   1.605 -      using cong_add_lcancel_nat 
   1.606 +      using cong_add_lcancel_nat
   1.607        by (metis cong_dvd_eq_nat dvd_0_right cong_dvd_modulus_nat cong_mult_self_nat nat_mult_1)
   1.608 -    finally have "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
   1.609 -      using c by simp }
   1.610 -  note th = this
   1.611 -  have "e \<le> d \<or> d \<le> e" by arith
   1.612 -  moreover
   1.613 -  {assume ed: "e \<le> d" from th[OF na ed] have ?thesis .}
   1.614 -  moreover
   1.615 -  {assume de: "d \<le> e"
   1.616 -    from th[OF na de] have ?thesis
   1.617 -    by (metis cong_sym_nat)}
   1.618 -  ultimately show ?thesis by blast
   1.619 +    finally show ?thesis
   1.620 +      using c by simp
   1.621 +  qed
   1.622 +  consider "e \<le> d" | "d \<le> e" by arith
   1.623 +  then show ?thesis
   1.624 +  proof cases
   1.625 +    case 1
   1.626 +    with na show ?thesis by (rule th)
   1.627 +  next
   1.628 +    case 2
   1.629 +    from th[OF na this] show ?thesis
   1.630 +      by (metis cong_sym_nat)
   1.631 +  qed
   1.632  qed
   1.633  
   1.634 -subsection\<open>Another trivial primality characterization\<close>
   1.635 +
   1.636 +subsection \<open>Another trivial primality characterization\<close>
   1.637  
   1.638 -lemma prime_prime_factor:
   1.639 -  "prime (n::nat) \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)" 
   1.640 +lemma prime_prime_factor: "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)"
   1.641    (is "?lhs \<longleftrightarrow> ?rhs")
   1.642 -proof (cases "n=0 \<or> n=1")
   1.643 +  for n :: nat
   1.644 +proof (cases "n = 0 \<or> n = 1")
   1.645    case True
   1.646    then show ?thesis
   1.647       by (metis bigger_prime dvd_0_right not_prime_1 not_prime_0)
   1.648 @@ -405,7 +458,7 @@
   1.649    proof
   1.650      assume "prime n"
   1.651      then show ?rhs
   1.652 -      by (metis  not_prime_1 prime_nat_iff)
   1.653 +      by (metis not_prime_1 prime_nat_iff)
   1.654    next
   1.655      assume ?rhs
   1.656      with False show "prime n"
   1.657 @@ -413,322 +466,402 @@
   1.658    qed
   1.659  qed
   1.660  
   1.661 -lemma prime_divisor_sqrt:
   1.662 -  "prime (n::nat) \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
   1.663 +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)"
   1.664 +  for n :: nat
   1.665  proof -
   1.666 -  {assume "n=0 \<or> n=1" hence ?thesis
   1.667 -    by auto}
   1.668 -  moreover
   1.669 -  {assume n: "n\<noteq>0" "n\<noteq>1"
   1.670 -    hence np: "n > 1" by arith
   1.671 -    {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"
   1.672 -      from H d have d1n: "d = 1 \<or> d=n" by blast
   1.673 -      {assume dn: "d=n"
   1.674 -        have "n\<^sup>2 > n*1" using n by (simp add: power2_eq_square)
   1.675 -        with dn d(2) have "d=1" by simp}
   1.676 -      with d1n have "d = 1" by blast  }
   1.677 +  consider "n = 0" | "n = 1" | "n \<noteq> 0" "n \<noteq> 1" by blast
   1.678 +  then show ?thesis
   1.679 +  proof cases
   1.680 +    case 1
   1.681 +    then show ?thesis by simp
   1.682 +  next
   1.683 +    case 2
   1.684 +    then show ?thesis by simp
   1.685 +  next
   1.686 +    case n: 3
   1.687 +    then have np: "n > 1" by arith
   1.688 +    {
   1.689 +      fix d
   1.690 +      assume d: "d dvd n" "d\<^sup>2 \<le> n"
   1.691 +        and H: "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
   1.692 +      from H d have d1n: "d = 1 \<or> d = n" by blast
   1.693 +      then have "d = 1"
   1.694 +      proof
   1.695 +        assume dn: "d = n"
   1.696 +        from n have "n\<^sup>2 > n * 1"
   1.697 +          by (simp add: power2_eq_square)
   1.698 +        with dn d(2) show ?thesis by simp
   1.699 +      qed
   1.700 +    }
   1.701      moreover
   1.702 -    {fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1"
   1.703 +    {
   1.704 +      fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1"
   1.705        from d n have "d \<noteq> 0"
   1.706          by (metis dvd_0_left_iff)
   1.707 -      hence dp: "d > 0" by simp
   1.708 +      then have dp: "d > 0" by simp
   1.709        from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast
   1.710        from n dp e have ep:"e > 0" by simp
   1.711 -      have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n" using dp ep
   1.712 +      from dp ep have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n"
   1.713          by (auto simp add: e power2_eq_square mult_le_cancel_left)
   1.714 -      moreover
   1.715 -      {assume h: "d\<^sup>2 \<le> n"
   1.716 -        from H[rule_format, of d] h d have "d = 1" by blast}
   1.717 -      moreover
   1.718 -      {assume h: "e\<^sup>2 \<le> n"
   1.719 -        from e have "e dvd n" unfolding dvd_def by (simp add: mult.commute)
   1.720 -        with H[rule_format, of e] h have "e=1" by simp
   1.721 -        with e have "d = n" by simp}
   1.722 -      ultimately have "d=1 \<or> d=n"  by blast}
   1.723 -    ultimately have ?thesis unfolding prime_nat_iff using np n(2) by blast}
   1.724 -  ultimately show ?thesis by auto
   1.725 +      then have "d = 1 \<or> d = n"
   1.726 +      proof
   1.727 +        assume "d\<^sup>2 \<le> n"
   1.728 +        with H[rule_format, of d] d have "d = 1" by blast
   1.729 +        then show ?thesis ..
   1.730 +      next
   1.731 +        assume h: "e\<^sup>2 \<le> n"
   1.732 +        from e have "e dvd n" by (simp add: dvd_def mult.commute)
   1.733 +        with H[rule_format, of e] h have "e = 1" by simp
   1.734 +        with e have "d = n" by simp
   1.735 +        then show ?thesis ..
   1.736 +      qed
   1.737 +    }
   1.738 +    ultimately show ?thesis
   1.739 +      unfolding prime_nat_iff using np n(2) by blast
   1.740 +  qed
   1.741  qed
   1.742  
   1.743  lemma prime_prime_factor_sqrt:
   1.744 -  "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)"
   1.745 +  "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)"
   1.746    (is "?lhs \<longleftrightarrow>?rhs")
   1.747 -proof-
   1.748 -  {assume "n=0 \<or> n=1" 
   1.749 -   hence ?thesis
   1.750 -     by (metis not_prime_0 not_prime_1)}
   1.751 -  moreover
   1.752 -  {assume n: "n\<noteq>0" "n\<noteq>1"
   1.753 -    {assume H: ?lhs
   1.754 -      from H[unfolded prime_divisor_sqrt] n
   1.755 -      have ?rhs
   1.756 -        by (metis prime_prime_factor) }
   1.757 -    moreover
   1.758 -    {assume H: ?rhs
   1.759 -      {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1"
   1.760 +proof -
   1.761 +  consider "n = 0" | "n = 1" | "n \<noteq> 0" "n \<noteq> 1"
   1.762 +    by blast
   1.763 +  then show ?thesis
   1.764 +  proof cases
   1.765 +    case 1
   1.766 +    then show ?thesis by (metis not_prime_0)
   1.767 +  next
   1.768 +    case 2
   1.769 +    then show ?thesis by (metis not_prime_1)
   1.770 +  next
   1.771 +    case n: 3
   1.772 +    show ?thesis
   1.773 +    proof
   1.774 +      assume ?lhs
   1.775 +      from this[unfolded prime_divisor_sqrt] n show ?rhs
   1.776 +        by (metis prime_prime_factor)
   1.777 +    next
   1.778 +      assume ?rhs
   1.779 +      {
   1.780 +        fix d
   1.781 +        assume d: "d dvd n" "d\<^sup>2 \<le> n" "d \<noteq> 1"
   1.782          then obtain p where p: "prime p" "p dvd d"
   1.783 -          by (metis prime_factor_nat) 
   1.784 +          by (metis prime_factor_nat)
   1.785          from d(1) n have dp: "d > 0"
   1.786 -          by (metis dvd_0_left neq0_conv) 
   1.787 +          by (metis dvd_0_left neq0_conv)
   1.788          from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)
   1.789          have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith
   1.790 -        with H n p(1) dvd_trans[OF p(2) d(1)] have False  by blast}
   1.791 -      with n prime_divisor_sqrt  have ?lhs by auto}
   1.792 -    ultimately have ?thesis by blast }
   1.793 -  ultimately show ?thesis by (cases "n=0 \<or> n=1", auto)
   1.794 +        with \<open>?rhs\<close> n p(1) dvd_trans[OF p(2) d(1)] have False
   1.795 +          by blast
   1.796 +      }
   1.797 +      with n prime_divisor_sqrt show ?lhs by auto
   1.798 +    qed
   1.799 +  qed
   1.800  qed
   1.801  
   1.802  
   1.803 -subsection\<open>Pocklington theorem\<close>
   1.804 +subsection \<open>Pocklington theorem\<close>
   1.805  
   1.806  lemma pocklington_lemma:
   1.807 -  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and an: "[a^ (n - 1) = 1] (mod n)"
   1.808 -  and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
   1.809 -  and pp: "prime (p::nat)" and pn: "p dvd n"
   1.810 +  fixes p :: nat
   1.811 +  assumes n: "n \<ge> 2" and nqr: "n - 1 = q * r"
   1.812 +    and an: "[a^ (n - 1) = 1] (mod n)"
   1.813 +    and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n"
   1.814 +    and pp: "prime p" and pn: "p dvd n"
   1.815    shows "[p = 1] (mod q)"
   1.816  proof -
   1.817 -  have p01: "p \<noteq> 0" "p \<noteq> 1" using pp by (auto intro: prime_gt_0_nat)
   1.818 -  obtain k where k: "a ^ (q * r) - 1 = n*k"
   1.819 +  have p01: "p \<noteq> 0" "p \<noteq> 1"
   1.820 +    using pp by (auto intro: prime_gt_0_nat)
   1.821 +  obtain k where k: "a ^ (q * r) - 1 = n * k"
   1.822      by (metis an cong_to_1_nat dvd_def nqr)
   1.823 -  from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast
   1.824 -  {assume a0: "a = 0"
   1.825 -    hence "a^ (n - 1) = 0" using n by (simp add: power_0_left)
   1.826 -    with n an mod_less[of 1 n]  have False by (simp add: power_0_left cong_nat_def)}
   1.827 -  hence a0: "a\<noteq>0" ..
   1.828 -  from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp
   1.829 -  hence "(a ^ (q * r) - 1) + 1  = a ^ (q * r)" by simp
   1.830 -  with k l have "a ^ (q * r) = p*l*k + 1" by simp
   1.831 -  hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: ac_simps)
   1.832 -  hence odq: "ord p (a^r) dvd q"
   1.833 +  from pn[unfolded dvd_def] obtain l where l: "n = p * l"
   1.834 +    by blast
   1.835 +  have a0: "a \<noteq> 0"
   1.836 +  proof
   1.837 +    assume "a = 0"
   1.838 +    with n have "a^ (n - 1) = 0"
   1.839 +      by (simp add: power_0_left)
   1.840 +    with n an mod_less[of 1 n] show False
   1.841 +      by (simp add: power_0_left cong_nat_def)
   1.842 +  qed
   1.843 +  with n nqr have aqr0: "a ^ (q * r) \<noteq> 0"
   1.844 +    by simp
   1.845 +  then have "(a ^ (q * r) - 1) + 1  = a ^ (q * r)"
   1.846 +    by simp
   1.847 +  with k l have "a ^ (q * r) = p * l * k + 1"
   1.848 +    by simp
   1.849 +  then have "a ^ (r * q) + p * 0 = 1 + p * (l * k)"
   1.850 +    by (simp add: ac_simps)
   1.851 +  then have odq: "ord p (a^r) dvd q"
   1.852      unfolding ord_divides[symmetric] power_mult[symmetric]
   1.853 -    by (metis an cong_dvd_modulus_nat mult.commute nqr pn) 
   1.854 -  from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d" by blast
   1.855 -  {assume d1: "d \<noteq> 1"
   1.856 +    by (metis an cong_dvd_modulus_nat mult.commute nqr pn)
   1.857 +  from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d"
   1.858 +    by blast
   1.859 +  have d1: "d = 1"
   1.860 +  proof (rule ccontr)
   1.861 +    assume d1: "d \<noteq> 1"
   1.862      obtain P where P: "prime P" "P dvd d"
   1.863 -      by (metis d1 prime_factor_nat) 
   1.864 +      by (metis d1 prime_factor_nat)
   1.865      from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp
   1.866      from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast
   1.867      from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast
   1.868 -    have P0: "P \<noteq> 0" using P(1)
   1.869 -      by (metis not_prime_0) 
   1.870 +    from P(1) have P0: "P \<noteq> 0"
   1.871 +      by (metis not_prime_0)
   1.872      from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast
   1.873      from d s t P0  have s': "ord p (a^r) * t = s"
   1.874 -      by (metis mult.commute mult_cancel1 mult.assoc) 
   1.875 +      by (metis mult.commute mult_cancel1 mult.assoc)
   1.876      have "ord p (a^r) * t*r = r * ord p (a^r) * t"
   1.877        by (metis mult.assoc mult.commute)
   1.878 -    hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"
   1.879 +    then have exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"
   1.880        by (simp only: power_mult)
   1.881 -    then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"
   1.882 +    then have "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"
   1.883        by (metis cong_exp_nat ord power_one)
   1.884 -    have pd0: "p dvd a^(ord p (a^r) * t*r) - 1"
   1.885 -      by (metis cong_to_1_nat exps th)
   1.886 -    from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" using P0 by simp
   1.887 +    then have pd0: "p dvd a^(ord p (a^r) * t*r) - 1"
   1.888 +      by (metis cong_to_1_nat exps)
   1.889 +    from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r"
   1.890 +      using P0 by simp
   1.891      with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp
   1.892 -    with p01 pn pd0 coprime_common_divisor_nat have False 
   1.893 -      by auto}
   1.894 -  hence d1: "d = 1" by blast
   1.895 -  hence o: "ord p (a^r) = q" using d by simp
   1.896 -  from pp totient_prime [of p]
   1.897 -  have totient_eq: "totient p = p - 1" by simp
   1.898 -  {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
   1.899 +    with p01 pn pd0 coprime_common_divisor_nat show False
   1.900 +      by auto
   1.901 +  qed
   1.902 +  with d have o: "ord p (a^r) = q" by simp
   1.903 +  from pp totient_prime [of p] have totient_eq: "totient p = p - 1"
   1.904 +    by simp
   1.905 +  {
   1.906 +    fix d
   1.907 +    assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
   1.908      from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast
   1.909      from n have "n \<noteq> 0" by simp
   1.910      then have False using d dp pn
   1.911 -      by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)} 
   1.912 -  hence cpa: "coprime p a" by auto
   1.913 +      by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)
   1.914 +  }
   1.915 +  then have cpa: "coprime p a" by auto
   1.916    have arp: "coprime (a^r) p"
   1.917 -    by (metis coprime_exp cpa gcd.commute) 
   1.918 -  from euler_theorem [OF arp, simplified ord_divides] o totient_eq
   1.919 -  have "q dvd (p - 1)" by simp
   1.920 -  then obtain d where d:"p - 1 = q * d" 
   1.921 +    by (metis coprime_exp cpa gcd.commute)
   1.922 +  from euler_theorem [OF arp, simplified ord_divides] o totient_eq have "q dvd (p - 1)"
   1.923 +    by simp
   1.924 +  then obtain d where d:"p - 1 = q * d"
   1.925      unfolding dvd_def by blast
   1.926 -  have p0:"p \<noteq> 0"
   1.927 -    by (metis p01(1)) 
   1.928 -  from p0 d have "p + q * 0 = 1 + q * d" by simp
   1.929 +  have "p \<noteq> 0"
   1.930 +    by (metis p01(1))
   1.931 +  with d have "p + q * 0 = 1 + q * d" by simp
   1.932    then show ?thesis
   1.933      by (metis cong_iff_lin_nat mult.commute)
   1.934  qed
   1.935  
   1.936  theorem pocklington:
   1.937 -  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
   1.938 -  and an: "[a^ (n - 1) = 1] (mod n)"
   1.939 -  and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
   1.940 +  assumes n: "n \<ge> 2" and nqr: "n - 1 = q * r" and sqr: "n \<le> q\<^sup>2"
   1.941 +    and an: "[a^ (n - 1) = 1] (mod n)"
   1.942 +    and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
   1.943    shows "prime n"
   1.944 -unfolding prime_prime_factor_sqrt[of n]
   1.945 -proof-
   1.946 -  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)"
   1.947 -  from n have n01: "n\<noteq>0" "n\<noteq>1" by arith+
   1.948 -  {fix p assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n"
   1.949 -    from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)" by (simp add: power2_eq_square)
   1.950 -    hence pq: "p \<le> q"
   1.951 -      by (metis le0 power_le_imp_le_base) 
   1.952 -    from pocklington_lemma[OF n nqr an aq p(1,2)] 
   1.953 -    have th: "q dvd p - 1"
   1.954 -      by (metis cong_to_1_nat) 
   1.955 -    have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
   1.956 -    with pq th have False
   1.957 -      by (simp add: nat_dvd_not_less)}
   1.958 +  unfolding prime_prime_factor_sqrt[of n]
   1.959 +proof -
   1.960 +  let ?ths = "n \<noteq> 0 \<and> n \<noteq> 1 \<and> (\<nexists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
   1.961 +  from n have n01: "n \<noteq> 0" "n \<noteq> 1" by arith+
   1.962 +  {
   1.963 +    fix p
   1.964 +    assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n"
   1.965 +    from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)"
   1.966 +      by (simp add: power2_eq_square)
   1.967 +    then have pq: "p \<le> q"
   1.968 +      by (metis le0 power_le_imp_le_base)
   1.969 +    from pocklington_lemma[OF n nqr an aq p(1,2)] have *: "q dvd p - 1"
   1.970 +      by (metis cong_to_1_nat)
   1.971 +    have "p - 1 \<noteq> 0"
   1.972 +      using prime_ge_2_nat [OF p(1)] by arith
   1.973 +    with pq * have False
   1.974 +      by (simp add: nat_dvd_not_less)
   1.975 +  }
   1.976    with n01 show ?ths by blast
   1.977  qed
   1.978  
   1.979 -(* Variant for application, to separate the exponentiation.                  *)
   1.980 +text \<open>Variant for application, to separate the exponentiation.\<close>
   1.981  lemma pocklington_alt:
   1.982 -  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
   1.983 -  and an: "[a^ (n - 1) = 1] (mod n)"
   1.984 -  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)"
   1.985 +  assumes n: "n \<ge> 2" and nqr: "n - 1 = q * r" and sqr: "n \<le> q\<^sup>2"
   1.986 +    and an: "[a^ (n - 1) = 1] (mod n)"
   1.987 +    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)"
   1.988    shows "prime n"
   1.989 -proof-
   1.990 -  {fix p assume p: "prime p" "p dvd q"
   1.991 -    from aq[rule_format] p obtain b where
   1.992 -      b: "[a^((n - 1) div p) = b] (mod n)" "coprime (b - 1) n" by blast
   1.993 -    {assume a0: "a=0"
   1.994 -      from n an have "[0 = 1] (mod n)" unfolding a0 power_0_left by auto
   1.995 -      hence False using n by (simp add: cong_nat_def dvd_eq_mod_eq_0[symmetric])}
   1.996 -    hence a0: "a\<noteq> 0" ..
   1.997 -    hence a1: "a \<ge> 1" by arith
   1.998 +proof -
   1.999 +  {
  1.1000 +    fix p
  1.1001 +    assume p: "prime p" "p dvd q"
  1.1002 +    from aq[rule_format] p obtain b where b: "[a^((n - 1) div p) = b] (mod n)" "coprime (b - 1) n"
  1.1003 +      by blast
  1.1004 +    have a0: "a \<noteq> 0"
  1.1005 +    proof
  1.1006 +      assume a0: "a = 0"
  1.1007 +      from n an have "[0 = 1] (mod n)"
  1.1008 +        unfolding a0 power_0_left by auto
  1.1009 +      then show False
  1.1010 +        using n by (simp add: cong_nat_def dvd_eq_mod_eq_0[symmetric])
  1.1011 +    qed
  1.1012 +    then have a1: "a \<ge> 1" by arith
  1.1013      from one_le_power[OF a1] have ath: "1 \<le> a ^ ((n - 1) div p)" .
  1.1014 -    {assume b0: "b = 0"
  1.1015 +    have b0: "b \<noteq> 0"
  1.1016 +    proof
  1.1017 +      assume b0: "b = 0"
  1.1018        from p(2) nqr have "(n - 1) mod p = 0"
  1.1019          by (metis mod_0 mod_mod_cancel mod_mult_self1_is_0)
  1.1020        with div_mult_mod_eq[of "n - 1" p]
  1.1021        have "(n - 1) div p * p= n - 1" by auto
  1.1022 -      hence eq: "(a^((n - 1) div p))^p = a^(n - 1)"
  1.1023 +      then have eq: "(a^((n - 1) div p))^p = a^(n - 1)"
  1.1024          by (simp only: power_mult[symmetric])
  1.1025 -      have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
  1.1026 +      have "p - 1 \<noteq> 0"
  1.1027 +        using prime_ge_2_nat [OF p(1)] by arith
  1.1028        then have pS: "Suc (p - 1) = p" by arith
  1.1029 -      from b have d: "n dvd a^((n - 1) div p)" unfolding b0
  1.1030 -        by auto
  1.1031 -      from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n
  1.1032 -      have False
  1.1033 -        by simp}
  1.1034 -    then have b0: "b \<noteq> 0" ..
  1.1035 -    hence b1: "b \<ge> 1" by arith 
  1.1036 -    from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]] 
  1.1037 -         ath b1 b nqr
  1.1038 +      from b have d: "n dvd a^((n - 1) div p)"
  1.1039 +        unfolding b0 by auto
  1.1040 +      from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n show False
  1.1041 +        by simp
  1.1042 +    qed
  1.1043 +    then have b1: "b \<ge> 1" by arith
  1.1044 +    from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]]
  1.1045 +      ath b1 b nqr
  1.1046      have "coprime (a ^ ((n - 1) div p) - 1) n"
  1.1047 -      by simp}
  1.1048 -  hence th: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n "
  1.1049 +      by simp
  1.1050 +  }
  1.1051 +  then have "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n "
  1.1052      by blast
  1.1053 -  from pocklington[OF n nqr sqr an th] show ?thesis .
  1.1054 +  then show ?thesis by (rule pocklington[OF n nqr sqr an])
  1.1055  qed
  1.1056  
  1.1057  
  1.1058 -subsection\<open>Prime factorizations\<close>
  1.1059 +subsection \<open>Prime factorizations\<close>
  1.1060  
  1.1061  (* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
  1.1062  
  1.1063 -definition "primefact ps n = (foldr op * ps 1 = n \<and> (\<forall>p\<in> set ps. prime p))"
  1.1064 +definition "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> (\<forall>p\<in> set ps. prime p)"
  1.1065  
  1.1066 -lemma primefact: 
  1.1067 -  assumes n: "n \<noteq> (0::nat)"
  1.1068 +lemma primefact:
  1.1069 +  fixes n :: nat
  1.1070 +  assumes n: "n \<noteq> 0"
  1.1071    shows "\<exists>ps. primefact ps n"
  1.1072  proof -
  1.1073 -  have "\<exists>xs. mset xs = prime_factorization n" by (rule ex_mset)
  1.1074 -  then guess xs .. note xs = this
  1.1075 -  from assms have "n = prod_mset (prime_factorization n)" 
  1.1076 +  obtain xs where xs: "mset xs = prime_factorization n"
  1.1077 +    using ex_mset [of "prime_factorization n"] by blast
  1.1078 +  from assms have "n = prod_mset (prime_factorization n)"
  1.1079      by (simp add: prod_mset_prime_factorization)
  1.1080    also have "\<dots> = prod_mset (mset xs)" by (simp add: xs)
  1.1081 -  also have "\<dots> = foldr op * xs 1" by (induction xs) simp_all
  1.1082 +  also have "\<dots> = foldr op * xs 1" by (induct xs) simp_all
  1.1083    finally have "foldr op * xs 1 = n" ..
  1.1084 -  moreover from xs have "\<forall>p\<in>#mset xs. prime p"
  1.1085 -    by auto
  1.1086 +  moreover from xs have "\<forall>p\<in>#mset xs. prime p" by auto
  1.1087    ultimately have "primefact xs n" by (auto simp: primefact_def)
  1.1088 -  thus ?thesis ..
  1.1089 +  then show ?thesis ..
  1.1090  qed
  1.1091  
  1.1092  lemma primefact_contains:
  1.1093 -  assumes pf: "primefact ps n" and p: "prime p" and pn: "p dvd n"
  1.1094 -  shows "(p::nat) \<in> set ps"
  1.1095 +  fixes p :: nat
  1.1096 +  assumes pf: "primefact ps n"
  1.1097 +    and p: "prime p"
  1.1098 +    and pn: "p dvd n"
  1.1099 +  shows "p \<in> set ps"
  1.1100    using pf p pn
  1.1101 -proof(induct ps arbitrary: p n)
  1.1102 -  case Nil thus ?case by (auto simp add: primefact_def)
  1.1103 +proof (induct ps arbitrary: p n)
  1.1104 +  case Nil
  1.1105 +  then show ?case by (auto simp: primefact_def)
  1.1106  next
  1.1107 -  case (Cons q qs p n)
  1.1108 +  case (Cons q qs)
  1.1109    from Cons.prems[unfolded primefact_def]
  1.1110 -  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
  1.1111 -  {assume "p dvd q"
  1.1112 -    with p(1) q(1) have "p = q" unfolding prime_nat_iff by auto
  1.1113 -    hence ?case by simp}
  1.1114 -  moreover
  1.1115 -  { assume h: "p dvd foldr op * qs 1"
  1.1116 +  have q: "prime q" "q * foldr op * qs 1 = n" "\<forall>p \<in>set qs. prime p"
  1.1117 +    and p: "prime p" "p dvd q * foldr op * qs 1"
  1.1118 +    by simp_all
  1.1119 +  consider "p dvd q" | "p dvd foldr op * qs 1"
  1.1120 +    by (metis p prime_dvd_mult_eq_nat)
  1.1121 +  then show ?case
  1.1122 +  proof cases
  1.1123 +    case 1
  1.1124 +    with p(1) q(1) have "p = q"
  1.1125 +      unfolding prime_nat_iff by auto
  1.1126 +    then show ?thesis by simp
  1.1127 +  next
  1.1128 +    case prem: 2
  1.1129      from q(3) have pqs: "primefact qs (foldr op * qs 1)"
  1.1130        by (simp add: primefact_def)
  1.1131 -    from Cons.hyps[OF pqs p(1) h] have ?case by simp}
  1.1132 -  ultimately show ?case
  1.1133 -    by (metis p prime_dvd_mult_eq_nat) 
  1.1134 +    from Cons.hyps[OF pqs p(1) prem] show ?thesis by simp
  1.1135 +  qed
  1.1136  qed
  1.1137  
  1.1138  lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps"
  1.1139    by (auto simp add: primefact_def list_all_iff)
  1.1140  
  1.1141 -(* Variant of Lucas theorem.                                                 *)
  1.1142 -
  1.1143 +text \<open>Variant of Lucas theorem.\<close>
  1.1144  lemma lucas_primefact:
  1.1145    assumes n: "n \<ge> 2" and an: "[a^(n - 1) = 1] (mod n)"
  1.1146 -  and psn: "foldr op * ps 1 = n - 1"
  1.1147 -  and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps"
  1.1148 +    and psn: "foldr op * ps 1 = n - 1"
  1.1149 +    and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps"
  1.1150    shows "prime n"
  1.1151 -proof-
  1.1152 -  {fix p assume p: "prime p" "p dvd n - 1" "[a ^ ((n - 1) div p) = 1] (mod n)"
  1.1153 +proof -
  1.1154 +  {
  1.1155 +    fix p
  1.1156 +    assume p: "prime p" "p dvd n - 1" "[a ^ ((n - 1) div p) = 1] (mod n)"
  1.1157      from psn psp have psn1: "primefact ps (n - 1)"
  1.1158        by (auto simp add: list_all_iff primefact_variant)
  1.1159      from p(3) primefact_contains[OF psn1 p(1,2)] psp
  1.1160 -    have False by (induct ps, auto)}
  1.1161 +    have False by (induct ps) auto
  1.1162 +  }
  1.1163    with lucas[OF n an] show ?thesis by blast
  1.1164  qed
  1.1165  
  1.1166 -(* Variant of Pocklington theorem.                                           *)
  1.1167 -
  1.1168 +text \<open>Variant of Pocklington theorem.\<close>
  1.1169  lemma pocklington_primefact:
  1.1170    assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2"
  1.1171 -  and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q"
  1.1172 -  and bqn: "(b^q) mod n = 1"
  1.1173 -  and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
  1.1174 +    and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q"
  1.1175 +    and bqn: "(b^q) mod n = 1"
  1.1176 +    and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
  1.1177    shows "prime n"
  1.1178 -proof-
  1.1179 +proof -
  1.1180    from bqn psp qrn
  1.1181    have bqn: "a ^ (n - 1) mod n = 1"
  1.1182 -    and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps"  
  1.1183 -    unfolding arnb[symmetric] power_mod 
  1.1184 +    and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps"
  1.1185 +    unfolding arnb[symmetric] power_mod
  1.1186      by (simp_all add: power_mult[symmetric] algebra_simps)
  1.1187 -  from n  have n0: "n > 0" by arith
  1.1188 +  from n have n0: "n > 0" by arith
  1.1189    from div_mult_mod_eq[of "a^(n - 1)" n]
  1.1190      mod_less_divisor[OF n0, of "a^(n - 1)"]
  1.1191    have an1: "[a ^ (n - 1) = 1] (mod n)"
  1.1192      by (metis bqn cong_nat_def mod_mod_trivial)
  1.1193 -  {fix p assume p: "prime p" "p dvd q"
  1.1194 +  have "coprime (a ^ ((n - 1) div p) - 1) n" if p: "prime p" "p dvd q" for p
  1.1195 +  proof -
  1.1196      from psp psq have pfpsq: "primefact ps q"
  1.1197        by (auto simp add: primefact_variant list_all_iff)
  1.1198      from psp primefact_contains[OF pfpsq p]
  1.1199      have p': "coprime (a ^ (r * (q div p)) mod n - 1) n"
  1.1200        by (simp add: list_all_iff)
  1.1201 -    from p prime_nat_iff have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)" 
  1.1202 +    from p prime_nat_iff have p01: "p \<noteq> 0" "p \<noteq> 1" "p = Suc (p - 1)"
  1.1203        by auto
  1.1204      from div_mult1_eq[of r q p] p(2)
  1.1205      have eq1: "r* (q div p) = (n - 1) div p"
  1.1206        unfolding qrn[symmetric] dvd_eq_mod_eq_0 by (simp add: mult.commute)
  1.1207 -    have ath: "\<And>a (b::nat). a <= b \<Longrightarrow> a \<noteq> 0 ==> 1 <= a \<and> 1 <= b" by arith
  1.1208 -    {assume "a ^ ((n - 1) div p) mod n = 0"
  1.1209 -      then obtain s where s: "a ^ ((n - 1) div p) = n*s"
  1.1210 +    have ath: "a \<le> b \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> 1 \<le> a \<and> 1 \<le> b" for a b :: nat
  1.1211 +      by arith
  1.1212 +    {
  1.1213 +      assume "a ^ ((n - 1) div p) mod n = 0"
  1.1214 +      then obtain s where s: "a ^ ((n - 1) div p) = n * s"
  1.1215          unfolding mod_eq_0_iff by blast
  1.1216 -      hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
  1.1217 -      from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto
  1.1218 -      from dvd_trans[OF p(2) qn1]
  1.1219 -      have npp: "(n - 1) div p * p = n - 1" by simp
  1.1220 -      with eq0 have "a^ (n - 1) = (n*s)^p"
  1.1221 +      then have eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
  1.1222 +      from qrn[symmetric] have qn1: "q dvd n - 1"
  1.1223 +        by (auto simp: dvd_def)
  1.1224 +      from dvd_trans[OF p(2) qn1] have npp: "(n - 1) div p * p = n - 1"
  1.1225 +        by simp
  1.1226 +      with eq0 have "a ^ (n - 1) = (n * s) ^ p"
  1.1227          by (simp add: power_mult[symmetric])
  1.1228 -      hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp
  1.1229 +      with bqn p01 have "1 = (n * s)^(Suc (p - 1)) mod n"
  1.1230 +        by simp
  1.1231        also have "\<dots> = 0" by (simp add: mult.assoc)
  1.1232 -      finally have False by simp }
  1.1233 -      then have th11: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto
  1.1234 -    have th1: "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)"
  1.1235 -      unfolding cong_nat_def by simp
  1.1236 -    from  th1   ath[OF mod_less_eq_dividend th11]
  1.1237 -    have th: "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)"
  1.1238 +      finally have False by simp
  1.1239 +    }
  1.1240 +    then have *: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto
  1.1241 +    have "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)"
  1.1242 +      by (simp add: cong_nat_def)
  1.1243 +    with ath[OF mod_less_eq_dividend *]
  1.1244 +    have "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)"
  1.1245        by (metis cong_diff_nat cong_refl_nat)
  1.1246 -    have "coprime (a ^ ((n - 1) div p) - 1) n"
  1.1247 -      by (metis cong_imp_coprime_nat eq1 p' th) }
  1.1248 -  with pocklington[OF n qrn[symmetric] nq2 an1]
  1.1249 -  show ?thesis by blast
  1.1250 +    then show ?thesis
  1.1251 +      by (metis cong_imp_coprime_nat eq1 p')
  1.1252 +  qed
  1.1253 +  with pocklington[OF n qrn[symmetric] nq2 an1] show ?thesis
  1.1254 +    by blast
  1.1255  qed
  1.1256  
  1.1257  end
     2.1 --- a/src/HOL/Number_Theory/Residues.thy	Tue Aug 01 17:33:04 2017 +0200
     2.2 +++ b/src/HOL/Number_Theory/Residues.thy	Tue Aug 01 22:19:37 2017 +0200
     2.3 @@ -17,24 +17,26 @@
     2.4    Totient
     2.5  begin
     2.6  
     2.7 -definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" where
     2.8 -  "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))"
     2.9 +definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool"
    2.10 +  where "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))"
    2.11  
    2.12 -definition Legendre :: "int \<Rightarrow> int \<Rightarrow> int" where
    2.13 -  "Legendre a p = (if ([a = 0] (mod p)) then 0
    2.14 -    else if QuadRes p a then 1
    2.15 -    else -1)"
    2.16 +definition Legendre :: "int \<Rightarrow> int \<Rightarrow> int"
    2.17 +  where "Legendre a p =
    2.18 +    (if ([a = 0] (mod p)) then 0
    2.19 +     else if QuadRes p a then 1
    2.20 +     else -1)"
    2.21 +
    2.22  
    2.23  subsection \<open>A locale for residue rings\<close>
    2.24  
    2.25  definition residue_ring :: "int \<Rightarrow> int ring"
    2.26 -where
    2.27 -  "residue_ring m =
    2.28 -    \<lparr>carrier = {0..m - 1},
    2.29 -     monoid.mult = \<lambda>x y. (x * y) mod m,
    2.30 -     one = 1,
    2.31 -     zero = 0,
    2.32 -     add = \<lambda>x y. (x + y) mod m\<rparr>"
    2.33 +  where
    2.34 +    "residue_ring m =
    2.35 +      \<lparr>carrier = {0..m - 1},
    2.36 +       monoid.mult = \<lambda>x y. (x * y) mod m,
    2.37 +       one = 1,
    2.38 +       zero = 0,
    2.39 +       add = \<lambda>x y. (x + y) mod m\<rparr>"
    2.40  
    2.41  locale residues =
    2.42    fixes m :: int and R (structure)
    2.43 @@ -88,37 +90,37 @@
    2.44  \<close>
    2.45  
    2.46  lemma res_carrier_eq: "carrier R = {0..m - 1}"
    2.47 -  unfolding R_def residue_ring_def by auto
    2.48 +  by (auto simp: R_def residue_ring_def)
    2.49  
    2.50  lemma res_add_eq: "x \<oplus> y = (x + y) mod m"
    2.51 -  unfolding R_def residue_ring_def by auto
    2.52 +  by (auto simp: R_def residue_ring_def)
    2.53  
    2.54  lemma res_mult_eq: "x \<otimes> y = (x * y) mod m"
    2.55 -  unfolding R_def residue_ring_def by auto
    2.56 +  by (auto simp: R_def residue_ring_def)
    2.57  
    2.58  lemma res_zero_eq: "\<zero> = 0"
    2.59 -  unfolding R_def residue_ring_def by auto
    2.60 +  by (auto simp: R_def residue_ring_def)
    2.61  
    2.62  lemma res_one_eq: "\<one> = 1"
    2.63 -  unfolding R_def residue_ring_def units_of_def by auto
    2.64 +  by (auto simp: R_def residue_ring_def units_of_def)
    2.65  
    2.66  lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
    2.67    using m_gt_one
    2.68    unfolding Units_def R_def residue_ring_def
    2.69    apply auto
    2.70 -  apply (subgoal_tac "x \<noteq> 0")
    2.71 -  apply auto
    2.72 -  apply (metis invertible_coprime_int)
    2.73 +    apply (subgoal_tac "x \<noteq> 0")
    2.74 +     apply auto
    2.75 +   apply (metis invertible_coprime_int)
    2.76    apply (subst (asm) coprime_iff_invertible'_int)
    2.77 -  apply (auto simp add: cong_int_def mult.commute)
    2.78 +   apply (auto simp add: cong_int_def mult.commute)
    2.79    done
    2.80  
    2.81  lemma res_neg_eq: "\<ominus> x = (- x) mod m"
    2.82    using m_gt_one unfolding R_def a_inv_def m_inv_def residue_ring_def
    2.83    apply simp
    2.84    apply (rule the_equality)
    2.85 -  apply (simp add: mod_add_right_eq)
    2.86 -  apply (simp add: add.commute mod_add_right_eq)
    2.87 +   apply (simp add: mod_add_right_eq)
    2.88 +   apply (simp add: add.commute mod_add_right_eq)
    2.89    apply (metis add.right_neutral minus_add_cancel mod_add_right_eq mod_pos_pos_trivial)
    2.90    done
    2.91  
    2.92 @@ -139,18 +141,16 @@
    2.93    using insert m_gt_one by auto
    2.94  
    2.95  lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
    2.96 -  unfolding R_def residue_ring_def
    2.97 -  by (auto simp add: mod_simps)
    2.98 +  by (auto simp: R_def residue_ring_def mod_simps)
    2.99  
   2.100  lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
   2.101 -  unfolding R_def residue_ring_def
   2.102 -  by (auto simp add: mod_simps)
   2.103 +  by (auto simp: R_def residue_ring_def mod_simps)
   2.104  
   2.105  lemma zero_cong: "\<zero> = 0"
   2.106 -  unfolding R_def residue_ring_def by auto
   2.107 +  by (auto simp: R_def residue_ring_def)
   2.108  
   2.109  lemma one_cong: "\<one> = 1 mod m"
   2.110 -  using m_gt_one unfolding R_def residue_ring_def by auto
   2.111 +  using m_gt_one by (auto simp: R_def residue_ring_def)
   2.112  
   2.113  (* FIXME revise algebra library to use 1? *)
   2.114  lemma pow_cong: "(x mod m) (^) n = x^n mod m"
   2.115 @@ -173,24 +173,26 @@
   2.116    assumes "1 < m" and "coprime a m"
   2.117    shows "a mod m \<in> Units R"
   2.118  proof (cases "a mod m = 0")
   2.119 -  case True with assms show ?thesis
   2.120 +  case True
   2.121 +  with assms show ?thesis
   2.122      by (auto simp add: res_units_eq gcd_red_int [symmetric])
   2.123  next
   2.124    case False
   2.125    from assms have "0 < m" by simp
   2.126 -  with pos_mod_sign [of m a] have "0 \<le> a mod m" .
   2.127 +  then have "0 \<le> a mod m" by (rule pos_mod_sign [of m a])
   2.128    with False have "0 < a mod m" by simp
   2.129    with assms show ?thesis
   2.130      by (auto simp add: res_units_eq gcd_red_int [symmetric] ac_simps)
   2.131  qed
   2.132  
   2.133  lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)"
   2.134 -  unfolding cong_int_def by auto
   2.135 +  by (auto simp: cong_int_def)
   2.136  
   2.137  
   2.138  text \<open>Simplifying with these will translate a ring equation in R to a congruence.\<close>
   2.139 -lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong
   2.140 -    prod_cong sum_cong neg_cong res_eq_to_cong
   2.141 +lemmas res_to_cong_simps =
   2.142 +  add_cong mult_cong pow_cong one_cong
   2.143 +  prod_cong sum_cong neg_cong res_eq_to_cong
   2.144  
   2.145  text \<open>Other useful facts about the residue ring.\<close>
   2.146  lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2"
   2.147 @@ -220,11 +222,11 @@
   2.148  
   2.149  lemma is_field: "field R"
   2.150  proof -
   2.151 -  have "\<And>x. \<lbrakk>gcd x (int p) \<noteq> 1; 0 \<le> x; x < int p\<rbrakk> \<Longrightarrow> x = 0"
   2.152 +  have "gcd x (int p) \<noteq> 1 \<Longrightarrow> 0 \<le> x \<Longrightarrow> x < int p \<Longrightarrow> x = 0" for x
   2.153      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)
   2.154    then show ?thesis
   2.155 -  apply (intro cring.field_intro2 cring)
   2.156 -  apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
   2.157 +    apply (intro cring.field_intro2 cring)
   2.158 +     apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
   2.159      done
   2.160  qed
   2.161  
   2.162 @@ -245,23 +247,26 @@
   2.163  
   2.164  subsection \<open>Euler's theorem\<close>
   2.165  
   2.166 -lemma (in residues) totient_eq:
   2.167 -  "totient (nat m) = card (Units R)"
   2.168 +lemma (in residues) totient_eq: "totient (nat m) = card (Units R)"
   2.169  proof -
   2.170    have *: "inj_on nat (Units R)"
   2.171      by (rule inj_onI) (auto simp add: res_units_eq)
   2.172    define m' where "m' = nat m"
   2.173 -  from m_gt_one have m: "m = int m'" "m' > 1" by (simp_all add: m'_def)
   2.174 -  from m have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
   2.175 +  from m_gt_one have "m = int m'" "m' > 1"
   2.176 +    by (simp_all add: m'_def)
   2.177 +  then have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
   2.178      unfolding res_units_eq
   2.179      by (cases x; cases "x = m") (auto simp: totatives_def transfer_int_nat_gcd)
   2.180 -  hence "Units R = int ` totatives m'" by blast
   2.181 -  hence "totatives m' = nat ` Units R" by (simp add: image_image)
   2.182 +  then have "Units R = int ` totatives m'"
   2.183 +    by blast
   2.184 +  then have "totatives m' = nat ` Units R"
   2.185 +    by (simp add: image_image)
   2.186    then have "card (totatives (nat m)) = card (nat ` Units R)"
   2.187      by (simp add: m'_def)
   2.188    also have "\<dots> = card (Units R)"
   2.189      using * card_image [of nat "Units R"] by auto
   2.190 -  finally show ?thesis by (simp add: totient_def)
   2.191 +  finally show ?thesis
   2.192 +    by (simp add: totient_def)
   2.193  qed
   2.194  
   2.195  lemma (in residues_prime) totient_eq: "totient p = p - 1"
   2.196 @@ -324,26 +329,26 @@
   2.197    have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i\<in>\<Union>?Inverse_Pairs. i)"
   2.198      apply (subst UR)
   2.199      apply (subst finprod_Un_disjoint)
   2.200 -    apply (auto intro: funcsetI)
   2.201 +         apply (auto intro: funcsetI)
   2.202      using inv_one apply auto[1]
   2.203      using inv_eq_neg_one_eq apply auto
   2.204      done
   2.205    also have "(\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"
   2.206      apply (subst finprod_insert)
   2.207 -    apply auto
   2.208 +        apply auto
   2.209      apply (frule one_eq_neg_one)
   2.210      using a apply force
   2.211      done
   2.212    also have "(\<Otimes>i\<in>(\<Union>?Inverse_Pairs). i) = (\<Otimes>A\<in>?Inverse_Pairs. (\<Otimes>y\<in>A. y))"
   2.213      apply (subst finprod_Union_disjoint)
   2.214 -    apply auto
   2.215 -    apply (metis Units_inv_inv)+
   2.216 +       apply auto
   2.217 +     apply (metis Units_inv_inv)+
   2.218      done
   2.219    also have "\<dots> = \<one>"
   2.220      apply (rule finprod_one)
   2.221 -    apply auto
   2.222 +     apply auto
   2.223      apply (subst finprod_insert)
   2.224 -    apply auto
   2.225 +        apply auto
   2.226      apply (metis inv_eq_self)
   2.227      done
   2.228    finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>"
   2.229 @@ -361,7 +366,7 @@
   2.230    finally have "fact (p - 1) mod p = \<ominus> \<one>" .
   2.231    then show ?thesis
   2.232      by (metis of_nat_fact Divides.transfer_int_nat_functions(2)
   2.233 -      cong_int_def res_neg_eq res_one_eq)
   2.234 +        cong_int_def res_neg_eq res_one_eq)
   2.235  qed
   2.236  
   2.237  lemma wilson_theorem:
   2.238 @@ -380,13 +385,11 @@
   2.239  
   2.240  text \<open>
   2.241    This result can be transferred to the multiplicative group of
   2.242 -  $\mathbb{Z}/p\mathbb{Z}$ for $p$ prime.\<close>
   2.243 +  \<open>\<int>/p\<int>\<close> for \<open>p\<close> prime.\<close>
   2.244  
   2.245  lemma mod_nat_int_pow_eq:
   2.246    fixes n :: nat and p a :: int
   2.247 -  assumes "a \<ge> 0" "p \<ge> 0"
   2.248 -  shows "(nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
   2.249 -  using assms
   2.250 +  shows "a \<ge> 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow> (nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
   2.251    by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric])
   2.252  
   2.253  theorem residue_prime_mult_group_has_gen :
   2.254 @@ -394,43 +397,55 @@
   2.255   assumes prime_p : "prime p"
   2.256   shows "\<exists>a \<in> {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \<in> UNIV}"
   2.257  proof -
   2.258 -  have "p\<ge>2" using prime_gt_1_nat[OF prime_p] by simp
   2.259 -  interpret R:residues_prime "p" "residue_ring p" unfolding residues_prime_def
   2.260 -    by (simp add: prime_p)
   2.261 -  have car: "carrier (residue_ring (int p)) - {\<zero>\<^bsub>residue_ring (int p)\<^esub>} =  {1 .. int p - 1}"
   2.262 +  have "p \<ge> 2"
   2.263 +    using prime_gt_1_nat[OF prime_p] by simp
   2.264 +  interpret R: residues_prime p "residue_ring p"
   2.265 +    by (simp add: residues_prime_def prime_p)
   2.266 +  have car: "carrier (residue_ring (int p)) - {\<zero>\<^bsub>residue_ring (int p)\<^esub>} = {1 .. int p - 1}"
   2.267      by (auto simp add: R.zero_cong R.res_carrier_eq)
   2.268 -  obtain a where a:"a \<in> {1 .. int p - 1}"
   2.269 -         and a_gen:"{1 .. int p - 1} = {a(^)\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \<in> UNIV}"
   2.270 -    apply atomize_elim using field.finite_field_mult_group_has_gen[OF R.is_field]
   2.271 +
   2.272 +  have "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)"
   2.273 +    if "x \<in> {1 .. int p - 1}" for x and i :: nat
   2.274 +    using that R.pow_cong[of x i] by auto
   2.275 +  moreover
   2.276 +  obtain a where a: "a \<in> {1 .. int p - 1}"
   2.277 +    and a_gen: "{1 .. int p - 1} = {a(^)\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \<in> UNIV}"
   2.278 +    using field.finite_field_mult_group_has_gen[OF R.is_field]
   2.279      by (auto simp add: car[symmetric] carrier_mult_of)
   2.280 -  { fix x fix i :: nat assume x: "x \<in> {1 .. int p - 1}"
   2.281 -    hence "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)" using R.pow_cong[of x i] by auto}
   2.282 -  note * = this
   2.283 -  have **:"nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
   2.284 +  moreover
   2.285 +  have "nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
   2.286    proof
   2.287 -    { fix n assume n: "n \<in> ?L"
   2.288 -      then have "n \<in> ?R" using \<open>p\<ge>2\<close> by force
   2.289 -    } thus "?L \<subseteq> ?R" by blast
   2.290 -    { fix n assume n: "n \<in> ?R"
   2.291 -      then have "n \<in> ?L" using \<open>p\<ge>2\<close> Set_Interval.transfer_nat_int_set_functions(2) by fastforce
   2.292 -    } thus "?R \<subseteq> ?L" by blast
   2.293 +    have "n \<in> ?R" if "n \<in> ?L" for n
   2.294 +      using that \<open>p\<ge>2\<close> by force
   2.295 +    then show "?L \<subseteq> ?R" by blast
   2.296 +    have "n \<in> ?L" if "n \<in> ?R" for n
   2.297 +      using that \<open>p\<ge>2\<close> Set_Interval.transfer_nat_int_set_functions(2) by fastforce
   2.298 +    then show "?R \<subseteq> ?L" by blast
   2.299    qed
   2.300 +  moreover
   2.301    have "nat ` {a^i mod (int p) | i::nat. i \<in> UNIV} = {nat a^i mod p | i . i \<in> UNIV}" (is "?L = ?R")
   2.302    proof
   2.303 -    { fix x assume x: "x \<in> ?L"
   2.304 -      then obtain i where i:"x = nat (a^i mod (int p))" by blast
   2.305 -      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
   2.306 -      hence "x \<in> ?R" using i by blast
   2.307 -    } thus "?L \<subseteq> ?R" by blast
   2.308 -    { fix x assume x: "x \<in> ?R"
   2.309 -      then obtain i where i:"x = nat a^i mod p" by blast
   2.310 -      hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
   2.311 -    } thus "?R \<subseteq> ?L" by blast
   2.312 +    have "x \<in> ?R" if "x \<in> ?L" for x
   2.313 +    proof -
   2.314 +      from that obtain i where i: "x = nat (a^i mod (int p))"
   2.315 +        by blast
   2.316 +      then have "x = nat a ^ i mod p"
   2.317 +        using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
   2.318 +      with i show ?thesis by blast
   2.319 +    qed
   2.320 +    then show "?L \<subseteq> ?R" by blast
   2.321 +    have "x \<in> ?L" if "x \<in> ?R" for x
   2.322 +    proof -
   2.323 +      from that obtain i where i: "x = nat a^i mod p"
   2.324 +        by blast
   2.325 +      with mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> show ?thesis
   2.326 +        by auto
   2.327 +    qed
   2.328 +    then show "?R \<subseteq> ?L" by blast
   2.329    qed
   2.330 -  hence "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"
   2.331 -    using * a a_gen ** by presburger
   2.332 -  moreover
   2.333 -  have "nat a \<in> {1 .. p - 1}" using a by force
   2.334 +  ultimately have "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"
   2.335 +    by presburger
   2.336 +  moreover from a have "nat a \<in> {1 .. p - 1}" by force
   2.337    ultimately show ?thesis ..
   2.338  qed
   2.339  
     3.1 --- a/src/HOL/Number_Theory/Totient.thy	Tue Aug 01 17:33:04 2017 +0200
     3.2 +++ b/src/HOL/Number_Theory/Totient.thy	Tue Aug 01 22:19:37 2017 +0200
     3.3 @@ -177,7 +177,7 @@
     3.4    
     3.5  lemma totient_less: 
     3.6    assumes "n > 1"
     3.7 -  shows   "totient n < n"
     3.8 +  shows "totient n < n"
     3.9  proof -
    3.10    from assms have "card (totatives n) \<le> card {0<..<n}"
    3.11      using totatives_less[of _ n] totatives_subset[of n] by (intro card_mono) auto