1030   rewrite a term according to a given theorem. They are useful in cases where

  1030   rewrite a term according to theorem. They are useful in cases where

  1053   that the simproc is triggered by the pattern @{term "Suc n"}. For this we

  1053   that the simproc is triggered by the pattern @{term "Suc n"}. This can be

  1054   can add the simproc with this pattern to the current simpset as follows

  1054   done by adding the simproc to the current simproc as follows

  1062   an argument). After this setup, the simplifier is aware of

  1062   an argument about a morphism\footnote{FIXME: what does the morphism do?}). 

  1063   this simproc and you can test whether it fires with the lemma

  1063   After this, the simplifier is aware of the simproc and you can test whether 

  1064   it fires on the lemma

  1072   once for the right-hand side. This is because during simplification the

  1073   once for the right-hand side. The reason is that during simplification the

  1073   simplifier will by default reduce the term @{term "1::nat"} to @{term "Suc

  1074   simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc

  1076   We can add or delete the simproc by the usual methods. For example

  1077   We can add or delete the simproc by the usual \isacommand{declare}-statement. 

  1077   the simproc will be deleted by the declaration:

  1078   For example the simproc will be deleted if you type:

  1095   Now the message shows up only once. 

  1096   Now the message shows up only once since @{term "1::nat"} is left unchanged. 

  1113   Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}.

  1114   Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}

  1114   We can turn this function into a simproc using

  1115   (therefore we printing it out using the function @{ML string_of_term in Syntax}).

  1116   We can turn this function into a proper simproc using

  1119       Simplifier.simproc_i @{theory} "fail_sp'" [@{term "Suc n"}] 

  1121   let 

  1120         (K fail_sp_aux')*}

  1122     val thy = @{theory}

  1123     val pat = [@{term "Suc n"}]

  1124   in

  1125     Simplifier.simproc_i thy "fail_sp'" pat (K fail_sp_aux')

  1126   end*}

  1124 

  1130   The function also takes a list of patterns that can trigger the simproc.

  1125   Simprocs are applied from inside to outside, from left to right. You can see

  1131   It might be interesting to notice that simprocs are applied from inside 

  1126   this in the proof

  1132   to outside and from left to right. You can see this in the proof

  1134   since it prints out the sequence @{term "Suc 0"}, @{term "Suc (Suc 0)"} and 

  1140   since the @{ML fail_sp'}-simproc prints out the sequence 

  1135   @{term "Suc 1"}.

  1141 

  1136 

  1142 @{text [display]

  1137   To see how a simproc applies a theorem  let us rewrite terms according to the 

  1143 "> Suc 0

  1138   equation:

  1144 > Suc (Suc 0) 

  1145 > Suc 1"}

  1146 

  1147   To see how a simproc applies a theorem  let us implement a simproc that

  1148   rewrites terms according to the equation:

  1145   The simproc expects the equation to be a meta-equation, however it can contain 

  1155   Simprocs expect that the given equation is a meta-equation, however the

  1146   possible preconditions (the simproc then only fires if the preconditions can be 

  1156   equation can contain preconditions (the simproc then will only fire if the 

  1147   solved). Let us further assume we want to only rewrite terms greater than 

  1157   preconditions can be solved). To see how rewriting can be tuned precisely, let us 

  1158   further assume we want that the simproc only rewrites terms greater than 

  1151 ML{*fun plus_one_sp_aux thy ss redex =

  1162 ML{*fun plus_one_sp_aux ss redex =

  1160 ML{*val plus_one_sproc = 

  1171 ML{*val plus_one_sp =

  1161        Simplifier.simproc_i @{theory} "sproc +1" [@{term "Suc n"}] 

  1172   let

  1162          plus_one_sp_aux*}

  1173     val thy = @{theory}

  1163 

  1174     val pat = [@{term "Suc n"}] 

  1164 text {*

  1175   in

  1165   Now the simproc fires one every term of the for @{term "Suc n"}, but

  1176     Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)

  1166   the lemma is only applied whenever the term is not @{term "Suc 0"}. So

  1177   end*}

  1167   in 

  1178 

  1179 text {*

  1180   Now the have set up the simproc so that it is triggered by terms

  1181   of the form @{term "Suc n"}, but inside the simproc we only produce

  1182   a theorem if the term is not @{term "Suc 0"}. The result you can see

  1183   in the following proof.

  1171 apply(tactic {* simp_tac (HOL_ss addsimprocs [plus_one_sproc]) 1*})

  1187 apply(tactic {* simp_tac (HOL_ss addsimprocs [plus_one_sp]) 1*})

  1180   where the first argument is rewritten, but not the second. With @{ML

  1196   As usual with simplification you have to be careful with loops: you already have

  1181   plus_one_sproc} you already have to be careful to not cause the simplifier

  1197   one @{ML plus_one_sp}, if you apply if with the default simpset (because

  1182   to loop. If we call this simproc together with the default simpset, we

  1198   the default simpset contains a rule which just undoes the rewriting 

  1183   already have a loop as it contains a rule which just undoes the rewriting of

  1199   @{ML plus_one_sp}).

  1184   the simproc.

  1200 

  1201   Let us next implement a simproc that replaces terms of the form @{term "Suc n"}

  1202   with the number @{text n} increase by one. First we implement a function that

  1203   takes a term and produces the corresponding integer value, if it can.

  1204 

  1190 text {* This function might raise @{ML TERM}. *}

  1210 text {* 

  1211   It uses the library function @{ML dest_number in HOLogic} that transforms

  1212   (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so

  1213   on, into integer values. This function raises the exception @{ML TERM} if

  1214   the term is not a number. The next function expects a pair consisting of a term

  1215   @{text t} and the corresponding integer value @{text n}. 

  1216 *}

  1217 

  1218 ML %linenosgray{*fun get_thm ctxt (t, n) =

  1219 let

  1220   val num = HOLogic.mk_number @{typ "nat"} n

  1221   val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (t,num))

  1222 in

  1223   mk_meta_eq (Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1)))

  1224 end*}

  1225 

  1226 text {*

  1227   From the integer value it generates the corresponding Isabelle term, called 

  1228   @{text num} (Line 3), and then generates the equation @{text "t = num"} (Line 4)

  1229   which it proves by simplification in Line 6. The function @{ML mk_meta_eq} 

  1230   at the outside of the proof just transforms the equality to a meta-equality.

  1231 

  1232   Both functions can be stringed together in the function that produces the 

  1233   actual theorem for the simproc.

  1234 *}

  1204   SOME (mk_meta_eq (get_thm (t,dest_suc_trm t)))

  1240   SOME (get_thm ctxt (t, dest_suc_trm t))

  1209   (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following loops.)

  1245   (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following will loop.)

  1210 *}

  1246 

  1211 

  1247   This function uses the fact that @{ML dest_suc_trm} might throw an exception 

  1212 ML{*val nat_number_sp = 

  1248   @{ML TERM}. In this case there is nothing that can be rewritten and therefore no

  1213        Simplifier.simproc_i @{theory} "nat_number" [@{term "Suc n"}] 

  1249   theorem is produced. To try out the simproc on an example, you can set it up as 

  1214          (K nat_number_sp_aux) *}

  1250   follows:

  1251 *}

  1252 

  1253 ML{*val nat_number_sp =

  1254   let

  1255     val thy = @{theory}

  1256     val pat = [@{term "Suc n"}]

  1257   in 

  1258     Simplifier.simproc_i thy "nat_number" pat (K nat_number_sp_aux) 

  1259   end*}

  1260 

  1261 text {* 

  1262   Now in the lemma

  1263   *}