src/HOL/NumberTheory/IntFact.thy
author paulson
Thu Aug 03 10:46:01 2000 +0200 (2000-08-03)
changeset 9508 4d01dbf6ded7
child 11049 7eef34adb852
permissions -rw-r--r--
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson@9508
     1
(*  Title:	IntFact.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
IntFact = IntPrimes + 
paulson@9508
     8
paulson@9508
     9
consts
paulson@9508
    10
  zfact    :: int => int
paulson@9508
    11
  setprod  :: int set => int
paulson@9508
    12
  d22set   :: int => int set
paulson@9508
    13
paulson@9508
    14
recdef zfact "measure ((% n.(nat n)) ::int=>nat)"
paulson@9508
    15
    "zfact n = (if n<=#0 then #1 else n*zfact(n-#1))"
paulson@9508
    16
paulson@9508
    17
defs
paulson@9508
    18
  setprod_def  "setprod A == (if finite A then fold (op*) #1 A else #1)"
paulson@9508
    19
paulson@9508
    20
recdef d22set "measure ((%a.(nat a)) ::int=>nat)"
paulson@9508
    21
    "d22set a = (if #1<a then insert a (d22set (a-#1)) else {})"
paulson@9508
    22
paulson@9508
    23
end