src/HOL/Old_Number_Theory/Euler.thy
author huffman
Sun Nov 13 19:26:53 2011 +0100 (2011-11-13)
changeset 45480 a39bb6d42ace
parent 44766 d4d33a4d7548
child 53077 a1b3784f8129
permissions -rw-r--r--
remove unnecessary number-representation-specific rules from metis calls;
speed up another proof
wenzelm@38159
     1
(*  Title:      HOL/Old_Number_Theory/Euler.thy
paulson@13871
     2
    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
paulson@13871
     3
*)
paulson@13871
     4
paulson@13871
     5
header {* Euler's criterion *}
paulson@13871
     6
wenzelm@38159
     7
theory Euler
wenzelm@38159
     8
imports Residues EvenOdd
wenzelm@38159
     9
begin
paulson@13871
    10
wenzelm@38159
    11
definition MultInvPair :: "int => int => int => int set"
wenzelm@38159
    12
  where "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
wenzelm@19670
    13
wenzelm@38159
    14
definition SetS :: "int => int => int set set"
wenzelm@38159
    15
  where "SetS a p = MultInvPair a p ` SRStar p"
paulson@13871
    16
wenzelm@19670
    17
wenzelm@19670
    18
subsection {* Property for MultInvPair *}
paulson@13871
    19
wenzelm@19670
    20
lemma MultInvPair_prop1a:
wenzelm@19670
    21
  "[| zprime p; 2 < p; ~([a = 0](mod p));
wenzelm@19670
    22
      X \<in> (SetS a p); Y \<in> (SetS a p);
wenzelm@19670
    23
      ~((X \<inter> Y) = {}) |] ==> X = Y"
paulson@13871
    24
  apply (auto simp add: SetS_def)
wenzelm@16974
    25
  apply (drule StandardRes_SRStar_prop1a)+ defer 1
wenzelm@16974
    26
  apply (drule StandardRes_SRStar_prop1a)+
paulson@13871
    27
  apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym)
wenzelm@20369
    28
  apply (drule notE, rule MultInv_zcong_prop1, auto)[]
wenzelm@20369
    29
  apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
wenzelm@20369
    30
  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
wenzelm@20369
    31
  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[]
wenzelm@20369
    32
  apply (drule MultInv_zcong_prop1, auto)[]
wenzelm@20369
    33
  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
wenzelm@20369
    34
  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
wenzelm@20369
    35
  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[]
wenzelm@19670
    36
  done
paulson@13871
    37
wenzelm@19670
    38
lemma MultInvPair_prop1b:
wenzelm@19670
    39
  "[| zprime p; 2 < p; ~([a = 0](mod p));
wenzelm@19670
    40
      X \<in> (SetS a p); Y \<in> (SetS a p);
wenzelm@19670
    41
      X \<noteq> Y |] ==> X \<inter> Y = {}"
paulson@13871
    42
  apply (rule notnotD)
paulson@13871
    43
  apply (rule notI)
paulson@13871
    44
  apply (drule MultInvPair_prop1a, auto)
wenzelm@19670
    45
  done
paulson@13871
    46
nipkow@16663
    47
lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>  
paulson@13871
    48
    \<forall>X \<in> SetS a p. \<forall>Y \<in> SetS a p. X \<noteq> Y --> X\<inter>Y = {}"
paulson@13871
    49
  by (auto simp add: MultInvPair_prop1b)
paulson@13871
    50
nipkow@16663
    51
lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> 
wenzelm@16974
    52
                          Union ( SetS a p) = SRStar p"
paulson@13871
    53
  apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4 
paulson@13871
    54
    SRStar_mult_prop2)
paulson@13871
    55
  apply (frule StandardRes_SRStar_prop3)
paulson@13871
    56
  apply (rule bexI, auto)
wenzelm@19670
    57
  done
paulson@13871
    58
wenzelm@41541
    59
lemma MultInvPair_distinct:
wenzelm@41541
    60
  assumes "zprime p" and "2 < p" and
wenzelm@41541
    61
    "~([a = 0] (mod p))" and
wenzelm@41541
    62
    "~([j = 0] (mod p))" and
wenzelm@41541
    63
    "~(QuadRes p a)"
wenzelm@41541
    64
  shows "~([j = a * MultInv p j] (mod p))"
wenzelm@20369
    65
proof
wenzelm@16974
    66
  assume "[j = a * MultInv p j] (mod p)"
wenzelm@16974
    67
  then have "[j * j = (a * MultInv p j) * j] (mod p)"
paulson@13871
    68
    by (auto simp add: zcong_scalar)
wenzelm@16974
    69
  then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
huffman@44766
    70
    by (auto simp add: mult_ac)
wenzelm@16974
    71
  have "[j * j = a] (mod p)"
wenzelm@41541
    72
  proof -
wenzelm@41541
    73
    from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)"
