--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Factorization.thy Wed Mar 08 16:14:12 2000 +0100
@@ -0,0 +1,38 @@
+(* Title: HOL/ex/Factorization.thy
+ ID: $Id$
+ Author: Thomas Marthedal Rasmussen
+ Copyright 2000 University of Cambridge
+
+Fundamental Theorem of Arithmetic (unique factorization into primes)
+*)
+
+
+Factorization = Primes + Perm +
+
+consts
+ primel :: nat list => bool
+ nondec :: nat list => bool
+ prod :: nat list => nat
+ oinsert :: [nat, nat list] => nat list
+ sort :: nat list => nat list
+
+defs
+ primel_def "primel xs == set xs <= prime"
+
+primrec
+ "nondec [] = True"
+ "nondec (x#xs) = (case xs of [] => True | y#ys => x<=y & nondec xs)"
+
+primrec
+ "prod [] = 1"
+ "prod (x#xs) = x * prod xs"
+
+primrec
+ "oinsert x [] = [x]"
+ "oinsert x (y#ys) = (if x<=y then x#y#ys else y#oinsert x ys)"
+
+primrec
+ "sort [] = []"
+ "sort (x#xs) = oinsert x (sort xs)"
+
+end
\ No newline at end of file