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