wenzelm@41541
    74
      by (simp add: MultInv_prop2a)
wenzelm@41541
    75
    from this and a show ?thesis
wenzelm@41541
    76
      by (auto simp add: zcong_zmult_prop2)
wenzelm@41541
    77
  qed
wenzelm@41541
    78
  then have "[j^2 = a] (mod p)" by (simp add: power2_eq_square)
wenzelm@41541
    79
  with assms show False by (simp add: QuadRes_def)
wenzelm@16974
    80
qed
paulson@13871
    81
nipkow@16663
    82
lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
paulson@13871
    83
                                ~(QuadRes p a); ~([j = 0] (mod p)) |]  ==> 
wenzelm@16974
    84
                             card (MultInvPair a p j) = 2"
paulson@13871
    85
  apply (auto simp add: MultInvPair_def)
wenzelm@16974
    86
  apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))")
paulson@13871
    87
  apply auto
huffman@45480
    88
  apply (metis MultInvPair_distinct StandardRes_def aux)
wenzelm@20369
    89
  done
paulson@13871
    90
wenzelm@19670
    91
wenzelm@19670
    92
subsection {* Properties of SetS *}
paulson@13871
    93
wenzelm@16974
    94
lemma SetS_finite: "2 < p ==> finite (SetS a p)"
nipkow@40786
    95
  by (auto simp add: SetS_def SRStar_finite [of p])
paulson@13871
    96
wenzelm@16974
    97
lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X"
paulson@13871
    98
  by (auto simp add: SetS_def MultInvPair_def)
paulson@13871
    99
nipkow@16663
   100
lemma SetS_elems_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
paulson@13871
   101
                        ~(QuadRes p a) |]  ==>
wenzelm@16974
   102
                        \<forall>X \<in> SetS a p. card X = 2"
paulson@13871
   103
  apply (auto simp add: SetS_def)
paulson@13871
   104
  apply (frule StandardRes_SRStar_prop1a)
paulson@13871
   105
  apply (rule MultInvPair_card_two, auto)
wenzelm@19670
   106
  done
paulson@13871
   107
wenzelm@16974
   108
lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
wenzelm@41541
   109
  by (auto simp add: SetS_finite SetS_elems_finite)
paulson@13871
   110
paulson@13871
   111
lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); 
wenzelm@16974
   112
    \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S"
berghofe@22274
   113
  by (induct set: finite) auto
paulson@13871
   114
wenzelm@41541
   115
lemma SetS_card:
wenzelm@41541
   116
  assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)"
wenzelm@41541
   117
  shows "int(card(SetS a p)) = (p - 1) div 2"
wenzelm@16974
   118
proof -
wenzelm@41541
   119
  have "(p - 1) = 2 * int(card(SetS a p))"
wenzelm@16974
   120
  proof -
wenzelm@16974
   121
    have "p - 1 = int(card(Union (SetS a p)))"
wenzelm@41541
   122
      by (auto simp add: assms MultInvPair_prop2 SRStar_card)
wenzelm@16974
   123
    also have "... = int (setsum card (SetS a p))"
wenzelm@41541
   124
      by (auto simp add: assms SetS_finite SetS_elems_finite
wenzelm@41541
   125
        MultInvPair_prop1c [of p a] card_Union_disjoint)
wenzelm@16974
   126
    also have "... = int(setsum (%x.2) (SetS a p))"
wenzelm@41541
   127
      using assms by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite
paulson@15047
   128
        card_setsum_aux simp del: setsum_constant)
wenzelm@16974
   129
    also have "... = 2 * int(card( SetS a p))"
wenzelm@41541
   130
      by (auto simp add: assms SetS_finite setsum_const2)
wenzelm@16974
   131
    finally show ?thesis .
wenzelm@16974
   132
  qed
wenzelm@41541
   133
  then show ?thesis by auto
wenzelm@16974
   134
qed
paulson@13871
   135
nipkow@16663
   136
lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
paulson@13871
   137
                              ~(QuadRes p a); x \<in> (SetS a p) |] ==> 
wenzelm@16974
   138
                          [\<Prod>x = a] (mod p)"
paulson@13871
   139
  apply (auto simp add: SetS_def MultInvPair_def)
paulson@13871
   140
  apply (frule StandardRes_SRStar_prop1a)
wenzelm@16974
   141
  apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)")
paulson@13871
   142
  apply (auto simp add: StandardRes_prop2 MultInvPair_distinct)
paulson@13871
   143
  apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in 
wenzelm@16974
   144
    StandardRes_prop4)
wenzelm@16974
   145
  apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)")
paulson@13871
   146
  apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and
paulson@13871
   147
                   b = "x * (a * MultInv p x)" and
wenzelm@16974
   148
                   c = "a * (x * MultInv p x)" in  zcong_trans, force)
