|
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 |