874 we need to match the conclusion of |
874 we need to match the conclusion of |
875 @{thm [source] rule} against the goal reading off an instantiation for |
875 @{thm [source] rule} against the goal reading off an instantiation for |
876 @{thm [source] rule}. For this the function @{ML_ind first_order_match in Thm} |
876 @{thm [source] rule}. For this the function @{ML_ind first_order_match in Thm} |
877 matches two @{ML_type cterm}s and produces, in the successful case, a matcher |
877 matches two @{ML_type cterm}s and produces, in the successful case, a matcher |
878 that can be used to instantiate the theorem. The instantiation |
878 that can be used to instantiate the theorem. The instantiation |
879 can be done with the function @{ML_ind instantiate in Drule}. To automate |
879 can be done with the function @{ML_ind instantiate_normalize in Drule}. To automate |
880 this we implement the following function. |
880 this we implement the following function. |
881 *} |
881 *} |
882 |
882 |
883 ML %linenosgray{*fun fo_rtac thm = Subgoal.FOCUS (fn {concl, ...} => |
883 ML %linenosgray{*fun fo_rtac thm = Subgoal.FOCUS (fn {concl, ...} => |
884 let |
884 let |
885 val concl_pat = Drule.strip_imp_concl (cprop_of thm) |
885 val concl_pat = Drule.strip_imp_concl (cprop_of thm) |
886 val insts = Thm.first_order_match (concl_pat, concl) |
886 val insts = Thm.first_order_match (concl_pat, concl) |
887 in |
887 in |
888 rtac (Drule.instantiate insts thm) 1 |
888 rtac (Drule.instantiate_normalize insts thm) 1 |
889 end)*} |
889 end)*} |
890 |
890 |
891 text {* |
891 text {* |
892 Note that we use @{ML FOCUS in Subgoal} because it gives us directly access |
892 Note that we use @{ML FOCUS in Subgoal} because it gives us directly access |
893 to the conclusion of the goal state, but also because this function |
893 to the conclusion of the goal state, but also because this function |