src/HOL/NumberTheory/Euler.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 15047 fa62de5862b9
child 15392 290bc97038c7
permissions -rw-r--r--
import -> imports
     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 = Residues + EvenOdd:;
     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: "[| p \<in> zprime; 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)
    32   apply (drule MultInv_zcong_prop2, auto)
    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)
    36   apply (drule MultInv_zcong_prop2, auto)
    37   apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
    38 done
    39 
    40 lemma MultInvPair_prop1b: "[| p \<in> zprime; 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: "[| p \<in> zprime; 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: "[| p \<in> zprime; 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: "[| p \<in> zprime; 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 "p \<in> zprime" 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: "[| p \<in> zprime; 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: "[| p \<in> zprime; 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_finite_subsets)
   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: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> 
   128                   int(card(SetS a p)) = (p - 1) div 2";
   129 proof -;
   130   assume "p \<in> zprime" 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_sets)
   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: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p));
   152                               ~(QuadRes p a); x \<in> (SetS a p) |] ==> 
   153                           [setprod 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 [rule_format]: "2 < p --> (SRStar p) = {1} \<union> 
   176     (d22set (p - 1))";
   177   apply (induct p rule: d22set.induct, auto)
   178   apply (simp add: SRStar_def d22set.simps, arith)
   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: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
   189                                  [setprod (Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)";
   190 proof -;
   191   assume "p \<in> zprime" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)";
   192   then have "[setprod (Union (SetS a p)) = 
   193       gsetprod setprod (SetS a p)] (mod p)";
   194     by (auto simp add: SetS_finite SetS_elems_finite
   195                        MultInvPair_prop1c setprod_disj_sets)
   196   also; have "[gsetprod setprod (SetS a p) = 
   197       gsetprod (%x. a) (SetS a p)] (mod p)";
   198     apply (rule gsetprod_same_function_zcong)
   199     by (auto simp add: prems SetS_setprod_prop SetS_finite)
   200   also (zcong_trans) have "[gsetprod (%x. a) (SetS a p) = 
   201       a^(card (SetS a p))] (mod p)";
   202     by (auto simp add: prems SetS_finite gsetprod_const)
   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: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)) |] ==> 
   212                                     setprod (Union (SetS a p)) = zfact (p - 1)";
   213 proof -;
   214   assume "p \<in> zprime" and "2 < p" and "~([a = 0](mod p))";
   215   then have "setprod (Union (SetS a p)) = setprod (SRStar p)";
   216     by (auto simp add: MultInvPair_prop2)
   217   also have "... = setprod ({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 "setprod({1} \<union> (d22set (p - 1))) = setprod (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: "[| p \<in> zprime; 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; p \<in> zprime; ~([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; p \<in> zprime; [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; p \<in> zprime; ~([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; p \<in> zprime |] ==> [(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