src/HOL/Number_Theory/Pocklington.thy
author paulson <lp15@cam.ac.uk>
Thu, 06 Feb 2014 13:04:06 +0000
changeset 55346 d344d663658a
parent 55337 5d45fb978d5a
child 55370 e6be866b5f5b
permissions -rw-r--r--
fixed problem (?) by deleting "thm" line
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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 non-coprime 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 non-coprime 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