src/HOL/NumberTheory/EulerFermat.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9508 4d01dbf6ded7
child 10834 a7897aebbffc
permissions -rw-r--r--
hide many names from Datatype_Universe.

(*  Title:	EulerFermat.thy
    ID:         $Id$
    Author:	Thomas M. Rasmussen
    Copyright	2000  University of Cambridge
*)

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