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