Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
authorpaulson
Thu Mar 20 15:58:25 2003 +0100 (2003-03-20)
changeset 1387126e5f5e624f6
parent 13870 cf947d1ec5ff
child 13872 601514e63534
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
src/HOL/NumberTheory/Euler.thy
src/HOL/NumberTheory/EvenOdd.thy
src/HOL/NumberTheory/Finite2.thy
src/HOL/NumberTheory/Gauss.thy
src/HOL/NumberTheory/Int2.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
src/HOL/NumberTheory/ROOT.ML
src/HOL/NumberTheory/Residues.thy
src/HOL/NumberTheory/document/root.tex
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/NumberTheory/Euler.thy	Thu Mar 20 15:58:25 2003 +0100
     1.3 @@ -0,0 +1,345 @@
     1.4 +(*  Title:      HOL/Quadratic_Reciprocity/Euler.thy
     1.5 +    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     1.6 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.7 +*)
     1.8 +
     1.9 +header {* Euler's criterion *}
    1.10 +
    1.11 +theory Euler = Residues + EvenOdd:;
    1.12 +
    1.13 +constdefs
    1.14 +  MultInvPair :: "int => int => int => int set"
    1.15 +  "MultInvPair a p j == {StandardRes p j, StandardRes p (a * (MultInv p j))}"
    1.16 +  SetS        :: "int => int => int set set"
    1.17 +  "SetS        a p   ==  ((MultInvPair a p) ` (SRStar p))";
    1.18 +
    1.19 +(****************************************************************)
    1.20 +(*                                                              *)
    1.21 +(* Property for MultInvPair                                     *)
    1.22 +(*                                                              *)
    1.23 +(****************************************************************)
    1.24 +
    1.25 +lemma MultInvPair_prop1a: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p));
    1.26 +                              X \<in> (SetS a p); Y \<in> (SetS a p);
    1.27 +                              ~((X \<inter> Y) = {}) |] ==> 
    1.28 +                           X = Y";
    1.29 +  apply (auto simp add: SetS_def)
    1.30 +  apply (drule StandardRes_SRStar_prop1a)+; defer 1;
    1.31 +  apply (drule StandardRes_SRStar_prop1a)+;
    1.32 +  apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym)
    1.33 +  apply (drule notE, rule MultInv_zcong_prop1, auto)
    1.34 +  apply (drule notE, rule MultInv_zcong_prop2, auto)
    1.35 +  apply (drule MultInv_zcong_prop2, auto)
    1.36 +  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
    1.37 +  apply (drule MultInv_zcong_prop1, auto)
    1.38 +  apply (drule MultInv_zcong_prop2, auto)
    1.39 +  apply (drule MultInv_zcong_prop2, auto)
    1.40 +  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
    1.41 +done
    1.42 +
    1.43 +lemma MultInvPair_prop1b: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p));
    1.44 +                              X \<in> (SetS a p); Y \<in> (SetS a p);
    1.45 +                              X \<noteq> Y |] ==>
    1.46 +                              X \<inter> Y = {}";
    1.47 +  apply (rule notnotD)
    1.48 +  apply (rule notI)
    1.49 +  apply (drule MultInvPair_prop1a, auto)
    1.50 +done
    1.51 +
    1.52 +lemma MultInvPair_prop1c: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)) |] ==>  
    1.53 +    \<forall>X \<in> SetS a p. \<forall>Y \<in> SetS a p. X \<noteq> Y --> X\<inter>Y = {}"
    1.54 +  by (auto simp add: MultInvPair_prop1b)
    1.55 +
    1.56 +lemma MultInvPair_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)) |] ==> 
    1.57 +                          Union ( SetS a p) = SRStar p";
    1.58 +  apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4 
    1.59 +    SRStar_mult_prop2)
    1.60 +  apply (frule StandardRes_SRStar_prop3)
    1.61 +  apply (rule bexI, auto)
    1.62 +done
    1.63 +
    1.64 +lemma MultInvPair_distinct: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); 
    1.65 +                                ~([j = 0] (mod p)); 
    1.66 +                                ~(QuadRes p a) |]  ==> 
    1.67 +                             ~([j = a * MultInv p j] (mod p))";
    1.68 +  apply auto
    1.69 +proof -;
    1.70 +  assume "p \<in> zprime" and "2 < p" and "~([a = 0] (mod p))" and 
    1.71 +    "~([j = 0] (mod p))" and "~(QuadRes p a)";
    1.72 +  assume "[j = a * MultInv p j] (mod p)";
    1.73 +  then have "[j * j = (a * MultInv p j) * j] (mod p)";
    1.74 +    by (auto simp add: zcong_scalar)
    1.75 +  then have a:"[j * j = a * (MultInv p j * j)] (mod p)";
    1.76 +    by (auto simp add: zmult_ac)
    1.77 +  have "[j * j = a] (mod p)";
    1.78 +    proof -;
    1.79 +      from prems have b: "[MultInv p j * j = 1] (mod p)";
    1.80 +        by (simp add: MultInv_prop2a)
    1.81 +      from b a show ?thesis;
    1.82 +        by (auto simp add: zcong_zmult_prop2)
    1.83 +    qed;
    1.84 +  then have "[j^2 = a] (mod p)";
    1.85 +    apply(subgoal_tac "2 = Suc(Suc(0))");
    1.86 +    apply (erule ssubst)
    1.87 +    apply (auto simp only: power_Suc power_0)
    1.88 +    by auto
    1.89 +  with prems show False;
    1.90 +    by (simp add: QuadRes_def)
    1.91 +qed;
    1.92 +
    1.93 +lemma MultInvPair_card_two: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); 
    1.94 +                                ~(QuadRes p a); ~([j = 0] (mod p)) |]  ==> 
    1.95 +                             card (MultInvPair a p j) = 2";
    1.96 +  apply (auto simp add: MultInvPair_def)
    1.97 +  apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))");
    1.98 +  apply auto
    1.99 +  apply (simp only: StandardRes_prop2)
   1.100 +  apply (drule MultInvPair_distinct)
   1.101 +by auto
   1.102 +
   1.103 +(****************************************************************)
   1.104 +(*                                                              *)
   1.105 +(* Properties of SetS                                           *)
   1.106 +(*                                                              *)
   1.107 +(****************************************************************)
   1.108 +
   1.109 +lemma SetS_finite: "2 < p ==> finite (SetS a p)";
   1.110 +  by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI)
   1.111 +
   1.112 +lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X";
   1.113 +  by (auto simp add: SetS_def MultInvPair_def)
   1.114 +
   1.115 +lemma SetS_elems_card: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); 
   1.116 +                        ~(QuadRes p a) |]  ==>
   1.117 +                        \<forall>X \<in> SetS a p. card X = 2";
   1.118 +  apply (auto simp add: SetS_def)
   1.119 +  apply (frule StandardRes_SRStar_prop1a)
   1.120 +  apply (rule MultInvPair_card_two, auto)
   1.121 +done
   1.122 +
   1.123 +lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))";
   1.124 +  by (auto simp add: SetS_finite SetS_elems_finite finite_union_finite_subsets)
   1.125 +
   1.126 +lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); 
   1.127 +    \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S";
   1.128 +by (induct set: Finites, auto)
   1.129 +
   1.130 +lemma SetS_card: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> 
   1.131 +                  int(card(SetS a p)) = (p - 1) div 2";
   1.132 +proof -;
   1.133 +  assume "p \<in> zprime" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)";
   1.134 +  then have "(p - 1) = 2 * int(card(SetS a p))";
   1.135 +  proof -;
   1.136 +    have "p - 1 = int(card(Union (SetS a p)))";
   1.137 +      by (auto simp add: prems MultInvPair_prop2 SRStar_card)
   1.138 +    also have "... = int (setsum card (SetS a p))";
   1.139 +      by (auto simp add: prems SetS_finite SetS_elems_finite
   1.140 +                         MultInvPair_prop1c [of p a] card_union_disjoint_sets)
   1.141 +    also have "... = int(setsum (%x.2) (SetS a p))";
   1.142 +      apply (insert prems)
   1.143 +      apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite 
   1.144 +        card_setsum_aux)
   1.145 +    done
   1.146 +    also have "... = 2 * int(card( SetS a p))";
   1.147 +      by (auto simp add: prems SetS_finite setsum_const2)
   1.148 +    finally show ?thesis .;
   1.149 +  qed;
   1.150 +  from this show ?thesis;
   1.151 +    by auto
   1.152 +qed;
   1.153 +
   1.154 +lemma SetS_setprod_prop: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p));
   1.155 +                              ~(QuadRes p a); x \<in> (SetS a p) |] ==> 
   1.156 +                          [setprod x = a] (mod p)";
   1.157 +  apply (auto simp add: SetS_def MultInvPair_def)
   1.158 +  apply (frule StandardRes_SRStar_prop1a)
   1.159 +  apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)");
   1.160 +  apply (auto simp add: StandardRes_prop2 MultInvPair_distinct)
   1.161 +  apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in 
   1.162 +    StandardRes_prop4);
   1.163 +  apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)");
   1.164 +  apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and
   1.165 +                   b = "x * (a * MultInv p x)" and
   1.166 +                   c = "a * (x * MultInv p x)" in  zcong_trans, force);
   1.167 +  apply (frule_tac p = p and x = x in MultInv_prop2, auto)
   1.168 +  apply (drule_tac a = "x * MultInv p x" and b = 1 in zcong_zmult_prop2)
   1.169 +  apply (auto simp add: zmult_ac)
   1.170 +done
   1.171 +
   1.172 +lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1";
   1.173 +  by arith
   1.174 +
   1.175 +lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)";
   1.176 +  by auto
   1.177 +
   1.178 +lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} \<union> 
   1.179 +    (d22set (p - 1))";
   1.180 +  apply (induct p rule: d22set.induct, auto)
   1.181 +  apply (simp add: SRStar_def d22set.simps, arith)
   1.182 +  apply (simp add: SRStar_def d22set.simps, clarify)
   1.183 +  apply (frule aux1)
   1.184 +  apply (frule aux2, auto)
   1.185 +  apply (simp_all add: SRStar_def)
   1.186 +  apply (simp add: d22set.simps)
   1.187 +  apply (frule d22set_le)
   1.188 +  apply (frule d22set_g_1, auto)
   1.189 +done
   1.190 +
   1.191 +lemma Union_SetS_setprod_prop1: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
   1.192 +                                 [setprod (Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)";
   1.193 +proof -;
   1.194 +  assume "p \<in> zprime" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)";
   1.195 +  then have "[setprod (Union (SetS a p)) = 
   1.196 +      gsetprod setprod (SetS a p)] (mod p)";
   1.197 +    by (auto simp add: SetS_finite SetS_elems_finite
   1.198 +                       MultInvPair_prop1c setprod_disj_sets)
   1.199 +  also; have "[gsetprod setprod (SetS a p) = 
   1.200 +      gsetprod (%x. a) (SetS a p)] (mod p)";
   1.201 +    apply (rule gsetprod_same_function_zcong)
   1.202 +    by (auto simp add: prems SetS_setprod_prop SetS_finite)
   1.203 +  also (zcong_trans) have "[gsetprod (%x. a) (SetS a p) = 
   1.204 +      a^(card (SetS a p))] (mod p)";
   1.205 +    by (auto simp add: prems SetS_finite gsetprod_const)
   1.206 +  finally (zcong_trans) show ?thesis;
   1.207 +    apply (rule zcong_trans)
   1.208 +    apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto);
   1.209 +    apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force);
   1.210 +    apply (auto simp add: prems SetS_card)
   1.211 +  done
   1.212 +qed;
   1.213 +
   1.214 +lemma Union_SetS_setprod_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)) |] ==> 
   1.215 +                                    setprod (Union (SetS a p)) = zfact (p - 1)";
   1.216 +proof -;
   1.217 +  assume "p \<in> zprime" and "2 < p" and "~([a = 0](mod p))";
   1.218 +  then have "setprod (Union (SetS a p)) = setprod (SRStar p)";
   1.219 +    by (auto simp add: MultInvPair_prop2)
   1.220 +  also have "... = setprod ({1} \<union> (d22set (p - 1)))";
   1.221 +    by (auto simp add: prems SRStar_d22set_prop)
   1.222 +  also have "... = zfact(p - 1)";
   1.223 +  proof -;
   1.224 +     have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))";
   1.225 +      apply (insert prems, auto)
   1.226 +      apply (drule d22set_g_1)
   1.227 +      apply (auto simp add: d22set_fin)
   1.228 +     done
   1.229 +     then have "setprod({1} \<union> (d22set (p - 1))) = setprod (d22set (p - 1))";
   1.230 +       by auto
   1.231 +     then show ?thesis
   1.232 +       by (auto simp add: d22set_prod_zfact)
   1.233 +  qed;
   1.234 +  finally show ?thesis .;
   1.235 +qed;
   1.236 +
   1.237 +lemma zfact_prop: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
   1.238 +                   [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)";
   1.239 +  apply (frule Union_SetS_setprod_prop1) 
   1.240 +  apply (auto simp add: Union_SetS_setprod_prop2)
   1.241 +done
   1.242 +
   1.243 +(****************************************************************)
   1.244 +(*                                                              *)
   1.245 +(*  Prove the first part of Euler's Criterion:                  *)
   1.246 +(*    ~(QuadRes p x) |] ==>                                     *)
   1.247 +(*                   [x^(nat (((p) - 1) div 2)) = -1](mod p)    *)
   1.248 +(*                                                              *)
   1.249 +(****************************************************************)
   1.250 +
   1.251 +lemma Euler_part1: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)); 
   1.252 +    ~(QuadRes p x) |] ==> 
   1.253 +      [x^(nat (((p) - 1) div 2)) = -1](mod p)";
   1.254 +  apply (frule zfact_prop, auto)
   1.255 +  apply (frule Wilson_Russ)
   1.256 +  apply (auto simp add: zcong_sym)
   1.257 +  apply (rule zcong_trans, auto)
   1.258 +done
   1.259 +
   1.260 +(********************************************************************)
   1.261 +(*                                                                  *)
   1.262 +(* Prove another part of Euler Criterion:                           *)
   1.263 +(*        [a = 0] (mod p) ==> [0 = a ^ nat ((p - 1) div 2)] (mod p) *)
   1.264 +(*                                                                  *)
   1.265 +(********************************************************************)
   1.266 +
   1.267 +lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)";
   1.268 +proof -;
   1.269 +  assume "0 < p";
   1.270 +  then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))";
   1.271 +    by (auto simp add: diff_add_assoc)
   1.272 +  also have "... = (a ^ 1) * a ^ (nat(p) - 1)";
   1.273 +    by (simp only: zpower_zadd_distrib)
   1.274 +  also have "... = a * a ^ (nat(p) - 1)";
   1.275 +    by auto
   1.276 +  finally show ?thesis .;
   1.277 +qed;
   1.278 +
   1.279 +lemma aux_2: "[| (2::int) < p; p \<in> zOdd |] ==> 0 < ((p - 1) div 2)";
   1.280 +proof -;
   1.281 +  assume "2 < p" and "p \<in> zOdd";
   1.282 +  then have "(p - 1):zEven";
   1.283 +    by (auto simp add: zEven_def zOdd_def)
   1.284 +  then have aux_1: "2 * ((p - 1) div 2) = (p - 1)";
   1.285 +    by (auto simp add: even_div_2_prop2)
   1.286 +  then have "1 < (p - 1)"
   1.287 +    by auto
   1.288 +  then have " 1 < (2 * ((p - 1) div 2))";
   1.289 +    by (auto simp add: aux_1)
   1.290 +  then have "0 < (2 * ((p - 1) div 2)) div 2";
   1.291 +    by auto
   1.292 +  then show ?thesis by auto
   1.293 +qed;
   1.294 +
   1.295 +lemma Euler_part2: "[| 2 < p; p \<in> zprime; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)";
   1.296 +  apply (frule zprime_zOdd_eq_grt_2)
   1.297 +  apply (frule aux_2, auto)
   1.298 +  apply (frule_tac a = a in aux_1, auto)
   1.299 +  apply (frule zcong_zmult_prop1, auto)
   1.300 +done
   1.301 +
   1.302 +(****************************************************************)
   1.303 +(*                                                              *)
   1.304 +(* Prove the final part of Euler's Criterion:                   *)
   1.305 +(*           QuadRes p x |] ==>                                 *)
   1.306 +(*                      [x^(nat (((p) - 1) div 2)) = 1](mod p)  *)
   1.307 +(*                                                              *)
   1.308 +(****************************************************************)
   1.309 +
   1.310 +lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)";
   1.311 +  apply (subgoal_tac "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> 
   1.312 +    ~([y ^ 2 = 0] (mod p))");
   1.313 +  apply (auto simp add: zcong_sym [of "y^2" x p] intro: zcong_trans)
   1.314 +  apply (auto simp add: zcong_eq_zdvd_prop intro: zpower_zdvd_prop1)
   1.315 +done
   1.316 +
   1.317 +lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))";
   1.318 +  by (auto simp add: nat_mult_distrib)
   1.319 +
   1.320 +lemma Euler_part3: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)); QuadRes p x |] ==> 
   1.321 +                      [x^(nat (((p) - 1) div 2)) = 1](mod p)";
   1.322 +  apply (subgoal_tac "p \<in> zOdd")
   1.323 +  apply (auto simp add: QuadRes_def)
   1.324 +  apply (frule aux__1, auto)
   1.325 +  apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower);
   1.326 +  apply (auto simp add: zpower_zpower)
   1.327 +  apply (rule zcong_trans)
   1.328 +  apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"]);
   1.329 +  apply (simp add: aux__2)
   1.330 +  apply (frule odd_minus_one_even)
   1.331 +  apply (frule even_div_2_prop2)
   1.332 +  apply (auto intro: Little_Fermat simp add: zprime_zOdd_eq_grt_2)
   1.333 +done
   1.334 +
   1.335 +(********************************************************************)
   1.336 +(*                                                                  *)
   1.337 +(* Finally show Euler's Criterion                                   *)
   1.338 +(*                                                                  *)
   1.339 +(********************************************************************)
   1.340 +
   1.341 +theorem Euler_Criterion: "[| 2 < p; p \<in> zprime |] ==> [(Legendre a p) =
   1.342 +    a^(nat (((p) - 1) div 2))] (mod p)";
   1.343 +  apply (auto simp add: Legendre_def Euler_part2)
   1.344 +  apply (frule Euler_part3, auto simp add: zcong_sym)
   1.345 +  apply (frule Euler_part1, auto simp add: zcong_sym)
   1.346 +done
   1.347 +
   1.348 +end;
   1.349 \ No newline at end of file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/NumberTheory/EvenOdd.thy	Thu Mar 20 15:58:25 2003 +0100
     2.3 @@ -0,0 +1,254 @@
     2.4 +(*  Title:      HOL/Quadratic_Reciprocity/EvenOdd.thy
     2.5 +    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     2.6 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.7 +*)
     2.8 +
     2.9 +header {*Parity: Even and Odd Integers*}
    2.10 +
    2.11 +theory EvenOdd = Int2:;
    2.12 +
    2.13 +text{*Note.  This theory is being revised.  See the web page
    2.14 +\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
    2.15 +
    2.16 +constdefs
    2.17 +  zOdd    :: "int set"
    2.18 +  "zOdd == {x. \<exists>k. x = 2*k + 1}"
    2.19 +  zEven   :: "int set"
    2.20 +  "zEven == {x. \<exists>k. x = 2 * k}"
    2.21 +
    2.22 +(***********************************************************)
    2.23 +(*                                                         *)
    2.24 +(* Some useful properties about even and odd               *)
    2.25 +(*                                                         *)
    2.26 +(***********************************************************)
    2.27 +
    2.28 +lemma one_not_even: "~(1 \<in> zEven)";
    2.29 +  apply (simp add: zEven_def)
    2.30 +  apply (rule allI, case_tac "k \<le> 0", auto)
    2.31 +done
    2.32 +
    2.33 +lemma even_odd_conj: "~(x \<in> zOdd & x \<in> zEven)";
    2.34 +  apply (auto simp add: zOdd_def zEven_def)
    2.35 +  proof -;
    2.36 +    fix a b;
    2.37 +    assume "2 * (a::int) = 2 * (b::int) + 1"; 
    2.38 +    then have "2 * (a::int) - 2 * (b :: int) = 1";
    2.39 +       by arith
    2.40 +    then have "2 * (a - b) = 1";
    2.41 +       by (auto simp add: zdiff_zmult_distrib)
    2.42 +    moreover have "(2 * (a - b)):zEven";
    2.43 +       by (auto simp only: zEven_def)
    2.44 +    ultimately show "False";
    2.45 +       by (auto simp add: one_not_even)
    2.46 +  qed;
    2.47 +
    2.48 +lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)";
    2.49 +  apply (auto simp add: zOdd_def zEven_def)
    2.50 +  proof -;
    2.51 +    assume "\<forall>k. x \<noteq> 2 * k";
    2.52 +    have "0 \<le> (x mod 2) & (x mod 2) < 2";
    2.53 +      by (auto intro: pos_mod_sign pos_mod_bound)
    2.54 +    then have "x mod 2 = 0 | x mod 2 = 1" by arith
    2.55 +    moreover from prems have "x mod 2 \<noteq> 0" by auto
    2.56 +    ultimately have "x mod 2 = 1" by auto
    2.57 +    thus "\<exists>k. x = 2 * k + 1";
    2.58 +      by (insert zmod_zdiv_equality [of "x" "2"], auto)
    2.59 +  qed;
    2.60 +
    2.61 +lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven";
    2.62 +  by (insert even_odd_disj, auto)
    2.63 +
    2.64 +lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \<in> zOdd";
    2.65 +  apply (case_tac "x \<in> zOdd", auto)
    2.66 +  apply (drule not_odd_impl_even)
    2.67 +  apply (auto simp add: zEven_def zOdd_def)
    2.68 +  proof -;
    2.69 +    fix a b; 
    2.70 +    assume "2 * a * y = 2 * b + 1";
    2.71 +    then have "2 * a * y - 2 * b = 1";
    2.72 +      by arith
    2.73 +    then have "2 * (a * y - b) = 1";
    2.74 +      by (auto simp add: zdiff_zmult_distrib)
    2.75 +    moreover have "(2 * (a * y - b)):zEven";
    2.76 +       by (auto simp only: zEven_def)
    2.77 +    ultimately show "False";
    2.78 +       by (auto simp add: one_not_even)
    2.79 +  qed;
    2.80 +
    2.81 +lemma odd_minus_one_even: "x \<in> zOdd ==> (x - 1):zEven";
    2.82 +  by (auto simp add: zOdd_def zEven_def)
    2.83 +
    2.84 +lemma even_div_2_prop1: "x \<in> zEven ==> (x mod 2) = 0";
    2.85 +  by (auto simp add: zEven_def)
    2.86 +
    2.87 +lemma even_div_2_prop2: "x \<in> zEven ==> (2 * (x div 2)) = x";
    2.88 +  by (auto simp add: zEven_def)
    2.89 +
    2.90 +lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven";
    2.91 +  apply (auto simp add: zEven_def)
    2.92 +  by (auto simp only: zadd_zmult_distrib2 [THEN sym])
    2.93 +
    2.94 +lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven";
    2.95 +  by (auto simp add: zEven_def)
    2.96 +
    2.97 +lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven";
    2.98 +  apply (auto simp add: zEven_def)
    2.99 +  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
   2.100 +
   2.101 +lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven";
   2.102 +  apply (auto simp add: zOdd_def zEven_def)
   2.103 +  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
   2.104 +
   2.105 +lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd";
   2.106 +  apply (auto simp add: zOdd_def zEven_def)
   2.107 +  apply (rule_tac x = "k - ka - 1" in exI)
   2.108 +  by auto
   2.109 +
   2.110 +lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd";
   2.111 +  apply (auto simp add: zOdd_def zEven_def)
   2.112 +  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
   2.113 +
   2.114 +lemma odd_times_odd: "[| x \<in> zOdd;  y \<in> zOdd |] ==> x * y \<in> zOdd";
   2.115 +  apply (auto simp add: zOdd_def zadd_zmult_distrib zadd_zmult_distrib2)
   2.116 +  apply (rule_tac x = "2 * ka * k + ka + k" in exI)
   2.117 +  by (auto simp add: zadd_zmult_distrib)
   2.118 +
   2.119 +lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))";
   2.120 +  by (insert even_odd_conj even_odd_disj, auto)
   2.121 +
   2.122 +lemma even_product: "x * y \<in> zEven ==> x \<in> zEven | y \<in> zEven"; 
   2.123 +  by (insert odd_iff_not_even odd_times_odd, auto)
   2.124 +
   2.125 +lemma even_diff: "x - y \<in> zEven = ((x \<in> zEven) = (y \<in> zEven))";
   2.126 +  apply (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
   2.127 +     even_minus_odd odd_minus_even)
   2.128 +  proof -;
   2.129 +    assume "x - y \<in> zEven" and "x \<in> zEven";
   2.130 +    show "y \<in> zEven";
   2.131 +    proof (rule classical);
   2.132 +      assume "~(y \<in> zEven)"; 
   2.133 +      then have "y \<in> zOdd" 
   2.134 +        by (auto simp add: odd_iff_not_even)
   2.135 +      with prems have "x - y \<in> zOdd";
   2.136 +        by (simp add: even_minus_odd)
   2.137 +      with prems have "False"; 
   2.138 +        by (auto simp add: odd_iff_not_even)
   2.139 +      thus ?thesis;
   2.140 +        by auto
   2.141 +    qed;
   2.142 +    next assume "x - y \<in> zEven" and "y \<in> zEven"; 
   2.143 +    show "x \<in> zEven";
   2.144 +    proof (rule classical);
   2.145 +      assume "~(x \<in> zEven)"; 
   2.146 +      then have "x \<in> zOdd" 
   2.147 +        by (auto simp add: odd_iff_not_even)
   2.148 +      with prems have "x - y \<in> zOdd";
   2.149 +        by (simp add: odd_minus_even)
   2.150 +      with prems have "False"; 
   2.151 +        by (auto simp add: odd_iff_not_even)
   2.152 +      thus ?thesis;
   2.153 +        by auto
   2.154 +    qed;
   2.155 +  qed;
   2.156 +
   2.157 +lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1";
   2.158 +proof -;
   2.159 +  assume "x \<in> zEven" and "0 \<le> x";
   2.160 +  then have "\<exists>k. x = 2 * k";
   2.161 +    by (auto simp only: zEven_def)
   2.162 +  then show ?thesis;
   2.163 +    proof;
   2.164 +      fix a;
   2.165 +      assume "x = 2 * a";
   2.166 +      from prems have a: "0 \<le> a";
   2.167 +        by arith
   2.168 +      from prems have "nat x = nat(2 * a)";
   2.169 +        by auto
   2.170 +      also from a have "nat (2 * a) = 2 * nat a";
   2.171 +        by (auto simp add: nat_mult_distrib)
   2.172 +      finally have "(-1::int)^nat x = (-1)^(2 * nat a)";
   2.173 +        by auto
   2.174 +      also have "... = ((-1::int)^2)^ (nat a)";
   2.175 +        by (auto simp add: zpower_zpower [THEN sym])
   2.176 +      also have "(-1::int)^2 = 1";
   2.177 +        by auto
   2.178 +      finally; show ?thesis;
   2.179 +        by (auto simp add: zpower_1)
   2.180 +    qed;
   2.181 +qed;
   2.182 +
   2.183 +lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1";
   2.184 +proof -;
   2.185 +  assume "x \<in> zOdd" and "0 \<le> x";
   2.186 +  then have "\<exists>k. x = 2 * k + 1";
   2.187 +    by (auto simp only: zOdd_def)
   2.188 +  then show ?thesis;
   2.189 +    proof;
   2.190 +      fix a;
   2.191 +      assume "x = 2 * a + 1";
   2.192 +      from prems have a: "0 \<le> a";
   2.193 +        by arith
   2.194 +      from prems have "nat x = nat(2 * a + 1)";
   2.195 +        by auto
   2.196 +      also from a have "nat (2 * a + 1) = 2 * nat a + 1";
   2.197 +        by (auto simp add: nat_mult_distrib nat_add_distrib)
   2.198 +      finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)";
   2.199 +        by auto
   2.200 +      also have "... = ((-1::int)^2)^ (nat a) * (-1)^1";
   2.201 +        by (auto simp add: zpower_zpower [THEN sym] zpower_zadd_distrib)
   2.202 +      also have "(-1::int)^2 = 1";
   2.203 +        by auto
   2.204 +      finally; show ?thesis;
   2.205 +        by (auto simp add: zpower_1)
   2.206 +    qed;
   2.207 +qed;
   2.208 +
   2.209 +lemma neg_one_power_parity: "[| 0 \<le> x; 0 \<le> y; (x \<in> zEven) = (y \<in> zEven) |] ==> 
   2.210 +  (-1::int)^(nat x) = (-1::int)^(nat y)";
   2.211 +  apply (insert even_odd_disj [of x])
   2.212 +  apply (insert even_odd_disj [of y])
   2.213 +  by (auto simp add: neg_one_even_power neg_one_odd_power)
   2.214 +
   2.215 +lemma one_not_neg_one_mod_m: "2 < m ==> ~([1 = -1] (mod m))";
   2.216 +  by (auto simp add: zcong_def zdvd_not_zless)
   2.217 +
   2.218 +lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2";
   2.219 +  apply (auto simp only: zEven_def)
   2.220 +  proof -;
   2.221 +    fix k assume "x < 2 * k";
   2.222 +    then have "x div 2 < k" by (auto simp add: div_prop1)
   2.223 +    also have "k = (2 * k) div 2"; by auto
   2.224 +    finally show "x div 2 < 2 * k div 2" by auto
   2.225 +  qed;
   2.226 +
   2.227 +lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2";
   2.228 +  by (auto simp add: zEven_def, auto simp add: zdiv_zadd1_eq)
   2.229 +
   2.230 +lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y";
   2.231 +  by (auto simp add: zEven_def)
   2.232 +
   2.233 +(* An odd prime is greater than 2 *)
   2.234 +
   2.235 +lemma zprime_zOdd_eq_grt_2: "p \<in> zprime ==> (p \<in> zOdd) = (2 < p)";
   2.236 +  apply (auto simp add: zOdd_def zprime_def)
   2.237 +  apply (drule_tac x = 2 in allE)
   2.238 +  apply (insert odd_iff_not_even [of p])  
   2.239 +by (auto simp add: zOdd_def zEven_def)
   2.240 +
   2.241 +(* Powers of -1 and parity *)
   2.242 +
   2.243 +lemma neg_one_special: "finite A ==> 
   2.244 +    ((-1 :: int) ^ card A) * (-1 ^ card A) = 1";
   2.245 +  by (induct set: Finites, auto)
   2.246 +
   2.247 +lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1";
   2.248 +  apply (induct_tac n)
   2.249 +  by auto
   2.250 +
   2.251 +lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |]
   2.252 +  ==> ((-1::int)^j = (-1::int)^k)";
   2.253 +  apply (insert neg_one_power [of j])
   2.254 +  apply (insert neg_one_power [of k])
   2.255 +  by (auto simp add: one_not_neg_one_mod_m zcong_sym)
   2.256 +
   2.257 +end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/NumberTheory/Finite2.thy	Thu Mar 20 15:58:25 2003 +0100
     3.3 @@ -0,0 +1,425 @@
     3.4 +(*  Title:      HOL/Quadratic_Reciprocity/Finite2.thy
     3.5 +    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     3.6 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.7 +*)
     3.8 +
     3.9 +header {*Finite Sets and Finite Sums*}
    3.10 +
    3.11 +theory Finite2 = Main + IntFact:;
    3.12 +
    3.13 +text{*These are useful for combinatorial and number-theoretic counting
    3.14 +arguments.*}
    3.15 +
    3.16 +text{*Note.  This theory is being revised.  See the web page
    3.17 +\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
    3.18 +
    3.19 +(******************************************************************)
    3.20 +(*                                                                *)
    3.21 +(* gsetprod: A generalized set product function, for ints only.   *)
    3.22 +(* Note that "setprod", as defined in IntFact, is equivalent to   *)
    3.23 +(*   our "gsetprod id".                                           *) 
    3.24 +(*                                                                *)
    3.25 +(******************************************************************)
    3.26 +
    3.27 +consts
    3.28 +  gsetprod :: "('a => int) => 'a set => int"
    3.29 +
    3.30 +defs
    3.31 +  gsetprod_def: "gsetprod f A ==  if finite A then fold (op * o f) 1 A else 1";
    3.32 +
    3.33 +lemma gsetprod_empty [simp]: "gsetprod f {} = 1";
    3.34 +  by (auto simp add: gsetprod_def)
    3.35 +
    3.36 +lemma gsetprod_insert [simp]: "[| finite A; a \<notin> A |] ==> 
    3.37 +    gsetprod f (insert a A) = f a * gsetprod f A";
    3.38 +  by (simp add: gsetprod_def LC_def LC.fold_insert)
    3.39 +
    3.40 +(******************************************************************)
    3.41 +(*                                                                *)
    3.42 +(* Useful properties of sums and products                         *)
    3.43 +(*                                                                *)
    3.44 +(******************************************************************);
    3.45 +
    3.46 +subsection {* Useful properties of sums and products *}
    3.47 +
    3.48 +lemma setprod_gsetprod_id: "setprod A = gsetprod id A";
    3.49 +  by (auto simp add: setprod_def gsetprod_def)
    3.50 +
    3.51 +lemma setsum_same_function: "[| finite S; \<forall>x \<in> S. f x = g x |] ==> 
    3.52 +    setsum f S = setsum g S";
    3.53 +by (induct set: Finites, auto)
    3.54 +
    3.55 +lemma gsetprod_same_function: "[| finite S; \<forall>x \<in> S. f x = g x |] ==> 
    3.56 +  gsetprod f S = gsetprod g S";
    3.57 +by (induct set: Finites, auto)
    3.58 +
    3.59 +lemma setsum_same_function_zcong: 
    3.60 +   "[| finite S; \<forall>x \<in> S. [f x = g x](mod m) |] 
    3.61 +     ==> [setsum f S = setsum g S] (mod m)";
    3.62 +   by (induct set: Finites, auto simp add: zcong_zadd)
    3.63 +
    3.64 +lemma gsetprod_same_function_zcong: 
    3.65 +   "[| finite S; \<forall>x \<in> S. [f x = g x](mod m) |] 
    3.66 +     ==> [gsetprod f S = gsetprod g S] (mod m)";
    3.67 +by (induct set: Finites, auto simp add: zcong_zmult)
    3.68 +
    3.69 +lemma gsetprod_Un_Int: "finite A ==> finite B
    3.70 +    ==> gsetprod g (A \<union> B) * gsetprod g (A \<inter> B) = 
    3.71 +    gsetprod g A * gsetprod g B";
    3.72 +  apply (induct set: Finites)
    3.73 +by (auto simp add: Int_insert_left insert_absorb)
    3.74 +
    3.75 +lemma gsetprod_Un_disjoint: "[| finite A; finite B; A \<inter> B = {} |] ==> 
    3.76 +    gsetprod g (A \<union> B) = gsetprod g A * gsetprod g B";
    3.77 +  apply (subst gsetprod_Un_Int [symmetric])
    3.78 +by auto
    3.79 +
    3.80 +lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)";
    3.81 +  apply (induct set: Finites)
    3.82 +by (auto simp add: zadd_zmult_distrib2)
    3.83 +
    3.84 +lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = 
    3.85 +    int(c) * int(card X)";
    3.86 +  apply (induct set: Finites)
    3.87 +  apply (auto simp add: zadd_zmult_distrib2)
    3.88 +done
    3.89 +
    3.90 +lemma setsum_minus: "finite A ==> setsum (%x. ((f x)::int) - g x) A = 
    3.91 +  setsum f A - setsum g A";
    3.92 +  by (induct set: Finites, auto)
    3.93 +
    3.94 +lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = 
    3.95 +    c * setsum f A";
    3.96 +  apply (induct set: Finites, auto)
    3.97 +  by (auto simp only: zadd_zmult_distrib2) 
    3.98 +
    3.99 +lemma setsum_non_neg: "[| finite A; \<forall>x \<in> A. (0::int) \<le> f x |] ==>
   3.100 +    0 \<le>  setsum f A";
   3.101 +  by (induct set: Finites, auto)
   3.102 +
   3.103 +lemma gsetprod_const: "finite X ==> gsetprod (%x. (c :: int)) X = c ^ (card X)";
   3.104 +  apply (induct set: Finites)
   3.105 +by auto
   3.106 +
   3.107 +(******************************************************************)
   3.108 +(*                                                                *)
   3.109 +(* Cardinality of some explicit finite sets                       *)
   3.110 +(*                                                                *)
   3.111 +(******************************************************************);
   3.112 +
   3.113 +subsection {* Cardinality of explicit finite sets *}
   3.114 +
   3.115 +lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B";
   3.116 +by (simp add: finite_subset finite_imageI)
   3.117 +
   3.118 +lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}";
   3.119 +apply (rule_tac N = "{y. y < x}" and n = x in bounded_nat_set_is_finite)
   3.120 +by auto
   3.121 +
   3.122 +lemma bdd_nat_set_le_finite: "finite { y::nat . y \<le> x  }";
   3.123 +apply (subgoal_tac "{ y::nat . y \<le> x  } = { y::nat . y < Suc x}")
   3.124 +by (auto simp add: bdd_nat_set_l_finite)
   3.125 +
   3.126 +lemma  bdd_int_set_l_finite: "finite { x::int . 0 \<le> x & x < n}";
   3.127 +apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq> 
   3.128 +    int ` {(x :: nat). x < nat n}");
   3.129 +apply (erule finite_surjI)
   3.130 +apply (auto simp add: bdd_nat_set_l_finite image_def)
   3.131 +apply (rule_tac x = "nat x" in exI, simp) 
   3.132 +done
   3.133 +
   3.134 +lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}";
   3.135 +apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
   3.136 +apply (erule ssubst)
   3.137 +apply (rule bdd_int_set_l_finite)
   3.138 +by auto
   3.139 +
   3.140 +lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}";
   3.141 +apply (subgoal_tac "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}")
   3.142 +by (auto simp add: bdd_int_set_l_finite finite_subset)
   3.143 +
   3.144 +lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}";
   3.145 +apply (subgoal_tac "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}")
   3.146 +by (auto simp add: bdd_int_set_le_finite finite_subset)
   3.147 +
   3.148 +lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x";
   3.149 +apply (induct_tac x, force)
   3.150 +proof -;
   3.151 +  fix n::nat;
   3.152 +  assume "card {y. y < n} = n"; 
   3.153 +  have "{y. y < Suc n} = insert n {y. y < n}";
   3.154 +    by auto
   3.155 +  then have "card {y. y < Suc n} = card (insert n {y. y < n})";
   3.156 +    by auto
   3.157 +  also have "... = Suc (card {y. y < n})";
   3.158 +    apply (rule card_insert_disjoint)
   3.159 +    by (auto simp add: bdd_nat_set_l_finite)
   3.160 +  finally show "card {y. y < Suc n} = Suc n"; 
   3.161 +    by (simp add: prems)
   3.162 +qed;
   3.163 +
   3.164 +lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x";
   3.165 +apply (subgoal_tac "{ y::nat. y \<le> x} = { y::nat. y < Suc x}")
   3.166 +by (auto simp add: card_bdd_nat_set_l)
   3.167 +
   3.168 +lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n";
   3.169 +proof -;
   3.170 +  fix n::int;
   3.171 +  assume "0 \<le> n";
   3.172 +  have "finite {y. y < nat n}";
   3.173 +    by (rule bdd_nat_set_l_finite)
   3.174 +  moreover have "inj_on (%y. int y) {y. y < nat n}";
   3.175 +    by (auto simp add: inj_on_def)
   3.176 +  ultimately have "card (int ` {y. y < nat n}) = card {y. y < nat n}";
   3.177 +    by (rule card_image)
   3.178 +  also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}";
   3.179 +    apply (auto simp add: zless_nat_eq_int_zless image_def)
   3.180 +    apply (rule_tac x = "nat x" in exI)
   3.181 +    by (auto simp add: nat_0_le)
   3.182 +  also; have "card {y. y < nat n} = nat n" 
   3.183 +    by (rule card_bdd_nat_set_l)
   3.184 +  finally show "card {y. 0 \<le> y & y < n} = nat n"; .;
   3.185 +qed;
   3.186 +
   3.187 +lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} = 
   3.188 +  nat n + 1";
   3.189 +apply (subgoal_tac "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}")
   3.190 +apply (insert card_bdd_int_set_l [of "n+1"])
   3.191 +by (auto simp add: nat_add_distrib)
   3.192 +
   3.193 +lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==> 
   3.194 +    card {x. 0 < x & x \<le> n} = nat n";
   3.195 +proof -;
   3.196 +  fix n::int;
   3.197 +  assume "0 \<le> n";
   3.198 +  have "finite {x. 0 \<le> x & x < n}";
   3.199 +    by (rule bdd_int_set_l_finite)
   3.200 +  moreover have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}";
   3.201 +    by (auto simp add: inj_on_def)
   3.202 +  ultimately have "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) = 
   3.203 +     card {x. 0 \<le> x & x < n}";
   3.204 +    by (rule card_image)
   3.205 +  also from prems have "... = nat n";
   3.206 +    by (rule card_bdd_int_set_l)
   3.207 +  also; have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}";
   3.208 +    apply (auto simp add: image_def)
   3.209 +    apply (rule_tac x = "x - 1" in exI)
   3.210 +    by arith
   3.211 +  finally; show "card {x. 0 < x & x \<le> n} = nat n";.;
   3.212 +qed;
   3.213 +
   3.214 +lemma card_bdd_int_set_l_l: "0 < (n::int) ==> 
   3.215 +    card {x. 0 < x & x < n} = nat n - 1";
   3.216 +  apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}")
   3.217 +  apply (insert card_bdd_int_set_l_le [of "n - 1"])
   3.218 +  by (auto simp add: nat_diff_distrib)
   3.219 +
   3.220 +lemma int_card_bdd_int_set_l_l: "0 < n ==> 
   3.221 +    int(card {x. 0 < x & x < n}) = n - 1";
   3.222 +  apply (auto simp add: card_bdd_int_set_l_l)
   3.223 +  apply (subgoal_tac "Suc 0 \<le> nat n")
   3.224 +  apply (auto simp add: zdiff_int [THEN sym])
   3.225 +  apply (subgoal_tac "0 < nat n", arith)
   3.226 +  by (simp add: zero_less_nat_eq)
   3.227 +
   3.228 +lemma int_card_bdd_int_set_l_le: "0 \<le> n ==> 
   3.229 +    int(card {x. 0 < x & x \<le> n}) = n";
   3.230 +  by (auto simp add: card_bdd_int_set_l_le)
   3.231 +
   3.232 +(******************************************************************)
   3.233 +(*                                                                *)
   3.234 +(* Cartesian products of finite sets                              *)
   3.235 +(*                                                                *)
   3.236 +(******************************************************************)
   3.237 +
   3.238 +subsection {* Cardinality of finite cartesian products *}
   3.239 +
   3.240 +lemma insert_Sigma [simp]: "~(A = {}) ==>
   3.241 +  (insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)";
   3.242 +  by blast
   3.243 +
   3.244 +lemma cartesian_product_finite: "[| finite A; finite B |] ==> 
   3.245 +    finite (A <*> B)";
   3.246 +  apply (rule_tac F = A in finite_induct)
   3.247 +  by auto
   3.248 +
   3.249 +lemma cartesian_product_card_a [simp]: "finite A ==> 
   3.250 +    card({x} <*> A) = card(A)"; 
   3.251 +  apply (subgoal_tac "inj_on (%y .(x,y)) A");
   3.252 +  apply (frule card_image, assumption)
   3.253 +  apply (subgoal_tac "(Pair x ` A) = {x} <*> A");
   3.254 +  by (auto simp add: inj_on_def)
   3.255 +
   3.256 +lemma cartesian_product_card [simp]: "[| finite A; finite B |] ==> 
   3.257 +  card (A <*> B) = card(A) * card(B)";
   3.258 +  apply (rule_tac F = A in finite_induct, auto)
   3.259 +  apply (case_tac "F = {}", force)
   3.260 +  apply (subgoal_tac "card({x} <*> B \<union> F <*> B) = card({x} <*> B) + 
   3.261 +    card(F <*> B)");
   3.262 +  apply simp
   3.263 +  apply (rule card_Un_disjoint)
   3.264 +  by auto
   3.265 +
   3.266 +(******************************************************************)
   3.267 +(*                                                                *)
   3.268 +(* Sums and products over finite sets                             *)
   3.269 +(*                                                                *)
   3.270 +(******************************************************************)
   3.271 +
   3.272 +subsection {* Reindexing sums and products *}
   3.273 +
   3.274 +lemma sum_prop [rule_format]: "finite B ==>
   3.275 +                  inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B";
   3.276 +apply (rule finite_induct, assumption, force)
   3.277 +apply (rule impI, auto)
   3.278 +apply (simp add: inj_on_def)
   3.279 +apply (subgoal_tac "f x \<notin> f ` F")
   3.280 +apply (subgoal_tac "finite (f ` F)");
   3.281 +apply (auto simp add: setsum_insert)
   3.282 +by (simp add: inj_on_def) 
   3.283 +
   3.284 +lemma sum_prop_id: "finite B ==> inj_on f B ==> 
   3.285 +    setsum f B = setsum id (f ` B)";
   3.286 +by (auto simp add: sum_prop id_o)
   3.287 +
   3.288 +lemma prod_prop [rule_format]: "finite B ==>
   3.289 +        inj_on f B --> gsetprod h (f ` B) = gsetprod (h \<circ> f) B";
   3.290 +  apply (rule finite_induct, assumption, force)
   3.291 +  apply (rule impI)
   3.292 +  apply (auto simp add: inj_on_def)
   3.293 +  apply (subgoal_tac "f x \<notin> f ` F")
   3.294 +  apply (subgoal_tac "finite (f ` F)");
   3.295 +by (auto simp add: gsetprod_insert)
   3.296 +
   3.297 +lemma prod_prop_id: "[| finite B; inj_on f B |] ==> 
   3.298 +    gsetprod id (f ` B) = (gsetprod f B)";
   3.299 +  by (simp add: prod_prop id_o)
   3.300 +
   3.301 +subsection {* Lemmas for counting arguments *}
   3.302 +
   3.303 +lemma finite_union_finite_subsets: "[| finite A; \<forall>X \<in> A. finite X |] ==> 
   3.304 +    finite (Union A)";
   3.305 +apply (induct set: Finites)
   3.306 +by auto
   3.307 +
   3.308 +lemma finite_index_UNION_finite_sets: "finite A ==> 
   3.309 +    (\<forall>x \<in> A. finite (f x)) --> finite (UNION A f)";
   3.310 +by (induct_tac rule: finite_induct, auto)
   3.311 +
   3.312 +lemma card_union_disjoint_sets: "finite A ==> 
   3.313 +    ((\<forall>X \<in> A. finite X) & (\<forall>X \<in> A. \<forall>Y \<in> A. X \<noteq> Y --> X \<inter> Y = {})) ==> 
   3.314 +    card (Union A) = setsum card A";
   3.315 +  apply auto
   3.316 +  apply (induct set: Finites, auto)
   3.317 +  apply (frule_tac B = "Union F" and A = x in card_Un_Int)
   3.318 +by (auto simp add: finite_union_finite_subsets)
   3.319 +
   3.320 +(*
   3.321 +  We just duplicated something in the standard library: the next lemma 
   3.322 +  is setsum_UN_disjoint in Finite_Set
   3.323 +
   3.324 +lemma setsum_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
   3.325 +    ((\<forall>x \<in> A. finite (g x)) & 
   3.326 +    (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
   3.327 +      setsum f (UNION A g) = setsum (%x. setsum f (g x)) A";
   3.328 +apply (induct_tac rule: finite_induct)
   3.329 +apply (assumption, simp, clarify)
   3.330 +apply (subgoal_tac "g x \<inter> (UNION F g) = {}");
   3.331 +apply (subgoal_tac "finite (UNION F g)");
   3.332 +apply (simp add: setsum_Un_disjoint)
   3.333 +by (auto simp add: finite_index_UNION_finite_sets)
   3.334 +
   3.335 +*)
   3.336 +
   3.337 +lemma int_card_eq_setsum [rule_format]: "finite A ==> 
   3.338 +    int (card A) = setsum (%x. 1) A";
   3.339 +  by (erule finite_induct, auto)
   3.340 +
   3.341 +lemma card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
   3.342 +    ((\<forall>x \<in> A. finite (g x)) & 
   3.343 +    (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
   3.344 +      card (UNION A g) = setsum (%x. card (g x)) A";
   3.345 +apply clarify
   3.346 +apply (frule_tac f = "%x.(1::nat)" and A = g in 
   3.347 +    setsum_UN_disjoint);
   3.348 +apply assumption+;
   3.349 +apply (subgoal_tac "finite (UNION A g)");
   3.350 +apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
   3.351 +apply (auto simp only: card_eq_setsum)
   3.352 +apply (erule setsum_same_function)
   3.353 +by (auto simp add: card_eq_setsum)
   3.354 +
   3.355 +lemma int_card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
   3.356 +    ((\<forall>x \<in> A. finite (g x)) & 
   3.357 +    (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
   3.358 +       int(card (UNION A g)) = setsum (%x. int( card (g x))) A";
   3.359 +apply clarify
   3.360 +apply (frule_tac f = "%x.(1::int)" and A = g in 
   3.361 +    setsum_UN_disjoint);
   3.362 +apply assumption+;
   3.363 +apply (subgoal_tac "finite (UNION A g)");
   3.364 +apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
   3.365 +apply (auto simp only: int_card_eq_setsum)
   3.366 +apply (erule setsum_same_function)
   3.367 +by (auto simp add: int_card_eq_setsum)
   3.368 +
   3.369 +lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
   3.370 +    g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A";
   3.371 +apply (frule_tac h = g and f = f in sum_prop, auto)
   3.372 +apply (subgoal_tac "setsum g B = setsum g (f ` A)");
   3.373 +apply (simp add: inj_on_def)
   3.374 +apply (subgoal_tac "card A = card B")
   3.375 +apply (drule_tac A = "f ` A" and B = B in card_seteq)
   3.376 +apply (auto simp add: card_image)
   3.377 +apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
   3.378 +apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
   3.379 +by auto
   3.380 +
   3.381 +lemma gsetprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
   3.382 +    g ` B \<subseteq> A; inj_on g B |] ==> gsetprod g B = gsetprod (g \<circ> f) A";
   3.383 +  apply (frule_tac h = g and f = f in prod_prop, auto) 
   3.384 +  apply (subgoal_tac "gsetprod g B = gsetprod g (f ` A)"); 
   3.385 +  apply (simp add: inj_on_def)
   3.386 +  apply (subgoal_tac "card A = card B")
   3.387 +  apply (drule_tac A = "f ` A" and B = B in card_seteq)
   3.388 +  apply (auto simp add: card_image)
   3.389 +  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
   3.390 +by (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
   3.391 +
   3.392 +lemma setsum_union_disjoint_sets [rule_format]: "finite A ==> 
   3.393 +    ((\<forall>X \<in> A. finite X) & (\<forall>X \<in> A. \<forall>Y \<in> A. X \<noteq> Y --> X \<inter> Y = {})) 
   3.394 +    --> setsum f (Union A) = setsum (%x. setsum f x) A";
   3.395 +apply (induct_tac rule: finite_induct)
   3.396 +apply (assumption, simp, clarify)
   3.397 +apply (subgoal_tac "x \<inter> (Union F) = {}");
   3.398 +apply (subgoal_tac "finite (Union F)");
   3.399 +  by (auto simp add: setsum_Un_disjoint Union_def)
   3.400 +
   3.401 +lemma gsetprod_union_disjoint_sets [rule_format]: "[| 
   3.402 +    finite (A :: int set set); 
   3.403 +    (\<forall>X \<in> A. finite (X :: int set));
   3.404 +    (\<forall>X \<in> A. (\<forall>Y \<in> A. (X :: int set) \<noteq> (Y :: int set) --> 
   3.405 +      (X \<inter> Y) = {})) |] ==> 
   3.406 +  ( gsetprod (f :: int => int) (Union A) = gsetprod (%x. gsetprod f x) A)";
   3.407 +  apply (induct set: Finites)
   3.408 +  apply (auto simp add: gsetprod_empty) 
   3.409 +  apply (subgoal_tac "gsetprod f (x \<union> Union F) = 
   3.410 +    gsetprod f x * gsetprod f (Union F)");
   3.411 +  apply simp
   3.412 +  apply (rule gsetprod_Un_disjoint)
   3.413 +by (auto simp add: gsetprod_Un_disjoint Union_def)
   3.414 +
   3.415 +lemma gsetprod_disjoint_sets: "[| finite A;
   3.416 +    \<forall>X \<in> A. finite X; 
   3.417 +    \<forall>X \<in> A. \<forall>Y \<in> A. (X \<noteq> Y --> X \<inter> Y = {}) |] ==> 
   3.418 +  gsetprod id (Union A) = gsetprod (gsetprod id) A";
   3.419 +  apply (rule_tac f = id in gsetprod_union_disjoint_sets)
   3.420 +  by auto
   3.421 +
   3.422 +lemma setprod_disj_sets: "[| finite (A::int set set);
   3.423 +    \<forall>X \<in> A. finite X;
   3.424 +    \<forall>X \<in> A. \<forall>Y \<in> A. (X \<noteq> Y --> X \<inter> Y = {}) |] ==> 
   3.425 +  setprod (Union A) = gsetprod (%x. setprod x) A";
   3.426 +  by (auto simp add: setprod_gsetprod_id gsetprod_disjoint_sets)
   3.427 +
   3.428 +end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/NumberTheory/Gauss.thy	Thu Mar 20 15:58:25 2003 +0100
     4.3 @@ -0,0 +1,510 @@
     4.4 +(*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy
     4.5 +    Authors:    Jeremy Avigad, David Gray, and Adam Kramer)
     4.6 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4.7 +*)
     4.8 +
     4.9 +header {* Gauss' Lemma *}
    4.10 +
    4.11 +theory Gauss = Euler:;
    4.12 +
    4.13 +locale GAUSS =
    4.14 +  fixes p :: "int"
    4.15 +  fixes a :: "int"
    4.16 +  fixes A :: "int set"
    4.17 +  fixes B :: "int set"
    4.18 +  fixes C :: "int set"
    4.19 +  fixes D :: "int set"
    4.20 +  fixes E :: "int set"
    4.21 +  fixes F :: "int set"
    4.22 +
    4.23 +  assumes p_prime: "p \<in> zprime"
    4.24 +  assumes p_g_2: "2 < p"
    4.25 +  assumes p_a_relprime: "~[a = 0](mod p)"
    4.26 +  assumes a_nonzero:    "0 < a"
    4.27 +
    4.28 +  defines A_def: "A == {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
    4.29 +  defines B_def: "B == (%x. x * a) ` A"
    4.30 +  defines C_def: "C == (StandardRes p) ` B"
    4.31 +  defines D_def: "D == C \<inter> {x. x \<le> ((p - 1) div 2)}"
    4.32 +  defines E_def: "E == C \<inter> {x. ((p - 1) div 2) < x}"
    4.33 +  defines F_def: "F == (%x. (p - x)) ` E";
    4.34 +
    4.35 +subsection {* Basic properties of p *}
    4.36 +
    4.37 +lemma (in GAUSS) p_odd: "p \<in> zOdd";
    4.38 +  by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
    4.39 +
    4.40 +lemma (in GAUSS) p_g_0: "0 < p";
    4.41 +  by (insert p_g_2, auto)
    4.42 +
    4.43 +lemma (in GAUSS) int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2";
    4.44 +  by (insert p_g_2, auto simp add: pos_imp_zdiv_nonneg_iff)
    4.45 +
    4.46 +lemma (in GAUSS) p_minus_one_l: "(p - 1) div 2 < p";
    4.47 +  proof -;
    4.48 +    have "p - 1 = (p - 1) div 1" by auto
    4.49 +    then have "(p - 1) div 2 \<le> p - 1"
    4.50 +      apply (rule ssubst) back;
    4.51 +      apply (rule zdiv_mono2)
    4.52 +      by (auto simp add: p_g_0)
    4.53 +    then have "(p - 1) div 2 \<le> p - 1";
    4.54 +      by auto
    4.55 +    then show ?thesis by simp
    4.56 +qed;
    4.57 +
    4.58 +lemma (in GAUSS) p_eq: "p = (2 * (p - 1) div 2) + 1";
    4.59 +  apply (insert zdiv_zmult_self2 [of 2 "p - 1"])
    4.60 +by auto
    4.61 +
    4.62 +lemma zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)";
    4.63 +  apply (frule odd_minus_one_even)
    4.64 +  apply (simp add: zEven_def)
    4.65 +  apply (subgoal_tac "2 \<noteq> 0")
    4.66 +  apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2)  
    4.67 +by (auto simp add: even_div_2_prop2)
    4.68 +
    4.69 +lemma (in GAUSS) p_eq2: "p = (2 * ((p - 1) div 2)) + 1";
    4.70 +  apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto)
    4.71 +by (frule zodd_imp_zdiv_eq, auto)
    4.72 +
    4.73 +subsection {* Basic Properties of the Gauss Sets *}
    4.74 +
    4.75 +lemma (in GAUSS) finite_A: "finite (A)";
    4.76 +  apply (auto simp add: A_def) 
    4.77 +thm bdd_int_set_l_finite;
    4.78 +  apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}"); 
    4.79 +by (auto simp add: bdd_int_set_l_finite finite_subset)
    4.80 +
    4.81 +lemma (in GAUSS) finite_B: "finite (B)";
    4.82 +  by (auto simp add: B_def finite_A finite_imageI)
    4.83 +
    4.84 +lemma (in GAUSS) finite_C: "finite (C)";
    4.85 +  by (auto simp add: C_def finite_B finite_imageI)
    4.86 +
    4.87 +lemma (in GAUSS) finite_D: "finite (D)";
    4.88 +  by (auto simp add: D_def finite_Int finite_C)
    4.89 +
    4.90 +lemma (in GAUSS) finite_E: "finite (E)";
    4.91 +  by (auto simp add: E_def finite_Int finite_C)
    4.92 +
    4.93 +lemma (in GAUSS) finite_F: "finite (F)";
    4.94 +  by (auto simp add: F_def finite_E finite_imageI)
    4.95 +
    4.96 +lemma (in GAUSS) C_eq: "C = D \<union> E";
    4.97 +  by (auto simp add: C_def D_def E_def)
    4.98 +
    4.99 +lemma (in GAUSS) A_card_eq: "card A = nat ((p - 1) div 2)";
   4.100 +  apply (auto simp add: A_def) 
   4.101 +  apply (insert int_nat)
   4.102 +  apply (erule subst)
   4.103 +  by (auto simp add: card_bdd_int_set_l_le)
   4.104 +
   4.105 +lemma (in GAUSS) inj_on_xa_A: "inj_on (%x. x * a) A";
   4.106 +  apply (insert a_nonzero)
   4.107 +by (simp add: A_def inj_on_def)
   4.108 +
   4.109 +lemma (in GAUSS) A_res: "ResSet p A";
   4.110 +  apply (auto simp add: A_def ResSet_def) 
   4.111 +  apply (rule_tac m = p in zcong_less_eq) 
   4.112 +  apply (insert p_g_2, auto) 
   4.113 +  apply (subgoal_tac [1-2] "(p - 1) div 2 < p");
   4.114 +by (auto, auto simp add: p_minus_one_l)
   4.115 +
   4.116 +lemma (in GAUSS) B_res: "ResSet p B";
   4.117 +  apply (insert p_g_2 p_a_relprime p_minus_one_l)
   4.118 +  apply (auto simp add: B_def) 
   4.119 +  apply (rule ResSet_image)
   4.120 +  apply (auto simp add: A_res) 
   4.121 +  apply (auto simp add: A_def)
   4.122 +  proof -;
   4.123 +    fix x fix y
   4.124 +    assume a: "[x * a = y * a] (mod p)"
   4.125 +    assume b: "0 < x"
   4.126 +    assume c: "x \<le> (p - 1) div 2"
   4.127 +    assume d: "0 < y"
   4.128 +    assume e: "y \<le> (p - 1) div 2"
   4.129 +    from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] 
   4.130 +        have "[x = y](mod p)";
   4.131 +      by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) 
   4.132 +    with zcong_less_eq [of x y p] p_minus_one_l 
   4.133 +         order_le_less_trans [of x "(p - 1) div 2" p]
   4.134 +         order_le_less_trans [of y "(p - 1) div 2" p] show "x = y";
   4.135 +      by (simp add: prems p_minus_one_l p_g_0)
   4.136 +qed;
   4.137 +
   4.138 +lemma (in GAUSS) SR_B_inj: "inj_on (StandardRes p) B";
   4.139 +  apply (auto simp add: B_def StandardRes_def inj_on_def A_def prems)
   4.140 +  proof -;
   4.141 +    fix x fix y
   4.142 +    assume a: "x * a mod p = y * a mod p"
   4.143 +    assume b: "0 < x"
   4.144 +    assume c: "x \<le> (p - 1) div 2"
   4.145 +    assume d: "0 < y"
   4.146 +    assume e: "y \<le> (p - 1) div 2"
   4.147 +    assume f: "x \<noteq> y"
   4.148 +    from a have "[x * a = y * a](mod p)";
   4.149 +      by (simp add: zcong_zmod_eq p_g_0)
   4.150 +    with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] 
   4.151 +        have "[x = y](mod p)";
   4.152 +      by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) 
   4.153 +    with zcong_less_eq [of x y p] p_minus_one_l 
   4.154 +         order_le_less_trans [of x "(p - 1) div 2" p]
   4.155 +         order_le_less_trans [of y "(p - 1) div 2" p] have "x = y";
   4.156 +      by (simp add: prems p_minus_one_l p_g_0)
   4.157 +    then have False;
   4.158 +      by (simp add: f)
   4.159 +    then show "a = 0";
   4.160 +      by simp
   4.161 +qed;
   4.162 +
   4.163 +lemma (in GAUSS) inj_on_pminusx_E: "inj_on (%x. p - x) E";
   4.164 +  apply (auto simp add: E_def C_def B_def A_def)
   4.165 +  apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI);
   4.166 +by auto
   4.167 +
   4.168 +lemma (in GAUSS) A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)";
   4.169 +  apply (auto simp add: A_def)
   4.170 +  apply (frule_tac m = p in zcong_not_zero)
   4.171 +  apply (insert p_minus_one_l)
   4.172 +by auto
   4.173 +
   4.174 +lemma (in GAUSS) A_greater_zero: "x \<in> A ==> 0 < x";
   4.175 +  by (auto simp add: A_def)
   4.176 +
   4.177 +lemma (in GAUSS) B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)";
   4.178 +  apply (auto simp add: B_def)
   4.179 +  apply (frule A_ncong_p) 
   4.180 +  apply (insert p_a_relprime p_prime a_nonzero)
   4.181 +  apply (frule_tac a = x and b = a in zcong_zprime_prod_zero_contra)
   4.182 +by (auto simp add: A_greater_zero)
   4.183 +
   4.184 +lemma (in GAUSS) B_greater_zero: "x \<in> B ==> 0 < x";
   4.185 +  apply (insert a_nonzero)
   4.186 +by (auto simp add: B_def zmult_pos A_greater_zero)
   4.187 +
   4.188 +lemma (in GAUSS) C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)";
   4.189 +  apply (auto simp add: C_def)
   4.190 +  apply (frule B_ncong_p)
   4.191 +  apply (subgoal_tac "[x = StandardRes p x](mod p)");
   4.192 +  defer; apply (simp add: StandardRes_prop1)
   4.193 +  apply (frule_tac a = x and b = "StandardRes p x" and c = 0 in zcong_trans)
   4.194 +by auto
   4.195 +
   4.196 +lemma (in GAUSS) C_greater_zero: "y \<in> C ==> 0 < y";
   4.197 +  apply (auto simp add: C_def)
   4.198 +  proof -;
   4.199 +    fix x;
   4.200 +    assume a: "x \<in> B";
   4.201 +    from p_g_0 have "0 \<le> StandardRes p x";
   4.202 +      by (simp add: StandardRes_lbound)
   4.203 +    moreover have "~[x = 0] (mod p)";
   4.204 +      by (simp add: a B_ncong_p)
   4.205 +    then have "StandardRes p x \<noteq> 0";
   4.206 +      by (simp add: StandardRes_prop3)
   4.207 +    ultimately show "0 < StandardRes p x";
   4.208 +      by (simp add: order_le_less)
   4.209 +qed;
   4.210 +
   4.211 +lemma (in GAUSS) D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)";
   4.212 +  by (auto simp add: D_def C_ncong_p)
   4.213 +
   4.214 +lemma (in GAUSS) E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)";
   4.215 +  by (auto simp add: E_def C_ncong_p)
   4.216 +
   4.217 +lemma (in GAUSS) F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)";
   4.218 +  apply (auto simp add: F_def) 
   4.219 +  proof -;
   4.220 +    fix x assume a: "x \<in> E" assume b: "[p - x = 0] (mod p)"
   4.221 +    from E_ncong_p have "~[x = 0] (mod p)";
   4.222 +      by (simp add: a)
   4.223 +    moreover from a have "0 < x";
   4.224 +      by (simp add: a E_def C_greater_zero)
   4.225 +    moreover from a have "x < p";
   4.226 +      by (auto simp add: E_def C_def p_g_0 StandardRes_ubound)
   4.227 +    ultimately have "~[p - x = 0] (mod p)";
   4.228 +      by (simp add: zcong_not_zero)
   4.229 +    from this show False by (simp add: b)
   4.230 +qed;
   4.231 +
   4.232 +lemma (in GAUSS) F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}";
   4.233 +  apply (auto simp add: F_def E_def) 
   4.234 +  apply (insert p_g_0)
   4.235 +  apply (frule_tac x = xa in StandardRes_ubound)
   4.236 +  apply (frule_tac x = x in StandardRes_ubound)
   4.237 +  apply (subgoal_tac "xa = StandardRes p xa")
   4.238 +  apply (auto simp add: C_def StandardRes_prop2 StandardRes_prop1)
   4.239 +  proof -;
   4.240 +    from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have 
   4.241 +        "2 * (p - 1) div 2 = 2 * ((p - 1) div 2)";
   4.242 +      by simp
   4.243 +    with p_eq2 show " !!x. [| (p - 1) div 2 < StandardRes p x; x \<in> B |]
   4.244 +         ==> p - StandardRes p x \<le> (p - 1) div 2";
   4.245 +      by simp
   4.246 +qed;
   4.247 +
   4.248 +lemma (in GAUSS) D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}";
   4.249 +  by (auto simp add: D_def C_greater_zero)
   4.250 +
   4.251 +lemma (in GAUSS) F_eq: "F = {x. \<exists>y \<in> A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}";
   4.252 +  by (auto simp add: F_def E_def D_def C_def B_def A_def)
   4.253 +
   4.254 +lemma (in GAUSS) D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p - 1) div 2)}";
   4.255 +  by (auto simp add: D_def C_def B_def A_def)
   4.256 +
   4.257 +lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2";
   4.258 +  by (auto simp add: D_eq)
   4.259 +
   4.260 +lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2";
   4.261 +  apply (auto simp add: F_eq A_def)
   4.262 +  proof -;
   4.263 +    fix y;
   4.264 +    assume "(p - 1) div 2 < StandardRes p (y * a)";
   4.265 +    then have "p - StandardRes p (y * a) < p - ((p - 1) div 2)";
   4.266 +      by arith
   4.267 +    also from p_eq2 have "... = 2 * ((p - 1) div 2) + 1 - ((p - 1) div 2)"; 
   4.268 +      by (rule subst, auto)
   4.269 +    also; have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1";
   4.270 +      by arith
   4.271 +    finally show "p - StandardRes p (y * a) \<le> (p - 1) div 2";
   4.272 +      by (insert zless_add1_eq [of "p - StandardRes p (y * a)" 
   4.273 +          "(p - 1) div 2"],auto);
   4.274 +qed;
   4.275 +
   4.276 +lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x,p) = 1";
   4.277 +  apply (insert p_prime p_minus_one_l)
   4.278 +by (auto simp add: A_def zless_zprime_imp_zrelprime)
   4.279 +
   4.280 +lemma (in GAUSS) A_prod_relprime: "zgcd((gsetprod id A),p) = 1";
   4.281 +  by (insert all_A_relprime finite_A, simp add: all_relprime_prod_relprime)
   4.282 +
   4.283 +subsection {* Relationships Between Gauss Sets *}
   4.284 +
   4.285 +lemma (in GAUSS) B_card_eq_A: "card B = card A";
   4.286 +  apply (insert finite_A)
   4.287 +by (simp add: finite_A B_def inj_on_xa_A card_image)
   4.288 +
   4.289 +lemma (in GAUSS) B_card_eq: "card B = nat ((p - 1) div 2)";
   4.290 +  by (auto simp add: B_card_eq_A A_card_eq)
   4.291 +
   4.292 +lemma (in GAUSS) F_card_eq_E: "card F = card E";
   4.293 +  apply (insert finite_E)
   4.294 +by (simp add: F_def inj_on_pminusx_E card_image)
   4.295 +
   4.296 +lemma (in GAUSS) C_card_eq_B: "card C = card B";
   4.297 +  apply (insert finite_B)
   4.298 +  apply (subgoal_tac "inj_on (StandardRes p) B");
   4.299 +  apply (simp add: B_def C_def card_image)
   4.300 +  apply (rule StandardRes_inj_on_ResSet)
   4.301 +by (simp add: B_res)
   4.302 +
   4.303 +lemma (in GAUSS) D_E_disj: "D \<inter> E = {}";
   4.304 +  by (auto simp add: D_def E_def)
   4.305 +
   4.306 +lemma (in GAUSS) C_card_eq_D_plus_E: "card C = card D + card E";
   4.307 +  by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
   4.308 +
   4.309 +lemma (in GAUSS) C_prod_eq_D_times_E: "gsetprod id E * gsetprod id D = gsetprod id C";
   4.310 +  apply (insert D_E_disj finite_D finite_E C_eq)
   4.311 +  apply (frule gsetprod_Un_disjoint [of D E id])
   4.312 +by auto
   4.313 +
   4.314 +lemma (in GAUSS) C_B_zcong_prod: "[gsetprod id C = gsetprod id B] (mod p)";
   4.315 +thm gsetprod_same_function_zcong;  
   4.316 +  apply (auto simp add: C_def)
   4.317 +  apply (insert finite_B SR_B_inj) 
   4.318 +  apply (frule_tac f = "StandardRes p" in prod_prop_id, auto) 
   4.319 +  apply (rule gsetprod_same_function_zcong)
   4.320 +by (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
   4.321 +
   4.322 +lemma (in GAUSS) F_Un_D_subset: "(F \<union> D) \<subseteq> A";
   4.323 +  apply (rule Un_least)
   4.324 +by (auto simp add: A_def F_subset D_subset)
   4.325 +
   4.326 +lemma two_eq: "2 * (x::int) = x + x";
   4.327 +  by arith
   4.328 +
   4.329 +lemma (in GAUSS) F_D_disj: "(F \<inter> D) = {}";
   4.330 +  apply (simp add: F_eq D_eq)
   4.331 +  apply (auto simp add: F_eq D_eq)
   4.332 +  proof -;
   4.333 +    fix y; fix ya;
   4.334 +    assume "p - StandardRes p (y * a) = StandardRes p (ya * a)";
   4.335 +    then have "p = StandardRes p (y * a) + StandardRes p (ya * a)";
   4.336 +      by arith
   4.337 +    moreover have "p dvd p";
   4.338 +      by auto
   4.339 +    ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))";
   4.340 +      by auto
   4.341 +    then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)";
   4.342 +      by (auto simp add: zcong_def)
   4.343 +    have "[y * a = StandardRes p (y * a)] (mod p)";
   4.344 +      by (simp only: zcong_sym StandardRes_prop1)
   4.345 +    moreover have "[ya * a = StandardRes p (ya * a)] (mod p)";
   4.346 +      by (simp only: zcong_sym StandardRes_prop1)
   4.347 +    ultimately have "[y * a + ya * a = 
   4.348 +        StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)";
   4.349 +      by (rule zcong_zadd)
   4.350 +    with a have "[y * a + ya * a = 0] (mod p)";
   4.351 +      apply (elim zcong_trans)
   4.352 +      by (simp only: zcong_refl)
   4.353 +    also have "y * a + ya * a = a * (y + ya)";
   4.354 +      by (simp add: zadd_zmult_distrib2 zmult_commute)
   4.355 +    finally have "[a * (y + ya) = 0] (mod p)";.;
   4.356 +    with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
   4.357 +        p_a_relprime
   4.358 +        have a: "[y + ya = 0] (mod p)";
   4.359 +      by auto
   4.360 +    assume b: "y \<in> A" and c: "ya: A";
   4.361 +    with A_def have "0 < y + ya";
   4.362 +      by auto
   4.363 +    moreover from b c A_def have "y + ya \<le> (p - 1) div 2 + (p - 1) div 2";
   4.364 +      by auto 
   4.365 +    moreover from b c p_eq2 A_def have "y + ya < p";
   4.366 +      by auto
   4.367 +    ultimately show False;
   4.368 +      apply simp
   4.369 +      apply (frule_tac m = p in zcong_not_zero)
   4.370 +      by (auto simp add: a)
   4.371 +qed;
   4.372 +
   4.373 +lemma (in GAUSS) F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)";
   4.374 +  apply (insert F_D_disj finite_F finite_D)
   4.375 +  proof -;
   4.376 +    have "card (F \<union> D) = card E + card D";
   4.377 +      by (auto simp add: finite_F finite_D F_D_disj 
   4.378 +                         card_Un_disjoint F_card_eq_E)
   4.379 +    then have "card (F \<union> D) = card C";
   4.380 +      by (simp add: C_card_eq_D_plus_E)
   4.381 +    from this show "card (F \<union> D) = nat ((p - 1) div 2)"; 
   4.382 +      by (simp add: C_card_eq_B B_card_eq)
   4.383 +qed;
   4.384 +
   4.385 +lemma (in GAUSS) F_Un_D_eq_A: "F \<union> D = A";
   4.386 +  apply (insert finite_A F_Un_D_subset A_card_eq F_Un_D_card) 
   4.387 +by (auto simp add: card_seteq)
   4.388 +
   4.389 +lemma (in GAUSS) prod_D_F_eq_prod_A: 
   4.390 +    "(gsetprod id D) * (gsetprod id F) = gsetprod id A";
   4.391 +  apply (insert F_D_disj finite_D finite_F)
   4.392 +  apply (frule gsetprod_Un_disjoint [of F D id])
   4.393 +by (auto simp add: F_Un_D_eq_A)
   4.394 +
   4.395 +lemma (in GAUSS) prod_F_zcong:
   4.396 +    "[gsetprod id F = ((-1) ^ (card E)) * (gsetprod id E)] (mod p)";
   4.397 +  proof -;
   4.398 +    have "gsetprod id F = gsetprod id (op - p ` E)";
   4.399 +      by (auto simp add: F_def)
   4.400 +    then have "gsetprod id F = gsetprod (op - p) E";
   4.401 +      apply simp
   4.402 +      apply (insert finite_E inj_on_pminusx_E)
   4.403 +      by (frule_tac f = "op - p" in prod_prop_id, auto)
   4.404 +    then have one: 
   4.405 +      "[gsetprod id F = gsetprod (StandardRes p o (op - p)) E] (mod p)";
   4.406 +      apply simp
   4.407 +      apply (insert p_g_0 finite_E)
   4.408 +      by (auto simp add: StandardRes_prod)
   4.409 +    moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)";
   4.410 +      apply clarify
   4.411 +      apply (insert zcong_id [of p])
   4.412 +      by (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
   4.413 +    moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)";
   4.414 +      apply clarify
   4.415 +      by (simp add: StandardRes_prop1 zcong_sym)
   4.416 +    moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)";
   4.417 +      apply clarify
   4.418 +      apply (insert a b)
   4.419 +      by (rule_tac b = "p - x" in zcong_trans, auto)
   4.420 +    ultimately have c:
   4.421 +      "[gsetprod (StandardRes p o (op - p)) E = gsetprod (uminus) E](mod p)";
   4.422 +      apply simp
   4.423 +      apply (insert finite_E p_g_0)
   4.424 +      by (frule gsetprod_same_function_zcong [of E "StandardRes p o (op - p)"
   4.425 +                                                     uminus p], auto);
   4.426 +    then have two: "[gsetprod id F = gsetprod (uminus) E](mod p)";
   4.427 +      apply (insert one c)
   4.428 +      by (rule zcong_trans [of "gsetprod id F" 
   4.429 +                               "gsetprod (StandardRes p o op - p) E" p
   4.430 +                               "gsetprod uminus E"], auto); 
   4.431 +    also have "gsetprod uminus E = (gsetprod id E) * (-1)^(card E)"; 
   4.432 +      apply (insert finite_E)
   4.433 +      by (induct set: Finites, auto)
   4.434 +    then have "gsetprod uminus E = (-1) ^ (card E) * (gsetprod id E)";
   4.435 +      by (simp add: zmult_commute)
   4.436 +    with two show ?thesis
   4.437 +      by simp
   4.438 +qed;
   4.439 +
   4.440 +subsection {* Gauss' Lemma *}
   4.441 +
   4.442 +lemma (in GAUSS) aux: "gsetprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = gsetprod id A * a ^ card A";
   4.443 +  by (auto simp add: finite_E neg_one_special)
   4.444 +
   4.445 +theorem (in GAUSS) pre_gauss_lemma:
   4.446 +    "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)";
   4.447 +  proof -;
   4.448 +    have "[gsetprod id A = gsetprod id F * gsetprod id D](mod p)";
   4.449 +      by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
   4.450 +    then have "[gsetprod id A = ((-1)^(card E) * gsetprod id E) * 
   4.451 +        gsetprod id D] (mod p)";
   4.452 +      apply (rule zcong_trans)
   4.453 +      by (auto simp add: prod_F_zcong zcong_scalar)
   4.454 +    then have "[gsetprod id A = ((-1)^(card E) * gsetprod id C)] (mod p)";
   4.455 +      apply (rule zcong_trans)
   4.456 +      apply (insert C_prod_eq_D_times_E, erule subst)
   4.457 +      by (subst zmult_assoc, auto)
   4.458 +    then have "[gsetprod id A = ((-1)^(card E) * gsetprod id B)] (mod p)"
   4.459 +      apply (rule zcong_trans)
   4.460 +      by (simp add: C_B_zcong_prod zcong_scalar2)
   4.461 +    then have "[gsetprod id A = ((-1)^(card E) *
   4.462 +        (gsetprod id ((%x. x * a) ` A)))] (mod p)";
   4.463 +      by (simp add: B_def)
   4.464 +    then have "[gsetprod id A = ((-1)^(card E) * (gsetprod (%x. x * a) A))] 
   4.465 +        (mod p)";
   4.466 +      apply (rule zcong_trans)
   4.467 +      by (simp add: finite_A inj_on_xa_A prod_prop_id zcong_scalar2)
   4.468 +    moreover have "gsetprod (%x. x * a) A = 
   4.469 +        gsetprod (%x. a) A * gsetprod id A";
   4.470 +      by (insert finite_A, induct set: Finites, auto)
   4.471 +    ultimately have "[gsetprod id A = ((-1)^(card E) * (gsetprod (%x. a) A * 
   4.472 +        gsetprod id A))] (mod p)";
   4.473 +      by simp 
   4.474 +    then have "[gsetprod id A = ((-1)^(card E) * a^(card A) * 
   4.475 +        gsetprod id A)](mod p)";
   4.476 +      apply (rule zcong_trans)
   4.477 +      by (simp add: zcong_scalar2 zcong_scalar finite_A gsetprod_const
   4.478 +        zmult_assoc)
   4.479 +    then have a: "[gsetprod id A * (-1)^(card E) = 
   4.480 +        ((-1)^(card E) * a^(card A) * gsetprod id A * (-1)^(card E))](mod p)";
   4.481 +      by (rule zcong_scalar)
   4.482 +    then have "[gsetprod id A * (-1)^(card E) = gsetprod id A * 
   4.483 +        (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)";
   4.484 +      apply (rule zcong_trans)
   4.485 +      by (simp add: a zmult_commute zmult_left_commute)
   4.486 +    then have "[gsetprod id A * (-1)^(card E) = gsetprod id A * 
   4.487 +        a^(card A)](mod p)";
   4.488 +      apply (rule zcong_trans)
   4.489 +      by (simp add: aux)
   4.490 +    with this zcong_cancel2 [of p "gsetprod id A" "-1 ^ card E" "a ^ card A"]
   4.491 +         p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)";
   4.492 +       by (simp add: order_less_imp_le)
   4.493 +    from this show ?thesis
   4.494 +      by (simp add: A_card_eq zcong_sym)
   4.495 +qed;
   4.496 +
   4.497 +theorem (in GAUSS) gauss_lemma: "(Legendre a p) = (-1) ^ (card E)";
   4.498 +proof -;
   4.499 +  from Euler_Criterion p_prime p_g_2 have
   4.500 +    "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)";
   4.501 +    by auto
   4.502 +  moreover note pre_gauss_lemma;
   4.503 +  ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)";
   4.504 +    by (rule zcong_trans)
   4.505 +  moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)";
   4.506 +    by (auto simp add: Legendre_def)
   4.507 +  moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1";
   4.508 +    by (rule neg_one_power)
   4.509 +  ultimately show ?thesis;
   4.510 +    by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym)
   4.511 +qed;
   4.512 +
   4.513 +end;
   4.514 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/NumberTheory/Int2.thy	Thu Mar 20 15:58:25 2003 +0100
     5.3 @@ -0,0 +1,310 @@
     5.4 +(*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy
     5.5 +    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     5.6 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5.7 +*)
     5.8 +
     5.9 +header {*Integers: Divisibility and Congruences*}
    5.10 +
    5.11 +theory Int2 = Finite2 + WilsonRuss:;
    5.12 +
    5.13 +text{*Note.  This theory is being revised.  See the web page
    5.14 +\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
    5.15 +
    5.16 +constdefs
    5.17 +  MultInv :: "int => int => int" 
    5.18 +  "MultInv p x == x ^ nat (p - 2)";
    5.19 +
    5.20 +(*****************************************************************)
    5.21 +(*                                                               *)
    5.22 +(* Useful lemmas about dvd and powers                            *)
    5.23 +(*                                                               *)
    5.24 +(*****************************************************************)
    5.25 +
    5.26 +lemma zpower_zdvd_prop1 [rule_format]: "((0 < n) & (p dvd y)) --> 
    5.27 +    p dvd ((y::int) ^ n)";
    5.28 +  by (induct_tac n, auto simp add: zdvd_zmult zdvd_zmult2 [of p y])
    5.29 +
    5.30 +lemma zdvd_bounds: "n dvd m ==> (m \<le> (0::int) | n \<le> m)";
    5.31 +proof -;
    5.32 +  assume "n dvd m";
    5.33 +  then have "~(0 < m & m < n)";
    5.34 +    apply (insert zdvd_not_zless [of m n])
    5.35 +    by (rule contrapos_pn, auto)
    5.36 +  then have "(~0 < m | ~m < n)"  by auto
    5.37 +  then show ?thesis by auto
    5.38 +qed;
    5.39 +
    5.40 +lemma aux4: " -(m * n) = (-m) * (n::int)";
    5.41 +  by auto
    5.42 +
    5.43 +lemma zprime_zdvd_zmult_better: "[| p \<in> zprime;  p dvd (m * n) |] ==> 
    5.44 +    (p dvd m) | (p dvd n)";
    5.45 +  apply (case_tac "0 \<le> m")
    5.46 +  apply (simp add: zprime_zdvd_zmult)
    5.47 +  by (insert zprime_zdvd_zmult [of "-m" p n], auto)
    5.48 +
    5.49 +lemma zpower_zdvd_prop2 [rule_format]: "p \<in> zprime --> p dvd ((y::int) ^ n) 
    5.50 +    --> 0 < n --> p dvd y";
    5.51 +  apply (induct_tac n, auto)
    5.52 +  apply (frule zprime_zdvd_zmult_better, auto)
    5.53 +done
    5.54 +
    5.55 +lemma stupid: "(0 :: int) \<le> y ==> x \<le> x + y";
    5.56 +  by arith
    5.57 +
    5.58 +lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y";
    5.59 +proof -;
    5.60 +  assume "0 < z";
    5.61 +  then have "(x div z) * z \<le> (x div z) * z + x mod z";
    5.62 +  apply (rule_tac x = "x div z * z" in stupid)
    5.63 +  by (simp add: pos_mod_sign)
    5.64 +  also have "... = x";
    5.65 +    by (auto simp add: zmod_zdiv_equality [THEN sym] zmult_ac)
    5.66 +  also assume  "x < y * z";
    5.67 +  finally show ?thesis;
    5.68 +    by (auto simp add: prems zmult_zless_cancel2, insert prems, arith)
    5.69 +qed;
    5.70 +
    5.71 +lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y";
    5.72 +proof -;
    5.73 +  assume "0 < z" and "x < (y * z) + z";
    5.74 +  then have "x < (y + 1) * z" by (auto simp add: int_distrib)
    5.75 +  then have "x div z < y + 1";
    5.76 +    by (rule_tac y = "y + 1" in div_prop1, auto simp add: prems)
    5.77 +  then show ?thesis by auto
    5.78 +qed;
    5.79 +
    5.80 +lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)";
    5.81 +proof-;
    5.82 +  assume "0 < y";
    5.83 +  from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto
    5.84 +  moreover have "0 \<le> x mod y";
    5.85 +    by (auto simp add: prems pos_mod_sign)
    5.86 +  ultimately show ?thesis;
    5.87 +    by arith
    5.88 +qed;
    5.89 +
    5.90 +(*****************************************************************)
    5.91 +(*                                                               *)
    5.92 +(* Useful properties of congruences                              *)
    5.93 +(*                                                               *)
    5.94 +(*****************************************************************)
    5.95 +
    5.96 +lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)";
    5.97 +  by (auto simp add: zcong_def)
    5.98 +
    5.99 +lemma zcong_id: "[m = 0] (mod m)";
   5.100 +  by (auto simp add: zcong_def zdvd_0_right)
   5.101 +
   5.102 +lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)";
   5.103 +  by (auto simp add: zcong_refl zcong_zadd)
   5.104 +
   5.105 +lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)";
   5.106 +  by (induct_tac z, auto simp add: zcong_zmult)
   5.107 +
   5.108 +lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==> 
   5.109 +    [a = d](mod m)";
   5.110 +  by (auto, rule_tac b = c in zcong_trans)
   5.111 +
   5.112 +lemma aux1: "a - b = (c::int) ==> a = c + b";
   5.113 +  by auto
   5.114 +
   5.115 +lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) = 
   5.116 +    [c = b * d] (mod m))";
   5.117 +  apply (auto simp add: zcong_def dvd_def)
   5.118 +  apply (rule_tac x = "ka + k * d" in exI)
   5.119 +  apply (drule aux1)+;
   5.120 +  apply (auto simp add: int_distrib)
   5.121 +  apply (rule_tac x = "ka - k * d" in exI)
   5.122 +  apply (drule aux1)+;
   5.123 +  apply (auto simp add: int_distrib)
   5.124 +done
   5.125 +
   5.126 +lemma zcong_zmult_prop2: "[a = b](mod m) ==> 
   5.127 +    ([c = d * a](mod m) = [c = d * b] (mod m))";
   5.128 +  by (auto simp add: zmult_ac zcong_zmult_prop1)
   5.129 +
   5.130 +lemma zcong_zmult_prop3: "[|p \<in> zprime; ~[x = 0] (mod p); 
   5.131 +    ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)";
   5.132 +  apply (auto simp add: zcong_def)
   5.133 +  apply (drule zprime_zdvd_zmult_better, auto)
   5.134 +done
   5.135 +
   5.136 +lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m); 
   5.137 +    x < m; y < m |] ==> x = y";
   5.138 +  apply (simp add: zcong_zmod_eq)
   5.139 +  apply (subgoal_tac "(x mod m) = x");
   5.140 +  apply (subgoal_tac "(y mod m) = y");
   5.141 +  apply simp
   5.142 +  apply (rule_tac [1-2] mod_pos_pos_trivial)
   5.143 +by auto
   5.144 +
   5.145 +lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==> 
   5.146 +    ~([x = 1] (mod p))";
   5.147 +proof;
   5.148 +  assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
   5.149 +  then have "[1 = -1] (mod p)";
   5.150 +    apply (auto simp add: zcong_sym)
   5.151 +    apply (drule zcong_trans, auto)
   5.152 +  done
   5.153 +  then have "[1 + 1 = -1 + 1] (mod p)";
   5.154 +    by (simp only: zcong_shift)
   5.155 +  then have "[2 = 0] (mod p)";
   5.156 +    by auto
   5.157 +  then have "p dvd 2";
   5.158 +    by (auto simp add: dvd_def zcong_def)
   5.159 +  with prems show False;
   5.160 +    by (auto simp add: zdvd_not_zless)
   5.161 +qed;
   5.162 +
   5.163 +lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)";
   5.164 +  by (auto simp add: zcong_def)
   5.165 +
   5.166 +lemma zcong_zprime_prod_zero: "[| p \<in> zprime; 0 < a |] ==> 
   5.167 +  [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)"; 
   5.168 +  by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult)
   5.169 +
   5.170 +lemma zcong_zprime_prod_zero_contra: "[| p \<in> zprime; 0 < a |] ==>
   5.171 +  ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)";
   5.172 +  apply auto 
   5.173 +  apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero)
   5.174 +by auto
   5.175 +
   5.176 +lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)"; 
   5.177 +  by (auto simp add: zcong_zero_equiv_div zdvd_not_zless)
   5.178 +
   5.179 +lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0";
   5.180 +  apply (drule order_le_imp_less_or_eq, auto)
   5.181 +by (frule_tac m = m in zcong_not_zero, auto)
   5.182 +
   5.183 +lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |]
   5.184 +    ==> zgcd (gsetprod id A,y) = 1";
   5.185 +  by (induct set: Finites, auto simp add: zgcd_zgcd_zmult)
   5.186 +
   5.187 +(*****************************************************************)
   5.188 +(*                                                               *)
   5.189 +(* Some properties of MultInv                                    *)
   5.190 +(*                                                               *)
   5.191 +(*****************************************************************)
   5.192 +
   5.193 +lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> 
   5.194 +    [(MultInv p x) = (MultInv p y)] (mod p)";
   5.195 +  by (auto simp add: MultInv_def zcong_zpower)
   5.196 +
   5.197 +lemma MultInv_prop2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
   5.198 +  [(x * (MultInv p x)) = 1] (mod p)";
   5.199 +proof (simp add: MultInv_def zcong_eq_zdvd_prop);
   5.200 +  assume "2 < p" and "p \<in> zprime" and "~ p dvd x";
   5.201 +  have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)";
   5.202 +    by auto
   5.203 +  also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)";
   5.204 +    by (simp only: nat_add_distrib, auto)
   5.205 +  also have "p - 2 + 1 = p - 1" by arith
   5.206 +  finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)";
   5.207 +    by (rule ssubst, auto)
   5.208 +  also from prems have "[x ^ nat (p - 1) = 1] (mod p)";
   5.209 +    by (auto simp add: Little_Fermat) 
   5.210 +  finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)";.;
   5.211 +qed;
   5.212 +
   5.213 +lemma MultInv_prop2a: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
   5.214 +    [(MultInv p x) * x = 1] (mod p)";
   5.215 +  by (auto simp add: MultInv_prop2 zmult_ac)
   5.216 +
   5.217 +lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))";
   5.218 +  by (simp add: nat_diff_distrib)
   5.219 +
   5.220 +lemma aux_2: "2 < p ==> 0 < nat (p - 2)";
   5.221 +  by auto
   5.222 +
   5.223 +lemma MultInv_prop3: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
   5.224 +    ~([MultInv p x = 0](mod p))";
   5.225 +  apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1)
   5.226 +  apply (drule aux_2)
   5.227 +  apply (drule zpower_zdvd_prop2, auto)
   5.228 +done
   5.229 +
   5.230 +lemma aux__1: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==> 
   5.231 +    [(MultInv p (MultInv p x)) = (x * (MultInv p x) * 
   5.232 +      (MultInv p (MultInv p x)))] (mod p)";
   5.233 +  apply (drule MultInv_prop2, auto)
   5.234 +  apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto);
   5.235 +  apply (auto simp add: zcong_sym)
   5.236 +done
   5.237 +
   5.238 +lemma aux__2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==>
   5.239 +    [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)";
   5.240 +  apply (frule MultInv_prop3, auto)
   5.241 +  apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
   5.242 +  apply (drule MultInv_prop2, auto)
   5.243 +  apply (drule_tac k = x in zcong_scalar2, auto)
   5.244 +  apply (auto simp add: zmult_ac)
   5.245 +done
   5.246 +
   5.247 +lemma MultInv_prop4: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
   5.248 +    [(MultInv p (MultInv p x)) = x] (mod p)";
   5.249 +  apply (frule aux__1, auto)
   5.250 +  apply (drule aux__2, auto)
   5.251 +  apply (drule zcong_trans, auto)
   5.252 +done
   5.253 +
   5.254 +lemma MultInv_prop5: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)); 
   5.255 +    ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> 
   5.256 +    [x = y] (mod p)";
   5.257 +  apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and 
   5.258 +    m = p and k = x in zcong_scalar)
   5.259 +  apply (insert MultInv_prop2 [of p x], simp)
   5.260 +  apply (auto simp only: zcong_sym [of "MultInv p x * x"])
   5.261 +  apply (auto simp add:  zmult_ac)
   5.262 +  apply (drule zcong_trans, auto)
   5.263 +  apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto)
   5.264 +  apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac)
   5.265 +  apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
   5.266 +  apply (auto simp add: zcong_sym)
   5.267 +done
   5.268 +
   5.269 +lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> 
   5.270 +    [a * MultInv p j = a * MultInv p k] (mod p)";
   5.271 +  by (drule MultInv_prop1, auto simp add: zcong_scalar2)
   5.272 +
   5.273 +lemma aux___1: "[j = a * MultInv p k] (mod p) ==> 
   5.274 +    [j * k = a * MultInv p k * k] (mod p)";
   5.275 +  by (auto simp add: zcong_scalar)
   5.276 +
   5.277 +lemma aux___2: "[|2 < p; p \<in> zprime; ~([k = 0](mod p)); 
   5.278 +    [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)";
   5.279 +  apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 
   5.280 +    [of "MultInv p k * k" 1 p "j * k" a])
   5.281 +  apply (auto simp add: zmult_ac)
   5.282 +done
   5.283 +
   5.284 +lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = 
   5.285 +     (MultInv p j) * a] (mod p)";
   5.286 +  by (auto simp add: zmult_assoc zcong_scalar2)
   5.287 +
   5.288 +lemma aux___4: "[|2 < p; p \<in> zprime; ~([j = 0](mod p)); 
   5.289 +    [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
   5.290 +       ==> [k = a * (MultInv p j)] (mod p)";
   5.291 +  apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 
   5.292 +    [of "MultInv p j * j" 1 p "MultInv p j * a" k])
   5.293 +  apply (auto simp add: zmult_ac zcong_sym)
   5.294 +done
   5.295 +
   5.296 +lemma MultInv_zcong_prop2: "[| 2 < p; p \<in> zprime; ~([k = 0](mod p)); 
   5.297 +    ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> 
   5.298 +    [k = a * MultInv p j] (mod p)";
   5.299 +  apply (drule aux___1)
   5.300 +  apply (frule aux___2, auto)
   5.301 +  by (drule aux___3, drule aux___4, auto)
   5.302 +
   5.303 +lemma MultInv_zcong_prop3: "[| 2 < p; p \<in> zprime; ~([a = 0](mod p)); 
   5.304 +    ~([k = 0](mod p)); ~([j = 0](mod p));
   5.305 +    [a * MultInv p j = a * MultInv p k] (mod p) |] ==> 
   5.306 +      [j = k] (mod p)";
   5.307 +  apply (auto simp add: zcong_eq_zdvd_prop [of a p])
   5.308 +  apply (frule zprime_imp_zrelprime, auto)
   5.309 +  apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto)
   5.310 +  apply (drule MultInv_prop5, auto)
   5.311 +done
   5.312 +
   5.313 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Thu Mar 20 15:58:25 2003 +0100
     6.3 @@ -0,0 +1,628 @@
     6.4 +(*  Title:      HOL/Quadratic_Reciprocity/Quadratic_Reciprocity.thy
     6.5 +    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     6.6 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     6.7 +*)
     6.8 +
     6.9 +header {* The law of Quadratic reciprocity *}
    6.10 +
    6.11 +theory Quadratic_Reciprocity = Gauss:;
    6.12 +
    6.13 +(***************************************************************)
    6.14 +(*                                                             *)
    6.15 +(*  Lemmas leading up to the proof of theorem 3.3 in           *)
    6.16 +(*  Niven and Zuckerman's presentation                         *)
    6.17 +(*                                                             *)
    6.18 +(***************************************************************)
    6.19 +
    6.20 +lemma (in GAUSS) QRLemma1: "a * setsum id A = 
    6.21 +  p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E";
    6.22 +proof -;
    6.23 +  from finite_A have "a * setsum id A = setsum (%x. a * x) A"; 
    6.24 +    by (auto simp add: setsum_const_mult id_def)
    6.25 +  also have "setsum (%x. a * x) = setsum (%x. x * a)"; 
    6.26 +    by (auto simp add: zmult_commute)
    6.27 +  also; have "setsum (%x. x * a) A = setsum id B";
    6.28 +    by (auto simp add: B_def sum_prop_id finite_A inj_on_xa_A)
    6.29 +  also have "... = setsum (%x. p * (x div p) + StandardRes p x) B";
    6.30 +    apply (rule setsum_same_function)
    6.31 +    by (auto simp add: finite_B StandardRes_def zmod_zdiv_equality)
    6.32 +  also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B";
    6.33 +    by (rule setsum_addf)
    6.34 +  also; have "setsum (StandardRes p) B = setsum id C";
    6.35 +    by (auto simp add: C_def sum_prop_id [THEN sym] finite_B 
    6.36 +      SR_B_inj)
    6.37 +  also; from C_eq have "... = setsum id (D \<union> E)";
    6.38 +    by auto
    6.39 +  also; from finite_D finite_E have "... = setsum id D + setsum id E";
    6.40 +    apply (rule setsum_Un_disjoint)
    6.41 +    by (auto simp add: D_def E_def)
    6.42 +  also have "setsum (%x. p * (x div p)) B = 
    6.43 +      setsum ((%x. p * (x div p)) o (%x. (x * a))) A";
    6.44 +    by (auto simp add: B_def sum_prop finite_A inj_on_xa_A)
    6.45 +  also have "... = setsum (%x. p * ((x * a) div p)) A";
    6.46 +    by (auto simp add: o_def)
    6.47 +  also from finite_A have "setsum (%x. p * ((x * a) div p)) A = 
    6.48 +    p * setsum (%x. ((x * a) div p)) A";
    6.49 +    by (auto simp add: setsum_const_mult)
    6.50 +  finally show ?thesis by arith
    6.51 +qed;
    6.52 +
    6.53 +lemma (in GAUSS) QRLemma2: "setsum id A = p * int (card E) - setsum id E + 
    6.54 +  setsum id D"; 
    6.55 +proof -;
    6.56 +  from F_Un_D_eq_A have "setsum id A = setsum id (D \<union> F)";
    6.57 +    by (simp add: Un_commute)
    6.58 +  also from F_D_disj finite_D finite_F have 
    6.59 +      "... = setsum id D + setsum id F";
    6.60 +    apply (simp add: Int_commute)
    6.61 +    by (intro setsum_Un_disjoint) 
    6.62 +  also from F_def have "F = (%x. (p - x)) ` E";
    6.63 +    by auto
    6.64 +  also from finite_E inj_on_pminusx_E have "setsum id ((%x. (p - x)) ` E) =
    6.65 +      setsum (%x. (p - x)) E";
    6.66 +    by (auto simp add: sum_prop)
    6.67 +  also from finite_E have "setsum (op - p) E = setsum (%x. p) E - setsum id E";
    6.68 +    by (auto simp add: setsum_minus id_def)
    6.69 +  also from finite_E have "setsum (%x. p) E = p * int(card E)";
    6.70 +    by (intro setsum_const)
    6.71 +  finally show ?thesis;
    6.72 +    by arith
    6.73 +qed;
    6.74 +
    6.75 +lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A = 
    6.76 +    p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E";
    6.77 +proof -;
    6.78 +  have "(a - 1) * setsum id A = a * setsum id A - setsum id A";
    6.79 +    by (auto simp add: zdiff_zmult_distrib)  
    6.80 +  also note QRLemma1;
    6.81 +  also; from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D + 
    6.82 +     setsum id E - setsum id A = 
    6.83 +      p * (\<Sum>x \<in> A. x * a div p) + setsum id D + 
    6.84 +      setsum id E - (p * int (card E) - setsum id E + setsum id D)";
    6.85 +    by auto
    6.86 +  also; have "... = p * (\<Sum>x \<in> A. x * a div p) - 
    6.87 +      p * int (card E) + 2 * setsum id E"; 
    6.88 +    by arith
    6.89 +  finally show ?thesis;
    6.90 +    by (auto simp only: zdiff_zmult_distrib2)
    6.91 +qed;
    6.92 +
    6.93 +lemma (in GAUSS) QRLemma4: "a \<in> zOdd ==> 
    6.94 +    (setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)";
    6.95 +proof -;
    6.96 +  assume a_odd: "a \<in> zOdd";
    6.97 +  from QRLemma3 have a: "p * (setsum (%x. ((x * a) div p)) A - int(card E)) =
    6.98 +      (a - 1) * setsum id A - 2 * setsum id E"; 
    6.99 +    by arith
   6.100 +  from a_odd have "a - 1 \<in> zEven"
   6.101 +    by (rule odd_minus_one_even)
   6.102 +  hence "(a - 1) * setsum id A \<in> zEven";
   6.103 +    by (rule even_times_either)
   6.104 +  moreover have "2 * setsum id E \<in> zEven";
   6.105 +    by (auto simp add: zEven_def)
   6.106 +  ultimately have "(a - 1) * setsum id A - 2 * setsum id E \<in> zEven"
   6.107 +    by (rule even_minus_even)
   6.108 +  with a have "p * (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
   6.109 +    by simp
   6.110 +  hence "p \<in> zEven | (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
   6.111 +    by (rule even_product)
   6.112 +  with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
   6.113 +    by (auto simp add: odd_iff_not_even)
   6.114 +  thus ?thesis;
   6.115 +    by (auto simp only: even_diff [THEN sym])
   6.116 +qed;
   6.117 +
   6.118 +lemma (in GAUSS) QRLemma5: "a \<in> zOdd ==> 
   6.119 +   (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))";
   6.120 +proof -;
   6.121 +  assume "a \<in> zOdd";
   6.122 +  from QRLemma4 have
   6.123 +    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)";..;
   6.124 +  moreover have "0 \<le> int(card E)";
   6.125 +    by auto
   6.126 +  moreover have "0 \<le> setsum (%x. ((x * a) div p)) A";
   6.127 +    proof (intro setsum_non_neg);
   6.128 +      from finite_A show "finite A";.;
   6.129 +      next show "\<forall>x \<in> A. 0 \<le> x * a div p";
   6.130 +      proof;
   6.131 +        fix x;
   6.132 +        assume "x \<in> A";
   6.133 +        then have "0 \<le> x";
   6.134 +          by (auto simp add: A_def)
   6.135 +        with a_nonzero have "0 \<le> x * a";
   6.136 +          by (auto simp add: int_0_le_mult_iff)
   6.137 +        with p_g_2 show "0 \<le> x * a div p"; 
   6.138 +          by (auto simp add: pos_imp_zdiv_nonneg_iff)
   6.139 +      qed;
   6.140 +    qed;
   6.141 +  ultimately have "(-1::int)^nat((int (card E))) =
   6.142 +      (-1)^nat(((\<Sum>x \<in> A. x * a div p)))";
   6.143 +    by (intro neg_one_power_parity, auto)
   6.144 +  also have "nat (int(card E)) = card E";
   6.145 +    by auto
   6.146 +  finally show ?thesis;.;
   6.147 +qed;
   6.148 +
   6.149 +lemma MainQRLemma: "[| a \<in> zOdd; 0 < a; ~([a = 0] (mod p));p \<in> zprime; 2 < p;
   6.150 +  A = {x. 0 < x & x \<le> (p - 1) div 2} |] ==> 
   6.151 +  (Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))";
   6.152 +  apply (subst GAUSS.gauss_lemma)
   6.153 +  apply (auto simp add: GAUSS_def)
   6.154 +  apply (subst GAUSS.QRLemma5)
   6.155 +by (auto simp add: GAUSS_def)
   6.156 +
   6.157 +(******************************************************************)
   6.158 +(*                                                                *)
   6.159 +(* Stuff about S, S1 and S2...                                    *)
   6.160 +(*                                                                *)
   6.161 +(******************************************************************)
   6.162 +
   6.163 +locale QRTEMP =
   6.164 +  fixes p     :: "int"
   6.165 +  fixes q     :: "int"
   6.166 +  fixes P_set :: "int set"
   6.167 +  fixes Q_set :: "int set"
   6.168 +  fixes S     :: "(int * int) set"
   6.169 +  fixes S1    :: "(int * int) set"
   6.170 +  fixes S2    :: "(int * int) set"
   6.171 +  fixes f1    :: "int => (int * int) set"
   6.172 +  fixes f2    :: "int => (int * int) set"
   6.173 +
   6.174 +  assumes p_prime: "p \<in> zprime"
   6.175 +  assumes p_g_2: "2 < p"
   6.176 +  assumes q_prime: "q \<in> zprime"
   6.177 +  assumes q_g_2: "2 < q"
   6.178 +  assumes p_neq_q:      "p \<noteq> q"
   6.179 +
   6.180 +  defines P_set_def: "P_set == {x. 0 < x & x \<le> ((p - 1) div 2) }"
   6.181 +  defines Q_set_def: "Q_set == {x. 0 < x & x \<le> ((q - 1) div 2) }"
   6.182 +  defines S_def:     "S     == P_set <*> Q_set"
   6.183 +  defines S1_def:    "S1    == { (x, y). (x, y):S & ((p * y) < (q * x)) }"
   6.184 +  defines S2_def:    "S2    == { (x, y). (x, y):S & ((q * x) < (p * y)) }"
   6.185 +  defines f1_def:    "f1 j  == { (j1, y). (j1, y):S & j1 = j & 
   6.186 +                                 (y \<le> (q * j) div p) }"
   6.187 +  defines f2_def:    "f2 j  == { (x, j1). (x, j1):S & j1 = j & 
   6.188 +                                 (x \<le> (p * j) div q) }";
   6.189 +
   6.190 +lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2";
   6.191 +proof -;
   6.192 +  from prems have "2 < p" by (simp add: QRTEMP_def)
   6.193 +  then have "2 \<le> p - 1" by arith
   6.194 +  then have "2 div 2 \<le> (p - 1) div 2" by (rule zdiv_mono1, auto)
   6.195 +  then show ?thesis by auto
   6.196 +qed;
   6.197 +
   6.198 +lemma (in QRTEMP) q_fact: "0 < (q - 1) div 2";
   6.199 +proof -;
   6.200 +  from prems have "2 < q" by (simp add: QRTEMP_def)
   6.201 +  then have "2 \<le> q - 1" by arith
   6.202 +  then have "2 div 2 \<le> (q - 1) div 2" by (rule zdiv_mono1, auto)
   6.203 +  then show ?thesis by auto
   6.204 +qed;
   6.205 +
   6.206 +lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==> 
   6.207 +    (p * b \<noteq> q * a)";
   6.208 +proof;
   6.209 +  assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2";
   6.210 +  then have "q dvd (p * b)" by (auto simp add: dvd_def)
   6.211 +  with q_prime p_g_2 have "q dvd p | q dvd b";
   6.212 +    by (auto simp add: zprime_zdvd_zmult)
   6.213 +  moreover have "~ (q dvd p)";
   6.214 +  proof;
   6.215 +    assume "q dvd p";
   6.216 +    with p_prime have "q = 1 | q = p"
   6.217 +      apply (auto simp add: zprime_def QRTEMP_def)
   6.218 +      apply (drule_tac x = q and R = False in allE)
   6.219 +      apply (simp add: QRTEMP_def)    
   6.220 +      apply (subgoal_tac "0 \<le> q", simp add: QRTEMP_def)
   6.221 +      apply (insert prems)
   6.222 +    by (auto simp add: QRTEMP_def)
   6.223 +    with q_g_2 p_neq_q show False by auto
   6.224 +  qed;
   6.225 +  ultimately have "q dvd b" by auto
   6.226 +  then have "q \<le> b";
   6.227 +  proof -;
   6.228 +    assume "q dvd b";
   6.229 +    moreover from prems have "0 < b" by auto
   6.230 +    ultimately show ?thesis by (insert zdvd_bounds [of q b], auto)
   6.231 +  qed;
   6.232 +  with prems have "q \<le> (q - 1) div 2" by auto
   6.233 +  then have "2 * q \<le> 2 * ((q - 1) div 2)" by arith
   6.234 +  then have "2 * q \<le> q - 1";
   6.235 +  proof -;
   6.236 +    assume "2 * q \<le> 2 * ((q - 1) div 2)";
   6.237 +    with prems have "q \<in> zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
   6.238 +    with odd_minus_one_even have "(q - 1):zEven" by auto
   6.239 +    with even_div_2_prop2 have "(q - 1) = 2 * ((q - 1) div 2)" by auto
   6.240 +    with prems show ?thesis by auto
   6.241 +  qed;
   6.242 +  then have p1: "q \<le> -1" by arith
   6.243 +  with q_g_2 show False by auto
   6.244 +qed;
   6.245 +
   6.246 +lemma (in QRTEMP) P_set_finite: "finite (P_set)";
   6.247 +  by (insert p_fact, auto simp add: P_set_def bdd_int_set_l_le_finite)
   6.248 +
   6.249 +lemma (in QRTEMP) Q_set_finite: "finite (Q_set)";
   6.250 +  by (insert q_fact, auto simp add: Q_set_def bdd_int_set_l_le_finite)
   6.251 +
   6.252 +lemma (in QRTEMP) S_finite: "finite S";
   6.253 +  by (auto simp add: S_def  P_set_finite Q_set_finite cartesian_product_finite)
   6.254 +
   6.255 +lemma (in QRTEMP) S1_finite: "finite S1";
   6.256 +proof -;
   6.257 +  have "finite S" by (auto simp add: S_finite)
   6.258 +  moreover have "S1 \<subseteq> S" by (auto simp add: S1_def S_def)
   6.259 +  ultimately show ?thesis by (auto simp add: finite_subset)
   6.260 +qed;
   6.261 +
   6.262 +lemma (in QRTEMP) S2_finite: "finite S2";
   6.263 +proof -;
   6.264 +  have "finite S" by (auto simp add: S_finite)
   6.265 +  moreover have "S2 \<subseteq> S" by (auto simp add: S2_def S_def)
   6.266 +  ultimately show ?thesis by (auto simp add: finite_subset)
   6.267 +qed;
   6.268 +
   6.269 +lemma (in QRTEMP) P_set_card: "(p - 1) div 2 = int (card (P_set))";
   6.270 +  by (insert p_fact, auto simp add: P_set_def card_bdd_int_set_l_le)
   6.271 +
   6.272 +lemma (in QRTEMP) Q_set_card: "(q - 1) div 2 = int (card (Q_set))";
   6.273 +  by (insert q_fact, auto simp add: Q_set_def card_bdd_int_set_l_le)
   6.274 +
   6.275 +lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
   6.276 +  apply (insert P_set_card Q_set_card P_set_finite Q_set_finite)
   6.277 +  apply (auto simp add: S_def zmult_int)
   6.278 +done
   6.279 +
   6.280 +lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}";
   6.281 +  by (auto simp add: S1_def S2_def)
   6.282 +
   6.283 +lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \<union> S2";
   6.284 +  apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def)
   6.285 +  proof -;
   6.286 +    fix a and b;
   6.287 +    assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2";
   6.288 +    with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
   6.289 +    moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
   6.290 +    ultimately show "p * b < q * a" by auto
   6.291 +  qed;
   6.292 +
   6.293 +lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) = 
   6.294 +    int(card(S1)) + int(card(S2))";
   6.295 +proof-;
   6.296 +  have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
   6.297 +    by (auto simp add: S_card)
   6.298 +  also have "... = int( card(S1) + card(S2))";
   6.299 +    apply (insert S1_finite S2_finite S1_Int_S2_prop S1_Union_S2_prop)
   6.300 +    apply (drule card_Un_disjoint, auto)
   6.301 +  done
   6.302 +  also have "... = int(card(S1)) + int(card(S2))" by auto
   6.303 +  finally show ?thesis .;
   6.304 +qed;
   6.305 +
   6.306 +lemma (in QRTEMP) aux1a: "[| 0 < a; a \<le> (p - 1) div 2; 
   6.307 +                             0 < b; b \<le> (q - 1) div 2 |] ==>
   6.308 +                          (p * b < q * a) = (b \<le> q * a div p)";
   6.309 +proof -;
   6.310 +  assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2";
   6.311 +  have "p * b < q * a ==> b \<le> q * a div p";
   6.312 +  proof -;
   6.313 +    assume "p * b < q * a";
   6.314 +    then have "p * b \<le> q * a" by auto
   6.315 +    then have "(p * b) div p \<le> (q * a) div p";
   6.316 +      by (rule zdiv_mono1, insert p_g_2, auto)
   6.317 +    then show "b \<le> (q * a) div p";
   6.318 +      apply (subgoal_tac "p \<noteq> 0")
   6.319 +      apply (frule zdiv_zmult_self2, force)
   6.320 +      by (insert p_g_2, auto)
   6.321 +  qed;
   6.322 +  moreover have "b \<le> q * a div p ==> p * b < q * a";
   6.323 +  proof -;
   6.324 +    assume "b \<le> q * a div p";
   6.325 +    then have "p * b \<le> p * ((q * a) div p)";
   6.326 +      by (insert p_g_2, auto simp add: zmult_zle_cancel1)
   6.327 +    also have "... \<le> q * a";
   6.328 +      by (rule zdiv_leq_prop, insert p_g_2, auto)
   6.329 +    finally have "p * b \<le> q * a" .;
   6.330 +    then have "p * b < q * a | p * b = q * a";
   6.331 +      by (simp only: order_le_imp_less_or_eq)
   6.332 +    moreover have "p * b \<noteq> q * a";
   6.333 +      by (rule  pb_neq_qa, insert prems, auto)
   6.334 +    ultimately show ?thesis by auto
   6.335 +  qed;
   6.336 +  ultimately show ?thesis ..;
   6.337 +qed;
   6.338 +
   6.339 +lemma (in QRTEMP) aux1b: "[| 0 < a; a \<le> (p - 1) div 2; 
   6.340 +                             0 < b; b \<le> (q - 1) div 2 |] ==>
   6.341 +                          (q * a < p * b) = (a \<le> p * b div q)";
   6.342 +proof -;
   6.343 +  assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2";
   6.344 +  have "q * a < p * b ==> a \<le> p * b div q";
   6.345 +  proof -;
   6.346 +    assume "q * a < p * b";
   6.347 +    then have "q * a \<le> p * b" by auto
   6.348 +    then have "(q * a) div q \<le> (p * b) div q";
   6.349 +      by (rule zdiv_mono1, insert q_g_2, auto)
   6.350 +    then show "a \<le> (p * b) div q";
   6.351 +      apply (subgoal_tac "q \<noteq> 0")
   6.352 +      apply (frule zdiv_zmult_self2, force)
   6.353 +      by (insert q_g_2, auto)
   6.354 +  qed;
   6.355 +  moreover have "a \<le> p * b div q ==> q * a < p * b";
   6.356 +  proof -;
   6.357 +    assume "a \<le> p * b div q";
   6.358 +    then have "q * a \<le> q * ((p * b) div q)";
   6.359 +      by (insert q_g_2, auto simp add: zmult_zle_cancel1)
   6.360 +    also have "... \<le> p * b";
   6.361 +      by (rule zdiv_leq_prop, insert q_g_2, auto)
   6.362 +    finally have "q * a \<le> p * b" .;
   6.363 +    then have "q * a < p * b | q * a = p * b";
   6.364 +      by (simp only: order_le_imp_less_or_eq)
   6.365 +    moreover have "p * b \<noteq> q * a";
   6.366 +      by (rule  pb_neq_qa, insert prems, auto)
   6.367 +    ultimately show ?thesis by auto
   6.368 +  qed;
   6.369 +  ultimately show ?thesis ..;
   6.370 +qed;
   6.371 +
   6.372 +lemma aux2: "[| p \<in> zprime; q \<in> zprime; 2 < p; 2 < q |] ==> 
   6.373 +             (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2";
   6.374 +proof-;
   6.375 +  assume "p \<in> zprime" and "q \<in> zprime" and "2 < p" and "2 < q";
   6.376 +  (* Set up what's even and odd *)
   6.377 +  then have "p \<in> zOdd & q \<in> zOdd";
   6.378 +    by (auto simp add:  zprime_zOdd_eq_grt_2)
   6.379 +  then have even1: "(p - 1):zEven & (q - 1):zEven";
   6.380 +    by (auto simp add: odd_minus_one_even)
   6.381 +  then have even2: "(2 * p):zEven & ((q - 1) * p):zEven";
   6.382 +    by (auto simp add: zEven_def)
   6.383 +  then have even3: "(((q - 1) * p) + (2 * p)):zEven";
   6.384 +    by (auto simp: even_plus_even)
   6.385 +  (* using these prove it *)
   6.386 +  from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)";
   6.387 +    by (auto simp add: int_distrib)
   6.388 +  then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2";
   6.389 +    apply (rule_tac x = "((p - 1) * q)" in even_div_2_l);
   6.390 +    by (auto simp add: even3, auto simp add: zmult_ac)
   6.391 +  also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)";
   6.392 +    by (auto simp add: even1 even_prod_div_2)
   6.393 +  also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p";
   6.394 +    by (auto simp add: even1 even2 even_prod_div_2 even_sum_div_2)
   6.395 +  finally show ?thesis 
   6.396 +    apply (rule_tac x = " q * ((p - 1) div 2)" and 
   6.397 +                    y = "(q - 1) div 2" in div_prop2);
   6.398 +    by (insert prems, auto)
   6.399 +qed;
   6.400 +
   6.401 +lemma (in QRTEMP) aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p";
   6.402 +proof;
   6.403 +  fix j;
   6.404 +  assume j_fact: "j \<in> P_set";
   6.405 +  have "int (card (f1 j)) = int (card {y. y \<in> Q_set & y \<le> (q * j) div p})";
   6.406 +  proof -;
   6.407 +    have "finite (f1 j)";
   6.408 +    proof -;
   6.409 +      have "(f1 j) \<subseteq> S" by (auto simp add: f1_def)
   6.410 +      with S_finite show ?thesis by (auto simp add: finite_subset)
   6.411 +    qed;
   6.412 +    moreover have "inj_on (%(x,y). y) (f1 j)";
   6.413 +      by (auto simp add: f1_def inj_on_def)
   6.414 +    ultimately have "card ((%(x,y). y) ` (f1 j)) = card  (f1 j)";
   6.415 +      by (auto simp add: f1_def card_image)
   6.416 +    moreover have "((%(x,y). y) ` (f1 j)) = {y. y \<in> Q_set & y \<le> (q * j) div p}";
   6.417 +      by (insert prems, auto simp add: f1_def S_def Q_set_def P_set_def 
   6.418 +        image_def)
   6.419 +    ultimately show ?thesis by (auto simp add: f1_def)
   6.420 +  qed;
   6.421 +  also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})";
   6.422 +  proof -;
   6.423 +    have "{y. y \<in> Q_set & y \<le> (q * j) div p} = 
   6.424 +        {y. 0 < y & y \<le> (q * j) div p}";
   6.425 +      apply (auto simp add: Q_set_def)
   6.426 +      proof -;
   6.427 +        fix x;
   6.428 +        assume "0 < x" and "x \<le> q * j div p";
   6.429 +        with j_fact P_set_def  have "j \<le> (p - 1) div 2"; by auto
   6.430 +        with q_g_2; have "q * j \<le> q * ((p - 1) div 2)";
   6.431 +          by (auto simp add: zmult_zle_cancel1)
   6.432 +        with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p";
   6.433 +          by (auto simp add: zdiv_mono1)
   6.434 +        also from prems have "... \<le> (q - 1) div 2";
   6.435 +          apply simp apply (insert aux2) by (simp add: QRTEMP_def)
   6.436 +        finally show "x \<le> (q - 1) div 2" by (insert prems, auto)
   6.437 +      qed;
   6.438 +    then show ?thesis by auto
   6.439 +  qed;
   6.440 +  also have "... = (q * j) div p";
   6.441 +  proof -;
   6.442 +    from j_fact P_set_def have "0 \<le> j" by auto
   6.443 +    with q_g_2 have "q * 0 \<le> q * j" by (auto simp only: zmult_zle_mono2)
   6.444 +    then have "0 \<le> q * j" by auto
   6.445 +    then have "0 div p \<le> (q * j) div p";
   6.446 +      apply (rule_tac a = 0 in zdiv_mono1)
   6.447 +      by (insert p_g_2, auto)
   6.448 +    also have "0 div p = 0" by auto
   6.449 +    finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
   6.450 +  qed;
   6.451 +  finally show "int (card (f1 j)) = q * j div p" .;
   6.452 +qed;
   6.453 +
   6.454 +lemma (in QRTEMP) aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q";
   6.455 +proof;
   6.456 +  fix j;
   6.457 +  assume j_fact: "j \<in> Q_set";
   6.458 +  have "int (card (f2 j)) = int (card {y. y \<in> P_set & y \<le> (p * j) div q})";
   6.459 +  proof -;
   6.460 +    have "finite (f2 j)";
   6.461 +    proof -;
   6.462 +      have "(f2 j) \<subseteq> S" by (auto simp add: f2_def)
   6.463 +      with S_finite show ?thesis by (auto simp add: finite_subset)
   6.464 +    qed;
   6.465 +    moreover have "inj_on (%(x,y). x) (f2 j)";
   6.466 +      by (auto simp add: f2_def inj_on_def)
   6.467 +    ultimately have "card ((%(x,y). x) ` (f2 j)) = card  (f2 j)";
   6.468 +      by (auto simp add: f2_def card_image)
   6.469 +    moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}";
   6.470 +      by (insert prems, auto simp add: f2_def S_def Q_set_def 
   6.471 +        P_set_def image_def)
   6.472 +    ultimately show ?thesis by (auto simp add: f2_def)
   6.473 +  qed;
   6.474 +  also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})";
   6.475 +  proof -;
   6.476 +    have "{y. y \<in> P_set & y \<le> (p * j) div q} = 
   6.477 +        {y. 0 < y & y \<le> (p * j) div q}";
   6.478 +      apply (auto simp add: P_set_def)
   6.479 +      proof -;
   6.480 +        fix x;
   6.481 +        assume "0 < x" and "x \<le> p * j div q";
   6.482 +        with j_fact Q_set_def  have "j \<le> (q - 1) div 2"; by auto
   6.483 +        with p_g_2; have "p * j \<le> p * ((q - 1) div 2)";
   6.484 +          by (auto simp add: zmult_zle_cancel1)
   6.485 +        with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q";
   6.486 +          by (auto simp add: zdiv_mono1)
   6.487 +        also from prems have "... \<le> (p - 1) div 2";
   6.488 +          by (auto simp add: aux2 QRTEMP_def)
   6.489 +        finally show "x \<le> (p - 1) div 2" by (insert prems, auto)
   6.490 +      qed;
   6.491 +    then show ?thesis by auto
   6.492 +  qed;
   6.493 +  also have "... = (p * j) div q";
   6.494 +  proof -;
   6.495 +    from j_fact Q_set_def have "0 \<le> j" by auto
   6.496 +    with p_g_2 have "p * 0 \<le> p * j" by (auto simp only: zmult_zle_mono2)
   6.497 +    then have "0 \<le> p * j" by auto
   6.498 +    then have "0 div q \<le> (p * j) div q";
   6.499 +      apply (rule_tac a = 0 in zdiv_mono1)
   6.500 +      by (insert q_g_2, auto)
   6.501 +    also have "0 div q = 0" by auto
   6.502 +    finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
   6.503 +  qed;
   6.504 +  finally show "int (card (f2 j)) = p * j div q" .;
   6.505 +qed;
   6.506 +
   6.507 +lemma (in QRTEMP) S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set";
   6.508 +proof -;
   6.509 +  have "\<forall>x \<in> P_set. finite (f1 x)";
   6.510 +  proof;
   6.511 +    fix x;
   6.512 +    have "f1 x \<subseteq> S" by (auto simp add: f1_def)
   6.513 +    with S_finite show "finite (f1 x)" by (auto simp add: finite_subset)
   6.514 +  qed;
   6.515 +  moreover have "(\<forall>x \<in> P_set. \<forall>y \<in> P_set. x \<noteq> y --> (f1 x) \<inter> (f1 y) = {})";
   6.516 +    by (auto simp add: f1_def)
   6.517 +  moreover note P_set_finite;
   6.518 +  ultimately have "int(card (UNION P_set f1)) = 
   6.519 +      setsum (%x. int(card (f1 x))) P_set";
   6.520 +    by (rule_tac A = P_set in int_card_indexed_union_disjoint_sets, auto)
   6.521 +  moreover have "S1 = UNION P_set f1";
   6.522 +    by (auto simp add: f1_def S_def S1_def S2_def P_set_def Q_set_def aux1a)
   6.523 +  ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set" 
   6.524 +    by auto
   6.525 +  also have "... = setsum (%j. q * j div p) P_set";
   6.526 +  proof -;
   6.527 +    note aux3a
   6.528 +    with  P_set_finite show ?thesis by (rule setsum_same_function)
   6.529 +  qed;
   6.530 +  finally show ?thesis .;
   6.531 +qed;
   6.532 +
   6.533 +lemma (in QRTEMP) S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set";
   6.534 +proof -;
   6.535 +  have "\<forall>x \<in> Q_set. finite (f2 x)";
   6.536 +  proof;
   6.537 +    fix x;
   6.538 +    have "f2 x \<subseteq> S" by (auto simp add: f2_def)
   6.539 +    with S_finite show "finite (f2 x)" by (auto simp add: finite_subset)
   6.540 +  qed;
   6.541 +  moreover have "(\<forall>x \<in> Q_set. \<forall>y \<in> Q_set. x \<noteq> y --> 
   6.542 +      (f2 x) \<inter> (f2 y) = {})";
   6.543 +    by (auto simp add: f2_def)
   6.544 +  moreover note Q_set_finite;
   6.545 +  ultimately have "int(card (UNION Q_set f2)) = 
   6.546 +      setsum (%x. int(card (f2 x))) Q_set";
   6.547 +    by (rule_tac A = Q_set in int_card_indexed_union_disjoint_sets, auto)
   6.548 +  moreover have "S2 = UNION Q_set f2";
   6.549 +    by (auto simp add: f2_def S_def S1_def S2_def P_set_def Q_set_def aux1b)
   6.550 +  ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set" 
   6.551 +    by auto
   6.552 +  also have "... = setsum (%j. p * j div q) Q_set";
   6.553 +  proof -;
   6.554 +    note aux3b;
   6.555 +    with Q_set_finite show ?thesis by (rule setsum_same_function)
   6.556 +  qed;
   6.557 +  finally show ?thesis .;
   6.558 +qed;
   6.559 +
   6.560 +lemma (in QRTEMP) S1_carda: "int (card(S1)) = 
   6.561 +    setsum (%j. (j * q) div p) P_set";
   6.562 +  by (auto simp add: S1_card zmult_ac)
   6.563 +
   6.564 +lemma (in QRTEMP) S2_carda: "int (card(S2)) = 
   6.565 +    setsum (%j. (j * p) div q) Q_set";
   6.566 +  by (auto simp add: S2_card zmult_ac)
   6.567 +
   6.568 +lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) + 
   6.569 +    (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)";
   6.570 +proof -;
   6.571 +  have "(setsum (%j. (j * p) div q) Q_set) + 
   6.572 +      (setsum (%j. (j * q) div p) P_set) = int (card S2) + int (card S1)";
   6.573 +    by (auto simp add: S1_carda S2_carda)
   6.574 +  also have "... = int (card S1) + int (card S2)";
   6.575 +    by auto
   6.576 +  also have "... = ((p - 1) div 2) * ((q - 1) div 2)";
   6.577 +    by (auto simp add: card_sum_S1_S2)
   6.578 +  finally show ?thesis .;
   6.579 +qed;
   6.580 +
   6.581 +lemma pq_prime_neq: "[| p \<in> zprime; q \<in> zprime; p \<noteq> q |] ==> (~[p = 0] (mod q))";
   6.582 +  apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
   6.583 +  apply (drule_tac x = q in allE)
   6.584 +  apply (drule_tac x = p in allE)
   6.585 +by auto
   6.586 +
   6.587 +lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) = 
   6.588 +    (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
   6.589 +proof -;
   6.590 +  from prems have "~([p = 0] (mod q))";
   6.591 +    by (auto simp add: pq_prime_neq QRTEMP_def)
   6.592 +  with prems have a1: "(Legendre p q) = (-1::int) ^ 
   6.593 +      nat(setsum (%x. ((x * p) div q)) Q_set)";
   6.594 +    apply (rule_tac p = q in  MainQRLemma)
   6.595 +    by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
   6.596 +  from prems have "~([q = 0] (mod p))";
   6.597 +    apply (rule_tac p = q and q = p in pq_prime_neq)
   6.598 +    apply (simp add: QRTEMP_def)+;
   6.599 +    by arith
   6.600 +  with prems have a2: "(Legendre q p) = 
   6.601 +      (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)";
   6.602 +    apply (rule_tac p = p in  MainQRLemma)
   6.603 +    by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
   6.604 +  from a1 a2 have "(Legendre p q) * (Legendre q p) = 
   6.605 +      (-1::int) ^ nat(setsum (%x. ((x * p) div q)) Q_set) *
   6.606 +        (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)";
   6.607 +    by auto
   6.608 +  also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) + 
   6.609 +                   nat(setsum (%x. ((x * q) div p)) P_set))";
   6.610 +    by (auto simp add: zpower_zadd_distrib)
   6.611 +  also have "nat(setsum (%x. ((x * p) div q)) Q_set) + 
   6.612 +      nat(setsum (%x. ((x * q) div p)) P_set) =
   6.613 +        nat((setsum (%x. ((x * p) div q)) Q_set) + 
   6.614 +          (setsum (%x. ((x * q) div p)) P_set))";
   6.615 +    apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in 
   6.616 +      nat_add_distrib [THEN sym]);
   6.617 +    by (auto simp add: S1_carda [THEN sym] S2_carda [THEN sym])
   6.618 +  also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))";
   6.619 +    by (auto simp add: pq_sum_prop)
   6.620 +  finally show ?thesis .;
   6.621 +qed;
   6.622 +
   6.623 +theorem Quadratic_Reciprocity:
   6.624 +     "[| p \<in> zOdd; p \<in> zprime; q \<in> zOdd; q \<in> zprime; 
   6.625 +         p \<noteq> q |] 
   6.626 +      ==> (Legendre p q) * (Legendre q p) = 
   6.627 +          (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
   6.628 +  by (auto simp add: QRTEMP.QR_short zprime_zOdd_eq_grt_2 [THEN sym] 
   6.629 +                     QRTEMP_def)
   6.630 +
   6.631 +end
     7.1 --- a/src/HOL/NumberTheory/ROOT.ML	Tue Mar 18 18:07:06 2003 +0100
     7.2 +++ b/src/HOL/NumberTheory/ROOT.ML	Thu Mar 20 15:58:25 2003 +0100
     7.3 @@ -1,3 +1,16 @@
     7.4 +(*  Title:      HOL/NumberTheory/ROOT.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Lawrence C Paulson
     7.7 +    Copyright   2003  University of Cambridge
     7.8 +
     7.9 +This directory contains formalized proofs of Wilson's Theorem (by Thomas M
    7.10 +Rasmussen) and of Gauss' law of quadratic reciprocity (by Avigad, Gray and
    7.11 +Kramer).  The latter formalization follows Eisenstein's proof, which is the
    7.12 +one most commonly found in introductory textbooks, and also uses a
    7.13 +trick used David Russinoff with the Boyer-Moore theorem prover.
    7.14 +See his "A mechanical proof of quadratic reciprocity," Journal of Automated
    7.15 +Reasoning 8:3-21, 1992.
    7.16 +*)
    7.17  
    7.18  no_document use_thy "Permutation";
    7.19  no_document use_thy "Primes";
    7.20 @@ -8,3 +21,4 @@
    7.21  use_thy "EulerFermat";
    7.22  use_thy "WilsonRuss";
    7.23  use_thy "WilsonBij";
    7.24 +use_thy "Quadratic_Reciprocity";
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/NumberTheory/Residues.thy	Thu Mar 20 15:58:25 2003 +0100
     8.3 @@ -0,0 +1,187 @@
     8.4 +(*  Title:      HOL/Quadratic_Reciprocity/Residues.thy
     8.5 +    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     8.6 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     8.7 +*)
     8.8 +
     8.9 +header {* Residue Sets *}
    8.10 +
    8.11 +theory Residues = Int2:;
    8.12 +
    8.13 +text{*Note.  This theory is being revised.  See the web page
    8.14 +\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
    8.15 +
    8.16 +(*****************************************************************)
    8.17 +(*                                                               *)
    8.18 +(* Define the residue of a set, the standard residue, quadratic  *)
    8.19 +(* residues, and prove some basic properties.                    *)
    8.20 +(*                                                               *)
    8.21 +(*****************************************************************)
    8.22 +
    8.23 +constdefs
    8.24 +  ResSet      :: "int => int set => bool"
    8.25 +  "ResSet m X == \<forall>y1 y2. (((y1 \<in> X) & (y2 \<in> X) & [y1 = y2] (mod m)) --> 
    8.26 +    y1 = y2)"
    8.27 +
    8.28 +  StandardRes :: "int => int => int"
    8.29 +  "StandardRes m x == x mod m"
    8.30 +
    8.31 +  QuadRes     :: "int => int => bool"
    8.32 +  "QuadRes m x == \<exists>y. ([(y ^ 2) = x] (mod m))"
    8.33 +
    8.34 +  Legendre    :: "int => int => int"      
    8.35 +  "Legendre a p == (if ([a = 0] (mod p)) then 0
    8.36 +                     else if (QuadRes p a) then 1
    8.37 +                     else -1)"
    8.38 +
    8.39 +  SR          :: "int => int set"
    8.40 +  "SR p == {x. (0 \<le> x) & (x < p)}"
    8.41 +
    8.42 +  SRStar      :: "int => int set"
    8.43 +  "SRStar p == {x. (0 < x) & (x < p)}";
    8.44 +
    8.45 +(******************************************************************)
    8.46 +(*                                                                *)
    8.47 +(* Some useful properties of StandardRes                          *)
    8.48 +(*                                                                *)
    8.49 +(******************************************************************)
    8.50 +
    8.51 +subsection {* Properties of StandardRes *}
    8.52 +
    8.53 +lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)";
    8.54 +  by (auto simp add: StandardRes_def zcong_zmod)
    8.55 +
    8.56 +lemma StandardRes_prop2: "0 < m ==> (StandardRes m x1 = StandardRes m x2)
    8.57 +      = ([x1 = x2] (mod m))";
    8.58 +  by (auto simp add: StandardRes_def zcong_zmod_eq)
    8.59 +
    8.60 +lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))";
    8.61 +  by (auto simp add: StandardRes_def zcong_def zdvd_iff_zmod_eq_0)
    8.62 +
    8.63 +lemma StandardRes_prop4: "2 < m 
    8.64 +     ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)";
    8.65 +  by (auto simp add: StandardRes_def zcong_zmod_eq 
    8.66 +                     zmod_zmult_distrib [of x y m])
    8.67 +
    8.68 +lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x";
    8.69 +  by (auto simp add: StandardRes_def pos_mod_sign)
    8.70 +
    8.71 +lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p";
    8.72 +  by (auto simp add: StandardRes_def pos_mod_bound)
    8.73 +
    8.74 +lemma StandardRes_eq_zcong: 
    8.75 +   "(StandardRes m x = 0) = ([x = 0](mod m))";
    8.76 +  by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) 
    8.77 +
    8.78 +(******************************************************************)
    8.79 +(*                                                                *)
    8.80 +(* Some useful stuff relating StandardRes and SRStar and SR       *)
    8.81 +(*                                                                *)
    8.82 +(******************************************************************)
    8.83 +
    8.84 +subsection {* Relations between StandardRes, SRStar, and SR *}
    8.85 +
    8.86 +lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p";
    8.87 +  by (auto simp add: SRStar_def SR_def)
    8.88 +
    8.89 +lemma StandardRes_SR_prop: "x \<in> SR p ==> StandardRes p x = x";
    8.90 +  by (auto simp add: SR_def StandardRes_def mod_pos_pos_trivial)
    8.91 +
    8.92 +lemma StandardRes_SRStar_prop1: "2 < p ==> (StandardRes p x \<in> SRStar p) 
    8.93 +     = (~[x = 0] (mod p))";
    8.94 +  apply (auto simp add: StandardRes_prop3 StandardRes_def
    8.95 +                        SRStar_def pos_mod_bound)
    8.96 +  apply (subgoal_tac "0 < p")
    8.97 +by (drule_tac a = x in pos_mod_sign, arith, simp)
    8.98 +
    8.99 +lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))";
   8.100 +  by (auto simp add: SRStar_def zcong_def zdvd_not_zless)
   8.101 +
   8.102 +lemma StandardRes_SRStar_prop2: "[| 2 < p; p \<in> zprime; x \<in> SRStar p |] 
   8.103 +     ==> StandardRes p (MultInv p x) \<in> SRStar p";
   8.104 +  apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp);
   8.105 +  apply (rule MultInv_prop3)
   8.106 +  apply (auto simp add: SRStar_def zcong_def zdvd_not_zless)
   8.107 +done
   8.108 +
   8.109 +lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x";
   8.110 +  by (auto simp add: SRStar_SR_prop StandardRes_SR_prop)
   8.111 +
   8.112 +lemma StandardRes_SRStar_prop4: "[| p \<in> zprime; 2 < p; x \<in> SRStar p |] 
   8.113 +     ==> StandardRes p x \<in> SRStar p";
   8.114 +  by (frule StandardRes_SRStar_prop3, auto)
   8.115 +
   8.116 +lemma SRStar_mult_prop1: "[| p \<in> zprime; 2 < p; x \<in> SRStar p; y \<in> SRStar p|] 
   8.117 +     ==> (StandardRes p (x * y)):SRStar p";
   8.118 +  apply (frule_tac x = x in StandardRes_SRStar_prop4, auto)
   8.119 +  apply (frule_tac x = y in StandardRes_SRStar_prop4, auto)
   8.120 +  apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
   8.121 +done
   8.122 +
   8.123 +lemma SRStar_mult_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)); 
   8.124 +     x \<in> SRStar p |] 
   8.125 +     ==> StandardRes p (a * MultInv p x) \<in> SRStar p";
   8.126 +  apply (frule_tac x = x in StandardRes_SRStar_prop2, auto)
   8.127 +  apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1)
   8.128 +  apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
   8.129 +done
   8.130 +
   8.131 +lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p - 1";
   8.132 +  by (auto simp add: SRStar_def int_card_bdd_int_set_l_l)
   8.133 +
   8.134 +lemma SRStar_finite: "2 < p ==> finite( SRStar p)";
   8.135 +  by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
   8.136 +
   8.137 +(******************************************************************)
   8.138 +(*                                                                *)
   8.139 +(* Some useful stuff about ResSet and StandardRes                 *)
   8.140 +(*                                                                *)
   8.141 +(******************************************************************)
   8.142 +
   8.143 +subsection {* Properties relating ResSets with StandardRes *}
   8.144 +
   8.145 +lemma aux: "x mod m = y mod m ==> [x = y] (mod m)";
   8.146 +  apply (subgoal_tac "x = y ==> [x = y](mod m)");
   8.147 +  apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)");
   8.148 +  apply (auto simp add: zcong_zmod [of x y m])
   8.149 +done
   8.150 +
   8.151 +lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)";
   8.152 +  apply (auto simp add: ResSet_def StandardRes_def inj_on_def)
   8.153 +  apply (drule_tac m = m in aux, auto)
   8.154 +done
   8.155 +
   8.156 +lemma StandardRes_Sum: "[| finite X; 0 < m |] 
   8.157 +     ==> [setsum f X = setsum (StandardRes m o f) X](mod m)"; 
   8.158 +  apply (rule_tac F = X in finite_induct)
   8.159 +  apply (auto intro!: zcong_zadd simp add: StandardRes_prop1)
   8.160 +done
   8.161 +
   8.162 +lemma SR_pos: "0 < m ==> (StandardRes m ` X) \<subseteq> {x. 0 \<le> x & x < m}";
   8.163 +  by (auto simp add: StandardRes_ubound StandardRes_lbound)
   8.164 +
   8.165 +lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X";
   8.166 +  apply (rule_tac f = "StandardRes m" in finite_imageD) 
   8.167 +  apply (rule_tac B = "{x. (0 :: int) \<le> x & x < m}" in finite_subset);
   8.168 +by (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos)
   8.169 +
   8.170 +lemma mod_mod_is_mod: "[x = x mod m](mod m)";
   8.171 +  by (auto simp add: zcong_zmod)
   8.172 +
   8.173 +lemma StandardRes_prod: "[| finite X; 0 < m |] 
   8.174 +     ==> [gsetprod f X = gsetprod (StandardRes m o f) X] (mod m)";
   8.175 +  apply (rule_tac F = X in finite_induct)
   8.176 +by (auto intro!: zcong_zmult simp add: StandardRes_prop1)
   8.177 +
   8.178 +lemma ResSet_image: "[| 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) |] ==> ResSet m (f ` A)";
   8.179 +  by (auto simp add: ResSet_def)
   8.180 +
   8.181 +(****************************************************************)
   8.182 +(*                                                              *)
   8.183 +(* Property for SRStar                                          *)
   8.184 +(*                                                              *)
   8.185 +(****************************************************************)
   8.186 +
   8.187 +lemma ResSet_SRStar_prop: "ResSet p (SRStar p)";
   8.188 +  by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
   8.189 +
   8.190 +end;
   8.191 \ No newline at end of file
     9.1 --- a/src/HOL/NumberTheory/document/root.tex	Tue Mar 18 18:07:06 2003 +0100
     9.2 +++ b/src/HOL/NumberTheory/document/root.tex	Thu Mar 20 15:58:25 2003 +0100
     9.3 @@ -9,11 +9,39 @@
     9.4  \begin{document}
     9.5  
     9.6  \title{Some results of number theory}
     9.7 -\author{Lawrence C Paulson \\
     9.8 -  Thomas M Rasmussen \\
     9.9 -  Christophe Tabacznyj}
    9.10 +\author{Jeremy Avigad\\
    9.11 +    David Gray\\
    9.12 +    Adam Kramer\\
    9.13 +    Thomas M Rasmussen}
    9.14 +
    9.15  \maketitle
    9.16  
    9.17 +\begin{abstract}
    9.18 +This directory contains formalized proofs of many results of number theory.
    9.19 +The proofs of the Chinese Remainder Theorem and Wilson's Theorem are due to
    9.20 +Rasmussen.  The proof of Gauss's law of quadratic reciprocity is due to
    9.21 +Avigad, Gray and Kramer.  Proofs can be found in most introductory number
    9.22 +theory textbooks; Goldman's \emph{The Queen of Mathematics: a Historically
    9.23 +Motivated Guide to Number Theory} provides some historical context.
    9.24 +
    9.25 +Avigad, Gray and Kramer have also provided library theories dealing with
    9.26 +finite sets and finite sums, divisibility and congruences, parity and
    9.27 +residues.  The authors are engaged in redesigning and polishing these theories
    9.28 +for more serious use.  For the latest information in this respect, please see
    9.29 +the web page \url{http://www.andrew.cmu.edu/~avigad/isabelle}.  Other theories
    9.30 +contain proofs of Euler's criteria, Gauss' lemma, and the law of quadratic
    9.31 +reciprocity.  The formalization follows Eisenstein's proof, which is the one
    9.32 +most commonly found in introductory textbooks; in particular, it follows the
    9.33 +presentation in Niven and Zuckerman, \emph{The Theory of Numbers}.
    9.34 +
    9.35 +To avoid having to count roots of polynomials, however, we relied on a trick
    9.36 +previously used by David Russinoff in formalizing quadratic reciprocity for
    9.37 +the Boyer-Moore theorem prover; see Russinoff, David, ``A mechanical proof
    9.38 +of quadratic reciprocity,'' \emph{Journal of Automated Reasoning} 8:3-21,
    9.39 +1992.  We are grateful to Larry Paulson for calling our attention to this
    9.40 +reference.
    9.41 +\end{abstract}
    9.42 +
    9.43  \tableofcontents
    9.44  
    9.45  \begin{center}