src/HOL/NumberTheory/EulerFermat.thy
author wenzelm
Sun Feb 04 19:31:13 2001 +0100 (2001-02-04)
changeset 11049 7eef34adb852
parent 10834 a7897aebbffc
child 11549 e7265e70fd7c
permissions -rw-r--r--
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm@11049
     1
(*  Title:      HOL/NumberTheory/EulerFermat.thy
paulson@9508
     2
    ID:         $Id$
wenzelm@11049
     3
    Author:     Thomas M. Rasmussen
wenzelm@11049
     4
    Copyright   2000  University of Cambridge
paulson@9508
     5
*)
paulson@9508
     6
wenzelm@11049
     7
header {* Fermat's Little Theorem extended to Euler's Totient function *}
wenzelm@11049
     8
wenzelm@11049
     9
theory EulerFermat = BijectionRel + IntFact:
wenzelm@11049
    10
wenzelm@11049
    11
text {*
wenzelm@11049
    12
  Fermat's Little Theorem extended to Euler's Totient function. More
wenzelm@11049
    13
  abstract approach than Boyer-Moore (which seems necessary to achieve
wenzelm@11049
    14
  the extended version).
wenzelm@11049
    15
*}
wenzelm@11049
    16
wenzelm@11049
    17
wenzelm@11049
    18
subsection {* Definitions and lemmas *}
paulson@9508
    19
paulson@9508
    20
consts
wenzelm@11049
    21
  RsetR :: "int => int set set"
wenzelm@11049
    22
  BnorRset :: "int * int => int set"
wenzelm@11049
    23
  norRRset :: "int => int set"
wenzelm@11049
    24
  noXRRset :: "int => int => int set"
wenzelm@11049
    25
  phi :: "int => nat"
wenzelm@11049
    26
  is_RRset :: "int set => int => bool"
wenzelm@11049
    27
  RRset2norRR :: "int set => int => int => int"
paulson@9508
    28
paulson@9508
    29
inductive "RsetR m"
wenzelm@11049
    30
  intros
wenzelm@11049
    31
    empty [simp]: "{} \<in> RsetR m"
wenzelm@11049
    32
    insert: "A \<in> RsetR m ==> zgcd (a, m) = #1 ==>
wenzelm@11049
    33
      \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
paulson@9508
    34
wenzelm@11049
    35
recdef BnorRset
wenzelm@11049
    36
  "measure ((\<lambda>(a, m). nat a) :: int * int => nat)"
wenzelm@11049
    37
  "BnorRset (a, m) =
