784 | SOME th => cprem_of th 1 |
784 | SOME th => cprem_of th 1 |
785 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
785 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
786 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) |
786 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) |
787 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
787 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
788 in |
788 in |
789 Simplifier.rewrite_rule [rt] thm |
789 @{thm Pure.equal_elim_rule1} OF [rt,thm] |
790 end |
790 end |
|
791 *} |
|
792 |
|
793 ML {* |
|
794 fun repeat_eqsubst_thm ctxt thms thm = |
|
795 repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm) |
|
796 handle _ => thm |
791 *} |
797 *} |
792 |
798 |
793 text {* expects atomized definition *} |
799 text {* expects atomized definition *} |
794 ML {* |
800 ML {* |
795 fun add_lower_defs_aux ctxt thm = |
801 fun add_lower_defs_aux ctxt thm = |
796 let |
802 let |
797 val e1 = @{thm fun_cong} OF [thm] |
803 val e1 = @{thm fun_cong} OF [thm]; |
798 val f = eqsubst_thm ctxt @{thms fun_map.simps} e1 |
804 val f = eqsubst_thm ctxt @{thms fun_map.simps} e1; |
|
805 val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f; |
|
806 val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I} g; |
|
807 val i = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] h |
799 in |
808 in |
800 thm :: (add_lower_defs_aux ctxt f) |
809 thm :: (add_lower_defs_aux ctxt i) |
801 end |
810 end |
802 handle _ => [thm] |
811 handle _ => [thm] |
803 *} |
812 *} |
804 |
813 |
805 ML {* |
814 ML {* |