equal
deleted
inserted
replaced
1 theory Nominal2 |
1 theory Nominal2 |
2 imports |
2 imports |
3 Nominal2_Base Nominal2_Eqvt Nominal2_Abs |
3 Nominal2_Base Nominal2_Eqvt Nominal2_Abs |
4 uses ("nominal_dt_rawperm.ML") |
4 uses ("nominal_dt_rawfuns.ML") |
5 ("nominal_dt_rawfuns.ML") |
|
6 ("nominal_dt_alpha.ML") |
5 ("nominal_dt_alpha.ML") |
7 ("nominal_dt_quot.ML") |
6 ("nominal_dt_quot.ML") |
8 begin |
7 begin |
9 |
|
10 use "nominal_dt_rawperm.ML" |
|
11 ML {* open Nominal_Dt_RawPerm *} |
|
12 |
8 |
13 use "nominal_dt_rawfuns.ML" |
9 use "nominal_dt_rawfuns.ML" |
14 ML {* open Nominal_Dt_RawFuns *} |
10 ML {* open Nominal_Dt_RawFuns *} |
15 |
11 |
16 use "nominal_dt_alpha.ML" |
12 use "nominal_dt_alpha.ML" |
610 (* proving that perm_bns preserve alpha *) |
606 (* proving that perm_bns preserve alpha *) |
611 val qperm_bn_alpha_thms = |
607 val qperm_bn_alpha_thms = |
612 if get_STEPS lthy > 33 |
608 if get_STEPS lthy > 33 |
613 then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' |
609 then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' |
614 qalpha_refl_thms lthyC |
610 qalpha_refl_thms lthyC |
|
611 else [] |
|
612 |
|
613 (* proving the relationship of bn and permute_bn *) |
|
614 val qpermute_bn_thms = |
|
615 if get_STEPS lthy > 33 |
|
616 then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC |
615 else [] |
617 else [] |
616 |
618 |
617 (* noting the theorems *) |
619 (* noting the theorems *) |
618 |
620 |
619 (* generating the prefix for the theorem names *) |
621 (* generating the prefix for the theorem names *) |
639 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
641 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
640 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |
642 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |
641 ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) |
643 ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) |
642 ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) |
644 ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) |
643 ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) |
645 ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) |
|
646 ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms) |
644 in |
647 in |
645 (0, lthy9') |
648 (0, lthy9') |
646 end handle TEST ctxt => (0, ctxt) |
649 end handle TEST ctxt => (0, ctxt) |
647 *} |
650 *} |
648 |
651 |