wenzelm@11049
    38
   (if #0 < a then
wenzelm@11049
    39
    let na = BnorRset (a - #1, m)
wenzelm@11049
    40
    in (if zgcd (a, m) = #1 then insert a na else na)
wenzelm@11049
    41
    else {})"
paulson@9508
    42
paulson@9508
    43
defs
wenzelm@11049
    44
  norRRset_def: "norRRset m == BnorRset (m - #1, m)"
wenzelm@11049
    45
  noXRRset_def: "noXRRset m x == (\<lambda>a. a * x) ` norRRset m"
wenzelm@11049
    46
  phi_def: "phi m == card (norRRset m)"
wenzelm@11049
    47
  is_RRset_def: "is_RRset A m == A \<in> RsetR m \<and> card A = phi m"
wenzelm@11049
    48
  RRset2norRR_def:
wenzelm@11049
    49
    "RRset2norRR A m a ==
wenzelm@11049
    50
     (if #1 < m \<and> is_RRset A m \<and> a \<in> A then
wenzelm@11049
    51
        SOME b. zcong a b m \<and> b \<in> norRRset m
wenzelm@11049
    52
      else #0)"
wenzelm@11049
    53
wenzelm@11049
    54
constdefs
wenzelm@11049
    55
  zcongm :: "int => int => int => bool"
wenzelm@11049
    56
  "zcongm m == \<lambda>a b. zcong a b m"
wenzelm@11049
    57
wenzelm@11049
    58
lemma abs_eq_1_iff [iff]: "(abs z = (#1::int)) = (z = #1 \<or> z = #-1)"
wenzelm@11049
    59
  -- {* LCP: not sure why this lemma is needed now *}
wenzelm@11049
    60
  apply (auto simp add: zabs_def)
wenzelm@11049
    61
  done
wenzelm@11049
    62
wenzelm@11049
    63
wenzelm@11049
    64
text {* \medskip @{text norRRset} *}
wenzelm@11049
    65
wenzelm@11049
    66
declare BnorRset.simps [simp del]
wenzelm@11049
    67
wenzelm@11049
    68
lemma BnorRset_induct:
wenzelm@11049
    69
  "(!!a m. P {} a m) ==>
wenzelm@11049
    70
    (!!a m. #0 < (a::int) ==> P (BnorRset (a - #1, m::int)) (a - #1) m
wenzelm@11049
    71
      ==> P (BnorRset(a,m)) a m)
wenzelm@11049
    72
    ==> P (BnorRset(u,v)) u v"
wenzelm@11049
    73
proof -
wenzelm@11049
    74
  case antecedent
wenzelm@11049
    75
  show ?thesis
wenzelm@11049
    76
    apply (rule BnorRset.induct)
wenzelm@11049
    77
    apply safe
wenzelm@11049
    78
     apply (case_tac [2] "#0 < a")
wenzelm@11049
    79
      apply (rule_tac [2] antecedent)
wenzelm@11049
    80
       apply simp_all
wenzelm@11049
    81
     apply (simp_all add: BnorRset.simps antecedent)
wenzelm@11049
    82
  done
wenzelm@11049
    83
qed
wenzelm@11049
    84
wenzelm@11049
    85
lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) --> b \<le> a"
wenzelm@11049
    86
  apply (induct a m rule: BnorRset_induct)
wenzelm@11049
    87
   prefer 2
wenzelm@11049
    88
   apply (subst BnorRset.simps)
wenzelm@11049
    89
   apply (unfold Let_def)
wenzelm@11049
    90
   apply auto
wenzelm@11049
    91
  done
wenzelm@11049
    92
wenzelm@11049
    93
lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)"
wenzelm@11049
    94
  apply (auto dest: Bnor_mem_zle)
wenzelm@11049
    95
  done
wenzelm@11049
    96
wenzelm@11049
    97
lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> #0 < b"
wenzelm@11049
    98
  apply (induct a m rule: BnorRset_induct)
wenzelm@11049
    99
   prefer 2
wenzelm@11049
   100
   apply (subst BnorRset.simps)
wenzelm@11049
   101
   apply (unfold Let_def)
wenzelm@11049
   102
   apply auto
wenzelm@11049
   103
  done
wenzelm@11049
   104
wenzelm@11049
   105
lemma Bnor_mem_if [rule_format]:
wenzelm@11049
   106
    "zgcd (b, m) = #1 --> #0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
wenzelm@11049
   107
  apply (induct a m rule: BnorRset.induct)
wenzelm@11049
   108
  apply auto
wenzelm@11049
   109
   apply (case_tac "a = b")
wenzelm@11049
   110
    prefer 2
wenzelm@11049
   111
    apply (simp add: order_less_le)
wenzelm@11049
   112
   apply (simp (no_asm_simp))
wenzelm@11049
   113
   prefer 2
wenzelm@11049
   114
   apply (subst BnorRset.simps)
wenzelm@11049
   115
   defer
wenzelm@11049
   116
   apply (subst BnorRset.simps)
wenzelm@11049
   117
   apply (unfold Let_def)
wenzelm@11049
   118
   apply auto
wenzelm@11049
   119
  done
paulson@9508
   120
wenzelm@11049
   121
lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset (a, m) \<in> RsetR m"
wenzelm@11049
   122
  apply (induct a m rule: BnorRset_induct)
wenzelm@11049
   123
   apply simp
wenzelm@11049
   124
  apply (subst BnorRset.simps)
wenzelm@11049
   125
  apply (unfold Let_def)
wenzelm@11049
   126
  apply auto
wenzelm@11049
   127
  apply (rule RsetR.insert)
wenzelm@11049
   128
    apply (rule_tac [3] allI)
wenzelm@11049
   129
    apply (rule_tac [3] impI)
wenzelm@11049
   130
    apply (rule_tac [3] zcong_not)
wenzelm@11049
   131
       apply (subgoal_tac [6] "a' \<le> a - #1")
wenzelm@11049
   132
        apply (rule_tac [7] Bnor_mem_zle)
wenzelm@11049
   133
        apply (rule_tac [5] Bnor_mem_zg)
wenzelm@11049
   134
        apply auto
wenzelm@11049
   135
  done
wenzelm@11049
   136
wenzelm@11049
   137
lemma Bnor_fin: "finite (BnorRset (a, m))"
wenzelm@11049
   138
  apply (induct a m rule: BnorRset_induct)
wenzelm@11049
   139
   prefer 2
wenzelm@11049
   140
   apply (subst BnorRset.simps)
wenzelm@11049
   141
   apply (unfold Let_def)
wenzelm@11049
   142
   apply auto
wenzelm@11049
   143
  done
wenzelm@11049
   144
wenzelm@11049
   145
lemma aux: "a \<le> b - #1 ==> a < (b::int)"
wenzelm@11049
   146
  apply auto
wenzelm@11049
   147
  done
paulson@9508
   148
wenzelm@11049
   149
lemma norR_mem_unique:
wenzelm@11049
   150
  "#1 < m ==>
wenzelm@11049
   151
    zgcd (a, m) = #1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m"
wenzelm@11049
   152
  apply (unfold norRRset_def)
wenzelm@11049
   153
  apply (cut_tac a = a and m = m in zcong_zless_unique)
wenzelm@11049
   154
   apply auto
wenzelm@11049
   155
   apply (rule_tac [2] m = m in zcong_zless_imp_eq)
wenzelm@11049
   156
       apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
wenzelm@11049
   157
	 order_less_imp_le aux simp add: zcong_sym)
