# HG changeset patch
# User paulson
# Date 1048172305 -3600
# Node ID 26e5f5e624f6eb0231ee89a4dd4d5ce72de4dd89
# Parent  cf947d1ec5ffbfb61b3d1c8a09b87cadd2b9f54a
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer

diff -r cf947d1ec5ff -r 26e5f5e624f6 src/HOL/NumberTheory/Euler.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/Euler.thy	Thu Mar 20 15:58:25 2003 +0100
@@ -0,0 +1,345 @@
+(*  Title:      HOL/Quadratic_Reciprocity/Euler.thy
+    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+header {* Euler's criterion *}
+
+theory Euler = Residues + EvenOdd:;
+
+constdefs
+  MultInvPair :: "int => int => int => int set"
+  "MultInvPair a p j == {StandardRes p j, StandardRes p (a * (MultInv p j))}"
+  SetS        :: "int => int => int set set"
+  "SetS        a p   ==  ((MultInvPair a p) ` (SRStar p))";
+
+(****************************************************************)
+(*                                                              *)
+(* Property for MultInvPair                                     *)
+(*                                                              *)
+(****************************************************************)
+
+lemma MultInvPair_prop1a: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p));
+                              X \<in> (SetS a p); Y \<in> (SetS a p);
+                              ~((X \<inter> Y) = {}) |] ==> 
+                           X = Y";
+  apply (auto simp add: SetS_def)
+  apply (drule StandardRes_SRStar_prop1a)+; defer 1;
+  apply (drule StandardRes_SRStar_prop1a)+;
+  apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym)
+  apply (drule notE, rule MultInv_zcong_prop1, auto)
+  apply (drule notE, rule MultInv_zcong_prop2, auto)
+  apply (drule MultInv_zcong_prop2, auto)
+  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
+  apply (drule MultInv_zcong_prop1, auto)
+  apply (drule MultInv_zcong_prop2, auto)
+  apply (drule MultInv_zcong_prop2, auto)
+  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
+done
+
+lemma MultInvPair_prop1b: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p));
+                              X \<in> (SetS a p); Y \<in> (SetS a p);
+                              X \<noteq> Y |] ==>
+                              X \<inter> Y = {}";
+  apply (rule notnotD)
+  apply (rule notI)
+  apply (drule MultInvPair_prop1a, auto)
+done
+
+lemma MultInvPair_prop1c: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)) |] ==>  
+    \<forall>X \<in> SetS a p. \<forall>Y \<in> SetS a p. X \<noteq> Y --> X\<inter>Y = {}"
+  by (auto simp add: MultInvPair_prop1b)
+
+lemma MultInvPair_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)) |] ==> 
+                          Union ( SetS a p) = SRStar p";
+  apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4 
+    SRStar_mult_prop2)
+  apply (frule StandardRes_SRStar_prop3)
+  apply (rule bexI, auto)
+done
+
+lemma MultInvPair_distinct: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); 
+                                ~([j = 0] (mod p)); 
+                                ~(QuadRes p a) |]  ==> 
+                             ~([j = a * MultInv p j] (mod p))";
+  apply auto
+proof -;
+  assume "p \<in> zprime" and "2 < p" and "~([a = 0] (mod p))" and 
+    "~([j = 0] (mod p))" and "~(QuadRes p a)";
+  assume "[j = a * MultInv p j] (mod p)";
+  then have "[j * j = (a * MultInv p j) * j] (mod p)";
+    by (auto simp add: zcong_scalar)
+  then have a:"[j * j = a * (MultInv p j * j)] (mod p)";
+    by (auto simp add: zmult_ac)
+  have "[j * j = a] (mod p)";
+    proof -;
+      from prems have b: "[MultInv p j * j = 1] (mod p)";
+        by (simp add: MultInv_prop2a)
+      from b a show ?thesis;
+        by (auto simp add: zcong_zmult_prop2)
+    qed;
+  then have "[j^2 = a] (mod p)";
+    apply(subgoal_tac "2 = Suc(Suc(0))");
+    apply (erule ssubst)
+    apply (auto simp only: power_Suc power_0)
+    by auto
+  with prems show False;
+    by (simp add: QuadRes_def)
+qed;
+
+lemma MultInvPair_card_two: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); 
+                                ~(QuadRes p a); ~([j = 0] (mod p)) |]  ==> 
+                             card (MultInvPair a p j) = 2";
+  apply (auto simp add: MultInvPair_def)
+  apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))");
+  apply auto
+  apply (simp only: StandardRes_prop2)
+  apply (drule MultInvPair_distinct)
+by auto
+
+(****************************************************************)
+(*                                                              *)
+(* Properties of SetS                                           *)
+(*                                                              *)
+(****************************************************************)
+
+lemma SetS_finite: "2 < p ==> finite (SetS a p)";
+  by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI)
+
+lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X";
+  by (auto simp add: SetS_def MultInvPair_def)
+
+lemma SetS_elems_card: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); 
+                        ~(QuadRes p a) |]  ==>
+                        \<forall>X \<in> SetS a p. card X = 2";
+  apply (auto simp add: SetS_def)
+  apply (frule StandardRes_SRStar_prop1a)
+  apply (rule MultInvPair_card_two, auto)
+done
+
+lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))";
+  by (auto simp add: SetS_finite SetS_elems_finite finite_union_finite_subsets)
+
+lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); 
+    \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S";
+by (induct set: Finites, auto)
+
+lemma SetS_card: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> 
+                  int(card(SetS a p)) = (p - 1) div 2";
+proof -;
+  assume "p \<in> zprime" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)";
+  then have "(p - 1) = 2 * int(card(SetS a p))";
+  proof -;
+    have "p - 1 = int(card(Union (SetS a p)))";
+      by (auto simp add: prems MultInvPair_prop2 SRStar_card)
+    also have "... = int (setsum card (SetS a p))";
+      by (auto simp add: prems SetS_finite SetS_elems_finite
+                         MultInvPair_prop1c [of p a] card_union_disjoint_sets)
+    also have "... = int(setsum (%x.2) (SetS a p))";
+      apply (insert prems)
+      apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite 
+        card_setsum_aux)
+    done
+    also have "... = 2 * int(card( SetS a p))";
+      by (auto simp add: prems SetS_finite setsum_const2)
+    finally show ?thesis .;
+  qed;
+  from this show ?thesis;
+    by auto
+qed;
+
+lemma SetS_setprod_prop: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p));
+                              ~(QuadRes p a); x \<in> (SetS a p) |] ==> 
+                          [setprod x = a] (mod p)";
+  apply (auto simp add: SetS_def MultInvPair_def)
+  apply (frule StandardRes_SRStar_prop1a)
+  apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)");
+  apply (auto simp add: StandardRes_prop2 MultInvPair_distinct)
+  apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in 
+    StandardRes_prop4);
+  apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)");
+  apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and
+                   b = "x * (a * MultInv p x)" and
+                   c = "a * (x * MultInv p x)" in  zcong_trans, force);
+  apply (frule_tac p = p and x = x in MultInv_prop2, auto)
+  apply (drule_tac a = "x * MultInv p x" and b = 1 in zcong_zmult_prop2)
+  apply (auto simp add: zmult_ac)
+done
+
+lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1";
+  by arith
+
+lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)";
+  by auto
+
+lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} \<union> 
+    (d22set (p - 1))";
+  apply (induct p rule: d22set.induct, auto)
+  apply (simp add: SRStar_def d22set.simps, arith)
+  apply (simp add: SRStar_def d22set.simps, clarify)
+  apply (frule aux1)
+  apply (frule aux2, auto)
+  apply (simp_all add: SRStar_def)
+  apply (simp add: d22set.simps)
+  apply (frule d22set_le)
+  apply (frule d22set_g_1, auto)
+done
+
+lemma Union_SetS_setprod_prop1: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
+                                 [setprod (Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)";
+proof -;
+  assume "p \<in> zprime" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)";
+  then have "[setprod (Union (SetS a p)) = 
+      gsetprod setprod (SetS a p)] (mod p)";
+    by (auto simp add: SetS_finite SetS_elems_finite
+                       MultInvPair_prop1c setprod_disj_sets)
+  also; have "[gsetprod setprod (SetS a p) = 
+      gsetprod (%x. a) (SetS a p)] (mod p)";
+    apply (rule gsetprod_same_function_zcong)
+    by (auto simp add: prems SetS_setprod_prop SetS_finite)
+  also (zcong_trans) have "[gsetprod (%x. a) (SetS a p) = 
+      a^(card (SetS a p))] (mod p)";
+    by (auto simp add: prems SetS_finite gsetprod_const)
+  finally (zcong_trans) show ?thesis;
+    apply (rule zcong_trans)
+    apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto);
+    apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force);
+    apply (auto simp add: prems SetS_card)
+  done
+qed;
+
+lemma Union_SetS_setprod_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)) |] ==> 
+                                    setprod (Union (SetS a p)) = zfact (p - 1)";
+proof -;
+  assume "p \<in> zprime" and "2 < p" and "~([a = 0](mod p))";
+  then have "setprod (Union (SetS a p)) = setprod (SRStar p)";
+    by (auto simp add: MultInvPair_prop2)
+  also have "... = setprod ({1} \<union> (d22set (p - 1)))";
+    by (auto simp add: prems SRStar_d22set_prop)
+  also have "... = zfact(p - 1)";
+  proof -;
+     have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))";
+      apply (insert prems, auto)
+      apply (drule d22set_g_1)
+      apply (auto simp add: d22set_fin)
+     done
+     then have "setprod({1} \<union> (d22set (p - 1))) = setprod (d22set (p - 1))";
+       by auto
+     then show ?thesis
+       by (auto simp add: d22set_prod_zfact)
+  qed;
+  finally show ?thesis .;
+qed;
+
+lemma zfact_prop: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
+                   [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)";
+  apply (frule Union_SetS_setprod_prop1) 
+  apply (auto simp add: Union_SetS_setprod_prop2)
+done
+
+(****************************************************************)
+(*                                                              *)
+(*  Prove the first part of Euler's Criterion:                  *)
+(*    ~(QuadRes p x) |] ==>                                     *)
+(*                   [x^(nat (((p) - 1) div 2)) = -1](mod p)    *)
+(*                                                              *)
+(****************************************************************)
+
+lemma Euler_part1: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)); 
+    ~(QuadRes p x) |] ==> 
+      [x^(nat (((p) - 1) div 2)) = -1](mod p)";
+  apply (frule zfact_prop, auto)
+  apply (frule Wilson_Russ)
+  apply (auto simp add: zcong_sym)
+  apply (rule zcong_trans, auto)
+done
+
+(********************************************************************)
+(*                                                                  *)
+(* Prove another part of Euler Criterion:                           *)
+(*        [a = 0] (mod p) ==> [0 = a ^ nat ((p - 1) div 2)] (mod p) *)
+(*                                                                  *)
+(********************************************************************)
+
+lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)";
+proof -;
+  assume "0 < p";
+  then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))";
+    by (auto simp add: diff_add_assoc)
+  also have "... = (a ^ 1) * a ^ (nat(p) - 1)";
+    by (simp only: zpower_zadd_distrib)
+  also have "... = a * a ^ (nat(p) - 1)";
+    by auto
+  finally show ?thesis .;
+qed;
+
+lemma aux_2: "[| (2::int) < p; p \<in> zOdd |] ==> 0 < ((p - 1) div 2)";
+proof -;
+  assume "2 < p" and "p \<in> zOdd";
+  then have "(p - 1):zEven";
+    by (auto simp add: zEven_def zOdd_def)
+  then have aux_1: "2 * ((p - 1) div 2) = (p - 1)";
+    by (auto simp add: even_div_2_prop2)
+  then have "1 < (p - 1)"
+    by auto
+  then have " 1 < (2 * ((p - 1) div 2))";
+    by (auto simp add: aux_1)
+  then have "0 < (2 * ((p - 1) div 2)) div 2";
+    by auto
+  then show ?thesis by auto
+qed;
+
+lemma Euler_part2: "[| 2 < p; p \<in> zprime; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)";
+  apply (frule zprime_zOdd_eq_grt_2)
+  apply (frule aux_2, auto)
+  apply (frule_tac a = a in aux_1, auto)
+  apply (frule zcong_zmult_prop1, auto)
+done
+
+(****************************************************************)
+(*                                                              *)
+(* Prove the final part of Euler's Criterion:                   *)
+(*           QuadRes p x |] ==>                                 *)
+(*                      [x^(nat (((p) - 1) div 2)) = 1](mod p)  *)
+(*                                                              *)
+(****************************************************************)
+
+lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)";
+  apply (subgoal_tac "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> 
+    ~([y ^ 2 = 0] (mod p))");
+  apply (auto simp add: zcong_sym [of "y^2" x p] intro: zcong_trans)
+  apply (auto simp add: zcong_eq_zdvd_prop intro: zpower_zdvd_prop1)
+done
+
+lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))";
+  by (auto simp add: nat_mult_distrib)
+
+lemma Euler_part3: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)); QuadRes p x |] ==> 
+                      [x^(nat (((p) - 1) div 2)) = 1](mod p)";
+  apply (subgoal_tac "p \<in> zOdd")
+  apply (auto simp add: QuadRes_def)
+  apply (frule aux__1, auto)
+  apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower);
+  apply (auto simp add: zpower_zpower)
+  apply (rule zcong_trans)
+  apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"]);
+  apply (simp add: aux__2)
+  apply (frule odd_minus_one_even)
+  apply (frule even_div_2_prop2)
+  apply (auto intro: Little_Fermat simp add: zprime_zOdd_eq_grt_2)
+done
+
+(********************************************************************)
+(*                                                                  *)
+(* Finally show Euler's Criterion                                   *)
+(*                                                                  *)
+(********************************************************************)
+
+theorem Euler_Criterion: "[| 2 < p; p \<in> zprime |] ==> [(Legendre a p) =
+    a^(nat (((p) - 1) div 2))] (mod p)";
+  apply (auto simp add: Legendre_def Euler_part2)
+  apply (frule Euler_part3, auto simp add: zcong_sym)
+  apply (frule Euler_part1, auto simp add: zcong_sym)
+done
+
+end;
\ No newline at end of file
diff -r cf947d1ec5ff -r 26e5f5e624f6 src/HOL/NumberTheory/EvenOdd.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/EvenOdd.thy	Thu Mar 20 15:58:25 2003 +0100
@@ -0,0 +1,254 @@
+(*  Title:      HOL/Quadratic_Reciprocity/EvenOdd.thy
+    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+header {*Parity: Even and Odd Integers*}
+
+theory EvenOdd = Int2:;
+
+text{*Note.  This theory is being revised.  See the web page
+\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
+
+constdefs
+  zOdd    :: "int set"
+  "zOdd == {x. \<exists>k. x = 2*k + 1}"
+  zEven   :: "int set"
+  "zEven == {x. \<exists>k. x = 2 * k}"
+
+(***********************************************************)
+(*                                                         *)
+(* Some useful properties about even and odd               *)
+(*                                                         *)
+(***********************************************************)
+
+lemma one_not_even: "~(1 \<in> zEven)";
+  apply (simp add: zEven_def)
+  apply (rule allI, case_tac "k \<le> 0", auto)
+done
+
+lemma even_odd_conj: "~(x \<in> zOdd & x \<in> zEven)";
+  apply (auto simp add: zOdd_def zEven_def)
+  proof -;
+    fix a b;
+    assume "2 * (a::int) = 2 * (b::int) + 1"; 
+    then have "2 * (a::int) - 2 * (b :: int) = 1";
+       by arith
+    then have "2 * (a - b) = 1";
+       by (auto simp add: zdiff_zmult_distrib)
+    moreover have "(2 * (a - b)):zEven";
+       by (auto simp only: zEven_def)
+    ultimately show "False";
+       by (auto simp add: one_not_even)
+  qed;
+
+lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)";
+  apply (auto simp add: zOdd_def zEven_def)
+  proof -;
+    assume "\<forall>k. x \<noteq> 2 * k";
+    have "0 \<le> (x mod 2) & (x mod 2) < 2";
+      by (auto intro: pos_mod_sign pos_mod_bound)
+    then have "x mod 2 = 0 | x mod 2 = 1" by arith
+    moreover from prems have "x mod 2 \<noteq> 0" by auto
+    ultimately have "x mod 2 = 1" by auto
+    thus "\<exists>k. x = 2 * k + 1";
+      by (insert zmod_zdiv_equality [of "x" "2"], auto)
+  qed;
+
+lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven";
+  by (insert even_odd_disj, auto)
+
+lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \<in> zOdd";
+  apply (case_tac "x \<in> zOdd", auto)
+  apply (drule not_odd_impl_even)
+  apply (auto simp add: zEven_def zOdd_def)
+  proof -;
+    fix a b; 
+    assume "2 * a * y = 2 * b + 1";
+    then have "2 * a * y - 2 * b = 1";
+      by arith
+    then have "2 * (a * y - b) = 1";
+      by (auto simp add: zdiff_zmult_distrib)
+    moreover have "(2 * (a * y - b)):zEven";
+       by (auto simp only: zEven_def)
+    ultimately show "False";
+       by (auto simp add: one_not_even)
+  qed;
+
+lemma odd_minus_one_even: "x \<in> zOdd ==> (x - 1):zEven";
+  by (auto simp add: zOdd_def zEven_def)
+
+lemma even_div_2_prop1: "x \<in> zEven ==> (x mod 2) = 0";
+  by (auto simp add: zEven_def)
+
+lemma even_div_2_prop2: "x \<in> zEven ==> (2 * (x div 2)) = x";
+  by (auto simp add: zEven_def)
+
+lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven";
+  apply (auto simp add: zEven_def)
+  by (auto simp only: zadd_zmult_distrib2 [THEN sym])
+
+lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven";
+  by (auto simp add: zEven_def)
+
+lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven";
+  apply (auto simp add: zEven_def)
+  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
+
+lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven";
+  apply (auto simp add: zOdd_def zEven_def)
+  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
+
+lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd";
+  apply (auto simp add: zOdd_def zEven_def)
+  apply (rule_tac x = "k - ka - 1" in exI)
+  by auto
+
+lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd";
+  apply (auto simp add: zOdd_def zEven_def)
+  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
+
+lemma odd_times_odd: "[| x \<in> zOdd;  y \<in> zOdd |] ==> x * y \<in> zOdd";
+  apply (auto simp add: zOdd_def zadd_zmult_distrib zadd_zmult_distrib2)
+  apply (rule_tac x = "2 * ka * k + ka + k" in exI)
+  by (auto simp add: zadd_zmult_distrib)
+
+lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))";
+  by (insert even_odd_conj even_odd_disj, auto)
+
+lemma even_product: "x * y \<in> zEven ==> x \<in> zEven | y \<in> zEven"; 
+  by (insert odd_iff_not_even odd_times_odd, auto)
+
+lemma even_diff: "x - y \<in> zEven = ((x \<in> zEven) = (y \<in> zEven))";
+  apply (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
+     even_minus_odd odd_minus_even)
+  proof -;
+    assume "x - y \<in> zEven" and "x \<in> zEven";
+    show "y \<in> zEven";
+    proof (rule classical);
+      assume "~(y \<in> zEven)"; 
+      then have "y \<in> zOdd" 
+        by (auto simp add: odd_iff_not_even)
+      with prems have "x - y \<in> zOdd";
+        by (simp add: even_minus_odd)
+      with prems have "False"; 
+        by (auto simp add: odd_iff_not_even)
+      thus ?thesis;
+        by auto
+    qed;
+    next assume "x - y \<in> zEven" and "y \<in> zEven"; 
+    show "x \<in> zEven";
+    proof (rule classical);
+      assume "~(x \<in> zEven)"; 
+      then have "x \<in> zOdd" 
+        by (auto simp add: odd_iff_not_even)
+      with prems have "x - y \<in> zOdd";
+        by (simp add: odd_minus_even)
+      with prems have "False"; 
+        by (auto simp add: odd_iff_not_even)
+      thus ?thesis;
+        by auto
+    qed;
+  qed;
+
+lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1";
+proof -;
+  assume "x \<in> zEven" and "0 \<le> x";
+  then have "\<exists>k. x = 2 * k";
+    by (auto simp only: zEven_def)
+  then show ?thesis;
+    proof;
+      fix a;
+      assume "x = 2 * a";
+      from prems have a: "0 \<le> a";
+        by arith
+      from prems have "nat x = nat(2 * a)";
+        by auto
+      also from a have "nat (2 * a) = 2 * nat a";
+        by (auto simp add: nat_mult_distrib)
+      finally have "(-1::int)^nat x = (-1)^(2 * nat a)";
+        by auto
+      also have "... = ((-1::int)^2)^ (nat a)";
+        by (auto simp add: zpower_zpower [THEN sym])
+      also have "(-1::int)^2 = 1";
+        by auto
+      finally; show ?thesis;
+        by (auto simp add: zpower_1)
+    qed;
+qed;
+
+lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1";
+proof -;
+  assume "x \<in> zOdd" and "0 \<le> x";
+  then have "\<exists>k. x = 2 * k + 1";
+    by (auto simp only: zOdd_def)
+  then show ?thesis;
+    proof;
+      fix a;
+      assume "x = 2 * a + 1";
+      from prems have a: "0 \<le> a";
+        by arith
+      from prems have "nat x = nat(2 * a + 1)";
+        by auto
+      also from a have "nat (2 * a + 1) = 2 * nat a + 1";
+        by (auto simp add: nat_mult_distrib nat_add_distrib)
+      finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)";
+        by auto
+      also have "... = ((-1::int)^2)^ (nat a) * (-1)^1";
+        by (auto simp add: zpower_zpower [THEN sym] zpower_zadd_distrib)
+      also have "(-1::int)^2 = 1";
+        by auto
+      finally; show ?thesis;
+        by (auto simp add: zpower_1)
+    qed;
+qed;
+
+lemma neg_one_power_parity: "[| 0 \<le> x; 0 \<le> y; (x \<in> zEven) = (y \<in> zEven) |] ==> 
+  (-1::int)^(nat x) = (-1::int)^(nat y)";
+  apply (insert even_odd_disj [of x])
+  apply (insert even_odd_disj [of y])
+  by (auto simp add: neg_one_even_power neg_one_odd_power)
+
+lemma one_not_neg_one_mod_m: "2 < m ==> ~([1 = -1] (mod m))";
+  by (auto simp add: zcong_def zdvd_not_zless)
+
+lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2";
+  apply (auto simp only: zEven_def)
+  proof -;
+    fix k assume "x < 2 * k";
+    then have "x div 2 < k" by (auto simp add: div_prop1)
+    also have "k = (2 * k) div 2"; by auto
+    finally show "x div 2 < 2 * k div 2" by auto
+  qed;
+
+lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2";
+  by (auto simp add: zEven_def, auto simp add: zdiv_zadd1_eq)
+
+lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y";
+  by (auto simp add: zEven_def)
+
+(* An odd prime is greater than 2 *)
+
+lemma zprime_zOdd_eq_grt_2: "p \<in> zprime ==> (p \<in> zOdd) = (2 < p)";
+  apply (auto simp add: zOdd_def zprime_def)
+  apply (drule_tac x = 2 in allE)
+  apply (insert odd_iff_not_even [of p])  
+by (auto simp add: zOdd_def zEven_def)
+
+(* Powers of -1 and parity *)
+
+lemma neg_one_special: "finite A ==> 
+    ((-1 :: int) ^ card A) * (-1 ^ card A) = 1";
+  by (induct set: Finites, auto)
+
+lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1";
+  apply (induct_tac n)
+  by auto
+
+lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |]
+  ==> ((-1::int)^j = (-1::int)^k)";
+  apply (insert neg_one_power [of j])
+  apply (insert neg_one_power [of k])
+  by (auto simp add: one_not_neg_one_mod_m zcong_sym)
+
+end;
diff -r cf947d1ec5ff -r 26e5f5e624f6 src/HOL/NumberTheory/Finite2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/Finite2.thy	Thu Mar 20 15:58:25 2003 +0100
@@ -0,0 +1,425 @@
+(*  Title:      HOL/Quadratic_Reciprocity/Finite2.thy
+    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+header {*Finite Sets and Finite Sums*}
+
+theory Finite2 = Main + IntFact:;
+
+text{*These are useful for combinatorial and number-theoretic counting
+arguments.*}
+
+text{*Note.  This theory is being revised.  See the web page
+\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
+
+(******************************************************************)
+(*                                                                *)
+(* gsetprod: A generalized set product function, for ints only.   *)
+(* Note that "setprod", as defined in IntFact, is equivalent to   *)
+(*   our "gsetprod id".                                           *) 
+(*                                                                *)
+(******************************************************************)
+
+consts
+  gsetprod :: "('a => int) => 'a set => int"
+
+defs
+  gsetprod_def: "gsetprod f A ==  if finite A then fold (op * o f) 1 A else 1";
+
+lemma gsetprod_empty [simp]: "gsetprod f {} = 1";
+  by (auto simp add: gsetprod_def)
+
+lemma gsetprod_insert [simp]: "[| finite A; a \<notin> A |] ==> 
+    gsetprod f (insert a A) = f a * gsetprod f A";
+  by (simp add: gsetprod_def LC_def LC.fold_insert)
+
+(******************************************************************)
+(*                                                                *)
+(* Useful properties of sums and products                         *)
+(*                                                                *)
+(******************************************************************);
+
+subsection {* Useful properties of sums and products *}
+
+lemma setprod_gsetprod_id: "setprod A = gsetprod id A";
+  by (auto simp add: setprod_def gsetprod_def)
+
+lemma setsum_same_function: "[| finite S; \<forall>x \<in> S. f x = g x |] ==> 
+    setsum f S = setsum g S";
+by (induct set: Finites, auto)
+
+lemma gsetprod_same_function: "[| finite S; \<forall>x \<in> S. f x = g x |] ==> 
+  gsetprod f S = gsetprod g S";
+by (induct set: Finites, auto)
+
+lemma setsum_same_function_zcong: 
+   "[| finite S; \<forall>x \<in> S. [f x = g x](mod m) |] 
+     ==> [setsum f S = setsum g S] (mod m)";
+   by (induct set: Finites, auto simp add: zcong_zadd)
+
+lemma gsetprod_same_function_zcong: 
+   "[| finite S; \<forall>x \<in> S. [f x = g x](mod m) |] 
+     ==> [gsetprod f S = gsetprod g S] (mod m)";
+by (induct set: Finites, auto simp add: zcong_zmult)
+
+lemma gsetprod_Un_Int: "finite A ==> finite B
+    ==> gsetprod g (A \<union> B) * gsetprod g (A \<inter> B) = 
+    gsetprod g A * gsetprod g B";
+  apply (induct set: Finites)
+by (auto simp add: Int_insert_left insert_absorb)
+
+lemma gsetprod_Un_disjoint: "[| finite A; finite B; A \<inter> B = {} |] ==> 
+    gsetprod g (A \<union> B) = gsetprod g A * gsetprod g B";
+  apply (subst gsetprod_Un_Int [symmetric])
+by auto
+
+lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)";
+  apply (induct set: Finites)
+by (auto simp add: zadd_zmult_distrib2)
+
+lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = 
+    int(c) * int(card X)";
+  apply (induct set: Finites)
+  apply (auto simp add: zadd_zmult_distrib2)
+done
+
+lemma setsum_minus: "finite A ==> setsum (%x. ((f x)::int) - g x) A = 
+  setsum f A - setsum g A";
+  by (induct set: Finites, auto)
+
+lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = 
+    c * setsum f A";
+  apply (induct set: Finites, auto)
+  by (auto simp only: zadd_zmult_distrib2) 
+
+lemma setsum_non_neg: "[| finite A; \<forall>x \<in> A. (0::int) \<le> f x |] ==>
+    0 \<le>  setsum f A";
+  by (induct set: Finites, auto)
+
+lemma gsetprod_const: "finite X ==> gsetprod (%x. (c :: int)) X = c ^ (card X)";
+  apply (induct set: Finites)
+by auto
+
+(******************************************************************)
+(*                                                                *)
+(* Cardinality of some explicit finite sets                       *)
+(*                                                                *)
+(******************************************************************);
+
+subsection {* Cardinality of explicit finite sets *}
+
+lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B";
+by (simp add: finite_subset finite_imageI)
+
+lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}";
+apply (rule_tac N = "{y. y < x}" and n = x in bounded_nat_set_is_finite)
+by auto
+
+lemma bdd_nat_set_le_finite: "finite { y::nat . y \<le> x  }";
+apply (subgoal_tac "{ y::nat . y \<le> x  } = { y::nat . y < Suc x}")
+by (auto simp add: bdd_nat_set_l_finite)
+
+lemma  bdd_int_set_l_finite: "finite { x::int . 0 \<le> x & x < n}";
+apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq> 
+    int ` {(x :: nat). x < nat n}");
+apply (erule finite_surjI)
+apply (auto simp add: bdd_nat_set_l_finite image_def)
+apply (rule_tac x = "nat x" in exI, simp) 
+done
+
+lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}";
+apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
+apply (erule ssubst)
+apply (rule bdd_int_set_l_finite)
+by auto
+
+lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}";
+apply (subgoal_tac "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}")
+by (auto simp add: bdd_int_set_l_finite finite_subset)
+
+lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}";
+apply (subgoal_tac "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}")
+by (auto simp add: bdd_int_set_le_finite finite_subset)
+
+lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x";
+apply (induct_tac x, force)
+proof -;
+  fix n::nat;
+  assume "card {y. y < n} = n"; 
+  have "{y. y < Suc n} = insert n {y. y < n}";
+    by auto
+  then have "card {y. y < Suc n} = card (insert n {y. y < n})";
+    by auto
+  also have "... = Suc (card {y. y < n})";
+    apply (rule card_insert_disjoint)
+    by (auto simp add: bdd_nat_set_l_finite)
+  finally show "card {y. y < Suc n} = Suc n"; 
+    by (simp add: prems)
+qed;
+
+lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x";
+apply (subgoal_tac "{ y::nat. y \<le> x} = { y::nat. y < Suc x}")
+by (auto simp add: card_bdd_nat_set_l)
+
+lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n";
+proof -;
+  fix n::int;
+  assume "0 \<le> n";
+  have "finite {y. y < nat n}";
+    by (rule bdd_nat_set_l_finite)
+  moreover have "inj_on (%y. int y) {y. y < nat n}";
+    by (auto simp add: inj_on_def)
+  ultimately have "card (int ` {y. y < nat n}) = card {y. y < nat n}";
+    by (rule card_image)
+  also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}";
+    apply (auto simp add: zless_nat_eq_int_zless image_def)
+    apply (rule_tac x = "nat x" in exI)
+    by (auto simp add: nat_0_le)
+  also; have "card {y. y < nat n} = nat n" 
+    by (rule card_bdd_nat_set_l)
+  finally show "card {y. 0 \<le> y & y < n} = nat n"; .;
+qed;
+
+lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} = 
+  nat n + 1";
+apply (subgoal_tac "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}")
+apply (insert card_bdd_int_set_l [of "n+1"])
+by (auto simp add: nat_add_distrib)
+
+lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==> 
+    card {x. 0 < x & x \<le> n} = nat n";
+proof -;
+  fix n::int;
+  assume "0 \<le> n";
+  have "finite {x. 0 \<le> x & x < n}";
+    by (rule bdd_int_set_l_finite)
+  moreover have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}";
+    by (auto simp add: inj_on_def)
+  ultimately have "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) = 
+     card {x. 0 \<le> x & x < n}";
+    by (rule card_image)
+  also from prems have "... = nat n";
+    by (rule card_bdd_int_set_l)
+  also; have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}";
+    apply (auto simp add: image_def)
+    apply (rule_tac x = "x - 1" in exI)
+    by arith
+  finally; show "card {x. 0 < x & x \<le> n} = nat n";.;
+qed;
+
+lemma card_bdd_int_set_l_l: "0 < (n::int) ==> 
+    card {x. 0 < x & x < n} = nat n - 1";
+  apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}")
+  apply (insert card_bdd_int_set_l_le [of "n - 1"])
+  by (auto simp add: nat_diff_distrib)
+
+lemma int_card_bdd_int_set_l_l: "0 < n ==> 
+    int(card {x. 0 < x & x < n}) = n - 1";
+  apply (auto simp add: card_bdd_int_set_l_l)
+  apply (subgoal_tac "Suc 0 \<le> nat n")
+  apply (auto simp add: zdiff_int [THEN sym])
+  apply (subgoal_tac "0 < nat n", arith)
+  by (simp add: zero_less_nat_eq)
+
+lemma int_card_bdd_int_set_l_le: "0 \<le> n ==> 
+    int(card {x. 0 < x & x \<le> n}) = n";
+  by (auto simp add: card_bdd_int_set_l_le)
+
+(******************************************************************)
+(*                                                                *)
+(* Cartesian products of finite sets                              *)
+(*                                                                *)
+(******************************************************************)
+
+subsection {* Cardinality of finite cartesian products *}
+
+lemma insert_Sigma [simp]: "~(A = {}) ==>
+  (insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)";
+  by blast
+
+lemma cartesian_product_finite: "[| finite A; finite B |] ==> 
+    finite (A <*> B)";
+  apply (rule_tac F = A in finite_induct)
+  by auto
+
+lemma cartesian_product_card_a [simp]: "finite A ==> 
+    card({x} <*> A) = card(A)"; 
+  apply (subgoal_tac "inj_on (%y .(x,y)) A");
+  apply (frule card_image, assumption)
+  apply (subgoal_tac "(Pair x ` A) = {x} <*> A");
+  by (auto simp add: inj_on_def)
+
+lemma cartesian_product_card [simp]: "[| finite A; finite B |] ==> 
+  card (A <*> B) = card(A) * card(B)";
+  apply (rule_tac F = A in finite_induct, auto)
+  apply (case_tac "F = {}", force)
+  apply (subgoal_tac "card({x} <*> B \<union> F <*> B) = card({x} <*> B) + 
+    card(F <*> B)");
+  apply simp
+  apply (rule card_Un_disjoint)
+  by auto
+
+(******************************************************************)
+(*                                                                *)
+(* Sums and products over finite sets                             *)
+(*                                                                *)
+(******************************************************************)
+
+subsection {* Reindexing sums and products *}
+
+lemma sum_prop [rule_format]: "finite B ==>
+                  inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B";
+apply (rule finite_induct, assumption, force)
+apply (rule impI, auto)
+apply (simp add: inj_on_def)
+apply (subgoal_tac "f x \<notin> f ` F")
+apply (subgoal_tac "finite (f ` F)");
+apply (auto simp add: setsum_insert)
+by (simp add: inj_on_def) 
+
+lemma sum_prop_id: "finite B ==> inj_on f B ==> 
+    setsum f B = setsum id (f ` B)";
+by (auto simp add: sum_prop id_o)
+
+lemma prod_prop [rule_format]: "finite B ==>
+        inj_on f B --> gsetprod h (f ` B) = gsetprod (h \<circ> f) B";
+  apply (rule finite_induct, assumption, force)
+  apply (rule impI)
+  apply (auto simp add: inj_on_def)
+  apply (subgoal_tac "f x \<notin> f ` F")
+  apply (subgoal_tac "finite (f ` F)");
+by (auto simp add: gsetprod_insert)
+
+lemma prod_prop_id: "[| finite B; inj_on f B |] ==> 
+    gsetprod id (f ` B) = (gsetprod f B)";
+  by (simp add: prod_prop id_o)
+
+subsection {* Lemmas for counting arguments *}
+
+lemma finite_union_finite_subsets: "[| finite A; \<forall>X \<in> A. finite X |] ==> 
+    finite (Union A)";
+apply (induct set: Finites)
+by auto
+
+lemma finite_index_UNION_finite_sets: "finite A ==> 
+    (\<forall>x \<in> A. finite (f x)) --> finite (UNION A f)";
+by (induct_tac rule: finite_induct, auto)
+
+lemma card_union_disjoint_sets: "finite A ==> 
+    ((\<forall>X \<in> A. finite X) & (\<forall>X \<in> A. \<forall>Y \<in> A. X \<noteq> Y --> X \<inter> Y = {})) ==> 
+    card (Union A) = setsum card A";
+  apply auto
+  apply (induct set: Finites, auto)
+  apply (frule_tac B = "Union F" and A = x in card_Un_Int)
+by (auto simp add: finite_union_finite_subsets)
+
+(*
+  We just duplicated something in the standard library: the next lemma 
+  is setsum_UN_disjoint in Finite_Set
+
+lemma setsum_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
+    ((\<forall>x \<in> A. finite (g x)) & 
+    (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
+      setsum f (UNION A g) = setsum (%x. setsum f (g x)) A";
+apply (induct_tac rule: finite_induct)
+apply (assumption, simp, clarify)
+apply (subgoal_tac "g x \<inter> (UNION F g) = {}");
+apply (subgoal_tac "finite (UNION F g)");
+apply (simp add: setsum_Un_disjoint)
+by (auto simp add: finite_index_UNION_finite_sets)
+
+*)
+
+lemma int_card_eq_setsum [rule_format]: "finite A ==> 
+    int (card A) = setsum (%x. 1) A";
+  by (erule finite_induct, auto)
+
+lemma card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
+    ((\<forall>x \<in> A. finite (g x)) & 
+    (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
+      card (UNION A g) = setsum (%x. card (g x)) A";
+apply clarify
+apply (frule_tac f = "%x.(1::nat)" and A = g in 
+    setsum_UN_disjoint);
+apply assumption+;
+apply (subgoal_tac "finite (UNION A g)");
+apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
+apply (auto simp only: card_eq_setsum)
+apply (erule setsum_same_function)
+by (auto simp add: card_eq_setsum)
+
+lemma int_card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
+    ((\<forall>x \<in> A. finite (g x)) & 
+    (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
+       int(card (UNION A g)) = setsum (%x. int( card (g x))) A";
+apply clarify
+apply (frule_tac f = "%x.(1::int)" and A = g in 
+    setsum_UN_disjoint);
+apply assumption+;
+apply (subgoal_tac "finite (UNION A g)");
+apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
+apply (auto simp only: int_card_eq_setsum)
+apply (erule setsum_same_function)
+by (auto simp add: int_card_eq_setsum)
+
+lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
+    g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A";
+apply (frule_tac h = g and f = f in sum_prop, auto)
+apply (subgoal_tac "setsum g B = setsum g (f ` A)");
+apply (simp add: inj_on_def)
+apply (subgoal_tac "card A = card B")
+apply (drule_tac A = "f ` A" and B = B in card_seteq)
+apply (auto simp add: card_image)
+apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
+apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
+by auto
+
+lemma gsetprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
+    g ` B \<subseteq> A; inj_on g B |] ==> gsetprod g B = gsetprod (g \<circ> f) A";
+  apply (frule_tac h = g and f = f in prod_prop, auto) 
+  apply (subgoal_tac "gsetprod g B = gsetprod g (f ` A)"); 
+  apply (simp add: inj_on_def)
+  apply (subgoal_tac "card A = card B")
+  apply (drule_tac A = "f ` A" and B = B in card_seteq)
+  apply (auto simp add: card_image)
+  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
+by (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
+
+lemma setsum_union_disjoint_sets [rule_format]: "finite A ==> 
+    ((\<forall>X \<in> A. finite X) & (\<forall>X \<in> A. \<forall>Y \<in> A. X \<noteq> Y --> X \<inter> Y = {})) 
+    --> setsum f (Union A) = setsum (%x. setsum f x) A";
+apply (induct_tac rule: finite_induct)
+apply (assumption, simp, clarify)
+apply (subgoal_tac "x \<inter> (Union F) = {}");
+apply (subgoal_tac "finite (Union F)");
+  by (auto simp add: setsum_Un_disjoint Union_def)
+
+lemma gsetprod_union_disjoint_sets [rule_format]: "[| 
+    finite (A :: int set set); 
+    (\<forall>X \<in> A. finite (X :: int set));
+    (\<forall>X \<in> A. (\<forall>Y \<in> A. (X :: int set) \<noteq> (Y :: int set) --> 
+      (X \<inter> Y) = {})) |] ==> 
+  ( gsetprod (f :: int => int) (Union A) = gsetprod (%x. gsetprod f x) A)";
+  apply (induct set: Finites)
+  apply (auto simp add: gsetprod_empty) 
+  apply (subgoal_tac "gsetprod f (x \<union> Union F) = 
+    gsetprod f x * gsetprod f (Union F)");
+  apply simp
+  apply (rule gsetprod_Un_disjoint)
+by (auto simp add: gsetprod_Un_disjoint Union_def)
+
+lemma gsetprod_disjoint_sets: "[| finite A;
+    \<forall>X \<in> A. finite X; 
+    \<forall>X \<in> A. \<forall>Y \<in> A. (X \<noteq> Y --> X \<inter> Y = {}) |] ==> 
+  gsetprod id (Union A) = gsetprod (gsetprod id) A";
+  apply (rule_tac f = id in gsetprod_union_disjoint_sets)
+  by auto
+
+lemma setprod_disj_sets: "[| finite (A::int set set);
+    \<forall>X \<in> A. finite X;
+    \<forall>X \<in> A. \<forall>Y \<in> A. (X \<noteq> Y --> X \<inter> Y = {}) |] ==> 
+  setprod (Union A) = gsetprod (%x. setprod x) A";
+  by (auto simp add: setprod_gsetprod_id gsetprod_disjoint_sets)
+
+end;
diff -r cf947d1ec5ff -r 26e5f5e624f6 src/HOL/NumberTheory/Gauss.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/Gauss.thy	Thu Mar 20 15:58:25 2003 +0100
@@ -0,0 +1,510 @@
+(*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy
+    Authors:    Jeremy Avigad, David Gray, and Adam Kramer)
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+header {* Gauss' Lemma *}
+
+theory Gauss = Euler:;
+
+locale GAUSS =
+  fixes p :: "int"
+  fixes a :: "int"
+  fixes A :: "int set"
+  fixes B :: "int set"
+  fixes C :: "int set"
+  fixes D :: "int set"
+  fixes E :: "int set"
+  fixes F :: "int set"
+
+  assumes p_prime: "p \<in> zprime"
+  assumes p_g_2: "2 < p"
+  assumes p_a_relprime: "~[a = 0](mod p)"
+  assumes a_nonzero:    "0 < a"
+
+  defines A_def: "A == {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
+  defines B_def: "B == (%x. x * a) ` A"
+  defines C_def: "C == (StandardRes p) ` B"
+  defines D_def: "D == C \<inter> {x. x \<le> ((p - 1) div 2)}"
+  defines E_def: "E == C \<inter> {x. ((p - 1) div 2) < x}"
+  defines F_def: "F == (%x. (p - x)) ` E";
+
+subsection {* Basic properties of p *}
+
+lemma (in GAUSS) p_odd: "p \<in> zOdd";
+  by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
+
+lemma (in GAUSS) p_g_0: "0 < p";
+  by (insert p_g_2, auto)
+
+lemma (in GAUSS) int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2";
+  by (insert p_g_2, auto simp add: pos_imp_zdiv_nonneg_iff)
+
+lemma (in GAUSS) p_minus_one_l: "(p - 1) div 2 < p";
+  proof -;
+    have "p - 1 = (p - 1) div 1" by auto
+    then have "(p - 1) div 2 \<le> p - 1"
+      apply (rule ssubst) back;
+      apply (rule zdiv_mono2)
+      by (auto simp add: p_g_0)
+    then have "(p - 1) div 2 \<le> p - 1";
+      by auto
+    then show ?thesis by simp
+qed;
+
+lemma (in GAUSS) p_eq: "p = (2 * (p - 1) div 2) + 1";
+  apply (insert zdiv_zmult_self2 [of 2 "p - 1"])
+by auto
+
+lemma zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)";
+  apply (frule odd_minus_one_even)
+  apply (simp add: zEven_def)
+  apply (subgoal_tac "2 \<noteq> 0")
+  apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2)  
+by (auto simp add: even_div_2_prop2)
+
+lemma (in GAUSS) p_eq2: "p = (2 * ((p - 1) div 2)) + 1";
+  apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto)
+by (frule zodd_imp_zdiv_eq, auto)
+
+subsection {* Basic Properties of the Gauss Sets *}
+
+lemma (in GAUSS) finite_A: "finite (A)";
+  apply (auto simp add: A_def) 
+thm bdd_int_set_l_finite;
+  apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}"); 
+by (auto simp add: bdd_int_set_l_finite finite_subset)
+
+lemma (in GAUSS) finite_B: "finite (B)";
+  by (auto simp add: B_def finite_A finite_imageI)
+
+lemma (in GAUSS) finite_C: "finite (C)";
+  by (auto simp add: C_def finite_B finite_imageI)
+
+lemma (in GAUSS) finite_D: "finite (D)";
+  by (auto simp add: D_def finite_Int finite_C)
+
+lemma (in GAUSS) finite_E: "finite (E)";
+  by (auto simp add: E_def finite_Int finite_C)
+
+lemma (in GAUSS) finite_F: "finite (F)";
+  by (auto simp add: F_def finite_E finite_imageI)
+
+lemma (in GAUSS) C_eq: "C = D \<union> E";
+  by (auto simp add: C_def D_def E_def)
+
+lemma (in GAUSS) A_card_eq: "card A = nat ((p - 1) div 2)";
+  apply (auto simp add: A_def) 
+  apply (insert int_nat)
+  apply (erule subst)
+  by (auto simp add: card_bdd_int_set_l_le)
+
+lemma (in GAUSS) inj_on_xa_A: "inj_on (%x. x * a) A";
+  apply (insert a_nonzero)
+by (simp add: A_def inj_on_def)
+
+lemma (in GAUSS) A_res: "ResSet p A";
+  apply (auto simp add: A_def ResSet_def) 
+  apply (rule_tac m = p in zcong_less_eq) 
+  apply (insert p_g_2, auto) 
+  apply (subgoal_tac [1-2] "(p - 1) div 2 < p");
+by (auto, auto simp add: p_minus_one_l)
+
+lemma (in GAUSS) B_res: "ResSet p B";
+  apply (insert p_g_2 p_a_relprime p_minus_one_l)
+  apply (auto simp add: B_def) 
+  apply (rule ResSet_image)
+  apply (auto simp add: A_res) 
+  apply (auto simp add: A_def)
+  proof -;
+    fix x fix y
+    assume a: "[x * a = y * a] (mod p)"
+    assume b: "0 < x"
+    assume c: "x \<le> (p - 1) div 2"
+    assume d: "0 < y"
+    assume e: "y \<le> (p - 1) div 2"
+    from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] 
+        have "[x = y](mod p)";
+      by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) 
+    with zcong_less_eq [of x y p] p_minus_one_l 
+         order_le_less_trans [of x "(p - 1) div 2" p]
+         order_le_less_trans [of y "(p - 1) div 2" p] show "x = y";
+      by (simp add: prems p_minus_one_l p_g_0)
+qed;
+
+lemma (in GAUSS) SR_B_inj: "inj_on (StandardRes p) B";
+  apply (auto simp add: B_def StandardRes_def inj_on_def A_def prems)
+  proof -;
+    fix x fix y
+    assume a: "x * a mod p = y * a mod p"
+    assume b: "0 < x"
+    assume c: "x \<le> (p - 1) div 2"
+    assume d: "0 < y"
+    assume e: "y \<le> (p - 1) div 2"
+    assume f: "x \<noteq> y"
+    from a have "[x * a = y * a](mod p)";
+      by (simp add: zcong_zmod_eq p_g_0)
+    with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] 
+        have "[x = y](mod p)";
+      by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) 
+    with zcong_less_eq [of x y p] p_minus_one_l 
+         order_le_less_trans [of x "(p - 1) div 2" p]
+         order_le_less_trans [of y "(p - 1) div 2" p] have "x = y";
+      by (simp add: prems p_minus_one_l p_g_0)
+    then have False;
+      by (simp add: f)
+    then show "a = 0";
+      by simp
+qed;
+
+lemma (in GAUSS) inj_on_pminusx_E: "inj_on (%x. p - x) E";
+  apply (auto simp add: E_def C_def B_def A_def)
+  apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI);
+by auto
+
+lemma (in GAUSS) A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)";
+  apply (auto simp add: A_def)
+  apply (frule_tac m = p in zcong_not_zero)
+  apply (insert p_minus_one_l)
+by auto
+
+lemma (in GAUSS) A_greater_zero: "x \<in> A ==> 0 < x";
+  by (auto simp add: A_def)
+
+lemma (in GAUSS) B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)";
+  apply (auto simp add: B_def)
+  apply (frule A_ncong_p) 
+  apply (insert p_a_relprime p_prime a_nonzero)
+  apply (frule_tac a = x and b = a in zcong_zprime_prod_zero_contra)
+by (auto simp add: A_greater_zero)
+
+lemma (in GAUSS) B_greater_zero: "x \<in> B ==> 0 < x";
+  apply (insert a_nonzero)
+by (auto simp add: B_def zmult_pos A_greater_zero)
+
+lemma (in GAUSS) C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)";
+  apply (auto simp add: C_def)
+  apply (frule B_ncong_p)
+  apply (subgoal_tac "[x = StandardRes p x](mod p)");
+  defer; apply (simp add: StandardRes_prop1)
+  apply (frule_tac a = x and b = "StandardRes p x" and c = 0 in zcong_trans)
+by auto
+
+lemma (in GAUSS) C_greater_zero: "y \<in> C ==> 0 < y";
+  apply (auto simp add: C_def)
+  proof -;
+    fix x;
+    assume a: "x \<in> B";
+    from p_g_0 have "0 \<le> StandardRes p x";
+      by (simp add: StandardRes_lbound)
+    moreover have "~[x = 0] (mod p)";
+      by (simp add: a B_ncong_p)
+    then have "StandardRes p x \<noteq> 0";
+      by (simp add: StandardRes_prop3)
+    ultimately show "0 < StandardRes p x";
+      by (simp add: order_le_less)
+qed;
+
+lemma (in GAUSS) D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)";
+  by (auto simp add: D_def C_ncong_p)
+
+lemma (in GAUSS) E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)";
+  by (auto simp add: E_def C_ncong_p)
+
+lemma (in GAUSS) F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)";
+  apply (auto simp add: F_def) 
+  proof -;
+    fix x assume a: "x \<in> E" assume b: "[p - x = 0] (mod p)"
+    from E_ncong_p have "~[x = 0] (mod p)";
+      by (simp add: a)
+    moreover from a have "0 < x";
+      by (simp add: a E_def C_greater_zero)
+    moreover from a have "x < p";
+      by (auto simp add: E_def C_def p_g_0 StandardRes_ubound)
+    ultimately have "~[p - x = 0] (mod p)";
+      by (simp add: zcong_not_zero)
+    from this show False by (simp add: b)
+qed;
+
+lemma (in GAUSS) F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}";
+  apply (auto simp add: F_def E_def) 
+  apply (insert p_g_0)
+  apply (frule_tac x = xa in StandardRes_ubound)
+  apply (frule_tac x = x in StandardRes_ubound)
+  apply (subgoal_tac "xa = StandardRes p xa")
+  apply (auto simp add: C_def StandardRes_prop2 StandardRes_prop1)
+  proof -;
+    from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have 
+        "2 * (p - 1) div 2 = 2 * ((p - 1) div 2)";
+      by simp
+    with p_eq2 show " !!x. [| (p - 1) div 2 < StandardRes p x; x \<in> B |]
+         ==> p - StandardRes p x \<le> (p - 1) div 2";
+      by simp
+qed;
+
+lemma (in GAUSS) D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}";
+  by (auto simp add: D_def C_greater_zero)
+
+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))}";
+  by (auto simp add: F_def E_def D_def C_def B_def A_def)
+
+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)}";
+  by (auto simp add: D_def C_def B_def A_def)
+
+lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2";
+  by (auto simp add: D_eq)
+
+lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2";
+  apply (auto simp add: F_eq A_def)
+  proof -;
+    fix y;
+    assume "(p - 1) div 2 < StandardRes p (y * a)";
+    then have "p - StandardRes p (y * a) < p - ((p - 1) div 2)";
+      by arith
+    also from p_eq2 have "... = 2 * ((p - 1) div 2) + 1 - ((p - 1) div 2)"; 
+      by (rule subst, auto)
+    also; have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1";
+      by arith
+    finally show "p - StandardRes p (y * a) \<le> (p - 1) div 2";
+      by (insert zless_add1_eq [of "p - StandardRes p (y * a)" 
+          "(p - 1) div 2"],auto);
+qed;
+
+lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x,p) = 1";
+  apply (insert p_prime p_minus_one_l)
+by (auto simp add: A_def zless_zprime_imp_zrelprime)
+
+lemma (in GAUSS) A_prod_relprime: "zgcd((gsetprod id A),p) = 1";
+  by (insert all_A_relprime finite_A, simp add: all_relprime_prod_relprime)
+
+subsection {* Relationships Between Gauss Sets *}
+
+lemma (in GAUSS) B_card_eq_A: "card B = card A";
+  apply (insert finite_A)
+by (simp add: finite_A B_def inj_on_xa_A card_image)
+
+lemma (in GAUSS) B_card_eq: "card B = nat ((p - 1) div 2)";
+  by (auto simp add: B_card_eq_A A_card_eq)
+
+lemma (in GAUSS) F_card_eq_E: "card F = card E";
+  apply (insert finite_E)
+by (simp add: F_def inj_on_pminusx_E card_image)
+
+lemma (in GAUSS) C_card_eq_B: "card C = card B";
+  apply (insert finite_B)
+  apply (subgoal_tac "inj_on (StandardRes p) B");
+  apply (simp add: B_def C_def card_image)
+  apply (rule StandardRes_inj_on_ResSet)
+by (simp add: B_res)
+
+lemma (in GAUSS) D_E_disj: "D \<inter> E = {}";
+  by (auto simp add: D_def E_def)
+
+lemma (in GAUSS) C_card_eq_D_plus_E: "card C = card D + card E";
+  by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
+
+lemma (in GAUSS) C_prod_eq_D_times_E: "gsetprod id E * gsetprod id D = gsetprod id C";
+  apply (insert D_E_disj finite_D finite_E C_eq)
+  apply (frule gsetprod_Un_disjoint [of D E id])
+by auto
+
+lemma (in GAUSS) C_B_zcong_prod: "[gsetprod id C = gsetprod id B] (mod p)";
+thm gsetprod_same_function_zcong;  
+  apply (auto simp add: C_def)
+  apply (insert finite_B SR_B_inj) 
+  apply (frule_tac f = "StandardRes p" in prod_prop_id, auto) 
+  apply (rule gsetprod_same_function_zcong)
+by (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
+
+lemma (in GAUSS) F_Un_D_subset: "(F \<union> D) \<subseteq> A";
+  apply (rule Un_least)
+by (auto simp add: A_def F_subset D_subset)
+
+lemma two_eq: "2 * (x::int) = x + x";
+  by arith
+
+lemma (in GAUSS) F_D_disj: "(F \<inter> D) = {}";
+  apply (simp add: F_eq D_eq)
+  apply (auto simp add: F_eq D_eq)
+  proof -;
+    fix y; fix ya;
+    assume "p - StandardRes p (y * a) = StandardRes p (ya * a)";
+    then have "p = StandardRes p (y * a) + StandardRes p (ya * a)";
+      by arith
+    moreover have "p dvd p";
+      by auto
+    ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))";
+      by auto
+    then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)";
+      by (auto simp add: zcong_def)
+    have "[y * a = StandardRes p (y * a)] (mod p)";
+      by (simp only: zcong_sym StandardRes_prop1)
+    moreover have "[ya * a = StandardRes p (ya * a)] (mod p)";
+      by (simp only: zcong_sym StandardRes_prop1)
+    ultimately have "[y * a + ya * a = 
+        StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)";
+      by (rule zcong_zadd)
+    with a have "[y * a + ya * a = 0] (mod p)";
+      apply (elim zcong_trans)
+      by (simp only: zcong_refl)
+    also have "y * a + ya * a = a * (y + ya)";
+      by (simp add: zadd_zmult_distrib2 zmult_commute)
+    finally have "[a * (y + ya) = 0] (mod p)";.;
+    with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
+        p_a_relprime
+        have a: "[y + ya = 0] (mod p)";
+      by auto
+    assume b: "y \<in> A" and c: "ya: A";
+    with A_def have "0 < y + ya";
+      by auto
+    moreover from b c A_def have "y + ya \<le> (p - 1) div 2 + (p - 1) div 2";
+      by auto 
+    moreover from b c p_eq2 A_def have "y + ya < p";
+      by auto
+    ultimately show False;
+      apply simp
+      apply (frule_tac m = p in zcong_not_zero)
+      by (auto simp add: a)
+qed;
+
+lemma (in GAUSS) F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)";
+  apply (insert F_D_disj finite_F finite_D)
+  proof -;
+    have "card (F \<union> D) = card E + card D";
+      by (auto simp add: finite_F finite_D F_D_disj 
+                         card_Un_disjoint F_card_eq_E)
+    then have "card (F \<union> D) = card C";
+      by (simp add: C_card_eq_D_plus_E)
+    from this show "card (F \<union> D) = nat ((p - 1) div 2)"; 
+      by (simp add: C_card_eq_B B_card_eq)
+qed;
+
+lemma (in GAUSS) F_Un_D_eq_A: "F \<union> D = A";
+  apply (insert finite_A F_Un_D_subset A_card_eq F_Un_D_card) 
+by (auto simp add: card_seteq)
+
+lemma (in GAUSS) prod_D_F_eq_prod_A: 
+    "(gsetprod id D) * (gsetprod id F) = gsetprod id A";
+  apply (insert F_D_disj finite_D finite_F)
+  apply (frule gsetprod_Un_disjoint [of F D id])
+by (auto simp add: F_Un_D_eq_A)
+
+lemma (in GAUSS) prod_F_zcong:
+    "[gsetprod id F = ((-1) ^ (card E)) * (gsetprod id E)] (mod p)";
+  proof -;
+    have "gsetprod id F = gsetprod id (op - p ` E)";
+      by (auto simp add: F_def)
+    then have "gsetprod id F = gsetprod (op - p) E";
+      apply simp
+      apply (insert finite_E inj_on_pminusx_E)
+      by (frule_tac f = "op - p" in prod_prop_id, auto)
+    then have one: 
+      "[gsetprod id F = gsetprod (StandardRes p o (op - p)) E] (mod p)";
+      apply simp
+      apply (insert p_g_0 finite_E)
+      by (auto simp add: StandardRes_prod)
+    moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)";
+      apply clarify
+      apply (insert zcong_id [of p])
+      by (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
+    moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)";
+      apply clarify
+      by (simp add: StandardRes_prop1 zcong_sym)
+    moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)";
+      apply clarify
+      apply (insert a b)
+      by (rule_tac b = "p - x" in zcong_trans, auto)
+    ultimately have c:
+      "[gsetprod (StandardRes p o (op - p)) E = gsetprod (uminus) E](mod p)";
+      apply simp
+      apply (insert finite_E p_g_0)
+      by (frule gsetprod_same_function_zcong [of E "StandardRes p o (op - p)"
+                                                     uminus p], auto);
+    then have two: "[gsetprod id F = gsetprod (uminus) E](mod p)";
+      apply (insert one c)
+      by (rule zcong_trans [of "gsetprod id F" 
+                               "gsetprod (StandardRes p o op - p) E" p
+                               "gsetprod uminus E"], auto); 
+    also have "gsetprod uminus E = (gsetprod id E) * (-1)^(card E)"; 
+      apply (insert finite_E)
+      by (induct set: Finites, auto)
+    then have "gsetprod uminus E = (-1) ^ (card E) * (gsetprod id E)";
+      by (simp add: zmult_commute)
+    with two show ?thesis
+      by simp
+qed;
+
+subsection {* Gauss' Lemma *}
+
+lemma (in GAUSS) aux: "gsetprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = gsetprod id A * a ^ card A";
+  by (auto simp add: finite_E neg_one_special)
+
+theorem (in GAUSS) pre_gauss_lemma:
+    "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)";
+  proof -;
+    have "[gsetprod id A = gsetprod id F * gsetprod id D](mod p)";
+      by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
+    then have "[gsetprod id A = ((-1)^(card E) * gsetprod id E) * 
+        gsetprod id D] (mod p)";
+      apply (rule zcong_trans)
+      by (auto simp add: prod_F_zcong zcong_scalar)
+    then have "[gsetprod id A = ((-1)^(card E) * gsetprod id C)] (mod p)";
+      apply (rule zcong_trans)
+      apply (insert C_prod_eq_D_times_E, erule subst)
+      by (subst zmult_assoc, auto)
+    then have "[gsetprod id A = ((-1)^(card E) * gsetprod id B)] (mod p)"
+      apply (rule zcong_trans)
+      by (simp add: C_B_zcong_prod zcong_scalar2)
+    then have "[gsetprod id A = ((-1)^(card E) *
+        (gsetprod id ((%x. x * a) ` A)))] (mod p)";
+      by (simp add: B_def)
+    then have "[gsetprod id A = ((-1)^(card E) * (gsetprod (%x. x * a) A))] 
+        (mod p)";
+      apply (rule zcong_trans)
+      by (simp add: finite_A inj_on_xa_A prod_prop_id zcong_scalar2)
+    moreover have "gsetprod (%x. x * a) A = 
+        gsetprod (%x. a) A * gsetprod id A";
+      by (insert finite_A, induct set: Finites, auto)
+    ultimately have "[gsetprod id A = ((-1)^(card E) * (gsetprod (%x. a) A * 
+        gsetprod id A))] (mod p)";
+      by simp 
+    then have "[gsetprod id A = ((-1)^(card E) * a^(card A) * 
+        gsetprod id A)](mod p)";
+      apply (rule zcong_trans)
+      by (simp add: zcong_scalar2 zcong_scalar finite_A gsetprod_const
+        zmult_assoc)
+    then have a: "[gsetprod id A * (-1)^(card E) = 
+        ((-1)^(card E) * a^(card A) * gsetprod id A * (-1)^(card E))](mod p)";
+      by (rule zcong_scalar)
+    then have "[gsetprod id A * (-1)^(card E) = gsetprod id A * 
+        (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)";
+      apply (rule zcong_trans)
+      by (simp add: a zmult_commute zmult_left_commute)
+    then have "[gsetprod id A * (-1)^(card E) = gsetprod id A * 
+        a^(card A)](mod p)";
+      apply (rule zcong_trans)
+      by (simp add: aux)
+    with this zcong_cancel2 [of p "gsetprod id A" "-1 ^ card E" "a ^ card A"]
+         p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)";
+       by (simp add: order_less_imp_le)
+    from this show ?thesis
+      by (simp add: A_card_eq zcong_sym)
+qed;
+
+theorem (in GAUSS) gauss_lemma: "(Legendre a p) = (-1) ^ (card E)";
+proof -;
+  from Euler_Criterion p_prime p_g_2 have
+    "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)";
+    by auto
+  moreover note pre_gauss_lemma;
+  ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)";
+    by (rule zcong_trans)
+  moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)";
+    by (auto simp add: Legendre_def)
+  moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1";
+    by (rule neg_one_power)
+  ultimately show ?thesis;
+    by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym)
+qed;
+
+end;
\ No newline at end of file
diff -r cf947d1ec5ff -r 26e5f5e624f6 src/HOL/NumberTheory/Int2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/Int2.thy	Thu Mar 20 15:58:25 2003 +0100
@@ -0,0 +1,310 @@
+(*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy
+    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+header {*Integers: Divisibility and Congruences*}
+
+theory Int2 = Finite2 + WilsonRuss:;
+
+text{*Note.  This theory is being revised.  See the web page
+\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
+
+constdefs
+  MultInv :: "int => int => int" 
+  "MultInv p x == x ^ nat (p - 2)";
+
+(*****************************************************************)
+(*                                                               *)
+(* Useful lemmas about dvd and powers                            *)
+(*                                                               *)
+(*****************************************************************)
+
+lemma zpower_zdvd_prop1 [rule_format]: "((0 < n) & (p dvd y)) --> 
+    p dvd ((y::int) ^ n)";
+  by (induct_tac n, auto simp add: zdvd_zmult zdvd_zmult2 [of p y])
+
+lemma zdvd_bounds: "n dvd m ==> (m \<le> (0::int) | n \<le> m)";
+proof -;
+  assume "n dvd m";
+  then have "~(0 < m & m < n)";
+    apply (insert zdvd_not_zless [of m n])
+    by (rule contrapos_pn, auto)
+  then have "(~0 < m | ~m < n)"  by auto
+  then show ?thesis by auto
+qed;
+
+lemma aux4: " -(m * n) = (-m) * (n::int)";
+  by auto
+
+lemma zprime_zdvd_zmult_better: "[| p \<in> zprime;  p dvd (m * n) |] ==> 
+    (p dvd m) | (p dvd n)";
+  apply (case_tac "0 \<le> m")
+  apply (simp add: zprime_zdvd_zmult)
+  by (insert zprime_zdvd_zmult [of "-m" p n], auto)
+
+lemma zpower_zdvd_prop2 [rule_format]: "p \<in> zprime --> p dvd ((y::int) ^ n) 
+    --> 0 < n --> p dvd y";
+  apply (induct_tac n, auto)
+  apply (frule zprime_zdvd_zmult_better, auto)
+done
+
+lemma stupid: "(0 :: int) \<le> y ==> x \<le> x + y";
+  by arith
+
+lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y";
+proof -;
+  assume "0 < z";
+  then have "(x div z) * z \<le> (x div z) * z + x mod z";
+  apply (rule_tac x = "x div z * z" in stupid)
+  by (simp add: pos_mod_sign)
+  also have "... = x";
+    by (auto simp add: zmod_zdiv_equality [THEN sym] zmult_ac)
+  also assume  "x < y * z";
+  finally show ?thesis;
+    by (auto simp add: prems zmult_zless_cancel2, insert prems, arith)
+qed;
+
+lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y";
+proof -;
+  assume "0 < z" and "x < (y * z) + z";
+  then have "x < (y + 1) * z" by (auto simp add: int_distrib)
+  then have "x div z < y + 1";
+    by (rule_tac y = "y + 1" in div_prop1, auto simp add: prems)
+  then show ?thesis by auto
+qed;
+
+lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)";
+proof-;
+  assume "0 < y";
+  from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto
+  moreover have "0 \<le> x mod y";
+    by (auto simp add: prems pos_mod_sign)
+  ultimately show ?thesis;
+    by arith
+qed;
+
+(*****************************************************************)
+(*                                                               *)
+(* Useful properties of congruences                              *)
+(*                                                               *)
+(*****************************************************************)
+
+lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)";
+  by (auto simp add: zcong_def)
+
+lemma zcong_id: "[m = 0] (mod m)";
+  by (auto simp add: zcong_def zdvd_0_right)
+
+lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)";
+  by (auto simp add: zcong_refl zcong_zadd)
+
+lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)";
+  by (induct_tac z, auto simp add: zcong_zmult)
+
+lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==> 
+    [a = d](mod m)";
+  by (auto, rule_tac b = c in zcong_trans)
+
+lemma aux1: "a - b = (c::int) ==> a = c + b";
+  by auto
+
+lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) = 
+    [c = b * d] (mod m))";
+  apply (auto simp add: zcong_def dvd_def)
+  apply (rule_tac x = "ka + k * d" in exI)
+  apply (drule aux1)+;
+  apply (auto simp add: int_distrib)
+  apply (rule_tac x = "ka - k * d" in exI)
+  apply (drule aux1)+;
+  apply (auto simp add: int_distrib)
+done
+
+lemma zcong_zmult_prop2: "[a = b](mod m) ==> 
+    ([c = d * a](mod m) = [c = d * b] (mod m))";
+  by (auto simp add: zmult_ac zcong_zmult_prop1)
+
+lemma zcong_zmult_prop3: "[|p \<in> zprime; ~[x = 0] (mod p); 
+    ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)";
+  apply (auto simp add: zcong_def)
+  apply (drule zprime_zdvd_zmult_better, auto)
+done
+
+lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m); 
+    x < m; y < m |] ==> x = y";
+  apply (simp add: zcong_zmod_eq)
+  apply (subgoal_tac "(x mod m) = x");
+  apply (subgoal_tac "(y mod m) = y");
+  apply simp
+  apply (rule_tac [1-2] mod_pos_pos_trivial)
+by auto
+
+lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==> 
+    ~([x = 1] (mod p))";
+proof;
+  assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
+  then have "[1 = -1] (mod p)";
+    apply (auto simp add: zcong_sym)
+    apply (drule zcong_trans, auto)
+  done
+  then have "[1 + 1 = -1 + 1] (mod p)";
+    by (simp only: zcong_shift)
+  then have "[2 = 0] (mod p)";
+    by auto
+  then have "p dvd 2";
+    by (auto simp add: dvd_def zcong_def)
+  with prems show False;
+    by (auto simp add: zdvd_not_zless)
+qed;
+
+lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)";
+  by (auto simp add: zcong_def)
+
+lemma zcong_zprime_prod_zero: "[| p \<in> zprime; 0 < a |] ==> 
+  [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)"; 
+  by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult)
+
+lemma zcong_zprime_prod_zero_contra: "[| p \<in> zprime; 0 < a |] ==>
+  ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)";
+  apply auto 
+  apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero)
+by auto
+
+lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)"; 
+  by (auto simp add: zcong_zero_equiv_div zdvd_not_zless)
+
+lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0";
+  apply (drule order_le_imp_less_or_eq, auto)
+by (frule_tac m = m in zcong_not_zero, auto)
+
+lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |]
+    ==> zgcd (gsetprod id A,y) = 1";
+  by (induct set: Finites, auto simp add: zgcd_zgcd_zmult)
+
+(*****************************************************************)
+(*                                                               *)
+(* Some properties of MultInv                                    *)
+(*                                                               *)
+(*****************************************************************)
+
+lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> 
+    [(MultInv p x) = (MultInv p y)] (mod p)";
+  by (auto simp add: MultInv_def zcong_zpower)
+
+lemma MultInv_prop2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
+  [(x * (MultInv p x)) = 1] (mod p)";
+proof (simp add: MultInv_def zcong_eq_zdvd_prop);
+  assume "2 < p" and "p \<in> zprime" and "~ p dvd x";
+  have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)";
+    by auto
+  also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)";
+    by (simp only: nat_add_distrib, auto)
+  also have "p - 2 + 1 = p - 1" by arith
+  finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)";
+    by (rule ssubst, auto)
+  also from prems have "[x ^ nat (p - 1) = 1] (mod p)";
+    by (auto simp add: Little_Fermat) 
+  finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)";.;
+qed;
+
+lemma MultInv_prop2a: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
+    [(MultInv p x) * x = 1] (mod p)";
+  by (auto simp add: MultInv_prop2 zmult_ac)
+
+lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))";
+  by (simp add: nat_diff_distrib)
+
+lemma aux_2: "2 < p ==> 0 < nat (p - 2)";
+  by auto
+
+lemma MultInv_prop3: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
+    ~([MultInv p x = 0](mod p))";
+  apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1)
+  apply (drule aux_2)
+  apply (drule zpower_zdvd_prop2, auto)
+done
+
+lemma aux__1: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==> 
+    [(MultInv p (MultInv p x)) = (x * (MultInv p x) * 
+      (MultInv p (MultInv p x)))] (mod p)";
+  apply (drule MultInv_prop2, auto)
+  apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto);
+  apply (auto simp add: zcong_sym)
+done
+
+lemma aux__2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==>
+    [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)";
+  apply (frule MultInv_prop3, auto)
+  apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
+  apply (drule MultInv_prop2, auto)
+  apply (drule_tac k = x in zcong_scalar2, auto)
+  apply (auto simp add: zmult_ac)
+done
+
+lemma MultInv_prop4: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
+    [(MultInv p (MultInv p x)) = x] (mod p)";
+  apply (frule aux__1, auto)
+  apply (drule aux__2, auto)
+  apply (drule zcong_trans, auto)
+done
+
+lemma MultInv_prop5: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)); 
+    ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> 
+    [x = y] (mod p)";
+  apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and 
+    m = p and k = x in zcong_scalar)
+  apply (insert MultInv_prop2 [of p x], simp)
+  apply (auto simp only: zcong_sym [of "MultInv p x * x"])
+  apply (auto simp add:  zmult_ac)
+  apply (drule zcong_trans, auto)
+  apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto)
+  apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac)
+  apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
+  apply (auto simp add: zcong_sym)
+done
+
+lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> 
+    [a * MultInv p j = a * MultInv p k] (mod p)";
+  by (drule MultInv_prop1, auto simp add: zcong_scalar2)
+
+lemma aux___1: "[j = a * MultInv p k] (mod p) ==> 
+    [j * k = a * MultInv p k * k] (mod p)";
+  by (auto simp add: zcong_scalar)
+
+lemma aux___2: "[|2 < p; p \<in> zprime; ~([k = 0](mod p)); 
+    [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)";
+  apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 
+    [of "MultInv p k * k" 1 p "j * k" a])
+  apply (auto simp add: zmult_ac)
+done
+
+lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = 
+     (MultInv p j) * a] (mod p)";
+  by (auto simp add: zmult_assoc zcong_scalar2)
+
+lemma aux___4: "[|2 < p; p \<in> zprime; ~([j = 0](mod p)); 
+    [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
+       ==> [k = a * (MultInv p j)] (mod p)";
+  apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 
+    [of "MultInv p j * j" 1 p "MultInv p j * a" k])
+  apply (auto simp add: zmult_ac zcong_sym)
+done
+
+lemma MultInv_zcong_prop2: "[| 2 < p; p \<in> zprime; ~([k = 0](mod p)); 
+    ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> 
+    [k = a * MultInv p j] (mod p)";
+  apply (drule aux___1)
+  apply (frule aux___2, auto)
+  by (drule aux___3, drule aux___4, auto)
+
+lemma MultInv_zcong_prop3: "[| 2 < p; p \<in> zprime; ~([a = 0](mod p)); 
+    ~([k = 0](mod p)); ~([j = 0](mod p));
+    [a * MultInv p j = a * MultInv p k] (mod p) |] ==> 
+      [j = k] (mod p)";
+  apply (auto simp add: zcong_eq_zdvd_prop [of a p])
+  apply (frule zprime_imp_zrelprime, auto)
+  apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto)
+  apply (drule MultInv_prop5, auto)
+done
+
+end
diff -r cf947d1ec5ff -r 26e5f5e624f6 src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Thu Mar 20 15:58:25 2003 +0100
@@ -0,0 +1,628 @@
+(*  Title:      HOL/Quadratic_Reciprocity/Quadratic_Reciprocity.thy
+    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+header {* The law of Quadratic reciprocity *}
+
+theory Quadratic_Reciprocity = Gauss:;
+
+(***************************************************************)
+(*                                                             *)
+(*  Lemmas leading up to the proof of theorem 3.3 in           *)
+(*  Niven and Zuckerman's presentation                         *)
+(*                                                             *)
+(***************************************************************)
+
+lemma (in GAUSS) QRLemma1: "a * setsum id A = 
+  p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E";
+proof -;
+  from finite_A have "a * setsum id A = setsum (%x. a * x) A"; 
+    by (auto simp add: setsum_const_mult id_def)
+  also have "setsum (%x. a * x) = setsum (%x. x * a)"; 
+    by (auto simp add: zmult_commute)
+  also; have "setsum (%x. x * a) A = setsum id B";
+    by (auto simp add: B_def sum_prop_id finite_A inj_on_xa_A)
+  also have "... = setsum (%x. p * (x div p) + StandardRes p x) B";
+    apply (rule setsum_same_function)
+    by (auto simp add: finite_B StandardRes_def zmod_zdiv_equality)
+  also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B";
+    by (rule setsum_addf)
+  also; have "setsum (StandardRes p) B = setsum id C";
+    by (auto simp add: C_def sum_prop_id [THEN sym] finite_B 
+      SR_B_inj)
+  also; from C_eq have "... = setsum id (D \<union> E)";
+    by auto
+  also; from finite_D finite_E have "... = setsum id D + setsum id E";
+    apply (rule setsum_Un_disjoint)
+    by (auto simp add: D_def E_def)
+  also have "setsum (%x. p * (x div p)) B = 
+      setsum ((%x. p * (x div p)) o (%x. (x * a))) A";
+    by (auto simp add: B_def sum_prop finite_A inj_on_xa_A)
+  also have "... = setsum (%x. p * ((x * a) div p)) A";
+    by (auto simp add: o_def)
+  also from finite_A have "setsum (%x. p * ((x * a) div p)) A = 
+    p * setsum (%x. ((x * a) div p)) A";
+    by (auto simp add: setsum_const_mult)
+  finally show ?thesis by arith
+qed;
+
+lemma (in GAUSS) QRLemma2: "setsum id A = p * int (card E) - setsum id E + 
+  setsum id D"; 
+proof -;
+  from F_Un_D_eq_A have "setsum id A = setsum id (D \<union> F)";
+    by (simp add: Un_commute)
+  also from F_D_disj finite_D finite_F have 
+      "... = setsum id D + setsum id F";
+    apply (simp add: Int_commute)
+    by (intro setsum_Un_disjoint) 
+  also from F_def have "F = (%x. (p - x)) ` E";
+    by auto
+  also from finite_E inj_on_pminusx_E have "setsum id ((%x. (p - x)) ` E) =
+      setsum (%x. (p - x)) E";
+    by (auto simp add: sum_prop)
+  also from finite_E have "setsum (op - p) E = setsum (%x. p) E - setsum id E";
+    by (auto simp add: setsum_minus id_def)
+  also from finite_E have "setsum (%x. p) E = p * int(card E)";
+    by (intro setsum_const)
+  finally show ?thesis;
+    by arith
+qed;
+
+lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A = 
+    p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E";
+proof -;
+  have "(a - 1) * setsum id A = a * setsum id A - setsum id A";
+    by (auto simp add: zdiff_zmult_distrib)  
+  also note QRLemma1;
+  also; from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D + 
+     setsum id E - setsum id A = 
+      p * (\<Sum>x \<in> A. x * a div p) + setsum id D + 
+      setsum id E - (p * int (card E) - setsum id E + setsum id D)";
+    by auto
+  also; have "... = p * (\<Sum>x \<in> A. x * a div p) - 
+      p * int (card E) + 2 * setsum id E"; 
+    by arith
+  finally show ?thesis;
+    by (auto simp only: zdiff_zmult_distrib2)
+qed;
+
+lemma (in GAUSS) QRLemma4: "a \<in> zOdd ==> 
+    (setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)";
+proof -;
+  assume a_odd: "a \<in> zOdd";
+  from QRLemma3 have a: "p * (setsum (%x. ((x * a) div p)) A - int(card E)) =
+      (a - 1) * setsum id A - 2 * setsum id E"; 
+    by arith
+  from a_odd have "a - 1 \<in> zEven"
+    by (rule odd_minus_one_even)
+  hence "(a - 1) * setsum id A \<in> zEven";
+    by (rule even_times_either)
+  moreover have "2 * setsum id E \<in> zEven";
+    by (auto simp add: zEven_def)
+  ultimately have "(a - 1) * setsum id A - 2 * setsum id E \<in> zEven"
+    by (rule even_minus_even)
+  with a have "p * (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
+    by simp
+  hence "p \<in> zEven | (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
+    by (rule even_product)
+  with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
+    by (auto simp add: odd_iff_not_even)
+  thus ?thesis;
+    by (auto simp only: even_diff [THEN sym])
+qed;
+
+lemma (in GAUSS) QRLemma5: "a \<in> zOdd ==> 
+   (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))";
+proof -;
+  assume "a \<in> zOdd";
+  from QRLemma4 have
+    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)";..;
+  moreover have "0 \<le> int(card E)";
+    by auto
+  moreover have "0 \<le> setsum (%x. ((x * a) div p)) A";
+    proof (intro setsum_non_neg);
+      from finite_A show "finite A";.;
+      next show "\<forall>x \<in> A. 0 \<le> x * a div p";
+      proof;
+        fix x;
+        assume "x \<in> A";
+        then have "0 \<le> x";
+          by (auto simp add: A_def)
+        with a_nonzero have "0 \<le> x * a";
+          by (auto simp add: int_0_le_mult_iff)
+        with p_g_2 show "0 \<le> x * a div p"; 
+          by (auto simp add: pos_imp_zdiv_nonneg_iff)
+      qed;
+    qed;
+  ultimately have "(-1::int)^nat((int (card E))) =
+      (-1)^nat(((\<Sum>x \<in> A. x * a div p)))";
+    by (intro neg_one_power_parity, auto)
+  also have "nat (int(card E)) = card E";
+    by auto
+  finally show ?thesis;.;
+qed;
+
+lemma MainQRLemma: "[| a \<in> zOdd; 0 < a; ~([a = 0] (mod p));p \<in> zprime; 2 < p;
+  A = {x. 0 < x & x \<le> (p - 1) div 2} |] ==> 
+  (Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))";
+  apply (subst GAUSS.gauss_lemma)
+  apply (auto simp add: GAUSS_def)
+  apply (subst GAUSS.QRLemma5)
+by (auto simp add: GAUSS_def)
+
+(******************************************************************)
+(*                                                                *)
+(* Stuff about S, S1 and S2...                                    *)
+(*                                                                *)
+(******************************************************************)
+
+locale QRTEMP =
+  fixes p     :: "int"
+  fixes q     :: "int"
+  fixes P_set :: "int set"
+  fixes Q_set :: "int set"
+  fixes S     :: "(int * int) set"
+  fixes S1    :: "(int * int) set"
+  fixes S2    :: "(int * int) set"
+  fixes f1    :: "int => (int * int) set"
+  fixes f2    :: "int => (int * int) set"
+
+  assumes p_prime: "p \<in> zprime"
+  assumes p_g_2: "2 < p"
+  assumes q_prime: "q \<in> zprime"
+  assumes q_g_2: "2 < q"
+  assumes p_neq_q:      "p \<noteq> q"
+
+  defines P_set_def: "P_set == {x. 0 < x & x \<le> ((p - 1) div 2) }"
+  defines Q_set_def: "Q_set == {x. 0 < x & x \<le> ((q - 1) div 2) }"
+  defines S_def:     "S     == P_set <*> Q_set"
+  defines S1_def:    "S1    == { (x, y). (x, y):S & ((p * y) < (q * x)) }"
+  defines S2_def:    "S2    == { (x, y). (x, y):S & ((q * x) < (p * y)) }"
+  defines f1_def:    "f1 j  == { (j1, y). (j1, y):S & j1 = j & 
+                                 (y \<le> (q * j) div p) }"
+  defines f2_def:    "f2 j  == { (x, j1). (x, j1):S & j1 = j & 
+                                 (x \<le> (p * j) div q) }";
+
+lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2";
+proof -;
+  from prems have "2 < p" by (simp add: QRTEMP_def)
+  then have "2 \<le> p - 1" by arith
+  then have "2 div 2 \<le> (p - 1) div 2" by (rule zdiv_mono1, auto)
+  then show ?thesis by auto
+qed;
+
+lemma (in QRTEMP) q_fact: "0 < (q - 1) div 2";
+proof -;
+  from prems have "2 < q" by (simp add: QRTEMP_def)
+  then have "2 \<le> q - 1" by arith
+  then have "2 div 2 \<le> (q - 1) div 2" by (rule zdiv_mono1, auto)
+  then show ?thesis by auto
+qed;
+
+lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==> 
+    (p * b \<noteq> q * a)";
+proof;
+  assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2";
+  then have "q dvd (p * b)" by (auto simp add: dvd_def)
+  with q_prime p_g_2 have "q dvd p | q dvd b";
+    by (auto simp add: zprime_zdvd_zmult)
+  moreover have "~ (q dvd p)";
+  proof;
+    assume "q dvd p";
+    with p_prime have "q = 1 | q = p"
+      apply (auto simp add: zprime_def QRTEMP_def)
+      apply (drule_tac x = q and R = False in allE)
+      apply (simp add: QRTEMP_def)    
+      apply (subgoal_tac "0 \<le> q", simp add: QRTEMP_def)
+      apply (insert prems)
+    by (auto simp add: QRTEMP_def)
+    with q_g_2 p_neq_q show False by auto
+  qed;
+  ultimately have "q dvd b" by auto
+  then have "q \<le> b";
+  proof -;
+    assume "q dvd b";
+    moreover from prems have "0 < b" by auto
+    ultimately show ?thesis by (insert zdvd_bounds [of q b], auto)
+  qed;
+  with prems have "q \<le> (q - 1) div 2" by auto
+  then have "2 * q \<le> 2 * ((q - 1) div 2)" by arith
+  then have "2 * q \<le> q - 1";
+  proof -;
+    assume "2 * q \<le> 2 * ((q - 1) div 2)";
+    with prems have "q \<in> zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
+    with odd_minus_one_even have "(q - 1):zEven" by auto
+    with even_div_2_prop2 have "(q - 1) = 2 * ((q - 1) div 2)" by auto
+    with prems show ?thesis by auto
+  qed;
+  then have p1: "q \<le> -1" by arith
+  with q_g_2 show False by auto
+qed;
+
+lemma (in QRTEMP) P_set_finite: "finite (P_set)";
+  by (insert p_fact, auto simp add: P_set_def bdd_int_set_l_le_finite)
+
+lemma (in QRTEMP) Q_set_finite: "finite (Q_set)";
+  by (insert q_fact, auto simp add: Q_set_def bdd_int_set_l_le_finite)
+
+lemma (in QRTEMP) S_finite: "finite S";
+  by (auto simp add: S_def  P_set_finite Q_set_finite cartesian_product_finite)
+
+lemma (in QRTEMP) S1_finite: "finite S1";
+proof -;
+  have "finite S" by (auto simp add: S_finite)
+  moreover have "S1 \<subseteq> S" by (auto simp add: S1_def S_def)
+  ultimately show ?thesis by (auto simp add: finite_subset)
+qed;
+
+lemma (in QRTEMP) S2_finite: "finite S2";
+proof -;
+  have "finite S" by (auto simp add: S_finite)
+  moreover have "S2 \<subseteq> S" by (auto simp add: S2_def S_def)
+  ultimately show ?thesis by (auto simp add: finite_subset)
+qed;
+
+lemma (in QRTEMP) P_set_card: "(p - 1) div 2 = int (card (P_set))";
+  by (insert p_fact, auto simp add: P_set_def card_bdd_int_set_l_le)
+
+lemma (in QRTEMP) Q_set_card: "(q - 1) div 2 = int (card (Q_set))";
+  by (insert q_fact, auto simp add: Q_set_def card_bdd_int_set_l_le)
+
+lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
+  apply (insert P_set_card Q_set_card P_set_finite Q_set_finite)
+  apply (auto simp add: S_def zmult_int)
+done
+
+lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}";
+  by (auto simp add: S1_def S2_def)
+
+lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \<union> S2";
+  apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def)
+  proof -;
+    fix a and b;
+    assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2";
+    with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
+    moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
+    ultimately show "p * b < q * a" by auto
+  qed;
+
+lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) = 
+    int(card(S1)) + int(card(S2))";
+proof-;
+  have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
+    by (auto simp add: S_card)
+  also have "... = int( card(S1) + card(S2))";
+    apply (insert S1_finite S2_finite S1_Int_S2_prop S1_Union_S2_prop)
+    apply (drule card_Un_disjoint, auto)
+  done
+  also have "... = int(card(S1)) + int(card(S2))" by auto
+  finally show ?thesis .;
+qed;
+
+lemma (in QRTEMP) aux1a: "[| 0 < a; a \<le> (p - 1) div 2; 
+                             0 < b; b \<le> (q - 1) div 2 |] ==>
+                          (p * b < q * a) = (b \<le> q * a div p)";
+proof -;
+  assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2";
+  have "p * b < q * a ==> b \<le> q * a div p";
+  proof -;
+    assume "p * b < q * a";
+    then have "p * b \<le> q * a" by auto
+    then have "(p * b) div p \<le> (q * a) div p";
+      by (rule zdiv_mono1, insert p_g_2, auto)
+    then show "b \<le> (q * a) div p";
+      apply (subgoal_tac "p \<noteq> 0")
+      apply (frule zdiv_zmult_self2, force)
+      by (insert p_g_2, auto)
+  qed;
+  moreover have "b \<le> q * a div p ==> p * b < q * a";
+  proof -;
+    assume "b \<le> q * a div p";
+    then have "p * b \<le> p * ((q * a) div p)";
+      by (insert p_g_2, auto simp add: zmult_zle_cancel1)
+    also have "... \<le> q * a";
+      by (rule zdiv_leq_prop, insert p_g_2, auto)
+    finally have "p * b \<le> q * a" .;
+    then have "p * b < q * a | p * b = q * a";
+      by (simp only: order_le_imp_less_or_eq)
+    moreover have "p * b \<noteq> q * a";
+      by (rule  pb_neq_qa, insert prems, auto)
+    ultimately show ?thesis by auto
+  qed;
+  ultimately show ?thesis ..;
+qed;
+
+lemma (in QRTEMP) aux1b: "[| 0 < a; a \<le> (p - 1) div 2; 
+                             0 < b; b \<le> (q - 1) div 2 |] ==>
+                          (q * a < p * b) = (a \<le> p * b div q)";
+proof -;
+  assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2";
+  have "q * a < p * b ==> a \<le> p * b div q";
+  proof -;
+    assume "q * a < p * b";
+    then have "q * a \<le> p * b" by auto
+    then have "(q * a) div q \<le> (p * b) div q";
+      by (rule zdiv_mono1, insert q_g_2, auto)
+    then show "a \<le> (p * b) div q";
+      apply (subgoal_tac "q \<noteq> 0")
+      apply (frule zdiv_zmult_self2, force)
+      by (insert q_g_2, auto)
+  qed;
+  moreover have "a \<le> p * b div q ==> q * a < p * b";
+  proof -;
+    assume "a \<le> p * b div q";
+    then have "q * a \<le> q * ((p * b) div q)";
+      by (insert q_g_2, auto simp add: zmult_zle_cancel1)
+    also have "... \<le> p * b";
+      by (rule zdiv_leq_prop, insert q_g_2, auto)
+    finally have "q * a \<le> p * b" .;
+    then have "q * a < p * b | q * a = p * b";
+      by (simp only: order_le_imp_less_or_eq)
+    moreover have "p * b \<noteq> q * a";
+      by (rule  pb_neq_qa, insert prems, auto)
+    ultimately show ?thesis by auto
+  qed;
+  ultimately show ?thesis ..;
+qed;
+
+lemma aux2: "[| p \<in> zprime; q \<in> zprime; 2 < p; 2 < q |] ==> 
+             (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2";
+proof-;
+  assume "p \<in> zprime" and "q \<in> zprime" and "2 < p" and "2 < q";
+  (* Set up what's even and odd *)
+  then have "p \<in> zOdd & q \<in> zOdd";
+    by (auto simp add:  zprime_zOdd_eq_grt_2)
+  then have even1: "(p - 1):zEven & (q - 1):zEven";
+    by (auto simp add: odd_minus_one_even)
+  then have even2: "(2 * p):zEven & ((q - 1) * p):zEven";
+    by (auto simp add: zEven_def)
+  then have even3: "(((q - 1) * p) + (2 * p)):zEven";
+    by (auto simp: even_plus_even)
+  (* using these prove it *)
+  from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)";
+    by (auto simp add: int_distrib)
+  then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2";
+    apply (rule_tac x = "((p - 1) * q)" in even_div_2_l);
+    by (auto simp add: even3, auto simp add: zmult_ac)
+  also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)";
+    by (auto simp add: even1 even_prod_div_2)
+  also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p";
+    by (auto simp add: even1 even2 even_prod_div_2 even_sum_div_2)
+  finally show ?thesis 
+    apply (rule_tac x = " q * ((p - 1) div 2)" and 
+                    y = "(q - 1) div 2" in div_prop2);
+    by (insert prems, auto)
+qed;
+
+lemma (in QRTEMP) aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p";
+proof;
+  fix j;
+  assume j_fact: "j \<in> P_set";
+  have "int (card (f1 j)) = int (card {y. y \<in> Q_set & y \<le> (q * j) div p})";
+  proof -;
+    have "finite (f1 j)";
+    proof -;
+      have "(f1 j) \<subseteq> S" by (auto simp add: f1_def)
+      with S_finite show ?thesis by (auto simp add: finite_subset)
+    qed;
+    moreover have "inj_on (%(x,y). y) (f1 j)";
+      by (auto simp add: f1_def inj_on_def)
+    ultimately have "card ((%(x,y). y) ` (f1 j)) = card  (f1 j)";
+      by (auto simp add: f1_def card_image)
+    moreover have "((%(x,y). y) ` (f1 j)) = {y. y \<in> Q_set & y \<le> (q * j) div p}";
+      by (insert prems, auto simp add: f1_def S_def Q_set_def P_set_def 
+        image_def)
+    ultimately show ?thesis by (auto simp add: f1_def)
+  qed;
+  also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})";
+  proof -;
+    have "{y. y \<in> Q_set & y \<le> (q * j) div p} = 
+        {y. 0 < y & y \<le> (q * j) div p}";
+      apply (auto simp add: Q_set_def)
+      proof -;
+        fix x;
+        assume "0 < x" and "x \<le> q * j div p";
+        with j_fact P_set_def  have "j \<le> (p - 1) div 2"; by auto
+        with q_g_2; have "q * j \<le> q * ((p - 1) div 2)";
+          by (auto simp add: zmult_zle_cancel1)
+        with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p";
+          by (auto simp add: zdiv_mono1)
+        also from prems have "... \<le> (q - 1) div 2";
+          apply simp apply (insert aux2) by (simp add: QRTEMP_def)
+        finally show "x \<le> (q - 1) div 2" by (insert prems, auto)
+      qed;
+    then show ?thesis by auto
+  qed;
+  also have "... = (q * j) div p";
+  proof -;
+    from j_fact P_set_def have "0 \<le> j" by auto
+    with q_g_2 have "q * 0 \<le> q * j" by (auto simp only: zmult_zle_mono2)
+    then have "0 \<le> q * j" by auto
+    then have "0 div p \<le> (q * j) div p";
+      apply (rule_tac a = 0 in zdiv_mono1)
+      by (insert p_g_2, auto)
+    also have "0 div p = 0" by auto
+    finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
+  qed;
+  finally show "int (card (f1 j)) = q * j div p" .;
+qed;
+
+lemma (in QRTEMP) aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q";
+proof;
+  fix j;
+  assume j_fact: "j \<in> Q_set";
+  have "int (card (f2 j)) = int (card {y. y \<in> P_set & y \<le> (p * j) div q})";
+  proof -;
+    have "finite (f2 j)";
+    proof -;
+      have "(f2 j) \<subseteq> S" by (auto simp add: f2_def)
+      with S_finite show ?thesis by (auto simp add: finite_subset)
+    qed;
+    moreover have "inj_on (%(x,y). x) (f2 j)";
+      by (auto simp add: f2_def inj_on_def)
+    ultimately have "card ((%(x,y). x) ` (f2 j)) = card  (f2 j)";
+      by (auto simp add: f2_def card_image)
+    moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}";
+      by (insert prems, auto simp add: f2_def S_def Q_set_def 
+        P_set_def image_def)
+    ultimately show ?thesis by (auto simp add: f2_def)
+  qed;
+  also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})";
+  proof -;
+    have "{y. y \<in> P_set & y \<le> (p * j) div q} = 
+        {y. 0 < y & y \<le> (p * j) div q}";
+      apply (auto simp add: P_set_def)
+      proof -;
+        fix x;
+        assume "0 < x" and "x \<le> p * j div q";
+        with j_fact Q_set_def  have "j \<le> (q - 1) div 2"; by auto
+        with p_g_2; have "p * j \<le> p * ((q - 1) div 2)";
+          by (auto simp add: zmult_zle_cancel1)
+        with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q";
+          by (auto simp add: zdiv_mono1)
+        also from prems have "... \<le> (p - 1) div 2";
+          by (auto simp add: aux2 QRTEMP_def)
+        finally show "x \<le> (p - 1) div 2" by (insert prems, auto)
+      qed;
+    then show ?thesis by auto
+  qed;
+  also have "... = (p * j) div q";
+  proof -;
+    from j_fact Q_set_def have "0 \<le> j" by auto
+    with p_g_2 have "p * 0 \<le> p * j" by (auto simp only: zmult_zle_mono2)
+    then have "0 \<le> p * j" by auto
+    then have "0 div q \<le> (p * j) div q";
+      apply (rule_tac a = 0 in zdiv_mono1)
+      by (insert q_g_2, auto)
+    also have "0 div q = 0" by auto
+    finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
+  qed;
+  finally show "int (card (f2 j)) = p * j div q" .;
+qed;
+
+lemma (in QRTEMP) S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set";
+proof -;
+  have "\<forall>x \<in> P_set. finite (f1 x)";
+  proof;
+    fix x;
+    have "f1 x \<subseteq> S" by (auto simp add: f1_def)
+    with S_finite show "finite (f1 x)" by (auto simp add: finite_subset)
+  qed;
+  moreover have "(\<forall>x \<in> P_set. \<forall>y \<in> P_set. x \<noteq> y --> (f1 x) \<inter> (f1 y) = {})";
+    by (auto simp add: f1_def)
+  moreover note P_set_finite;
+  ultimately have "int(card (UNION P_set f1)) = 
+      setsum (%x. int(card (f1 x))) P_set";
+    by (rule_tac A = P_set in int_card_indexed_union_disjoint_sets, auto)
+  moreover have "S1 = UNION P_set f1";
+    by (auto simp add: f1_def S_def S1_def S2_def P_set_def Q_set_def aux1a)
+  ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set" 
+    by auto
+  also have "... = setsum (%j. q * j div p) P_set";
+  proof -;
+    note aux3a
+    with  P_set_finite show ?thesis by (rule setsum_same_function)
+  qed;
+  finally show ?thesis .;
+qed;
+
+lemma (in QRTEMP) S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set";
+proof -;
+  have "\<forall>x \<in> Q_set. finite (f2 x)";
+  proof;
+    fix x;
+    have "f2 x \<subseteq> S" by (auto simp add: f2_def)
+    with S_finite show "finite (f2 x)" by (auto simp add: finite_subset)
+  qed;
+  moreover have "(\<forall>x \<in> Q_set. \<forall>y \<in> Q_set. x \<noteq> y --> 
+      (f2 x) \<inter> (f2 y) = {})";
+    by (auto simp add: f2_def)
+  moreover note Q_set_finite;
+  ultimately have "int(card (UNION Q_set f2)) = 
+      setsum (%x. int(card (f2 x))) Q_set";
+    by (rule_tac A = Q_set in int_card_indexed_union_disjoint_sets, auto)
+  moreover have "S2 = UNION Q_set f2";
+    by (auto simp add: f2_def S_def S1_def S2_def P_set_def Q_set_def aux1b)
+  ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set" 
+    by auto
+  also have "... = setsum (%j. p * j div q) Q_set";
+  proof -;
+    note aux3b;
+    with Q_set_finite show ?thesis by (rule setsum_same_function)
+  qed;
+  finally show ?thesis .;
+qed;
+
+lemma (in QRTEMP) S1_carda: "int (card(S1)) = 
+    setsum (%j. (j * q) div p) P_set";
+  by (auto simp add: S1_card zmult_ac)
+
+lemma (in QRTEMP) S2_carda: "int (card(S2)) = 
+    setsum (%j. (j * p) div q) Q_set";
+  by (auto simp add: S2_card zmult_ac)
+
+lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) + 
+    (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)";
+proof -;
+  have "(setsum (%j. (j * p) div q) Q_set) + 
+      (setsum (%j. (j * q) div p) P_set) = int (card S2) + int (card S1)";
+    by (auto simp add: S1_carda S2_carda)
+  also have "... = int (card S1) + int (card S2)";
+    by auto
+  also have "... = ((p - 1) div 2) * ((q - 1) div 2)";
+    by (auto simp add: card_sum_S1_S2)
+  finally show ?thesis .;
+qed;
+
+lemma pq_prime_neq: "[| p \<in> zprime; q \<in> zprime; p \<noteq> q |] ==> (~[p = 0] (mod q))";
+  apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
+  apply (drule_tac x = q in allE)
+  apply (drule_tac x = p in allE)
+by auto
+
+lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) = 
+    (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
+proof -;
+  from prems have "~([p = 0] (mod q))";
+    by (auto simp add: pq_prime_neq QRTEMP_def)
+  with prems have a1: "(Legendre p q) = (-1::int) ^ 
+      nat(setsum (%x. ((x * p) div q)) Q_set)";
+    apply (rule_tac p = q in  MainQRLemma)
+    by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
+  from prems have "~([q = 0] (mod p))";
+    apply (rule_tac p = q and q = p in pq_prime_neq)
+    apply (simp add: QRTEMP_def)+;
+    by arith
+  with prems have a2: "(Legendre q p) = 
+      (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)";
+    apply (rule_tac p = p in  MainQRLemma)
+    by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
+  from a1 a2 have "(Legendre p q) * (Legendre q p) = 
+      (-1::int) ^ nat(setsum (%x. ((x * p) div q)) Q_set) *
+        (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)";
+    by auto
+  also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) + 
+                   nat(setsum (%x. ((x * q) div p)) P_set))";
+    by (auto simp add: zpower_zadd_distrib)
+  also have "nat(setsum (%x. ((x * p) div q)) Q_set) + 
+      nat(setsum (%x. ((x * q) div p)) P_set) =
+        nat((setsum (%x. ((x * p) div q)) Q_set) + 
+          (setsum (%x. ((x * q) div p)) P_set))";
+    apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in 
+      nat_add_distrib [THEN sym]);
+    by (auto simp add: S1_carda [THEN sym] S2_carda [THEN sym])
+  also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))";
+    by (auto simp add: pq_sum_prop)
+  finally show ?thesis .;
+qed;
+
+theorem Quadratic_Reciprocity:
+     "[| p \<in> zOdd; p \<in> zprime; q \<in> zOdd; q \<in> zprime; 
+         p \<noteq> q |] 
+      ==> (Legendre p q) * (Legendre q p) = 
+          (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
+  by (auto simp add: QRTEMP.QR_short zprime_zOdd_eq_grt_2 [THEN sym] 
+                     QRTEMP_def)
+
+end
diff -r cf947d1ec5ff -r 26e5f5e624f6 src/HOL/NumberTheory/ROOT.ML
--- a/src/HOL/NumberTheory/ROOT.ML	Tue Mar 18 18:07:06 2003 +0100
+++ b/src/HOL/NumberTheory/ROOT.ML	Thu Mar 20 15:58:25 2003 +0100
@@ -1,3 +1,16 @@
+(*  Title:      HOL/NumberTheory/ROOT.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson
+    Copyright   2003  University of Cambridge
+
+This directory contains formalized proofs of Wilson's Theorem (by Thomas M
+Rasmussen) and of Gauss' law of quadratic reciprocity (by Avigad, Gray and
+Kramer).  The latter formalization follows Eisenstein's proof, which is the
+one most commonly found in introductory textbooks, and also uses a
+trick used David Russinoff with the Boyer-Moore theorem prover.
+See his "A mechanical proof of quadratic reciprocity," Journal of Automated
+Reasoning 8:3-21, 1992.
+*)
 
 no_document use_thy "Permutation";
 no_document use_thy "Primes";
