src/HOL/NumberTheory/EulerFermat.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 19670 2e4a143c73c5
child 23755 1c4672d130b1
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
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
haftmann@16417
     9
theory EulerFermat imports BijectionRel IntFact begin
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"
paulson@9508
    22
paulson@9508
    23
inductive "RsetR m"
wenzelm@11049
    24
  intros
wenzelm@11049
    25
    empty [simp]: "{} \<in> RsetR m"
paulson@11868
    26
    insert: "A \<in> RsetR m ==> zgcd (a, m) = 1 ==>
wenzelm@11049
    27
      \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
paulson@9508
    28
wenzelm@19670
    29
consts
wenzelm@19670
    30
  BnorRset :: "int * int => int set"
wenzelm@19670
    31
wenzelm@11049
    32
recdef BnorRset
wenzelm@11049
    33
  "measure ((\<lambda>(a, m). nat a) :: int * int => nat)"
wenzelm@11049
    34
  "BnorRset (a, m) =
paulson@11868
    35
   (if 0 < a then
paulson@11868
    36
    let na = BnorRset (a - 1, m)
paulson@11868
    37
    in (if zgcd (a, m) = 1 then insert a na else na)
wenzelm@11049
    38
    else {})"
paulson@9508
    39
wenzelm@19670
    40
definition
wenzelm@21404
    41
  norRRset :: "int => int set" where
wenzelm@19670
    42
  "norRRset m = BnorRset (m - 1, m)"
wenzelm@19670
    43
wenzelm@21404
    44
definition
wenzelm@21404
    45
  noXRRset :: "int => int => int set" where
wenzelm@19670
    46
  "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
wenzelm@19670
    47
wenzelm@21404
    48
definition
wenzelm@21404
    49
  phi :: "int => nat" where
wenzelm@19670
    50
  "phi m = card (norRRset m)"
wenzelm@19670
    51
wenzelm@21404
    52
definition
wenzelm@21404
    53
  is_RRset :: "int set => int => bool" where
wenzelm@19670
    54
  "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
wenzelm@19670
    55
wenzelm@21404
    56
definition
wenzelm@21404
    57
  RRset2norRR :: "int set => int => int => int" where
wenzelm@19670
    58
  "RRset2norRR A m a =
paulson@11868
    59
     (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
wenzelm@11049
    60
        SOME b. zcong a b m \<and> b \<in> norRRset m
paulson@11868
    61
      else 0)"
wenzelm@11049
    62
wenzelm@21404
    63
definition
wenzelm@21404
    64
  zcongm :: "int => int => int => bool" where
wenzelm@19670
    65
  "zcongm m = (\<lambda>a b. zcong a b m)"
wenzelm@11049
    66
paulson@11868
    67
lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
wenzelm@11049
    68
  -- {* LCP: not sure why this lemma is needed now *}
wenzelm@18369
    69
  by (auto simp add: abs_if)
wenzelm@11049
    70
wenzelm@11049
    71
wenzelm@11049
    72
text {* \medskip @{text norRRset} *}
wenzelm@11049
    73
wenzelm@11049
    74
declare BnorRset.simps [simp del]
wenzelm@11049
    75
wenzelm@11049
    76
lemma BnorRset_induct:
wenzelm@18369
    77
  assumes "!!a m. P {} a m"
wenzelm@18369
    78
    and "!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m
wenzelm@18369
    79
      ==> P (BnorRset(a,m)) a m"
wenzelm@18369
    80
  shows "P (BnorRset(u,v)) u v"
wenzelm@18369
    81
  apply (rule BnorRset.induct)
wenzelm@18369
    82
  apply safe
wenzelm@18369
    83
   apply (case_tac [2] "0 < a")
wenzelm@18369
    84
    apply (rule_tac [2] prems)
wenzelm@18369
    85
     apply simp_all
wenzelm@18369
    86
   apply (simp_all add: BnorRset.simps prems)
wenzelm@11049
    87
  done
wenzelm@11049
    88
wenzelm@18369
    89
lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) \<longrightarrow> b \<le> a"
wenzelm@11049
    90
  apply (induct a m rule: BnorRset_induct)
wenzelm@18369
    91
   apply simp
wenzelm@18369
    92
  apply (subst BnorRset.simps)