wenzelm@11049
   158
  apply (rule_tac "x" = "b" in exI)
wenzelm@11049
   159
  apply safe
wenzelm@11049
   160
  apply (rule Bnor_mem_if)
wenzelm@11049
   161
    apply (case_tac [2] "b = #0")
wenzelm@11049
   162
     apply (auto intro: order_less_le [THEN iffD2])
wenzelm@11049
   163
   prefer 2
wenzelm@11049
   164
   apply (simp only: zcong_def)
wenzelm@11049
   165
   apply (subgoal_tac "zgcd (a, m) = m")
wenzelm@11049
   166
    prefer 2
wenzelm@11049
   167
    apply (subst zdvd_iff_zgcd [symmetric])
wenzelm@11049
   168
     apply (rule_tac [4] zgcd_zcong_zgcd)
wenzelm@11049
   169
       apply (simp_all add: zdvd_zminus_iff zcong_sym)
wenzelm@11049
   170
  done
wenzelm@11049
   171
wenzelm@11049
   172
wenzelm@11049
   173
text {* \medskip @{term noXRRset} *}
wenzelm@11049
   174
wenzelm@11049
   175
lemma RRset_gcd [rule_format]:
wenzelm@11049
   176
    "is_RRset A m ==> a \<in> A --> zgcd (a, m) = #1"
wenzelm@11049
   177
  apply (unfold is_RRset_def)
wenzelm@11049
   178
  apply (rule RsetR.induct)
wenzelm@11049
   179
    apply auto
wenzelm@11049
   180
  done
wenzelm@11049
   181
wenzelm@11049
   182
lemma RsetR_zmult_mono:
wenzelm@11049
   183
  "A \<in> RsetR m ==>
wenzelm@11049
   184
    #0 < m ==> zgcd (x, m) = #1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m"
wenzelm@11049
   185
  apply (erule RsetR.induct)
wenzelm@11049
   186
   apply simp_all
wenzelm@11049
   187
  apply (rule RsetR.insert)
wenzelm@11049
   188
    apply auto
wenzelm@11049
   189
   apply (blast intro: zgcd_zgcd_zmult)
wenzelm@11049
   190
  apply (simp add: zcong_cancel)
wenzelm@11049
   191
  done
wenzelm@11049
   192
wenzelm@11049
   193
lemma card_nor_eq_noX:
wenzelm@11049
   194
  "#0 < m ==>
wenzelm@11049
   195
    zgcd (x, m) = #1 ==> card (noXRRset m x) = card (norRRset m)"
