547 ||>> lift_thms qtys [] raw_bn_defs |
547 ||>> lift_thms qtys [] raw_bn_defs |
548 ||>> lift_thms qtys [] raw_perm_simps |
548 ||>> lift_thms qtys [] raw_perm_simps |
549 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
549 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
550 else raise TEST lthy9a |
550 else raise TEST lthy9a |
551 |
551 |
552 val ((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), lthyB) = |
552 val (((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), lthyB) = |
553 if get_STEPS lthy > 28 |
553 if get_STEPS lthy > 28 |
554 then |
554 then |
555 lthyA |
555 lthyA |
556 |> lift_thms qtys [] raw_size_eqvt |
556 |> lift_thms qtys [] raw_size_eqvt |
557 ||>> lift_thms qtys [] [raw_induct_thm] |
557 ||>> lift_thms qtys [] [raw_induct_thm] |
558 ||>> lift_thms qtys [] raw_exhaust_thms |
558 ||>> lift_thms qtys [] raw_exhaust_thms |
559 ||>> lift_thms qtys [] raw_size_thms |
559 ||>> lift_thms qtys [] raw_size_thms |
|
560 ||>> lift_thms qtys [] raw_perm_bn_simps |
560 else raise TEST lthyA |
561 else raise TEST lthyA |
561 |
562 |
562 val qinducts = Project_Rule.projections lthyA qinduct |
563 val qinducts = Project_Rule.projections lthyA qinduct |
563 |
564 |
564 (* supports lemmas *) |
565 (* supports lemmas *) |
631 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
632 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
632 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
633 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
633 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
634 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
634 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
635 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
635 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |
636 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |
|
637 ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) |
636 in |
638 in |
637 (0, lthy9') |
639 (0, lthy9') |
638 end handle TEST ctxt => (0, ctxt) |
640 end handle TEST ctxt => (0, ctxt) |
639 *} |
641 *} |
640 |
642 |