src/HOL/Number_Theory/Residues.thy
author haftmann
Wed Apr 12 09:27:43 2017 +0200 (2017-04-12)
changeset 65465 067210a08a22
parent 65416 f707dbcf11e3
child 65726 f5d64d094efe
permissions -rw-r--r--
more fundamental euler's totient function on nat rather than int;
avoid generic name phi;
separate theory for euler's totient function
wenzelm@41959
     1
(*  Title:      HOL/Number_Theory/Residues.thy
nipkow@31719
     2
    Author:     Jeremy Avigad
nipkow@31719
     3
wenzelm@41541
     4
An algebraic treatment of residue rings, and resulting proofs of
wenzelm@41959
     5
Euler's theorem and Wilson's theorem.
nipkow@31719
     6
*)
nipkow@31719
     7
wenzelm@60526
     8
section \<open>Residue rings\<close>
nipkow@31719
     9
nipkow@31719
    10
theory Residues
haftmann@65416
    11
imports
haftmann@65416
    12
  Cong
haftmann@65416
    13
  "~~/src/HOL/Algebra/More_Group"
haftmann@65416
    14
  "~~/src/HOL/Algebra/More_Ring"
haftmann@65416
    15
  "~~/src/HOL/Algebra/More_Finite_Product"
haftmann@65416
    16
  "~~/src/HOL/Algebra/Multiplicative_Group"
haftmann@65465
    17
  Totient
nipkow@31719
    18
begin
nipkow@31719
    19
eberlm@64282
    20
definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" where
eberlm@64282
    21
  "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))"
eberlm@64282
    22
eberlm@64282
    23
definition Legendre :: "int \<Rightarrow> int \<Rightarrow> int" where
eberlm@64282
    24
  "Legendre a p = (if ([a = 0] (mod p)) then 0
eberlm@64282
    25
    else if QuadRes p a then 1
eberlm@64282
    26
    else -1)"
eberlm@64282
    27
wenzelm@60527
    28
subsection \<open>A locale for residue rings\<close>
nipkow@31719
    29
wenzelm@60527
    30
definition residue_ring :: "int \<Rightarrow> int ring"
wenzelm@60528
    31
where
wenzelm@60527
    32
  "residue_ring m =
wenzelm@60527
    33
    \<lparr>carrier = {0..m - 1},
wenzelm@60527
    34
     mult = \<lambda>x y. (x * y) mod m,
wenzelm@60527
    35
     one = 1,
wenzelm@60527
    36
     zero = 0,
wenzelm@60527
    37
     add = \<lambda>x y. (x + y) mod m\<rparr>"
nipkow@31719
    38
nipkow@31719
    39
locale residues =
nipkow@31719
    40
  fixes m :: int and R (structure)
nipkow@31719
    41
  assumes m_gt_one: "m > 1"
wenzelm@60527
    42
  defines "R \<equiv> residue_ring m"
wenzelm@44872
    43
begin
nipkow@31719
    44
nipkow@31719
    45
lemma abelian_group: "abelian_group R"
lp15@65066
    46
proof -
lp15@65066
    47
  have "\<exists>y\<in>{0..m - 1}. (x + y) mod m = 0" if "0 \<le> x" "x < m" for x
lp15@65066
    48
  proof (cases "x = 0")
lp15@65066
    49
    case True
lp15@65066
    50
    with m_gt_one show ?thesis by simp
lp15@65066
    51
  next
lp15@65066
    52
    case False
lp15@65066
    53
    then have "(x + (m - x)) mod m = 0"
lp15@65066
    54
      by simp
lp15@65066
    55
    with m_gt_one that show ?thesis
lp15@65066
    56
      by (metis False atLeastAtMost_iff diff_ge_0_iff_ge diff_left_mono int_one_le_iff_zero_less less_le)
lp15@65066
    57
  qed
lp15@65066
    58
  with m_gt_one show ?thesis
lp15@65066
    59
    by (fastforce simp add: R_def residue_ring_def mod_add_right_eq ac_simps  intro!: abelian_groupI)
