author | kleing |
Mon, 15 Oct 2001 21:04:32 +0200 | |
changeset 11787 | 85b3735a51e1 |
parent 11786 | 51ce34ef5113 |
child 12114 | a8e860c86252 |
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 |
||
8962 | 9 |
Finite = Divides + Power + Inductive + SetInterval + |
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 |
|
7958 | 21 |
axclass finite<term |
22 |
finite "finite UNIV" |
|
23 |
||
5626 | 24 |
(* This definition, although traditional, is ugly to work with |
1556 | 25 |
constdefs |
26 |
card :: 'a set => nat |
|
27 |
"card A == LEAST n. ? f. A = {f i |i. i<n}" |
|
5626 | 28 |
Therefore we have switched to an inductive one: |
29 |
*) |
|
30 |
||
31 |
consts cardR :: "('a set * nat) set" |
|
32 |
||
33 |
inductive cardR |
|
34 |
intrs |
|
35 |
EmptyI "({},0) : cardR" |
|
36 |
InsertI "[| (A,n) : cardR; a ~: A |] ==> (insert a A, Suc n) : cardR" |
|
37 |
||
38 |
constdefs |
|
11786 | 39 |
card :: 'a set => nat |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11092
diff
changeset
|
40 |
"card A == THE n. (A,n) : cardR" |
1531 | 41 |
|
5616 | 42 |
(* |
43 |
A "fold" functional for finite sets. For n non-negative we have |
|
44 |
fold f e {x1,...,xn} = f x1 (... (f xn e)) |
|
45 |
where f is at least left-commutative. |
|
46 |
*) |
|
47 |
||
48 |
consts foldSet :: "[['b,'a] => 'a, 'a] => ('b set * 'a) set" |
|
49 |
||
50 |
inductive "foldSet f e" |
|
51 |
intrs |
|
52 |
emptyI "({}, e) : foldSet f e" |
|
53 |
||
54 |
insertI "[| x ~: A; (A,y) : foldSet f e |] |
|
55 |
==> (insert x A, f x y) : foldSet f e" |
|
56 |
||
57 |
constdefs |
|
11786 | 58 |
fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a" |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11092
diff
changeset
|
59 |
"fold f e A == THE x. (A,x) : foldSet f e" |
8962 | 60 |
|
11786 | 61 |
setsum :: "('a => 'b) => 'a set => 'b::plus_ac0" |
9087 | 62 |
"setsum f A == if finite A then fold (op+ o f) 0 A else 0" |
5616 | 63 |
|
11786 | 64 |
syntax |
65 |
"_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\\<Sum>_:_. _" [0, 51, 10] 10) |
|
66 |
syntax (symbols) |
|
67 |
"_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\\<Sum>_\\<in>_. _" [0, 51, 10] 10) |
|
68 |
translations |
|
69 |
"\\<Sum>i:A. b" == "setsum (%i. b) A" (* Beware of argument permutation! *) |
|
70 |
||
71 |
||
5616 | 72 |
locale LC = |
73 |
fixes |
|
74 |
f :: ['b,'a] => 'a |
|
75 |
assumes |
|
5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset
|
76 |
lcomm "f x (f y z) = f y (f x z)" |
5616 | 77 |
|
78 |
locale ACe = |
|
79 |
fixes |
|
80 |
f :: ['a,'a] => 'a |
|
81 |
e :: 'a |
|
82 |
assumes |
|
5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset
|
83 |
ident "f x e = x" |
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset
|
84 |
commute "f x y = f y x" |
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset
|
85 |
assoc "f (f x y) z = f x (f y z)" |
5616 | 86 |
|
923 | 87 |
end |