@@ -8,3 +21,4 @@
 use_thy "EulerFermat";
 use_thy "WilsonRuss";
 use_thy "WilsonBij";
+use_thy "Quadratic_Reciprocity";
diff -r cf947d1ec5ff -r 26e5f5e624f6 src/HOL/NumberTheory/Residues.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/Residues.thy	Thu Mar 20 15:58:25 2003 +0100
@@ -0,0 +1,187 @@
+(*  Title:      HOL/Quadratic_Reciprocity/Residues.thy
+    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+header {* Residue Sets *}
+
+theory Residues = Int2:;
+
+text{*Note.  This theory is being revised.  See the web page
+\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
+
+(*****************************************************************)
+(*                                                               *)
+(* Define the residue of a set, the standard residue, quadratic  *)
+(* residues, and prove some basic properties.                    *)
+(*                                                               *)
+(*****************************************************************)
+
+constdefs
+  ResSet      :: "int => int set => bool"
+  "ResSet m X == \<forall>y1 y2. (((y1 \<in> X) & (y2 \<in> X) & [y1 = y2] (mod m)) --> 
+    y1 = y2)"
+
+  StandardRes :: "int => int => int"
+  "StandardRes m x == x mod m"
+
+  QuadRes     :: "int => int => bool"
+  "QuadRes m x == \<exists>y. ([(y ^ 2) = x] (mod m))"
+
+  Legendre    :: "int => int => int"      
+  "Legendre a p == (if ([a = 0] (mod p)) then 0
+                     else if (QuadRes p a) then 1
+                     else -1)"
+
+  SR          :: "int => int set"
+  "SR p == {x. (0 \<le> x) & (x < p)}"
+
+  SRStar      :: "int => int set"
+  "SRStar p == {x. (0 < x) & (x < p)}";
+
+(******************************************************************)
+(*                                                                *)
+(* Some useful properties of StandardRes                          *)
+(*                                                                *)
+(******************************************************************)
+
+subsection {* Properties of StandardRes *}
+
+lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)";
+  by (auto simp add: StandardRes_def zcong_zmod)
+
+lemma StandardRes_prop2: "0 < m ==> (StandardRes m x1 = StandardRes m x2)
+      = ([x1 = x2] (mod m))";
+  by (auto simp add: StandardRes_def zcong_zmod_eq)
+
+lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))";
+  by (auto simp add: StandardRes_def zcong_def zdvd_iff_zmod_eq_0)
+
+lemma StandardRes_prop4: "2 < m 
+     ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)";
+  by (auto simp add: StandardRes_def zcong_zmod_eq 
+                     zmod_zmult_distrib [of x y m])
+
+lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x";
+  by (auto simp add: StandardRes_def pos_mod_sign)
+
+lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p";
+  by (auto simp add: StandardRes_def pos_mod_bound)
+
+lemma StandardRes_eq_zcong: 
+   "(StandardRes m x = 0) = ([x = 0](mod m))";
+  by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) 
+
+(******************************************************************)
+(*                                                                *)
+(* Some useful stuff relating StandardRes and SRStar and SR       *)
+(*                                                                *)
+(******************************************************************)
+
+subsection {* Relations between StandardRes, SRStar, and SR *}
+
+lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p";
+  by (auto simp add: SRStar_def SR_def)
+
+lemma StandardRes_SR_prop: "x \<in> SR p ==> StandardRes p x = x";
+  by (auto simp add: SR_def StandardRes_def mod_pos_pos_trivial)
+
+lemma StandardRes_SRStar_prop1: "2 < p ==> (StandardRes p x \<in> SRStar p) 
+     = (~[x = 0] (mod p))";
+  apply (auto simp add: StandardRes_prop3 StandardRes_def
+                        SRStar_def pos_mod_bound)
+  apply (subgoal_tac "0 < p")
+by (drule_tac a = x in pos_mod_sign, arith, simp)
+
+lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))";
+  by (auto simp add: SRStar_def zcong_def zdvd_not_zless)
+
+lemma StandardRes_SRStar_prop2: "[| 2 < p; p \<in> zprime; x \<in> SRStar p |] 
+     ==> StandardRes p (MultInv p x) \<in> SRStar p";
+  apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp);
+  apply (rule MultInv_prop3)
+  apply (auto simp add: SRStar_def zcong_def zdvd_not_zless)
+done
+
+lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x";
+  by (auto simp add: SRStar_SR_prop StandardRes_SR_prop)
+
+lemma StandardRes_SRStar_prop4: "[| p \<in> zprime; 2 < p; x \<in> SRStar p |] 
+     ==> StandardRes p x \<in> SRStar p";
+  by (frule StandardRes_SRStar_prop3, auto)
+
+lemma SRStar_mult_prop1: "[| p \<in> zprime; 2 < p; x \<in> SRStar p; y \<in> SRStar p|] 
+     ==> (StandardRes p (x * y)):SRStar p";
+  apply (frule_tac x = x in StandardRes_SRStar_prop4, auto)
+  apply (frule_tac x = y in StandardRes_SRStar_prop4, auto)
+  apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
+done
+
+lemma SRStar_mult_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)); 
+     x \<in> SRStar p |] 
+     ==> StandardRes p (a * MultInv p x) \<in> SRStar p";
+  apply (frule_tac x = x in StandardRes_SRStar_prop2, auto)
+  apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1)
+  apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
+done
+
+lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p - 1";
+  by (auto simp add: SRStar_def int_card_bdd_int_set_l_l)
+
+lemma SRStar_finite: "2 < p ==> finite( SRStar p)";
+  by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
+
+(******************************************************************)
+(*                                                                *)
+(* Some useful stuff about ResSet and StandardRes                 *)
+(*                                                                *)
+(******************************************************************)
+
+subsection {* Properties relating ResSets with StandardRes *}
+
+lemma aux: "x mod m = y mod m ==> [x = y] (mod m)";
+  apply (subgoal_tac "x = y ==> [x = y](mod m)");
+  apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)");
+  apply (auto simp add: zcong_zmod [of x y m])
+done
+
+lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)";
+  apply (auto simp add: ResSet_def StandardRes_def inj_on_def)
+  apply (drule_tac m = m in aux, auto)
+done
+
+lemma StandardRes_Sum: "[| finite X; 0 < m |] 
+     ==> [setsum f X = setsum (StandardRes m o f) X](mod m)"; 
+  apply (rule_tac F = X in finite_induct)
+  apply (auto intro!: zcong_zadd simp add: StandardRes_prop1)
+done
+
+lemma SR_pos: "0 < m ==> (StandardRes m ` X) \<subseteq> {x. 0 \<le> x & x < m}";
+  by (auto simp add: StandardRes_ubound StandardRes_lbound)
+
+lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X";
+  apply (rule_tac f = "StandardRes m" in finite_imageD) 
+  apply (rule_tac B = "{x. (0 :: int) \<le> x & x < m}" in finite_subset);
+by (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos)
+
+lemma mod_mod_is_mod: "[x = x mod m](mod m)";
+  by (auto simp add: zcong_zmod)
+
+lemma StandardRes_prod: "[| finite X; 0 < m |] 
+     ==> [gsetprod f X = gsetprod (StandardRes m o f) X] (mod m)";
+  apply (rule_tac F = X in finite_induct)
+by (auto intro!: zcong_zmult simp add: StandardRes_prop1)
+
+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)";
+  by (auto simp add: ResSet_def)
+
+(****************************************************************)
+(*                                                              *)
+(* Property for SRStar                                          *)
+(*                                                              *)
+(****************************************************************)
+
+lemma ResSet_SRStar_prop: "ResSet p (SRStar p)";
+  by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
+
+end;
\ No newline at end of file
diff -r cf947d1ec5ff -r 26e5f5e624f6 src/HOL/NumberTheory/document/root.tex
--- a/src/HOL/NumberTheory/document/root.tex	Tue Mar 18 18:07:06 2003 +0100
+++ b/src/HOL/NumberTheory/document/root.tex	Thu Mar 20 15:58:25 2003 +0100
@@ -9,11 +9,39 @@
 \begin{document}
 
 \title{Some results of number theory}
