src/HOL/NumberTheory/Euler.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 18369 694ea14ab4f2 child 19670 2e4a143c73c5 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
```     1 (*  Title:      HOL/Quadratic_Reciprocity/Euler.thy
```
```     2     ID:         \$Id\$
```
```     3     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
```
```     4 *)
```
```     5
```
```     6 header {* Euler's criterion *}
```
```     7
```
```     8 theory Euler imports Residues EvenOdd begin
```
```     9
```
```    10 constdefs
```
```    11   MultInvPair :: "int => int => int => int set"
```
```    12   "MultInvPair a p j == {StandardRes p j, StandardRes p (a * (MultInv p j))}"
```
```    13   SetS        :: "int => int => int set set"
```
```    14   "SetS        a p   ==  ((MultInvPair a p) ` (SRStar p))"
```
```    15
```
```    16 (****************************************************************)
```
```    17 (*                                                              *)
```
```    18 (* Property for MultInvPair                                     *)
```
```    19 (*                                                              *)
```
```    20 (****************************************************************)
```
```    21
```
```    22 lemma MultInvPair_prop1a: "[| zprime p; 2 < p; ~([a = 0](mod p));
```
```    23                               X \<in> (SetS a p); Y \<in> (SetS a p);
```
```    24                               ~((X \<inter> Y) = {}) |] ==>
```
```    25                            X = Y"
```
```    26   apply (auto simp add: SetS_def)
```
```    27   apply (drule StandardRes_SRStar_prop1a)+ defer 1
```
```    28   apply (drule StandardRes_SRStar_prop1a)+
```
```    29   apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym)
```
```    30   apply (drule notE, rule MultInv_zcong_prop1, auto)
```
```    31   apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym)
```
```    32   apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
```
```    33   apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
```
```    34   apply (drule MultInv_zcong_prop1, auto)
```
```    35   apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
```
```    36   apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
```
```    37   apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
```
```    38 done
```
```    39
```
```    40 lemma MultInvPair_prop1b: "[| zprime p; 2 < p; ~([a = 0](mod p));
```
```    41                               X \<in> (SetS a p); Y \<in> (SetS a p);
```
```    42                               X \<noteq> Y |] ==>
```
```    43                               X \<inter> Y = {}"
```
```    44   apply (rule notnotD)
```
```    45   apply (rule notI)
```
```    46   apply (drule MultInvPair_prop1a, auto)
```
```    47 done
```
```    48
```
```    49 lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>
```
```    50     \<forall>X \<in> SetS a p. \<forall>Y \<in> SetS a p. X \<noteq> Y --> X\<inter>Y = {}"
```
```    51   by (auto simp add: MultInvPair_prop1b)
```
```    52
```
```    53 lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>
```
```    54                           Union ( SetS a p) = SRStar p"
```
```    55   apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4
```
```    56     SRStar_mult_prop2)
```
```    57   apply (frule StandardRes_SRStar_prop3)
```
```    58   apply (rule bexI, auto)
```
```    59 done
```
```    60
```
```    61 lemma MultInvPair_distinct: "[| zprime p; 2 < p; ~([a = 0] (mod p));
```
```    62                                 ~([j = 0] (mod p));
```
```    63                                 ~(QuadRes p a) |]  ==>
```
```    64                              ~([j = a * MultInv p j] (mod p))"
```
```    65   apply auto
```
```    66 proof -
```
```    67   assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
```
```    68     "~([j = 0] (mod p))" and "~(QuadRes p a)"
```
```    69   assume "[j = a * MultInv p j] (mod p)"
```
```    70   then have "[j * j = (a * MultInv p j) * j] (mod p)"
```
```    71     by (auto simp add: zcong_scalar)
```
```    72   then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
```
```    73     by (auto simp add: zmult_ac)
```
```    74   have "[j * j = a] (mod p)"
```
```    75     proof -
```
```    76       from prems have b: "[MultInv p j * j = 1] (mod p)"
```
```    77         by (simp add: MultInv_prop2a)
```
```    78       from b a show ?thesis
```
```    79         by (auto simp add: zcong_zmult_prop2)
```
```    80     qed
```
```    81   then have "[j^2 = a] (mod p)"
```
```    82     apply(subgoal_tac "2 = Suc(Suc(0))")
```
```    83     apply (erule ssubst)
```
```    84     apply (auto simp only: power_Suc power_0)
```
```    85     by auto
```
```    86   with prems show False
```
```    87     by (simp add: QuadRes_def)
```
```    88 qed
```
```    89
```
```    90 lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p));
```
```    91                                 ~(QuadRes p a); ~([j = 0] (mod p)) |]  ==>
```
```    92                              card (MultInvPair a p j) = 2"
```
```    93   apply (auto simp add: MultInvPair_def)
```
```    94   apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))")
```
```    95   apply auto
```
```    96   apply (simp only: StandardRes_prop2)
```
```    97   apply (drule MultInvPair_distinct)
```
```    98 by auto
```
```    99
```
```   100 (****************************************************************)
```
```   101 (*                                                              *)
```
```   102 (* Properties of SetS                                           *)
```
```   103 (*                                                              *)
```
```   104 (****************************************************************)
```
```   105
```
```   106 lemma SetS_finite: "2 < p ==> finite (SetS a p)"
```
```   107   by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI)
```
```   108
```
```   109 lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X"
```
```   110   by (auto simp add: SetS_def MultInvPair_def)
```
```   111
```
```   112 lemma SetS_elems_card: "[| zprime p; 2 < p; ~([a = 0] (mod p));
```
```   113                         ~(QuadRes p a) |]  ==>
```
```   114                         \<forall>X \<in> SetS a p. card X = 2"
```
```   115   apply (auto simp add: SetS_def)
```
```   116   apply (frule StandardRes_SRStar_prop1a)
```
```   117   apply (rule MultInvPair_card_two, auto)
```
```   118 done
```
```   119
```
```   120 lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
```
```   121   by (auto simp add: SetS_finite SetS_elems_finite finite_Union)
```
```   122
```
```   123 lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set);
```
```   124     \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S"
```
```   125   by (induct set: Finites) auto
```
```   126
```
```   127 lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
```
```   128                   int(card(SetS a p)) = (p - 1) div 2"
```
```   129 proof -
```
```   130   assume "zprime p" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)"
```
```   131   then have "(p - 1) = 2 * int(card(SetS a p))"
```
```   132   proof -
```
```   133     have "p - 1 = int(card(Union (SetS a p)))"
```
```   134       by (auto simp add: prems MultInvPair_prop2 SRStar_card)
```
```   135     also have "... = int (setsum card (SetS a p))"
```
```   136       by (auto simp add: prems SetS_finite SetS_elems_finite
```
```   137                          MultInvPair_prop1c [of p a] card_Union_disjoint)
```
```   138     also have "... = int(setsum (%x.2) (SetS a p))"
```
```   139       apply (insert prems)
```
```   140       apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite
```
```   141         card_setsum_aux simp del: setsum_constant)
```
```   142     done
```
```   143     also have "... = 2 * int(card( SetS a p))"
```
```   144       by (auto simp add: prems SetS_finite setsum_const2)
```
```   145     finally show ?thesis .
```
```   146   qed
```
```   147   from this show ?thesis
```
```   148     by auto
```
```   149 qed
```
```   150
```
```   151 lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
```
```   152                               ~(QuadRes p a); x \<in> (SetS a p) |] ==>
```
```   153                           [\<Prod>x = a] (mod p)"
```
```   154   apply (auto simp add: SetS_def MultInvPair_def)
```
```   155   apply (frule StandardRes_SRStar_prop1a)
```
```   156   apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)")
```
```   157   apply (auto simp add: StandardRes_prop2 MultInvPair_distinct)
```
```   158   apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in
```
```   159     StandardRes_prop4)
```
```   160   apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)")
```
```   161   apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and
```
```   162                    b = "x * (a * MultInv p x)" and
```
```   163                    c = "a * (x * MultInv p x)" in  zcong_trans, force)
```
```   164   apply (frule_tac p = p and x = x in MultInv_prop2, auto)
```
```   165   apply (drule_tac a = "x * MultInv p x" and b = 1 in zcong_zmult_prop2)
```
```   166   apply (auto simp add: zmult_ac)
```
```   167 done
```
```   168
```
```   169 lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
```
```   170   by arith
```
```   171
```
```   172 lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)"
```
```   173   by auto
```
```   174
```
```   175 lemma SRStar_d22set_prop: "2 < p \<Longrightarrow> (SRStar p) = {1} \<union> (d22set (p - 1))"
```
```   176   apply (induct p rule: d22set.induct)
```
```   177   apply auto
```
```   178   apply (simp add: SRStar_def d22set.simps)
```
```   179   apply (simp add: SRStar_def d22set.simps, clarify)
```
```   180   apply (frule aux1)
```
```   181   apply (frule aux2, auto)
```
```   182   apply (simp_all add: SRStar_def)
```
```   183   apply (simp add: d22set.simps)
```
```   184   apply (frule d22set_le)
```
```   185   apply (frule d22set_g_1, auto)
```
```   186   done
```
```   187
```
```   188 lemma Union_SetS_setprod_prop1: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
```
```   189                                  [\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
```
```   190 proof -
```
```   191   assume "zprime p" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)"
```
```   192   then have "[\<Prod>(Union (SetS a p)) =
```
```   193       setprod (setprod (%x. x)) (SetS a p)] (mod p)"
```
```   194     by (auto simp add: SetS_finite SetS_elems_finite
```
```   195                        MultInvPair_prop1c setprod_Union_disjoint)
```
```   196   also have "[setprod (setprod (%x. x)) (SetS a p) =
```
```   197       setprod (%x. a) (SetS a p)] (mod p)"
```
```   198     by (rule setprod_same_function_zcong)
```
```   199       (auto simp add: prems SetS_setprod_prop SetS_finite)
```
```   200   also (zcong_trans) have "[setprod (%x. a) (SetS a p) =
```
```   201       a^(card (SetS a p))] (mod p)"
```
```   202     by (auto simp add: prems SetS_finite setprod_constant)
```
```   203   finally (zcong_trans) show ?thesis
```
```   204     apply (rule zcong_trans)
```
```   205     apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)
```
```   206     apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force)
```
```   207     apply (auto simp add: prems SetS_card)
```
```   208     done
```
```   209 qed
```
```   210
```
```   211 lemma Union_SetS_setprod_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>
```
```   212                                     \<Prod>(Union (SetS a p)) = zfact (p - 1)"
```
```   213 proof -
```
```   214   assume "zprime p" and "2 < p" and "~([a = 0](mod p))"
```
```   215   then have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
```
```   216     by (auto simp add: MultInvPair_prop2)
```
```   217   also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
```
```   218     by (auto simp add: prems SRStar_d22set_prop)
```
```   219   also have "... = zfact(p - 1)"
```
```   220   proof -
```
```   221     have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
```
```   222       apply (insert prems, auto)
```
```   223       apply (drule d22set_g_1)
```
```   224       apply (auto simp add: d22set_fin)
```
```   225       done
```
```   226     then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))"
```
```   227       by auto
```
```   228     then show ?thesis
```
```   229       by (auto simp add: d22set_prod_zfact)
```
```   230   qed
```
```   231   finally show ?thesis .
```
```   232 qed
```
```   233
```
```   234 lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
```
```   235                    [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)"
```
```   236   apply (frule Union_SetS_setprod_prop1)
```
```   237   apply (auto simp add: Union_SetS_setprod_prop2)
```
```   238   done
```
```   239
```
```   240 (****************************************************************)
```
```   241 (*                                                              *)
```
```   242 (*  Prove the first part of Euler's Criterion:                  *)
```
```   243 (*    ~(QuadRes p x) |] ==>                                     *)
```
```   244 (*                   [x^(nat (((p) - 1) div 2)) = -1](mod p)    *)
```
```   245 (*                                                              *)
```
```   246 (****************************************************************)
```
```   247
```
```   248 lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p));
```
```   249     ~(QuadRes p x) |] ==>
```
```   250       [x^(nat (((p) - 1) div 2)) = -1](mod p)"
```
```   251   apply (frule zfact_prop, auto)
```
```   252   apply (frule Wilson_Russ)
```
```   253   apply (auto simp add: zcong_sym)
```
```   254   apply (rule zcong_trans, auto)
```
```   255   done
```
```   256
```
```   257 (********************************************************************)
```
```   258 (*                                                                  *)
```
```   259 (* Prove another part of Euler Criterion:                           *)
```
```   260 (*        [a = 0] (mod p) ==> [0 = a ^ nat ((p - 1) div 2)] (mod p) *)
```
```   261 (*                                                                  *)
```
```   262 (********************************************************************)
```
```   263
```
```   264 lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
```
```   265 proof -
```
```   266   assume "0 < p"
```
```   267   then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))"
```
```   268     by (auto simp add: diff_add_assoc)
```
```   269   also have "... = (a ^ 1) * a ^ (nat(p) - 1)"
```
```   270     by (simp only: zpower_zadd_distrib)
```
```   271   also have "... = a * a ^ (nat(p) - 1)"
```
```   272     by auto
```
```   273   finally show ?thesis .
```
```   274 qed
```
```   275
```
```   276 lemma aux_2: "[| (2::int) < p; p \<in> zOdd |] ==> 0 < ((p - 1) div 2)"
```
```   277 proof -
```
```   278   assume "2 < p" and "p \<in> zOdd"
```
```   279   then have "(p - 1):zEven"
```
```   280     by (auto simp add: zEven_def zOdd_def)
```
```   281   then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
```
```   282     by (auto simp add: even_div_2_prop2)
```
```   283   then have "1 < (p - 1)"
```
```   284     by auto
```
```   285   then have " 1 < (2 * ((p - 1) div 2))"
```
```   286     by (auto simp add: aux_1)
```
```   287   then have "0 < (2 * ((p - 1) div 2)) div 2"
```
```   288     by auto
```
```   289   then show ?thesis by auto
```
```   290 qed
```
```   291
```
```   292 lemma Euler_part2: "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)"
```
```   293   apply (frule zprime_zOdd_eq_grt_2)
```
```   294   apply (frule aux_2, auto)
```
```   295   apply (frule_tac a = a in aux_1, auto)
```
```   296   apply (frule zcong_zmult_prop1, auto)
```
```   297   done
```
```   298
```
```   299 (****************************************************************)
```
```   300 (*                                                              *)
```
```   301 (* Prove the final part of Euler's Criterion:                   *)
```
```   302 (*           QuadRes p x |] ==>                                 *)
```
```   303 (*                      [x^(nat (((p) - 1) div 2)) = 1](mod p)  *)
```
```   304 (*                                                              *)
```
```   305 (****************************************************************)
```
```   306
```
```   307 lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
```
```   308   apply (subgoal_tac "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==>
```
```   309     ~([y ^ 2 = 0] (mod p))")
```
```   310   apply (auto simp add: zcong_sym [of "y^2" x p] intro: zcong_trans)
```
```   311   apply (auto simp add: zcong_eq_zdvd_prop intro: zpower_zdvd_prop1)
```
```   312   done
```
```   313
```
```   314 lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))"
```
```   315   by (auto simp add: nat_mult_distrib)
```
```   316
```
```   317 lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==>
```
```   318                       [x^(nat (((p) - 1) div 2)) = 1](mod p)"
```
```   319   apply (subgoal_tac "p \<in> zOdd")
```
```   320   apply (auto simp add: QuadRes_def)
```
```   321   apply (frule aux__1, auto)
```
```   322   apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower)
```
```   323   apply (auto simp add: zpower_zpower)
```
```   324   apply (rule zcong_trans)
```
```   325   apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
```
```   326   apply (simp add: aux__2)
```
```   327   apply (frule odd_minus_one_even)
```
```   328   apply (frule even_div_2_prop2)
```
```   329   apply (auto intro: Little_Fermat simp add: zprime_zOdd_eq_grt_2)
```
```   330   done
```
```   331
```
```   332 (********************************************************************)
```
```   333 (*                                                                  *)
```
```   334 (* Finally show Euler's Criterion                                   *)
```
```   335 (*                                                                  *)
```
```   336 (********************************************************************)
```
```   337
```
```   338 theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
```
```   339     a^(nat (((p) - 1) div 2))] (mod p)"
```
```   340   apply (auto simp add: Legendre_def Euler_part2)
```
```   341   apply (frule Euler_part3, auto simp add: zcong_sym)
```
```   342   apply (frule Euler_part1, auto simp add: zcong_sym)
```
```   343   done
```
```   344
```
```   345 end
```