paulson@13833
    93
   apply (unfold Let_def, auto)
wenzelm@11049
    94
  done
wenzelm@11049
    95
wenzelm@11049
    96
lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)"
wenzelm@18369
    97
  by (auto dest: Bnor_mem_zle)
wenzelm@11049
    98
paulson@11868
    99
lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> 0 < b"
wenzelm@11049
   100
  apply (induct a m rule: BnorRset_induct)
wenzelm@11049
   101
   prefer 2
wenzelm@11049
   102
   apply (subst BnorRset.simps)
paulson@13833
   103
   apply (unfold Let_def, auto)
wenzelm@11049
   104
  done
wenzelm@11049
   105
wenzelm@11049
   106
lemma Bnor_mem_if [rule_format]:
paulson@11868
   107
    "zgcd (b, m) = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
paulson@13833
   108
  apply (induct a m rule: BnorRset.induct, auto)
wenzelm@11049
   109
   apply (subst BnorRset.simps)
wenzelm@11049
   110
   defer
wenzelm@11049
   111
   apply (subst BnorRset.simps)
paulson@13833
   112
   apply (unfold Let_def, auto)
wenzelm@11049
   113
  done
paulson@9508
   114
wenzelm@11049
   115
lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset (a, m) \<in> RsetR m"
paulson@13833
   116
  apply (induct a m rule: BnorRset_induct, simp)
wenzelm@11049
   117
  apply (subst BnorRset.simps)
paulson@13833
   118
  apply (unfold Let_def, auto)
wenzelm@11049
   119
  apply (rule RsetR.insert)
wenzelm@11049
   120
    apply (rule_tac [3] allI)
wenzelm@11049
   121
    apply (rule_tac [3] impI)
wenzelm@11049
   122
    apply (rule_tac [3] zcong_not)
paulson@11868
   123
       apply (subgoal_tac [6] "a' \<le> a - 1")
wenzelm@11049
   124
        apply (rule_tac [7] Bnor_mem_zle)
paulson@13833
   125
        apply (rule_tac [5] Bnor_mem_zg, auto)
wenzelm@11049
   126
  done
wenzelm@11049
   127
wenzelm@11049
   128
lemma Bnor_fin: "finite (BnorRset (a, m))"
wenzelm@11049
   129
  apply (induct a m rule: BnorRset_induct)
wenzelm@11049
   130
   prefer 2
wenzelm@11049
   131
   apply (subst BnorRset.simps)
paulson@13833
   132
   apply (unfold Let_def, auto)
wenzelm@11049
   133
  done
wenzelm@11049
   134
wenzelm@13524
   135
lemma norR_mem_unique_aux: "a \<le> b - 1 ==> a < (b::int)"
wenzelm@11049
   136
  apply auto
wenzelm@11049
   137
  done
paulson@9508
   138
wenzelm@11049
   139
lemma norR_mem_unique:
paulson@11868
   140
  "1 < m ==>
paulson@11868
   141
    zgcd (a, m) = 1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m"
wenzelm@11049
   142
  apply (unfold norRRset_def)
paulson@13833
   143
  apply (cut_tac a = a and m = m in zcong_zless_unique, auto)
wenzelm@11049
   144
   apply (rule_tac [2] m = m in zcong_zless_imp_eq)
wenzelm@11049
   145
       apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
wenzelm@13524
   146
	 order_less_imp_le norR_mem_unique_aux simp add: zcong_sym)
ballarin@14174
   147
  apply (rule_tac x = b in exI, safe)
wenzelm@11049
   148
  apply (rule Bnor_mem_if)
paulson@11868
   149
    apply (case_tac [2] "b = 0")
wenzelm@11049
   150
     apply (auto intro: order_less_le [THEN iffD2])
wenzelm@11049
   151
   prefer 2
wenzelm@11049
   152
   apply (simp only: zcong_def)
wenzelm@11049
   153
   apply (subgoal_tac "zgcd (a, m) = m")
wenzelm@11049
   154
    prefer 2
wenzelm@11049
   155
    apply (subst zdvd_iff_zgcd [symmetric])
wenzelm@11049
   156
     apply (rule_tac [4] zgcd_zcong_zgcd)
wenzelm@11049
   157
       apply (simp_all add: zdvd_zminus_iff zcong_sym)
