831 |
831 |
832 \<^descr> @{command "simproc_setup"} defines a named simplification |
832 \<^descr> @{command "simproc_setup"} defines a named simplification |
833 procedure that is invoked by the Simplifier whenever any of the |
833 procedure that is invoked by the Simplifier whenever any of the |
834 given term patterns match the current redex. The implementation, |
834 given term patterns match the current redex. The implementation, |
835 which is provided as ML source text, needs to be of type @{ML_type |
835 which is provided as ML source text, needs to be of type @{ML_type |
836 "morphism -> simpset -> cterm -> thm option"}, where the @{ML_type |
836 "morphism -> Proof.context -> cterm -> thm option"}, where the @{ML_type |
837 cterm} represents the current redex \<open>r\<close> and the result is |
837 cterm} represents the current redex \<open>r\<close> and the result is |
838 supposed to be some proven rewrite rule \<open>r \<equiv> r'\<close> (or a |
838 supposed to be some proven rewrite rule \<open>r \<equiv> r'\<close> (or a |
839 generalized version), or @{ML NONE} to indicate failure. The |
839 generalized version), or @{ML NONE} to indicate failure. The |
840 @{ML_type simpset} argument holds the full context of the current |
840 @{ML_type Proof.context} argument holds the full context of the current |
841 Simplifier invocation, including the actual Isar proof context. The |
841 Simplifier invocation. The |
842 @{ML_type morphism} informs about the difference of the original |
842 @{ML_type morphism} informs about the difference of the original |
843 compilation context wrt.\ the one of the actual application later |
843 compilation context wrt.\ the one of the actual application later |
844 on. The optional @{keyword "identifier"} specifies theorems that |
844 on. The optional @{keyword "identifier"} specifies theorems that |
845 represent the logical content of the abstract theory of this |
845 represent the logical content of the abstract theory of this |
846 simproc. |
846 simproc. |