src/HOL/NumberTheory/EulerFermat.thy
 author paulson Thu, 03 Aug 2000 10:46:01 +0200 changeset 9508 4d01dbf6ded7 child 10834 a7897aebbffc permissions -rw-r--r--
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
```
(*  Title:	EulerFermat.thy
ID:         \$Id\$
Author:	Thomas M. Rasmussen
*)

EulerFermat = BijectionRel + IntFact +

consts
RsetR        :: "int => int set set"
BnorRset     :: "int*int=>int set"
norRRset     :: int => int set
noXRRset     :: [int, int] => int set
phi          :: int => nat
is_RRset     :: [int set, int] => bool
RRset2norRR  :: [int set, int, int] => int

inductive "RsetR m"
intrs
empty  "{} : RsetR m"
insert "[| A : RsetR m; zgcd(a,m) = #1; \
\            ALL a'. a':A --> ~ zcong a a' m |] \
\        ==> insert a A : RsetR m"

recdef BnorRset "measure ((% (a,m).(nat a)) ::int*int=>nat)"
"BnorRset (a,m) = (if #0<a then let na = BnorRset (a-#1,m) in
(if zgcd(a,m) = #1 then insert a na else na)
else {})"

defs
norRRset_def "norRRset m   == BnorRset (m-#1,m)"

noXRRset_def "noXRRset m x == (%a. a*x)``(norRRset m)"

phi_def      "phi m == card (norRRset m)"

is_RRset_def "is_RRset A m ==  (A : (RsetR m)) & card(A) = (phi m)"

RRset2norRR_def "RRset2norRR A m a ==
(if #1<m & (is_RRset A m) & a:A
then @b. zcong a b m & b:(norRRset m) else #0)"

consts zcongm :: int => [int, int] => bool
defs zcongm_def "zcongm m == (%a b. zcong a b m)"

end
```