src/HOL/Old_Number_Theory/Euler.thy
changeset 32479 521cc9bf2958
parent 30042 31039ee583fa
child 35544 342a448ae141
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy	Tue Sep 01 15:39:33 2009 +0200
     1.3 @@ -0,0 +1,304 @@
     1.4 +(*  Title:      HOL/Quadratic_Reciprocity/Euler.thy
     1.5 +    ID:         $Id$
     1.6 +    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     1.7 +*)
     1.8 +
     1.9 +header {* Euler's criterion *}
    1.10 +
    1.11 +theory Euler imports Residues EvenOdd begin
    1.12 +
    1.13 +definition
    1.14 +  MultInvPair :: "int => int => int => int set" where
    1.15 +  "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
    1.16 +
    1.17 +definition
    1.18 +  SetS        :: "int => int => int set set" where
    1.19 +  "SetS        a p   =  (MultInvPair a p ` SRStar p)"
    1.20 +
    1.21 +
    1.22 +subsection {* Property for MultInvPair *}
    1.23 +
    1.24 +lemma MultInvPair_prop1a:
    1.25 +  "[| zprime p; 2 < p; ~([a = 0](mod p));
    1.26 +      X \<in> (SetS a p); Y \<in> (SetS a p);
    1.27 +      ~((X \<inter> Y) = {}) |] ==> X = Y"
    1.28 +  apply (auto simp add: SetS_def)
    1.29 +  apply (drule StandardRes_SRStar_prop1a)+ defer 1
    1.30 +  apply (drule StandardRes_SRStar_prop1a)+
    1.31 +  apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym)
    1.32 +  apply (drule notE, rule MultInv_zcong_prop1, auto)[]
    1.33 +  apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
    1.34 +  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
    1.35 +  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[]
    1.36 +  apply (drule MultInv_zcong_prop1, auto)[]
    1.37 +  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
    1.38 +  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
    1.39 +  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[]
    1.40 +  done
    1.41 +
    1.42 +lemma MultInvPair_prop1b:
    1.43 +  "[| zprime p; 2 < p; ~([a = 0](mod p));
    1.44 +      X \<in> (SetS a p); Y \<in> (SetS a p);
    1.45 +      X \<noteq> Y |] ==> X \<inter> Y = {}"
    1.46 +  apply (rule notnotD)
    1.47 +  apply (rule notI)
    1.48 +  apply (drule MultInvPair_prop1a, auto)
    1.49 +  done
    1.50 +
    1.51 +lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>  
    1.52 +    \<forall>X \<in> SetS a p. \<forall>Y \<in> SetS a p. X \<noteq> Y --> X\<inter>Y = {}"
    1.53 +  by (auto simp add: MultInvPair_prop1b)
    1.54 +
    1.55 +lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> 
    1.56 +                          Union ( SetS a p) = SRStar p"
    1.57 +  apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4 
    1.58 +    SRStar_mult_prop2)
    1.59 +  apply (frule StandardRes_SRStar_prop3)
    1.60 +  apply (rule bexI, auto)
    1.61 +  done
    1.62 +
    1.63 +lemma MultInvPair_distinct: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
    1.64 +                                ~([j = 0] (mod p)); 
    1.65 +                                ~(QuadRes p a) |]  ==> 
    1.66 +                             ~([j = a * MultInv p j] (mod p))"
    1.67 +proof
    1.68 +  assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and 
    1.69 +    "~([j = 0] (mod p))" and "~(QuadRes p a)"
    1.70 +  assume "[j = a * MultInv p j] (mod p)"
    1.71 +  then have "[j * j = (a * MultInv p j) * j] (mod p)"
    1.72 +    by (auto simp add: zcong_scalar)
    1.73 +  then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
    1.74 +    by (auto simp add: zmult_ac)
    1.75 +  have "[j * j = a] (mod p)"
    1.76 +    proof -
    1.77 +      from prems have b: "[MultInv p j * j = 1] (mod p)"
    1.78 +        by (simp add: MultInv_prop2a)
    1.79 +      from b a show ?thesis
    1.80 +        by (auto simp add: zcong_zmult_prop2)
    1.81 +    qed
    1.82 +  then have "[j^2 = a] (mod p)"
    1.83 +    by (metis  number_of_is_id power2_eq_square succ_bin_simps)
    1.84 +  with prems show False
    1.85 +    by (simp add: QuadRes_def)
    1.86 +qed
    1.87 +
    1.88 +lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
    1.89 +                                ~(QuadRes p a); ~([j = 0] (mod p)) |]  ==> 
    1.90 +                             card (MultInvPair a p j) = 2"
    1.91 +  apply (auto simp add: MultInvPair_def)
    1.92 +  apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))")
    1.93 +  apply auto
    1.94 +  apply (metis MultInvPair_distinct Pls_def StandardRes_def aux number_of_is_id one_is_num_one)
    1.95 +  done
    1.96 +
    1.97 +
    1.98 +subsection {* Properties of SetS *}
    1.99 +
   1.100 +lemma SetS_finite: "2 < p ==> finite (SetS a p)"
   1.101 +  by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI)
   1.102 +
   1.103 +lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X"
   1.104 +  by (auto simp add: SetS_def MultInvPair_def)
   1.105 +
   1.106 +lemma SetS_elems_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
   1.107 +                        ~(QuadRes p a) |]  ==>
   1.108 +                        \<forall>X \<in> SetS a p. card X = 2"
   1.109 +  apply (auto simp add: SetS_def)
   1.110 +  apply (frule StandardRes_SRStar_prop1a)
   1.111 +  apply (rule MultInvPair_card_two, auto)
   1.112 +  done
   1.113 +
   1.114 +lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
   1.115 +  by (auto simp add: SetS_finite SetS_elems_finite finite_Union)
   1.116 +
   1.117 +lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); 
   1.118 +    \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S"
   1.119 +  by (induct set: finite) auto
   1.120 +
   1.121 +lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> 
   1.122 +                  int(card(SetS a p)) = (p - 1) div 2"
   1.123 +proof -
   1.124 +  assume "zprime p" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)"
   1.125 +  then have "(p - 1) = 2 * int(card(SetS a p))"
   1.126 +  proof -
   1.127 +    have "p - 1 = int(card(Union (SetS a p)))"
   1.128 +      by (auto simp add: prems MultInvPair_prop2 SRStar_card)
   1.129 +    also have "... = int (setsum card (SetS a p))"
   1.130 +      by (auto simp add: prems SetS_finite SetS_elems_finite
   1.131 +                         MultInvPair_prop1c [of p a] card_Union_disjoint)
   1.132 +    also have "... = int(setsum (%x.2) (SetS a p))"
   1.133 +      using prems
   1.134 +      by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite 
   1.135 +        card_setsum_aux simp del: setsum_constant)
   1.136 +    also have "... = 2 * int(card( SetS a p))"
   1.137 +      by (auto simp add: prems SetS_finite setsum_const2)
   1.138 +    finally show ?thesis .
   1.139 +  qed
   1.140 +  from this show ?thesis
   1.141 +    by auto
   1.142 +qed
   1.143 +
   1.144 +lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
   1.145 +                              ~(QuadRes p a); x \<in> (SetS a p) |] ==> 
   1.146 +                          [\<Prod>x = a] (mod p)"
   1.147 +  apply (auto simp add: SetS_def MultInvPair_def)
   1.148 +  apply (frule StandardRes_SRStar_prop1a)
   1.149 +  apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)")
   1.150 +  apply (auto simp add: StandardRes_prop2 MultInvPair_distinct)
   1.151 +  apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in 
   1.152 +    StandardRes_prop4)
   1.153 +  apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)")
   1.154 +  apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and
   1.155 +                   b = "x * (a * MultInv p x)" and
   1.156 +                   c = "a * (x * MultInv p x)" in  zcong_trans, force)
   1.157 +  apply (frule_tac p = p and x = x in MultInv_prop2, auto)
   1.158 +apply (metis StandardRes_SRStar_prop3 mult_1_right mult_commute zcong_sym zcong_zmult_prop1)
   1.159 +  apply (auto simp add: zmult_ac)
   1.160 +  done
   1.161 +
   1.162 +lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
   1.163 +  by arith
   1.164 +
   1.165 +lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)"
   1.166 +  by auto
   1.167 +
   1.168 +lemma SRStar_d22set_prop: "2 < p \<Longrightarrow> (SRStar p) = {1} \<union> (d22set (p - 1))"
   1.169 +  apply (induct p rule: d22set.induct)
   1.170 +  apply auto
   1.171 +  apply (simp add: SRStar_def d22set.simps)
   1.172 +  apply (simp add: SRStar_def d22set.simps, clarify)
   1.173 +  apply (frule aux1)
   1.174 +  apply (frule aux2, auto)
   1.175 +  apply (simp_all add: SRStar_def)
   1.176 +  apply (simp add: d22set.simps)
   1.177 +  apply (frule d22set_le)
   1.178 +  apply (frule d22set_g_1, auto)
   1.179 +  done
   1.180 +
   1.181 +lemma Union_SetS_setprod_prop1: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
   1.182 +                                 [\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
   1.183 +proof -
   1.184 +  assume "zprime p" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)"
   1.185 +  then have "[\<Prod>(Union (SetS a p)) = 
   1.186 +      setprod (setprod (%x. x)) (SetS a p)] (mod p)"
   1.187 +    by (auto simp add: SetS_finite SetS_elems_finite
   1.188 +                       MultInvPair_prop1c setprod_Union_disjoint)
   1.189 +  also have "[setprod (setprod (%x. x)) (SetS a p) = 
   1.190 +      setprod (%x. a) (SetS a p)] (mod p)"
   1.191 +    by (rule setprod_same_function_zcong)
   1.192 +      (auto simp add: prems SetS_setprod_prop SetS_finite)
   1.193 +  also (zcong_trans) have "[setprod (%x. a) (SetS a p) = 
   1.194 +      a^(card (SetS a p))] (mod p)"
   1.195 +    by (auto simp add: prems SetS_finite setprod_constant)
   1.196 +  finally (zcong_trans) show ?thesis
   1.197 +    apply (rule zcong_trans)
   1.198 +    apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)
   1.199 +    apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force)
   1.200 +    apply (auto simp add: prems SetS_card)
   1.201 +    done
   1.202 +qed
   1.203 +
   1.204 +lemma Union_SetS_setprod_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> 
   1.205 +                                    \<Prod>(Union (SetS a p)) = zfact (p - 1)"
   1.206 +proof -
   1.207 +  assume "zprime p" and "2 < p" and "~([a = 0](mod p))"
   1.208 +  then have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
   1.209 +    by (auto simp add: MultInvPair_prop2)
   1.210 +  also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
   1.211 +    by (auto simp add: prems SRStar_d22set_prop)
   1.212 +  also have "... = zfact(p - 1)"
   1.213 +  proof -
   1.214 +    have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
   1.215 +      by (metis d22set_fin d22set_g_1 linorder_neq_iff)
   1.216 +    then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))"
   1.217 +      by auto
   1.218 +    then show ?thesis
   1.219 +      by (auto simp add: d22set_prod_zfact)
   1.220 +  qed
   1.221 +  finally show ?thesis .
   1.222 +qed
   1.223 +
   1.224 +lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
   1.225 +                   [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)"
   1.226 +  apply (frule Union_SetS_setprod_prop1) 
   1.227 +  apply (auto simp add: Union_SetS_setprod_prop2)
   1.228 +  done
   1.229 +
   1.230 +text {* \medskip Prove the first part of Euler's Criterion: *}
   1.231 +
   1.232 +lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
   1.233 +    ~(QuadRes p x) |] ==> 
   1.234 +      [x^(nat (((p) - 1) div 2)) = -1](mod p)"
   1.235 +  by (metis Wilson_Russ number_of_is_id zcong_sym zcong_trans zfact_prop)
   1.236 +
   1.237 +text {* \medskip Prove another part of Euler Criterion: *}
   1.238 +
   1.239 +lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
   1.240 +proof -
   1.241 +  assume "0 < p"
   1.242 +  then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))"
   1.243 +    by (auto simp add: diff_add_assoc)
   1.244 +  also have "... = (a ^ 1) * a ^ (nat(p) - 1)"
   1.245 +    by (simp only: zpower_zadd_distrib)
   1.246 +  also have "... = a * a ^ (nat(p) - 1)"
   1.247 +    by auto
   1.248 +  finally show ?thesis .
   1.249 +qed
   1.250 +
   1.251 +lemma aux_2: "[| (2::int) < p; p \<in> zOdd |] ==> 0 < ((p - 1) div 2)"
   1.252 +proof -
   1.253 +  assume "2 < p" and "p \<in> zOdd"
   1.254 +  then have "(p - 1):zEven"
   1.255 +    by (auto simp add: zEven_def zOdd_def)
   1.256 +  then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
   1.257 +    by (auto simp add: even_div_2_prop2)
   1.258 +  with `2 < p` have "1 < (p - 1)"
   1.259 +    by auto
   1.260 +  then have " 1 < (2 * ((p - 1) div 2))"
   1.261 +    by (auto simp add: aux_1)
   1.262 +  then have "0 < (2 * ((p - 1) div 2)) div 2"
   1.263 +    by auto
   1.264 +  then show ?thesis by auto
   1.265 +qed
   1.266 +
   1.267 +lemma Euler_part2:
   1.268 +    "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)"
   1.269 +  apply (frule zprime_zOdd_eq_grt_2)
   1.270 +  apply (frule aux_2, auto)
   1.271 +  apply (frule_tac a = a in aux_1, auto)
   1.272 +  apply (frule zcong_zmult_prop1, auto)
   1.273 +  done
   1.274 +
   1.275 +text {* \medskip Prove the final part of Euler's Criterion: *}
   1.276 +
   1.277 +lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
   1.278 +  by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
   1.279 +
   1.280 +lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))"
   1.281 +  by (auto simp add: nat_mult_distrib)
   1.282 +
   1.283 +lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==> 
   1.284 +                      [x^(nat (((p) - 1) div 2)) = 1](mod p)"
   1.285 +  apply (subgoal_tac "p \<in> zOdd")
   1.286 +  apply (auto simp add: QuadRes_def)
   1.287 +   prefer 2 
   1.288 +   apply (metis number_of_is_id numeral_1_eq_1 zprime_zOdd_eq_grt_2)
   1.289 +  apply (frule aux__1, auto)
   1.290 +  apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower)
   1.291 +  apply (auto simp add: zpower_zpower) 
   1.292 +  apply (rule zcong_trans)
   1.293 +  apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
   1.294 +  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)
   1.295 +  done
   1.296 +
   1.297 +
   1.298 +text {* \medskip Finally show Euler's Criterion: *}
   1.299 +
   1.300 +theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
   1.301 +    a^(nat (((p) - 1) div 2))] (mod p)"
   1.302 +  apply (auto simp add: Legendre_def Euler_part2)
   1.303 +  apply (frule Euler_part3, auto simp add: zcong_sym)[]
   1.304 +  apply (frule Euler_part1, auto simp add: zcong_sym)[]
   1.305 +  done
   1.306 +
   1.307 +end