src/HOL/Old_Number_Theory/Residues.thy
 changeset 38159 e9b4835a54ee parent 32479 521cc9bf2958 child 41541 1fa4725c4656
```     1.1 --- a/src/HOL/Old_Number_Theory/Residues.thy	Thu Aug 05 23:43:43 2010 +0200
1.2 +++ b/src/HOL/Old_Number_Theory/Residues.thy	Fri Aug 06 12:37:00 2010 +0200
1.3 @@ -1,41 +1,36 @@
1.5 -    ID:         \$Id\$
1.6 +(*  Title:      HOL/Old_Number_Theory/Residues.thy
1.8  *)
1.9
1.10  header {* Residue Sets *}
1.11
1.12 -theory Residues imports Int2 begin
1.13 +theory Residues
1.14 +imports Int2
1.15 +begin
1.16
1.17  text {*
1.18    \medskip Define the residue of a set, the standard residue,
1.19    quadratic residues, and prove some basic properties. *}
1.20
1.21 -definition
1.22 -  ResSet      :: "int => int set => bool" where
1.23 -  "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
1.24 +definition ResSet :: "int => int set => bool"
1.25 +  where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
1.26
1.27 -definition
1.28 -  StandardRes :: "int => int => int" where
1.29 -  "StandardRes m x = x mod m"
1.30 +definition StandardRes :: "int => int => int"
1.31 +  where "StandardRes m x = x mod m"
1.32
1.33 -definition
1.34 -  QuadRes     :: "int => int => bool" where
1.35 -  "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
1.36 +definition QuadRes :: "int => int => bool"
1.37 +  where "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
1.38
1.39 -definition
1.40 -  Legendre    :: "int => int => int" where
1.41 +definition Legendre :: "int => int => int" where
1.42    "Legendre a p = (if ([a = 0] (mod p)) then 0
1.43                       else if (QuadRes p a) then 1
1.44                       else -1)"
1.45
1.46 -definition
1.47 -  SR          :: "int => int set" where
1.48 -  "SR p = {x. (0 \<le> x) & (x < p)}"
1.49 +definition SR :: "int => int set"
1.50 +  where "SR p = {x. (0 \<le> x) & (x < p)}"
1.51
1.52 -definition
1.53 -  SRStar      :: "int => int set" where
1.54 -  "SRStar p = {x. (0 < x) & (x < p)}"
1.55 +definition SRStar :: "int => int set"
1.56 +  where "SRStar p = {x. (0 < x) & (x < p)}"
1.57
1.58
1.59  subsection {* Some useful properties of StandardRes *}
```