src/HOL/Number_Theory/Pocklington.thy
 changeset 67051 e7e54a0b9197 parent 66888 930abfdf8727 child 67091 1393c2340eec
```     1.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Sat Nov 11 18:33:35 2017 +0000
1.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Sat Nov 11 18:41:08 2017 +0000
1.3 @@ -11,18 +11,11 @@
1.4  subsection \<open>Lemmas about previously defined terms\<close>
1.5
1.6  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.7 -  unfolding prime_nat_iff
1.8 -proof safe
1.9 -  fix m
1.10 -  assume p: "p > 0" "p \<noteq> 1"
1.11 -    and m: "m dvd p" "m \<noteq> p"
1.12 -    and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
1.13 -  from p m have "m \<noteq> 0" by (intro notI) auto
1.14 -  moreover from p m have "m < p" by (auto dest: dvd_imp_le)
1.15 -  ultimately have "coprime p m"
1.16 -    using * by blast
1.17 -  with m show "m = 1" by simp
1.18 -qed (auto simp: prime_nat_iff simp del: One_nat_def intro!: prime_imp_coprime dest: dvd_imp_le)
1.19 +  apply (auto simp add: prime_nat_iff)
1.20 +   apply (rule coprimeI)
1.21 +   apply (auto dest: nat_dvd_not_less simp add: ac_simps)
1.22 +  apply (metis One_nat_def dvd_1_iff_1 dvd_pos_nat gcd_nat.order_iff is_unit_gcd linorder_neqE_nat nat_dvd_not_less)
1.23 +  done
1.24
1.25  lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
1.26  proof -
1.27 @@ -46,7 +39,7 @@
1.28    from bezout_add_strong_nat [OF this]
1.29    obtain d x y where dxy: "d dvd a" "d dvd n" "a * x = n * y + d" by blast
1.30    from dxy(1,2) have d1: "d = 1"
1.31 -    by (metis assms coprime_nat)
1.32 +    using assms coprime_common_divisor [of a n d] by simp
1.33    with dxy(3) have "a * x * b = (n * y + 1) * b"
1.34      by simp
1.35    then have "a * (x * b) = n * (y * b) + b"
1.36 @@ -94,9 +87,9 @@
1.37    shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
1.38  proof -
1.39    from pa have ap: "coprime a p"
1.40 -    by (metis gcd.commute)
1.41 -  have px: "coprime x p"
1.42 -    by (metis gcd.commute p prime_nat_iff'' x0 xp)
1.43 +    by (simp add: ac_simps)
1.44 +  from x0 xp p have px: "coprime x p"
1.45 +    by (auto simp add: prime_nat_iff'' ac_simps)
1.46    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.47      by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
1.48    have "y \<noteq> 0"
1.49 @@ -104,8 +97,8 @@
1.50      assume "y = 0"
1.51      with y(2) have "p dvd a"
1.52        using cong_dvd_iff by auto
1.53 -    then show False
1.54 -      by (metis gcd_nat.absorb1 not_prime_1 p pa)
1.55 +    with not_prime_1 p pa show False
1.56 +      by (auto simp add: gcd_nat.order_iff)
1.57    qed
1.58    with y show ?thesis
1.59      by blast
1.60 @@ -128,9 +121,9 @@
1.61    obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)" "\<forall>y. ?P y \<longrightarrow> y = x"
1.62      by blast
1.63    from ma nb x have "coprime x a" "coprime x b"
1.64 -    by (metis cong_gcd_eq_nat)+
1.65 +    using cong_imp_coprime_nat cong_sym by blast+
1.66    then have "coprime x (a*b)"
1.67 -    by (metis coprime_mul_eq)
1.68 +    by simp
1.69    with x show ?thesis
1.70      by blast
1.71  qed
1.72 @@ -164,7 +157,8 @@
1.73        from dvd_mod_iff[OF d(2), of "a^m"] dam am1 show ?thesis
1.74          by simp
1.75      qed
1.76 -    then show ?thesis by blast
1.77 +    then show ?thesis
1.78 +      by (auto intro: coprimeI)
1.79    qed
1.80  qed
1.81
1.82 @@ -216,8 +210,8 @@
1.83    from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1"
1.84      by simp
1.85    from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1
1.86 -  have an: "coprime a n" "coprime (a^(n - 1)) n"
1.87 -    by (auto simp add: coprime_exp gcd.commute)
1.88 +  have an: "coprime a n" "coprime (a ^ (n - 1)) n"
1.89 +    using \<open>n \<ge> 2\<close> by simp_all
1.90    have False if H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
1.91    proof -
1.92      from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
1.93 @@ -229,7 +223,7 @@
1.94        let ?y = "a^ ((n - 1) div m * m)"
1.95        note mdeq = div_mult_mod_eq[of "(n - 1)" m]
1.96        have yn: "coprime ?y n"
1.97 -        by (metis an(1) coprime_exp gcd.commute)
1.98 +        using an(1) by (cases "(n - Suc 0) div m * m = 0") auto
1.99        have "?y mod n = (a^m)^((n - 1) div m) mod n"
1.100          by (simp add: algebra_simps power_mult)
1.101        also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n"
1.102 @@ -359,9 +353,11 @@
1.103      next
1.104        case (Suc d')
1.105        then have d0: "d \<noteq> 0" by simp
1.106 -      from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
1.107 +      from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1"
1.108 +        by (auto elim: not_coprimeE)
1.109        from \<open>?lhs\<close> obtain q1 q2 where q12: "a ^ d + n * q1 = 1 + n * q2"
1.110 -        by (metis prem d0 gcd.commute lucas_coprime_lemma)
1.111 +        using prem d0 lucas_coprime_lemma
1.112 +        by (auto elim: not_coprimeE simp add: ac_simps)
1.113        then have "a ^ d + n * q1 - n * q2 = 1" by simp
1.114        with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2 Suc p have "p dvd 1"
1.115          by metis
1.116 @@ -398,8 +394,10 @@
1.117    qed
1.118  qed
1.119
1.120 -lemma order_divides_totient: "ord n a dvd totient n" if "coprime n a"
1.121 -  by (metis euler_theorem gcd.commute ord_divides that)
1.122 +lemma order_divides_totient:
1.123 +  "ord n a dvd totient n" if "coprime n a"
1.124 +  using that euler_theorem [of a n]
1.125 +  by (simp add: ord_divides [symmetric] ac_simps)
1.126
1.127  lemma order_divides_expdiff:
1.128    fixes n::nat and a::nat assumes na: "coprime n a"
1.129 @@ -412,11 +410,11 @@
1.130      from na ed have "\<exists>c. d = e + c" by presburger
1.131      then obtain c where c: "d = e + c" ..
1.132      from na have an: "coprime a n"
1.133 -      by (metis gcd.commute)
1.134 -    have aen: "coprime (a^e) n"
1.135 -      by (metis coprime_exp gcd.commute na)
1.136 -    have acn: "coprime (a^c) n"
1.137 -      by (metis coprime_exp gcd.commute na)
1.138 +      by (simp add: ac_simps)
1.139 +    then have aen: "coprime (a ^ e) n"
1.140 +      by (cases "e > 0") simp_all
1.141 +    from an have acn: "coprime (a ^ c) n"
1.142 +      by (cases "c > 0") simp_all
1.143      from c have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
1.144        by simp
1.145      also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
1.146 @@ -620,8 +618,9 @@
1.147        by (metis cong_to_1_nat exps)
1.148      from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r"
1.149        using P0 by simp
1.150 -    with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp
1.151 -    with p01 pn pd0 coprime_common_divisor_nat show False
1.152 +    with caP have "coprime (a ^ (ord p (a ^ r) * t * r) - 1) n"
1.153 +      by simp
1.154 +    with p01 pn pd0 coprime_common_divisor [of _ n p] show False
1.155        by auto
1.156    qed
1.157    with d have o: "ord p (a^r) = q" by simp
1.158 @@ -632,12 +631,14 @@
1.159      assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
1.160      from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast
1.161      from n have "n \<noteq> 0" by simp
1.162 -    then have False using d dp pn
1.163 -      by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)
1.164 +    then have False using d dp pn an
1.165 +      by auto (metis One_nat_def Suc_lessI
1.166 +        \<open>1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p)\<close> \<open>a ^ (q * r) = p * l * k + 1\<close> add_diff_cancel_left' dvd_diff_nat dvd_power dvd_triv_left gcd_nat.trans nat_dvd_not_less nqr zero_less_diff zero_less_one)
1.167    }
1.168 -  then have cpa: "coprime p a" by auto
1.169 -  have arp: "coprime (a^r) p"
1.170 -    by (metis coprime_exp cpa gcd.commute)
1.171 +  then have cpa: "coprime p a"
1.172 +    by (auto intro: coprimeI)
1.173 +  then have arp: "coprime (a ^ r) p"
1.174 +    by (cases "r > 0") (simp_all add: ac_simps)
1.175    from euler_theorem [OF arp, simplified ord_divides] o totient_eq have "q dvd (p - 1)"
1.176      by simp
1.177    then obtain d where d:"p - 1 = q * d"
```