src/HOL/NumberTheory/EulerFermat.thy
author paulson
Thu Aug 03 10:46:01 2000 +0200 (2000-08-03)
changeset 9508 4d01dbf6ded7
child 10834 a7897aebbffc
permissions -rw-r--r--
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson@9508
     1
(*  Title:	EulerFermat.thy
paulson@9508
     2
    ID:         $Id$
paulson@9508
     3
    Author:	Thomas M. Rasmussen
paulson@9508
     4
    Copyright	2000  University of Cambridge
paulson@9508
     5
*)
paulson@9508
     6
paulson@9508
     7
EulerFermat = BijectionRel + IntFact +
paulson@9508
     8
paulson@9508
     9
consts
paulson@9508
    10
  RsetR        :: "int => int set set"
paulson@9508
    11
  BnorRset     :: "int*int=>int set" 
paulson@9508
    12
  norRRset     :: int => int set
paulson@9508
    13
  noXRRset     :: [int, int] => int set
paulson@9508
    14
  phi          :: int => nat
paulson@9508
    15
  is_RRset     :: [int set, int] => bool
paulson@9508
    16
  RRset2norRR  :: [int set, int, int] => int
paulson@9508
    17
paulson@9508
    18
inductive "RsetR m"
paulson@9508
    19
intrs
paulson@9508
    20
  empty  "{} : RsetR m"
paulson@9508
    21
  insert "[| A : RsetR m; zgcd(a,m) = #1; \
paulson@9508
    22
\            ALL a'. a':A --> ~ zcong a a' m |] \
paulson@9508
    23
\        ==> insert a A : RsetR m"
paulson@9508
    24
paulson@9508
    25
recdef BnorRset "measure ((% (a,m).(nat a)) ::int*int=>nat)"
paulson@9508
    26
    "BnorRset (a,m) = (if #0<a then let na = BnorRset (a-#1,m) in
paulson@9508
    27
                         (if zgcd(a,m) = #1 then insert a na else na) 
paulson@9508
    28
                       else {})"
paulson@9508
    29
paulson@9508
    30
defs
paulson@9508
    31
  norRRset_def "norRRset m   == BnorRset (m-#1,m)"
paulson@9508
    32
paulson@9508
    33
  noXRRset_def "noXRRset m x == (%a. a*x)``(norRRset m)"
paulson@9508
    34
paulson@9508
    35
  phi_def      "phi m == card (norRRset m)"
paulson@9508
    36
paulson@9508
    37
  is_RRset_def "is_RRset A m ==  (A : (RsetR m)) & card(A) = (phi m)"
paulson@9508
    38
paulson@9508
    39
  RRset2norRR_def "RRset2norRR A m a == 
paulson@9508
    40
                     (if #1<m & (is_RRset A m) & a:A 
paulson@9508
    41
                      then @b. zcong a b m & b:(norRRset m) else #0)"
paulson@9508
    42
paulson@9508
    43
consts zcongm :: int => [int, int] => bool
paulson@9508
    44
defs zcongm_def "zcongm m == (%a b. zcong a b m)"
paulson@9508
    45
paulson@9508
    46
end