wenzelm@11049
   158
  done
wenzelm@11049
   159
wenzelm@11049
   160
wenzelm@11049
   161
text {* \medskip @{term noXRRset} *}
wenzelm@11049
   162
wenzelm@11049
   163
lemma RRset_gcd [rule_format]:
paulson@11868
   164
    "is_RRset A m ==> a \<in> A --> zgcd (a, m) = 1"
wenzelm@11049
   165
  apply (unfold is_RRset_def)
paulson@13833
   166
  apply (rule RsetR.induct, auto)
wenzelm@11049
   167
  done
wenzelm@11049
   168
wenzelm@11049
   169
lemma RsetR_zmult_mono:
wenzelm@11049
   170
  "A \<in> RsetR m ==>
paulson@11868
   171
    0 < m ==> zgcd (x, m) = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m"
paulson@13833
   172
  apply (erule RsetR.induct, simp_all)
paulson@13833
   173
  apply (rule RsetR.insert, auto)
wenzelm@11049
   174
   apply (blast intro: zgcd_zgcd_zmult)
wenzelm@11049
   175
  apply (simp add: zcong_cancel)
wenzelm@11049
   176
  done
wenzelm@11049
   177
wenzelm@11049
   178
lemma card_nor_eq_noX:
paulson@11868
   179
  "0 < m ==>
paulson@11868
   180
    zgcd (x, m) = 1 ==> card (noXRRset m x) = card (norRRset m)"
wenzelm@11049
   181
  apply (unfold norRRset_def noXRRset_def)
wenzelm@11049
   182
  apply (rule card_image)
wenzelm@11049
   183
   apply (auto simp add: inj_on_def Bnor_fin)
wenzelm@11049
   184
  apply (simp add: BnorRset.simps)
wenzelm@11049
   185
  done
wenzelm@11049
   186
wenzelm@11049
   187
lemma noX_is_RRset:
paulson@11868
   188
    "0 < m ==> zgcd (x, m) = 1 ==> is_RRset (noXRRset m x) m"
wenzelm@11049
   189
  apply (unfold is_RRset_def phi_def)
wenzelm@11049
   190
  apply (auto simp add: card_nor_eq_noX)
wenzelm@11049
   191
  apply (unfold noXRRset_def norRRset_def)
wenzelm@11049
   192
  apply (rule RsetR_zmult_mono)
paulson@13833
   193
    apply (rule Bnor_in_RsetR, simp_all)
wenzelm@11049
   194
  done
paulson@9508
   195
wenzelm@11049
   196
lemma aux_some:
paulson@11868
   197
  "1 < m ==> is_RRset A m ==> a \<in> A
wenzelm@11049
   198
    ==> zcong a (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) m \<and>
wenzelm@11049
   199
      (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) \<in> norRRset m"
wenzelm@11049
   200
  apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex])
paulson@13833
   201
   apply (rule_tac [2] RRset_gcd, simp_all)
wenzelm@11049
   202
  done
wenzelm@11049
   203
wenzelm@11049
   204
lemma RRset2norRR_correct:
paulson@11868
   205
  "1 < m ==> is_RRset A m ==> a \<in> A ==>
wenzelm@11049
   206
    [a = RRset2norRR A m a] (mod m) \<and> RRset2norRR A m a \<in> norRRset m"
paulson@13833
   207
  apply (unfold RRset2norRR_def, simp)
paulson@13833
   208
  apply (rule aux_some, simp_all)
wenzelm@11049
   209
  done
wenzelm@11049
   210
wenzelm@11049
   211
lemmas RRset2norRR_correct1 =
wenzelm@11049
   212
  RRset2norRR_correct [THEN conjunct1, standard]
wenzelm@11049
   213
lemmas RRset2norRR_correct2 =
wenzelm@11049
   214
  RRset2norRR_correct [THEN conjunct2, standard]
wenzelm@11049
   215
wenzelm@11049
   216
lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
wenzelm@18369
   217
  by (induct set: RsetR) auto
wenzelm@11049
   218
wenzelm@11049
   219
lemma RRset_zcong_eq [rule_format]:
paulson@11868
   220
  "1 < m ==>
wenzelm@11049
   221
    is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
wenzelm@11049
   222
  apply (unfold is_RRset_def)
