0
|
1 |
(* Title: ZF/constructor.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
|
6 |
Constructor function module -- for Datatype Definitions
|
|
7 |
|
|
8 |
Defines constructors and a case-style eliminator (no primitive recursion)
|
|
9 |
|
|
10 |
Features:
|
|
11 |
* least or greatest fixedpoints
|
|
12 |
* user-specified product and sum constructions
|
|
13 |
* mutually recursive datatypes
|
|
14 |
* recursion over arbitrary monotone operators
|
|
15 |
* flexible: can derive any reasonable set of introduction rules
|
|
16 |
* automatically constructs a case analysis operator (but no recursion op)
|
|
17 |
* efficient treatment of large declarations (e.g. 60 constructors)
|
|
18 |
*)
|
|
19 |
|
|
20 |
(** STILL NEEDS: some treatment of recursion **)
|
|
21 |
|
|
22 |
signature CONSTRUCTOR =
|
|
23 |
sig
|
|
24 |
val thy : theory (*parent theory*)
|
|
25 |
val rec_specs : (string * string * (string list * string)list) list
|
|
26 |
(*recursion ops, types, domains, constructors*)
|
|
27 |
val rec_styp : string (*common type of all recursion ops*)
|
|
28 |
val ext : Syntax.sext option (*syntax extension for new theory*)
|
|
29 |
val sintrs : string list (*desired introduction rules*)
|
|
30 |
val monos : thm list (*monotonicity of each M operator*)
|
|
31 |
val type_intrs : thm list (*type-checking intro rules*)
|
|
32 |
val type_elims : thm list (*type-checking elim rules*)
|
|
33 |
end;
|
|
34 |
|
|
35 |
signature CONSTRUCTOR_RESULT =
|
|
36 |
sig
|
|
37 |
val con_thy : theory (*theory defining the constructors*)
|
|
38 |
val con_defs : thm list (*definitions made in con_thy*)
|
|
39 |
val case_eqns : thm list (*equations for case operator*)
|
|
40 |
val free_iffs : thm list (*freeness rewrite rules*)
|
|
41 |
val free_SEs : thm list (*freeness destruct rules*)
|
|
42 |
val mk_free : string -> thm (*makes freeness theorems*)
|
|
43 |
val congs : thm list (*congruence rules for simplifier*)
|
|
44 |
end;
|
|
45 |
|
|
46 |
|
|
47 |
functor Constructor_Fun (structure Const: CONSTRUCTOR and
|
|
48 |
Pr : PR and Su : SU) : CONSTRUCTOR_RESULT =
|
|
49 |
struct
|
|
50 |
open Logic Const;
|
|
51 |
|
|
52 |
val dummy = writeln"Defining the constructor functions...";
|
|
53 |
|
|
54 |
val case_name = "f"; (*name for case variables*)
|
|
55 |
|
|
56 |
(** Extract basic information from arguments **)
|
|
57 |
|
|
58 |
val sign = sign_of thy;
|
|
59 |
val rdty = Sign.typ_of o Sign.read_ctyp sign;
|
|
60 |
|
|
61 |
val rec_names = map #1 rec_specs;
|
|
62 |
|
|
63 |
val dummy = assert_all Syntax.is_identifier rec_names
|
|
64 |
(fn a => "Name of recursive set not an identifier: " ^ a);
|
|
65 |
|
|
66 |
(*Expands multiple constant declarations*)
|
|
67 |
fun pairtypes (cs,st) = map (rpair st) cs;
|
|
68 |
|
|
69 |
(*Constructors with types and arguments*)
|
|
70 |
fun mk_con_ty_list cons_pairs =
|
|
71 |
let fun mk_con_ty (a,st) =
|
|
72 |
let val T = rdty st
|
|
73 |
val args = mk_frees "xa" (binder_types T)
|
|
74 |
in (a,T,args) end
|
|
75 |
in map mk_con_ty (flat (map pairtypes cons_pairs)) end;
|
|
76 |
|
|
77 |
val con_ty_lists = map (mk_con_ty_list o #3) rec_specs;
|
|
78 |
|
|
79 |
(** Define the constructors **)
|
|
80 |
|
|
81 |
(*We identify 0 (the empty set) with the empty tuple*)
|
|
82 |
fun mk_tuple [] = Const("0",iT)
|
|
83 |
| mk_tuple args = foldr1 (app Pr.pair) args;
|
|
84 |
|
|
85 |
fun mk_inject n k u = access_bal(ap Su.inl, ap Su.inr, u) n k;
|
|
86 |
|
|
87 |
val npart = length rec_names; (*number of mutually recursive parts*)
|
|
88 |
|
|
89 |
(*Make constructor definition*)
|
|
90 |
fun mk_con_defs (kpart, con_ty_list) =
|
|
91 |
let val ncon = length con_ty_list (*number of constructors*)
|
|
92 |
fun mk_def ((a,T,args), kcon) = (*kcon = index of this constructor*)
|
|
93 |
mk_defpair sign
|
|
94 |
(list_comb (Const(a,T), args),
|
|
95 |
mk_inject npart kpart (mk_inject ncon kcon (mk_tuple args)))
|
|
96 |
in map mk_def (con_ty_list ~~ (1 upto ncon)) end;
|
|
97 |
|
|
98 |
(** Define the case operator **)
|
|
99 |
|
|
100 |
(*Combine split terms using case; yields the case operator for one part*)
|
|
101 |
fun call_case case_list =
|
|
102 |
let fun call_f (free,args) =
|
|
103 |
ap_split Pr.split_const free (map (#2 o dest_Free) args)
|
|
104 |
in fold_bal (app Su.elim) (map call_f case_list) end;
|
|
105 |
|
|
106 |
(** Generating function variables for the case definition
|
|
107 |
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
|
|
108 |
|
|
109 |
(*Treatment of a single constructor*)
|
|
110 |
fun add_case ((a,T,args), (opno,cases)) =
|
|
111 |
if Syntax.is_identifier a
|
|
112 |
then (opno,
|
|
113 |
(Free(case_name ^ "_" ^ a, T), args) :: cases)
|
|
114 |
else (opno+1,
|
|
115 |
(Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: cases);
|
|
116 |
|
|
117 |
(*Treatment of a list of constructors, for one part*)
|
|
118 |
fun add_case_list (con_ty_list, (opno,case_lists)) =
|
|
119 |
let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))
|
|
120 |
in (opno', case_list :: case_lists) end;
|
|
121 |
|
|
122 |
(*Treatment of all parts*)
|
|
123 |
val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
|
|
124 |
|
|
125 |
val big_case_typ = flat (map (map #2) con_ty_lists) ---> (iT-->iT);
|
|
126 |
|
|
127 |
val big_rec_name = space_implode "_" rec_names;
|
|
128 |
|
|
129 |
val big_case_name = big_rec_name ^ "_case";
|
|
130 |
|
|
131 |
(*The list of all the function variables*)
|
|
132 |
val big_case_args = flat (map (map #1) case_lists);
|
|
133 |
|
|
134 |
val big_case_tm =
|
|
135 |
list_comb (Const(big_case_name, big_case_typ), big_case_args);
|
|
136 |
|
|
137 |
val big_case_def =
|
|
138 |
mk_defpair sign
|
|
139 |
(big_case_tm, fold_bal (app Su.elim) (map call_case case_lists));
|
|
140 |
|
|
141 |
(** Build the new theory **)
|
|
142 |
|
|
143 |
val axpairs =
|
|
144 |
big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists));
|
|
145 |
|
|
146 |
val const_decs = remove_mixfixes ext
|
|
147 |
(([big_case_name], flatten_typ sign big_case_typ) ::
|
|
148 |
(big_rec_name ins rec_names, rec_styp) ::
|
|
149 |
flat (map #3 rec_specs));
|
|
150 |
|
|
151 |
val con_thy = extend_theory thy (big_rec_name ^ "_Constructors")
|
|
152 |
([], [], [], [], const_decs, ext) axpairs;
|
|
153 |
|
|
154 |
(*1st element is the case definition; others are the constructors*)
|
|
155 |
val con_defs = map (get_axiom con_thy o #1) axpairs;
|
|
156 |
|
|
157 |
(** Prove the case theorem **)
|
|
158 |
|
|
159 |
(*Each equation has the form
|
|
160 |
rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
|
|
161 |
fun mk_case_equation ((a,T,args), case_free) =
|
|
162 |
mk_tprop
|
|
163 |
(eq_const $ (big_case_tm $ (list_comb (Const(a,T), args)))
|
|
164 |
$ (list_comb (case_free, args)));
|
|
165 |
|
|
166 |
val case_trans = hd con_defs RS def_trans;
|
|
167 |
|
|
168 |
(*proves a single case equation*)
|
|
169 |
fun case_tacsf con_def _ =
|
|
170 |
[rewtac con_def,
|
|
171 |
rtac case_trans 1,
|
|
172 |
REPEAT (resolve_tac [refl, Pr.split_eq RS trans,
|
|
173 |
Su.case_inl RS trans,
|
|
174 |
Su.case_inr RS trans] 1)];
|
|
175 |
|
|
176 |
fun prove_case_equation (arg,con_def) =
|
|
177 |
prove_term (sign_of con_thy) []
|
|
178 |
(mk_case_equation arg, case_tacsf con_def);
|
|
179 |
|
|
180 |
val free_iffs =
|
|
181 |
map standard (con_defs RL [def_swap_iff]) @
|
|
182 |
[Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
|
|
183 |
|
|
184 |
val free_SEs = map (gen_make_elim [conjE,FalseE]) (free_iffs RL [iffD1]);
|
|
185 |
|
|
186 |
val free_cs = ZF_cs addSEs free_SEs;
|
|
187 |
|
|
188 |
(*Typical theorems have the form ~con1=con2, con1=con2==>False,
|
|
189 |
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
|
|
190 |
fun mk_free s =
|
|
191 |
prove_goalw con_thy con_defs s
|
|
192 |
(fn prems => [cut_facts_tac prems 1, fast_tac free_cs 1]);
|
|
193 |
|
|
194 |
val case_eqns = map prove_case_equation
|
|
195 |
(flat con_ty_lists ~~ big_case_args ~~ tl con_defs);
|
|
196 |
|
|
197 |
val congs = mk_congs con_thy (flat (map #1 (const_decs @ ext_constants ext)));
|
|
198 |
end;
|
|
199 |
|
|
200 |
|