|
1 (* Title: ZF/co-inductive.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Co-inductive Definitions for Zermelo-Fraenkel Set Theory |
|
7 |
|
8 Uses greatest fixedpoints with Quine-inspired products and sums |
|
9 |
|
10 Sums are used only for mutual recursion; |
|
11 Products are used only to derive "streamlined" induction rules for relations |
|
12 *) |
|
13 |
|
14 structure Gfp = |
|
15 struct |
|
16 val oper = Const("gfp", [iT,iT-->iT]--->iT) |
|
17 val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT) |
|
18 val bnd_monoI = bnd_monoI |
|
19 val subs = def_gfp_subset |
|
20 val Tarski = def_gfp_Tarski |
|
21 val induct = def_Collect_coinduct |
|
22 end; |
|
23 |
|
24 structure Quine_Prod = |
|
25 struct |
|
26 val sigma = Const("QSigma", [iT, iT-->iT]--->iT) |
|
27 val pair = Const("QPair", [iT,iT]--->iT) |
|
28 val split_const = Const("qsplit", [[iT,iT]--->iT, iT]--->iT) |
|
29 val fsplit_const = Const("qfsplit", [[iT,iT]--->oT, iT]--->oT) |
|
30 val pair_iff = QPair_iff |
|
31 val split_eq = qsplit |
|
32 val fsplitI = qfsplitI |
|
33 val fsplitD = qfsplitD |
|
34 val fsplitE = qfsplitE |
|
35 end; |
|
36 |
|
37 structure Quine_Sum = |
|
38 struct |
|
39 val sum = Const("op <+>", [iT,iT]--->iT) |
|
40 val inl = Const("QInl", iT-->iT) |
|
41 val inr = Const("QInr", iT-->iT) |
|
42 val elim = Const("qcase", [iT-->iT, iT-->iT, iT]--->iT) |
|
43 val case_inl = qcase_QInl |
|
44 val case_inr = qcase_QInr |
|
45 val inl_iff = QInl_iff |
|
46 val inr_iff = QInr_iff |
|
47 val distinct = QInl_QInr_iff |
|
48 val distinct' = QInr_QInl_iff |
|
49 end; |
|
50 |
|
51 signature CO_INDRULE = |
|
52 sig |
|
53 val co_induct : thm |
|
54 end; |
|
55 |
|
56 |
|
57 functor Co_Inductive_Fun (Ind: INDUCTIVE) |
|
58 : sig include INTR_ELIM CO_INDRULE end = |
|
59 struct |
|
60 structure Intr_elim = |
|
61 Intr_elim_Fun(structure Ind=Ind and Fp=Gfp and |
|
62 Pr=Quine_Prod and Su=Quine_Sum); |
|
63 |
|
64 open Intr_elim |
|
65 val co_induct = raw_induct |
|
66 end; |
|
67 |