566 if get_STEPS lthy > 31 |
566 if get_STEPS lthy > 31 |
567 then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs |
567 then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs |
568 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
568 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
569 else [] |
569 else [] |
570 |
570 |
571 |
571 (* postprocessing of eq and fv theorems *) |
|
572 |
|
573 val qeq_iffs' = qeq_iffs |
|
574 |> map (simplify (HOL_basic_ss addsimps |
|
575 (@{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]} @ qfv_supp_thms))) |
|
576 |
|
577 val qsupp_constrs = qfv_defs |
|
578 |> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms))) |
|
579 |
572 (* noting the theorems *) |
580 (* noting the theorems *) |
573 |
581 |
574 (* generating the prefix for the theorem names *) |
582 (* generating the prefix for the theorem names *) |
575 val thms_name = |
583 val thms_name = |
576 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
584 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
577 fun thms_suffix s = Binding.qualified true s thms_name |
585 fun thms_suffix s = Binding.qualified true s thms_name |
578 |
586 |
579 val (_, lthy9') = lthyC |
587 val (_, lthy9') = lthyC |
580 |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) |
588 |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) |
581 ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs) |
589 ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs') |
582 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
590 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
583 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
591 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
584 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
592 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
585 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
593 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
586 ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps) |
594 ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps) |
588 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
596 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
589 ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) |
597 ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) |
590 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
598 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
591 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
599 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
592 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
600 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
593 ||>> Local_Theory.note ((thms_suffix "supp", []), qfv_supp_thms) |
601 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
594 in |
602 in |
595 (0, lthy9') |
603 (0, lthy9') |
596 end handle TEST ctxt => (0, ctxt) |
604 end handle TEST ctxt => (0, ctxt) |
597 *} |
605 *} |
598 |
606 |