250 (bn_fun_strs ~~ bn_fun_strs') |
250 (bn_fun_strs ~~ bn_fun_strs') |
251 |
251 |
252 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
252 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
253 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
253 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
254 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
254 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
255 val raw_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs) |
255 val raw_bn_descr = prep_bn_descr lthy dt_full_names' raw_dts (map snd raw_bn_eqs) |
256 |
256 |
257 val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy |
257 val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy |
258 val (raw_bn_funs, raw_bn_eqs, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 |
258 val (raw_bn_funs2, raw_bn_eqs2, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 |
259 |
259 |
260 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
260 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
261 fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); |
261 fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); |
262 val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns; |
262 val raw_bn_descr_exp = map (export_fun (Morphism.term morphism_2_0)) raw_bn_descr; |
263 in |
263 in |
264 (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, raw_bns, lthy2) |
264 (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr_exp, raw_bn_descr, lthy2) |
265 end |
265 end |
266 *} |
266 *} |
267 |
267 |
268 lemma equivp_hack: "equivp x" |
268 lemma equivp_hack: "equivp x" |
269 sorry |
269 sorry |
288 fun remove_loop t = |
288 fun remove_loop t = |
289 let val _ = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of t)) in t end |
289 let val _ = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of t)) in t end |
290 handle TERM _ => @{thm eqTrueI} OF [t] |
290 handle TERM _ => @{thm eqTrueI} OF [t] |
291 *} |
291 *} |
292 |
292 |
293 text {* |
|
294 nominal_datatype2 does the following things in order: |
|
295 |
|
296 Parser.thy/raw_nominal_decls |
|
297 1) define the raw datatype |
|
298 2) define the raw binding functions |
|
299 |
|
300 Perm.thy/define_raw_perms |
|
301 3) define permutations of the raw datatype and show that the raw type is |
|
302 in the pt typeclass |
|
303 |
|
304 Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha |
|
305 4) define fv and fv_bn |
|
306 5) define alpha and alpha_bn |
|
307 |
|
308 Perm.thy/distinct_rel |
|
309 6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...) (Proof by cases; simp) |
|
310 |
|
311 Tacs.thy/build_rel_inj |
|
312 6) prove alpha_eq_iff (C1 x = C2 y \<leftrightarrow> P x y ...) |
|
313 (left-to-right by intro rule, right-to-left by cases; simp) |
|
314 Equivp.thy/prove_eqvt |
|
315 7) prove bn_eqvt (common induction on the raw datatype) |
|
316 8) prove fv_eqvt (common induction on the raw datatype with help of above) |
|
317 Rsp.thy/build_alpha_eqvts |
|
318 9) prove alpha_eqvt and alpha_bn_eqvt |
|
319 (common alpha-induction, unfolding alpha_gen, permute of #* and =) |
|
320 Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps |
|
321 10) prove that alpha and alpha_bn are equivalence relations |
|
322 (common induction and application of 'compose' lemmas) |
|
323 Lift.thy/define_quotient_types |
|
324 11) define quotient types |
|
325 Rsp.thy/build_fvbv_rsps |
|
326 12) prove bn respects (common induction and simp with alpha_gen) |
|
327 Rsp.thy/prove_const_rsp |
|
328 13) prove fv respects (common induction and simp with alpha_gen) |
|
329 14) prove permute respects (unfolds to alpha_eqvt) |
|
330 Rsp.thy/prove_alpha_bn_rsp |
|
331 15) prove alpha_bn respects |
|
332 (alpha_induct then cases then sym and trans of the relations) |
|
333 Rsp.thy/prove_alpha_alphabn |
|
334 16) show that alpha implies alpha_bn (by unduction, needed in following step) |
|
335 Rsp.thy/prove_const_rsp |
|
336 17) prove respects for all datatype constructors |
|
337 (unfold eq_iff and alpha_gen; introduce zero permutations; simp) |
|
338 Perm.thy/quotient_lift_consts_export |
|
339 18) define lifted constructors, fv, bn, alpha_bn, permutations |
|
340 Perm.thy/define_lifted_perms |
|
341 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass |
|
342 Lift.thy/lift_thm |
|
343 20) lift permutation simplifications |
|
344 21) lift induction |
|
345 22) lift fv |
|
346 23) lift bn |
|
347 24) lift eq_iff |
|
348 25) lift alpha_distincts |
|
349 26) lift fv and bn eqvts |
|
350 Equivp.thy/prove_supports |
|
351 27) prove that union of arguments supports constructors |
|
352 Equivp.thy/prove_fs |
|
353 28) show that the lifted type is in fs typeclass (* by q_induct, supports *) |
|
354 Equivp.thy/supp_eq |
|
355 29) prove supp = fv |
|
356 *} |
|
357 |
293 |
358 ML {* |
294 ML {* |
359 (* for testing porposes - to exit the procedure early *) |
295 (* for testing porposes - to exit the procedure early *) |
360 exception TEST of Proof.context |
296 exception TEST of Proof.context |
361 |
297 |
368 |
304 |
369 ML {* |
305 ML {* |
370 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
306 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
371 let |
307 let |
372 (* definition of the raw datatypes and raw bn-functions *) |
308 (* definition of the raw datatypes and raw bn-functions *) |
373 val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, raw_bns2, lthy1) = |
309 val (raw_dt_names, raw_bclauses, raw_bn_funs2, raw_bn_eqs2, raw_bn_funs, raw_bn_eqs, raw_bn_descr, raw_bn_descr2, lthy1) = |
374 if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
310 if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
375 else raise TEST lthy |
311 else raise TEST lthy |
376 |
312 |
377 (*val _ = tracing ("exported: " ^ commas (map @{make_string} raw_bns))*) |
313 val _ = tracing ("raw_bn_descr " ^ @{make_string} raw_bn_descr) |
378 (*val _ = tracing ("plain: " ^ commas (map @{make_string} raw_bns2))*) |
314 val _ = tracing ("raw_bn_descr2 " ^ @{make_string} raw_bn_descr2) |
|
315 val _ = tracing ("bclauses " ^ @{make_string} bclauses) |
|
316 val _ = tracing ("raw_bn_fund " ^ @{make_string} raw_bn_funs) |
|
317 val _ = tracing ("raw_bn_eqs " ^ @{make_string} raw_bn_eqs) |
|
318 val _ = tracing ("raw_bn_fund2 " ^ @{make_string} raw_bn_funs2) |
|
319 val _ = tracing ("raw_bn_eqs2 " ^ cat_lines (map (Syntax.string_of_term lthy o snd) raw_bn_eqs2)) |
379 |
320 |
380 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names) |
321 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names) |
381 val {descr, sorts, ...} = dtinfo |
322 val {descr, sorts, ...} = dtinfo |
382 val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr |
323 val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr |
383 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr |
324 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr |
389 val rel_distinct = map #distinct rel_dtinfos; (* thm list list *) |
330 val rel_distinct = map #distinct rel_dtinfos; (* thm list list *) |
390 val induct_thm = #induct dtinfo; |
331 val induct_thm = #induct dtinfo; |
391 val exhaust_thms = map #exhaust dtinfos; |
332 val exhaust_thms = map #exhaust dtinfos; |
392 |
333 |
393 (* definitions of raw permutations *) |
334 (* definitions of raw permutations *) |
394 val ((perms, raw_perm_defs, raw_perm_simps), lthy2) = |
335 val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = |
395 if get_STEPS lthy1 > 2 |
336 if get_STEPS lthy1 > 2 |
396 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
337 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
397 else raise TEST lthy1 |
338 else raise TEST lthy1 |
398 |
339 |
399 (* noting the raw permutations as eqvt theorems *) |
340 (* noting the raw permutations as eqvt theorems *) |
403 val thy = Local_Theory.exit_global lthy2a; |
344 val thy = Local_Theory.exit_global lthy2a; |
404 val thy_name = Context.theory_name thy |
345 val thy_name = Context.theory_name thy |
405 |
346 |
406 (* definition of raw fv_functions *) |
347 (* definition of raw fv_functions *) |
407 val lthy3 = Theory_Target.init NONE thy; |
348 val lthy3 = Theory_Target.init NONE thy; |
408 val raw_bn_funs = map (fn (f, _, _) => f) raw_bns; |
|
409 |
349 |
410 val (fv, fvbn, fv_def, lthy3a) = |
350 val (fv, fvbn, fv_def, lthy3a) = |
411 if get_STEPS lthy2 > 3 |
351 if get_STEPS lthy2 > 3 |
412 then define_raw_fvs descr sorts raw_bns raw_bns2 raw_bclauses lthy3 |
352 then define_raw_fvs (map (fn (x, _, _) => Binding.name_of x) bn_funs) (map snd bn_eqs) descr sorts raw_bn_descr raw_bn_descr2 raw_bclauses lthy3 |
413 else raise TEST lthy3 |
353 else raise TEST lthy3 |
414 |
354 |
|
355 |
415 (* definition of raw alphas *) |
356 (* definition of raw alphas *) |
416 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
357 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
417 if get_STEPS lthy > 4 |
358 if get_STEPS lthy > 4 |
418 then define_raw_alpha dtinfo raw_bns raw_bclauses fv lthy3a |
359 then define_raw_alpha dtinfo raw_bn_descr raw_bclauses fv lthy3a |
419 else raise TEST lthy3a |
360 else raise TEST lthy3a |
420 |
361 |
421 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
362 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
422 |
363 |
423 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
364 val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr; |
424 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
365 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
425 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
366 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
426 val bns = raw_bn_funs ~~ bn_nos; |
367 val bns = raw_bn_funs ~~ bn_nos; |
427 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
368 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
428 (rel_distinct ~~ alpha_ts_nobn)); |
369 (rel_distinct ~~ alpha_ts_nobn)); |
431 |
372 |
432 (* definition of raw_alpha_eq_iff lemmas *) |
373 (* definition of raw_alpha_eq_iff lemmas *) |
433 val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 |
374 val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 |
434 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; |
375 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; |
435 |
376 |
436 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);*) |
|
437 |
|
438 (* proving equivariance lemmas *) |
377 (* proving equivariance lemmas *) |
439 val _ = warning "Proving equivariance"; |
378 val _ = warning "Proving equivariance"; |
440 val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4 |
379 val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4 |
441 val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fvbn) lthy5 |
380 val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fvbn) lthy5 |
442 val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6; |
381 val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6; |
472 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
411 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
473 val (fv_rsp_pre, lthy10) = fold_map |
412 val (fv_rsp_pre, lthy10) = fold_map |
474 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
413 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
475 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; |
414 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; |
476 val fv_rsp = flat (map snd fv_rsp_pre); |
415 val fv_rsp = flat (map snd fv_rsp_pre); |
477 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms |
416 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
478 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
417 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
479 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
418 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
480 else |
419 else |
481 let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
420 let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
482 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
421 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
486 in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
425 in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
487 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
426 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
488 const_rsp_tac) raw_consts lthy11a |
427 const_rsp_tac) raw_consts lthy11a |
489 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn) |
428 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn) |
490 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12; |
429 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12; |
491 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
430 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
492 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
431 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
493 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a; |
432 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a; |
494 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
433 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
495 val (qalpha_ts_bn, qalphabn_defs, lthy12c) = |
434 val (qalpha_ts_bn, qalphabn_defs, lthy12c) = |
496 quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
435 quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
497 val _ = warning "Lifting permutations"; |
436 val _ = warning "Lifting permutations"; |
498 val thy = Local_Theory.exit_global lthy12c; |
437 val thy = Local_Theory.exit_global lthy12c; |
499 val perm_names = map (fn x => "permute_" ^ x) qty_names |
438 val perm_names = map (fn x => "permute_" ^ x) qty_names |
500 val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
439 val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ raw_perm_funs) raw_perm_simps thy; |
501 val lthy13 = Theory_Target.init NONE thy'; |
440 val lthy13 = Theory_Target.init NONE thy'; |
502 val q_name = space_implode "_" qty_names; |
441 val q_name = space_implode "_" qty_names; |
503 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
442 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
504 val _ = warning "Lifting induction"; |
443 val _ = warning "Lifting induction"; |
505 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |
444 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |
715 |
654 |
716 val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl |
655 val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl |
717 (main_parser >> nominal_datatype2_cmd) |
656 (main_parser >> nominal_datatype2_cmd) |
718 *} |
657 *} |
719 |
658 |
720 (* |
659 |
721 atom_decl name |
660 text {* |
722 |
661 nominal_datatype2 does the following things in order: |
723 nominal_datatype lam = |
662 |
724 Var name |
663 Parser.thy/raw_nominal_decls |
725 | App lam lam |
664 1) define the raw datatype |
726 | Lam x::name t::lam bind_set x in t |
665 2) define the raw binding functions |
727 | Let p::pt t::lam bind_set "bn p" in t |
666 |
728 and pt = |
667 Perm.thy/define_raw_perms |
729 P1 name |
668 3) define permutations of the raw datatype and show that the raw type is |
730 | P2 pt pt |
669 in the pt typeclass |
731 binder |
670 |
732 bn::"pt \<Rightarrow> atom set" |
671 Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha |
733 where |
672 4) define fv and fv_bn |
734 "bn (P1 x) = {atom x}" |
673 5) define alpha and alpha_bn |
735 | "bn (P2 p1 p2) = bn p1 \<union> bn p2" |
674 |
736 |
675 Perm.thy/distinct_rel |
737 find_theorems Var_raw |
676 6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...) (Proof by cases; simp) |
738 |
677 |
739 |
678 Tacs.thy/build_rel_inj |
740 |
679 6) prove alpha_eq_iff (C1 x = C2 y \<leftrightarrow> P x y ...) |
741 thm lam_pt.bn |
680 (left-to-right by intro rule, right-to-left by cases; simp) |
742 thm lam_pt.fv[simplified lam_pt.supp(1-2)] |
681 Equivp.thy/prove_eqvt |
743 thm lam_pt.eq_iff |
682 7) prove bn_eqvt (common induction on the raw datatype) |
744 thm lam_pt.induct |
683 8) prove fv_eqvt (common induction on the raw datatype with help of above) |
745 thm lam_pt.perm |
684 Rsp.thy/build_alpha_eqvts |
746 |
685 9) prove alpha_eqvt and alpha_bn_eqvt |
747 nominal_datatype exp = |
686 (common alpha-induction, unfolding alpha_gen, permute of #* and =) |
748 EVar name |
687 Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps |
749 | EUnit |
688 10) prove that alpha and alpha_bn are equivalence relations |
750 | EPair q1::exp q2::exp |
689 (common induction and application of 'compose' lemmas) |
751 | ELetRec l::lrbs e::exp bind "b_lrbs l" in e l |
690 Lift.thy/define_quotient_types |
752 |
691 11) define quotient types |
753 and fnclause = |
692 Rsp.thy/build_fvbv_rsps |
754 K x::name p::pat f::exp bind_res "b_pat p" in f |
693 12) prove bn respects (common induction and simp with alpha_gen) |
755 |
694 Rsp.thy/prove_const_rsp |
756 and fnclauses = |
695 13) prove fv respects (common induction and simp with alpha_gen) |
757 S fnclause |
696 14) prove permute respects (unfolds to alpha_eqvt) |
758 | ORs fnclause fnclauses |
697 Rsp.thy/prove_alpha_bn_rsp |
759 |
698 15) prove alpha_bn respects |
760 and lrb = |
699 (alpha_induct then cases then sym and trans of the relations) |
761 Clause fnclauses |
700 Rsp.thy/prove_alpha_alphabn |
762 |
701 16) show that alpha implies alpha_bn (by unduction, needed in following step) |
763 and lrbs = |
702 Rsp.thy/prove_const_rsp |
764 Single lrb |
703 17) prove respects for all datatype constructors |
765 | More lrb lrbs |
704 (unfold eq_iff and alpha_gen; introduce zero permutations; simp) |
766 |
705 Perm.thy/quotient_lift_consts_export |
767 and pat = |
706 18) define lifted constructors, fv, bn, alpha_bn, permutations |
768 PVar name |
707 Perm.thy/define_lifted_perms |
769 | PUnit |
708 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass |
770 | PPair pat pat |
709 Lift.thy/lift_thm |
771 |
710 20) lift permutation simplifications |
772 binder |
711 21) lift induction |
773 b_lrbs :: "lrbs \<Rightarrow> atom list" and |
712 22) lift fv |
774 b_pat :: "pat \<Rightarrow> atom set" and |
713 23) lift bn |
775 b_fnclauses :: "fnclauses \<Rightarrow> atom list" and |
714 24) lift eq_iff |
776 b_fnclause :: "fnclause \<Rightarrow> atom list" and |
715 25) lift alpha_distincts |
777 b_lrb :: "lrb \<Rightarrow> atom list" |
716 26) lift fv and bn eqvts |
778 |
717 Equivp.thy/prove_supports |
779 where |
718 27) prove that union of arguments supports constructors |
780 "b_lrbs (Single l) = b_lrb l" |
719 Equivp.thy/prove_fs |
781 | "b_lrbs (More l ls) = append (b_lrb l) (b_lrbs ls)" |
720 28) show that the lifted type is in fs typeclass (* by q_induct, supports *) |
782 | "b_pat (PVar x) = {atom x}" |
721 Equivp.thy/supp_eq |
783 | "b_pat (PUnit) = {}" |
722 29) prove supp = fv |
784 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2" |
723 *} |
785 | "b_fnclauses (S fc) = (b_fnclause fc)" |
724 |
786 | "b_fnclauses (ORs fc fcs) = append (b_fnclause fc) (b_fnclauses fcs)" |
725 |
787 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
726 |
788 | "b_fnclause (K x pat exp) = [atom x]" |
727 end |
789 |
728 |
790 thm exp_fnclause_fnclauses_lrb_lrbs_pat.bn |
729 |
791 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv |
730 |
792 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff |
|
793 thm exp_fnclause_fnclauses_lrb_lrbs_pat.induct |
|
794 thm exp_fnclause_fnclauses_lrb_lrbs_pat.perm |
|
795 |
|
796 nominal_datatype ty = |
|
797 Vr "name" |
|
798 | Fn "ty" "ty" |
|
799 and tys = |
|
800 Al xs::"name fset" t::"ty" bind_res xs in t |
|
801 |
|
802 thm ty_tys.fv[simplified ty_tys.supp] |
|
803 thm ty_tys.eq_iff |
|
804 |
|
805 *) |
|
806 |
|
807 (* some further tests *) |
|
808 |
|
809 (* |
|
810 nominal_datatype ty2 = |
|
811 Vr2 "name" |
|
812 | Fn2 "ty2" "ty2" |
|
813 |
|
814 nominal_datatype tys2 = |
|
815 All2 xs::"name fset" ty::"ty2" bind_res xs in ty |
|
816 |
|
817 nominal_datatype lam2 = |
|
818 Var2 "name" |
|
819 | App2 "lam2" "lam2 list" |
|
820 | Lam2 x::"name" t::"lam2" bind x in t |
|
821 *) |
|
822 |
|
823 |
|
824 |
|
825 end |
|
826 |
|
827 |
|
828 |
|