14   reasoning at the user level, where goals are modified in a sequence of proof

    14   reasoning at the user-level, where goals are modified in a sequence of proof

   104   user level of Isabelle the tactic @{ML foo_tac} or 

   104   user-level of Isabelle the tactic @{ML foo_tac} or 

   332   (unlike @{ML my_print_tac} it prints the goal state as the user would see it). 

   332   (unlike @{ML my_print_tac}, it prints the goal state as the user would see it). 

  1025   powerful simplifier. There are the following five main tactics behind 

  1025   powerful simplifier. The power of simplifier is at the same time a

  1026   the simplifier (in parentheses is their userlevel counterpart)

  1026   strength and a weakness, because you can easily make the simplifier to

  1027   loop and its behaviour can sometimes be difficult to predict. There is also

  1028   a multitude of options that configurate the behaviour of the simplifier. We

  1029   describe some of them in this and the next section.

  1030 

  1031   There are the following five main tactics behind 

  1032   the simplifier (in parentheses is their user-level counterparts):

  1047   corrsponds on the ML-level to the tactic

  1055   corresponds on the ML-level to the tactic

  1054 thm imp_cong simp_implies_cong

  1062 text {*

  1055 

  1063   If the simplifier cannot make any progress, then it leaves the goal unchanged

  1056 text {*

  1064   and does not raise any error message. That means if you use it to unfold a definition

  1057   The crucial information the developer has to control is the simpset

  1065   for a constant and this constant is not present in a goal state, you can still

  1058   to be used by the simplifier. If not handled with care, then the 

  1066   safely apply the simplifier.

  1059   simplifier can easily run forever. 

  1067 

  1060 

  1068   When using the simplifier, the crucial information you have to control is

  1061   It might be surprising that a simpset is quite more complex than just

  1069   the simpset. If not handled with care, then the simplifier can easily run

  1062   a simple list of theorems. One reason for the complexity is that the

  1070   into a loop. It might be surprising that a simpset is more complex than just a

  1063   simplifier must be able to rewrite inside terms and should also be

  1071   simple collection of theorems used as simplification rules. One reason for

  1064   able to rewrite according to rules that have precoditions. The rewriting

  1072   the complexity is that the simplifier must be able to rewrite inside terms

  1065   inside terms requires congruence rules which are meta-equalities 

  1073   and should also be able to rewrite according to rules that have

  1066   typical of the form

  1074   precoditions.

  1075 

  1076 

  1077   The rewriting inside terms requires congruence rules, which

  1078   are meta-equalities typical of the form

  1070                   {@{text "contr t\<^isub>1\<dots>t\<^isub>n \<equiv> contr s\<^isub>1\<dots>s\<^isub>n"}}}

  1083                   {@{text "constr t\<^isub>1\<dots>t\<^isub>n \<equiv> constr s\<^isub>1\<dots>s\<^isub>n"}}}

  1084   \end{center}

  1073   with @{text "constr"} being a term-constructor. However there are also more complicated 

  1087   with @{text "constr"} being a term-constructor. Every simpset contains only

  1074   congruence rules. The user can declare lemmas to be congruence rules using the 

  1088   one concruence rule for each term-constructor, which however can be

  1075   attribute @{text "[cong]"} (theses lemmas are usually equations that are internally 

  1089   overwritten. The user can declare lemmas to be congruence rules using the

  1076   transformed into meta-equations (FIXME: check that).

  1090   attribute @{text "[cong]"}. In HOL, the user usually states these lemmas as

  1077   

  1091   equations, which are then internally transformed into meta-equations.

  1078   The rewriting with rules involving preconditions requires solvers. However

  1092 

  1079   there are also simprocs, which can produce rewrite rules on demand (see 

  1093 

  1080   next section). Another component are split rules, which can simplify for example

  1094   The rewriting with rules involving preconditions requires what is in

  1081   the then and else branches of if-statements under the corresponding 

  1095   Isabelle called a subgoaler, a solver and a looper. These can be arbitrary

  1082   precoditions. (FIXME: loopers and subgoalers?)

  1096   tactics that can be installed in a simpset. However, simpsets also include

  1097   simprocs, which can produce rewrite rules on demand (see next

  1098   section). Another component are split-rules, which can simplify for example

  1099   the ``then'' and ``else'' branches of if-statements under the corresponding

  1100   precoditions.

  1101 

  1102   \begin{readmore}

  1103   For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}

  1104   and @{ML_file "Pure/simplifier.ML"}. The simplifier for HOL is set up in 

  1105   @{ML_file "HOL/Tools/simpdata.ML"}. Generic splitters are implemented in 

  1106   @{ML_file  "Provers/splitter.ML"}.

  1107   \end{readmore}

  1088   @{ML addsimps} & @{ML delsimps}\\

  1113   @{ML addsimps}   & @{ML delsimps}\\

  1089   @{ML addcongs} & @{ML delcongs}\\

  1114   @{ML addcongs}   & @{ML delcongs}\\

  1115   @{ML addsimprocs} & @{ML delsimprocs}\\

  1093   The most frequently used simpsets in HOL are @{ML HOL_basic_ss} and @{ML HOL_ss}.

  1119   (FIXME: What about splitters? @{ML addsplits}, @{ML delsplits})

  1094 *}

  1120 *}

  1095 

  1121 

  1096 ML {* warning (Pretty.string_of (MetaSimplifier.pretty_ss HOL_ss)) *}

  1122 text_raw {*

  1097 

  1123 \begin{figure}[tp]

  1098 ML {*

  1124 \begin{isabelle}*}

  1099 fun get_parts ss = 

  1125 ML{*fun get_parts ss = 

  1101   val ({rules, ...}, {congs, procs, loop_tacs, solvers, ...}) = MetaSimplifier.rep_ss ss

  1127   val ({rules, ...}, {congs, procs, ...}) = MetaSimplifier.rep_ss ss

  1102 in

  1128   

  1103   (rules, congs, procs, loop_tacs, solvers)

  1129   val rules_list = Net.entries rules

  1104 end  

  1130   val rnames = map #name rules_list

  1105 *}

  1131   val rthms =  map #thm rules_list

  1106 

  1132 

  1107 ML {*

  1133   val congs_list = fst congs

  1108   Pretty.big_list

  1134   val cnames = map fst congs_list  

  1109 *}

  1135   val cthms = map (#thm o snd) congs_list

  1110 

  1136 

  1111 

  1137   val proc_list = Net.entries procs

  1112 ML {*

  1138 in

  1113 fun print_ss ss =

  1139   (rnames ~~ rthms, cnames ~~ cthms)

  1114   let

  1140 end

  1115     val pretty_thms = map (enclose "  " "\n" o  Display.string_of_thm)

  1141 

  1116 

  1142 fun print_parts ctxt ss =

  1117     fun pretty_cong (name, {thm, lhs}) =

  1143 let

  1118       name ^ ":" ^ (Display.string_of_thm thm);

  1144   val (simps, congs) = get_parts ss

  1119 

  1145 

  1120     val (rules, congs, procs, loop_tacs, solvers) = get_parts ss;

  1146   fun name_thm (nm, thm) =

  1121     val smps = map #thm (Net.entries rules);

  1147       "  " ^ nm ^ ": " ^ (str_of_thm ctxt thm)

  1122  

  1148 

  1123   in

  1149   val s1 = ["Simplification rules:"]

  1124     "simplification rules:\n" ^ 

  1150   val s2 = map name_thm simps

  1125        (implode (pretty_thms smps)) ^

  1151   val s3 = ["Congruences rules:"]

  1126     "congruences:" ^ (commas (map pretty_cong (fst congs))) ^ "\n" ^

  1152   val s4 = map name_thm congs

  1127     "loopers:" ^ (commas (map (quote o fst) loop_tacs))

  1153 in

  1128   end;

  1154   (s1 @ s2 @ s3 @ s4) 

  1129 *}

  1155      |> separate "\n"

  1130 

  1156      |> implode

  1131 thm FalseE

  1157      |> warning

  1132 

  1158 end*}

  1133 thm simp_impliesI

  1159 text_raw {* 

  1134 lemma "P (Suc 0) \<Longrightarrow> P ?x"

  1160 \end{isabelle}

  1135 apply(tactic {* CHANGED (simp_tac HOL_basic_ss 1) *})

  1161 \caption{The function @{ML MetaSimplifier.rep_ss} returns a record containing

  1136 oops

  1162   a simpset. We are here only interested in the simplifcation rules, congruence rules and

  1137 

  1163   simprocs. The first and third are discrimination nets, which from which we extract

  1138 ML {* warning (print_ss HOL_ss) *}

  1164   lists using @{ML Net.entries}. The congruence rules are stored in 

  1139 

  1165   an association list, associating a constant with a rule.\label{fig:prettyss}}

  1140 text {*

  1166 \end{figure} *}

  1141   @{ML HOL_basic_ss} can deal essentially only with goals of the form: 

  1167 

  1142   @{thm TrueI}, @{thm refl[no_vars]} @{term "x \<equiv> x"} and @{thm FalseE}, 

  1168 text {* 

  1169   To see how they work, consider the two functions in Figure~\ref{fig:prettyss}, which

  1170   print out some parts of a simpset. If you use them to print out the components of the

  1171   empty simpset, the most primitive simpset

  1172   

  1173   @{ML_response_fake [display,gray]

  1174   "print_parts @{context} empty_ss"

  1175 "Simplification rules:

  1176 Congruences rules:"}

  1177 

  1178   you can see it contains nothing. This simpset is usually not useful, except as a 

  1179   building block to build bigger simpsets. For example you can add to @{ML empty_ss} 

  1180   the simplification rule @{thm [source] Diff_Int} as follows:

  1181 *}

  1182 

  1183 ML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}

  1184 

  1185 text {*

  1186   Printing out the components of this simpset gives:

  1187 

  1188   @{ML_response_fake [display,gray]

  1189   "print_parts @{context} ss1"

  1190 "Simplification rules:

  1191   ??.unknown: ?A1 - ?B1 \<inter> ?C1 \<equiv> ?A1 - ?B1 \<union> (?A1 - ?C1)

  1192 Congruences rules:"}

  1193 

  1194   Adding the congruence rule @{thm [source] UN_cong} 

  1195 *}

  1196 

  1197 ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *}

  1198 

  1199 text {*

  1200   gives

  1201 

  1202   @{ML_response_fake [display,gray]

  1203   "print_parts @{context} ss2"

  1204 "Simplification rules:

  1205   ??.unknown: ?A1 - ?B1 \<inter> ?C1 \<equiv> ?A1 - ?B1 \<union> (?A1 - ?C1)

  1206 Congruences rules:

  1207   UNION: \<lbrakk>?A1 = ?B1; \<And>x. x \<in> ?B1 \<Longrightarrow> ?C1 x = ?D1 x\<rbrakk> \<Longrightarrow> 

  1208      \<Union>x\<in>?A1. ?C1 x \<equiv> \<Union>x\<in>?B1. ?D1 x"}

  1209 

  1210   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 

  1211   expects this form of the simplification and congruence rules. However, even 

  1212   adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.

  1213 

  1214   In the context of HOL the first useful simpset is @{ML HOL_basic_ss}. While

  1215   printing out the components of this simpset

  1216 

  1217   @{ML_response_fake [display,gray]

  1218   "print_parts @{context} HOL_basic_ss"

  1219 "Simplification rules:

  1220 Congruences rules:"}

  1221 

  1222   also produces ``nothing'', the printout is misleading. In fact

  1223   the simpset @{ML HOL_basic_ss} is setup so that it can be used to solve goals of the

  1224   form  @{thm TrueI}, @{thm refl[no_vars]}, @{term "t \<equiv> t"} and @{thm FalseE[no_vars]}, 

  1146 ML {* setsubgoaler *}

  1228 lemma 

  1147 

  1229  "True" and "t = t" and "t \<equiv> t" and "False \<Longrightarrow> Foo" and "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"

  1148 text {*

  1230 apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})

  1149   (FIXME: what do the simplifier tactics do when nothing can be rewritten)

  1231 done

  1150 

  1232 

  1233 text {*

  1234   This is because how the tactics for the subgoaler, solver and looper are set 

  1235   up. 

  1236 

  1237   The simpset @{ML HOL_ss}, which is an extention of @{ML HOL_basic_ss}, contains 

  1238   already many useful simplification rules for the logical connectives in HOL. 

  1239 

  1240   @{ML_response_fake [display,gray]

  1241   "print_parts @{context} HOL_ss"

  1242 "Simplification rules:

  1243   Pure.triv_forall_equality: (\<And>x. PROP ?V) \<equiv> PROP ?V

  1244   HOL.the_eq_trivial: THE x. x = ?y \<equiv> ?y

  1245   HOL.the_sym_eq_trivial: THE y. ?y = y \<equiv> ?y

  1246   \<dots>

  1247 Congruences rules:

  1248   HOL.simp_implies: \<dots>

  1249     \<Longrightarrow> (PROP ?P =simp=> PROP ?Q) \<equiv> (PROP ?P' =simp=> PROP ?Q')

  1250   op -->: \<lbrakk>?P \<equiv> ?P'; ?P' \<Longrightarrow> ?Q \<equiv> ?Q'\<rbrakk> \<Longrightarrow> ?P \<longrightarrow> ?Q \<equiv> ?P' \<longrightarrow> ?Q'"}

  1251 

  1252   

  1253   The main point of these simpsets is that they are small enough to

  1254   not cause any loops with most of the simplification rules that

  1255   you might like to add. 

  1256 *}

  1257 

  1258 

  1259 text_raw {*

  1260 \begin{figure}[tp]

  1261 \begin{isabelle} *}

  1262 types  prm = "(nat \<times> nat) list"

  1263 consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a"  ("_ \<bullet> _" [80,80] 80)

  1264 

  1265 primrec (perm_nat)

  1266  "[]\<bullet>c = c"

  1267  "(ab#pi)\<bullet>c = (if (pi\<bullet>c)=fst ab 

  1268                  then snd ab 

  1269                  else (if (pi\<bullet>c)=snd ab then fst ab else (pi\<bullet>c)))" 

  1270 

  1271 primrec (perm_prod)

  1272  "pi\<bullet>(x, y) = (pi\<bullet>x, pi\<bullet>y)"

  1273 

  1274 primrec (perm_list)

  1275  "pi\<bullet>[] = []"

  1276  "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"

  1277 

  1278 lemma perm_append[simp]:

  1279   fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"

  1280   shows "((pi\<^isub>1@pi\<^isub>2)\<bullet>c) = (pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c))"

  1281 by (induct pi\<^isub>1) (auto) 

  1282 

  1283 lemma perm_eq[simp]:

  1284   fixes c::"nat" and pi::"prm"

  1285   shows "(pi\<bullet>c = pi\<bullet>d) = (c = d)" 

  1286 by (induct pi) (auto)

  1287 

  1288 lemma perm_rev[simp]:

  1289   fixes c::"nat" and pi::"prm"

  1290   shows "pi\<bullet>((rev pi)\<bullet>c) = c"

  1291 by (induct pi arbitrary: c) (auto)

  1292 

  1293 lemma perm_compose:

  1294   fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"

  1295   shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)" 

  1296 by (induct pi\<^isub>2) (auto)

  1297 text_raw {*

  1298 \end{isabelle}\medskip

  1299 \caption{A simple theory about permutations over @{typ nat}. The point is that the

  1300   lemma @{thm [source] perm_compose} cannot be directly added to the simplifier, as

  1301   it would cause the simplifier to loop. It can still be used as a simplification 

  1302   rule if the permutation is sufficiently protected.\label{fig:perms}

  1303   (FIXME: Uses old primrec.)}

  1304 \end{figure} *}

  1305 

  1306 

  1307 text {*

  1308   Often the situation arises that simplification rules will cause the

  1309   simplifier to run into an infinite loop. Consider for example the simple

  1310   theory about permutations shown in Figure~\ref{fig:perms}. The purpose of

  1311   the lemmas is to pus permutations as far inside a term where they might

  1312   disappear using the lemma @{thm [source] perm_rev}. However, to fully

  1313   simplifiy all instances, it would be desirable to add also the lemma @{thm

  1314   [source] perm_compose} to the simplifier in order to push permutations over

  1315   other permutations. Unfortunately, the right-hand side of this lemma is

  1316   again an instance of the left-hand side and so causes an infinite

  1317   loop. On the user-level it is difficult to work around such situations

  1318   and we end up with clunky proofs such as:

  1319 *}

  1320 

  1321 lemma 

  1322   fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"

  1323   shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"

  1324 apply(simp)

  1325 apply(rule trans)

  1326 apply(rule perm_compose)

  1327 apply(simp)

  1328 done 

  1329 

  1330 text {*

  1331   On the ML-level, we can however generate a single simplifier tactic that solves

  1332   such proofs. The trick is to introduce an auxiliary constant for permutations 

  1333   and split the simplification into two phases. Let us say the auxiliary constant is

  1334 *}

  1335 

  1336 definition

  1337   perm_aux :: "prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet>aux _" [80,80] 80)

  1338 where

  1339   "pi \<bullet>aux c \<equiv> pi \<bullet> c"

  1340 

  1341 text {* Now the lemmas *}

  1342 

  1343 lemma perm_aux_expand:

  1344   fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"

  1345   shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = pi\<^isub>1 \<bullet>aux (pi\<^isub>2\<bullet>c)" 

  1346 unfolding perm_aux_def by (rule refl)

  1347 

  1348 lemma perm_compose_aux:

  1349   fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"

  1350   shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>aux c) = (pi\<^isub>1\<bullet>pi\<^isub>2) \<bullet>aux (pi\<^isub>1\<bullet>c)" 

  1351 unfolding perm_aux_def by (rule perm_compose)

  1352 

  1353 text {* 

  1354   are simple consequence of the definition and @{thm [source] perm_compose}. 

  1355   More importantly, the lemma @{thm [source] perm_compose_aux} can be safely 

  1356   added to the simplifier, because now the right-hand side is not anymore an instance 

  1357   of the left-hand side. So you can write 

  1358 *}

  1359 

  1360 ML %linenosgray{*val perm_simp_tac =

  1361 let

  1362   val thms1 = [@{thm perm_aux_expand}]

  1363   val thms2 = [@{thm perm_append}, @{thm perm_eq}, @{thm perm_rev}, 

  1364                @{thm perm_compose_aux}] @ @{thms perm_prod.simps} @ 

  1365                @{thms perm_list.simps} @ @{thms perm_nat.simps}

  1366   val thms3 = [@{thm perm_aux_def}]

  1367 in

  1368   simp_tac (HOL_basic_ss addsimps thms1)

  1369   THEN' simp_tac (HOL_basic_ss addsimps thms2)

  1370   THEN' simp_tac (HOL_basic_ss addsimps thms3)

  1371 end*}

  1372 

  1373 text {*

  1374   This trick is not noticable for the user.

  1375 *}

  1376 

  1377 lemma 

  1378   fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"

  1379   shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"

  1380 apply(tactic {* perm_simp_tac 1 *})

  1381 done

  1382 

  1383 

  1384 text {*

  1385   (FIXME: Is it interesting to say something about @{term "op =simp=>"}?)

  1386 

  1387   (FIXME: Unfortunately one cannot access any simproc, as there is 

  1388   no @{text rep_proc} in function @{ML get_parts}.)

  1389 

  1390   (FIXME: What are the second components of the congruence rules---something to

  1391   do with weak congruence constants?)

  1392 

  1393   (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?)