lp15@65066
    60
qed    
nipkow@31719
    61
nipkow@31719
    62
lemma comm_monoid: "comm_monoid R"
lp15@65066
    63
  unfolding R_def residue_ring_def
nipkow@31719
    64
  apply (rule comm_monoidI)
lp15@65066
    65
    using m_gt_one  apply auto
lp15@65066
    66
  apply (metis mod_mult_right_eq mult.assoc mult.commute)
lp15@65066
    67
  apply (metis mult.commute)
wenzelm@41541
    68
  done
nipkow@31719
    69
nipkow@31719
    70
lemma cring: "cring R"
lp15@65066
    71
  apply (intro cringI abelian_group comm_monoid)
lp15@65066
    72
  unfolding R_def residue_ring_def
lp15@65066
    73
  apply (auto simp add: comm_semiring_class.distrib mod_add_eq mod_mult_left_eq)
wenzelm@41541
    74
  done
nipkow@31719
    75
nipkow@31719
    76
end
nipkow@31719
    77
nipkow@31719
    78
sublocale residues < cring
nipkow@31719
    79
  by (rule cring)
nipkow@31719
    80
nipkow@31719
    81
wenzelm@41541
    82
context residues
wenzelm@41541
    83
begin
nipkow@31719
    84
wenzelm@60527
    85
text \<open>
wenzelm@60527
    86
  These lemmas translate back and forth between internal and
wenzelm@60527
    87
  external concepts.
wenzelm@60527
    88
\<close>
nipkow@31719
    89
nipkow@31719
    90
lemma res_carrier_eq: "carrier R = {0..m - 1}"
wenzelm@44872
    91
  unfolding R_def residue_ring_def by auto
nipkow@31719
    92
nipkow@31719
    93
lemma res_add_eq: "x \<oplus> y = (x + y) mod m"
wenzelm@44872
    94
  unfolding R_def residue_ring_def by auto
nipkow@31719
    95
nipkow@31719
    96
lemma res_mult_eq: "x \<otimes> y = (x * y) mod m"
wenzelm@44872
    97
  unfolding R_def residue_ring_def by auto
nipkow@31719
    98
nipkow@31719
    99
lemma res_zero_eq: "\<zero> = 0"
wenzelm@44872
   100
  unfolding R_def residue_ring_def by auto
nipkow@31719
   101
nipkow@31719
   102
lemma res_one_eq: "\<one> = 1"
wenzelm@44872
   103
  unfolding R_def residue_ring_def units_of_def by auto
nipkow@31719
   104
wenzelm@60527
   105
lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
lp15@65066
   106
  using m_gt_one
lp15@65066
   107
  unfolding Units_def R_def residue_ring_def
nipkow@31719
   108
  apply auto
wenzelm@60527
   109
  apply (subgoal_tac "x \<noteq> 0")
nipkow@31719
   110
  apply auto
lp15@55352
   111
  apply (metis invertible_coprime_int)
