equal
deleted
inserted
replaced
588 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
588 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
589 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *} |
589 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *} |
590 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
590 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
591 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
591 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
592 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *} |
592 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *} |
593 ML {* val thm = @{thm spec[OF FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]],symmetric]} *} |
593 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
594 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
594 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
595 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *} |
595 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *} |
596 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
596 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
597 ML {* ObjectLogic.rulify ind_r_s *} |
597 ML {* ObjectLogic.rulify ind_r_s *} |
598 |
598 |
623 (* ML {* lift @{thm append_assoc} *} *) |
623 (* ML {* lift @{thm append_assoc} *} *) |
624 |
624 |
625 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
625 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
626 notation ( output) "Trueprop" ("#_" [1000] 1000) |
626 notation ( output) "Trueprop" ("#_" [1000] 1000) |
627 |
627 |
|
628 (* |
628 ML {* |
629 ML {* |
629 fun lift_theorem_fset_aux thm lthy = |
630 fun lift_theorem_fset_aux thm lthy = |
630 let |
631 let |
631 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
632 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
632 val goal = build_repabs_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"}; |
633 val goal = build_repabs_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"}; |
639 val [nthm3] = ProofContext.export lthy2 lthy [nthm2] |
640 val [nthm3] = ProofContext.export lthy2 lthy [nthm2] |
640 in |
641 in |
641 nthm3 |
642 nthm3 |
642 end |
643 end |
643 *} |
644 *} |
644 |
645 *) |
|
646 |
|
647 (* |
645 ML {* lift_theorem_fset_aux @{thm m1} @{context} *} |
648 ML {* lift_theorem_fset_aux @{thm m1} @{context} *} |
646 ML {* |
649 ML {* |
647 fun lift_theorem_fset name thm lthy = |
650 fun lift_theorem_fset name thm lthy = |
648 let |
651 let |
649 val lifted_thm = lift_theorem_fset_aux thm lthy; |
652 val lifted_thm = lift_theorem_fset_aux thm lthy; |
650 val (_, lthy2) = note (name, lifted_thm) lthy; |
653 val (_, lthy2) = note (name, lifted_thm) lthy; |
651 in |
654 in |
652 lthy2 |
655 lthy2 |
653 end; |
656 end; |
654 *} |
657 *} |
|
658 *) |
655 |
659 |
656 (* These do not work without proper definitions to rewrite back *) |
660 (* These do not work without proper definitions to rewrite back *) |
657 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
661 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
658 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
662 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
659 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
663 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |