527 ||>> lift_thms qtys [] raw_bn_defs |
527 ||>> lift_thms qtys [] raw_bn_defs |
528 ||>> lift_thms qtys [] raw_perm_simps |
528 ||>> lift_thms qtys [] raw_perm_simps |
529 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
529 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
530 else raise TEST lthy9a |
530 else raise TEST lthy9a |
531 |
531 |
532 val (((qsize_eqvt, [qinduct]), qexhausts), lthyB) = |
532 val ((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), lthyB) = |
533 if get_STEPS lthy > 27 |
533 if get_STEPS lthy > 27 |
534 then |
534 then |
535 lthyA |
535 lthyA |
536 |> lift_thms qtys [] raw_size_eqvt |
536 |> lift_thms qtys [] raw_size_eqvt |
537 ||>> lift_thms qtys [] [raw_induct_thm] |
537 ||>> lift_thms qtys [] [raw_induct_thm] |
538 ||>> lift_thms qtys [] raw_exhaust_thms |
538 ||>> lift_thms qtys [] raw_exhaust_thms |
|
539 ||>> lift_thms qtys [] raw_size_thms |
539 else raise TEST lthyA |
540 else raise TEST lthyA |
540 |
541 |
541 val qinducts = Project_Rule.projections lthyA qinduct |
542 val qinducts = Project_Rule.projections lthyA qinduct |
542 |
543 |
543 (* supports lemmas *) |
544 (* supports lemmas *) |
580 ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs) |
581 ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs) |
581 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
582 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
582 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
583 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
583 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
584 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
584 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
585 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
|
586 ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps) |
585 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
587 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
586 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
588 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
587 ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) |
589 ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) |
588 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
590 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
589 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
591 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |