
diff -r 0c32a609fcad -r a0bdee64194c doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Thu Feb 05 10:26:16 1998 +0100
+++ b/doc-src/Ref/simplifier.tex	Thu Feb 05 10:26:59 1998 +0100
@@ -91,13 +91,13 @@
 by (Asm_simp_tac 1);
 \end{ttbox}
 
-\medskip {\tt Asm_full_simp_tac} is the most powerful of this quartet
+\medskip \texttt{Asm_full_simp_tac} is the most powerful of this quartet
 of tactics but may also loop where some of the others terminate.  For
 example,
 \begin{ttbox}
 {\out  1. ALL x. f x = g (f (g x)) ==> f 0 = f 0 + 0}
 \end{ttbox}
-is solved by {\tt Simp_tac}, but {\tt Asm_simp_tac} and {\tt
+is solved by \texttt{Simp_tac}, but \texttt{Asm_simp_tac} and {\tt
   Asm_simp_tac} loop because the rewrite rule $f\,\Var{x} =
 g\,(f\,(g\,\Var{x}))$ extracted from the assumption does not
 terminate.  Isabelle notices certain simple forms of nontermination,
@@ -366,10 +366,10 @@
 
 \begin{ttdescription}
   
-\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds simplification
+\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds the simplification
   procedures $procs$ to the current simpset.
   
-\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes simplification
+\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes the simplification
   procedures $procs$ from the current simpset.
 
 \end{ttdescription}
@@ -505,7 +505,7 @@
 
 The solver is a pair of tactics that attempt to solve a subgoal after
 simplification.  Typically it just proves trivial subgoals such as
-{\tt True} and $t=t$.  It could use sophisticated means such as {\tt
+\texttt{True} and $t=t$.  It could use sophisticated means such as {\tt
   blast_tac}, though that could make simplification expensive.
 
 Rewriting does not instantiate unknowns.  For example, rewriting
@@ -564,7 +564,7 @@
 the solver.  For this reason, solver tactics must be prepared to solve
 goals of the form $t = \Var{x}$, usually by reflexivity.  In
 particular, reflexivity should be tried before any of the fancy
-tactics like {\tt blast_tac}.
+tactics like \texttt{blast_tac}.
 
 It may even happen that due to simplification the subgoal is no longer
 an equality.  For example $False \bimp \Var{Q}$ could be rewritten to
@@ -846,7 +846,7 @@
 {\out val prem = "f(Suc(?n)) = Suc(f(?n))}
 {\out             [!!n. f(Suc(n)) = Suc(f(n))]" : thm}
 \end{ttbox}
-In the theorem~{\tt prem}, note that $f$ is a free variable while
+In the theorem~\texttt{prem}, note that $f$ is a free variable while
 $\Var{n}$ is a schematic variable.
 \begin{ttbox}
 by (res_inst_tac [("n","i")] induct 1);
@@ -958,7 +958,7 @@
 
 \item To complete your set of rewrite rules, you must add not just
   associativity~(A) and commutativity~(C) but also a derived rule, {\bf
-    left-commutativity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
+    left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
 \end{itemize}
 Ordered rewriting with the combination of A, C, and~LC sorts a term
 lexicographically:
@@ -973,14 +973,14 @@
 This example is again set in \HOL\ (see \texttt{HOL/ex/NatSum}).
 Theory \thydx{Arith} contains natural numbers arithmetic.  Its
 associated simpset contains many arithmetic laws including
-distributivity of~$\times$ over~$+$, while {\tt add_ac} is a list
+distributivity of~$\times$ over~$+$, while \texttt{add_ac} is a list
 consisting of the A, C and LC laws for~$+$ on type \texttt{nat}.  Let
 us prove the theorem
 \[ \sum@{i=1}^n i = n\times(n+1)/2. \]
 %
-A functional~{\tt sum} represents the summation operator under the
-interpretation ${\tt sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$.  We
-extend {\tt Arith} as follows:
+A functional~\texttt{sum} represents the summation operator under the
+interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$.  We
+extend \texttt{Arith} as follows:
 \begin{ttbox}
 NatSum = Arith +
 consts sum     :: [nat=>nat, nat] => nat
@@ -997,7 +997,7 @@
 Delsimprocs nat_cancel;
 Addsimps add_ac;
 \end{ttbox}
-Our desired theorem now reads ${\tt sum} \, (\lambda i.i) \, (n+1) =
+Our desired theorem now reads $\texttt{sum} \, (\lambda i.i) \, (n+1) =
 n\times(n+1)/2$.  The Isabelle goal has both sides multiplied by~$2$:
 \begin{ttbox}
 goal NatSum.thy "2 * sum (\%i.i) (Suc n) = n * Suc n";
@@ -1032,7 +1032,7 @@
 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
 {\out No subgoals!}
 \end{ttbox}
-Simplification cannot prove the induction step if we omit {\tt add_ac} from
+Simplification cannot prove the induction step if we omit \texttt{add_ac} from
 the simpset.  Observe that like terms have not been collected:
 \begin{ttbox}
 {\out Level 3}
@@ -1050,7 +1050,7 @@
 
 
 \subsection{Re-orienting equalities}
-Ordered rewriting with the derived rule {\tt symmetry} can reverse
+Ordered rewriting with the derived rule \texttt{symmetry} can reverse
 equations:
 \begin{ttbox}
 val symmetry = prove_goal HOL.thy "(x=y) = (y=x)"
@@ -1058,16 +1058,16 @@
 \end{ttbox}
 This is frequently useful.  Assumptions of the form $s=t$, where $t$ occurs
 in the conclusion but not~$s$, can often be brought into the right form.
-For example, ordered rewriting with {\tt symmetry} can prove the goal
+For example, ordered rewriting with \texttt{symmetry} can prove the goal
 \[ f(a)=b \conj f(a)=c \imp b=c. \]
-Here {\tt symmetry} reverses both $f(a)=b$ and $f(a)=c$
+Here \texttt{symmetry} reverses both $f(a)=b$ and $f(a)=c$
 because $f(a)$ is lexicographically greater than $b$ and~$c$.  These
 re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the
 conclusion by~$f(a)$. 
 
 Another example is the goal $\neg(t=u) \imp \neg(u=t)$.
 The differing orientations make this appear difficult to prove.  Ordered
-rewriting with {\tt symmetry} makes the equalities agree.  (Without
+rewriting with \texttt{symmetry} makes the equalities agree.  (Without
 knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$
 or~$u=t$.)  Then the simplifier can prove the goal outright.
 
@@ -1126,7 +1126,8 @@
 \begin{ttbox}
 local
   val lhss =
-    [read_cterm (sign_of Prod.thy) ("f::'a*'b=>'c", TVar (("'z", 0), []))];
+    [read_cterm (sign_of Prod.thy) 
+                ("f::'a*'b=>'c", TVar (("'z", 0), []))];
   val rew = mk_meta_eq pair_eta_expand; \medskip
   fun proc _ _ (Abs _) = Some rew
     | proc _ _ _ = None;
@@ -1165,10 +1166,10 @@
 use "$ISABELLE_HOME/src/Provers/splitter.ML";
 \end{ttbox}
 
-Simplification requires reflecting various object-equalities to
-meta-level rewrite rules.  This demands rules stating that equal terms
-and equivalent formulae are also equal at the meta-level.  The rule
-declaration part of the file {\tt FOL/IFOL.thy} contains the two lines
+Simplification requires converting object-equalities to meta-level rewrite
+rules.  This demands rules stating that equal terms and equivalent formulae
+are also equal at the meta-level.  The rule declaration part of the file
+\texttt{FOL/IFOL.thy} contains the two lines
 \begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem}
 eq_reflection   "(x=y)   ==> (x==y)"
 iff_reflection  "(P<->Q) ==> (P==Q)"
@@ -1177,7 +1178,7 @@
 particular logic.  In Constructive Type Theory, equality is a ternary
 relation of the form $a=b\in A$; the type~$A$ determines the meaning
 of the equality essentially as a partial equivalence relation.  The
-present simplifier cannot be used.  Rewriting in {\tt CTT} uses
+present simplifier cannot be used.  Rewriting in \texttt{CTT} uses
 another simplifier, which resides in the file {\tt
   Provers/typedsimp.ML} and is not documented.  Even this does not
 work for later variants of Constructive Type Theory that use
@@ -1198,7 +1199,7 @@
                   (IntPr.fast_tac 1) ]));
 \end{ttbox}
 The following rewrite rules about conjunction are a selection of those
-proved on {\tt FOL/simpdata.ML}.  Later, these will be supplied to the
+proved on \texttt{FOL/simpdata.ML}.  Later, these will be supplied to the
 standard simpset.
 \begin{ttbox}
 val conj_simps = map int_prove_fun
@@ -1225,20 +1226,20 @@
 setmksimps : simpset * (thm -> thm list) -> simpset \hfill{\bf infix 4}
 \end{ttbox}
 The next step is to define the function for preprocessing rewrite rules.
-This will be installed by calling {\tt setmksimps} below.  Preprocessing
+This will be installed by calling \texttt{setmksimps} below.  Preprocessing
 occurs whenever rewrite rules are added, whether by user command or
 automatically.  Preprocessing involves extracting atomic rewrites at the
 object-level, then reflecting them to the meta-level.
 
-To start, the function {\tt gen_all} strips any meta-level
+To start, the function \texttt{gen_all} strips any meta-level
 quantifiers from the front of the given theorem.  Usually there are none
 anyway.
 \begin{ttbox}
 fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
 \end{ttbox}
-The function {\tt atomize} analyses a theorem in order to extract
+The function \texttt{atomize} analyses a theorem in order to extract
 atomic rewrite rules.  The head of all the patterns, matched by the
-wildcard~{\tt _}, is the coercion function {\tt Trueprop}.
+wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}.
 \begin{ttbox}
 fun atomize th = case concl_of th of 
     _ $ (Const("op &",_) $ _ $ _)   => atomize(th RS conjunct1) \at
@@ -1260,21 +1261,21 @@
 \item Universal quantification: remove the quantifier, replacing the bound
   variable by a schematic variable, and extract rewrites from the body.
 
-\item {\tt True} and {\tt False} contain no useful rewrites.
+\item \texttt{True} and \texttt{False} contain no useful rewrites.
 
 \item Anything else: return the theorem in a singleton list.
 \end{itemize}
 The resulting theorems are not literally atomic --- they could be
 disjunctive, for example --- but are broken down as much as possible.  See
-the file {\tt ZF/simpdata.ML} for a sophisticated translation of
+the file \texttt{ZF/simpdata.ML} for a sophisticated translation of
 set-theoretic formulae into rewrite rules.
 
 The simplified rewrites must now be converted into meta-equalities.  The
-rule {\tt eq_reflection} converts equality rewrites, while {\tt
+rule \texttt{eq_reflection} converts equality rewrites, while {\tt
   iff_reflection} converts if-and-only-if rewrites.  The latter possibility
 can arise in two other ways: the negative theorem~$\neg P$ is converted to
-$P\equiv{\tt False}$, and any other theorem~$P$ is converted to
-$P\equiv{\tt True}$.  The rules {\tt iff_reflection_F} and {\tt
+$P\equiv\texttt{False}$, and any other theorem~$P$ is converted to
+$P\equiv\texttt{True}$.  The rules \texttt{iff_reflection_F} and {\tt
   iff_reflection_T} accomplish this conversion.
 \begin{ttbox}
 val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
@@ -1283,7 +1284,7 @@
 val P_iff_T = int_prove_fun "P ==> (P <-> True)";
 val iff_reflection_T = P_iff_T RS iff_reflection;
 \end{ttbox}
-The function {\tt mk_meta_eq} converts a theorem to a meta-equality
+The function \texttt{mk_meta_eq} converts a theorem to a meta-equality
 using the case analysis described above.
 \begin{ttbox}
 fun mk_meta_eq th = case concl_of th of
@@ -1292,13 +1293,13 @@
   | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
   | _                           => th RS iff_reflection_T;
 \end{ttbox}
-The three functions {\tt gen_all}, {\tt atomize} and {\tt mk_meta_eq} will
-be composed together and supplied below to {\tt setmksimps}.
+The three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_meta_eq} will
+be composed together and supplied below to \texttt{setmksimps}.
 
 
 \subsection{Making the initial simpset}
 
-It is time to assemble these items.  We open module {\tt Simplifier}
+It is time to assemble these items.  We open module \texttt{Simplifier}
 to gain direct access to its components.  We define the infix operator
 \ttindex{addcongs} to insert congruence rules; given a list of
 theorems, it converts their conclusions into meta-equalities and
@@ -1317,16 +1318,16 @@
 fun ss addsplits splits = ss addloop (split_tac splits);
 \end{ttbox}
 
-The list {\tt IFOL_simps} contains the default rewrite rules for
-first-order logic.  The first of these is the reflexive law expressed
-as the equivalence $(a=a)\bimp{\tt True}$; the rewrite rule $a=a$ is
+The list \texttt{IFOL_simps} contains the default rewrite rules for
+intuitionistic first-order logic.  The first of these is the reflexive law
+expressed as the equivalence $(a=a)\bimp\texttt{True}$; the rewrite rule $a=a$ is
 clearly useless.
 \begin{ttbox}
 val IFOL_simps =
    [refl RS P_iff_T] \at conj_simps \at disj_simps \at not_simps \at 
     imp_simps \at iff_simps \at quant_simps;
 \end{ttbox}
-The list {\tt triv_rls} contains trivial theorems for the solver.  Any
+The list \texttt{triv_rls} contains trivial theorems for the solver.  Any
 subgoal that is simplified to one of these will be removed.
 \begin{ttbox}
 val notFalseI = int_prove_fun "~False";
@@ -1335,15 +1336,15 @@
 %
 The basic simpset for intuitionistic \FOL{} is
 \ttindexbold{FOL_basic_ss}.  It preprocess rewrites using {\tt
-  gen_all}, {\tt atomize} and {\tt mk_meta_eq}.  It solves simplified
-subgoals using {\tt triv_rls} and assumptions, and by detecting
+  gen_all}, \texttt{atomize} and \texttt{mk_meta_eq}.  It solves simplified
+subgoals using \texttt{triv_rls} and assumptions, and by detecting
 contradictions.  It uses \ttindex{asm_simp_tac} to tackle subgoals of
 conditional rewrites.
 
-Other simpsets built from {\tt FOL_basic_ss} will inherit these items.
+Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.
 In particular, \ttindexbold{IFOL_ss}, which introduces {\tt
   IFOL_simps} as rewrite rules.  \ttindexbold{FOL_ss} will later
-extend {\tt IFOL_ss} with classical rewrite rules such as $\neg\neg
+extend \texttt{IFOL_ss} with classical rewrite rules such as $\neg\neg
 P\bimp P$.
 \index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler}
 \index{*addsimps}\index{*addcongs}
@@ -1355,20 +1356,22 @@
                                  eq_assume_tac, ematch_tac [FalseE]];
 
 val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
