| author | wenzelm |
| Tue, 16 Jul 2002 18:37:03 +0200 | |
| changeset 13368 | 8f8ba32d148b |
| parent 13194 | 812b00ed1c03 |
| child 14046 | 6616e6c53d48 |
| permissions | -rw-r--r-- |
| 12610 | 1 |
(* Title: ZF/Induct/FoldSet.thy |
|
12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
3 |
Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
4 |
|
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
5 |
|
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
6 |
A "fold" functional for finite sets. For n non-negative we have |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
7 |
fold f e {x1,...,xn} = f x1 (... (f xn e)) where f is at
|
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
8 |
least left-commutative. |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
9 |
*) |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
10 |
|
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
11 |
FoldSet = Main + |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
12 |
|
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
13 |
consts fold_set :: "[i, i, [i,i]=>i, i] => i" |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
14 |
|
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
15 |
inductive |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
16 |
domains "fold_set(A, B, f,e)" <= "Fin(A)*B" |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
17 |
intrs |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
18 |
emptyI "e:B ==> <0, e>:fold_set(A, B, f,e)" |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
19 |
consI "[| x:A; x ~:C; <C,y> : fold_set(A, B,f,e); f(x,y):B |] |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
20 |
==> <cons(x,C), f(x,y)>:fold_set(A, B, f, e)" |
| 13194 | 21 |
type_intrs "Fin_intros" |
|
12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
22 |
|
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
23 |
constdefs |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
24 |
|
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
25 |
fold :: "[i, [i,i]=>i, i, i] => i" ("fold[_]'(_,_,_')")
|
|
12860
7fc3fbfed8ef
Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents:
12610
diff
changeset
|
26 |
"fold[B](f,e, A) == THE x. <A, x>:fold_set(A, B, f,e)" |
|
12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
27 |
|
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
28 |
setsum :: "[i=>i, i] => i" |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
29 |
"setsum(g, C) == if Finite(C) then |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
30 |
fold[int](%x y. g(x) $+ y, #0, C) else #0" |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
31 |
end |