author | paulson |
Wed, 27 Jan 1999 15:58:22 +0100 | |
changeset 6154 | 6a00a5baef2b |
parent 6015 | d1d5dd2f121c |
child 7958 | f531589c9fc1 |
permissions | -rw-r--r-- |
1475 | 1 |
(* Title: HOL/Finite.thy |
923 | 2 |
ID: $Id$ |
1531 | 3 |
Author: Lawrence C Paulson & Tobias Nipkow |
4 |
Copyright 1995 University of Cambridge & TU Muenchen |
|
923 | 5 |
|
5616 | 6 |
Finite sets, their cardinality, and a fold functional. |
923 | 7 |
*) |
8 |
||
5101 | 9 |
Finite = Divides + Power + Inductive + |
1531 | 10 |
|
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset
|
11 |
consts Finites :: 'a set set |
923 | 12 |
|
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset
|
13 |
inductive "Finites" |
923 | 14 |
intrs |
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset
|
15 |
emptyI "{} : Finites" |
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset
|
16 |
insertI "A : Finites ==> insert a A : Finites" |
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset
|
17 |
|
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset
|
18 |
syntax finite :: 'a set => bool |
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset
|
19 |
translations "finite A" == "A : Finites" |
923 | 20 |
|
5626 | 21 |
(* This definition, although traditional, is ugly to work with |
1556 | 22 |
constdefs |
23 |
card :: 'a set => nat |
|
24 |
"card A == LEAST n. ? f. A = {f i |i. i<n}" |
|
5626 | 25 |
Therefore we have switched to an inductive one: |
26 |
*) |
|
27 |
||
28 |
consts cardR :: "('a set * nat) set" |
|
29 |
||
30 |
inductive cardR |
|
31 |
intrs |
|
32 |
EmptyI "({},0) : cardR" |
|
33 |
InsertI "[| (A,n) : cardR; a ~: A |] ==> (insert a A, Suc n) : cardR" |
|
34 |
||
35 |
constdefs |
|
36 |
card :: 'a set => nat |
|
37 |
"card A == @n. (A,n) : cardR" |
|
1531 | 38 |
|
5616 | 39 |
(* |
40 |
A "fold" functional for finite sets. For n non-negative we have |
|
41 |
fold f e {x1,...,xn} = f x1 (... (f xn e)) |
|
42 |
where f is at least left-commutative. |
|
43 |
*) |
|
44 |
||
45 |
consts foldSet :: "[['b,'a] => 'a, 'a] => ('b set * 'a) set" |
|
46 |
||
47 |
inductive "foldSet f e" |
|
48 |
intrs |
|
49 |
emptyI "({}, e) : foldSet f e" |
|
50 |
||
51 |
insertI "[| x ~: A; (A,y) : foldSet f e |] |
|
52 |
==> (insert x A, f x y) : foldSet f e" |
|
53 |
||
54 |
constdefs |
|
55 |
fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a" |
|
56 |
"fold f e A == @x. (A,x) : foldSet f e" |
|
57 |
(* A frequent instance: *) |
|
58 |
setsum :: ('a => nat) => 'a set => nat |
|
59 |
"setsum f == fold (op+ o f) 0" |
|
60 |
||
61 |
locale LC = |
|
62 |
fixes |
|
63 |
f :: ['b,'a] => 'a |
|
64 |
assumes |
|
5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset
|
65 |
lcomm "f x (f y z) = f y (f x z)" |
5616 | 66 |
|
67 |
locale ACe = |
|
68 |
fixes |
|
69 |
f :: ['a,'a] => 'a |
|
70 |
e :: 'a |
|
71 |
assumes |
|
5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset
|
72 |
ident "f x e = x" |
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset
|
73 |
commute "f x y = f y x" |
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset
|
74 |
assoc "f (f x y) z = f x (f y z)" |
5616 | 75 |
|
923 | 76 |
end |