--- /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
--- /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;
--- /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;
--- /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
--- /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
--- /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
--- 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";
--- /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
--- 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}