equal
deleted
inserted
replaced
584 if get_STEPS lthy > 32 |
584 if get_STEPS lthy > 32 |
585 then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs |
585 then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs |
586 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
586 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
587 else [] |
587 else [] |
588 |
588 |
|
589 (* proving that the qbn result is finite *) |
|
590 val qbn_finite_thms = |
|
591 if get_STEPS lthy > 33 |
|
592 then prove_bns_finite qtys qbns qinduct qbn_defs lthyC |
|
593 else [] |
|
594 |
589 (* postprocessing of eq and fv theorems *) |
595 (* postprocessing of eq and fv theorems *) |
590 |
596 |
591 val qeq_iffs' = qeq_iffs |
597 val qeq_iffs' = qeq_iffs |
592 |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms)) |
598 |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms)) |
593 |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
599 |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
630 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
636 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
631 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
637 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
632 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
638 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
633 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |
639 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |
634 ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) |
640 ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) |
|
641 ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) |
635 in |
642 in |
636 (0, lthy9') |
643 (0, lthy9') |
637 end handle TEST ctxt => (0, ctxt) |
644 end handle TEST ctxt => (0, ctxt) |
638 *} |
645 *} |
639 |
646 |