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"