nipkow@31952
   112
  apply (subst (asm) coprime_iff_invertible'_int)
haftmann@57512
   113
  apply (auto simp add: cong_int_def mult.commute)
wenzelm@41541
   114
  done
nipkow@31719
   115
nipkow@31719
   116
lemma res_neg_eq: "\<ominus> x = (- x) mod m"
lp15@65066
   117
  using m_gt_one unfolding R_def a_inv_def m_inv_def residue_ring_def
lp15@65066
   118
  apply simp
nipkow@31719
   119
  apply (rule the_equality)
lp15@65066
   120
  apply (simp add: mod_add_right_eq)
lp15@65066
   121
  apply (simp add: add.commute mod_add_right_eq)
lp15@65066
   122
  apply (metis add.right_neutral minus_add_cancel mod_add_right_eq mod_pos_pos_trivial)
wenzelm@41541
   123
  done
nipkow@31719
   124
wenzelm@44872
   125
lemma finite [iff]: "finite (carrier R)"
haftmann@65416
   126
  by (simp add: res_carrier_eq)
nipkow@31719
   127
wenzelm@44872
   128
lemma finite_Units [iff]: "finite (Units R)"
haftmann@65416
   129
  by (simp add: finite_ring_finite_units)
nipkow@31719
   130
wenzelm@60527
   131
text \<open>
wenzelm@63167
   132
  The function \<open>a \<mapsto> a mod m\<close> maps the integers to the
wenzelm@60527
   133
  residue classes. The following lemmas show that this mapping
wenzelm@60527
   134
  respects addition and multiplication on the integers.
wenzelm@60527
   135
\<close>
nipkow@31719
   136
wenzelm@60527
   137
lemma mod_in_carrier [iff]: "a mod m \<in> carrier R"
wenzelm@60527
   138
  unfolding res_carrier_eq
wenzelm@60527
   139
  using insert m_gt_one by auto
nipkow@31719
   140
nipkow@31719
   141
lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
wenzelm@44872
   142
  unfolding R_def residue_ring_def
haftmann@64593
   143
  by (auto simp add: mod_simps)
nipkow@31719
   144
nipkow@31719
   145
lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
lp15@55352
   146
  unfolding R_def residue_ring_def
haftmann@64593
   147
  by (auto simp add: mod_simps)
nipkow@31719
   148
nipkow@31719
   149
lemma zero_cong: "\<zero> = 0"
wenzelm@44872
   150
  unfolding R_def residue_ring_def by auto
nipkow@31719
   151
nipkow@31719
   152
lemma one_cong: "\<one> = 1 mod m"
wenzelm@44872
   153
  using m_gt_one unfolding R_def residue_ring_def by auto
nipkow@31719
   154
wenzelm@60527
   155
(* FIXME revise algebra library to use 1? *)
nipkow@31719
   156
lemma pow_cong: "(x mod m) (^) n = x^n mod m"
lp15@65066
   157
  using m_gt_one
nipkow@31719
   158
  apply (induct n)
wenzelm@41541
   159
  apply (auto simp add: nat_pow_def one_cong)
haftmann@57512
   160
  apply (metis mult.commute mult_cong)
wenzelm@41541
   161
  done
nipkow@31719
   162
nipkow@31719
   163
lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m"
lp15@55352
   164
  by (metis mod_minus_eq res_neg_eq)
nipkow@31719
   165
wenzelm@60528
   166
lemma (in residues) prod_cong: "finite A \<Longrightarrow> (\<Otimes>i\<in>A. (f i) mod m) = (\<Prod>i\<in>A. f i) mod m"
lp15@55352
   167
  by (induct set: finite) (auto simp: one_cong mult_cong)
nipkow@31719
   168
wenzelm@60528
   169
lemma (in residues) sum_cong: "finite A \<Longrightarrow> (\<Oplus>i\<in>A. (f i) mod m) = (\<Sum>i\<in>A. f i) mod m"
lp15@55352
   170
  by (induct set: finite) (auto simp: zero_cong add_cong)
nipkow@31719
   171
haftmann@60688
   172
lemma mod_in_res_units [simp]:
haftmann@60688
   173
  assumes "1 < m" and "coprime a m"
haftmann@60688
   174
  shows "a mod m \<in> Units R"
haftmann@60688
   175
proof (cases "a mod m = 0")
haftmann@60688
   176
  case True with assms show ?thesis
haftmann@60688
   177
    by (auto simp add: res_units_eq gcd_red_int [symmetric])
haftmann@60688
   178
next
haftmann@60688
   179
  case False
haftmann@60688
   180
  from assms have "0 < m" by simp
haftmann@60688
   181
  with pos_mod_sign [of m a] have "0 \<le> a mod m" .
haftmann@60688
   182
  with False have "0 < a mod m" by simp
haftmann@60688
   183
  with assms show ?thesis
haftmann@60688
   184
    by (auto simp add: res_units_eq gcd_red_int [symmetric] ac_simps)
haftmann@60688
   185
qed
nipkow@31719
   186
wenzelm@60528
   187
lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)"
nipkow@31719
   188
  unfolding cong_int_def by auto
nipkow@31719
   189
