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 (Co)Inductive Definitions for Zermelo-Fraenkel Set Theory |
|
7 |
|
8 Inductive definitions use least fixedpoints with standard products and sums |
|
9 Coinductive definitions use greatest fixedpoints with Quine products and sums |
|
10 |
|
11 Sums are used only for mutual recursion; |
|
12 Products are used only to derive "streamlined" induction rules for relations |
|
13 *) |
|
14 |
|
15 local open Ind_Syntax |
|
16 in |
|
17 structure Lfp = |
|
18 struct |
|
19 val oper = Const("lfp", [iT,iT-->iT]--->iT) |
|
20 val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT) |
|
21 val bnd_monoI = bnd_monoI |
|
22 val subs = def_lfp_subset |
|
23 val Tarski = def_lfp_Tarski |
|
24 val induct = def_induct |
|
25 end; |
|
26 |
|
27 structure Standard_Prod = |
|
28 struct |
|
29 val sigma = Const("Sigma", [iT, iT-->iT]--->iT) |
|
30 val pair = Const("Pair", [iT,iT]--->iT) |
|
31 val split_const = Const("split", [[iT,iT]--->iT, iT]--->iT) |
|
32 val fsplit_const = Const("fsplit", [[iT,iT]--->oT, iT]--->oT) |
|
33 val pair_iff = Pair_iff |
|
34 val split_eq = split |
|
35 val fsplitI = fsplitI |
|
36 val fsplitD = fsplitD |
|
37 val fsplitE = fsplitE |
|
38 end; |
|
39 |
|
40 structure Standard_Sum = |
|
41 struct |
|
42 val sum = Const("op +", [iT,iT]--->iT) |
|
43 val inl = Const("Inl", iT-->iT) |
|
44 val inr = Const("Inr", iT-->iT) |
|
45 val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT) |
|
46 val case_inl = case_Inl |
|
47 val case_inr = case_Inr |
|
48 val inl_iff = Inl_iff |
|
49 val inr_iff = Inr_iff |
|
50 val distinct = Inl_Inr_iff |
|
51 val distinct' = Inr_Inl_iff |
|
52 end; |
|
53 end; |
|
54 |
|
55 functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) |
|
56 : sig include INTR_ELIM INDRULE end = |
|
57 struct |
|
58 structure Intr_elim = |
|
59 Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and |
|
60 Pr=Standard_Prod and Su=Standard_Sum); |
|
61 |
|
62 structure Indrule = Indrule_Fun (structure Inductive=Inductive and |
|
63 Pr=Standard_Prod and Intr_elim=Intr_elim); |
|
64 |
|
65 open Intr_elim Indrule |
|
66 end; |
|
67 |
|
68 |
|
69 structure Ind = Add_inductive_def_Fun |
|
70 (structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum); |
|
71 |
|
72 |
|
73 signature INDUCTIVE_STRING = |
|
74 sig |
|
75 val thy_name : string (*name of the new theory*) |
|
76 val rec_doms : (string*string) list (*recursion terms and their domains*) |
|
77 val sintrs : string list (*desired introduction rules*) |
|
78 end; |
|
79 |
|
80 |
|
81 (*For upwards compatibility: can be called directly from ML*) |
|
82 functor Inductive_Fun |
|
83 (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end) |
|
84 : sig include INTR_ELIM INDRULE end = |
|
85 Ind_section_Fun |
|
86 (open Inductive Ind_Syntax |
|
87 val sign = sign_of thy; |
|
88 val rec_tms = map (readtm sign iT o #1) rec_doms |
|
89 and domts = map (readtm sign iT o #2) rec_doms |
|
90 and intr_tms = map (readtm sign propT) sintrs; |
|
91 val thy = thy |> Ind.add_fp_def_i(rec_tms, domts, intr_tms) |
|
92 |> add_thyname thy_name); |
|
93 |
|
94 |
|
95 |
|
96 local open Ind_Syntax |
|
97 in |
|
98 structure Gfp = |
|
99 struct |
|
100 val oper = Const("gfp", [iT,iT-->iT]--->iT) |
|
101 val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT) |
|
102 val bnd_monoI = bnd_monoI |
|
103 val subs = def_gfp_subset |
|
104 val Tarski = def_gfp_Tarski |
|
105 val induct = def_Collect_coinduct |
|
106 end; |
|
107 |
|
108 structure Quine_Prod = |
|
109 struct |
|
110 val sigma = Const("QSigma", [iT, iT-->iT]--->iT) |
|
111 val pair = Const("QPair", [iT,iT]--->iT) |
|
112 val split_const = Const("qsplit", [[iT,iT]--->iT, iT]--->iT) |
|
113 val fsplit_const = Const("qfsplit", [[iT,iT]--->oT, iT]--->oT) |
|
114 val pair_iff = QPair_iff |
|
115 val split_eq = qsplit |
|
116 val fsplitI = qfsplitI |
|
117 val fsplitD = qfsplitD |
|
118 val fsplitE = qfsplitE |
|
119 end; |
|
120 |
|
121 structure Quine_Sum = |
|
122 struct |
|
123 val sum = Const("op <+>", [iT,iT]--->iT) |
|
124 val inl = Const("QInl", iT-->iT) |
|
125 val inr = Const("QInr", iT-->iT) |
|
126 val elim = Const("qcase", [iT-->iT, iT-->iT, iT]--->iT) |
|
127 val case_inl = qcase_QInl |
|
128 val case_inr = qcase_QInr |
|
129 val inl_iff = QInl_iff |
|
130 val inr_iff = QInr_iff |
|
131 val distinct = QInl_QInr_iff |
|
132 val distinct' = QInr_QInl_iff |
|
133 end; |
|
134 end; |
|
135 |
|
136 |
|
137 signature COINDRULE = |
|
138 sig |
|
139 val coinduct : thm |
|
140 end; |
|
141 |
|
142 |
|
143 functor CoInd_section_Fun |
|
144 (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) |
|
145 : sig include INTR_ELIM COINDRULE end = |
|
146 struct |
|
147 structure Intr_elim = |
|
148 Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and |
|
149 Pr=Quine_Prod and Su=Quine_Sum); |
|
150 |
|
151 open Intr_elim |
|
152 val coinduct = raw_induct |
|
153 end; |
|
154 |
|
155 |
|
156 structure CoInd = |
|
157 Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum); |
|
158 |
|
159 |
|
160 (*For upwards compatibility: can be called directly from ML*) |
|
161 functor CoInductive_Fun |
|
162 (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end) |
|
163 : sig include INTR_ELIM COINDRULE end = |
|
164 CoInd_section_Fun |
|
165 (open Inductive Ind_Syntax |
|
166 val sign = sign_of thy; |
|
167 val rec_tms = map (readtm sign iT o #1) rec_doms |
|
168 and domts = map (readtm sign iT o #2) rec_doms |
|
169 and intr_tms = map (readtm sign propT) sintrs; |
|
170 val thy = thy |> CoInd.add_fp_def_i(rec_tms, domts, intr_tms) |
|
171 |> add_thyname thy_name); |
|
172 |
|
173 |
|
174 |
|
175 (*For installing the theory section. co is either "" or "Co"*) |
|
176 fun inductive_decl co = |
|
177 let open ThyParse Ind_Syntax |
|
178 fun mk_intr_name (s,_) = (*the "op" cancels any infix status*) |
|
179 if Syntax.is_identifier s then "op " ^ s else "_" |
|
180 fun mk_params (((((domains: (string*string) list, ipairs), |
|
181 monos), con_defs), type_intrs), type_elims) = |
|
182 let val big_rec_name = space_implode "_" |
|
183 (map (scan_to_id o trim o #1) domains) |
|
184 and srec_tms = mk_list (map #1 domains) |
|
185 and sdoms = mk_list (map #2 domains) |
|
186 and sintrs = mk_big_list (map snd ipairs) |
|
187 val stri_name = big_rec_name ^ "_Intrnl" |
|
188 in |
|
189 (";\n\n\ |
|
190 \structure " ^ stri_name ^ " =\n\ |
|
191 \ let open Ind_Syntax in\n\ |
|
192 \ struct\n\ |
|
193 \ val rec_tms\t= map (readtm (sign_of thy) iT) " |
|
194 ^ srec_tms ^ "\n\ |
|
195 \ and domts\t= map (readtm (sign_of thy) iT) " |
|
196 ^ sdoms ^ "\n\ |
|
197 \ and intr_tms\t= map (readtm (sign_of thy) propT)\n" |
|
198 ^ sintrs ^ "\n\ |
|
199 \ end\n\ |
|
200 \ end;\n\n\ |
|
201 \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n (" ^ |
|
202 stri_name ^ ".rec_tms, " ^ |
|
203 stri_name ^ ".domts, " ^ |
|
204 stri_name ^ ".intr_tms)" |
|
205 , |
|
206 "structure " ^ big_rec_name ^ " =\n\ |
|
207 \ struct\n\ |
|
208 \ val _ = writeln \"" ^ co ^ |
|
209 "Inductive definition " ^ big_rec_name ^ "\"\n\ |
|
210 \ structure Result = " ^ co ^ "Ind_section_Fun\n\ |
|
211 \ (open " ^ stri_name ^ "\n\ |
|
212 \ val thy\t\t= thy\n\ |
|
213 \ val monos\t\t= " ^ monos ^ "\n\ |
|
214 \ val con_defs\t\t= " ^ con_defs ^ "\n\ |
|
215 \ val type_intrs\t= " ^ type_intrs ^ "\n\ |
|
216 \ val type_elims\t= " ^ type_elims ^ ");\n\n\ |
|
217 \ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\ |
|
218 \ open Result\n\ |
|
219 \ end\n" |
|
220 ) |
|
221 end |
|
222 val domains = "domains" $$-- repeat1 (string --$$ "<=" -- !! string) |
|
223 val ipairs = "intrs" $$-- repeat1 (ident -- !! string) |
|
224 fun optstring s = optional (s $$-- string) "\"[]\"" >> trim |
|
225 in domains -- ipairs -- optstring "monos" -- optstring "con_defs" |
|
226 -- optstring "type_intrs" -- optstring "type_elims" |
|
227 >> mk_params |
|
228 end; |
|