|
1 (* Title: ZF/inductive.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Inductive Definitions for Zermelo-Fraenkel Set Theory |
|
7 |
|
8 Uses least fixedpoints with standard 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 |
|
15 structure Lfp = |
|
16 struct |
|
17 val oper = Const("lfp", [iT,iT-->iT]--->iT) |
|
18 val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT) |
|
19 val bnd_monoI = bnd_monoI |
|
20 val subs = def_lfp_subset |
|
21 val Tarski = def_lfp_Tarski |
|
22 val induct = def_induct |
|
23 end; |
|
24 |
|
25 structure Standard_Prod = |
|
26 struct |
|
27 val sigma = Const("Sigma", [iT, iT-->iT]--->iT) |
|
28 val pair = Const("Pair", [iT,iT]--->iT) |
|
29 val split_const = Const("split", [[iT,iT]--->iT, iT]--->iT) |
|
30 val fsplit_const = Const("fsplit", [[iT,iT]--->oT, iT]--->oT) |
|
31 val pair_iff = Pair_iff |
|
32 val split_eq = split |
|
33 val fsplitI = fsplitI |
|
34 val fsplitD = fsplitD |
|
35 val fsplitE = fsplitE |
|
36 end; |
|
37 |
|
38 structure Standard_Sum = |
|
39 struct |
|
40 val sum = Const("op +", [iT,iT]--->iT) |
|
41 val inl = Const("Inl", iT-->iT) |
|
42 val inr = Const("Inr", iT-->iT) |
|
43 val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT) |
|
44 val case_inl = case_Inl |
|
45 val case_inr = case_Inr |
|
46 val inl_iff = Inl_iff |
|
47 val inr_iff = Inr_iff |
|
48 val distinct = Inl_Inr_iff |
|
49 val distinct' = Inr_Inl_iff |
|
50 end; |
|
51 |
|
52 functor Inductive_Fun (Ind: INDUCTIVE) : sig include INTR_ELIM INDRULE end = |
|
53 struct |
|
54 structure Intr_elim = |
|
55 Intr_elim_Fun(structure Ind=Ind and Fp=Lfp and |
|
56 Pr=Standard_Prod and Su=Standard_Sum); |
|
57 |
|
58 structure Indrule = Indrule_Fun (structure Ind=Ind and |
|
59 Pr=Standard_Prod and Intr_elim=Intr_elim); |
|
60 |
|
61 open Intr_elim Indrule |
|
62 end; |
|
63 |