wenzelm@11049
   223
  apply (rule RsetR.induct)
wenzelm@11049
   224
    apply (auto simp add: zcong_sym)
wenzelm@11049
   225
  done
wenzelm@11049
   226
wenzelm@11049
   227
lemma aux:
wenzelm@11049
   228
  "P (SOME a. P a) ==> Q (SOME a. Q a) ==>
wenzelm@11049
   229
    (SOME a. P a) = (SOME a. Q a) ==> \<exists>a. P a \<and> Q a"
wenzelm@11049
   230
  apply auto
wenzelm@11049
   231
  done
wenzelm@11049
   232
wenzelm@11049
   233
lemma RRset2norRR_inj:
paulson@11868
   234
    "1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A"
paulson@13833
   235
  apply (unfold RRset2norRR_def inj_on_def, auto)
wenzelm@11049
   236
  apply (subgoal_tac "\<exists>b. ([x = b] (mod m) \<and> b \<in> norRRset m) \<and>
wenzelm@11049
   237
      ([y = b] (mod m) \<and> b \<in> norRRset m)")
wenzelm@11049
   238
   apply (rule_tac [2] aux)
wenzelm@11049
   239
     apply (rule_tac [3] aux_some)
wenzelm@11049
   240
       apply (rule_tac [2] aux_some)
paulson@13833
   241
         apply (rule RRset_zcong_eq, auto)
wenzelm@11049
   242
  apply (rule_tac b = b in zcong_trans)
wenzelm@11049
   243
   apply (simp_all add: zcong_sym)
wenzelm@11049
   244
  done
wenzelm@11049
   245
wenzelm@11049
   246
lemma RRset2norRR_eq_norR:
paulson@11868
   247
    "1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m"
wenzelm@11049
   248
  apply (rule card_seteq)
wenzelm@11049
   249
    prefer 3
wenzelm@11049
   250
    apply (subst card_image)
nipkow@15402
   251
      apply (rule_tac RRset2norRR_inj, auto)
nipkow@15402
   252
     apply (rule_tac [3] RRset2norRR_correct2, auto)
wenzelm@11049
   253
    apply (unfold is_RRset_def phi_def norRRset_def)
nipkow@15402
   254
    apply (auto simp add: Bnor_fin)
wenzelm@11049
   255
  done
wenzelm@11049
   256
wenzelm@11049
   257
wenzelm@13524
   258
lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
paulson@13833
   259
by (unfold inj_on_def, auto)
paulson@9508
   260
wenzelm@11049
   261
lemma Bnor_prod_power [rule_format]:
nipkow@15392
   262
  "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset (a, m)) =
nipkow@15392
   263
      \<Prod>(BnorRset(a, m)) * x^card (BnorRset (a, m))"
wenzelm@11049
   264
  apply (induct a m rule: BnorRset_induct)
wenzelm@11049
   265
   prefer 2
paulson@15481
   266
   apply (simplesubst BnorRset.simps)  --{*multiple redexes*}
paulson@13833
   267
   apply (unfold Let_def, auto)
wenzelm@11049
   268
  apply (simp add: Bnor_fin Bnor_mem_zle_swap)
wenzelm@11049
   269
  apply (subst setprod_insert)
wenzelm@13524
   270
    apply (rule_tac [2] Bnor_prod_power_aux)
wenzelm@11049
   271
     apply (unfold inj_on_def)
wenzelm@11049
   272
     apply (simp_all add: zmult_ac Bnor_fin finite_imageI
wenzelm@11049
   273
       Bnor_mem_zle_swap)
wenzelm@11049
   274
  done
wenzelm@11049
   275
wenzelm@11049
   276
wenzelm@11049
   277
subsection {* Fermat *}
wenzelm@11049
   278
wenzelm@11049
   279
lemma bijzcong_zcong_prod:
nipkow@15392
   280
    "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)"
wenzelm@11049
   281
  apply (unfold zcongm_def)
wenzelm@11049
   282
  apply (erule bijR.induct)
wenzelm@11049
   283
   apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B")
wenzelm@11049
   284
    apply (auto intro: fin_bijRl fin_bijRr zcong_zmult)
wenzelm@11049
   285
  done
wenzelm@11049
   286
wenzelm@11049
   287
lemma Bnor_prod_zgcd [rule_format]:
nipkow@15392
   288
    "a < m --> zgcd (\<Prod>(BnorRset(a, m)), m) = 1"
wenzelm@11049
   289
  apply (induct a m rule: BnorRset_induct)
wenzelm@11049
   290
   prefer 2
wenzelm@11049
   291
   apply (subst BnorRset.simps)
paulson@13833
   292
   apply (unfold Let_def, auto)
wenzelm@11049
   293
  apply (simp add: Bnor_fin Bnor_mem_zle_swap)
wenzelm@11049
   294
  apply (blast intro: zgcd_zgcd_zmult)
wenzelm@11049
   295
  done
paulson@9508
   296
wenzelm@11049
   297
theorem Euler_Fermat:
paulson@11868
   298
    "0 < m ==> zgcd (x, m) = 1 ==> [x^(phi m) = 1] (mod m)"
wenzelm@11049
   299
  apply (unfold norRRset_def phi_def)
paulson@11868
   300
  apply (case_tac "x = 0")
paulson@11868
   301
   apply (case_tac [2] "m = 1")
wenzelm@11049
   302
    apply (rule_tac [3] iffD1)
nipkow@15392
   303
     apply (rule_tac [3] k = "\<Prod>(BnorRset(m - 1, m))"
wenzelm@11049
   304
       in zcong_cancel2)
wenzelm@11049
   305
      prefer 5
wenzelm@11049
   306
      apply (subst Bnor_prod_power [symmetric])
paulson@13833
   307
        apply (rule_tac [7] Bnor_prod_zgcd, simp_all)
wenzelm@11049
   308
  apply (rule bijzcong_zcong_prod)
wenzelm@11049
   309
  apply (fold norRRset_def noXRRset_def)
wenzelm@11049
   310
  apply (subst RRset2norRR_eq_norR [symmetric])
paulson@13833
   311
    apply (rule_tac [3] inj_func_bijR, auto)
nipkow@13187
   312
     apply (unfold zcongm_def)
nipkow@13187
   313
     apply (rule_tac [2] RRset2norRR_correct1)
nipkow@13187
   314
       apply (rule_tac [5] RRset2norRR_inj)
nipkow@13187
   315
        apply (auto intro: order_less_le [THEN iffD2]
wenzelm@11049
   316
	   simp add: noX_is_RRset)
wenzelm@11049
   317
  apply (unfold noXRRset_def norRRset_def)
wenzelm@11049
   318
  apply (rule finite_imageI)
wenzelm@11049
   319
  apply (rule Bnor_fin)
wenzelm@11049
   320
  done
wenzelm@11049
   321
nipkow@16733
   322
lemma Bnor_prime:
nipkow@16733
   323
  "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset (a, p)) = nat a"
wenzelm@11049
   324
  apply (induct a p rule: BnorRset.induct)
wenzelm@11049
   325
  apply (subst BnorRset.simps)
nipkow@16733
   326
  apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime)