-\author{Lawrence C Paulson \\
-  Thomas M Rasmussen \\
-  Christophe Tabacznyj}
+\author{Jeremy Avigad\\
+    David Gray\\
+    Adam Kramer\\
+    Thomas M Rasmussen}
+
 \maketitle
 
+\begin{abstract}
+This directory contains formalized proofs of many results of number theory.
+The proofs of the Chinese Remainder Theorem and Wilson's Theorem are due to
+Rasmussen.  The proof of Gauss's law of quadratic reciprocity is due to
+Avigad, Gray and Kramer.  Proofs can be found in most introductory number
+theory textbooks; Goldman's \emph{The Queen of Mathematics: a Historically
+Motivated Guide to Number Theory} provides some historical context.
+
+Avigad, Gray and Kramer have also provided library theories dealing with
+finite sets and finite sums, divisibility and congruences, parity and
+residues.  The authors are engaged in redesigning and polishing these theories
+for more serious use.  For the latest information in this respect, please see
+the web page \url{http://www.andrew.cmu.edu/~avigad/isabelle}.  Other theories
+contain proofs of Euler's criteria, Gauss' lemma, and the law of quadratic
+reciprocity.  The formalization follows Eisenstein's proof, which is the one
+most commonly found in introductory textbooks; in particular, it follows the
+presentation in Niven and Zuckerman, \emph{The Theory of Numbers}.
+
+To avoid having to count roots of polynomials, however, we relied on a trick
+previously used by David Russinoff in formalizing quadratic reciprocity for
+the Boyer-Moore theorem prover; see Russinoff, David, ``A mechanical proof
+of quadratic reciprocity,'' \emph{Journal of Automated Reasoning} 8:3-21,
+1992.  We are grateful to Larry Paulson for calling our attention to this
+reference.
+\end{abstract}
+
 \tableofcontents
 
 \begin{center}