paulson@13871
   149
  apply (frule_tac p = p and x = x in MultInv_prop2, auto)
paulson@25760
   150
apply (metis StandardRes_SRStar_prop3 mult_1_right mult_commute zcong_sym zcong_zmult_prop1)
huffman@44766
   151
  apply (auto simp add: mult_ac)
wenzelm@19670
   152
  done
paulson@13871
   153
wenzelm@16974
   154
lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
paulson@13871
   155
  by arith
paulson@13871
   156
wenzelm@16974
   157
lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)"
paulson@13871
   158
  by auto
paulson@13871
   159
krauss@35544
   160
lemma d22set_induct_old: "(\<And>a::int. 1 < a \<longrightarrow> P (a - 1) \<Longrightarrow> P a) \<Longrightarrow> P x"
krauss@35544
   161
using d22set.induct by blast
krauss@35544
   162
wenzelm@18369
   163
lemma SRStar_d22set_prop: "2 < p \<Longrightarrow> (SRStar p) = {1} \<union> (d22set (p - 1))"
krauss@35544
   164
  apply (induct p rule: d22set_induct_old)
wenzelm@18369
   165
  apply auto
nipkow@16733
   166
  apply (simp add: SRStar_def d22set.simps)
paulson@13871
   167
  apply (simp add: SRStar_def d22set.simps, clarify)
paulson@13871
   168
  apply (frule aux1)
paulson@13871
   169
  apply (frule aux2, auto)
paulson@13871
   170
  apply (simp_all add: SRStar_def)
paulson@13871
   171
  apply (simp add: d22set.simps)
paulson@13871
   172
  apply (frule d22set_le)
paulson@13871
   173
  apply (frule d22set_g_1, auto)
wenzelm@18369
   174
  done
paulson@13871
   175
wenzelm@41541
   176
lemma Union_SetS_setprod_prop1:
wenzelm@41541
   177
  assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
wenzelm@41541
   178
    "~(QuadRes p a)"
wenzelm@41541
   179
  shows "[\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
nipkow@15392
   180
proof -
wenzelm@41541
   181
  from assms have "[\<Prod>(Union (SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
paulson@13871
   182
    by (auto simp add: SetS_finite SetS_elems_finite
wenzelm@41541
   183
      MultInvPair_prop1c setprod_Union_disjoint)
nipkow@15392
   184
  also have "[setprod (setprod (%x. x)) (SetS a p) = 
nipkow@15392
   185
      setprod (%x. a) (SetS a p)] (mod p)"
wenzelm@18369
   186
    by (rule setprod_same_function_zcong)
wenzelm@41541
   187
      (auto simp add: assms SetS_setprod_prop SetS_finite)
nipkow@15392
   188
  also (zcong_trans) have "[setprod (%x. a) (SetS a p) = 
nipkow@15392
   189
      a^(card (SetS a p))] (mod p)"
wenzelm@41541
   190
    by (auto simp add: assms SetS_finite setprod_constant)
nipkow@15392
   191
  finally (zcong_trans) show ?thesis
paulson@13871
   192
    apply (rule zcong_trans)
nipkow@15392
   193
    apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)
nipkow@15392
   194
    apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force)
wenzelm@41541
   195
    apply (auto simp add: assms SetS_card)
wenzelm@18369
   196
    done
nipkow@15392
   197
qed
paulson@13871
   198
wenzelm@41541
   199
lemma Union_SetS_setprod_prop2:
wenzelm@41541
   200
  assumes "zprime p" and "2 < p" and "~([a = 0](mod p))"
wenzelm@41541
   201
  shows "\<Prod>(Union (SetS a p)) = zfact (p - 1)"
wenzelm@16974
   202
proof -
wenzelm@41541
   203
  from assms have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
paulson@13871
   204
    by (auto simp add: MultInvPair_prop2)
nipkow@15392
   205
  also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
wenzelm@41541
   206
    by (auto simp add: assms SRStar_d22set_prop)
nipkow@15392
   207
  also have "... = zfact(p - 1)"
nipkow@15392
   208
  proof -
wenzelm@18369
   209
    have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
paulson@25760
   210
      by (metis d22set_fin d22set_g_1 linorder_neq_iff)
wenzelm@18369
   211
    then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))"
wenzelm@18369
   212
      by auto
wenzelm@18369
   213
    then show ?thesis
wenzelm@18369
   214
      by (auto simp add: d22set_prod_zfact)
wenzelm@16974
   215
  qed
nipkow@15392
   216
  finally show ?thesis .
wenzelm@16974
   217
qed
paulson@13871
   218
nipkow@16663
   219
lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
wenzelm@16974
   220
                   [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)"
paulson@13871
   221
  apply (frule Union_SetS_setprod_prop1) 
paulson@13871
   222
  apply (auto simp add: Union_SetS_setprod_prop2)
