256 ||>> pair raw_bclauses |
256 ||>> pair raw_bclauses |
257 ||>> pair raw_bns |
257 ||>> pair raw_bns |
258 end |
258 end |
259 *} |
259 *} |
260 |
260 |
|
261 |
|
262 text {* |
|
263 nominal_datatype2 does the following things in order: |
|
264 |
|
265 Parser.thy/raw_nominal_decls |
|
266 1) define the raw datatype |
|
267 2) define the raw binding functions |
|
268 |
|
269 Perm.thy/define_raw_perms |
|
270 3) define permutations of the raw datatype and show that the raw type is |
|
271 in the pt typeclass |
|
272 |
|
273 Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha |
|
274 4) define fv and fv_bn |
|
275 5) define alpha and alpha_bn |
|
276 |
|
277 Perm.thy/distinct_rel |
|
278 6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...) (Proof by cases; simp) |
|
279 |
|
280 Tacs.thy/build_rel_inj |
|
281 6) prove alpha_eq_iff (C1 x = C2 y \<leftrightarrow> P x y ...) |
|
282 (left-to-right by intro rule, right-to-left by cases; simp) |
|
283 Equivp.thy/prove_eqvt |
|
284 7) prove bn_eqvt (common induction on the raw datatype) |
|
285 8) prove fv_eqvt (common induction on the raw datatype with help of above) |
|
286 Rsp.thy/build_alpha_eqvts |
|
287 9) prove alpha_eqvt and alpha_bn_eqvt |
|
288 (common alpha-induction, unfolding alpha_gen, permute of #* and =) |
|
289 Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps |
|
290 10) prove that alpha and alpha_bn are equivalence relations |
|
291 (common induction and application of 'compose' lemmas) |
|
292 Lift.thy/define_quotient_types |
|
293 11) define quotient types |
|
294 Rsp.thy/build_fvbv_rsps |
|
295 12) prove bn respects (common induction and simp with alpha_gen) |
|
296 Rsp.thy/prove_const_rsp |
|
297 13) prove fv respects (common induction and simp with alpha_gen) |
|
298 14) prove permute respects (unfolds to alpha_eqvt) |
|
299 Rsp.thy/prove_alpha_bn_rsp |
|
300 15) prove alpha_bn respects |
|
301 (alpha_induct then cases then sym and trans of the relations) |
|
302 Rsp.thy/prove_alpha_alphabn |
|
303 16) show that alpha implies alpha_bn (by unduction, needed in following step) |
|
304 Rsp.thy/prove_const_rsp |
|
305 17) prove respects for all datatype constructors |
|
306 (unfold eq_iff and alpha_gen; introduce zero permutations; simp) |
|
307 Perm.thy/quotient_lift_consts_export |
|
308 18) define lifted constructors, fv, bn, alpha_bn, permutations |
|
309 Perm.thy/define_lifted_perms |
|
310 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass |
|
311 Lift.thy/lift_thm |
|
312 20) lift permutation simplifications |
|
313 21) lift induction |
|
314 22) lift fv |
|
315 23) lift bn |
|
316 24) lift eq_iff |
|
317 25) lift alpha_distincts |
|
318 26) lift fv and bn eqvts |
|
319 Equivp.thy/prove_supports |
|
320 27) prove that union of arguments supports constructors |
|
321 Equivp.thy/prove_fs |
|
322 28) show that the lifted type is in fs typeclass (* by q_induct, supports *) |
|
323 Equivp.thy/supp_eq |
|
324 29) prove supp = fv |
|
325 *} |
|
326 |
|
327 |
261 ML {* |
328 ML {* |
262 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
329 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
263 let |
330 let |
|
331 |
|
332 (* definition of the raw datatype and raw bn-functions *) |
264 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) = |
333 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) = |
265 raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
334 raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
266 |
335 |
267 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
336 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
268 val {descr, sorts, ...} = dtinfo; |
337 val {descr, sorts, ...} = dtinfo; |
277 val rel_dtinfos = List.take (dtinfos, (length dts)); |
346 val rel_dtinfos = List.take (dtinfos, (length dts)); |
278 val rel_distinct = map #distinct rel_dtinfos; |
347 val rel_distinct = map #distinct rel_dtinfos; |
279 val induct = #induct dtinfo; |
348 val induct = #induct dtinfo; |
280 val exhausts = map #exhaust dtinfos; |
349 val exhausts = map #exhaust dtinfos; |
281 |
350 |
|
351 (* definitions of raw permutations *) |
282 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
352 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
283 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1; |
353 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1; |
284 |
354 |
285 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
355 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
286 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
356 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
656 and tys = |
728 and tys = |
657 Al xs::"name fset" t::"ty" bind_res xs in t |
729 Al xs::"name fset" t::"ty" bind_res xs in t |
658 |
730 |
659 thm ty_tys.fv[simplified ty_tys.supp] |
731 thm ty_tys.fv[simplified ty_tys.supp] |
660 thm ty_tys.eq_iff |
732 thm ty_tys.eq_iff |
|
733 *) |
|
734 |
661 |
735 |
662 (* some further tests *) |
736 (* some further tests *) |
663 |
737 |
664 nominal_datatype ty = |
738 (* |
665 Vr "name" |
739 nominal_datatype ty2 = |
666 | Fn "ty" "ty" |
740 Vr2 "name" |
667 |
741 | Fn2 "ty2" "ty2" |
668 nominal_datatype tys = |
742 |
669 All xs::"name fset" ty::"ty_raw" bind_res xs in ty |
743 nominal_datatype tys2 = |
|
744 All2 xs::"name fset" ty::"ty2" bind_res xs in ty |
670 |
745 |
671 nominal_datatype lam2 = |
746 nominal_datatype lam2 = |
672 Var2 "name" |
747 Var2 "name" |
673 | App2 "lam2" "lam2 list" |
748 | App2 "lam2" "lam2 list" |
674 | Lam2 x::"name" t::"lam2" bind x in t |
749 | Lam2 x::"name" t::"lam2" bind x in t |
675 |
750 *) |
676 |
751 |
677 |
752 |
678 |
753 |
679 end |
754 end |
680 |
755 |
681 |
756 |
682 |
757 |