equal
deleted
inserted
replaced
|
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 |