nipkow@31719
   190
wenzelm@60528
   191
text \<open>Simplifying with these will translate a ring equation in R to a congruence.\<close>
nipkow@31719
   192
lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong
nipkow@31719
   193
    prod_cong sum_cong neg_cong res_eq_to_cong
nipkow@31719
   194
wenzelm@60527
   195
text \<open>Other useful facts about the residue ring.\<close>
nipkow@31719
   196
lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2"
nipkow@31719
   197
  apply (simp add: res_one_eq res_neg_eq)
haftmann@57512
   198
  apply (metis add.commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff
wenzelm@60528
   199
    zero_neq_one zmod_zminus1_eq_if)
wenzelm@41541
   200
  done
nipkow@31719
   201
nipkow@31719
   202
end
nipkow@31719
   203
nipkow@31719
   204
wenzelm@60527
   205
subsection \<open>Prime residues\<close>
nipkow@31719
   206
nipkow@31719
   207
locale residues_prime =
eberlm@63534
   208
  fixes p :: nat and R (structure)
nipkow@31719
   209
  assumes p_prime [intro]: "prime p"
eberlm@63534
   210
  defines "R \<equiv> residue_ring (int p)"
nipkow@31719
   211
nipkow@31719
   212
sublocale residues_prime < residues p
lp15@65066
   213
  unfolding R_def residues_def
nipkow@31719
   214
  using p_prime apply auto
haftmann@62348
   215
  apply (metis (full_types) of_nat_1 of_nat_less_iff prime_gt_1_nat)
wenzelm@41541
   216
  done
nipkow@31719
   217
wenzelm@44872
   218
context residues_prime
wenzelm@44872
   219
begin
nipkow@31719
   220
nipkow@31719
   221
lemma is_field: "field R"
lp15@65066
   222
proof -
lp15@65066
   223
  have "\<And>x. \<lbrakk>gcd x (int p) \<noteq> 1; 0 \<le> x; x < int p\<rbrakk> \<Longrightarrow> x = 0"
lp15@65066
   224
    by (metis dual_order.order_iff_strict gcd.commute less_le_not_le p_prime prime_imp_coprime prime_nat_int_transfer zdvd_imp_le)
lp15@65066
   225
  then show ?thesis
lp15@65066
   226
  apply (intro cring.field_intro2 cring)
wenzelm@44872
   227
  apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
lp15@65066
   228
    done
lp15@65066
   229
qed
nipkow@31719
   230
nipkow@31719
   231
lemma res_prime_units_eq: "Units R = {1..p - 1}"
nipkow@31719
   232
  apply (subst res_units_eq)
nipkow@31719
   233
  apply auto
haftmann@62348
   234
  apply (subst gcd.commute)
lp15@55352
   235
  apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless)
wenzelm@41541
   236
  done
nipkow@31719
   237
nipkow@31719
   238
end
nipkow@31719
   239
nipkow@31719
   240
sublocale residues_prime < field
nipkow@31719
   241
  by (rule is_field)
nipkow@31719
   242
nipkow@31719
   243
wenzelm@60527
   244
section \<open>Test cases: Euler's theorem and Wilson's theorem\<close>
nipkow@31719
   245
wenzelm@60527
   246
subsection \<open>Euler's theorem\<close>
nipkow@31719
   247
haftmann@65465
   248
lemma (in residues) totient_eq:
haftmann@65465
   249
  "totient (nat m) = card (Units R)"
lp15@55261
   250
proof -
haftmann@65465
   251
  have *: "inj_on nat (Units R)"
haftmann@65465
   252
    by (rule inj_onI) (auto simp add: res_units_eq)
haftmann@65465
   253
  have "totatives (nat m) = nat ` Units R"
haftmann@65465
   254
    by (auto simp add: res_units_eq totatives_def transfer_nat_int_gcd(1))
haftmann@65465
   255
      (smt One_nat_def image_def mem_Collect_eq nat_0 nat_eq_iff nat_less_iff of_nat_1 transfer_int_nat_gcd(1))
