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)"
```