291 ML {* val cheat_equivp = Unsynchronized.ref false *} |
291 ML {* val cheat_equivp = Unsynchronized.ref false *} |
292 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
292 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
293 ML {* val cheat_const_rsp = Unsynchronized.ref false *} |
293 ML {* val cheat_const_rsp = Unsynchronized.ref false *} |
294 |
294 |
295 (* nominal_datatype2 does the following things in order: |
295 (* nominal_datatype2 does the following things in order: |
|
296 |
|
297 Parser.thy/raw_nominal_decls |
296 1) define the raw datatype |
298 1) define the raw datatype |
297 2) define the raw binding functions |
299 2) define the raw binding functions |
|
300 Perm.thy/define_raw_perms |
298 3) define permutations of the raw datatype and show that raw type is in the pt typeclass |
301 3) define permutations of the raw datatype and show that raw type is in the pt typeclass |
299 4) define fv and fb_bn |
302 Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha |
|
303 4) define fv and fv_bn |
300 5) define alpha and alpha_bn |
304 5) define alpha and alpha_bn |
|
305 Perm.thy/distinct_rel |
301 6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...) (Proof by cases; simp) |
306 6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...) (Proof by cases; simp) |
|
307 Tacs.thy/build_rel_inj |
302 6) prove alpha_eq_iff (C1 x = C2 y \<leftrightarrow> P x y ...) |
308 6) prove alpha_eq_iff (C1 x = C2 y \<leftrightarrow> P x y ...) |
303 (left-to-right by intro rule, right-to-left by cases; simp) |
309 (left-to-right by intro rule, right-to-left by cases; simp) |
|
310 Equivp.thy/prove_eqvt |
304 7) prove bn_eqvt (common induction on the raw datatype) |
311 7) prove bn_eqvt (common induction on the raw datatype) |
305 8) prove fv_eqvt (common induction on the raw datatype with help of above) |
312 8) prove fv_eqvt (common induction on the raw datatype with help of above) |
|
313 Rsp.thy/build_alpha_eqvts |
306 9) prove alpha_eqvt and alpha_bn_eqvt |
314 9) prove alpha_eqvt and alpha_bn_eqvt |
307 (common alpha-induction, unfolding alpha_gen, permute of #* and =) |
315 (common alpha-induction, unfolding alpha_gen, permute of #* and =) |
|
316 Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps |
308 10) prove that alpha and alpha_bn are equivalence relations |
317 10) prove that alpha and alpha_bn are equivalence relations |
309 (common induction and application of 'compose' lemmas) |
318 (common induction and application of 'compose' lemmas) |
|
319 Lift.thy/define_quotient_types |
310 11) define quotient types |
320 11) define quotient types |
|
321 Rsp.thy/build_fvbv_rsps |
311 12) prove bn respects (common induction and simp with alpha_gen) |
322 12) prove bn respects (common induction and simp with alpha_gen) |
|
323 Rsp.thy/prove_const_rsp |
312 13) prove fv respects (common induction and simp with alpha_gen) |
324 13) prove fv respects (common induction and simp with alpha_gen) |
313 14) prove permute respects (unfolds to alpha_eqvt) |
325 14) prove permute respects (unfolds to alpha_eqvt) |
|
326 Rsp.thy/prove_alpha_bn_rsp |
314 15) prove alpha_bn respects |
327 15) prove alpha_bn respects |
315 (alpha_induct then cases then sym and trans of the relations) |
328 (alpha_induct then cases then sym and trans of the relations) |
|
329 Rsp.thy/prove_alpha_alphabn |
316 16) show that alpha implies alpha_bn (by unduction, needed in following step) |
330 16) show that alpha implies alpha_bn (by unduction, needed in following step) |
|
331 Rsp.thy/prove_const_rsp |
317 17) prove respects for all datatype constructors |
332 17) prove respects for all datatype constructors |
318 (unfold eq_iff and alpha_gen; introduce zero permutations; simp) |
333 (unfold eq_iff and alpha_gen; introduce zero permutations; simp) |
|
334 Lift.thy/quotient_lift_consts_export |
319 18) define lifted constructors, fv, bn, alpha_bn, permutations |
335 18) define lifted constructors, fv, bn, alpha_bn, permutations |
|
336 Perm.thy/define_lifted_perms |
320 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass |
337 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass |
|
338 Lift.thy/lift_thm |
321 20) lift permutation simplifications |
339 20) lift permutation simplifications |
322 21) lift induction |
340 21) lift induction |
323 22) lift fv |
341 22) lift fv |
324 23) lift bn |
342 23) lift bn |
325 24) lift eq_iff |
343 24) lift eq_iff |
326 25) lift alpha_distincts |
344 25) lift alpha_distincts |
327 26) lift fv and bn eqvts |
345 26) lift fv and bn eqvts |
|
346 Equivp.thy/prove_supports |
328 27) prove that union of arguments supports constructors |
347 27) prove that union of arguments supports constructors |
|
348 Equivp.thy/prove_fs |
329 28) show that the lifted type is in fs typeclass (* by q_induct, supports *) |
349 28) show that the lifted type is in fs typeclass (* by q_induct, supports *) |
|
350 Equivp.thy/supp_eq |
330 29) prove supp = fv |
351 29) prove supp = fv |
331 *) |
352 *) |
332 ML {* |
353 ML {* |
333 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
354 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
334 let |
355 let |