wenzelm@11049
   196
  apply (unfold norRRset_def noXRRset_def)
wenzelm@11049
   197
  apply (rule card_image)
wenzelm@11049
   198
   apply (auto simp add: inj_on_def Bnor_fin)
wenzelm@11049
   199
  apply (simp add: BnorRset.simps)
wenzelm@11049
   200
  done
wenzelm@11049
   201
wenzelm@11049
   202
lemma noX_is_RRset:
wenzelm@11049
   203
    "#0 < m ==> zgcd (x, m) = #1 ==> is_RRset (noXRRset m x) m"
wenzelm@11049
   204
  apply (unfold is_RRset_def phi_def)
wenzelm@11049
   205
  apply (auto simp add: card_nor_eq_noX)
wenzelm@11049
   206
  apply (unfold noXRRset_def norRRset_def)
wenzelm@11049
   207
  apply (rule RsetR_zmult_mono)
wenzelm@11049
   208
    apply (rule Bnor_in_RsetR)
wenzelm@11049
   209
    apply simp_all
wenzelm@11049
   210
  done
paulson@9508
   211
wenzelm@11049
   212
lemma aux_some:
wenzelm@11049
   213
  "#1 < m ==> is_RRset A m ==> a \<in> A
wenzelm@11049
   214
    ==> zcong a (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) m \<and>
wenzelm@11049
   215
      (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) \<in> norRRset m"
wenzelm@11049
   216
  apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex])
wenzelm@11049
   217
   apply (rule_tac [2] RRset_gcd)
wenzelm@11049
   218
    apply simp_all
wenzelm@11049
   219
  done
wenzelm@11049
   220
wenzelm@11049
   221
lemma RRset2norRR_correct:
wenzelm@11049
   222
  "#1 < m ==> is_RRset A m ==> a \<in> A ==>
wenzelm@11049
   223
    [a = RRset2norRR A m a] (mod m) \<and> RRset2norRR A m a \<in> norRRset m"
wenzelm@11049
   224
  apply (unfold RRset2norRR_def)
wenzelm@11049
   225
  apply simp
wenzelm@11049
   226
  apply (rule aux_some)
wenzelm@11049
   227
    apply simp_all
wenzelm@11049
   228
  done
wenzelm@11049
   229
wenzelm@11049
   230
lemmas RRset2norRR_correct1 =
wenzelm@11049
   231
  RRset2norRR_correct [THEN conjunct1, standard]
wenzelm@11049
   232
lemmas RRset2norRR_correct2 =
wenzelm@11049
   233
  RRset2norRR_correct [THEN conjunct2, standard]
wenzelm@11049
   234
wenzelm@11049
   235
lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
wenzelm@11049
   236
  apply (erule RsetR.induct)
wenzelm@11049
   237
   apply auto
wenzelm@11049
   238
  done
wenzelm@11049
   239
wenzelm@11049
   240
lemma RRset_zcong_eq [rule_format]:
wenzelm@11049
   241
  "#1 < m ==>
wenzelm@11049
   242
    is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
wenzelm@11049
   243
  apply (unfold is_RRset_def)
wenzelm@11049
   244
  apply (rule RsetR.induct)
wenzelm@11049
   245
    apply (auto simp add: zcong_sym)
wenzelm@11049
   246
  done
wenzelm@11049
   247
wenzelm@11049
   248
lemma aux:
wenzelm@11049
   249
  "P (SOME a. P a) ==> Q (SOME a. Q a) ==>
wenzelm@11049
   250
    (SOME a. P a) = (SOME a. Q a) ==> \<exists>a. P a \<and> Q a"
wenzelm@11049
   251
  apply auto
wenzelm@11049
   252
  done
wenzelm@11049
   253
wenzelm@11049
   254
lemma RRset2norRR_inj:
wenzelm@11049
   255
    "#1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A"
wenzelm@11049
   256
  apply (unfold RRset2norRR_def inj_on_def)
wenzelm@11049
   257
  apply auto
