Removed obsolete section about reordering assumptions.
Mon, 04 Nov 2002 14:17:00 +0100
changeset 13693 77052bb8aed3
parent 13692 27f3c83e2984
child 13694 be3e2fa01b0f
Removed obsolete section about reordering assumptions.
--- a/doc-src/Ref/simplifier.tex	Fri Nov 01 17:44:26 2002 +0100
+++ b/doc-src/Ref/simplifier.tex	Mon Nov 04 14:17:00 2002 +0100
@@ -113,8 +113,8 @@
 gives rise to the infinite reduction sequence
-P\,(f\,x) \stackrel{f\,x = f\,y}{\mapsto} P\,(f\,y) \stackrel{y = x}{\mapsto}
-P\,(f\,x) \stackrel{f\,x = f\,y}{\mapsto} \cdots
+P\,(f\,x) \stackrel{f\,x = f\,y}{\longmapsto} P\,(f\,y) \stackrel{y = x}{\longmapsto}
+P\,(f\,x) \stackrel{f\,x = f\,y}{\longmapsto} \cdots
 whereas applying the same tactic to
@@ -976,45 +976,6 @@
 {\out No subgoals!}
-\subsection{Reordering assumptions}
-As mentioned in {\S}\ref{sec:simp-for-dummies-tacs},
-\ttindex{asm_full_simp_tac} may require the assumptions to be permuted
-to be more effective.  Given the subgoal
-{\out 1. [| ALL x. P x --> f x = g x; Q(f a); P a; R |] ==> S}
-we can rotate the assumptions two positions to the right
-by (rotate_tac ~2 1);
-to obtain
-{\out 1. [| P a; R; ALL x. P x --> f x = g x; Q(f a) |] ==> S}
-which enables \verb$asm_full_simp_tac$ to simplify \verb$Q(f a)$ to
-\verb$Q(g a)$ because now all required assumptions are to the left of
-\verb$Q(f a)$.
-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","Q(f a)")] asm_rl 1);
-which is more directed and leads to
-{\out 1. [| ALL x. P x --> f x = g x; P a; R; Q(f a) |] ==> S}
-  Reordering assumptions usually leads to brittle proofs and should be
-  avoided.  Future versions of \verb$asm_full_simp_tac$ will completely
-  remove the need for such manipulations.
 \section{Permutative rewrite rules}
 \index{rewrite rules!permutative|(}