paulson@13833
   327
  apply (subgoal_tac "finite (BnorRset (a - 1,m))")
paulson@13833
   328
   apply (subgoal_tac "a ~: BnorRset (a - 1,m)")
paulson@13833
   329
    apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1)
paulson@13833
   330
   apply (frule Bnor_mem_zle, arith)
paulson@13833
   331
  apply (frule Bnor_fin)
wenzelm@11049
   332
  done
wenzelm@11049
   333
nipkow@16663
   334
lemma phi_prime: "zprime p ==> phi p = nat (p - 1)"
wenzelm@11049
   335
  apply (unfold phi_def norRRset_def)
paulson@13833
   336
  apply (rule Bnor_prime, auto)
wenzelm@11049
   337
  done
wenzelm@11049
   338
wenzelm@11049
   339
theorem Little_Fermat:
nipkow@16663
   340
    "zprime p ==> \<not> p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)"
wenzelm@11049
   341
  apply (subst phi_prime [symmetric])
wenzelm@11049
   342
   apply (rule_tac [2] Euler_Fermat)
wenzelm@11049
   343
    apply (erule_tac [3] zprime_imp_zrelprime)
paulson@13833
   344
    apply (unfold zprime_def, auto)
wenzelm@11049
   345
  done
paulson@9508
   346
paulson@9508
   347
end