|
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 |