diff -r faacfd4392b5 -r 5a5c8ea5f66a src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Tue Nov 07 19:39:54 2006 +0100
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Tue Nov 07 19:40:13 2006 +0100
@@ -14,7 +14,10 @@
   Zuckerman's presentation.
 *}
 
-lemma (in GAUSS) QRLemma1: "a * setsum id A =
+context GAUSS
+begin
+
+lemma 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"
@@ -44,7 +47,7 @@
   finally show ?thesis by arith
 qed
 
-lemma (in GAUSS) QRLemma2: "setsum id A = p * int (card E) - setsum id E +
+lemma 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)"
@@ -65,7 +68,7 @@
     by arith
 qed
 
-lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A =
+lemma 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"
@@ -83,7 +86,7 @@
     by (auto simp only: zdiff_zmult_distrib2)
 qed
 
-lemma (in GAUSS) QRLemma4: "a \<in> zOdd ==>
+lemma QRLemma4: "a \<in> zOdd ==>
     (setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)"
 proof -
   assume a_odd: "a \<in> zOdd"
@@ -108,7 +111,7 @@
     by (auto simp only: even_diff [symmetric])
 qed
 
-lemma (in GAUSS) QRLemma5: "a \<in> zOdd ==>
+lemma QRLemma5: "a \<in> zOdd ==>
    (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
 proof -
   assume "a \<in> zOdd"
@@ -138,6 +141,8 @@
   finally show ?thesis .
 qed
 
+end
+
 lemma MainQRLemma: "[| a \<in> zOdd; 0 < a; ~([a = 0] (mod p)); zprime p; 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))"
@@ -145,6 +150,7 @@
   apply (auto simp add: GAUSS_def)
   apply (subst GAUSS.QRLemma5)
   apply (auto simp add: GAUSS_def)
+  apply (simp add: GAUSS.A_def [OF GAUSS.intro] GAUSS_def)
   done
 
 
@@ -153,47 +159,51 @@
 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: "zprime p"
   assumes p_g_2: "2 < p"
   assumes q_prime: "zprime q"
   assumes q_g_2: "2 < q"
   assumes p_neq_q:      "p \<noteq> q"
+begin
 
-  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) }"
+definition
+  P_set :: "int set"
+  "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
+
+  Q_set :: "int set"
+  "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
+  
+  S :: "(int * int) set"
+  "S = P_set <*> Q_set"
+
+  S1 :: "(int * int) set"
+  "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
 
-lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2"
+  S2 :: "(int * int) set"
+  "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
+
+  f1 :: "int => (int * int) set"
+  "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
+
+  f2 :: "int => (int * int) set"
+  "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
+
+lemma 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
+  from p_g_2 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"
+lemma 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
+  from q_g_2 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 |] ==>
+lemma 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"
@@ -234,43 +244,43 @@
   with q_g_2 show False by auto
 qed
 
-lemma (in QRTEMP) P_set_finite: "finite (P_set)"
+lemma P_set_finite: "finite (P_set)"
   using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)
 
-lemma (in QRTEMP) Q_set_finite: "finite (Q_set)"
+lemma Q_set_finite: "finite (Q_set)"
   using q_fact by (auto simp add: Q_set_def bdd_int_set_l_le_finite)
 
-lemma (in QRTEMP) S_finite: "finite S"
+lemma S_finite: "finite S"
   by (auto simp add: S_def  P_set_finite Q_set_finite finite_cartesian_product)
 
-lemma (in QRTEMP) S1_finite: "finite S1"
+lemma 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"
+lemma 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))"
+lemma P_set_card: "(p - 1) div 2 = int (card (P_set))"
   using p_fact by (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))"
+lemma Q_set_card: "(q - 1) div 2 = int (card (Q_set))"
   using q_fact by (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))"
+lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
   using P_set_card Q_set_card P_set_finite Q_set_finite
   by (auto simp add: S_def zmult_int setsum_constant)
 
-lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}"
+lemma 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"
+lemma 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
@@ -280,7 +290,7 @@
   ultimately show "p * b < q * a" by auto
 qed
 
-lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) =
+lemma 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))"
@@ -293,7 +303,7 @@
   finally show ?thesis .
 qed
 
-lemma (in QRTEMP) aux1a: "[| 0 < a; a \<le> (p - 1) div 2;
+lemma 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 -
@@ -327,7 +337,7 @@
   ultimately show ?thesis ..
 qed
 
-lemma (in QRTEMP) aux1b: "[| 0 < a; a \<le> (p - 1) div 2;
+lemma 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 -
@@ -361,6 +371,8 @@
   ultimately show ?thesis ..
 qed
 
+end
+
 lemma aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
              (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
 proof-
@@ -390,7 +402,10 @@
     using prems by auto
 qed
 
-lemma (in QRTEMP) aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
+context QRTEMP
+begin
+
+lemma aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
 proof
   fix j
   assume j_fact: "j \<in> P_set"
@@ -422,7 +437,7 @@
         by (auto simp add: mult_le_cancel_left)
       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"
+      also from prems P_set_def have "... \<le> (q - 1) div 2"
         apply simp
         apply (insert aux2)
         apply (simp add: QRTEMP_def)
@@ -446,7 +461,7 @@
   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"
+lemma aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q"
 proof
   fix j
   assume j_fact: "j \<in> Q_set"
@@ -499,7 +514,7 @@
   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"
+lemma S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set"
 proof -
   have "\<forall>x \<in> P_set. finite (f1 x)"
   proof
@@ -522,7 +537,7 @@
   finally show ?thesis .
 qed
 
-lemma (in QRTEMP) S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set"
+lemma S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set"
 proof -
   have "\<forall>x \<in> Q_set. finite (f2 x)"
   proof
@@ -546,15 +561,15 @@
   finally show ?thesis .
 qed
 
-lemma (in QRTEMP) S1_carda: "int (card(S1)) =
+lemma 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)) =
+lemma 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) +
+lemma 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) +
@@ -567,6 +582,8 @@
   finally show ?thesis .
 qed
 
+end
+
 lemma pq_prime_neq: "[| zprime p; zprime q; p \<noteq> q |] ==> (~[p = 0] (mod q))"
   apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
   apply (drule_tac x = q in allE)
@@ -574,12 +591,15 @@
   apply auto
   done
 
-lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) =
+context QRTEMP
+begin
+
+lemma 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) ^
+  with prems Q_set_def have a1: "(Legendre p q) = (-1::int) ^
       nat(setsum (%x. ((x * p) div q)) Q_set)"
     apply (rule_tac p = q in  MainQRLemma)
     apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
@@ -588,7 +608,7 @@
     apply (rule_tac p = q and q = p in pq_prime_neq)
     apply (simp add: QRTEMP_def)+
     done
-  with prems have a2: "(Legendre q p) =
+  with prems P_set_def have a2: "(Legendre q p) =
       (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
     apply (rule_tac p = p in  MainQRLemma)
     apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
@@ -613,6 +633,8 @@
   finally show ?thesis .
 qed
 
+end
+
 theorem Quadratic_Reciprocity:
      "[| p \<in> zOdd; zprime p; q \<in> zOdd; zprime q;
          p \<noteq> q |]