added section on "Reordering assumptions".
Fri, 28 Jul 1995 19:17:03 +0200
changeset 1213 a8f6d0fa2a59
parent 1212 7059356e18e0
child 1214 3f3888213ceb
added section on "Reordering assumptions".
--- a/doc-src/Ref/simplifier.tex	Fri Jul 28 18:05:50 1995 +0200
+++ b/doc-src/Ref/simplifier.tex	Fri Jul 28 19:17:03 1995 +0200
@@ -254,6 +254,16 @@
   one.  Working from left to right, it uses each assumption in the
   simplification of those following.
+  Since \verb$asm_full_simp_tac$ works from left to right, it sometimes
+misses opportunities for simplification: given the subgoal
+{\out [| P(f(a)); f(a) = t |] ==> ...}
+\verb$asm_full_simp_tac$ will not simplify the first assumption using the
+second but will leave the assumptions unchanged. See
+\S\ref{sec:reordering-asms} for ways around this problem.
 Using the simplifier effectively may take a bit of experimentation.  The
 tactics can be traced with the ML command \verb$trace_simp := true$.  To
 remind yourself of what is in a simpset, use the function \verb$rep_ss$ to
@@ -417,6 +427,40 @@
 {\out No subgoals!}
+\subsection{Reordering assumptions}
+As mentioned above, \ttindex{asm_full_simp_tac} may require the assumptions
+to be permuted to be more effective. Given the subgoal
+{\out 1. [| P(f(a)); Q; f(a) = t; R |] ==> S}
+we can rotate the assumptions two positions to the right
+by (rotate_tac ~2 1);
+to obtain
+{\out 1. [| f(a) = t; R; P(f(a)); Q |] ==> S}
+which enables \verb$asm_full_simp_tac$ to simplify \verb$P(f(a))$ to
+Since rotation alone cannot produce arbitrary permutations, you can also pick
+out a particular assumption which needs to be rewritten and move it the the
+right end of the assumptions. In the above case rotation can be replaced by
+by (dres_inst_tac [("psi","P(f(a))")] asm_rl 1);
+which is more directed and leads to
+{\out 1. [| Q; f(a) = t; R; P(f(a)) |] ==> S}
+Note that reordering assumptions usually leads to brittle proofs and should
+therefore be avoided. Future versions of \verb$asm_full_simp_tac$ may remove
+the need for such manipulations.
 \section{Permutative rewrite rules}
 \index{rewrite rules!permutative|(}