-                            addsimprocs [defALL_regroup,defEX_regroup]
+                            addsimprocs [defALL_regroup, defEX_regroup]
                             setSSolver   safe_solver
                             setSolver  unsafe_solver
-                            setmksimps (map mk_meta_eq o atomize o gen_all);
+                            setmksimps (map mk_meta_eq o 
+                                        atomize o gen_all);
 
-val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps {\at} int_ex_simps {\at} int_all_simps)
+val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps {\at} 
+                                     int_ex_simps {\at} int_all_simps)
                            addcongs [imp_cong];
 \end{ttbox}
-This simpset takes {\tt imp_cong} as a congruence rule in order to use
+This simpset takes \texttt{imp_cong} as a congruence rule in order to use
 contextual information to simplify the conclusions of implications:
 \[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp
    (\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'})
 \]
-By adding the congruence rule {\tt conj_cong}, we could obtain a similar
+By adding the congruence rule \texttt{conj_cong}, we could obtain a similar
 effect for conjunctions.
 
 
@@ -1376,7 +1379,7 @@
 
 To set up case splitting, we must prove the theorem \texttt{meta_iffD}
 below and pass it to \ttindexbold{mk_case_split_tac}.  The tactic
-\ttindexbold{split_tac} uses {\tt mk_meta_eq}, defined above, to
+\ttindexbold{split_tac} uses \texttt{mk_meta_eq}, defined above, to
 convert the splitting rules to meta-equalities.
 \begin{ttbox}
 val meta_iffD = 
@@ -1399,7 +1402,7 @@
 \langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) 
 \] 
 Case splits should be allowed only when necessary; they are expensive
-and hard to control.  Here is an example of use, where {\tt expand_if}
+and hard to control.  Here is an example of use, where \texttt{expand_if}
 is the first rule above:
 \begin{ttbox}
 by (simp_tac (simpset() addloop (split_tac [expand_if])) 1);




