1021   Something about simprocs.

  1023 *}

  1022 

  1024 

  1023 *}

  1025 section {* Simprocs *}

  1026 

  1027 text {*

  1028   In Isabelle you can also implement custom simplification procedures, called

  1029   \emph{simprocs}. Simprocs can be triggered on a specified term-pattern and

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

  1031   a rewriting rule must be produced on ``demand'' or when rewriting by

  1032   simplification is too unpredictable and potentially loops.

  1033 

  1034   To see how simprocs work, let us first write a simproc that just prints out

  1035   the pattern that triggers it and otherwise does nothing. For this

  1036   you can use the function:

  1037 *}

  1038 

  1039 ML %linenosgray{*fun fail_sp_aux simpset redex = 

  1040 let

  1041   val ctxt = Simplifier.the_context simpset

  1042   val _ = warning ("The redex: " ^ (str_of_cterm ctxt redex))

  1043 in

  1044   NONE

  1045 end*}

  1046 

  1047 text {*

  1048   This function takes a simpset and a redex (a @{ML_type cterm}) as

  1049   argument. In Lines 3 and~4, we first extract the context from the given

  1050   simpset and then print out a message containing the redex.  The function

  1051   returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the

  1052   moment we are \emph{not} interested in actually rewriting anything. We want

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

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

  1055 *}

  1056 

  1057 simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *}

  1058 

  1059 text {*

  1060   where the second argument specifies the pattern and the right-hand side

  1061   contains the code of the simproc (we have to use @{ML K} since we ignoring

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

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

  1064 *}

  1065 

  1066 lemma shows "Suc 0 = 1"

  1067 apply(simp)

  1068 (*<*)oops(*>*)

  1069 

  1070 text {*

  1071   This will print out the message twice: once for the left-hand side and

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

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

  1074   0"}, and then the simproc ``fires'' also on that term. 

  1075 

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

  1077   the simproc will be deleted by the declaration:

  1078 *}

  1079 

  1080 declare [[simproc del: fail_sp]]

  1081 

  1082 text {*

  1083   If you want to see what happens with just \emph{this} simproc, without any 

  1084   interference from other rewrite rules, you can call @{text fail_sp} 

  1085   as follows:

  1086 *}

  1087 

  1088 lemma shows "Suc 0 = 1"

  1089 apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc fail_sp}]) 1*})

  1090 (*<*)oops(*>*)

  1091 

  1092 text {*

  1093   (FIXME: should one use HOL-basic-ss or HOL-ss?)

  1094 

  1095   Now the message shows up only once. 

  1096 

  1097   Setting up a simproc using the command \isacommand{setup\_simproc} will

  1098   always add automatically the simproc to the current simpset. If you do not

  1099   want this, then you have to use a slightly different method for setting 

  1100   up the simproc. First the function @{ML fail_sp_aux} needs to be modified

  1101   to

  1102 *}

  1103 

  1104 ML{*fun fail_sp_aux' simpset redex = 

  1105 let

  1106   val ctxt = Simplifier.the_context simpset

  1107   val _ = warning ("The redex: " ^ (Syntax.string_of_term ctxt redex))

  1108 in

  1109   NONE

  1110 end*}

  1111 

  1112 text {*

  1113   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 *}

  1116 

  1117 

  1118 ML{*val fail_sp' = 

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

  1120         (K fail_sp_aux')*}

  1121 

  1122 text {*

  1123   Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).

  1124 

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

  1126   this in the proof

  1127 *}

  1128 

  1129 lemma shows "Suc (Suc 0) = (Suc 1)"

  1130 apply(tactic {* simp_tac (HOL_ss addsimprocs [fail_sp']) 1*})

  1131 (*<*)oops(*>*)

  1132 

  1133 text {*

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

  1135   @{term "Suc 1"}.

  1136 

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

  1138   equation:

  1139 *}

  1140 

  1141 lemma plus_one: 

  1142   shows "Suc n \<equiv> n + 1" by simp

  1143 

  1144 text {*

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

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

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

  1148   @{term "Suc 0"}. For this we can write

  1149 *}

  1150 

  1151 ML{*fun plus_one_sp_aux thy ss redex =

  1152   case redex of

  1153     @{term "Suc 0"} => NONE

  1154   | _ => SOME @{thm plus_one}*}

  1155 

  1156 text {*

  1157   and set up the simproc as follows.

  1158 *}

  1159 

  1160 ML{*val plus_one_sproc = 

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

  1162          plus_one_sp_aux*}

  1163 

  1164 text {*

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

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

  1167   in 

  1168 *}

  1169 

  1170 lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"

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

  1172 txt{*

  1173   the simproc produces the goal state

  1174 

  1175   @{subgoals[display]}

  1176 *}  

  1177 (*<*)oops(*>*)

  1178 

  1179 text {*

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

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

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

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

  1184   the simproc.

  1185 *}

  1186 

  1187 ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t

  1188   | dest_suc_trm t = snd (HOLogic.dest_number t)*}

  1189 

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

  1191 

  1192 ML{*fun nat_number_sp_aux ss t =

  1193 let 

  1194   val ctxt = Simplifier.the_context ss

  1195 

  1196   fun get_thm (t, n) =

  1197   let

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

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

  1200   in

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

  1202   end

  1203 in

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

  1205   handle TERM _ => NONE

  1206 end*}

  1207 

  1208 text {*

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

  1210 *}

  1211 

  1212 ML{*val nat_number_sp = 

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

  1214          (K nat_number_sp_aux) *}

  1215 

  1216 lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"

  1217   apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})

  1218 txt {* 

  1219   @{subgoals [display]}

  1220   *}

  1221 (*<*)oops(*>*)