src/HOL/NumberTheory/EulerFermat.thy
changeset 21404 eb85850d3eb7
parent 19670 2e4a143c73c5
child 23755 1c4672d130b1
     1.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -38,25 +38,30 @@
     1.4      else {})"
     1.5  
     1.6  definition
     1.7 -  norRRset :: "int => int set"
     1.8 +  norRRset :: "int => int set" where
     1.9    "norRRset m = BnorRset (m - 1, m)"
    1.10  
    1.11 -  noXRRset :: "int => int => int set"
    1.12 +definition
    1.13 +  noXRRset :: "int => int => int set" where
    1.14    "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
    1.15  
    1.16 -  phi :: "int => nat"
    1.17 +definition
    1.18 +  phi :: "int => nat" where
    1.19    "phi m = card (norRRset m)"
    1.20  
    1.21 -  is_RRset :: "int set => int => bool"
    1.22 +definition
    1.23 +  is_RRset :: "int set => int => bool" where
    1.24    "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
    1.25  
    1.26 -  RRset2norRR :: "int set => int => int => int"
    1.27 +definition
    1.28 +  RRset2norRR :: "int set => int => int => int" where
    1.29    "RRset2norRR A m a =
    1.30       (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
    1.31          SOME b. zcong a b m \<and> b \<in> norRRset m
    1.32        else 0)"
    1.33  
    1.34 -  zcongm :: "int => int => int => bool"
    1.35 +definition
    1.36 +  zcongm :: "int => int => int => bool" where
    1.37    "zcongm m = (\<lambda>a b. zcong a b m)"
    1.38  
    1.39  lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"