src/HOL/Number_Theory/Pocklington.thy
 changeset 55337 5d45fb978d5a parent 55321 eadea363deb6 child 55346 d344d663658a
equal inserted replaced
55334:5f5104069b33 55337:5d45fb978d5a
`    35         by (metis prime_gt_0_nat q(1))`
`    35         by (metis prime_gt_0_nat q(1))`
`    36       from dvd_imp_le[OF q(2)] p0 have qp: "q \<le> p" by arith`
`    36       from dvd_imp_le[OF q(2)] p0 have qp: "q \<le> p" by arith`
`    37       {assume "q = p" hence ?lhs using q(1) by blast}`
`    37       {assume "q = p" hence ?lhs using q(1) by blast}`
`    38       moreover`
`    38       moreover`
`    39       {assume "q\<noteq>p" with qp have qplt: "q < p" by arith`
`    39       {assume "q\<noteq>p" with qp have qplt: "q < p" by arith`
`    40         from H[rule_format, of q] qplt q0 have "coprime p q" by arith`
`    40         from H qplt q0 have "coprime p q" by arith`
`    41        hence ?lhs`
`    41        hence ?lhs using q`
`    42          by (metis gcd_semilattice_nat.inf_absorb2 one_not_prime_nat q(1) q(2))}`
`    42          by (metis gcd_semilattice_nat.inf_absorb2 one_not_prime_nat)}`
`    43       ultimately have ?lhs by blast}`
`    43       ultimately have ?lhs by blast}`
`    44     ultimately have ?thesis by blast}`
`    44     ultimately have ?thesis by blast}`
`    45   ultimately show ?thesis  by (cases"p=0 \<or> p=1", auto)`
`    45   ultimately show ?thesis  by (cases"p=0 \<or> p=1", auto)`
`    46 qed`
`    46 qed`
`    47 `
`    47 `
`    63   from bezout_add_strong_nat[OF az, of n]`
`    63   from bezout_add_strong_nat[OF az, of n]`
`    64   obtain d x y where dxy: "d dvd a" "d dvd n" "a*x = n*y + d" by blast`
`    64   obtain d x y where dxy: "d dvd a" "d dvd n" "a*x = n*y + d" by blast`
`    65   from dxy(1,2) have d1: "d = 1"`
`    65   from dxy(1,2) have d1: "d = 1"`
`    66     by (metis assms coprime_nat) `
`    66     by (metis assms coprime_nat) `
`    67   hence "a*x*b = (n*y + 1)*b" using dxy(3) by simp`
`    67   hence "a*x*b = (n*y + 1)*b" using dxy(3) by simp`
`    68   hence "a*(x*b) = n*(y*b) + b"`
`    68   hence "a*(x*b) = n*(y*b) + b" `
`    69     by (auto simp add: algebra_simps)`
`    69     by (auto simp add: algebra_simps)`
`    70   hence "a*(x*b) mod n = (n*(y*b) + b) mod n" by simp`
`    70   hence "a*(x*b) mod n = (n*(y*b) + b) mod n" by simp`
`    71   hence "a*(x*b) mod n = b mod n" by (simp add: mod_add_left_eq)`
`    71   hence "a*(x*b) mod n = b mod n" by (simp add: mod_add_left_eq)`
`    72   hence "[a*(x*b) = b] (mod n)" unfolding cong_nat_def .`
`    72   hence "[a*(x*b) = b] (mod n)" unfolding cong_nat_def .`
`    73   hence ?thesis by blast}`
`    73   hence ?thesis by blast}`
`   110       by (metis gcd_nat.absorb1 one_not_prime_nat p pa th)}`
`   110       by (metis gcd_nat.absorb1 one_not_prime_nat p pa th)}`
`   111   with y show ?thesis unfolding Ex1_def using neq0_conv by blast`
`   111   with y show ?thesis unfolding Ex1_def using neq0_conv by blast`
`   112 qed`
`   112 qed`
`   113 `
`   113 `
`   114 lemma cong_unique_inverse_prime:`
`   114 lemma cong_unique_inverse_prime:`
`   116   assumes p: "prime p" and x0: "0 < x" and xp: "x < p"`
`   115   assumes p: "prime p" and x0: "0 < x" and xp: "x < p"`
`   117   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"`
`   116   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"`
`   118 by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd_nat.commute assms) `
`   117 by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd_nat.commute assms) `
`   119 `
`   118 `
`   120 lemma chinese_remainder_coprime_unique:`
`   119 lemma chinese_remainder_coprime_unique:`
`   156 proof -`
`   155 proof -`
`   157   have "1 \<le> card {0::int <.. 1}"`
`   156   have "1 \<le> card {0::int <.. 1}"`
`   158     by auto`
`   157     by auto`
`   159   also have "... \<le> card {x. 0 < x \<and> x < n \<and> coprime x n}"`
`   158   also have "... \<le> card {x. 0 < x \<and> x < n \<and> coprime x n}"`
`   160     apply (rule card_mono) using assms`
`   159     apply (rule card_mono) using assms`
`   161     apply (auto simp add: )`
`   160     by auto (metis dual_order.antisym gcd_1_int gcd_int.commute int_one_le_iff_zero_less)`
`   162     by (metis dual_order.antisym gcd_1_int gcd_int.commute int_one_le_iff_zero_less)`
`       `
`   163   also have "... = phi n"`
`   161   also have "... = phi n"`
`   164     by (simp add: phi_def)`
`   162     by (simp add: phi_def)`
`   165   finally show ?thesis .`
`   163   finally show ?thesis .`
`   166 qed`
`   164 qed`
`   167 `
`   165 `
`   218   with prime_phi phi_prime n1(1,2) show ?thesis`
`   216   with prime_phi phi_prime n1(1,2) show ?thesis`
`   219     by auto`
`   217     by auto`
`   220 qed`
`   218 qed`
`   221 `
`   219 `
`   222 lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"`
`   220 lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"`
`   223   (is "?lhs \<longleftrightarrow> ?rhs")`
`   221   by (metis ex_least_nat_le not_less0)`
`   224 proof`
`       `
`   225   assume ?rhs thus ?lhs by blast`
`       `
`   226 next`
`       `
`   227   assume H: ?lhs then obtain n where n: "P n" by blast`
`       `
`   228   let ?x = "Least P"`
`       `
`   229   {fix m assume m: "m < ?x"`
`       `
`   230     from not_less_Least[OF m] have "\<not> P m" .}`
`       `
`   231   with LeastI_ex[OF H] show ?rhs by blast`
`       `
`   232 qed`
`       `
`   233 `
`   222 `
`   234 lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> (P (Least P) \<and> (\<forall>m < (Least P). \<not> P m))"`
`   223 lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> (P (Least P) \<and> (\<forall>m < (Least P). \<not> P m))"`
`   235   (is "?lhs \<longleftrightarrow> ?rhs")`
`   224   (is "?lhs \<longleftrightarrow> ?rhs")`
`   236 proof-`
`   225 proof-`
`   237   {assume ?rhs hence ?lhs by blast}`
`   226   {assume ?rhs hence ?lhs by blast}`
`   286     obtain p where p: "prime p" "p dvd r"`
`   275     obtain p where p: "prime p" "p dvd r"`
`   287       by (metis prime_factor_nat r01(2))`
`   276       by (metis prime_factor_nat r01(2))`
`   288     hence th: "prime p \<and> p dvd n - 1" unfolding r by (auto intro: dvd_mult)`
`   277     hence th: "prime p \<and> p dvd n - 1" unfolding r by (auto intro: dvd_mult)`
`   289     have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r`
`   278     have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r`
`   290       by (simp add: power_mult)`
`   279       by (simp add: power_mult)`
`   291     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`
`   280     also have "\<dots> = (a^(m*(r div p))) mod n" `
`       `
`   281       using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] `
`       `
`   282       by simp`
`   292     also have "\<dots> = ((a^m)^(r div p)) mod n" by (simp add: power_mult)`
`   283     also have "\<dots> = ((a^m)^(r div p)) mod n" by (simp add: power_mult)`
`   293     also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod[of "a^m" "n" "r div p" ] ..`
`   284     also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod ..`
`   294     also have "\<dots> = 1" using m(3) onen by (simp add: cong_nat_def power_Suc_0)`
`   285     also have "\<dots> = 1" using m(3) onen by (simp add: cong_nat_def)`
`   295     finally have "[(a ^ ((n - 1) div p))= 1] (mod n)"`
`   286     finally have "[(a ^ ((n - 1) div p))= 1] (mod n)"`
`   296       using onen by (simp add: cong_nat_def)`
`   287       using onen by (simp add: cong_nat_def)`
`   297     with pn[rule_format, OF th] have False by blast}`
`   288     with pn th have False by blast}`
`   298   hence th: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" by blast`
`   289   hence th: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" by blast`
`   299   from lucas_weak[OF n2 an1 th] show ?thesis .`
`   290   from lucas_weak[OF n2 an1 th] show ?thesis .`
`   300 qed`
`   291 qed`
`   301 `
`   292 `
`   302 `
`   293 `
`   331 lemma ord_works:`
`   322 lemma ord_works:`
`   332   fixes n::nat`
`   323   fixes n::nat`
`   333   shows "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> ~[a^ m = 1] (mod n))"`
`   324   shows "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> ~[a^ m = 1] (mod n))"`
`   334 apply (cases "coprime n a")`
`   325 apply (cases "coprime n a")`
`   335 using coprime_ord[of n a]`
`   326 using coprime_ord[of n a]`
`   336 by (blast, simp add: ord_def cong_nat_def)`
`   327 by (auto simp add: ord_def cong_nat_def)`
`   337 `
`   328 `
`   338 lemma ord:`
`   329 lemma ord:`
`   339   fixes n::nat`
`   330   fixes n::nat`
`   340   shows "[a^(ord n a) = 1] (mod n)" using ord_works by blast`
`   331   shows "[a^(ord n a) = 1] (mod n)" using ord_works by blast`
`   341 `
`   332 `
`   376       obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto`
`   367       obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto`
`   377       from lh`
`   368       from lh`
`   378       obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2"`
`   369       obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2"`
`   379         by (metis H d0 gcd_nat.commute lucas_coprime_lemma) `
`   370         by (metis H d0 gcd_nat.commute lucas_coprime_lemma) `
`   380       hence "a ^ d + n * q1 - n * q2 = 1" by simp`
`   371       hence "a ^ d + n * q1 - n * q2 = 1" by simp`
`   381       with dvd_diff_nat [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' `
`   372       with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2  d' p`
`   382       have "p dvd 1" by simp`
`   373       have "p dvd 1"`
`       `
`   374         by metis`
`   383       with p(3) have False by simp`
`   375       with p(3) have False by simp`
`   384       hence ?rhs ..}`
`   376       hence ?rhs ..}`
`   385     ultimately have ?rhs by blast}`
`   377     ultimately have ?rhs by blast}`
`   386   moreover`
`   378   moreover`
`   387   {assume H: "coprime n a"`
`   379   {assume H: "coprime n a"`
`   451 qed`
`   443 qed`
`   452 `
`   444 `
`   453 subsection{*Another trivial primality characterization*}`
`   445 subsection{*Another trivial primality characterization*}`
`   454 `
`   446 `
`   455 lemma prime_prime_factor:`
`   447 lemma prime_prime_factor:`
`   456   "prime n \<longleftrightarrow> n \<noteq> 1\<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)"`
`   448   "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)" `
`   457 proof-`
`   449   (is "?lhs \<longleftrightarrow> ?rhs")`
`   458   {assume n: "n=0 \<or> n=1" `
`   450 proof (cases "n=0 \<or> n=1")`
`   459    hence ?thesis`
`   451   case True`
`   460      by (metis bigger_prime dvd_0_right one_not_prime_nat zero_not_prime_nat) }`
`   452   then show ?thesis`
`   461   moreover`
`   453      by (metis bigger_prime dvd_0_right one_not_prime_nat zero_not_prime_nat)`
`   462   {assume n: "n\<noteq>0" "n\<noteq>1"`
`   454 next`
`   463     {assume pn: "prime n"`
`   455   case False`
`   464 `
`   456   show ?thesis`
`   465       from pn[unfolded prime_def] have "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n"`
`   457   proof`
`   466         using n`
`   458     assume "prime n"`
`   467         apply (cases "n = 0 \<or> n=1",simp)`
`   459     then show ?rhs`
`   468         by (clarsimp, erule_tac x="p" in allE, auto)}`
`   460       by (metis one_not_prime_nat prime_nat_def)`
`   469     moreover`
`   461   next`
`   470     {assume H: "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n"`
`   462     assume ?rhs`
`   471       from n have n1: "n > 1" by arith`
`   463     with False show "prime n"`
`   472       {fix m assume m: "m dvd n" "m\<noteq>1"`
`   464       by (auto simp: prime_def) (metis One_nat_def prime_factor_nat prime_nat_def)`
`   473        then obtain p where p: "prime p" "p dvd m"`
`   465   qed`
`   474          by (metis prime_factor_nat) `
`       `
`   475        from dvd_trans[OF p(2) m(1)] p(1) H have "p = n" by blast`
`       `
`   476        with p(2) have "n dvd m"  by simp`
`       `
`   477        hence "m=n"  using dvd_antisym[OF m(1)] by simp }`
`       `
`   478       with n1 have "prime n"  unfolding prime_def by auto }`
`       `
`   479     ultimately have ?thesis using n by blast}`
`       `
`   480   ultimately       show ?thesis by auto`
`       `
`   481 qed`
`   466 qed`
`   482 `
`   467 `
`   483 lemma prime_divisor_sqrt:`
`   468 lemma prime_divisor_sqrt:`
`   484   "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"`
`   469   "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"`
`   485 proof -`
`   470 proof -`
`   526   moreover`
`   511   moreover`
`   527   {assume n: "n\<noteq>0" "n\<noteq>1"`
`   512   {assume n: "n\<noteq>0" "n\<noteq>1"`
`   528     {assume H: ?lhs`
`   513     {assume H: ?lhs`
`   529       from H[unfolded prime_divisor_sqrt] n`
`   514       from H[unfolded prime_divisor_sqrt] n`
`   530       have ?rhs`
`   515       have ?rhs`
`   531         apply clarsimp`
`   516         by (metis prime_prime_factor) }`
`   532         apply (erule_tac x="p" in allE)`
`       `
`   533         apply simp`
`       `
`   534         done`
`       `
`   535     }`
`       `
`   536     moreover`
`   517     moreover`
`   537     {assume H: ?rhs`
`   518     {assume H: ?rhs`
`   538       {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1"`
`   519       {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1"`
`   539         then obtain p where p: "prime p" "p dvd d"`
`   520         then obtain p where p: "prime p" "p dvd d"`
`   540           by (metis prime_factor_nat) `
`   521           by (metis prime_factor_nat) `
`   541         from n have np: "n > 0" by arith`
`   522         from d(1) n have dp: "d > 0"`
`   542         from d(1) n have "d \<noteq> 0" by - (rule ccontr, auto)`
`   523           by (metis dvd_0_left neq0_conv) `
`   543         hence dp: "d > 0" by arith`
`       `
`   544         from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)`
`   524         from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)`
`   545         have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith`
`   525         have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith`
`   546         with H n p(1) dvd_trans[OF p(2) d(1)] have False  by blast}`
`   526         with H n p(1) dvd_trans[OF p(2) d(1)] have False  by blast}`
`   547       with n prime_divisor_sqrt  have ?lhs by auto}`
`   527       with n prime_divisor_sqrt  have ?lhs by auto}`
`   548     ultimately have ?thesis by blast }`
`   528     ultimately have ?thesis by blast }`
`   587       by (metis mult_commute mult_cancel1 nat_mult_assoc) `
`   567       by (metis mult_commute mult_cancel1 nat_mult_assoc) `
`   588     have "ord p (a^r) * t*r = r * ord p (a^r) * t"`
`   568     have "ord p (a^r) * t*r = r * ord p (a^r) * t"`
`   589       by (metis mult_assoc mult_commute)`
`   569       by (metis mult_assoc mult_commute)`
`   590     hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"`
`   570     hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"`
`   591       by (simp only: power_mult)`
`   571       by (simp only: power_mult)`
`   594     then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"`
`   572     then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"`
`   595       by simp`
`   573       by (metis cong_exp_nat ord power_one)`
`   596     have pd0: "p dvd a^(ord p (a^r) * t*r) - 1"`
`   574     have pd0: "p dvd a^(ord p (a^r) * t*r) - 1"`
`   597       by (metis cong_to_1_nat exps th)`
`   575       by (metis cong_to_1_nat exps th)`
`   598     from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" using P0 by simp`
`   576     from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" using P0 by simp`
`   599     with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp`
`   577     with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp`
`   600     with p01 pn pd0 coprime_common_divisor_nat have False `
`   578     with p01 pn pd0 coprime_common_divisor_nat have False `
`   611   hence cpa: "coprime p a" by auto`
`   589   hence cpa: "coprime p a" by auto`
`   612   have arp: "coprime (a^r) p"`
`   590   have arp: "coprime (a^r) p"`
`   613     by (metis coprime_exp_nat cpa gcd_nat.commute) `
`   591     by (metis coprime_exp_nat cpa gcd_nat.commute) `
`   614   from euler_theorem_nat[OF arp, simplified ord_divides] o phip`
`   592   from euler_theorem_nat[OF arp, simplified ord_divides] o phip`
`   615   have "q dvd (p - 1)" by simp`
`   593   have "q dvd (p - 1)" by simp`
`   616   then obtain d where d:"p - 1 = q * d" unfolding dvd_def by blast`
`   594   then obtain d where d:"p - 1 = q * d" `
`       `
`   595     unfolding dvd_def by blast`
`   617   have p0:"p \<noteq> 0"`
`   596   have p0:"p \<noteq> 0"`
`   618     by (metis p01(1)) `
`   597     by (metis p01(1)) `
`   619   from p0 d have "p + q * 0 = 1 + q * d" by simp`
`   598   from p0 d have "p + q * 0 = 1 + q * d" by simp`
`   620   then show ?thesis`
`   599   then show ?thesis`
`   621     by (metis cong_iff_lin_nat mult_commute)`
`   600     by (metis cong_iff_lin_nat mult_commute)`
`   767   and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"`
`   746   and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"`
`   768   shows "prime n"`
`   747   shows "prime n"`
`   769 proof-`
`   748 proof-`
`   770   from bqn psp qrn`
`   749   from bqn psp qrn`
`   771   have bqn: "a ^ (n - 1) mod n = 1"`
`   750   have bqn: "a ^ (n - 1) mod n = 1"`
`   772     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`
`   751     and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps"  `
`       `
`   752     unfolding arnb[symmetric] power_mod `
`   773     by (simp_all add: power_mult[symmetric] algebra_simps)`
`   753     by (simp_all add: power_mult[symmetric] algebra_simps)`
`   774   from n  have n0: "n > 0" by arith`
`   754   from n  have n0: "n > 0" by arith`
`   775   from mod_div_equality[of "a^(n - 1)" n]`
`   755   from mod_div_equality[of "a^(n - 1)" n]`
`   776     mod_less_divisor[OF n0, of "a^(n - 1)"]`
`   756     mod_less_divisor[OF n0, of "a^(n - 1)"]`
`   777   have an1: "[a ^ (n - 1) = 1] (mod n)"`
`   757   have an1: "[a ^ (n - 1) = 1] (mod n)"`