1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Library/Pocklington.thy Mon Feb 25 12:04:09 2008 +0100
1.3 @@ -0,0 +1,1330 @@
1.4 +(* Title: HOL/Library/Pocklington.thy
1.5 + ID: $Id:
1.6 + Author: Amine Chaieb
1.7 +*)
1.8 +
1.9 +header {* Pocklington's Theorem for Primes *}
1.10 +
1.11 +
1.12 +theory Pocklington
1.13 +imports List Primes
1.14 +begin
1.15 +
1.16 +definition modeq:: "nat => nat => nat => bool" ("(1[_ = _] '(mod _'))")
1.17 + where "[a = b] (mod p) == ((a mod p) = (b mod p))"
1.18 +
1.19 +definition modneq:: "nat => nat => nat => bool" ("(1[_ \<noteq> _] '(mod _'))")
1.20 + where "[a \<noteq> b] (mod p) == ((a mod p) \<noteq> (b mod p))"
1.21 +
1.22 +lemma modeq_trans:
1.23 + "\<lbrakk> [a = b] (mod p); [b = c] (mod p) \<rbrakk> \<Longrightarrow> [a = c] (mod p)"
1.24 + by (simp add:modeq_def)
1.25 +
1.26 +lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
1.27 +proof
1.28 + assume H: "x mod n = y mod n"
1.29 + hence "x mod n - y mod n = 0" by simp
1.30 + hence "(x mod n - y mod n) mod n = 0" by simp
1.31 + hence "(x - y) mod n = 0" by (simp add: zmod_zdiff1_eq[symmetric])
1.32 + thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
1.33 +next
1.34 + assume H: "n dvd x - y"
1.35 + then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
1.36 + hence "x = n*k + y" by simp
1.37 + hence "x mod n = (n*k + y) mod n" by simp
1.38 + thus "x mod n = y mod n" by (simp add: zmod_zadd_left_eq)
1.39 +qed
1.40 +
1.41 +lemma nat_mod_lemma: assumes xyn: "[x = y] (mod n)" and xy:"y \<le> x"
1.42 + shows "\<exists>q. x = y + n * q"
1.43 +proof-
1.44 + from xy have th: "int x - int y = int (x - y)" by presburger
1.45 + from xyn have "int x mod int n = int y mod int n"
1.46 + by (simp add: modeq_def zmod_int[symmetric])
1.47 + hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])
1.48 + hence "n dvd x - y" by (simp add: th zdvd_int)
1.49 + then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
1.50 +qed
1.51 +
1.52 +lemma nat_mod: "[x = y] (mod n) \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
1.53 + (is "?lhs = ?rhs")
1.54 +proof
1.55 + assume H: "[x = y] (mod n)"
1.56 + {assume xy: "x \<le> y"
1.57 + from H have th: "[y = x] (mod n)" by (simp add: modeq_def)
1.58 + from nat_mod_lemma[OF th xy] have ?rhs
1.59 + apply clarify apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
1.60 + moreover
1.61 + {assume xy: "y \<le> x"
1.62 + from nat_mod_lemma[OF H xy] have ?rhs
1.63 + apply clarify apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
1.64 + ultimately show ?rhs using linear[of x y] by blast
1.65 +next
1.66 + assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
1.67 + hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
1.68 + thus ?lhs by (simp add: modeq_def)
1.69 +qed
1.70 +
1.71 +(* Lemmas about previously defined terms. *)
1.72 +
1.73 +lemma prime: "prime p \<longleftrightarrow> p \<noteq> 0 \<and> p\<noteq>1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
1.74 + (is "?lhs \<longleftrightarrow> ?rhs")
1.75 +proof-
1.76 + {assume "p=0 \<or> p=1" hence ?thesis using prime_0 prime_1 by (cases "p=0", simp_all)}
1.77 + moreover
1.78 + {assume p0: "p\<noteq>0" "p\<noteq>1"
1.79 + {assume H: "?lhs"
1.80 + {fix m assume m: "m > 0" "m < p"
1.81 + {assume "m=1" hence "coprime p m" by simp}
1.82 + moreover
1.83 + {assume "p dvd m" hence "p \<le> m" using dvd_imp_le m by blast with m(2)
1.84 + have "coprime p m" by simp}
1.85 + ultimately have "coprime p m" using prime_coprime[OF H, of m] by blast}
1.86 + hence ?rhs using p0 by auto}
1.87 + moreover
1.88 + { assume H: "\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m"
1.89 + from prime_factor[OF p0(2)] obtain q where q: "prime q" "q dvd p" by blast
1.90 + from prime_ge_2[OF q(1)] have q0: "q > 0" by arith
1.91 + from dvd_imp_le[OF q(2)] p0 have qp: "q \<le> p" by arith
1.92 + {assume "q = p" hence ?lhs using q(1) by blast}
1.93 + moreover
1.94 + {assume "q\<noteq>p" with qp have qplt: "q < p" by arith
1.95 + from H[rule_format, of q] qplt q0 have "coprime p q" by arith
1.96 + with coprime_prime[of p q q] q have False by simp hence ?lhs by blast}
1.97 + ultimately have ?lhs by blast}
1.98 + ultimately have ?thesis by blast}
1.99 + ultimately show ?thesis by (cases"p=0 \<or> p=1", auto)
1.100 +qed
1.101 +
1.102 +lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
1.103 +proof-
1.104 + have "{ m. 0 < m \<and> m < n } = {1..<n}" by auto
1.105 + thus ?thesis by simp
1.106 +qed
1.107 +
1.108 +lemma coprime_mod: assumes n: "n \<noteq> 0" shows "coprime (a mod n) n \<longleftrightarrow> coprime a n"
1.109 + using n dvd_mod_iff[of _ n a] by (auto simp add: coprime)
1.110 +
1.111 +(* Congruences. *)
1.112 +
1.113 +lemma cong_mod_01[simp,presburger]:
1.114 + "[x = y] (mod 0) \<longleftrightarrow> x = y" "[x = y] (mod 1)" "[x = 0] (mod n) \<longleftrightarrow> n dvd x"
1.115 + by (simp_all add: modeq_def, presburger)
1.116 +
1.117 +lemma cong_sub_cases:
1.118 + "[x = y] (mod n) \<longleftrightarrow> (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
1.119 +apply (auto simp add: nat_mod)
1.120 +apply (rule_tac x="q2" in exI)
1.121 +apply (rule_tac x="q1" in exI, simp)
1.122 +apply (rule_tac x="q2" in exI)
1.123 +apply (rule_tac x="q1" in exI, simp)
1.124 +apply (rule_tac x="q1" in exI)
1.125 +apply (rule_tac x="q2" in exI, simp)
1.126 +apply (rule_tac x="q1" in exI)
1.127 +apply (rule_tac x="q2" in exI, simp)
1.128 +done
1.129 +
1.130 +lemma cong_mult_lcancel: assumes an: "coprime a n" and axy:"[a * x = a * y] (mod n)"
1.131 + shows "[x = y] (mod n)"
1.132 +proof-
1.133 + {assume "a = 0" with an axy coprime_0'[of n] have ?thesis by (simp add: modeq_def) }
1.134 + moreover
1.135 + {assume az: "a\<noteq>0"
1.136 + {assume xy: "x \<le> y" hence axy': "a*x \<le> a*y" by simp
1.137 + with axy cong_sub_cases[of "a*x" "a*y" n] have "[a*(y - x) = 0] (mod n)"
1.138 + by (simp only: if_True diff_mult_distrib2)
1.139 + hence th: "n dvd a*(y -x)" by simp
1.140 + from coprime_divprod[OF th] an have "n dvd y - x"
1.141 + by (simp add: coprime_commute)
1.142 + hence ?thesis using xy cong_sub_cases[of x y n] by simp}
1.143 + moreover
1.144 + {assume H: "\<not>x \<le> y" hence xy: "y \<le> x" by arith
1.145 + from H az have axy': "\<not> a*x \<le> a*y" by auto
1.146 + with axy H cong_sub_cases[of "a*x" "a*y" n] have "[a*(x - y) = 0] (mod n)"
1.147 + by (simp only: if_False diff_mult_distrib2)
1.148 + hence th: "n dvd a*(x - y)" by simp
1.149 + from coprime_divprod[OF th] an have "n dvd x - y"
1.150 + by (simp add: coprime_commute)
1.151 + hence ?thesis using xy cong_sub_cases[of x y n] by simp}
1.152 + ultimately have ?thesis by blast}
1.153 + ultimately show ?thesis by blast
1.154 +qed
1.155 +
1.156 +lemma cong_mult_rcancel: assumes an: "coprime a n" and axy:"[x*a = y*a] (mod n)"
1.157 + shows "[x = y] (mod n)"
1.158 + using cong_mult_lcancel[OF an axy[unfolded mult_commute[of _a]]] .
1.159 +
1.160 +lemma cong_refl: "[x = x] (mod n)" by (simp add: modeq_def)
1.161 +
1.162 +lemma eq_imp_cong: "a = b \<Longrightarrow> [a = b] (mod n)" by (simp add: cong_refl)
1.163 +
1.164 +lemma cong_commute: "[x = y] (mod n) \<longleftrightarrow> [y = x] (mod n)"
1.165 + by (auto simp add: modeq_def)
1.166 +
1.167 +lemma cong_trans[trans]: "[x = y] (mod n) \<Longrightarrow> [y = z] (mod n) \<Longrightarrow> [x = z] (mod n)"
1.168 + by (simp add: modeq_def)
1.169 +
1.170 +lemma cong_add: assumes xx': "[x = x'] (mod n)" and yy':"[y = y'] (mod n)"
1.171 + shows "[x + y = x' + y'] (mod n)"
1.172 +proof-
1.173 + have "(x + y) mod n = (x mod n + y mod n) mod n"
1.174 + by (simp add: mod_add_left_eq[of x y n] mod_add_right_eq[of "x mod n" y n])
1.175 + also have "\<dots> = (x' mod n + y' mod n) mod n" using xx' yy' modeq_def by simp
1.176 + also have "\<dots> = (x' + y') mod n"
1.177 + by (simp add: mod_add_left_eq[of x' y' n] mod_add_right_eq[of "x' mod n" y' n])
1.178 + finally show ?thesis unfolding modeq_def .
1.179 +qed
1.180 +
1.181 +lemma cong_mult: assumes xx': "[x = x'] (mod n)" and yy':"[y = y'] (mod n)"
1.182 + shows "[x * y = x' * y'] (mod n)"
1.183 +proof-
1.184 + have "(x * y) mod n = (x mod n) * (y mod n) mod n"
1.185 + by (simp add: mod_mult1_eq'[of x y n] mod_mult1_eq[of "x mod n" y n])
1.186 + also have "\<dots> = (x' mod n) * (y' mod n) mod n" using xx'[unfolded modeq_def] yy'[unfolded modeq_def] by simp
1.187 + also have "\<dots> = (x' * y') mod n"
1.188 + by (simp add: mod_mult1_eq'[of x' y' n] mod_mult1_eq[of "x' mod n" y' n])
1.189 + finally show ?thesis unfolding modeq_def .
1.190 +qed
1.191 +
1.192 +lemma cong_exp: "[x = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
1.193 + by (induct k, auto simp add: cong_refl cong_mult)
1.194 +lemma cong_sub: assumes xx': "[x = x'] (mod n)" and yy': "[y = y'] (mod n)"
1.195 + and yx: "y <= x" and yx': "y' <= x'"
1.196 + shows "[x - y = x' - y'] (mod n)"
1.197 +proof-
1.198 + { fix x a x' a' y b y' b'
1.199 + have "(x::nat) + a = x' + a' \<Longrightarrow> y + b = y' + b' \<Longrightarrow> y <= x \<Longrightarrow> y' <= x'
1.200 + \<Longrightarrow> (x - y) + (a + b') = (x' - y') + (a' + b)" by arith}
1.201 + note th = this
1.202 + from xx' yy' obtain q1 q2 q1' q2' where q12: "x + n*q1 = x'+n*q2"
1.203 + and q12': "y + n*q1' = y'+n*q2'" unfolding nat_mod by blast+
1.204 + from th[OF q12 q12' yx yx']
1.205 + have "(x - y) + n*(q1 + q2') = (x' - y') + n*(q2 + q1')"
1.206 + by (simp add: right_distrib)
1.207 + thus ?thesis unfolding nat_mod by blast
1.208 +qed
1.209 +
1.210 +lemma cong_mult_lcancel_eq: assumes an: "coprime a n"
1.211 + shows "[a * x = a * y] (mod n) \<longleftrightarrow> [x = y] (mod n)" (is "?lhs \<longleftrightarrow> ?rhs")
1.212 +proof
1.213 + assume H: "?rhs" from cong_mult[OF cong_refl[of a n] H] show ?lhs .
1.214 +next
1.215 + assume H: "?lhs" hence H': "[x*a = y*a] (mod n)" by (simp add: mult_commute)
1.216 + from cong_mult_rcancel[OF an H'] show ?rhs .
1.217 +qed
1.218 +
1.219 +lemma cong_mult_rcancel_eq: assumes an: "coprime a n"
1.220 + shows "[x * a = y * a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.221 +using cong_mult_lcancel_eq[OF an, of x y] by (simp add: mult_commute)
1.222 +
1.223 +lemma cong_add_lcancel_eq: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.224 + by (simp add: nat_mod)
1.225 +
1.226 +lemma cong_add_rcancel_eq: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.227 + by (simp add: nat_mod)
1.228 +
1.229 +lemma cong_add_rcancel: "[x + a = y + a] (mod n) \<Longrightarrow> [x = y] (mod n)"
1.230 + by (simp add: nat_mod)
1.231 +
1.232 +lemma cong_add_lcancel: "[a + x = a + y] (mod n) \<Longrightarrow> [x = y] (mod n)"
1.233 + by (simp add: nat_mod)
1.234 +
1.235 +lemma cong_add_lcancel_eq_0: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.236 + by (simp add: nat_mod)
1.237 +
1.238 +lemma cong_add_rcancel_eq_0: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.239 + by (simp add: nat_mod)
1.240 +
1.241 +lemma cong_imp_eq: assumes xn: "x < n" and yn: "y < n" and xy: "[x = y] (mod n)"
1.242 + shows "x = y"
1.243 + using xy[unfolded modeq_def mod_less[OF xn] mod_less[OF yn]] .
1.244 +
1.245 +lemma cong_divides_modulus: "[x = y] (mod m) \<Longrightarrow> n dvd m ==> [x = y] (mod n)"
1.246 + apply (auto simp add: nat_mod dvd_def)
1.247 + apply (rule_tac x="k*q1" in exI)
1.248 + apply (rule_tac x="k*q2" in exI)
1.249 + by simp
1.250 +
1.251 +lemma cong_0_divides: "[x = 0] (mod n) \<longleftrightarrow> n dvd x" by simp
1.252 +
1.253 +lemma cong_1_divides:"[x = 1] (mod n) ==> n dvd x - 1"
1.254 + apply (cases "x\<le>1", simp_all)
1.255 + using cong_sub_cases[of x 1 n] by auto
1.256 +
1.257 +lemma cong_divides: "[x = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
1.258 +apply (auto simp add: nat_mod dvd_def)
1.259 +apply (rule_tac x="k + q1 - q2" in exI, simp add: add_mult_distrib2 diff_mult_distrib2)
1.260 +apply (rule_tac x="k + q2 - q1" in exI, simp add: add_mult_distrib2 diff_mult_distrib2)
1.261 +done
1.262 +
1.263 +lemma cong_coprime: assumes xy: "[x = y] (mod n)"
1.264 + shows "coprime n x \<longleftrightarrow> coprime n y"
1.265 +proof-
1.266 + {assume "n=0" hence ?thesis using xy by simp}
1.267 + moreover
1.268 + {assume nz: "n \<noteq> 0"
1.269 + have "coprime n x \<longleftrightarrow> coprime (x mod n) n"
1.270 + by (simp add: coprime_mod[OF nz, of x] coprime_commute[of n x])
1.271 + also have "\<dots> \<longleftrightarrow> coprime (y mod n) n" using xy[unfolded modeq_def] by simp
1.272 + also have "\<dots> \<longleftrightarrow> coprime y n" by (simp add: coprime_mod[OF nz, of y])
1.273 + finally have ?thesis by (simp add: coprime_commute) }
1.274 +ultimately show ?thesis by blast
1.275 +qed
1.276 +
1.277 +lemma cong_mod: "~(n = 0) \<Longrightarrow> [a mod n = a] (mod n)" by (simp add: modeq_def)
1.278 +
1.279 +lemma mod_mult_cong: "~(a = 0) \<Longrightarrow> ~(b = 0)
1.280 + \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
1.281 + by (simp add: modeq_def mod_mult2_eq mod_add_left_eq)
1.282 +
1.283 +lemma cong_mod_mult: "[x = y] (mod n) \<Longrightarrow> m dvd n \<Longrightarrow> [x = y] (mod m)"
1.284 + apply (auto simp add: nat_mod dvd_def)
1.285 + apply (rule_tac x="k*q1" in exI)
1.286 + apply (rule_tac x="k*q2" in exI, simp)
1.287 + done
1.288 +
1.289 +(* Some things when we know more about the order. *)
1.290 +
1.291 +lemma cong_le: "y <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
1.292 + using nat_mod_lemma[of x y n]
1.293 + apply auto
1.294 + apply (simp add: nat_mod)
1.295 + apply (rule_tac x="q" in exI)
1.296 + apply (rule_tac x="q + q" in exI)
1.297 + by (auto simp: ring_simps)
1.298 +
1.299 +lemma cong_to_1: "[a = 1] (mod n) \<longleftrightarrow> a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
1.300 +proof-
1.301 + {assume "n = 0 \<or> n = 1\<or> a = 0 \<or> a = 1" hence ?thesis
1.302 + apply (cases "n=0", simp_all add: cong_commute)
1.303 + apply (cases "n=1", simp_all add: cong_commute modeq_def)
1.304 + apply arith
1.305 + by (cases "a=1", simp_all add: modeq_def cong_commute)}
1.306 + moreover
1.307 + {assume n: "n\<noteq>0" "n\<noteq>1" and a:"a\<noteq>0" "a \<noteq> 1" hence a': "a \<ge> 1" by simp
1.308 + hence ?thesis using cong_le[OF a', of n] by auto }
1.309 + ultimately show ?thesis by auto
1.310 +qed
1.311 +
1.312 +(* Some basic theorems about solving congruences. *)
1.313 +
1.314 +
1.315 +lemma cong_solve: assumes an: "coprime a n" shows "\<exists>x. [a * x = b] (mod n)"
1.316 +proof-
1.317 + {assume "a=0" hence ?thesis using an by (simp add: modeq_def)}
1.318 + moreover
1.319 + {assume az: "a\<noteq>0"
1.320 + from bezout_add_strong[OF az, of n]
1.321 + obtain d x y where dxy: "d dvd a" "d dvd n" "a*x = n*y + d" by blast
1.322 + from an[unfolded coprime, rule_format, of d] dxy(1,2) have d1: "d = 1" by blast
1.323 + hence "a*x*b = (n*y + 1)*b" using dxy(3) by simp
1.324 + hence "a*(x*b) = n*(y*b) + b" by algebra
1.325 + hence "a*(x*b) mod n = (n*(y*b) + b) mod n" by simp
1.326 + hence "a*(x*b) mod n = b mod n" by (simp add: mod_add_left_eq)
1.327 + hence "[a*(x*b) = b] (mod n)" unfolding modeq_def .
1.328 + hence ?thesis by blast}
1.329 +ultimately show ?thesis by blast
1.330 +qed
1.331 +
1.332 +lemma cong_solve_unique: assumes an: "coprime a n" and nz: "n \<noteq> 0"
1.333 + shows "\<exists>!x. x < n \<and> [a * x = b] (mod n)"
1.334 +proof-
1.335 + let ?P = "\<lambda>x. x < n \<and> [a * x = b] (mod n)"
1.336 + from cong_solve[OF an] obtain x where x: "[a*x = b] (mod n)" by blast
1.337 + let ?x = "x mod n"
1.338 + from x have th: "[a * ?x = b] (mod n)"
1.339 + by (simp add: modeq_def mod_mult1_eq[of a x n])
1.340 + from mod_less_divisor[ of n x] nz th have Px: "?P ?x" by simp
1.341 + {fix y assume Py: "y < n" "[a * y = b] (mod n)"
1.342 + from Py(2) th have "[a * y = a*?x] (mod n)" by (simp add: modeq_def)
1.343 + hence "[y = ?x] (mod n)" by (simp add: cong_mult_lcancel_eq[OF an])
1.344 + with mod_less[OF Py(1)] mod_less_divisor[ of n x] nz
1.345 + have "y = ?x" by (simp add: modeq_def)}
1.346 + with Px show ?thesis by blast
1.347 +qed
1.348 +
1.349 +lemma cong_solve_unique_nontrivial:
1.350 + assumes p: "prime p" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p"
1.351 + shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
1.352 +proof-
1.353 + from p have p1: "p > 1" using prime_ge_2[OF p] by arith
1.354 + hence p01: "p \<noteq> 0" "p \<noteq> 1" by arith+
1.355 + from pa have ap: "coprime a p" by (simp add: coprime_commute)
1.356 + from prime_coprime[OF p, of x] dvd_imp_le[of p x] x0 xp have px:"coprime x p"
1.357 + by (auto simp add: coprime_commute)
1.358 + from cong_solve_unique[OF px p01(1)]
1.359 + obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y" by blast
1.360 + {assume y0: "y = 0"
1.361 + with y(2) have th: "p dvd a" by (simp add: cong_commute[of 0 a p])
1.362 + with p coprime_prime[OF pa, of p] have False by simp}
1.363 + with y show ?thesis unfolding Ex1_def using neq0_conv by blast
1.364 +qed
1.365 +lemma cong_unique_inverse_prime:
1.366 + assumes p: "prime p" and x0: "0 < x" and xp: "x < p"
1.367 + shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
1.368 + using cong_solve_unique_nontrivial[OF p coprime_1[of p] x0 xp] .
1.369 +
1.370 +(* Forms of the Chinese remainder theorem. *)
1.371 +
1.372 +lemma cong_chinese:
1.373 + assumes ab: "coprime a b" and xya: "[x = y] (mod a)"
1.374 + and xyb: "[x = y] (mod b)"
1.375 + shows "[x = y] (mod a*b)"
1.376 + using ab xya xyb
1.377 + by (simp add: cong_sub_cases[of x y a] cong_sub_cases[of x y b]
1.378 + cong_sub_cases[of x y "a*b"])
1.379 +(cases "x \<le> y", simp_all add: divides_mul[of a _ b])
1.380 +
1.381 +lemma chinese_remainder_unique:
1.382 + assumes ab: "coprime a b" and az: "a \<noteq> 0" and bz: "b\<noteq>0"
1.383 + shows "\<exists>!x. x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
1.384 +proof-
1.385 + from az bz have abpos: "a*b > 0" by simp
1.386 + from chinese_remainder[OF ab az bz] obtain x q1 q2 where
1.387 + xq12: "x = m + q1 * a" "x = n + q2 * b" by blast
1.388 + let ?w = "x mod (a*b)"
1.389 + have wab: "?w < a*b" by (simp add: mod_less_divisor[OF abpos])
1.390 + from xq12(1) have "?w mod a = ((m + q1 * a) mod (a*b)) mod a" by simp
1.391 + also have "\<dots> = m mod a" apply (simp add: mod_mult2_eq)
1.392 + apply (subst mod_add_left_eq)
1.393 + by simp
1.394 + finally have th1: "[?w = m] (mod a)" by (simp add: modeq_def)
1.395 + from xq12(2) have "?w mod b = ((n + q2 * b) mod (a*b)) mod b" by simp
1.396 + also have "\<dots> = ((n + q2 * b) mod (b*a)) mod b" by (simp add: mult_commute)
1.397 + also have "\<dots> = n mod b" apply (simp add: mod_mult2_eq)
1.398 + apply (subst mod_add_left_eq)
1.399 + by simp
1.400 + finally have th2: "[?w = n] (mod b)" by (simp add: modeq_def)
1.401 + {fix y assume H: "y < a*b" "[y = m] (mod a)" "[y = n] (mod b)"
1.402 + with th1 th2 have H': "[y = ?w] (mod a)" "[y = ?w] (mod b)"
1.403 + by (simp_all add: modeq_def)
1.404 + from cong_chinese[OF ab H'] mod_less[OF H(1)] mod_less[OF wab]
1.405 + have "y = ?w" by (simp add: modeq_def)}
1.406 + with th1 th2 wab show ?thesis by blast
1.407 +qed
1.408 +
1.409 +lemma chinese_remainder_coprime_unique:
1.410 + assumes ab: "coprime a b" and az: "a \<noteq> 0" and bz: "b \<noteq> 0"
1.411 + and ma: "coprime m a" and nb: "coprime n b"
1.412 + shows "\<exists>!x. coprime x (a * b) \<and> x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
1.413 +proof-
1.414 + let ?P = "\<lambda>x. x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
1.415 + from chinese_remainder_unique[OF ab az bz]
1.416 + obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)"
1.417 + "\<forall>y. ?P y \<longrightarrow> y = x" by blast
1.418 + from ma nb cong_coprime[OF x(2)] cong_coprime[OF x(3)]
1.419 + have "coprime x a" "coprime x b" by (simp_all add: coprime_commute)
1.420 + with coprime_mul[of x a b] have "coprime x (a*b)" by simp
1.421 + with x show ?thesis by blast
1.422 +qed
1.423 +
1.424 +(* Euler totient function. *)
1.425 +
1.426 +definition phi_def: "\<phi> n = card { m. 0 < m \<and> m <= n \<and> coprime m n }"
1.427 +lemma phi_0[simp]: "\<phi> 0 = 0"
1.428 + unfolding phi_def by (auto simp add: card_eq_0_iff)
1.429 +
1.430 +lemma phi_finite[simp]: "finite ({ m. 0 < m \<and> m <= n \<and> coprime m n })"
1.431 +proof-
1.432 + have "{ m. 0 < m \<and> m <= n \<and> coprime m n } \<subseteq> {0..n}" by auto
1.433 + thus ?thesis by (auto intro: finite_subset)
1.434 +qed
1.435 +
1.436 +declare coprime_1[presburger]
1.437 +lemma phi_1[simp]: "\<phi> 1 = 1"
1.438 +proof-
1.439 + {fix m
1.440 + have "0 < m \<and> m <= 1 \<and> coprime m 1 \<longleftrightarrow> m = 1" by presburger }
1.441 + thus ?thesis by (simp add: phi_def)
1.442 +qed
1.443 +
1.444 +lemma [simp]: "\<phi> (Suc 0) = Suc 0" using phi_1 by simp
1.445 +
1.446 +lemma phi_alt: "\<phi>(n) = card { m. coprime m n \<and> m < n}"
1.447 +proof-
1.448 + {assume "n=0 \<or> n=1" hence ?thesis by (cases "n=0", simp_all)}
1.449 + moreover
1.450 + {assume n: "n\<noteq>0" "n\<noteq>1"
1.451 + {fix m
1.452 + from n have "0 < m \<and> m <= n \<and> coprime m n \<longleftrightarrow> coprime m n \<and> m < n"
1.453 + apply (cases "m = 0", simp_all)
1.454 + apply (cases "m = 1", simp_all)
1.455 + apply (cases "m = n", auto)
1.456 + done }
1.457 + hence ?thesis unfolding phi_def by simp}
1.458 + ultimately show ?thesis by auto
1.459 +qed
1.460 +
1.461 +lemma phi_finite_lemma[simp]: "finite {m. coprime m n \<and> m < n}" (is "finite ?S")
1.462 + by (rule finite_subset[of "?S" "{0..n}"], auto)
1.463 +
1.464 +lemma phi_another: assumes n: "n\<noteq>1"
1.465 + shows "\<phi> n = card {m. 0 < m \<and> m < n \<and> coprime m n }"
1.466 +proof-
1.467 + {fix m
1.468 + from n have "0 < m \<and> m < n \<and> coprime m n \<longleftrightarrow> coprime m n \<and> m < n"
1.469 + by (cases "m=0", auto)}
1.470 + thus ?thesis unfolding phi_alt by auto
1.471 +qed
1.472 +
1.473 +lemma phi_limit: "\<phi> n \<le> n"
1.474 +proof-
1.475 + have "{ m. coprime m n \<and> m < n} \<subseteq> {0 ..<n}" by auto
1.476 + with card_mono[of "{0 ..<n}" "{ m. coprime m n \<and> m < n}"]
1.477 + show ?thesis unfolding phi_alt by auto
1.478 +qed
1.479 +
1.480 +lemma stupid[simp]: "{m. (0::nat) < m \<and> m < n} = {1..<n}"
1.481 + by auto
1.482 +
1.483 +lemma phi_limit_strong: assumes n: "n\<noteq>1"
1.484 + shows "\<phi>(n) \<le> n - 1"
1.485 +proof-
1.486 + show ?thesis
1.487 + unfolding phi_another[OF n] finite_number_segment[of n, symmetric]
1.488 + by (rule card_mono[of "{m. 0 < m \<and> m < n}" "{m. 0 < m \<and> m < n \<and> coprime m n}"], auto)
1.489 +qed
1.490 +
1.491 +lemma phi_lowerbound_1_strong: assumes n: "n \<ge> 1"
1.492 + shows "\<phi>(n) \<ge> 1"
1.493 +proof-
1.494 + let ?S = "{ m. 0 < m \<and> m <= n \<and> coprime m n }"
1.495 + from card_0_eq[of ?S] n have "\<phi> n \<noteq> 0" unfolding phi_alt
1.496 + apply auto
1.497 + apply (cases "n=1", simp_all)
1.498 + apply (rule exI[where x=1], simp)
1.499 + done
1.500 + thus ?thesis by arith
1.501 +qed
1.502 +
1.503 +lemma phi_lowerbound_1: "2 <= n ==> 1 <= \<phi>(n)"
1.504 + using phi_lowerbound_1_strong[of n] by auto
1.505 +
1.506 +lemma phi_lowerbound_2: assumes n: "3 <= n" shows "2 <= \<phi> (n)"
1.507 +proof-
1.508 + let ?S = "{ m. 0 < m \<and> m <= n \<and> coprime m n }"
1.509 + have inS: "{1, n - 1} \<subseteq> ?S" using n coprime_plus1[of "n - 1"]
1.510 + by (auto simp add: coprime_commute)
1.511 + from n have c2: "card {1, n - 1} = 2" by (auto simp add: card_insert_if)
1.512 + from card_mono[of ?S "{1, n - 1}", simplified inS c2] show ?thesis
1.513 + unfolding phi_def by auto
1.514 +qed
1.515 +
1.516 +lemma phi_prime: "\<phi> n = n - 1 \<and> n\<noteq>0 \<and> n\<noteq>1 \<longleftrightarrow> prime n"
1.517 +proof-
1.518 + {assume "n=0 \<or> n=1" hence ?thesis by (cases "n=1", simp_all)}
1.519 + moreover
1.520 + {assume n: "n\<noteq>0" "n\<noteq>1"
1.521 + let ?S = "{m. 0 < m \<and> m < n}"
1.522 + have fS: "finite ?S" by simp
1.523 + let ?S' = "{m. 0 < m \<and> m < n \<and> coprime m n}"
1.524 + have fS':"finite ?S'" apply (rule finite_subset[of ?S' ?S]) by auto
1.525 + {assume H: "\<phi> n = n - 1 \<and> n\<noteq>0 \<and> n\<noteq>1"
1.526 + hence ceq: "card ?S' = card ?S"
1.527 + using n finite_number_segment[of n] phi_another[OF n(2)] by simp
1.528 + {fix m assume m: "0 < m" "m < n" "\<not> coprime m n"
1.529 + hence mS': "m \<notin> ?S'" by auto
1.530 + have "insert m ?S' \<le> ?S" using m by auto
1.531 + from m have "card (insert m ?S') \<le> card ?S"
1.532 + by - (rule card_mono[of ?S "insert m ?S'"], auto)
1.533 + hence False
1.534 + unfolding card_insert_disjoint[of "?S'" m, OF fS' mS'] ceq
1.535 + by simp }
1.536 + hence "\<forall>m. 0 <m \<and> m < n \<longrightarrow> coprime m n" by blast
1.537 + hence "prime n" unfolding prime using n by (simp add: coprime_commute)}
1.538 + moreover
1.539 + {assume H: "prime n"
1.540 + hence "?S = ?S'" unfolding prime using n
1.541 + by (auto simp add: coprime_commute)
1.542 + hence "card ?S = card ?S'" by simp
1.543 + hence "\<phi> n = n - 1" unfolding phi_another[OF n(2)] by simp}
1.544 + ultimately have ?thesis using n by blast}
1.545 + ultimately show ?thesis by (cases "n=0") blast+
1.546 +qed
1.547 +
1.548 +(* Multiplicativity property. *)
1.549 +
1.550 +lemma phi_multiplicative: assumes ab: "coprime a b"
1.551 + shows "\<phi> (a * b) = \<phi> a * \<phi> b"
1.552 +proof-
1.553 + {assume "a = 0 \<or> b = 0 \<or> a = 1 \<or> b = 1"
1.554 + hence ?thesis
1.555 + by (cases "a=0", simp, cases "b=0", simp, cases"a=1", simp_all) }
1.556 + moreover
1.557 + {assume a: "a\<noteq>0" "a\<noteq>1" and b: "b\<noteq>0" "b\<noteq>1"
1.558 + hence ab0: "a*b \<noteq> 0" by simp
1.559 + let ?S = "\<lambda>k. {m. coprime m k \<and> m < k}"
1.560 + let ?f = "\<lambda>x. (x mod a, x mod b)"
1.561 + have eq: "?f ` (?S (a*b)) = (?S a \<times> ?S b)"
1.562 + proof-
1.563 + {fix x assume x:"x \<in> ?S (a*b)"
1.564 + hence x': "coprime x (a*b)" "x < a*b" by simp_all
1.565 + hence xab: "coprime x a" "coprime x b" by (simp_all add: coprime_mul_eq)
1.566 + from mod_less_divisor a b have xab':"x mod a < a" "x mod b < b" by auto
1.567 + from xab xab' have "?f x \<in> (?S a \<times> ?S b)"
1.568 + by (simp add: coprime_mod[OF a(1)] coprime_mod[OF b(1)])}
1.569 + moreover
1.570 + {fix x y assume x: "x \<in> ?S a" and y: "y \<in> ?S b"
1.571 + hence x': "coprime x a" "x < a" and y': "coprime y b" "y < b" by simp_all
1.572 + from chinese_remainder_coprime_unique[OF ab a(1) b(1) x'(1) y'(1)]
1.573 + obtain z where z: "coprime z (a * b)" "z < a * b" "[z = x] (mod a)"
1.574 + "[z = y] (mod b)" by blast
1.575 + hence "(x,y) \<in> ?f ` (?S (a*b))"
1.576 + using y'(2) mod_less_divisor[of b y] x'(2) mod_less_divisor[of a x]
1.577 + by (auto simp add: image_iff modeq_def)}
1.578 + ultimately show ?thesis by auto
1.579 + qed
1.580 + have finj: "inj_on ?f (?S (a*b))"
1.581 + unfolding inj_on_def
1.582 + proof(clarify)
1.583 + fix x y assume H: "coprime x (a * b)" "x < a * b" "coprime y (a * b)"
1.584 + "y < a * b" "x mod a = y mod a" "x mod b = y mod b"
1.585 + hence cp: "coprime x a" "coprime x b" "coprime y a" "coprime y b"
1.586 + by (simp_all add: coprime_mul_eq)
1.587 + from chinese_remainder_coprime_unique[OF ab a(1) b(1) cp(3,4)] H
1.588 + show "x = y" unfolding modeq_def by blast
1.589 + qed
1.590 + from card_image[OF finj, unfolded eq] have ?thesis
1.591 + unfolding phi_alt by simp }
1.592 + ultimately show ?thesis by auto
1.593 +qed
1.594 +
1.595 +(* Fermat's Little theorem / Fermat-Euler theorem. *)
1.596 +
1.597 +lemma (in comm_monoid_mult) fold_related:
1.598 + assumes Re: "R e e"
1.599 + and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)"
1.600 + and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
1.601 + shows "R (fold (op *) h e S) (fold (op *) g e S)"
1.602 + using prems
1.603 + by -(rule finite_subset_induct,auto)
1.604 +
1.605 +
1.606 +lemma nproduct_mod:
1.607 + assumes fS: "finite S" and n0: "n \<noteq> 0"
1.608 + shows "[setprod (\<lambda>m. a(m) mod n) S = setprod a S] (mod n)"
1.609 +proof-
1.610 + have th1:"[1 = 1] (mod n)" by (simp add: modeq_def)
1.611 + from cong_mult
1.612 + have th3:"\<forall>x1 y1 x2 y2.
1.613 + [x1 = x2] (mod n) \<and> [y1 = y2] (mod n) \<longrightarrow> [x1 * y1 = x2 * y2] (mod n)"
1.614 + by blast
1.615 + have th4:"\<forall>x\<in>S. [a x mod n = a x] (mod n)" by (simp add: modeq_def)
1.616 + from fold_related[where h="(\<lambda>m. a(m) mod n)" and g=a, OF th1 th3 fS, OF th4] show ?thesis unfolding setprod_def by (simp add: fS)
1.617 +qed
1.618 +
1.619 +lemma nproduct_cmul:
1.620 + assumes fS:"finite S"
1.621 + shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult,recpower})* a(m)) S = c ^ (card S) * setprod a S"
1.622 +unfolding setprod_timesf setprod_constant[OF fS, of c] ..
1.623 +
1.624 +lemma coprime_nproduct:
1.625 + assumes fS: "finite S" and Sn: "\<forall>x\<in>S. coprime n (a x)"
1.626 + shows "coprime n (setprod a S)"
1.627 + using fS Sn
1.628 +unfolding setprod_def
1.629 +apply -
1.630 +apply (rule finite_subset_induct)
1.631 +by (auto simp add: coprime_mul)
1.632 +
1.633 +lemma (in comm_monoid_mult)
1.634 + fold_eq_general:
1.635 + assumes fS: "finite S"
1.636 + and h: "\<forall>y\<in>S'. \<exists>!x. x\<in> S \<and> h(x) = y"
1.637 + and f12: "\<forall>x\<in>S. h x \<in> S' \<and> f2(h x) = f1 x"
1.638 + shows "fold (op *) f1 e S = fold (op *) f2 e S'"
1.639 +proof-
1.640 + from h f12 have hS: "h ` S = S'" by auto
1.641 + {fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y"
1.642 + from f12 h H have "x = y" by auto }
1.643 + hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast
1.644 + from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto
1.645 + from hS have "fold (op *) f2 e S' = fold (op *) f2 e (h ` S)" by simp
1.646 + also have "\<dots> = fold (op *) (f2 o h) e S"
1.647 + using fold_reindex[OF fS hinj, of f2 e] .
1.648 + also have "\<dots> = fold (op *) f1 e S " using th fold_cong[OF fS, of "f2 o h" f1 e]
1.649 + by blast
1.650 + finally show ?thesis ..
1.651 +qed
1.652 +
1.653 +lemma fermat_little: assumes an: "coprime a n"
1.654 + shows "[a ^ (\<phi> n) = 1] (mod n)"
1.655 +proof-
1.656 + {assume "n=0" hence ?thesis by simp}
1.657 + moreover
1.658 + {assume "n=1" hence ?thesis by (simp add: modeq_def)}
1.659 + moreover
1.660 + {assume nz: "n \<noteq> 0" and n1: "n \<noteq> 1"
1.661 + let ?S = "{m. coprime m n \<and> m < n}"
1.662 + let ?P = "\<Prod> ?S"
1.663 + have fS: "finite ?S" by simp
1.664 + have cardfS: "\<phi> n = card ?S" unfolding phi_alt ..
1.665 + {fix m assume m: "m \<in> ?S"
1.666 + hence "coprime m n" by simp
1.667 + with coprime_mul[of n a m] an have "coprime (a*m) n"
1.668 + by (simp add: coprime_commute)}
1.669 + hence Sn: "\<forall>m\<in> ?S. coprime (a*m) n " by blast
1.670 + from coprime_nproduct[OF fS, of n "\<lambda>m. m"] have nP:"coprime ?P n"
1.671 + by (simp add: coprime_commute)
1.672 + have Paphi: "[?P*a^ (\<phi> n) = ?P*1] (mod n)"
1.673 + proof-
1.674 + let ?h = "\<lambda>m. m mod n"
1.675 + {fix m assume mS: "m\<in> ?S"
1.676 + hence "?h m \<in> ?S" by simp}
1.677 + hence hS: "?h ` ?S = ?S"by (auto simp add: image_iff)
1.678 + have "a\<noteq>0" using an n1 nz apply- apply (rule ccontr) by simp
1.679 + hence inj: "inj_on (op * a) ?S" unfolding inj_on_def by simp
1.680 +
1.681 + have eq0: "fold op * (?h \<circ> op * a) 1 {m. coprime m n \<and> m < n} =
1.682 + fold op * (\<lambda>m. m) 1 {m. coprime m n \<and> m < n}"
1.683 + proof (rule fold_eq_general[where h="?h o (op * a)"])
1.684 + show "finite ?S" using fS .
1.685 + next
1.686 + {fix y assume yS: "y \<in> ?S" hence y: "coprime y n" "y < n" by simp_all
1.687 + from cong_solve_unique[OF an nz, of y]
1.688 + obtain x where x:"x < n" "[a * x = y] (mod n)" "\<forall>z. z < n \<and> [a * z = y] (mod n) \<longrightarrow> z=x" by blast
1.689 + from cong_coprime[OF x(2)] y(1)
1.690 + have xm: "coprime x n" by (simp add: coprime_mul_eq coprime_commute)
1.691 + {fix z assume "z \<in> ?S" "(?h \<circ> op * a) z = y"
1.692 + hence z: "coprime z n" "z < n" "(?h \<circ> op * a) z = y" by simp_all
1.693 + from x(3)[rule_format, of z] z(2,3) have "z=x"
1.694 + unfolding modeq_def mod_less[OF y(2)] by simp}
1.695 + with xm x(1,2) have "\<exists>!x. x \<in> ?S \<and> (?h \<circ> op * a) x = y"
1.696 + unfolding modeq_def mod_less[OF y(2)] by auto }
1.697 + thus "\<forall>y\<in>{m. coprime m n \<and> m < n}.
1.698 + \<exists>!x. x \<in> {m. coprime m n \<and> m < n} \<and> ((\<lambda>m. m mod n) \<circ> op * a) x = y" by blast
1.699 + next
1.700 + {fix x assume xS: "x\<in> ?S"
1.701 + hence x: "coprime x n" "x < n" by simp_all
1.702 + with an have "coprime (a*x) n"
1.703 + by (simp add: coprime_mul_eq[of n a x] coprime_commute)
1.704 + hence "?h (a*x) \<in> ?S" using nz
1.705 + by (simp add: coprime_mod[OF nz] mod_less_divisor)}
1.706 + thus " \<forall>x\<in>{m. coprime m n \<and> m < n}.
1.707 + ((\<lambda>m. m mod n) \<circ> op * a) x \<in> {m. coprime m n \<and> m < n} \<and>
1.708 + ((\<lambda>m. m mod n) \<circ> op * a) x = ((\<lambda>m. m mod n) \<circ> op * a) x" by simp
1.709 + qed
1.710 + from nproduct_mod[OF fS nz, of "op * a"]
1.711 + have "[(setprod (op *a) ?S) = (setprod (?h o (op * a)) ?S)] (mod n)"
1.712 + unfolding o_def
1.713 + by (simp add: cong_commute)
1.714 + also have "[setprod (?h o (op * a)) ?S = ?P ] (mod n)"
1.715 + using eq0 fS an by (simp add: setprod_def modeq_def o_def)
1.716 + finally show "[?P*a^ (\<phi> n) = ?P*1] (mod n)"
1.717 + unfolding cardfS mult_commute[of ?P "a^ (card ?S)"]
1.718 + nproduct_cmul[OF fS, symmetric] mult_1_right by simp
1.719 + qed
1.720 + from cong_mult_lcancel[OF nP Paphi] have ?thesis . }
1.721 + ultimately show ?thesis by blast
1.722 +qed
1.723 +
1.724 +lemma fermat_little_prime: assumes p: "prime p" and ap: "coprime a p"
1.725 + shows "[a^ (p - 1) = 1] (mod p)"
1.726 + using fermat_little[OF ap] p[unfolded phi_prime[symmetric]]
1.727 +by simp
1.728 +
1.729 +
1.730 +(* Lucas's theorem. *)
1.731 +
1.732 +lemma lucas_coprime_lemma:
1.733 + assumes m: "m\<noteq>0" and am: "[a^m = 1] (mod n)"
1.734 + shows "coprime a n"
1.735 +proof-
1.736 + {assume "n=1" hence ?thesis by simp}
1.737 + moreover
1.738 + {assume "n = 0" hence ?thesis using am m exp_eq_1[of a m] by simp}
1.739 + moreover
1.740 + {assume n: "n\<noteq>0" "n\<noteq>1"
1.741 + from m obtain m' where m': "m = Suc m'" by (cases m, blast+)
1.742 + {fix d
1.743 + assume d: "d dvd a" "d dvd n"
1.744 + from n have n1: "1 < n" by arith
1.745 + from am mod_less[OF n1] have am1: "a^m mod n = 1" unfolding modeq_def by simp
1.746 + from dvd_mult2[OF d(1), of "a^m'"] have dam:"d dvd a^m" by (simp add: m')
1.747 + from dvd_mod_iff[OF d(2), of "a^m"] dam am1
1.748 + have "d = 1" by simp }
1.749 + hence ?thesis unfolding coprime by auto
1.750 + }
1.751 + ultimately show ?thesis by blast
1.752 +qed
1.753 +
1.754 +lemma lucas_weak:
1.755 + assumes n: "n \<ge> 2" and an:"[a^(n - 1) = 1] (mod n)"
1.756 + and nm: "\<forall>m. 0 <m \<and> m < n - 1 \<longrightarrow> \<not> [a^m = 1] (mod n)"
1.757 + shows "prime n"
1.758 +proof-
1.759 + from n have n1: "n \<noteq> 1" "n\<noteq>0" "n - 1 \<noteq> 0" "n - 1 > 0" "n - 1 < n" by arith+
1.760 + from lucas_coprime_lemma[OF n1(3) an] have can: "coprime a n" .
1.761 + from fermat_little[OF can] have afn: "[a ^ \<phi> n = 1] (mod n)" .
1.762 + {assume "\<phi> n \<noteq> n - 1"
1.763 + with phi_limit_strong[OF n1(1)] phi_lowerbound_1[OF n]
1.764 + have c:"\<phi> n > 0 \<and> \<phi> n < n - 1" by arith
1.765 + from nm[rule_format, OF c] afn have False ..}
1.766 + hence "\<phi> n = n - 1" by blast
1.767 + with phi_prime[of n] n1(1,2) show ?thesis by simp
1.768 +qed
1.769 +
1.770 +lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"
1.771 + (is "?lhs \<longleftrightarrow> ?rhs")
1.772 +proof
1.773 + assume ?rhs thus ?lhs by blast
1.774 +next
1.775 + assume H: ?lhs then obtain n where n: "P n" by blast
1.776 + let ?x = "Least P"
1.777 + {fix m assume m: "m < ?x"
1.778 + from not_less_Least[OF m] have "\<not> P m" .}
1.779 + with LeastI_ex[OF H] show ?rhs by blast
1.780 +qed
1.781 +
1.782 +lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> (P (Least P) \<and> (\<forall>m < (Least P). \<not> P m))"
1.783 + (is "?lhs \<longleftrightarrow> ?rhs")
1.784 +proof-
1.785 + {assume ?rhs hence ?lhs by blast}
1.786 + moreover
1.787 + { assume H: ?lhs then obtain n where n: "P n" by blast
1.788 + let ?x = "Least P"
1.789 + {fix m assume m: "m < ?x"
1.790 + from not_less_Least[OF m] have "\<not> P m" .}
1.791 + with LeastI_ex[OF H] have ?rhs by blast}
1.792 + ultimately show ?thesis by blast
1.793 +qed
1.794 +
1.795 +lemma power_mod: "((x::nat) mod m)^n mod m = x^n mod m"
1.796 +proof(induct n)
1.797 + case 0 thus ?case by simp
1.798 +next
1.799 + case (Suc n)
1.800 + have "(x mod m)^(Suc n) mod m = ((x mod m) * (((x mod m) ^ n) mod m)) mod m"
1.801 + by (simp add: mod_mult1_eq[symmetric])
1.802 + also have "\<dots> = ((x mod m) * (x^n mod m)) mod m" using Suc.hyps by simp
1.803 + also have "\<dots> = x^(Suc n) mod m"
1.804 + by (simp add: mod_mult1_eq'[symmetric] mod_mult1_eq[symmetric])
1.805 + finally show ?case .
1.806 +qed
1.807 +
1.808 +lemma lucas:
1.809 + assumes n2: "n \<ge> 2" and an1: "[a^(n - 1) = 1] (mod n)"
1.810 + and pn: "\<forall>p. prime p \<and> p dvd n - 1 \<longrightarrow> \<not> [a^((n - 1) div p) = 1] (mod n)"
1.811 + shows "prime n"
1.812 +proof-
1.813 + from n2 have n01: "n\<noteq>0" "n\<noteq>1" "n - 1 \<noteq> 0" by arith+
1.814 + from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1" by simp
1.815 + from lucas_coprime_lemma[OF n01(3) an1] cong_coprime[OF an1]
1.816 + have an: "coprime a n" "coprime (a^(n - 1)) n" by (simp_all add: coprime_commute)
1.817 + {assume H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
1.818 + from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
1.819 + m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k" by blast
1.820 + {assume nm1: "(n - 1) mod m > 0"
1.821 + from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast
1.822 + let ?y = "a^ ((n - 1) div m * m)"
1.823 + note mdeq = mod_div_equality[of "(n - 1)" m]
1.824 + from coprime_exp[OF an(1)[unfolded coprime_commute[of a n]],
1.825 + of "(n - 1) div m * m"]
1.826 + have yn: "coprime ?y n" by (simp add: coprime_commute)
1.827 + have "?y mod n = (a^m)^((n - 1) div m) mod n"
1.828 + by (simp add: ring_simps power_mult)
1.829 + also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n"
1.830 + using power_mod[of "a^m" n "(n - 1) div m"] by simp
1.831 + also have "\<dots> = 1" using m(3)[unfolded modeq_def onen] onen by simp
1.832 + finally have th3: "?y mod n = 1" .
1.833 + have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
1.834 + using an1[unfolded modeq_def onen] onen
1.835 + mod_div_equality[of "(n - 1)" m, symmetric]
1.836 + by (simp add:power_add[symmetric] modeq_def th3 del: One_nat_def)
1.837 + from cong_mult_lcancel[of ?y n "a^((n - 1) mod m)" 1, OF yn th2]
1.838 + have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)" .
1.839 + from m(4)[rule_format, OF th0] nm1
1.840 + less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] th1
1.841 + have False by blast }
1.842 + hence "(n - 1) mod m = 0" by auto
1.843 + then have mn: "m dvd n - 1" by presburger
1.844 + then obtain r where r: "n - 1 = m*r" unfolding dvd_def by blast
1.845 + from n01 r m(2) have r01: "r\<noteq>0" "r\<noteq>1" by - (rule ccontr, simp)+
1.846 + from prime_factor[OF r01(2)] obtain p where p: "prime p" "p dvd r" by blast
1.847 + hence th: "prime p \<and> p dvd n - 1" unfolding r by (auto intro: dvd_mult)
1.848 + have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r
1.849 + by (simp add: power_mult)
1.850 + also have "\<dots> = (a^(m*(r div p))) mod n" using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] by simp
1.851 + also have "\<dots> = ((a^m)^(r div p)) mod n" by (simp add: power_mult)
1.852 + also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod[of "a^m" "n" "r div p" ] ..
1.853 + also have "\<dots> = 1" using m(3) onen by (simp add: modeq_def)
1.854 + finally have "[(a ^ ((n - 1) div p))= 1] (mod n)"
1.855 + using onen by (simp add: modeq_def)
1.856 + with pn[rule_format, OF th] have False by blast}
1.857 + hence th: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" by blast
1.858 + from lucas_weak[OF n2 an1 th] show ?thesis .
1.859 +qed
1.860 +
1.861 +(* Definition of the order of a number mod n (0 in non-coprime case). *)
1.862 +
1.863 +definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)"
1.864 +
1.865 +(* This has the expected properties. *)
1.866 +
1.867 +lemma coprime_ord:
1.868 + assumes na: "coprime n a"
1.869 + shows "ord n a > 0 \<and> [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.870 +proof-
1.871 + let ?P = "\<lambda>d. 0 < d \<and> [a ^ d = 1] (mod n)"
1.872 + from euclid[of a] obtain p where p: "prime p" "a < p" by blast
1.873 + from na have o: "ord n a = Least ?P" by (simp add: ord_def)
1.874 + {assume "n=0 \<or> n=1" with na have "\<exists>m>0. ?P m" apply auto apply (rule exI[where x=1]) by (simp add: modeq_def)}
1.875 + moreover
1.876 + {assume "n\<noteq>0 \<and> n\<noteq>1" hence n2:"n \<ge> 2" by arith
1.877 + from na have na': "coprime a n" by (simp add: coprime_commute)
1.878 + from phi_lowerbound_1[OF n2] fermat_little[OF na']
1.879 + have ex: "\<exists>m>0. ?P m" by - (rule exI[where x="\<phi> n"], auto) }
1.880 + ultimately have ex: "\<exists>m>0. ?P m" by blast
1.881 + from nat_exists_least_iff'[of ?P] ex na show ?thesis
1.882 + unfolding o[symmetric] by auto
1.883 +qed
1.884 +(* With the special value 0 for non-coprime case, it's more convenient. *)
1.885 +lemma ord_works:
1.886 + "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> ~[a^ m = 1] (mod n))"
1.887 +apply (cases "coprime n a")
1.888 +using coprime_ord[of n a]
1.889 +by (blast, simp add: ord_def modeq_def)
1.890 +
1.891 +lemma ord: "[a^(ord n a) = 1] (mod n)" using ord_works by blast
1.892 +lemma ord_minimal: "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> ~[a^m = 1] (mod n)"
1.893 + using ord_works by blast
1.894 +lemma ord_eq_0: "ord n a = 0 \<longleftrightarrow> ~coprime n a"
1.895 +by (cases "coprime n a", simp add: neq0_conv coprime_ord, simp add: neq0_conv ord_def)
1.896 +
1.897 +lemma ord_divides:
1.898 + "[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d" (is "?lhs \<longleftrightarrow> ?rhs")
1.899 +proof
1.900 + assume rh: ?rhs
1.901 + then obtain k where "d = ord n a * k" unfolding dvd_def by blast
1.902 + hence "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)"
1.903 + by (simp add : modeq_def power_mult power_mod)
1.904 + also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)"
1.905 + using ord[of a n, unfolded modeq_def] by (simp add: modeq_def power_mod)
1.906 + finally show ?lhs .
1.907 +next
1.908 + assume lh: ?lhs
1.909 + { assume H: "\<not> coprime n a"
1.910 + hence o: "ord n a = 0" by (simp add: ord_def)
1.911 + {assume d: "d=0" with o H have ?rhs by (simp add: modeq_def)}
1.912 + moreover
1.913 + {assume d0: "d\<noteq>0" then obtain d' where d': "d = Suc d'" by (cases d, auto)
1.914 + from H[unfolded coprime]
1.915 + obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
1.916 + from lh[unfolded nat_mod]
1.917 + obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2" by blast
1.918 + hence "a ^ d + n * q1 - n * q2 = 1" by simp
1.919 + with dvd_diff [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp
1.920 + with p(3) have False by simp
1.921 + hence ?rhs ..}
1.922 + ultimately have ?rhs by blast}
1.923 + moreover
1.924 + {assume H: "coprime n a"
1.925 + let ?o = "ord n a"
1.926 + let ?q = "d div ord n a"
1.927 + let ?r = "d mod ord n a"
1.928 + from cong_exp[OF ord[of a n], of ?q]
1.929 + have eqo: "[(a^?o)^?q = 1] (mod n)" by (simp add: modeq_def)
1.930 + from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
1.931 + hence op: "?o > 0" by simp
1.932 + from mod_div_equality[of d "ord n a"] lh
1.933 + have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: modeq_def mult_commute)
1.934 + hence "[(a^?o)^?q * (a^?r) = 1] (mod n)"
1.935 + by (simp add: modeq_def power_mult[symmetric] power_add[symmetric])
1.936 + hence th: "[a^?r = 1] (mod n)"
1.937 + using eqo mod_mult1_eq'[of "(a^?o)^?q" "a^?r" n]
1.938 + apply (simp add: modeq_def del: One_nat_def)
1.939 + by (simp add: mod_mult1_eq'[symmetric])
1.940 + {assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)}
1.941 + moreover
1.942 + {assume r: "?r \<noteq> 0"
1.943 + with mod_less_divisor[OF op, of d] have r0o:"?r >0 \<and> ?r < ?o" by simp
1.944 + from conjunct2[OF ord_works[of a n], rule_format, OF r0o] th
1.945 + have ?rhs by blast}
1.946 + ultimately have ?rhs by blast}
1.947 + ultimately show ?rhs by blast
1.948 +qed
1.949 +
1.950 +lemma order_divides_phi: "coprime n a \<Longrightarrow> ord n a dvd \<phi> n"
1.951 +using ord_divides fermat_little coprime_commute by simp
1.952 +lemma order_divides_expdiff:
1.953 + assumes na: "coprime n a"
1.954 + shows "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
1.955 +proof-
1.956 + {fix n a d e
1.957 + assume na: "coprime n a" and ed: "(e::nat) \<le> d"
1.958 + hence "\<exists>c. d = e + c" by arith
1.959 + then obtain c where c: "d = e + c" by arith
1.960 + from na have an: "coprime a n" by (simp add: coprime_commute)
1.961 + from coprime_exp[OF na, of e]
1.962 + have aen: "coprime (a^e) n" by (simp add: coprime_commute)
1.963 + from coprime_exp[OF na, of c]
1.964 + have acn: "coprime (a^c) n" by (simp add: coprime_commute)
1.965 + have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
1.966 + using c by simp
1.967 + also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
1.968 + also have "\<dots> \<longleftrightarrow> [a ^ c = 1] (mod n)"
1.969 + using cong_mult_lcancel_eq[OF aen, of "a^c" "a^0"] by simp
1.970 + also have "\<dots> \<longleftrightarrow> ord n a dvd c" by (simp only: ord_divides)
1.971 + also have "\<dots> \<longleftrightarrow> [e + c = e + 0] (mod ord n a)"
1.972 + using cong_add_lcancel_eq[of e c 0 "ord n a", simplified cong_0_divides]
1.973 + by simp
1.974 + finally have "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
1.975 + using c by simp }
1.976 + note th = this
1.977 + have "e \<le> d \<or> d \<le> e" by arith
1.978 + moreover
1.979 + {assume ed: "e \<le> d" from th[OF na ed] have ?thesis .}
1.980 + moreover
1.981 + {assume de: "d \<le> e"
1.982 + from th[OF na de] have ?thesis by (simp add: cong_commute) }
1.983 + ultimately show ?thesis by blast
1.984 +qed
1.985 +
1.986 +(* Another trivial primality characterization. *)
1.987 +
1.988 +lemma prime_prime_factor:
1.989 + "prime n \<longleftrightarrow> n \<noteq> 1\<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)"
1.990 +proof-
1.991 + {assume n: "n=0 \<or> n=1" hence ?thesis using prime_0 two_is_prime by auto}
1.992 + moreover
1.993 + {assume n: "n\<noteq>0" "n\<noteq>1"
1.994 + {assume pn: "prime n"
1.995 +
1.996 + from pn[unfolded prime_def] have "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n"
1.997 + using n
1.998 + apply (cases "n = 0 \<or> n=1",simp)
1.999 + by (clarsimp, erule_tac x="p" in allE, auto)}
1.1000 + moreover
1.1001 + {assume H: "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n"
1.1002 + from n have n1: "n > 1" by arith
1.1003 + {fix m assume m: "m dvd n" "m\<noteq>1"
1.1004 + from prime_factor[OF m(2)] obtain p where
1.1005 + p: "prime p" "p dvd m" by blast
1.1006 + from dvd_trans[OF p(2) m(1)] p(1) H have "p = n" by blast
1.1007 + with p(2) have "n dvd m" by simp
1.1008 + hence "m=n" using dvd_anti_sym[OF m(1)] by simp }
1.1009 + with n1 have "prime n" unfolding prime_def by auto }
1.1010 + ultimately have ?thesis using n by blast}
1.1011 + ultimately show ?thesis by auto
1.1012 +qed
1.1013 +
1.1014 +lemma prime_divisor_sqrt:
1.1015 + "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d^2 \<le> n \<longrightarrow> d = 1)"
1.1016 +proof-
1.1017 + {assume "n=0 \<or> n=1" hence ?thesis using prime_0 prime_1
1.1018 + by (auto simp add: nat_power_eq_0_iff)}
1.1019 + moreover
1.1020 + {assume n: "n\<noteq>0" "n\<noteq>1"
1.1021 + hence np: "n > 1" by arith
1.1022 + {fix d assume d: "d dvd n" "d^2 \<le> n" and H: "\<forall>m. m dvd n \<longrightarrow> m=1 \<or> m=n"
1.1023 + from H d have d1n: "d = 1 \<or> d=n" by blast
1.1024 + {assume dn: "d=n"
1.1025 + have "n^2 > n*1" using n
1.1026 + by (simp add: power2_eq_square mult_less_cancel1)
1.1027 + with dn d(2) have "d=1" by simp}
1.1028 + with d1n have "d = 1" by blast }
1.1029 + moreover
1.1030 + {fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'^2 \<le> n \<longrightarrow> d' = 1"
1.1031 + from d n have "d \<noteq> 0" apply - apply (rule ccontr) by simp
1.1032 + hence dp: "d > 0" by simp
1.1033 + from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast
1.1034 + from n dp e have ep:"e > 0" by simp
1.1035 + have "d^2 \<le> n \<or> e^2 \<le> n" using dp ep
1.1036 + by (auto simp add: e power2_eq_square mult_le_cancel_left)
1.1037 + moreover
1.1038 + {assume h: "d^2 \<le> n"
1.1039 + from H[rule_format, of d] h d have "d = 1" by blast}
1.1040 + moreover
1.1041 + {assume h: "e^2 \<le> n"
1.1042 + from e have "e dvd n" unfolding dvd_def by (simp add: mult_commute)
1.1043 + with H[rule_format, of e] h have "e=1" by simp
1.1044 + with e have "d = n" by simp}
1.1045 + ultimately have "d=1 \<or> d=n" by blast}
1.1046 + ultimately have ?thesis unfolding prime_def using np n(2) by blast}
1.1047 + ultimately show ?thesis by auto
1.1048 +qed
1.1049 +lemma prime_prime_factor_sqrt:
1.1050 + "prime n \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p^2 \<le> n)"
1.1051 + (is "?lhs \<longleftrightarrow>?rhs")
1.1052 +proof-
1.1053 + {assume "n=0 \<or> n=1" hence ?thesis using prime_0 prime_1 by auto}
1.1054 + moreover
1.1055 + {assume n: "n\<noteq>0" "n\<noteq>1"
1.1056 + {assume H: ?lhs
1.1057 + from H[unfolded prime_divisor_sqrt] n
1.1058 + have ?rhs apply clarsimp by (erule_tac x="p" in allE, simp add: prime_1)
1.1059 + }
1.1060 + moreover
1.1061 + {assume H: ?rhs
1.1062 + {fix d assume d: "d dvd n" "d^2 \<le> n" "d\<noteq>1"
1.1063 + from prime_factor[OF d(3)]
1.1064 + obtain p where p: "prime p" "p dvd d" by blast
1.1065 + from n have np: "n > 0" by arith
1.1066 + from d(1) n have "d \<noteq> 0" by - (rule ccontr, auto)
1.1067 + hence dp: "d > 0" by arith
1.1068 + from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)
1.1069 + have "p^2 \<le> n" unfolding power2_eq_square by arith
1.1070 + with H n p(1) dvd_trans[OF p(2) d(1)] have False by blast}
1.1071 + with n prime_divisor_sqrt have ?lhs by auto}
1.1072 + ultimately have ?thesis by blast }
1.1073 + ultimately show ?thesis by (cases "n=0 \<or> n=1", auto)
1.1074 +qed
1.1075 +(* Pocklington theorem. *)
1.1076 +
1.1077 +lemma pocklington_lemma:
1.1078 + assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and an: "[a^ (n - 1) = 1] (mod n)"
1.1079 + and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
1.1080 + and pp: "prime p" and pn: "p dvd n"
1.1081 + shows "[p = 1] (mod q)"
1.1082 +proof-
1.1083 + from pp prime_0 prime_1 have p01: "p \<noteq> 0" "p \<noteq> 1" by - (rule ccontr, simp)+
1.1084 + from cong_1_divides[OF an, unfolded nqr, unfolded dvd_def]
1.1085 + obtain k where k: "a ^ (q * r) - 1 = n*k" by blast
1.1086 + from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast
1.1087 + {assume a0: "a = 0"
1.1088 + hence "a^ (n - 1) = 0" using n by (simp add: power_0_left)
1.1089 + with n an mod_less[of 1 n] have False by (simp add: power_0_left modeq_def)}
1.1090 + hence a0: "a\<noteq>0" ..
1.1091 + from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by (simp add: neq0_conv)
1.1092 + hence "(a ^ (q * r) - 1) + 1 = a ^ (q * r)" by simp
1.1093 + with k l have "a ^ (q * r) = p*l*k + 1" by simp
1.1094 + hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: mult_ac)
1.1095 + hence odq: "ord p (a^r) dvd q"
1.1096 + unfolding ord_divides[symmetric] power_mult[symmetric] nat_mod by blast
1.1097 + from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d" by blast
1.1098 + {assume d1: "d \<noteq> 1"
1.1099 + from prime_factor[OF d1] obtain P where P: "prime P" "P dvd d" by blast
1.1100 + from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp
1.1101 + from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast
1.1102 + from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast
1.1103 + have P0: "P \<noteq> 0" using P(1) prime_0 by - (rule ccontr, simp)
1.1104 + from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast
1.1105 + from d s t P0 have s': "ord p (a^r) * t = s" by algebra
1.1106 + have "ord p (a^r) * t*r = r * ord p (a^r) * t" by algebra
1.1107 + hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"
1.1108 + by (simp only: power_mult)
1.1109 + have "[((a ^ r) ^ ord p (a^r)) ^ t= 1^t] (mod p)"
1.1110 + by (rule cong_exp, rule ord)
1.1111 + then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)" by simp
1.1112 + from cong_1_divides[OF th] exps have pd0: "p dvd a^(ord p (a^r) * t*r) - 1" by simp
1.1113 + from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" using P0 by simp
1.1114 + with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp
1.1115 + with p01 pn pd0 have False unfolding coprime by auto}
1.1116 + hence d1: "d = 1" by blast
1.1117 + hence o: "ord p (a^r) = q" using d by simp
1.1118 + from pp phi_prime[of p] have phip: " \<phi> p = p - 1" by simp
1.1119 + {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
1.1120 + from pp[unfolded prime_def] d have dp: "d = p" by blast
1.1121 + from n have n12:"Suc (n - 2) = n - 1" by arith
1.1122 + with divides_rexp[OF d(2)[unfolded dp], of "n - 2"]
1.1123 + have th0: "p dvd a ^ (n - 1)" by simp
1.1124 + from n have n0: "n \<noteq> 0" by simp
1.1125 + from d(2) an n12[symmetric] have a0: "a \<noteq> 0"
1.1126 + by - (rule ccontr, simp add: modeq_def)
1.1127 + have th1: "a^ (n - 1) \<noteq> 0" using n d(2) dp a0 by (auto simp add: neq0_conv)
1.1128 + from coprime_minus1[OF th1, unfolded coprime]
1.1129 + dvd_trans[OF pn cong_1_divides[OF an]] th0 d(3) dp
1.1130 + have False by auto}
1.1131 + hence cpa: "coprime p a" using coprime by auto
1.1132 + from coprime_exp[OF cpa, of r] coprime_commute
1.1133 + have arp: "coprime (a^r) p" by blast
1.1134 + from fermat_little[OF arp, simplified ord_divides] o phip
1.1135 + have "q dvd (p - 1)" by simp
1.1136 + then obtain d where d:"p - 1 = q * d" unfolding dvd_def by blast
1.1137 + from prime_0 pp have p0:"p \<noteq> 0" by - (rule ccontr, auto)
1.1138 + from p0 d have "p + q * 0 = 1 + q * d" by simp
1.1139 + with nat_mod[of p 1 q, symmetric]
1.1140 + show ?thesis by blast
1.1141 +qed
1.1142 +
1.1143 +lemma pocklington:
1.1144 + assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q^2"
1.1145 + and an: "[a^ (n - 1) = 1] (mod n)"
1.1146 + and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
1.1147 + shows "prime n"
1.1148 +unfolding prime_prime_factor_sqrt[of n]
1.1149 +proof-
1.1150 + let ?ths = "n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<twosuperior> \<le> n)"
1.1151 + from n have n01: "n\<noteq>0" "n\<noteq>1" by arith+
1.1152 + {fix p assume p: "prime p" "p dvd n" "p^2 \<le> n"
1.1153 + from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)" by (simp add: power2_eq_square)
1.1154 + hence pq: "p \<le> q" unfolding exp_mono_le .
1.1155 + from pocklington_lemma[OF n nqr an aq p(1,2)] cong_1_divides
1.1156 + have th: "q dvd p - 1" by blast
1.1157 + have "p - 1 \<noteq> 0"using prime_ge_2[OF p(1)] by arith
1.1158 + with divides_ge[OF th] pq have False by arith }
1.1159 + with n01 show ?ths by blast
1.1160 +qed
1.1161 +
1.1162 +(* Variant for application, to separate the exponentiation. *)
1.1163 +lemma pocklington_alt:
1.1164 + assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q^2"
1.1165 + and an: "[a^ (n - 1) = 1] (mod n)"
1.1166 + 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.1167 + shows "prime n"
1.1168 +proof-
1.1169 + {fix p assume p: "prime p" "p dvd q"
1.1170 + from aq[rule_format] p obtain b where
1.1171 + b: "[a^((n - 1) div p) = b] (mod n)" "coprime (b - 1) n" by blast
1.1172 + {assume a0: "a=0"
1.1173 + from n an have "[0 = 1] (mod n)" unfolding a0 power_0_left by auto
1.1174 + hence False using n by (simp add: modeq_def dvd_eq_mod_eq_0[symmetric])}
1.1175 + hence a0: "a\<noteq> 0" ..
1.1176 + hence a1: "a \<ge> 1" by arith
1.1177 + from one_le_power[OF a1] have ath: "1 \<le> a ^ ((n - 1) div p)" .
1.1178 + {assume b0: "b = 0"
1.1179 + from p(2) nqr have "(n - 1) mod p = 0"
1.1180 + apply (simp only: dvd_eq_mod_eq_0[symmetric]) by (rule dvd_mult2, simp)
1.1181 + with mod_div_equality[of "n - 1" p]
1.1182 + have "(n - 1) div p * p= n - 1" by auto
1.1183 + hence eq: "(a^((n - 1) div p))^p = a^(n - 1)"
1.1184 + by (simp only: power_mult[symmetric])
1.1185 + from prime_ge_2[OF p(1)] have pS: "Suc (p - 1) = p" by arith
1.1186 + from b(1) have d: "n dvd a^((n - 1) div p)" unfolding b0 cong_0_divides .
1.1187 + from divides_rexp[OF d, of "p - 1"] pS eq cong_divides[OF an] n
1.1188 + have False by simp}
1.1189 + then have b0: "b \<noteq> 0" ..
1.1190 + hence b1: "b \<ge> 1" by arith
1.1191 + from cong_coprime[OF cong_sub[OF b(1) cong_refl[of 1] ath b1]] b(2) nqr
1.1192 + have "coprime (a ^ ((n - 1) div p) - 1) n" by (simp add: coprime_commute)}
1.1193 + hence th: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n "
1.1194 + by blast
1.1195 + from pocklington[OF n nqr sqr an th] show ?thesis .
1.1196 +qed
1.1197 +
1.1198 +(* Prime factorizations. *)
1.1199 +
1.1200 +definition "primefact ps n = (foldr op * ps 1 = n \<and> (\<forall>p\<in> set ps. prime p))"
1.1201 +
1.1202 +lemma primefact: assumes n: "n \<noteq> 0"
1.1203 + shows "\<exists>ps. primefact ps n"
1.1204 +using n
1.1205 +proof(induct n rule: nat_less_induct)
1.1206 + fix n assume H: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>ps. primefact ps m)" and n: "n\<noteq>0"
1.1207 + let ?ths = "\<exists>ps. primefact ps n"
1.1208 + {assume "n = 1"
1.1209 + hence "primefact [] n" by (simp add: primefact_def)
1.1210 + hence ?ths by blast }
1.1211 + moreover
1.1212 + {assume n1: "n \<noteq> 1"
1.1213 + with n have n2: "n \<ge> 2" by arith
1.1214 + from prime_factor[OF n1] obtain p where p: "prime p" "p dvd n" by blast
1.1215 + from p(2) obtain m where m: "n = p*m" unfolding dvd_def by blast
1.1216 + from n m have m0: "m > 0" "m\<noteq>0" by auto
1.1217 + from prime_ge_2[OF p(1)] have "1 < p" by arith
1.1218 + with m0 m have mn: "m < n" by auto
1.1219 + from H[rule_format, OF mn m0(2)] obtain ps where ps: "primefact ps m" ..
1.1220 + from ps m p(1) have "primefact (p#ps) n" by (simp add: primefact_def)
1.1221 + hence ?ths by blast}
1.1222 + ultimately show ?ths by blast
1.1223 +qed
1.1224 +
1.1225 +lemma primefact_contains:
1.1226 + assumes pf: "primefact ps n" and p: "prime p" and pn: "p dvd n"
1.1227 + shows "p \<in> set ps"
1.1228 + using pf p pn
1.1229 +proof(induct ps arbitrary: p n)
1.1230 + case Nil thus ?case by (auto simp add: primefact_def)
1.1231 +next
1.1232 + case (Cons q qs p n)
1.1233 + from Cons.prems[unfolded primefact_def]
1.1234 + 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.1235 + {assume "p dvd q"
1.1236 + with p(1) q(1) have "p = q" unfolding prime_def by auto
1.1237 + hence ?case by simp}
1.1238 + moreover
1.1239 + { assume h: "p dvd foldr op * qs 1"
1.1240 + from q(3) have pqs: "primefact qs (foldr op * qs 1)"
1.1241 + by (simp add: primefact_def)
1.1242 + from Cons.hyps[OF pqs p(1) h] have ?case by simp}
1.1243 + ultimately show ?case using prime_divprod[OF p] by blast
1.1244 +qed
1.1245 +
1.1246 +lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps" by (auto simp add: primefact_def list_all_iff)
1.1247 +
1.1248 +(* Variant of Lucas theorem. *)
1.1249 +
1.1250 +lemma lucas_primefact:
1.1251 + assumes n: "n \<ge> 2" and an: "[a^(n - 1) = 1] (mod n)"
1.1252 + and psn: "foldr op * ps 1 = n - 1"
1.1253 + and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps"
1.1254 + shows "prime n"
1.1255 +proof-
1.1256 + {fix p assume p: "prime p" "p dvd n - 1" "[a ^ ((n - 1) div p) = 1] (mod n)"
1.1257 + from psn psp have psn1: "primefact ps (n - 1)"
1.1258 + by (auto simp add: list_all_iff primefact_variant)
1.1259 + from p(3) primefact_contains[OF psn1 p(1,2)] psp
1.1260 + have False by (induct ps, auto)}
1.1261 + with lucas[OF n an] show ?thesis by blast
1.1262 +qed
1.1263 +
1.1264 +(* Variant of Pocklington theorem. *)
1.1265 +
1.1266 +lemma mod_le: assumes n: "n \<noteq> (0::nat)" shows "m mod n \<le> m"
1.1267 +proof-
1.1268 + from mod_div_equality[of m n]
1.1269 + have "\<exists>x. x + m mod n = m" by blast
1.1270 + then show ?thesis by auto
1.1271 +qed
1.1272 +
1.1273 +
1.1274 +lemma pocklington_primefact:
1.1275 + assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q^2"
1.1276 + and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q"
1.1277 + and bqn: "(b^q) mod n = 1"
1.1278 + and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
1.1279 + shows "prime n"
1.1280 +proof-
1.1281 + from bqn psp qrn
1.1282 + have bqn: "a ^ (n - 1) mod n = 1"
1.1283 + and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps" unfolding arnb[symmetric] power_mod
1.1284 + by (simp_all add: power_mult[symmetric] ring_simps)
1.1285 + from n have n0: "n > 0" by arith
1.1286 + from mod_div_equality[of "a^(n - 1)" n]
1.1287 + mod_less_divisor[OF n0, of "a^(n - 1)"]
1.1288 + have an1: "[a ^ (n - 1) = 1] (mod n)"
1.1289 + unfolding nat_mod bqn
1.1290 + apply -
1.1291 + apply (rule exI[where x="0"])
1.1292 + apply (rule exI[where x="a^(n - 1) div n"])
1.1293 + by (simp add: ring_simps)
1.1294 + {fix p assume p: "prime p" "p dvd q"
1.1295 + from psp psq have pfpsq: "primefact ps q"
1.1296 + by (auto simp add: primefact_variant list_all_iff)
1.1297 + from psp primefact_contains[OF pfpsq p]
1.1298 + have p': "coprime (a ^ (r * (q div p)) mod n - 1) n"
1.1299 + by (simp add: list_all_iff)
1.1300 + from prime_ge_2[OF p(1)] have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)" by arith+
1.1301 + from div_mult1_eq[of r q p] p(2)
1.1302 + have eq1: "r* (q div p) = (n - 1) div p"
1.1303 + unfolding qrn[symmetric] dvd_eq_mod_eq_0 by (simp add: mult_commute)
1.1304 + have ath: "\<And>a (b::nat). a <= b \<Longrightarrow> a \<noteq> 0 ==> 1 <= a \<and> 1 <= b" by arith
1.1305 + from n0 have n00: "n \<noteq> 0" by arith
1.1306 + from mod_le[OF n00]
1.1307 + have th10: "a ^ ((n - 1) div p) mod n \<le> a ^ ((n - 1) div p)" .
1.1308 + {assume "a ^ ((n - 1) div p) mod n = 0"
1.1309 + then obtain s where s: "a ^ ((n - 1) div p) = n*s"
1.1310 + unfolding mod_eq_0_iff by blast
1.1311 + hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
1.1312 + from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto
1.1313 + from dvd_trans[OF p(2) qn1] div_mod_equality'[of "n - 1" p]
1.1314 + have npp: "(n - 1) div p * p = n - 1" by (simp add: dvd_eq_mod_eq_0)
1.1315 + with eq0 have "a^ (n - 1) = (n*s)^p"
1.1316 + by (simp add: power_mult[symmetric])
1.1317 + hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp
1.1318 + also have "\<dots> = 0" by (simp add: mult_assoc mod_mult_self_is_0)
1.1319 + finally have False by simp }
1.1320 + then have th11: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto
1.1321 + have th1: "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)"
1.1322 + unfolding modeq_def by simp
1.1323 + from cong_sub[OF th1 cong_refl[of 1]] ath[OF th10 th11]
1.1324 + have th: "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)"
1.1325 + by blast
1.1326 + from cong_coprime[OF th] p'[unfolded eq1]
1.1327 + have "coprime (a ^ ((n - 1) div p) - 1) n" by (simp add: coprime_commute) }
1.1328 + with pocklington[OF n qrn[symmetric] nq2 an1]
1.1329 + show ?thesis by blast
1.1330 +qed
1.1331 +
1.1332 +
1.1333 +end