6065
|
1 |
(* Title: ZF/Tools/datatype_package.ML
|
6052
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1994 University of Cambridge
|
|
5 |
|
6065
|
6 |
Datatype/Codatatype Definitions
|
6052
|
7 |
|
|
8 |
The functor will be instantiated for normal sums/products (datatype defs)
|
|
9 |
and non-standard sums/products (codatatype defs)
|
|
10 |
|
|
11 |
Sums are used only for mutual recursion;
|
|
12 |
Products are used only to derive "streamlined" induction rules for relations
|
|
13 |
*)
|
|
14 |
|
|
15 |
|
|
16 |
type datatype_result =
|
|
17 |
{con_defs : thm list, (*definitions made in thy*)
|
|
18 |
case_eqns : thm list, (*equations for case operator*)
|
|
19 |
recursor_eqns : thm list, (*equations for the recursor*)
|
|
20 |
free_iffs : thm list, (*freeness rewrite rules*)
|
|
21 |
free_SEs : thm list, (*freeness destruct rules*)
|
|
22 |
mk_free : string -> thm}; (*makes freeness theorems*)
|
|
23 |
|
|
24 |
|
|
25 |
signature DATATYPE_ARG =
|
|
26 |
sig
|
|
27 |
val intrs : thm list
|
|
28 |
val elims : thm list
|
|
29 |
end;
|
|
30 |
|
|
31 |
|
|
32 |
(*Functor's result signature*)
|
|
33 |
signature DATATYPE_PACKAGE =
|
|
34 |
sig
|
|
35 |
|
|
36 |
(*Insert definitions for the recursive sets, which
|
|
37 |
must *already* be declared as constants in parent theory!*)
|
|
38 |
val add_datatype_i :
|
|
39 |
term * term list * Ind_Syntax.constructor_spec list list *
|
|
40 |
thm list * thm list * thm list
|
|
41 |
-> theory -> theory * inductive_result * datatype_result
|
|
42 |
|
|
43 |
val add_datatype :
|
|
44 |
string * string list *
|
|
45 |
(string * string list * mixfix) list list *
|
|
46 |
thm list * thm list * thm list
|
|
47 |
-> theory -> theory * inductive_result * datatype_result
|
|
48 |
|
|
49 |
end;
|
|
50 |
|
|
51 |
|
|
52 |
(*Declares functions to add fixedpoint/constructor defs to a theory.
|
|
53 |
Recursive sets must *already* be declared as constants.*)
|
|
54 |
functor Add_datatype_def_Fun
|
|
55 |
(structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU
|
|
56 |
and Ind_Package : INDUCTIVE_PACKAGE
|
|
57 |
and Datatype_Arg : DATATYPE_ARG)
|
|
58 |
: DATATYPE_PACKAGE =
|
|
59 |
struct
|
|
60 |
|
|
61 |
|
|
62 |
(*con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
|
|
63 |
fun add_datatype_i (dom_sum, rec_tms, con_ty_lists,
|
|
64 |
monos, type_intrs, type_elims) thy =
|
|
65 |
let
|
|
66 |
open BasisLibrary
|
|
67 |
val dummy = (*has essential ancestors?*)
|
|
68 |
Theory.requires thy "Datatype" "(co)datatype definitions";
|
|
69 |
|
|
70 |
|
|
71 |
val rec_names = map (#1 o dest_Const o head_of) rec_tms
|
|
72 |
val rec_base_names = map Sign.base_name rec_names
|
|
73 |
val big_rec_base_name = space_implode "_" rec_base_names
|
|
74 |
|
|
75 |
val thy_path = thy |> Theory.add_path big_rec_base_name
|
|
76 |
val sign = sign_of thy_path
|
|
77 |
|
|
78 |
val big_rec_name = Sign.intern_const sign big_rec_base_name;
|
|
79 |
|
|
80 |
val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists)
|
|
81 |
|
|
82 |
val dummy =
|
|
83 |
writeln ((if (#1 (dest_Const Fp.oper) = "lfp") then "Datatype"
|
|
84 |
else "Codatatype")
|
|
85 |
^ " definition " ^ big_rec_name)
|
|
86 |
|
|
87 |
val case_varname = "f"; (*name for case variables*)
|
|
88 |
|
|
89 |
(** Define the constructors **)
|
|
90 |
|
|
91 |
(*The empty tuple is 0*)
|
|
92 |
fun mk_tuple [] = Const("0",iT)
|
|
93 |
| mk_tuple args = foldr1 (app Pr.pair) args;
|
|
94 |
|
|
95 |
fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k;
|
|
96 |
|
|
97 |
val npart = length rec_names; (*number of mutually recursive parts*)
|
|
98 |
|
|
99 |
|
|
100 |
val full_name = Sign.full_name sign;
|
|
101 |
|
|
102 |
(*Make constructor definition;
|
|
103 |
kpart is the number of this mutually recursive part*)
|
|
104 |
fun mk_con_defs (kpart, con_ty_list) =
|
|
105 |
let val ncon = length con_ty_list (*number of constructors*)
|
|
106 |
fun mk_def (((id,T,syn), name, args, prems), kcon) =
|
|
107 |
(*kcon is index of constructor*)
|
|
108 |
Logic.mk_defpair (list_comb (Const (full_name name, T), args),
|
|
109 |
mk_inject npart kpart
|
|
110 |
(mk_inject ncon kcon (mk_tuple args)))
|
|
111 |
in ListPair.map mk_def (con_ty_list, 1 upto ncon) end;
|
|
112 |
|
|
113 |
|
|
114 |
(*** Define the case operator ***)
|
|
115 |
|
|
116 |
(*Combine split terms using case; yields the case operator for one part*)
|
|
117 |
fun call_case case_list =
|
|
118 |
let fun call_f (free,[]) = Abs("null", iT, free)
|
|
119 |
| call_f (free,args) =
|
|
120 |
CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
|
|
121 |
Ind_Syntax.iT
|
|
122 |
free
|
|
123 |
in fold_bal (app Su.elim) (map call_f case_list) end;
|
|
124 |
|
|
125 |
(** Generating function variables for the case definition
|
|
126 |
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
|
|
127 |
|
|
128 |
(*The function variable for a single constructor*)
|
|
129 |
fun add_case (((_, T, _), name, args, _), (opno, cases)) =
|
|
130 |
if Syntax.is_identifier name then
|
|
131 |
(opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases)
|
|
132 |
else
|
|
133 |
(opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args)
|
|
134 |
:: cases);
|
|
135 |
|
|
136 |
(*Treatment of a list of constructors, for one part
|
|
137 |
Result adds a list of terms, each a function variable with arguments*)
|
|
138 |
fun add_case_list (con_ty_list, (opno, case_lists)) =
|
|
139 |
let val (opno', case_list) = foldr add_case (con_ty_list, (opno, []))
|
|
140 |
in (opno', case_list :: case_lists) end;
|
|
141 |
|
|
142 |
(*Treatment of all parts*)
|
|
143 |
val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
|
|
144 |
|
|
145 |
(*extract the types of all the variables*)
|
|
146 |
val case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
|
|
147 |
|
|
148 |
val case_base_name = big_rec_base_name ^ "_case";
|
|
149 |
val case_name = full_name case_base_name;
|
|
150 |
|
|
151 |
(*The list of all the function variables*)
|
|
152 |
val case_args = flat (map (map #1) case_lists);
|
|
153 |
|
|
154 |
val case_const = Const (case_name, case_typ);
|
|
155 |
val case_tm = list_comb (case_const, case_args);
|
|
156 |
|
|
157 |
val case_def = Logic.mk_defpair
|
|
158 |
(case_tm, fold_bal (app Su.elim) (map call_case case_lists));
|
|
159 |
|
|
160 |
|
|
161 |
(** Generating function variables for the recursor definition
|
|
162 |
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
|
|
163 |
|
|
164 |
(*a recursive call for x is the application rec`x *)
|
|
165 |
val rec_call = Ind_Syntax.apply_const $ Free ("rec", iT);
|
|
166 |
|
|
167 |
(*look back down the "case args" (which have been reversed) to
|
|
168 |
determine the de Bruijn index*)
|
|
169 |
fun make_rec_call ([], _) arg = error
|
|
170 |
"Internal error in datatype (variable name mismatch)"
|
|
171 |
| make_rec_call (a::args, i) arg =
|
|
172 |
if a = arg then rec_call $ Bound i
|
|
173 |
else make_rec_call (args, i+1) arg;
|
|
174 |
|
|
175 |
(*creates one case of the "X_case" definition of the recursor*)
|
|
176 |
fun call_recursor ((case_var, case_args), (recursor_var, recursor_args)) =
|
|
177 |
let fun add_abs (Free(a,T), u) = Abs(a,T,u)
|
|
178 |
val ncase_args = length case_args
|
|
179 |
val bound_args = map Bound ((ncase_args - 1) downto 0)
|
|
180 |
val rec_args = map (make_rec_call (rev case_args,0))
|
|
181 |
(List.drop(recursor_args, ncase_args))
|
|
182 |
in
|
|
183 |
foldr add_abs
|
|
184 |
(case_args, list_comb (recursor_var,
|
|
185 |
bound_args @ rec_args))
|
|
186 |
end
|
|
187 |
|
|
188 |
(*Find each recursive argument and add a recursive call for it*)
|
|
189 |
fun rec_args [] = []
|
|
190 |
| rec_args ((Const("op :",_)$arg$X)::prems) =
|
|
191 |
(case head_of X of
|
|
192 |
Const(a,_) => (*recursive occurrence?*)
|
6065
|
193 |
if a mem_string rec_names
|
6052
|
194 |
then arg :: rec_args prems
|
|
195 |
else rec_args prems
|
|
196 |
| _ => rec_args prems)
|
|
197 |
| rec_args (_::prems) = rec_args prems;
|
|
198 |
|
|
199 |
(*Add an argument position for each occurrence of a recursive set.
|
|
200 |
Strictly speaking, the recursive arguments are the LAST of the function
|
|
201 |
variable, but they all have type "i" anyway*)
|
|
202 |
fun add_rec_args args' T = (map (fn _ => iT) args') ---> T
|
|
203 |
|
|
204 |
(*Plug in the function variable type needed for the recursor
|
|
205 |
as well as the new arguments (recursive calls)*)
|
|
206 |
fun rec_ty_elem ((id, T, syn), name, args, prems) =
|
|
207 |
let val args' = rec_args prems
|
|
208 |
in ((id, add_rec_args args' T, syn),
|
|
209 |
name, args @ args', prems)
|
|
210 |
end;
|
|
211 |
|
|
212 |
val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists);
|
|
213 |
|
|
214 |
(*Treatment of all parts*)
|
|
215 |
val (_, recursor_lists) = foldr add_case_list (rec_ty_lists, (1,[]));
|
|
216 |
|
|
217 |
(*extract the types of all the variables*)
|
|
218 |
val recursor_typ = flat (map (map (#2 o #1)) rec_ty_lists)
|
|
219 |
---> (iT-->iT);
|
|
220 |
|
|
221 |
val recursor_base_name = big_rec_base_name ^ "_rec";
|
|
222 |
val recursor_name = full_name recursor_base_name;
|
|
223 |
|
|
224 |
(*The list of all the function variables*)
|
|
225 |
val recursor_args = flat (map (map #1) recursor_lists);
|
|
226 |
|
|
227 |
val recursor_tm =
|
|
228 |
list_comb (Const (recursor_name, recursor_typ), recursor_args);
|
|
229 |
|
|
230 |
val recursor_cases = map call_recursor
|
|
231 |
(flat case_lists ~~ flat recursor_lists)
|
|
232 |
|
|
233 |
val recursor_def =
|
|
234 |
Logic.mk_defpair
|
|
235 |
(recursor_tm,
|
|
236 |
Ind_Syntax.Vrecursor_const $
|
|
237 |
absfree ("rec", iT, list_comb (case_const, recursor_cases)));
|
|
238 |
|
|
239 |
(* Build the new theory *)
|
|
240 |
|
|
241 |
val need_recursor =
|
|
242 |
(#1 (dest_Const Fp.oper) = "lfp" andalso recursor_typ <> case_typ);
|
|
243 |
|
|
244 |
fun add_recursor thy =
|
|
245 |
if need_recursor then
|
|
246 |
thy |> Theory.add_consts_i
|
|
247 |
[(recursor_base_name, recursor_typ, NoSyn)]
|
6092
|
248 |
|> PureThy.add_defs_i [Thm.no_attributes recursor_def]
|
6052
|
249 |
else thy;
|
|
250 |
|
|
251 |
val thy0 = thy_path
|
|
252 |
|> Theory.add_consts_i
|
|
253 |
((case_base_name, case_typ, NoSyn) ::
|
|
254 |
map #1 (flat con_ty_lists))
|
|
255 |
|> PureThy.add_defs_i
|
6092
|
256 |
(map Thm.no_attributes
|
6052
|
257 |
(case_def ::
|
|
258 |
flat (ListPair.map mk_con_defs
|
|
259 |
(1 upto npart, con_ty_lists))))
|
|
260 |
|> add_recursor
|
|
261 |
|> Theory.parent_path
|
|
262 |
|
|
263 |
val con_defs = get_def thy0 case_name ::
|
|
264 |
map (get_def thy0 o #2) (flat con_ty_lists);
|
|
265 |
|
|
266 |
val (thy1, ind_result) =
|
|
267 |
thy0 |> Ind_Package.add_inductive_i
|
|
268 |
false (rec_tms, dom_sum, intr_tms,
|
|
269 |
monos, con_defs,
|
|
270 |
type_intrs @ Datatype_Arg.intrs,
|
|
271 |
type_elims @ Datatype_Arg.elims)
|
|
272 |
|
|
273 |
(**** Now prove the datatype theorems in this theory ****)
|
|
274 |
|
|
275 |
|
|
276 |
(*** Prove the case theorems ***)
|
|
277 |
|
|
278 |
(*Each equation has the form
|
|
279 |
case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
|
|
280 |
fun mk_case_eqn (((_,T,_), name, args, _), case_free) =
|
|
281 |
FOLogic.mk_Trueprop
|
|
282 |
(FOLogic.mk_eq
|
|
283 |
(case_tm $
|
|
284 |
(list_comb (Const (Sign.intern_const (sign_of thy1) name,T),
|
|
285 |
args)),
|
|
286 |
list_comb (case_free, args)));
|
|
287 |
|
|
288 |
val case_trans = hd con_defs RS Ind_Syntax.def_trans
|
|
289 |
and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
|
|
290 |
|
|
291 |
(*Proves a single case equation. Could use simp_tac, but it's slower!*)
|
|
292 |
fun case_tacsf con_def _ =
|
|
293 |
[rewtac con_def,
|
|
294 |
rtac case_trans 1,
|
|
295 |
REPEAT (resolve_tac [refl, split_trans,
|
|
296 |
Su.case_inl RS trans,
|
|
297 |
Su.case_inr RS trans] 1)];
|
|
298 |
|
|
299 |
fun prove_case_eqn (arg,con_def) =
|
|
300 |
prove_goalw_cterm []
|
|
301 |
(Ind_Syntax.traceIt "next case equation = "
|
|
302 |
(cterm_of (sign_of thy1) (mk_case_eqn arg)))
|
|
303 |
(case_tacsf con_def);
|
|
304 |
|
|
305 |
val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
|
|
306 |
|
|
307 |
val case_eqns =
|
|
308 |
map prove_case_eqn
|
|
309 |
(flat con_ty_lists ~~ case_args ~~ tl con_defs);
|
|
310 |
|
|
311 |
(*** Prove the recursor theorems ***)
|
|
312 |
|
|
313 |
val recursor_eqns = case try (get_def thy1) recursor_base_name of
|
|
314 |
None => (writeln " [ No recursion operator ]";
|
|
315 |
[])
|
|
316 |
| Some recursor_def =>
|
|
317 |
let
|
|
318 |
(*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *)
|
|
319 |
fun subst_rec (Const("op `",_) $ Free _ $ arg) = recursor_tm $ arg
|
|
320 |
| subst_rec tm =
|
|
321 |
let val (head, args) = strip_comb tm
|
|
322 |
in list_comb (head, map subst_rec args) end;
|
|
323 |
|
|
324 |
(*Each equation has the form
|
|
325 |
REC(coni(args)) = f_coni(args, REC(rec_arg), ...)
|
|
326 |
where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive
|
|
327 |
constructor argument.*)
|
|
328 |
fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) =
|
|
329 |
FOLogic.mk_Trueprop
|
|
330 |
(FOLogic.mk_eq
|
|
331 |
(recursor_tm $
|
|
332 |
(list_comb (Const (Sign.intern_const (sign_of thy1) name,T),
|
|
333 |
args)),
|
|
334 |
subst_rec (foldl betapply (recursor_case, args))));
|
|
335 |
|
|
336 |
val recursor_trans = recursor_def RS def_Vrecursor RS trans;
|
|
337 |
|
|
338 |
(*Proves a single recursor equation.*)
|
|
339 |
fun recursor_tacsf _ =
|
|
340 |
[rtac recursor_trans 1,
|
|
341 |
simp_tac (rank_ss addsimps case_eqns) 1,
|
|
342 |
IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)];
|
|
343 |
|
|
344 |
fun prove_recursor_eqn arg =
|
|
345 |
prove_goalw_cterm []
|
|
346 |
(Ind_Syntax.traceIt "next recursor equation = "
|
|
347 |
(cterm_of (sign_of thy1) (mk_recursor_eqn arg)))
|
|
348 |
recursor_tacsf
|
|
349 |
in
|
|
350 |
map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases)
|
|
351 |
end
|
|
352 |
|
|
353 |
val constructors =
|
|
354 |
map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
|
|
355 |
|
|
356 |
val free_iffs = con_iffs @
|
|
357 |
[Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
|
|
358 |
|
|
359 |
val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs;
|
|
360 |
|
|
361 |
val {elim, induct, mutual_induct, ...} = ind_result
|
|
362 |
|
|
363 |
(*Typical theorems have the form ~con1=con2, con1=con2==>False,
|
|
364 |
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
|
|
365 |
fun mk_free s =
|
|
366 |
prove_goalw (theory_of_thm elim) (*Don't use thy1: it will be stale*)
|
|
367 |
con_defs s
|
|
368 |
(fn prems => [cut_facts_tac prems 1,
|
|
369 |
fast_tac (ZF_cs addSEs free_SEs) 1]);
|
|
370 |
|
|
371 |
val simps = case_eqns @ recursor_eqns;
|
|
372 |
|
|
373 |
val dt_info =
|
|
374 |
{inductive = true,
|
|
375 |
constructors = constructors,
|
|
376 |
rec_rewrites = recursor_eqns,
|
|
377 |
case_rewrites = case_eqns,
|
|
378 |
induct = induct,
|
|
379 |
mutual_induct = mutual_induct,
|
|
380 |
exhaustion = elim};
|
|
381 |
|
|
382 |
val con_info =
|
|
383 |
{big_rec_name = big_rec_name,
|
|
384 |
constructors = constructors,
|
|
385 |
(*let primrec handle definition by cases*)
|
|
386 |
rec_rewrites = (case recursor_eqns of
|
|
387 |
[] => case_eqns | _ => recursor_eqns)};
|
|
388 |
|
|
389 |
(*associate with each constructor the datatype name and rewrites*)
|
|
390 |
val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
|
|
391 |
|
|
392 |
in
|
|
393 |
(*Updating theory components: simprules and datatype info*)
|
|
394 |
(thy1 |> Theory.add_path big_rec_base_name
|
6092
|
395 |
|> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
|
6052
|
396 |
|> DatatypesData.put
|
|
397 |
(Symtab.update
|
|
398 |
((big_rec_name, dt_info), DatatypesData.get thy1))
|
|
399 |
|> ConstructorsData.put
|
|
400 |
(foldr Symtab.update (con_pairs, ConstructorsData.get thy1))
|
|
401 |
|> Theory.parent_path,
|
|
402 |
ind_result,
|
|
403 |
{con_defs = con_defs,
|
|
404 |
case_eqns = case_eqns,
|
|
405 |
recursor_eqns = recursor_eqns,
|
|
406 |
free_iffs = free_iffs,
|
|
407 |
free_SEs = free_SEs,
|
|
408 |
mk_free = mk_free})
|
|
409 |
end;
|
|
410 |
|
|
411 |
|
|
412 |
fun add_datatype (sdom, srec_tms, scon_ty_lists,
|
|
413 |
monos, type_intrs, type_elims) thy =
|
|
414 |
let val sign = sign_of thy
|
|
415 |
val rec_tms = map (readtm sign Ind_Syntax.iT) srec_tms
|
|
416 |
val dom_sum =
|
|
417 |
if sdom = "" then
|
|
418 |
Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "lfp") rec_tms
|
|
419 |
else readtm sign Ind_Syntax.iT sdom
|
|
420 |
and con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
|
|
421 |
in
|
|
422 |
add_datatype_i (dom_sum, rec_tms, con_ty_lists,
|
|
423 |
monos, type_intrs, type_elims) thy
|
|
424 |
end
|
|
425 |
|
|
426 |
end;
|