|
1 theory Nominal2 |
|
2 imports |
|
3 "../Nominal-General/Nominal2_Base" |
|
4 "../Nominal-General/Nominal2_Eqvt" |
|
5 "../Nominal-General/Nominal2_Supp" |
|
6 "Nominal2_FSet" |
|
7 "Abs" |
|
8 uses ("nominal_dt_rawperm.ML") |
|
9 ("nominal_dt_rawfuns.ML") |
|
10 ("nominal_dt_alpha.ML") |
|
11 ("nominal_dt_quot.ML") |
|
12 ("nominal_dt_supp.ML") |
|
13 begin |
|
14 |
|
15 use "nominal_dt_rawperm.ML" |
|
16 ML {* open Nominal_Dt_RawPerm *} |
|
17 |
|
18 use "nominal_dt_rawfuns.ML" |
|
19 ML {* open Nominal_Dt_RawFuns *} |
|
20 |
|
21 use "nominal_dt_alpha.ML" |
|
22 ML {* open Nominal_Dt_Alpha *} |
|
23 |
|
24 use "nominal_dt_quot.ML" |
|
25 ML {* open Nominal_Dt_Quot *} |
|
26 |
|
27 use "nominal_dt_supp.ML" |
|
28 ML {* open Nominal_Dt_Supp *} |
|
29 |
|
30 section{* Interface for nominal_datatype *} |
|
31 |
|
32 ML {* |
|
33 (* attributes *) |
|
34 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
|
35 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
|
36 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
|
37 |
|
38 *} |
|
39 |
|
40 ML {* print_depth 50 *} |
|
41 |
|
42 ML {* |
|
43 fun get_cnstrs dts = |
|
44 map (fn (_, _, _, constrs) => constrs) dts |
|
45 |
|
46 fun get_typed_cnstrs dts = |
|
47 flat (map (fn (_, bn, _, constrs) => |
|
48 (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts) |
|
49 |
|
50 fun get_cnstr_strs dts = |
|
51 map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts)) |
|
52 |
|
53 fun get_bn_fun_strs bn_funs = |
|
54 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs |
|
55 *} |
|
56 |
|
57 |
|
58 text {* Infrastructure for adding "_raw" to types and terms *} |
|
59 |
|
60 ML {* |
|
61 fun add_raw s = s ^ "_raw" |
|
62 fun add_raws ss = map add_raw ss |
|
63 fun raw_bind bn = Binding.suffix_name "_raw" bn |
|
64 |
|
65 fun replace_str ss s = |
|
66 case (AList.lookup (op=) ss s) of |
|
67 SOME s' => s' |
|
68 | NONE => s |
|
69 |
|
70 fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts) |
|
71 | replace_typ ty_ss T = T |
|
72 |
|
73 fun raw_dts ty_ss dts = |
|
74 let |
|
75 fun raw_dts_aux1 (bind, tys, mx) = |
|
76 (raw_bind bind, map (replace_typ ty_ss) tys, mx) |
|
77 |
|
78 fun raw_dts_aux2 (ty_args, bind, mx, constrs) = |
|
79 (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs) |
|
80 in |
|
81 map raw_dts_aux2 dts |
|
82 end |
|
83 |
|
84 fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T) |
|
85 | replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T) |
|
86 | replace_aterm trm_ss trm = trm |
|
87 |
|
88 fun replace_term trm_ss ty_ss trm = |
|
89 trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) |
|
90 *} |
|
91 |
|
92 ML {* |
|
93 fun rawify_dts dt_names dts dts_env = |
|
94 let |
|
95 val raw_dts = raw_dts dts_env dts |
|
96 val raw_dt_names = add_raws dt_names |
|
97 in |
|
98 (raw_dt_names, raw_dts) |
|
99 end |
|
100 *} |
|
101 |
|
102 ML {* |
|
103 fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = |
|
104 let |
|
105 val bn_funs' = map (fn (bn, ty, mx) => |
|
106 (raw_bind bn, SOME (replace_typ dts_env ty), mx)) bn_funs |
|
107 |
|
108 val bn_eqs' = map (fn (attr, trm) => |
|
109 (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs |
|
110 in |
|
111 (bn_funs', bn_eqs') |
|
112 end |
|
113 *} |
|
114 |
|
115 ML {* |
|
116 fun rawify_bclauses dts_env cnstrs_env bn_fun_env bclauses = |
|
117 let |
|
118 fun rawify_bnds bnds = |
|
119 map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds |
|
120 |
|
121 fun rawify_bclause (BC (mode, bnds, bdys)) = BC (mode, rawify_bnds bnds, bdys) |
|
122 in |
|
123 map (map (map rawify_bclause)) bclauses |
|
124 end |
|
125 *} |
|
126 |
|
127 (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or |
|
128 appends of elements; in case of recursive calls it retruns also the applied |
|
129 bn function *) |
|
130 ML {* |
|
131 fun strip_bn_fun lthy args t = |
|
132 let |
|
133 fun aux t = |
|
134 case t of |
|
135 Const (@{const_name sup}, _) $ l $ r => aux l @ aux r |
|
136 | Const (@{const_name append}, _) $ l $ r => aux l @ aux r |
|
137 | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => |
|
138 (find_index (equal x) args, NONE) :: aux y |
|
139 | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => |
|
140 (find_index (equal x) args, NONE) :: aux y |
|
141 | Const (@{const_name bot}, _) => [] |
|
142 | Const (@{const_name Nil}, _) => [] |
|
143 | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)] |
|
144 | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t)) |
|
145 in |
|
146 aux t |
|
147 end |
|
148 *} |
|
149 |
|
150 ML {* |
|
151 (** definition of the raw binding functions **) |
|
152 |
|
153 (* TODO: needs cleaning *) |
|
154 fun find [] _ = error ("cannot find element") |
|
155 | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y |
|
156 |
|
157 fun prep_bn_info lthy dt_names dts eqs = |
|
158 let |
|
159 fun aux eq = |
|
160 let |
|
161 val (lhs, rhs) = eq |
|
162 |> HOLogic.dest_Trueprop |
|
163 |> HOLogic.dest_eq |
|
164 val (bn_fun, [cnstr]) = strip_comb lhs |
|
165 val (_, ty) = dest_Const bn_fun |
|
166 val (ty_name, _) = dest_Type (domain_type ty) |
|
167 val dt_index = find_index (fn x => x = ty_name) dt_names |
|
168 val (cnstr_head, cnstr_args) = strip_comb cnstr |
|
169 val rhs_elements = strip_bn_fun lthy cnstr_args rhs |
|
170 in |
|
171 (dt_index, (bn_fun, (cnstr_head, rhs_elements))) |
|
172 end |
|
173 fun order dts i ts = |
|
174 let |
|
175 val dt = nth dts i |
|
176 val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) |
|
177 val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts |
|
178 in |
|
179 map (find ts') cts |
|
180 end |
|
181 |
|
182 val unordered = AList.group (op=) (map aux eqs) |
|
183 val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered |
|
184 val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' |
|
185 val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) |
|
186 |
|
187 (*val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))*) |
|
188 (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*) |
|
189 (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*) |
|
190 in |
|
191 ordered' |
|
192 end |
|
193 |
|
194 |
|
195 fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy = |
|
196 if null raw_bn_funs |
|
197 then ([], [], [], [], lthy) |
|
198 else |
|
199 let |
|
200 val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs |
|
201 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
|
202 |
|
203 val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1) |
|
204 val {fs, simps, inducts, ...} = info |
|
205 |
|
206 val raw_bn_induct = (the inducts) |
|
207 val raw_bn_eqs = the simps |
|
208 |
|
209 val raw_bn_info = |
|
210 prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs) |
|
211 in |
|
212 (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) |
|
213 end |
|
214 *} |
|
215 |
|
216 ML {* |
|
217 fun define_raw_dts dts bn_funs bn_eqs binds lthy = |
|
218 let |
|
219 val thy = Local_Theory.exit_global lthy |
|
220 val thy_name = Context.theory_name thy |
|
221 |
|
222 val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts |
|
223 val dt_full_names = map (Long_Name.qualify thy_name) dt_names |
|
224 val dt_full_names' = add_raws dt_full_names |
|
225 val dts_env = dt_full_names ~~ dt_full_names' |
|
226 |
|
227 val cnstrs = get_cnstr_strs dts |
|
228 val cnstrs_ty = get_typed_cnstrs dts |
|
229 val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs |
|
230 val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name |
|
231 (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty |
|
232 val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names' |
|
233 |
|
234 val bn_fun_strs = get_bn_fun_strs bn_funs |
|
235 val bn_fun_strs' = add_raws bn_fun_strs |
|
236 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' |
|
237 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) |
|
238 (bn_fun_strs ~~ bn_fun_strs') |
|
239 |
|
240 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
|
241 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
|
242 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
|
243 |
|
244 val (raw_dt_full_names, thy1) = |
|
245 Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy |
|
246 |
|
247 val lthy1 = Named_Target.theory_init thy1 |
|
248 in |
|
249 (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) |
|
250 end |
|
251 *} |
|
252 |
|
253 |
|
254 ML {* |
|
255 (* for testing porposes - to exit the procedure early *) |
|
256 exception TEST of Proof.context |
|
257 |
|
258 val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 100); |
|
259 |
|
260 fun get_STEPS ctxt = Config.get ctxt STEPS |
|
261 *} |
|
262 |
|
263 setup STEPS_setup |
|
264 |
|
265 ML {* |
|
266 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = |
|
267 let |
|
268 (* definition of the raw datatypes *) |
|
269 val _ = warning "Definition of raw datatypes"; |
|
270 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
|
271 if get_STEPS lthy > 0 |
|
272 then define_raw_dts dts bn_funs bn_eqs bclauses lthy |
|
273 else raise TEST lthy |
|
274 |
|
275 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
|
276 val {descr, sorts, ...} = dtinfo |
|
277 |
|
278 val raw_tys = all_dtyps descr sorts |
|
279 val raw_full_ty_names = map (fst o dest_Type) raw_tys |
|
280 val tvs = hd raw_tys |
|
281 |> snd o dest_Type |
|
282 |> map dest_TFree |
|
283 |
|
284 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names |
|
285 |
|
286 val raw_cns_info = all_dtyp_constrs_types descr sorts |
|
287 val raw_constrs = flat (map (map (fn (c, _, _, _) => c)) raw_cns_info) |
|
288 |
|
289 val raw_inject_thms = flat (map #inject dtinfos) |
|
290 val raw_distinct_thms = flat (map #distinct dtinfos) |
|
291 val raw_induct_thm = #induct dtinfo |
|
292 val raw_induct_thms = #inducts dtinfo |
|
293 val raw_exhaust_thms = map #exhaust dtinfos |
|
294 val raw_size_trms = map size_const raw_tys |
|
295 val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) |
|
296 |> `(fn thms => (length thms) div 2) |
|
297 |> uncurry drop |
|
298 |
|
299 (* definitions of raw permutations by primitive recursion *) |
|
300 val _ = warning "Definition of raw permutations"; |
|
301 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = |
|
302 if get_STEPS lthy0 > 1 |
|
303 then define_raw_perms raw_full_ty_names raw_tys tvs raw_constrs raw_induct_thm lthy0 |
|
304 else raise TEST lthy0 |
|
305 |
|
306 (* noting the raw permutations as eqvt theorems *) |
|
307 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a |
|
308 |
|
309 (* definition of raw fv_functions *) |
|
310 val _ = warning "Definition of raw fv-functions"; |
|
311 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) = |
|
312 if get_STEPS lthy3 > 2 |
|
313 then define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
|
314 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
|
315 else raise TEST lthy3 |
|
316 |
|
317 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = |
|
318 if get_STEPS lthy3a > 3 |
|
319 then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses |
|
320 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a |
|
321 else raise TEST lthy3a |
|
322 |
|
323 (* definition of raw alphas *) |
|
324 val _ = warning "Definition of alphas"; |
|
325 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
|
326 if get_STEPS lthy3b > 4 |
|
327 then define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3b |
|
328 else raise TEST lthy3b |
|
329 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
|
330 |
|
331 (* definition of alpha-distinct lemmas *) |
|
332 val _ = warning "Distinct theorems"; |
|
333 val alpha_distincts = |
|
334 mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys |
|
335 |
|
336 (* definition of alpha_eq_iff lemmas *) |
|
337 (* they have a funny shape for the simplifier ---- CHECK WHETHER NEEDED*) |
|
338 val _ = warning "Eq-iff theorems"; |
|
339 val (alpha_eq_iff_simps, alpha_eq_iff) = |
|
340 if get_STEPS lthy > 5 |
|
341 then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases |
|
342 else raise TEST lthy4 |
|
343 |
|
344 (* proving equivariance lemmas for bns, fvs, size and alpha *) |
|
345 val _ = warning "Proving equivariance"; |
|
346 val raw_bn_eqvt = |
|
347 if get_STEPS lthy > 6 |
|
348 then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_defs @ raw_perm_simps) lthy4 |
|
349 else raise TEST lthy4 |
|
350 |
|
351 (* noting the raw_bn_eqvt lemmas in a temprorary theory *) |
|
352 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) lthy4) |
|
353 |
|
354 val raw_fv_eqvt = |
|
355 if get_STEPS lthy > 7 |
|
356 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) |
|
357 (Local_Theory.restore lthy_tmp) |
|
358 else raise TEST lthy4 |
|
359 |
|
360 val raw_size_eqvt = |
|
361 if get_STEPS lthy > 8 |
|
362 then raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) |
|
363 (Local_Theory.restore lthy_tmp) |
|
364 |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) |
|
365 |> map (fn thm => thm RS @{thm sym}) |
|
366 else raise TEST lthy4 |
|
367 |
|
368 val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) |
|
369 |
|
370 val (alpha_eqvt, lthy6) = |
|
371 if get_STEPS lthy > 9 |
|
372 then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 |
|
373 else raise TEST lthy4 |
|
374 |
|
375 (* proving alpha equivalence *) |
|
376 val _ = warning "Proving equivalence" |
|
377 |
|
378 val alpha_refl_thms = |
|
379 if get_STEPS lthy > 10 |
|
380 then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy6 |
|
381 else raise TEST lthy6 |
|
382 |
|
383 val alpha_sym_thms = |
|
384 if get_STEPS lthy > 11 |
|
385 then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy6 |
|
386 else raise TEST lthy6 |
|
387 |
|
388 val alpha_trans_thms = |
|
389 if get_STEPS lthy > 12 |
|
390 then raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms) |
|
391 alpha_intros alpha_induct alpha_cases lthy6 |
|
392 else raise TEST lthy6 |
|
393 |
|
394 val (alpha_equivp_thms, alpha_bn_equivp_thms) = |
|
395 if get_STEPS lthy > 13 |
|
396 then raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms |
|
397 alpha_trans_thms lthy6 |
|
398 else raise TEST lthy6 |
|
399 |
|
400 (* proving alpha implies alpha_bn *) |
|
401 val _ = warning "Proving alpha implies bn" |
|
402 |
|
403 val alpha_bn_imp_thms = |
|
404 if get_STEPS lthy > 14 |
|
405 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 |
|
406 else raise TEST lthy6 |
|
407 |
|
408 (* respectfulness proofs *) |
|
409 val raw_funs_rsp_aux = |
|
410 if get_STEPS lthy > 15 |
|
411 then raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
|
412 raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6 |
|
413 else raise TEST lthy6 |
|
414 |
|
415 val raw_funs_rsp = |
|
416 if get_STEPS lthy > 16 |
|
417 then map mk_funs_rsp raw_funs_rsp_aux |
|
418 else raise TEST lthy6 |
|
419 |
|
420 val raw_size_rsp = |
|
421 if get_STEPS lthy > 17 |
|
422 then |
|
423 raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct |
|
424 (raw_size_thms @ raw_size_eqvt) lthy6 |
|
425 |> map mk_funs_rsp |
|
426 else raise TEST lthy6 |
|
427 |
|
428 val raw_constrs_rsp = |
|
429 if get_STEPS lthy > 18 |
|
430 then raw_constrs_rsp raw_constrs alpha_trms alpha_intros |
|
431 (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 |
|
432 else raise TEST lthy6 |
|
433 |
|
434 val alpha_permute_rsp = |
|
435 if get_STEPS lthy > 19 |
|
436 then map mk_alpha_permute_rsp alpha_eqvt |
|
437 else raise TEST lthy6 |
|
438 |
|
439 val alpha_bn_rsp = |
|
440 if get_STEPS lthy > 20 |
|
441 then raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms |
|
442 else raise TEST lthy6 |
|
443 |
|
444 (* noting the quot_respects lemmas *) |
|
445 val (_, lthy6a) = |
|
446 if get_STEPS lthy > 21 |
|
447 then Local_Theory.note ((Binding.empty, [rsp_attr]), |
|
448 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6 |
|
449 else raise TEST lthy6 |
|
450 |
|
451 (* defining the quotient type *) |
|
452 val _ = warning "Declaring the quotient types" |
|
453 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
|
454 |
|
455 val (qty_infos, lthy7) = |
|
456 if get_STEPS lthy > 22 |
|
457 then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a |
|
458 else raise TEST lthy6a |
|
459 |
|
460 val qtys = map #qtyp qty_infos |
|
461 val qty_full_names = map (fst o dest_Type) qtys |
|
462 val qty_names = map Long_Name.base_name qty_full_names |
|
463 |
|
464 (* defining of quotient term-constructors, binding functions, free vars functions *) |
|
465 val _ = warning "Defining the quotient constants" |
|
466 val qconstrs_descr = |
|
467 flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) |
|
468 |> map2 (fn t => fn (b, mx) => (b, t, mx)) raw_constrs |
|
469 |
|
470 val qbns_descr = |
|
471 map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns |
|
472 |
|
473 val qfvs_descr = |
|
474 map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs |
|
475 |
|
476 val qfv_bns_descr = |
|
477 map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns |
|
478 |
|
479 val qalpha_bns_descr = |
|
480 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms |
|
481 |
|
482 val qperm_descr = |
|
483 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs |
|
484 |
|
485 val qsize_descr = |
|
486 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
|
487 |
|
488 val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = |
|
489 if get_STEPS lthy > 23 |
|
490 then |
|
491 lthy7 |
|
492 |> define_qconsts qtys qconstrs_descr |
|
493 ||>> define_qconsts qtys qbns_descr |
|
494 ||>> define_qconsts qtys qfvs_descr |
|
495 ||>> define_qconsts qtys qfv_bns_descr |
|
496 ||>> define_qconsts qtys qalpha_bns_descr |
|
497 else raise TEST lthy7 |
|
498 |
|
499 (* definition of the quotient permfunctions and pt-class *) |
|
500 val lthy9 = |
|
501 if get_STEPS lthy > 24 |
|
502 then define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 |
|
503 else raise TEST lthy8 |
|
504 |
|
505 val lthy9a = |
|
506 if get_STEPS lthy > 25 |
|
507 then define_qsizes qtys qty_full_names tvs qsize_descr lthy9 |
|
508 else raise TEST lthy9 |
|
509 |
|
510 val qtrms = map #qconst qconstrs_info |
|
511 val qbns = map #qconst qbns_info |
|
512 val qfvs = map #qconst qfvs_info |
|
513 val qfv_bns = map #qconst qfv_bns_info |
|
514 val qalpha_bns = map #qconst qalpha_bns_info |
|
515 |
|
516 (* lifting of the theorems *) |
|
517 val _ = warning "Lifting of Theorems" |
|
518 |
|
519 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
|
520 prod.cases} |
|
521 |
|
522 val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = |
|
523 if get_STEPS lthy > 26 |
|
524 then |
|
525 lthy9a |
|
526 |> lift_thms qtys [] alpha_distincts |
|
527 ||>> lift_thms qtys eq_iff_simps alpha_eq_iff |
|
528 ||>> lift_thms qtys [] raw_fv_defs |
|
529 ||>> lift_thms qtys [] raw_bn_defs |
|
530 ||>> lift_thms qtys [] raw_perm_simps |
|
531 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
|
532 else raise TEST lthy9a |
|
533 |
|
534 val (((qsize_eqvt, [qinduct]), qexhausts), lthyB) = |
|
535 if get_STEPS lthy > 27 |
|
536 then |
|
537 lthyA |
|
538 |> lift_thms qtys [] raw_size_eqvt |
|
539 ||>> lift_thms qtys [] [raw_induct_thm] |
|
540 ||>> lift_thms qtys [] raw_exhaust_thms |
|
541 else raise TEST lthyA |
|
542 |
|
543 (* supports lemmas *) |
|
544 val qsupports_thms = |
|
545 if get_STEPS lthy > 28 |
|
546 then prove_supports lthyB qperm_simps qtrms |
|
547 else raise TEST lthyB |
|
548 |
|
549 (* finite supp lemmas *) |
|
550 val qfsupp_thms = |
|
551 if get_STEPS lthy > 29 |
|
552 then prove_fsupp lthyB qtys qinduct qsupports_thms |
|
553 else raise TEST lthyB |
|
554 |
|
555 (* fs instances *) |
|
556 val lthyC = |
|
557 if get_STEPS lthy > 30 |
|
558 then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB |
|
559 else raise TEST lthyB |
|
560 |
|
561 (* noting the theorems *) |
|
562 |
|
563 (* generating the prefix for the theorem names *) |
|
564 val thms_name = |
|
565 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
|
566 fun thms_suffix s = Binding.qualified true s thms_name |
|
567 |
|
568 val (_, lthy9') = lthyC |
|
569 |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) |
|
570 ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs) |
|
571 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
|
572 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
|
573 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
|
574 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
|
575 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
|
576 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
|
577 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
|
578 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
|
579 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
|
580 in |
|
581 (0, lthy9') |
|
582 end handle TEST ctxt => (0, ctxt) |
|
583 *} |
|
584 |
|
585 section {* Preparing and parsing of the specification *} |
|
586 |
|
587 ML {* |
|
588 (* generates the parsed datatypes and |
|
589 declares the constructors |
|
590 *) |
|
591 fun prepare_dts dt_strs thy = |
|
592 let |
|
593 fun inter_fs_sort thy (a, S) = |
|
594 (a, Type.inter_sort (Sign.tsig_of thy) (@{sort fs}, S)) |
|
595 |
|
596 fun mk_type tname sorts (cname, cargs, mx) = |
|
597 let |
|
598 val full_tname = Sign.full_name thy tname |
|
599 val ty = Type (full_tname, map (TFree o inter_fs_sort thy) sorts) |
|
600 in |
|
601 (cname, cargs ---> ty, mx) |
|
602 end |
|
603 |
|
604 fun prep_constr (cname, cargs, mx, _) (constrs, sorts) = |
|
605 let |
|
606 val (cargs', sorts') = |
|
607 fold_map (Datatype.read_typ thy) (map snd cargs) sorts |
|
608 |>> map (map_type_tfree (TFree o inter_fs_sort thy)) |
|
609 in |
|
610 (constrs @ [(cname, cargs', mx)], sorts') |
|
611 end |
|
612 |
|
613 fun prep_dts (tvs, tname, mx, constrs) (constr_trms, dts, sorts) = |
|
614 let |
|
615 val (constrs', sorts') = |
|
616 fold prep_constr constrs ([], sorts) |
|
617 |
|
618 val constr_trms' = |
|
619 map (mk_type tname (rev sorts')) constrs' |
|
620 in |
|
621 (constr_trms @ constr_trms', dts @ [(tvs, tname, mx, constrs')], sorts') |
|
622 end |
|
623 |
|
624 val (constr_trms, dts, sorts) = fold prep_dts dt_strs ([], [], []); |
|
625 in |
|
626 thy |
|
627 |> Sign.add_consts_i constr_trms |
|
628 |> pair dts |
|
629 end |
|
630 *} |
|
631 |
|
632 ML {* |
|
633 (* parsing the binding function specification and *) |
|
634 (* declaring the functions in the local theory *) |
|
635 fun prepare_bn_funs bn_fun_strs bn_eq_strs thy = |
|
636 let |
|
637 val lthy = Named_Target.theory_init thy |
|
638 |
|
639 val ((bn_funs, bn_eqs), lthy') = |
|
640 Specification.read_spec bn_fun_strs bn_eq_strs lthy |
|
641 |
|
642 fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) |
|
643 |
|
644 val bn_funs' = map prep_bn_fun bn_funs |
|
645 in |
|
646 (Local_Theory.exit_global lthy') |
|
647 |> Sign.add_consts_i bn_funs' |
|
648 |> pair (bn_funs', bn_eqs) |
|
649 end |
|
650 *} |
|
651 |
|
652 text {* associates every SOME with the index in the list; drops NONEs *} |
|
653 ML {* |
|
654 fun indexify xs = |
|
655 let |
|
656 fun mapp _ [] = [] |
|
657 | mapp i (NONE :: xs) = mapp (i + 1) xs |
|
658 | mapp i (SOME x :: xs) = (x, i) :: mapp (i + 1) xs |
|
659 in |
|
660 mapp 0 xs |
|
661 end |
|
662 |
|
663 fun index_lookup xs x = |
|
664 case AList.lookup (op=) xs x of |
|
665 SOME x => x |
|
666 | NONE => error ("Cannot find " ^ x ^ " as argument annotation."); |
|
667 *} |
|
668 |
|
669 ML {* |
|
670 fun prepare_bclauses dt_strs thy = |
|
671 let |
|
672 val annos_bclauses = |
|
673 get_cnstrs dt_strs |
|
674 |> map (map (fn (_, antys, _, bns) => (map fst antys, bns))) |
|
675 |
|
676 fun prep_binder env bn_str = |
|
677 case (Syntax.read_term_global thy bn_str) of |
|
678 Free (x, _) => (NONE, index_lookup env x) |
|
679 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) |
|
680 | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.") |
|
681 |
|
682 fun prep_body env bn_str = index_lookup env bn_str |
|
683 |
|
684 fun prep_bclause env (mode, binders, bodies) = |
|
685 let |
|
686 val binders' = map (prep_binder env) binders |
|
687 val bodies' = map (prep_body env) bodies |
|
688 in |
|
689 BC (mode, binders', bodies') |
|
690 end |
|
691 |
|
692 fun prep_bclauses (annos, bclause_strs) = |
|
693 let |
|
694 val env = indexify annos (* for every label, associate the index *) |
|
695 in |
|
696 map (prep_bclause env) bclause_strs |
|
697 end |
|
698 in |
|
699 (map (map prep_bclauses) annos_bclauses, thy) |
|
700 end |
|
701 *} |
|
702 |
|
703 text {* |
|
704 adds an empty binding clause for every argument |
|
705 that is not already part of a binding clause |
|
706 *} |
|
707 |
|
708 ML {* |
|
709 fun included i bcs = |
|
710 let |
|
711 fun incl (BC (_, bns, bds)) = |
|
712 member (op =) (map snd bns) i orelse member (op =) bds i |
|
713 in |
|
714 exists incl bcs |
|
715 end |
|
716 *} |
|
717 |
|
718 ML {* |
|
719 fun complete dt_strs bclauses = |
|
720 let |
|
721 val args = |
|
722 get_cnstrs dt_strs |
|
723 |> map (map (fn (_, antys, _, _) => length antys)) |
|
724 |
|
725 fun complt n bcs = |
|
726 let |
|
727 fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])]) |
|
728 in |
|
729 bcs @ (flat (map_range (add bcs) n)) |
|
730 end |
|
731 in |
|
732 map2 (map2 complt) args bclauses |
|
733 end |
|
734 *} |
|
735 |
|
736 ML {* |
|
737 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
|
738 let |
|
739 val pre_typs = |
|
740 map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dt_strs |
|
741 |
|
742 (* this theory is used just for parsing *) |
|
743 val thy = ProofContext.theory_of lthy |
|
744 val tmp_thy = Theory.copy thy |
|
745 |
|
746 val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = |
|
747 tmp_thy |
|
748 |> Sign.add_types pre_typs |
|
749 |> prepare_dts dt_strs |
|
750 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
|
751 ||>> prepare_bclauses dt_strs |
|
752 |
|
753 val bclauses' = complete dt_strs bclauses |
|
754 in |
|
755 timeit (fn () => nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy |> snd) |
|
756 end |
|
757 *} |
|
758 |
|
759 ML {* |
|
760 (* nominal datatype parser *) |
|
761 local |
|
762 structure P = Parse; |
|
763 structure S = Scan |
|
764 |
|
765 fun triple ((x, y), z) = (x, y, z) |
|
766 fun tuple1 ((x, y, z), u) = (x, y, z, u) |
|
767 fun tuple2 (((x, y), z), u) = (x, y, u, z) |
|
768 fun tuple3 ((x, y), (z, u)) = (x, y, z, u) |
|
769 in |
|
770 |
|
771 val _ = Keyword.keyword "bind" |
|
772 |
|
773 val opt_name = Scan.option (P.binding --| Args.colon) |
|
774 |
|
775 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ |
|
776 |
|
777 val bind_mode = P.$$$ "bind" |-- |
|
778 S.optional (Args.parens |
|
779 (Args.$$$ "list" >> K Lst || Args.$$$ "set" >> K Set || Args.$$$ "res" >> K Res)) Lst |
|
780 |
|
781 val bind_clauses = |
|
782 P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple) |
|
783 |
|
784 val cnstr_parser = |
|
785 P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tuple2 |
|
786 |
|
787 (* datatype parser *) |
|
788 val dt_parser = |
|
789 (P.type_args -- P.binding -- P.opt_mixfix >> triple) -- |
|
790 (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple1 |
|
791 |
|
792 (* binding function parser *) |
|
793 val bnfun_parser = |
|
794 S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], []) |
|
795 |
|
796 (* main parser *) |
|
797 val main_parser = |
|
798 opt_name -- P.and_list1 dt_parser -- bnfun_parser >> tuple3 |
|
799 |
|
800 end |
|
801 |
|
802 (* Command Keyword *) |
|
803 val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl |
|
804 (main_parser >> nominal_datatype2_cmd) |
|
805 *} |
|
806 |
|
807 |
|
808 end |
|
809 |
|
810 |
|
811 |