haftmann@65465
   256
  then have "card (totatives (nat m)) = card (nat ` Units R)"
haftmann@65465
   257
    by simp
haftmann@65465
   258
  also have "\<dots> = card (Units R)"
haftmann@65465
   259
    using * card_image [of nat "Units R"] by auto
haftmann@65465
   260
  finally show ?thesis
haftmann@65465
   261
    by simp
lp15@55261
   262
qed
lp15@55261
   263
haftmann@65465
   264
lemma (in residues_prime) totient_eq: "totient p = p - 1"
haftmann@65465
   265
  using totient_eq by (simp add: res_prime_units_eq)
nipkow@31719
   266
haftmann@65465
   267
lemma (in residues) euler_theorem:
haftmann@65465
   268
  assumes "coprime a m"
haftmann@65465
   269
  shows "[a ^ totient (nat m) = 1] (mod m)"
haftmann@65416
   270
proof -
haftmann@65465
   271
  have "a ^ totient (nat m) mod m = 1 mod m"
haftmann@65465
   272
    by (metis assms finite_Units m_gt_one mod_in_res_units one_cong totient_eq pow_cong units_power_order_eq_one)
lp15@65066
   273
  then show ?thesis
lp15@65066
   274
    using res_eq_to_cong by blast
nipkow@31719
   275
qed
nipkow@31719
   276
nipkow@31719
   277
lemma euler_theorem:
haftmann@65465
   278
  fixes a m :: nat
haftmann@65465
   279
  assumes "coprime a m"
haftmann@65465
   280
  shows "[a ^ totient m = 1] (mod m)"
wenzelm@60527
   281
proof (cases "m = 0 | m = 1")
wenzelm@60527
   282
  case True
wenzelm@44872
   283
  then show ?thesis by auto
nipkow@31719
   284
next
wenzelm@60527
   285
  case False
wenzelm@41541
   286
  with assms show ?thesis
haftmann@65465
   287
    using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong
haftmann@65465
   288
    by (auto simp add: residues_def transfer_int_nat_gcd(1)) force
nipkow@31719
   289
qed
nipkow@31719
   290
nipkow@31719
   291
lemma fermat_theorem:
haftmann@65465
   292
  fixes p a :: nat
haftmann@65465
   293
  assumes "prime p" and "\<not> p dvd a"
haftmann@65465
   294
  shows "[a ^ (p - 1) = 1] (mod p)"
nipkow@31719
   295
proof -
haftmann@65465
   296
  from assms prime_imp_coprime [of p a] have "coprime a p"
haftmann@65465
   297
    by (auto simp add: ac_simps)
haftmann@65465
   298
  then have "[a ^ totient p = 1] (mod p)"
haftmann@65465
   299
     by (rule euler_theorem)
haftmann@65465
   300
  also have "totient p = p - 1"
haftmann@65465
   301
    by (rule prime_totient) (rule assms)
haftmann@65465
   302
  finally show ?thesis .
nipkow@31719
   303
qed
nipkow@31719
   304
nipkow@31719
   305
wenzelm@60526
   306
subsection \<open>Wilson's theorem\<close>
nipkow@31719
   307
wenzelm@60527
   308
lemma (in field) inv_pair_lemma: "x \<in> Units R \<Longrightarrow> y \<in> Units R \<Longrightarrow>
wenzelm@60527
   309
    {x, inv x} \<noteq> {y, inv y} \<Longrightarrow> {x, inv x} \<inter> {y, inv y} = {}"
nipkow@31719
   310
  apply auto
lp15@55352
   311
  apply (metis Units_inv_inv)+
wenzelm@41541
   312
  done
nipkow@31719
   313
nipkow@31719
   314
lemma (in residues_prime) wilson_theorem1:
nipkow@31719
   315
  assumes a: "p > 2"
lp15@59730
   316
  shows "[fact (p - 1) = (-1::int)] (mod p)"
nipkow@31719
   317
proof -
wenzelm@60527
   318
  let ?Inverse_Pairs = "{{x, inv x}| x. x \<in> Units R - {\<one>, \<ominus> \<one>}}"
