533 |
533 |
534 (* proving the strong exhausts and induct lemmas *) |
534 (* proving the strong exhausts and induct lemmas *) |
535 val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs' |
535 val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs' |
536 qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms |
536 qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms |
537 |
537 |
538 val qstrong_induct_thm = prove_strong_induct lthyC qinduct qstrong_exhaust_thms bclauses |
538 val qstrong_induct_thms = prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses |
539 |
539 |
540 |
540 |
541 (* noting the theorems *) |
541 (* noting the theorems *) |
542 |
542 |
543 (* generating the prefix for the theorem names *) |
543 (* generating the prefix for the theorem names *) |
556 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
556 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
557 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
557 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
558 ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) |
558 ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) |
559 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
559 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
560 ||>> Local_Theory.note ((thms_suffix "strong_exhaust", []), qstrong_exhaust_thms) |
560 ||>> Local_Theory.note ((thms_suffix "strong_exhaust", []), qstrong_exhaust_thms) |
|
561 ||>> Local_Theory.note ((thms_suffix "strong_induct", []), qstrong_induct_thms) |
561 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
562 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
562 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
563 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
563 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
564 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
564 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
565 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
565 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |
566 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |