equal
deleted
inserted
replaced
2 Factorisation within a factorial domain |
2 Factorisation within a factorial domain |
3 $Id$ |
3 $Id$ |
4 Author: Clemens Ballarin, started 25 November 1997 |
4 Author: Clemens Ballarin, started 25 November 1997 |
5 *) |
5 *) |
6 |
6 |
7 Factor = Ring + |
7 theory Factor imports Ring begin |
8 |
8 |
9 consts |
9 constdefs |
10 Factorisation :: ['a::ring, 'a list, 'a] => bool |
10 Factorisation :: "['a::ring, 'a list, 'a] => bool" |
11 (* factorisation of x into a list of irred factors and a unit u *) |
11 (* factorisation of x into a list of irred factors and a unit u *) |
12 |
12 "Factorisation x factors u == |
13 defs |
13 x = foldr op* factors u & |
14 Factorisation_def "Factorisation x factors u == |
14 (ALL a : set factors. irred a) & u dvd 1" |
15 x = foldr op* factors u & |
|
16 (ALL a : set factors. irred a) & u dvd 1" |
|
17 |
15 |
18 end |
16 end |