wenzelm@60527
   319
  have UR: "Units R = {\<one>, \<ominus> \<one>} \<union> \<Union>?Inverse_Pairs"
nipkow@31719
   320
    by auto
wenzelm@60527
   321
  have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i\<in>\<Union>?Inverse_Pairs. i)"
nipkow@31732
   322
    apply (subst UR)
nipkow@31719
   323
    apply (subst finprod_Un_disjoint)
lp15@55352
   324
    apply (auto intro: funcsetI)
wenzelm@60527
   325
    using inv_one apply auto[1]
wenzelm@60527
   326
    using inv_eq_neg_one_eq apply auto
nipkow@31719
   327
    done
wenzelm@60527
   328
  also have "(\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"
nipkow@31719
   329
    apply (subst finprod_insert)
nipkow@31719
   330
    apply auto
nipkow@31719
   331
    apply (frule one_eq_neg_one)
wenzelm@60527
   332
    using a apply force
nipkow@31719
   333
    done
wenzelm@60527
   334
  also have "(\<Otimes>i\<in>(\<Union>?Inverse_Pairs). i) = (\<Otimes>A\<in>?Inverse_Pairs. (\<Otimes>y\<in>A. y))"
wenzelm@60527
   335
    apply (subst finprod_Union_disjoint)
wenzelm@60527
   336
    apply auto
lp15@55352
   337
    apply (metis Units_inv_inv)+
nipkow@31719
   338
    done
nipkow@31719
   339
  also have "\<dots> = \<one>"
wenzelm@60527
   340
    apply (rule finprod_one)
wenzelm@60527
   341
    apply auto
wenzelm@60527
   342
    apply (subst finprod_insert)
wenzelm@60527
   343
    apply auto
lp15@55352
   344
    apply (metis inv_eq_self)
nipkow@31719
   345
    done
wenzelm@60527
   346
  finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>"
nipkow@31719
   347
    by simp
wenzelm@60527
   348
  also have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>Units R. i mod p)"
lp15@65066
   349
    by (rule finprod_cong') (auto simp: res_units_eq)
wenzelm@60527
   350
  also have "\<dots> = (\<Prod>i\<in>Units R. i) mod p"
lp15@65066
   351
    by (rule prod_cong) auto
nipkow@31719
   352
  also have "\<dots> = fact (p - 1) mod p"
nipkow@64272
   353
    apply (simp add: fact_prod)
lp15@65066
   354
    using assms
lp15@55242
   355
    apply (subst res_prime_units_eq)
nipkow@64272
   356
    apply (simp add: int_prod zmod_int prod_int_eq)
nipkow@31719
   357
    done
wenzelm@60527
   358
  finally have "fact (p - 1) mod p = \<ominus> \<one>" .
wenzelm@60527
   359
  then show ?thesis
wenzelm@60528
   360
    by (metis of_nat_fact Divides.transfer_int_nat_functions(2)
wenzelm@60528
   361
      cong_int_def res_neg_eq res_one_eq)
nipkow@31719
   362
qed
nipkow@31719
   363
lp15@55352
   364
lemma wilson_theorem:
wenzelm@60527
   365
  assumes "prime p"
wenzelm@60527
   366
  shows "[fact (p - 1) = - 1] (mod p)"
lp15@55352
   367
proof (cases "p = 2")
lp15@59667
   368
  case True
lp15@55352
   369
  then show ?thesis
nipkow@64272
   370
    by (simp add: cong_int_def fact_prod)
lp15@55352
   371
next
lp15@55352
   372
  case False
lp15@55352
   373
  then show ?thesis
lp15@55352
   374
    using assms prime_ge_2_nat
lp15@55352
   375
    by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq)
lp15@55352
   376
qed
nipkow@31719
   377
haftmann@65416
   378
text {*
haftmann@65416
   379
  This result can be transferred to the multiplicative group of
haftmann@65416
   380
  $\mathbb{Z}/p\mathbb{Z}$ for $p$ prime. *}
haftmann@65416
   381
