9944

1 
(* Title: HOL/ex/Factorization.thy


2 
ID: $Id$


3 
Author: Thomas Marthedal Rasmussen


4 
Copyright 2000 University of Cambridge


5 


6 
Fundamental Theorem of Arithmetic (unique factorization into primes)


7 
*)


8 


9 


10 
Factorization = Primes + Perm +


11 


12 
consts


13 
primel :: nat list => bool


14 
nondec :: nat list => bool


15 
prod :: nat list => nat


16 
oinsert :: [nat, nat list] => nat list


17 
sort :: nat list => nat list


18 


19 
defs


20 
primel_def "primel xs == set xs <= prime"


21 


22 
primrec


23 
"nondec [] = True"


24 
"nondec (x#xs) = (case xs of [] => True  y#ys => x<=y & nondec xs)"


25 


26 
primrec


27 
"prod [] = 1"


28 
"prod (x#xs) = x * prod xs"


29 


30 
primrec


31 
"oinsert x [] = [x]"


32 
"oinsert x (y#ys) = (if x<=y then x#y#ys else y#oinsert x ys)"


33 


34 
primrec


35 
"sort [] = []"


36 
"sort (x#xs) = oinsert x (sort xs)"


37 


38 
end 