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.4 -(*  Title:      HOL/Quadratic_Reciprocity/Residues.thy
     1.5 -    ID:         $Id$
     1.6 +(*  Title:      HOL/Old_Number_Theory/Residues.thy
     1.7      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     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 *}