equal
deleted
inserted
replaced
4 Copyright 1995 University of Cambridge & TU Muenchen |
4 Copyright 1995 University of Cambridge & TU Muenchen |
5 |
5 |
6 Finite sets, their cardinality, and a fold functional. |
6 Finite sets, their cardinality, and a fold functional. |
7 *) |
7 *) |
8 |
8 |
9 Finite = Divides + Power + Inductive + |
9 Finite = Divides + Power + Inductive + SetInterval + |
10 |
10 |
11 consts Finites :: 'a set set |
11 consts Finites :: 'a set set |
12 |
12 |
13 inductive "Finites" |
13 inductive "Finites" |
14 intrs |
14 intrs |
55 ==> (insert x A, f x y) : foldSet f e" |
55 ==> (insert x A, f x y) : foldSet f e" |
56 |
56 |
57 constdefs |
57 constdefs |
58 fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a" |
58 fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a" |
59 "fold f e A == @x. (A,x) : foldSet f e" |
59 "fold f e A == @x. (A,x) : foldSet f e" |
60 (* A frequent instance: *) |
60 |
61 setsum :: ('a => nat) => 'a set => nat |
61 setsum :: "('a => 'b) => 'a set => ('b::plus_ac0)" |
62 "setsum f == fold (op+ o f) 0" |
62 "setsum f == fold (op+ o f) 0" |
63 |
63 |
64 locale LC = |
64 locale LC = |
65 fixes |
65 fixes |
66 f :: ['b,'a] => 'a |
66 f :: ['b,'a] => 'a |