src/HOL/NumberTheory/IntFact.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:	IntFact.thy
    ID:         $Id$
    Author:	Thomas M. Rasmussen
    Copyright	2000  University of Cambridge
*)

IntFact = IntPrimes + 

consts
  zfact    :: int => int
  setprod  :: int set => int
  d22set   :: int => int set

recdef zfact "measure ((% n.(nat n)) ::int=>nat)"
    "zfact n = (if n<=#0 then #1 else n*zfact(n-#1))"

defs
  setprod_def  "setprod A == (if finite A then fold (op*) #1 A else #1)"

recdef d22set "measure ((%a.(nat a)) ::int=>nat)"
    "d22set a = (if #1<a then insert a (d22set (a-#1)) else {})"

end