--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Fri Nov 17 02:20:03 2006 +0100
@@ -168,25 +168,31 @@
begin
definition
- P_set :: "int set"
+ P_set :: "int set" where
"P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
- Q_set :: "int set"
+definition
+ Q_set :: "int set" where
"Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
- S :: "(int * int) set"
+definition
+ S :: "(int * int) set" where
"S = P_set <*> Q_set"
- S1 :: "(int * int) set"
+definition
+ S1 :: "(int * int) set" where
"S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
- S2 :: "(int * int) set"
+definition
+ S2 :: "(int * int) set" where
"S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
- f1 :: "int => (int * int) set"
+definition
+ f1 :: "int => (int * int) set" where
"f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
- f2 :: "int => (int * int) set"
+definition
+ f2 :: "int => (int * int) set" where
"f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
lemma p_fact: "0 < (p - 1) div 2"