wenzelm@11049
   258
  apply (subgoal_tac "\<exists>b. ([x = b] (mod m) \<and> b \<in> norRRset m) \<and>
wenzelm@11049
   259
      ([y = b] (mod m) \<and> b \<in> norRRset m)")
wenzelm@11049
   260
   apply (rule_tac [2] aux)
wenzelm@11049
   261
     apply (rule_tac [3] aux_some)
wenzelm@11049
   262
       apply (rule_tac [2] aux_some)
wenzelm@11049
   263
         apply (rule RRset_zcong_eq)
wenzelm@11049
   264
             apply auto
wenzelm@11049
   265
  apply (rule_tac b = b in zcong_trans)
wenzelm@11049
   266
   apply (simp_all add: zcong_sym)
wenzelm@11049
   267
  done
wenzelm@11049
   268
wenzelm@11049
   269
lemma RRset2norRR_eq_norR:
wenzelm@11049
   270
    "#1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m"
wenzelm@11049
   271
  apply (rule card_seteq)
wenzelm@11049
   272
    prefer 3
wenzelm@11049
   273
    apply (subst card_image)
wenzelm@11049
   274
      apply (rule_tac [2] RRset2norRR_inj)
wenzelm@11049
   275
       apply auto
wenzelm@11049
   276
     apply (rule_tac [4] RRset2norRR_correct2)
wenzelm@11049
   277
       apply auto
wenzelm@11049
   278
    apply (unfold is_RRset_def phi_def norRRset_def)
wenzelm@11049
   279
    apply (auto simp add: RsetR_fin Bnor_fin)
wenzelm@11049
   280
  done
wenzelm@11049
   281
wenzelm@11049
   282
wenzelm@11049
   283
lemma aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
wenzelm@11049
   284
  apply (unfold inj_on_def)
wenzelm@11049
   285
  apply auto
wenzelm@11049
   286
  done
paulson@9508
   287
wenzelm@11049
   288
lemma Bnor_prod_power [rule_format]:
wenzelm@11049
   289
  "x \<noteq> #0 ==> a < m --> setprod ((\<lambda>a. a * x) ` BnorRset (a, m)) =
wenzelm@11049
   290
      setprod (BnorRset(a, m)) * x^card (BnorRset (a, m))"
wenzelm@11049
   291
  apply (induct a m rule: BnorRset_induct)
wenzelm@11049
   292
   prefer 2
wenzelm@11049
   293
   apply (subst BnorRset.simps)
wenzelm@11049
   294
   apply (unfold Let_def)
wenzelm@11049
   295
   apply auto
wenzelm@11049
   296
  apply (simp add: Bnor_fin Bnor_mem_zle_swap)
wenzelm@11049
   297
  apply (subst setprod_insert)
wenzelm@11049
   298
    apply (rule_tac [2] aux)
wenzelm@11049
   299
     apply (unfold inj_on_def)
wenzelm@11049
   300
     apply (simp_all add: zmult_ac Bnor_fin finite_imageI
wenzelm@11049
   301
       Bnor_mem_zle_swap)
wenzelm@11049
   302
  done
wenzelm@11049
   303
wenzelm@11049
   304
wenzelm@11049
   305
subsection {* Fermat *}
wenzelm@11049
   306
wenzelm@11049
   307
lemma bijzcong_zcong_prod:
wenzelm@11049
   308
    "(A, B) \<in> bijR (zcongm m) ==> [setprod A = setprod B] (mod m)"
wenzelm@11049
   309
  apply (unfold zcongm_def)
wenzelm@11049
   310
  apply (erule bijR.induct)
wenzelm@11049
   311
   apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B")
wenzelm@11049
   312
    apply (auto intro: fin_bijRl fin_bijRr zcong_zmult)
wenzelm@11049
   313
  done
wenzelm@11049
   314
wenzelm@11049
   315
lemma Bnor_prod_zgcd [rule_format]:
wenzelm@11049
   316
    "a < m --> zgcd (setprod (BnorRset (a, m)), m) = #1"
wenzelm@11049
   317
  apply (induct a m rule: BnorRset_induct)
wenzelm@11049
   318
   prefer 2
wenzelm@11049
   319
   apply (subst BnorRset.simps)
wenzelm@11049
   320
   apply (unfold Let_def)
wenzelm@11049
   321
   apply auto
wenzelm@11049
   322
  apply (simp add: Bnor_fin Bnor_mem_zle_swap)
wenzelm@11049
   323
  apply (blast intro: zgcd_zgcd_zmult)
wenzelm@11049
   324
  done
paulson@9508
   325
wenzelm@11049
   326
theorem Euler_Fermat:
wenzelm@11049
   327
    "#0 < m ==> zgcd (x, m) = #1 ==> [x^(phi m) = #1] (mod m)"
wenzelm@11049
   328
  apply (unfold norRRset_def phi_def)
wenzelm@11049
   329
  apply (case_tac "x = #0")
wenzelm@11049
   330
   apply (case_tac [2] "m = #1")
wenzelm@11049
   331
    apply (rule_tac [3] iffD1)
wenzelm@11049
   332
     apply (rule_tac [3] k = "setprod (BnorRset (m - #1, m))"
wenzelm@11049
   333
       in zcong_cancel2)
wenzelm@11049
   334
      prefer 5
wenzelm@11049
   335
      apply (subst Bnor_prod_power [symmetric])
wenzelm@11049
   336
        apply (rule_tac [7] Bnor_prod_zgcd)
wenzelm@11049
   337
        apply simp_all
wenzelm@11049
   338
  apply (rule bijzcong_zcong_prod)
wenzelm@11049
   339
  apply (fold norRRset_def noXRRset_def)
wenzelm@11049
   340
  apply (subst RRset2norRR_eq_norR [symmetric])
wenzelm@11049
   341
    apply (rule_tac [3] inj_func_bijR)
wenzelm@11049
   342
      apply auto
wenzelm@11049
   343
      apply (unfold zcongm_def)
wenzelm@11049
   344
      apply (rule_tac [3] RRset2norRR_correct1)
wenzelm@11049
   345
        apply (rule_tac [6] RRset2norRR_inj)
wenzelm@11049
   346
         apply (auto intro: order_less_le [THEN iffD2]
wenzelm@11049
   347
	   simp add: noX_is_RRset)
wenzelm@11049
   348
  apply (unfold noXRRset_def norRRset_def)
wenzelm@11049
   349
  apply (rule finite_imageI)
wenzelm@11049
   350
  apply (rule Bnor_fin)
wenzelm@11049
   351
  done
wenzelm@11049
   352
wenzelm@11049
   353
lemma Bnor_prime [rule_format (no_asm)]:
wenzelm@11049
   354
  "p \<in> zprime ==>
wenzelm@11049
   355
    a < p --> (\<forall>b. #0 < b \<and> b \<le> a --> zgcd (b, p) = #1)
wenzelm@11049
   356
    --> card (BnorRset (a, p)) = nat a"
wenzelm@11049
   357
  apply (unfold zprime_def)
wenzelm@11049
   358
  apply (induct a p rule: BnorRset.induct)
wenzelm@11049
   359
  apply (subst BnorRset.simps)
wenzelm@11049
   360
  apply (unfold Let_def)
wenzelm@11049
   361
  apply auto
wenzelm@11049
   362
  done
wenzelm@11049
   363
wenzelm@11049
   364
lemma phi_prime: "p \<in> zprime ==> phi p = nat (p - #1)"
wenzelm@11049
   365
  apply (unfold phi_def norRRset_def)
wenzelm@11049
   366
  apply (rule Bnor_prime)
wenzelm@11049
   367
    apply auto
wenzelm@11049
   368
  apply (erule zless_zprime_imp_zrelprime)
wenzelm@11049
   369
   apply simp_all
wenzelm@11049
   370
  done
wenzelm@11049
   371
wenzelm@11049
   372
theorem Little_Fermat:
wenzelm@11049
   373
    "p \<in> zprime ==> \<not> p dvd x ==> [x^(nat (p - #1)) = #1] (mod p)"
wenzelm@11049
   374
  apply (subst phi_prime [symmetric])
wenzelm@11049
   375
   apply (rule_tac [2] Euler_Fermat)
wenzelm@11049
   376
    apply (erule_tac [3] zprime_imp_zrelprime)
wenzelm@11049
   377
    apply (unfold zprime_def)
wenzelm@11049
   378
    apply auto
wenzelm@11049
   379
  done
paulson@9508
   380
paulson@9508
   381
end