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

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

WilsonRuss = EulerFermat +

consts
  inv    :: "[int,int] => int" 
  wset   :: "int*int=>int set"

defs
  inv_def   "inv p a == (a ^ (nat (p - #2))) mod p"

recdef wset "measure ((%(a,p).(nat a)) ::int*int=>nat)"
    "wset (a,p) = (if #1<a then let ws = wset (a-#1,p) in
                     (if a:ws then ws else insert a (insert (inv p a) ws))
                   else {})"

end