isabelle: src/HOL/NumberTheory/IntFact.thy@c1d9500e2927 (annotated)

9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	1	(* Title: IntFact.thy
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	2	ID: $Id$
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	3	Author: Thomas M. Rasmussen
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	4	Copyright 2000 University of Cambridge
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	5	*)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	6
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	7	IntFact = IntPrimes +
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	8
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	9	consts
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	10	zfact :: int => int
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	11	setprod :: int set => int
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	12	d22set :: int => int set
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	13
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	14	recdef zfact "measure ((% n.(nat n)) ::int=>nat)"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	15	"zfact n = (if n<=#0 then #1 else n*zfact(n-#1))"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	16
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	17	defs
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	18	setprod_def "setprod A == (if finite A then fold (op*) #1 A else #1)"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	19
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	20	recdef d22set "measure ((%a.(nat a)) ::int=>nat)"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	21	"d22set a = (if #1<a then insert a (d22set (a-#1)) else {})"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	22
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	23	end

author	paulson
	Mon, 07 Aug 2000 10:27:35 +0200
changeset 9545	c1d9500e2927
parent 9508	4d01dbf6ded7
child 11049	7eef34adb852
permissions	-rw-r--r--