wenzelm@18369
   223
  done
paulson@13871
   224
wenzelm@19670
   225
text {* \medskip Prove the first part of Euler's Criterion: *}
paulson@13871
   226
nipkow@16663
   227
lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
paulson@13871
   228
    ~(QuadRes p x) |] ==> 
wenzelm@16974
   229
      [x^(nat (((p) - 1) div 2)) = -1](mod p)"
huffman@45480
   230
  by (metis Wilson_Russ zcong_sym zcong_trans zfact_prop)
paulson@13871
   231
wenzelm@19670
   232
text {* \medskip Prove another part of Euler Criterion: *}
paulson@13871
   233
wenzelm@16974
   234
lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
wenzelm@16974
   235
proof -
wenzelm@16974
   236
  assume "0 < p"
wenzelm@16974
   237
  then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))"
paulson@13871
   238
    by (auto simp add: diff_add_assoc)
wenzelm@16974
   239
  also have "... = (a ^ 1) * a ^ (nat(p) - 1)"
huffman@44766
   240
    by (simp only: power_add)
wenzelm@16974
   241
  also have "... = a * a ^ (nat(p) - 1)"
paulson@13871
   242
    by auto
wenzelm@16974
   243
  finally show ?thesis .
wenzelm@16974
   244
qed
paulson@13871
   245
wenzelm@16974
   246
lemma aux_2: "[| (2::int) < p; p \<in> zOdd |] ==> 0 < ((p - 1) div 2)"
wenzelm@16974
   247
proof -
wenzelm@16974
   248
  assume "2 < p" and "p \<in> zOdd"
wenzelm@16974
   249
  then have "(p - 1):zEven"
paulson@13871
   250
    by (auto simp add: zEven_def zOdd_def)
wenzelm@16974
   251
  then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
paulson@13871
   252
    by (auto simp add: even_div_2_prop2)
wenzelm@23373
   253
  with `2 < p` have "1 < (p - 1)"
paulson@13871
   254
    by auto
wenzelm@16974
   255
  then have " 1 < (2 * ((p - 1) div 2))"
paulson@13871
   256
    by (auto simp add: aux_1)
wenzelm@16974
   257
  then have "0 < (2 * ((p - 1) div 2)) div 2"
paulson@13871
   258
    by auto
paulson@13871
   259
  then show ?thesis by auto
wenzelm@16974
   260
qed
paulson@13871
   261
wenzelm@19670
   262
lemma Euler_part2:
wenzelm@19670
   263
    "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)"
paulson@13871
   264
  apply (frule zprime_zOdd_eq_grt_2)
paulson@13871
   265
  apply (frule aux_2, auto)
paulson@13871
   266
  apply (frule_tac a = a in aux_1, auto)
paulson@13871
   267
  apply (frule zcong_zmult_prop1, auto)
wenzelm@18369
   268
  done
paulson@13871
   269
wenzelm@19670
   270
text {* \medskip Prove the final part of Euler's Criterion: *}
paulson@13871
   271
wenzelm@16974
   272
lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
nipkow@30042
   273
  by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
paulson@13871
   274
wenzelm@16974
   275
lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))"
paulson@13871
   276
  by (auto simp add: nat_mult_distrib)
paulson@13871
   277
nipkow@16663
   278
lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==> 
wenzelm@16974
   279
                      [x^(nat (((p) - 1) div 2)) = 1](mod p)"
paulson@13871
   280
  apply (subgoal_tac "p \<in> zOdd")
paulson@13871
   281
  apply (auto simp add: QuadRes_def)
paulson@25675
   282
   prefer 2 
huffman@45480
   283
   apply (metis zprime_zOdd_eq_grt_2)
paulson@13871
   284
  apply (frule aux__1, auto)
wenzelm@16974
   285
  apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower)
paulson@25675
   286
  apply (auto simp add: zpower_zpower) 
paulson@13871
   287
  apply (rule zcong_trans)
wenzelm@16974
   288
  apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
huffman@45480
   289
  apply (metis Little_Fermat even_div_2_prop2 odd_minus_one_even mult_1 aux__2)
wenzelm@18369
   290
  done
paulson@13871
   291
wenzelm@19670
   292
wenzelm@19670
   293
text {* \medskip Finally show Euler's Criterion: *}
paulson@13871
   294
nipkow@16663
   295
theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
wenzelm@16974
   296
    a^(nat (((p) - 1) div 2))] (mod p)"
paulson@13871
   297
  apply (auto simp add: Legendre_def Euler_part2)
wenzelm@20369
   298
  apply (frule Euler_part3, auto simp add: zcong_sym)[]
wenzelm@20369
   299
  apply (frule Euler_part1, auto simp add: zcong_sym)[]
wenzelm@18369
   300
  done
paulson@13871
   301
wenzelm@18369
   302
end