haftmann@65416
   382
lemma mod_nat_int_pow_eq:
haftmann@65416
   383
  fixes n :: nat and p a :: int
haftmann@65416
   384
  assumes "a \<ge> 0" "p \<ge> 0"
haftmann@65416
   385
  shows "(nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
haftmann@65416
   386
  using assms
haftmann@65416
   387
  by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric])
haftmann@65416
   388
haftmann@65416
   389
theorem residue_prime_mult_group_has_gen :
haftmann@65416
   390
 fixes p :: nat
haftmann@65416
   391
 assumes prime_p : "prime p"
haftmann@65416
   392
 shows "\<exists>a \<in> {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \<in> UNIV}"
haftmann@65416
   393
proof -
haftmann@65416
   394
  have "p\<ge>2" using prime_gt_1_nat[OF prime_p] by simp
haftmann@65416
   395
  interpret R:residues_prime "p" "residue_ring p" unfolding residues_prime_def
haftmann@65416
   396
    by (simp add: prime_p)
haftmann@65416
   397
  have car: "carrier (residue_ring (int p)) - {\<zero>\<^bsub>residue_ring (int p)\<^esub>} =  {1 .. int p - 1}"
haftmann@65416
   398
    by (auto simp add: R.zero_cong R.res_carrier_eq)
haftmann@65416
   399
  obtain a where a:"a \<in> {1 .. int p - 1}"
haftmann@65416
   400
         and a_gen:"{1 .. int p - 1} = {a(^)\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \<in> UNIV}"
haftmann@65416
   401
    apply atomize_elim using field.finite_field_mult_group_has_gen[OF R.is_field]
haftmann@65416
   402
    by (auto simp add: car[symmetric] carrier_mult_of)
haftmann@65416
   403
  { fix x fix i :: nat assume x: "x \<in> {1 .. int p - 1}"
haftmann@65416
   404
    hence "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)" using R.pow_cong[of x i] by auto}
haftmann@65416
   405
  note * = this
haftmann@65416
   406
  have **:"nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
haftmann@65416
   407
  proof
haftmann@65416
   408
    { fix n assume n: "n \<in> ?L"
haftmann@65416
   409
      then have "n \<in> ?R" using `p\<ge>2` by force
haftmann@65416
   410
    } thus "?L \<subseteq> ?R" by blast
haftmann@65416
   411
    { fix n assume n: "n \<in> ?R"
haftmann@65416
   412
      then have "n \<in> ?L" using `p\<ge>2` Set_Interval.transfer_nat_int_set_functions(2) by fastforce
haftmann@65416
   413
    } thus "?R \<subseteq> ?L" by blast
haftmann@65416
   414
  qed
haftmann@65416
   415
  have "nat ` {a^i mod (int p) | i::nat. i \<in> UNIV} = {nat a^i mod p | i . i \<in> UNIV}" (is "?L = ?R")
haftmann@65416
   416
  proof
haftmann@65416
   417
    { fix x assume x: "x \<in> ?L"
haftmann@65416
   418
      then obtain i where i:"x = nat (a^i mod (int p))" by blast
haftmann@65416
   419
      hence "x = nat a ^ i mod p" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
haftmann@65416
   420
      hence "x \<in> ?R" using i by blast
haftmann@65416
   421
    } thus "?L \<subseteq> ?R" by blast
haftmann@65416
   422
    { fix x assume x: "x \<in> ?R"
haftmann@65416
   423
      then obtain i where i:"x = nat a^i mod p" by blast
haftmann@65416
   424
      hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
haftmann@65416
   425
    } thus "?R \<subseteq> ?L" by blast
haftmann@65416
   426
  qed
haftmann@65416
   427
  hence "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"
haftmann@65416
   428
    using * a a_gen ** by presburger
haftmann@65416
   429
  moreover
haftmann@65416
   430
  have "nat a \<in> {1 .. p - 1}" using a by force
haftmann@65416
   431
  ultimately show ?thesis ..
haftmann@65416
   432
qed
haftmann@65416
   433
nipkow@31719
   434
end