author  paulson <lp15@cam.ac.uk> 
Thu, 06 Feb 2014 13:04:06 +0000  
changeset 55346  d344d663658a 
parent 55337  5d45fb978d5a 
child 55370  e6be866b5f5b 
permissions  rwrr 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1 
(* Title: HOL/Number_Theory/Pocklington.thy 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

2 
Author: Amine Chaieb 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

3 
*) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

4 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

5 
header {* Pocklington's Theorem for Primes *} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

6 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

7 
theory Pocklington 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

8 
imports Residues 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

9 
begin 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

10 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

11 
subsection{*Lemmas about previously defined terms*} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

12 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

13 
lemma prime: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

14 
"prime p \<longleftrightarrow> p \<noteq> 0 \<and> p\<noteq>1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

15 
(is "?lhs \<longleftrightarrow> ?rhs") 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

16 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

17 
{assume "p=0 \<or> p=1" hence ?thesis 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

18 
by (metis one_not_prime_nat zero_not_prime_nat)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

19 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

20 
{assume p0: "p\<noteq>0" "p\<noteq>1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

21 
{assume H: "?lhs" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

22 
{fix m assume m: "m > 0" "m < p" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

23 
{assume "m=1" hence "coprime p m" by simp} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

24 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

25 
{assume "p dvd m" hence "p \<le> m" using dvd_imp_le m by blast with m(2) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

26 
have "coprime p m" by simp} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

27 
ultimately have "coprime p m" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

28 
by (metis H prime_imp_coprime_nat)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

29 
hence ?rhs using p0 by auto} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

30 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

31 
{ assume H: "\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

32 
obtain q where q: "prime q" "q dvd p" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

33 
by (metis p0(2) prime_factor_nat) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

34 
have q0: "q > 0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

35 
by (metis prime_gt_0_nat q(1)) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

36 
from dvd_imp_le[OF q(2)] p0 have qp: "q \<le> p" by arith 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

37 
{assume "q = p" hence ?lhs using q(1) by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

38 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

39 
{assume "q\<noteq>p" with qp have qplt: "q < p" by arith 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

40 
from H qplt q0 have "coprime p q" by arith 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

41 
hence ?lhs using q 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

42 
by (metis gcd_semilattice_nat.inf_absorb2 one_not_prime_nat)} 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

43 
ultimately have ?lhs by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

44 
ultimately have ?thesis by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

45 
ultimately show ?thesis by (cases"p=0 \<or> p=1", auto) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

46 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

47 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

48 
lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n  1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

49 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

50 
have "{ m. 0 < m \<and> m < n } = {1..<n}" by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

51 
thus ?thesis by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

52 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

53 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

54 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

55 
subsection{*Some basic theorems about solving congruences*} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

56 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

57 
lemma cong_solve: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

58 
fixes n::nat assumes an: "coprime a n" shows "\<exists>x. [a * x = b] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

59 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

60 
{assume "a=0" hence ?thesis using an by (simp add: cong_nat_def)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

61 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

62 
{assume az: "a\<noteq>0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

63 
from bezout_add_strong_nat[OF az, of n] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

64 
obtain d x y where dxy: "d dvd a" "d dvd n" "a*x = n*y + d" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

65 
from dxy(1,2) have d1: "d = 1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

66 
by (metis assms coprime_nat) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

67 
hence "a*x*b = (n*y + 1)*b" using dxy(3) by simp 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

68 
hence "a*(x*b) = n*(y*b) + b" 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

69 
by (auto simp add: algebra_simps) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

70 
hence "a*(x*b) mod n = (n*(y*b) + b) mod n" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

71 
hence "a*(x*b) mod n = b mod n" by (simp add: mod_add_left_eq) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

72 
hence "[a*(x*b) = b] (mod n)" unfolding cong_nat_def . 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

73 
hence ?thesis by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

74 
ultimately show ?thesis by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

75 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

76 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

77 
lemma cong_solve_unique: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

78 
fixes n::nat assumes an: "coprime a n" and nz: "n \<noteq> 0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

79 
shows "\<exists>!x. x < n \<and> [a * x = b] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

80 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

81 
let ?P = "\<lambda>x. x < n \<and> [a * x = b] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

82 
from cong_solve[OF an] obtain x where x: "[a*x = b] (mod n)" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

83 
let ?x = "x mod n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

84 
from x have th: "[a * ?x = b] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

85 
by (simp add: cong_nat_def mod_mult_right_eq[of a x n]) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

86 
from mod_less_divisor[ of n x] nz th have Px: "?P ?x" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

87 
{fix y assume Py: "y < n" "[a * y = b] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

88 
from Py(2) th have "[a * y = a*?x] (mod n)" by (simp add: cong_nat_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

89 
hence "[y = ?x] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

90 
by (metis an cong_mult_lcancel_nat) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

91 
with mod_less[OF Py(1)] mod_less_divisor[ of n x] nz 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

92 
have "y = ?x" by (simp add: cong_nat_def)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

93 
with Px show ?thesis by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

94 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

95 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

96 
lemma cong_solve_unique_nontrivial: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

97 
assumes p: "prime p" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

98 
shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

99 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

100 
from pa have ap: "coprime a p" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

101 
by (metis gcd_nat.commute) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

102 
have px:"coprime x p" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

103 
by (metis gcd_nat.commute p prime x0 xp) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

104 
obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

105 
by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

106 
{assume y0: "y = 0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

107 
with y(2) have th: "p dvd a" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

108 
by (metis cong_dvd_eq_nat gcd_lcm_complete_lattice_nat.top_greatest mult_0_right) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

109 
have False 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

110 
by (metis gcd_nat.absorb1 one_not_prime_nat p pa th)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

111 
with y show ?thesis unfolding Ex1_def using neq0_conv by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

112 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

113 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

114 
lemma cong_unique_inverse_prime: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

115 
assumes p: "prime p" and x0: "0 < x" and xp: "x < p" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

116 
shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

117 
by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd_nat.commute assms) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

118 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

119 
lemma chinese_remainder_coprime_unique: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

120 
fixes a::nat 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

121 
assumes ab: "coprime a b" and az: "a \<noteq> 0" and bz: "b \<noteq> 0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

122 
and ma: "coprime m a" and nb: "coprime n b" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

123 
shows "\<exists>!x. coprime x (a * b) \<and> x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

124 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

125 
let ?P = "\<lambda>x. x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

126 
from binary_chinese_remainder_unique_nat[OF ab az bz] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

127 
obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

128 
"\<forall>y. ?P y \<longrightarrow> y = x" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

129 
from ma nb x 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

130 
have "coprime x a" "coprime x b" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

131 
by (metis cong_gcd_eq_nat)+ 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

132 
then have "coprime x (a*b)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

133 
by (metis coprime_mul_eq_nat) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

134 
with x show ?thesis by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

135 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

136 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

137 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

138 
subsection{*Lucas's theorem*} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

139 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

140 
lemma phi_limit_strong: "phi(n) \<le> n  1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

141 
proof  
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

142 
have "phi n = card {x. 0 < x \<and> x < int n \<and> coprime x (int n)}" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

143 
by (simp add: phi_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

144 
also have "... \<le> card {0 <..< int n}" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

145 
by (rule card_mono) auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

146 
also have "... = card {0 <..< n}" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

147 
by (simp add: transfer_nat_int_set_functions) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

148 
also have "... \<le> n  1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

149 
by (metis card_greaterThanLessThan le_refl One_nat_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

150 
finally show ?thesis . 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

151 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

152 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

153 
lemma phi_lowerbound_1: assumes n: "n \<ge> 2" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

154 
shows "phi n \<ge> 1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

155 
proof  
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

156 
have "1 \<le> card {0::int <.. 1}" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

157 
by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

158 
also have "... \<le> card {x. 0 < x \<and> x < n \<and> coprime x n}" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

159 
apply (rule card_mono) using assms 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

160 
by auto (metis dual_order.antisym gcd_1_int gcd_int.commute int_one_le_iff_zero_less) 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

161 
also have "... = phi n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

162 
by (simp add: phi_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

163 
finally show ?thesis . 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

164 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

165 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

166 
lemma phi_lowerbound_1_nat: assumes n: "n \<ge> 2" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

167 
shows "phi(int n) \<ge> 1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

168 
by (metis n nat_le_iff nat_numeral phi_lowerbound_1) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

169 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

170 
lemma euler_theorem_nat: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

171 
fixes m::nat 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

172 
assumes "coprime a m" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

173 
shows "[a ^ phi m = 1] (mod m)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

174 
by (metis assms le0 euler_theorem [transferred]) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

175 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

176 
lemma lucas_coprime_lemma: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

177 
fixes n::nat 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

178 
assumes m: "m\<noteq>0" and am: "[a^m = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

179 
shows "coprime a n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

180 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

181 
{assume "n=1" hence ?thesis by simp} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

182 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

183 
{assume "n = 0" hence ?thesis using am m 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

184 
by (metis am cong_0_nat gcd_nat.right_neutral power_eq_one_eq_nat)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

185 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

186 
{assume n: "n\<noteq>0" "n\<noteq>1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

187 
from m obtain m' where m': "m = Suc m'" by (cases m, blast+) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

188 
{fix d 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

189 
assume d: "d dvd a" "d dvd n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

190 
from n have n1: "1 < n" by arith 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

191 
from am mod_less[OF n1] have am1: "a^m mod n = 1" unfolding cong_nat_def by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

192 
from dvd_mult2[OF d(1), of "a^m'"] have dam:"d dvd a^m" by (simp add: m') 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

193 
from dvd_mod_iff[OF d(2), of "a^m"] dam am1 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

194 
have "d = 1" by simp } 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

195 
hence ?thesis by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

196 
} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

197 
ultimately show ?thesis by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

198 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

199 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

200 
lemma lucas_weak: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

201 
fixes n::nat 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

202 
assumes n: "n \<ge> 2" and an:"[a^(n  1) = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

203 
and nm: "\<forall>m. 0 <m \<and> m < n  1 \<longrightarrow> \<not> [a^m = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

204 
shows "prime n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

205 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

206 
from n have n1: "n \<noteq> 1" "n\<noteq>0" "n  1 \<noteq> 0" "n  1 > 0" "n  1 < n" by arith+ 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

207 
from lucas_coprime_lemma[OF n1(3) an] have can: "coprime a n" . 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

208 
from euler_theorem_nat[OF can] have afn: "[a ^ phi n = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

209 
by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

210 
{assume "phi n \<noteq> n  1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

211 
with phi_limit_strong phi_lowerbound_1_nat [OF n] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

212 
have c:"phi n > 0 \<and> phi n < n  1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

213 
by (metis gr0I leD less_linear not_one_le_zero) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

214 
from nm[rule_format, OF c] afn have False ..} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

215 
hence "phi n = n  1" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

216 
with prime_phi phi_prime n1(1,2) show ?thesis 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

217 
by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

218 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

219 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

220 
lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))" 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

221 
by (metis ex_least_nat_le not_less0) 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

222 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

223 
lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> (P (Least P) \<and> (\<forall>m < (Least P). \<not> P m))" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

224 
(is "?lhs \<longleftrightarrow> ?rhs") 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

225 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

226 
{assume ?rhs hence ?lhs by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

227 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

228 
{ assume H: ?lhs then obtain n where n: "P n" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

229 
let ?x = "Least P" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

230 
{fix m assume m: "m < ?x" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

231 
from not_less_Least[OF m] have "\<not> P m" .} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

232 
with LeastI_ex[OF H] have ?rhs by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

233 
ultimately show ?thesis by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

234 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

235 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

236 
theorem lucas: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

237 
assumes n2: "n \<ge> 2" and an1: "[a^(n  1) = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

238 
and pn: "\<forall>p. prime p \<and> p dvd n  1 \<longrightarrow> [a^((n  1) div p) \<noteq> 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

239 
shows "prime n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

240 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

241 
from n2 have n01: "n\<noteq>0" "n\<noteq>1" "n  1 \<noteq> 0" by arith+ 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

242 
from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

243 
from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

244 
have an: "coprime a n" "coprime (a^(n  1)) n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

245 
by (auto simp add: coprime_exp_nat gcd_nat.commute) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

246 
{assume H0: "\<exists>m. 0 < m \<and> m < n  1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m") 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

247 
from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

248 
m: "0 < m" "m < n  1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

249 
{assume nm1: "(n  1) mod m > 0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

250 
from mod_less_divisor[OF m(1)] have th0:"(n  1) mod m < m" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

251 
let ?y = "a^ ((n  1) div m * m)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

252 
note mdeq = mod_div_equality[of "(n  1)" m] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

253 
have yn: "coprime ?y n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

254 
by (metis an(1) coprime_exp_nat gcd_nat.commute) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

255 
have "?y mod n = (a^m)^((n  1) div m) mod n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

256 
by (simp add: algebra_simps power_mult) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

257 
also have "\<dots> = (a^m mod n)^((n  1) div m) mod n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

258 
using power_mod[of "a^m" n "(n  1) div m"] by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

259 
also have "\<dots> = 1" using m(3)[unfolded cong_nat_def onen] onen 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

260 
by (metis power_one) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

261 
finally have th3: "?y mod n = 1" . 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

262 
have th2: "[?y * a ^ ((n  1) mod m) = ?y* 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

263 
using an1[unfolded cong_nat_def onen] onen 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

264 
mod_div_equality[of "(n  1)" m, symmetric] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

265 
by (simp add:power_add[symmetric] cong_nat_def th3 del: One_nat_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

266 
have th1: "[a ^ ((n  1) mod m) = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

267 
by (metis cong_mult_rcancel_nat nat_mult_commute th2 yn) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

268 
from m(4)[rule_format, OF th0] nm1 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

269 
less_trans[OF mod_less_divisor[OF m(1), of "n  1"] m(2)] th1 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

270 
have False by blast } 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

271 
hence "(n  1) mod m = 0" by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

272 
then have mn: "m dvd n  1" by presburger 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

273 
then obtain r where r: "n  1 = m*r" unfolding dvd_def by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

274 
from n01 r m(2) have r01: "r\<noteq>0" "r\<noteq>1" by  (rule ccontr, simp)+ 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

275 
obtain p where p: "prime p" "p dvd r" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

276 
by (metis prime_factor_nat r01(2)) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

277 
hence th: "prime p \<and> p dvd n  1" unfolding r by (auto intro: dvd_mult) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

278 
have "(a ^ ((n  1) div p)) mod n = (a^(m*r div p)) mod n" using r 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

279 
by (simp add: power_mult) 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

280 
also have "\<dots> = (a^(m*(r div p))) mod n" 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

281 
using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

282 
by simp 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

283 
also have "\<dots> = ((a^m)^(r div p)) mod n" by (simp add: power_mult) 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

284 
also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod .. 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

285 
also have "\<dots> = 1" using m(3) onen by (simp add: cong_nat_def) 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

286 
finally have "[(a ^ ((n  1) div p))= 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

287 
using onen by (simp add: cong_nat_def) 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

288 
with pn th have False by blast} 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

289 
hence th: "\<forall>m. 0 < m \<and> m < n  1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

290 
from lucas_weak[OF n2 an1 th] show ?thesis . 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

291 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

292 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

293 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

294 
subsection{*Definition of the order of a number mod n (0 in noncoprime case)*} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

295 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

296 
definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

297 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

298 
(* This has the expected properties. *) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

299 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

300 
lemma coprime_ord: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

301 
fixes n::nat 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

302 
assumes "coprime n a" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

303 
shows "ord n a > 0 \<and> [a ^(ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> [a^ m \<noteq> 1] (mod n))" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

304 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

305 
let ?P = "\<lambda>d. 0 < d \<and> [a ^ d = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

306 
from bigger_prime[of a] obtain p where p: "prime p" "a < p" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

307 
from assms have o: "ord n a = Least ?P" by (simp add: ord_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

308 
{assume "n=0 \<or> n=1" with assms have "\<exists>m>0. ?P m" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

309 
by auto} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

310 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

311 
{assume "n\<noteq>0 \<and> n\<noteq>1" hence n2:"n \<ge> 2" by arith 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

312 
from assms have na': "coprime a n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

313 
by (metis gcd_nat.commute) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

314 
from phi_lowerbound_1_nat[OF n2] euler_theorem_nat [OF na'] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

315 
have ex: "\<exists>m>0. ?P m" by  (rule exI[where x="phi n"], auto) } 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

316 
ultimately have ex: "\<exists>m>0. ?P m" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

317 
from nat_exists_least_iff'[of ?P] ex assms show ?thesis 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

318 
unfolding o[symmetric] by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

319 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

320 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

321 
(* With the special value 0 for noncoprime case, it's more convenient. *) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

322 
lemma ord_works: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

323 
fixes n::nat 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

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))" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

325 
apply (cases "coprime n a") 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

326 
using coprime_ord[of n a] 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

327 
by (auto simp add: ord_def cong_nat_def) 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

328 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

329 
lemma ord: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

330 
fixes n::nat 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

331 
shows "[a^(ord n a) = 1] (mod n)" using ord_works by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

332 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

333 
lemma ord_minimal: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

334 
fixes n::nat 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

335 
shows "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> ~[a^m = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

336 
using ord_works by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

337 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

338 
lemma ord_eq_0: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

339 
fixes n::nat 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

340 
shows "ord n a = 0 \<longleftrightarrow> ~coprime n a" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

341 
by (cases "coprime n a", simp add: coprime_ord, simp add: ord_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

342 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

343 
lemma divides_rexp: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

344 
"x dvd y \<Longrightarrow> (x::nat) dvd (y^(Suc n))" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

345 
by (simp add: dvd_mult2[of x y]) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

346 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

347 
lemma ord_divides: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

348 
fixes n::nat 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

349 
shows "[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d" (is "?lhs \<longleftrightarrow> ?rhs") 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

350 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

351 
assume rh: ?rhs 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

352 
then obtain k where "d = ord n a * k" unfolding dvd_def by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

353 
hence "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

354 
by (simp add : cong_nat_def power_mult power_mod) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

355 
also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

356 
using ord[of a n, unfolded cong_nat_def] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

357 
by (simp add: cong_nat_def power_mod) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

358 
finally show ?lhs . 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

359 
next 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

360 
assume lh: ?lhs 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

361 
{ assume H: "\<not> coprime n a" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

362 
hence o: "ord n a = 0" by (simp add: ord_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

363 
{assume d: "d=0" with o H have ?rhs by (simp add: cong_nat_def)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

364 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

365 
{assume d0: "d\<noteq>0" then obtain d' where d': "d = Suc d'" by (cases d, auto) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

366 
from H 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

367 
obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

368 
from lh 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

369 
obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

370 
by (metis H d0 gcd_nat.commute lucas_coprime_lemma) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

371 
hence "a ^ d + n * q1  n * q2 = 1" by simp 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

372 
with dvd_diff_nat [OF dvd_add [OF divides_rexp]] dvd_mult2 d' p 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

373 
have "p dvd 1" 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

374 
by metis 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

375 
with p(3) have False by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

376 
hence ?rhs ..} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

377 
ultimately have ?rhs by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

378 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

379 
{assume H: "coprime n a" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

380 
let ?o = "ord n a" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

381 
let ?q = "d div ord n a" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

382 
let ?r = "d mod ord n a" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

383 
have eqo: "[(a^?o)^?q = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

384 
by (metis cong_exp_nat ord power_one) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

385 
from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

386 
hence op: "?o > 0" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

387 
from mod_div_equality[of d "ord n a"] lh 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

388 
have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: cong_nat_def mult_commute) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

389 
hence "[(a^?o)^?q * (a^?r) = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

390 
by (simp add: cong_nat_def power_mult[symmetric] power_add[symmetric]) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

391 
hence th: "[a^?r = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

392 
using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

393 
apply (simp add: cong_nat_def del: One_nat_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

394 
by (simp add: mod_mult_left_eq[symmetric]) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

395 
{assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

396 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

397 
{assume r: "?r \<noteq> 0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

398 
with mod_less_divisor[OF op, of d] have r0o:"?r >0 \<and> ?r < ?o" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

399 
from conjunct2[OF ord_works[of a n], rule_format, OF r0o] th 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

400 
have ?rhs by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

401 
ultimately have ?rhs by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

402 
ultimately show ?rhs by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

403 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

404 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

405 
lemma order_divides_phi: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

406 
fixes n::nat shows "coprime n a \<Longrightarrow> ord n a dvd phi n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

407 
by (metis ord_divides euler_theorem_nat gcd_nat.commute) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

408 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

409 
lemma order_divides_expdiff: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

410 
fixes n::nat and a::nat assumes na: "coprime n a" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

411 
shows "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

412 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

413 
{fix n::nat and a::nat and d::nat and e::nat 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

414 
assume na: "coprime n a" and ed: "(e::nat) \<le> d" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

415 
hence "\<exists>c. d = e + c" by presburger 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

416 
then obtain c where c: "d = e + c" by presburger 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

417 
from na have an: "coprime a n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

418 
by (metis gcd_nat.commute) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

419 
have aen: "coprime (a^e) n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

420 
by (metis coprime_exp_nat gcd_nat.commute na) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

421 
have acn: "coprime (a^c) n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

422 
by (metis coprime_exp_nat gcd_nat.commute na) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

423 
have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

424 
using c by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

425 
also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

426 
also have "\<dots> \<longleftrightarrow> [a ^ c = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

427 
using cong_mult_lcancel_nat [OF aen, of "a^c" "a^0"] by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

428 
also have "\<dots> \<longleftrightarrow> ord n a dvd c" by (simp only: ord_divides) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

429 
also have "\<dots> \<longleftrightarrow> [e + c = e + 0] (mod ord n a)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

430 
using cong_add_lcancel_nat 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

431 
by (metis cong_dvd_eq_nat dvd_0_right cong_dvd_modulus_nat cong_mult_self_nat nat_mult_1) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

432 
finally have "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

433 
using c by simp } 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

434 
note th = this 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

435 
have "e \<le> d \<or> d \<le> e" by arith 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

436 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

437 
{assume ed: "e \<le> d" from th[OF na ed] have ?thesis .} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

438 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

439 
{assume de: "d \<le> e" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

440 
from th[OF na de] have ?thesis 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

441 
by (metis cong_sym_nat)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

442 
ultimately show ?thesis by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

443 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

444 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

445 
subsection{*Another trivial primality characterization*} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

446 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

447 
lemma prime_prime_factor: 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

448 
"prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)" 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

449 
(is "?lhs \<longleftrightarrow> ?rhs") 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

450 
proof (cases "n=0 \<or> n=1") 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

451 
case True 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

452 
then show ?thesis 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

453 
by (metis bigger_prime dvd_0_right one_not_prime_nat zero_not_prime_nat) 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

454 
next 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

455 
case False 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

456 
show ?thesis 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

457 
proof 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

458 
assume "prime n" 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

459 
then show ?rhs 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

460 
by (metis one_not_prime_nat prime_nat_def) 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

461 
next 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

462 
assume ?rhs 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

463 
with False show "prime n" 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

464 
by (auto simp: prime_def) (metis One_nat_def prime_factor_nat prime_nat_def) 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

465 
qed 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

466 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

467 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

468 
lemma prime_divisor_sqrt: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

469 
"prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

470 
proof  
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

471 
{assume "n=0 \<or> n=1" hence ?thesis 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

472 
by (metis dvd.order_refl le_refl one_not_prime_nat power_zero_numeral zero_not_prime_nat)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

473 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

474 
{assume n: "n\<noteq>0" "n\<noteq>1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

475 
hence np: "n > 1" by arith 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

476 
{fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" and H: "\<forall>m. m dvd n \<longrightarrow> m=1 \<or> m=n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

477 
from H d have d1n: "d = 1 \<or> d=n" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

478 
{assume dn: "d=n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

479 
have "n\<^sup>2 > n*1" using n by (simp add: power2_eq_square) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

480 
with dn d(2) have "d=1" by simp} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

481 
with d1n have "d = 1" by blast } 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

482 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

483 
{fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

484 
from d n have "d \<noteq> 0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

485 
by (metis dvd_0_left_iff) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

486 
hence dp: "d > 0" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

487 
from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

488 
from n dp e have ep:"e > 0" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

489 
have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n" using dp ep 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

490 
by (auto simp add: e power2_eq_square mult_le_cancel_left) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

491 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

492 
{assume h: "d\<^sup>2 \<le> n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

493 
from H[rule_format, of d] h d have "d = 1" by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

494 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

495 
{assume h: "e\<^sup>2 \<le> n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

496 
from e have "e dvd n" unfolding dvd_def by (simp add: mult_commute) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

497 
with H[rule_format, of e] h have "e=1" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

498 
with e have "d = n" by simp} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

499 
ultimately have "d=1 \<or> d=n" by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

500 
ultimately have ?thesis unfolding prime_def using np n(2) by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

501 
ultimately show ?thesis by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

502 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

503 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

504 
lemma prime_prime_factor_sqrt: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

505 
"prime n \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

506 
(is "?lhs \<longleftrightarrow>?rhs") 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

507 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

508 
{assume "n=0 \<or> n=1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

509 
hence ?thesis 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

510 
by (metis one_not_prime_nat zero_not_prime_nat)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

511 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

512 
{assume n: "n\<noteq>0" "n\<noteq>1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

513 
{assume H: ?lhs 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

514 
from H[unfolded prime_divisor_sqrt] n 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

515 
have ?rhs 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

516 
by (metis prime_prime_factor) } 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

517 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

518 
{assume H: ?rhs 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

519 
{fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

520 
then obtain p where p: "prime p" "p dvd d" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

521 
by (metis prime_factor_nat) 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

522 
from d(1) n have dp: "d > 0" 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

523 
by (metis dvd_0_left neq0_conv) 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

524 
from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

525 
have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

526 
with H n p(1) dvd_trans[OF p(2) d(1)] have False by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

527 
with n prime_divisor_sqrt have ?lhs by auto} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

528 
ultimately have ?thesis by blast } 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

529 
ultimately show ?thesis by (cases "n=0 \<or> n=1", auto) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

530 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

531 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

532 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

533 
subsection{*Pocklington theorem*} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

534 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

535 
lemma pocklington_lemma: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

536 
assumes n: "n \<ge> 2" and nqr: "n  1 = q*r" and an: "[a^ (n  1) = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

537 
and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n  1) div p)  1) n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

538 
and pp: "prime p" and pn: "p dvd n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

539 
shows "[p = 1] (mod q)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

540 
proof  
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

541 
have p01: "p \<noteq> 0" "p \<noteq> 1" using pp one_not_prime_nat zero_not_prime_nat by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

542 
obtain k where k: "a ^ (q * r)  1 = n*k" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

543 
by (metis an cong_to_1_nat dvd_def nqr) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

544 
from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

545 
{assume a0: "a = 0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

546 
hence "a^ (n  1) = 0" using n by (simp add: power_0_left) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

547 
with n an mod_less[of 1 n] have False by (simp add: power_0_left cong_nat_def)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

548 
hence a0: "a\<noteq>0" .. 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

549 
from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

550 
hence "(a ^ (q * r)  1) + 1 = a ^ (q * r)" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

551 
with k l have "a ^ (q * r) = p*l*k + 1" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

552 
hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: mult_ac) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

553 
hence odq: "ord p (a^r) dvd q" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

554 
unfolding ord_divides[symmetric] power_mult[symmetric] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

555 
by (metis an cong_dvd_modulus_nat mult_commute nqr pn) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

556 
from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

557 
{assume d1: "d \<noteq> 1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

558 
obtain P where P: "prime P" "P dvd d" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

559 
by (metis d1 prime_factor_nat) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

560 
from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

561 
from aq P(1) Pq have caP:"coprime (a^ ((n  1) div P)  1) n" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

562 
from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

563 
have P0: "P \<noteq> 0" using P(1) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

564 
by (metis zero_not_prime_nat) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

565 
from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

566 
from d s t P0 have s': "ord p (a^r) * t = s" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

567 
by (metis mult_commute mult_cancel1 nat_mult_assoc) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

568 
have "ord p (a^r) * t*r = r * ord p (a^r) * t" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

569 
by (metis mult_assoc mult_commute) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

570 
hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

571 
by (simp only: power_mult) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

572 
then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)" 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

573 
by (metis cong_exp_nat ord power_one) 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

574 
have pd0: "p dvd a^(ord p (a^r) * t*r)  1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

575 
by (metis cong_to_1_nat exps th) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

576 
from nqr s s' have "(n  1) div P = ord p (a^r) * t*r" using P0 by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

577 
with caP have "coprime (a^(ord p (a^r) * t*r)  1) n" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

578 
with p01 pn pd0 coprime_common_divisor_nat have False 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

579 
by auto} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

580 
hence d1: "d = 1" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

581 
hence o: "ord p (a^r) = q" using d by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

582 
from pp phi_prime[of p] have phip: "phi p = p  1" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

583 
{fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

584 
from pp[unfolded prime_def] d have dp: "d = p" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

585 
from n have "n \<noteq> 0" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

586 
then have False using d 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

587 
by (metis coprime_minus_one_nat dp lucas_coprime_lemma an coprime_nat 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

588 
gcd_lcm_complete_lattice_nat.top_greatest pn)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

589 
hence cpa: "coprime p a" by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

590 
have arp: "coprime (a^r) p" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

591 
by (metis coprime_exp_nat cpa gcd_nat.commute) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

592 
from euler_theorem_nat[OF arp, simplified ord_divides] o phip 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

593 
have "q dvd (p  1)" by simp 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

594 
then obtain d where d:"p  1 = q * d" 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

595 
unfolding dvd_def by blast 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

596 
have p0:"p \<noteq> 0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

597 
by (metis p01(1)) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

598 
from p0 d have "p + q * 0 = 1 + q * d" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

599 
then show ?thesis 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

600 
by (metis cong_iff_lin_nat mult_commute) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

601 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

602 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

603 
theorem pocklington: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

604 
assumes n: "n \<ge> 2" and nqr: "n  1 = q*r" and sqr: "n \<le> q\<^sup>2" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

605 
and an: "[a^ (n  1) = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

606 
and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n  1) div p)  1) n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

607 
shows "prime n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

608 
unfolding prime_prime_factor_sqrt[of n] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

609 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

610 
let ?ths = "n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

611 
from n have n01: "n\<noteq>0" "n\<noteq>1" by arith+ 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

612 
{fix p assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

613 
from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)" by (simp add: power2_eq_square) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

614 
hence pq: "p \<le> q" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

615 
by (metis le0 power_le_imp_le_base) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

616 
from pocklington_lemma[OF n nqr an aq p(1,2)] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

617 
have th: "q dvd p  1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

618 
by (metis cong_to_1_nat) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

619 
have "p  1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

620 
with pq p have False 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

621 
by (metis Suc_diff_1 gcd_le2_nat gcd_semilattice_nat.inf_absorb1 not_less_eq_eq 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

622 
prime_gt_0_nat th) } 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

623 
with n01 show ?ths by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

624 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

625 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

626 
(* Variant for application, to separate the exponentiation. *) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

627 
lemma pocklington_alt: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

628 
assumes n: "n \<ge> 2" and nqr: "n  1 = q*r" and sqr: "n \<le> q\<^sup>2" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

629 
and an: "[a^ (n  1) = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

630 
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)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

631 
shows "prime n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

632 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

633 
{fix p assume p: "prime p" "p dvd q" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

634 
from aq[rule_format] p obtain b where 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

635 
b: "[a^((n  1) div p) = b] (mod n)" "coprime (b  1) n" by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

636 
{assume a0: "a=0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

637 
from n an have "[0 = 1] (mod n)" unfolding a0 power_0_left by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

638 
hence False using n by (simp add: cong_nat_def dvd_eq_mod_eq_0[symmetric])} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

639 
hence a0: "a\<noteq> 0" .. 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

640 
hence a1: "a \<ge> 1" by arith 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

641 
from one_le_power[OF a1] have ath: "1 \<le> a ^ ((n  1) div p)" . 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

642 
{assume b0: "b = 0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

643 
from p(2) nqr have "(n  1) mod p = 0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

644 
by (metis mod_0 mod_mod_cancel mod_mult_self1_is_0) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

645 
with mod_div_equality[of "n  1" p] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

646 
have "(n  1) div p * p= n  1" by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

647 
hence eq: "(a^((n  1) div p))^p = a^(n  1)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

648 
by (simp only: power_mult[symmetric]) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

649 
have "p  1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

650 
then have pS: "Suc (p  1) = p" by arith 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

651 
from b have d: "n dvd a^((n  1) div p)" unfolding b0 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

652 
by (metis b0 diff_0_eq_0 gcd_dvd2_nat gcd_lcm_complete_lattice_nat.inf_bot_left 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

653 
gcd_lcm_complete_lattice_nat.inf_top_left) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

654 
from divides_rexp[OF d, of "p  1"] pS eq cong_dvd_eq_nat [OF an] n 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

655 
have False 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

656 
by simp} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

657 
then have b0: "b \<noteq> 0" .. 
55346
d344d663658a
fixed problem (?) by deleting "thm" line
paulson <lp15@cam.ac.uk>
parents:
55337
diff
changeset

658 
hence b1: "b \<ge> 1" by arith 
d344d663658a
fixed problem (?) by deleting "thm" line
paulson <lp15@cam.ac.uk>
parents:
55337
diff
changeset

659 
from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]] 
d344d663658a
fixed problem (?) by deleting "thm" line
paulson <lp15@cam.ac.uk>
parents:
55337
diff
changeset

660 
ath b1 b nqr 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

661 
have "coprime (a ^ ((n  1) div p)  1) n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

662 
by simp} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

663 
hence th: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n  1) div p)  1) n " 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

664 
by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

665 
from pocklington[OF n nqr sqr an th] show ?thesis . 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

666 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

667 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

668 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

669 
subsection{*Prime factorizations*} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

670 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

671 
text{*FIXME Some overlap with material in UniqueFactorization, class unique_factorization.*} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

672 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

673 
definition "primefact ps n = (foldr op * ps 1 = n \<and> (\<forall>p\<in> set ps. prime p))" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

674 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

675 
lemma primefact: assumes n: "n \<noteq> 0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

676 
shows "\<exists>ps. primefact ps n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

677 
using n 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

678 
proof(induct n rule: nat_less_induct) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

679 
fix n assume H: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>ps. primefact ps m)" and n: "n\<noteq>0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

680 
let ?ths = "\<exists>ps. primefact ps n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

681 
{assume "n = 1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

682 
hence "primefact [] n" by (simp add: primefact_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

683 
hence ?ths by blast } 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

684 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

685 
{assume n1: "n \<noteq> 1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

686 
with n have n2: "n \<ge> 2" by arith 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

687 
obtain p where p: "prime p" "p dvd n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

688 
by (metis n1 prime_factor_nat) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

689 
from p(2) obtain m where m: "n = p*m" unfolding dvd_def by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

690 
from n m have m0: "m > 0" "m\<noteq>0" by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

691 
have "1 < p" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

692 
by (metis p(1) prime_nat_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

693 
with m0 m have mn: "m < n" by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

694 
from H[rule_format, OF mn m0(2)] obtain ps where ps: "primefact ps m" .. 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

695 
from ps m p(1) have "primefact (p#ps) n" by (simp add: primefact_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

696 
hence ?ths by blast} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

697 
ultimately show ?ths by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

698 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

699 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

700 
lemma primefact_contains: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

701 
assumes pf: "primefact ps n" and p: "prime p" and pn: "p dvd n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

702 
shows "p \<in> set ps" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

703 
using pf p pn 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

704 
proof(induct ps arbitrary: p n) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

705 
case Nil thus ?case by (auto simp add: primefact_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

706 
next 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

707 
case (Cons q qs p n) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

708 
from Cons.prems[unfolded primefact_def] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

709 
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 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

710 
{assume "p dvd q" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

711 
with p(1) q(1) have "p = q" unfolding prime_def by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

712 
hence ?case by simp} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

713 
moreover 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

714 
{ assume h: "p dvd foldr op * qs 1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

715 
from q(3) have pqs: "primefact qs (foldr op * qs 1)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

716 
by (simp add: primefact_def) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

717 
from Cons.hyps[OF pqs p(1) h] have ?case by simp} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

718 
ultimately show ?case 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

719 
by (metis p prime_dvd_mult_eq_nat) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

720 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

721 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

722 
lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

723 
by (auto simp add: primefact_def list_all_iff) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

724 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

725 
(* Variant of Lucas theorem. *) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

726 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

727 
lemma lucas_primefact: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

728 
assumes n: "n \<ge> 2" and an: "[a^(n  1) = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

729 
and psn: "foldr op * ps 1 = n  1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

730 
and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n  1) div p) = 1] (mod n)) ps" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

731 
shows "prime n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

732 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

733 
{fix p assume p: "prime p" "p dvd n  1" "[a ^ ((n  1) div p) = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

734 
from psn psp have psn1: "primefact ps (n  1)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

735 
by (auto simp add: list_all_iff primefact_variant) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

736 
from p(3) primefact_contains[OF psn1 p(1,2)] psp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

737 
have False by (induct ps, auto)} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

738 
with lucas[OF n an] show ?thesis by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

739 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

740 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

741 
(* Variant of Pocklington theorem. *) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

742 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

743 
lemma pocklington_primefact: 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

744 
assumes n: "n \<ge> 2" and qrn: "q*r = n  1" and nq2: "n \<le> q\<^sup>2" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

745 
and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

746 
and bqn: "(b^q) mod n = 1" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

747 
and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n  1) n) ps" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

748 
shows "prime n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

749 
proof 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

750 
from bqn psp qrn 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

751 
have bqn: "a ^ (n  1) mod n = 1" 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

752 
and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n  1) n) ps" 
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

753 
unfolding arnb[symmetric] power_mod 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

754 
by (simp_all add: power_mult[symmetric] algebra_simps) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

755 
from n have n0: "n > 0" by arith 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

756 
from mod_div_equality[of "a^(n  1)" n] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

757 
mod_less_divisor[OF n0, of "a^(n  1)"] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

758 
have an1: "[a ^ (n  1) = 1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

759 
by (metis bqn cong_nat_def mod_mod_trivial) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

760 
{fix p assume p: "prime p" "p dvd q" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

761 
from psp psq have pfpsq: "primefact ps q" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

762 
by (auto simp add: primefact_variant list_all_iff) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

763 
from psp primefact_contains[OF pfpsq p] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

764 
have p': "coprime (a ^ (r * (q div p)) mod n  1) n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

765 
by (simp add: list_all_iff) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

766 
from p prime_def have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p  1)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

767 
by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

768 
from div_mult1_eq[of r q p] p(2) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

769 
have eq1: "r* (q div p) = (n  1) div p" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

770 
unfolding qrn[symmetric] dvd_eq_mod_eq_0 by (simp add: mult_commute) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

771 
have ath: "\<And>a (b::nat). a <= b \<Longrightarrow> a \<noteq> 0 ==> 1 <= a \<and> 1 <= b" by arith 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

772 
{assume "a ^ ((n  1) div p) mod n = 0" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

773 
then obtain s where s: "a ^ ((n  1) div p) = n*s" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

774 
unfolding mod_eq_0_iff by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

775 
hence eq0: "(a^((n  1) div p))^p = (n*s)^p" by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

776 
from qrn[symmetric] have qn1: "q dvd n  1" unfolding dvd_def by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

777 
from dvd_trans[OF p(2) qn1] div_mod_equality'[of "n  1" p] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

778 
have npp: "(n  1) div p * p = n  1" by (simp add: dvd_eq_mod_eq_0) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

779 
with eq0 have "a^ (n  1) = (n*s)^p" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

780 
by (simp add: power_mult[symmetric]) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

781 
hence "1 = (n*s)^(Suc (p  1)) mod n" using bqn p01 by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

782 
also have "\<dots> = 0" by (simp add: mult_assoc) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

783 
finally have False by simp } 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

784 
then have th11: "a ^ ((n  1) div p) mod n \<noteq> 0" by auto 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

785 
have th1: "[a ^ ((n  1) div p) mod n = a ^ ((n  1) div p)] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

786 
unfolding cong_nat_def by simp 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

787 
from th1 ath[OF mod_less_eq_dividend th11] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

788 
have th: "[a ^ ((n  1) div p) mod n  1 = a ^ ((n  1) div p)  1] (mod n)" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

789 
by (metis cong_diff_nat cong_refl_nat) 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

790 
have "coprime (a ^ ((n  1) div p)  1) n" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

791 
by (metis cong_imp_coprime_nat eq1 p' th) } 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

792 
with pocklington[OF n qrn[symmetric] nq2 an1] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

793 
show ?thesis by blast 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

794 
qed 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

795 

eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

796 
end 