648 |
648 |
649 fun old_make_const_def nconst_bname otrm mx rty qty lthy = |
649 fun old_make_const_def nconst_bname otrm mx rty qty lthy = |
650 make_const_def nconst_bname otrm mx [(qty, rty)] lthy |
650 make_const_def nconst_bname otrm mx [(qty, rty)] lthy |
651 *} |
651 *} |
652 |
652 |
|
653 text {* Does the same as 'subst' in a given prop or theorem *} |
|
654 ML {* |
|
655 fun eqsubst_prop ctxt thms t = |
|
656 let |
|
657 val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t) |
|
658 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
|
659 NONE => error "eqsubst_prop" |
|
660 | SOME th => cprem_of th 1 |
|
661 in term_of a' end |
|
662 *} |
|
663 |
|
664 ML {* |
|
665 fun repeat_eqsubst_prop ctxt thms t = |
|
666 repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t) |
|
667 handle _ => t |
|
668 *} |
|
669 |
|
670 |
|
671 ML {* |
|
672 fun eqsubst_thm ctxt thms thm = |
|
673 let |
|
674 val goalstate = Goal.init (Thm.cprop_of thm) |
|
675 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
|
676 NONE => error "eqsubst_thm" |
|
677 | SOME th => cprem_of th 1 |
|
678 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
|
679 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) |
|
680 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
|
681 in |
|
682 @{thm Pure.equal_elim_rule1} OF [rt,thm] |
|
683 end |
|
684 *} |
|
685 |
|
686 ML {* |
|
687 fun repeat_eqsubst_thm ctxt thms thm = |
|
688 repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm) |
|
689 handle _ => thm |
|
690 *} |
|
691 |
653 ML {* |
692 ML {* |
654 fun build_repabs_term lthy thm constructors rty qty = |
693 fun build_repabs_term lthy thm constructors rty qty = |
655 let |
694 let |
656 fun mk_rep tm = |
695 fun mk_rep tm = |
657 let |
696 let |
700 mk_rep(mk_abs(list_comb(opp,tms))) |
739 mk_rep(mk_abs(list_comb(opp,tms))) |
701 else if tms = [] then opp |
740 else if tms = [] then opp |
702 else list_comb(opp, tms) |
741 else list_comb(opp, tms) |
703 end |
742 end |
704 in |
743 in |
705 MetaSimplifier.rewrite_term @{theory} @{thms id_def_sym} [] |
744 repeat_eqsubst_prop lthy @{thms id_def_sym} |
706 (build_aux lthy (Thm.prop_of thm)) |
745 (build_aux lthy (Thm.prop_of thm)) |
707 end |
746 end |
708 *} |
747 *} |
709 |
748 |
710 text {* Assumes that it is given a regularized theorem *} |
749 text {* Assumes that it is given a regularized theorem *} |
829 end |
868 end |
830 *} |
869 *} |
831 |
870 |
832 section {* Cleaning the goal *} |
871 section {* Cleaning the goal *} |
833 |
872 |
834 text {* Does the same as 'subst' in a given theorem *} |
|
835 ML {* |
|
836 fun eqsubst_thm ctxt thms thm = |
|
837 let |
|
838 val goalstate = Goal.init (Thm.cprop_of thm) |
|
839 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
|
840 NONE => error "eqsubst_thm" |
|
841 | SOME th => cprem_of th 1 |
|
842 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
|
843 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) |
|
844 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
|
845 in |
|
846 @{thm Pure.equal_elim_rule1} OF [rt,thm] |
|
847 end |
|
848 *} |
|
849 |
|
850 ML {* |
|
851 fun repeat_eqsubst_thm ctxt thms thm = |
|
852 repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm) |
|
853 handle _ => thm |
|
854 *} |
|
855 |
|
856 text {* expects atomized definition *} |
873 text {* expects atomized definition *} |
857 ML {* |
874 ML {* |
858 fun add_lower_defs_aux ctxt thm = |
875 fun add_lower_defs_aux ctxt thm = |
859 let |
876 let |
860 val e1 = @{thm fun_cong} OF [thm]; |
877 val e1 = @{thm fun_cong} OF [thm]; |