
diff -r 3751567696bf -r 66fc71f3a347 doc-src/Intro/advanced.tex
--- a/doc-src/Intro/advanced.tex	Wed Apr 06 16:36:34 1994 +0200
+++ b/doc-src/Intro/advanced.tex	Fri Apr 15 11:35:44 1994 +0200
@@ -28,30 +28,30 @@
 A mathematical development goes through a progression of stages.  Each
 stage defines some concepts and derives rules about them.  We shall see how
 to derive rules, perhaps involving definitions, using Isabelle.  The
-following section will explain how to declare types, constants, axioms and
+following section will explain how to declare types, constants, rules and
 definitions.
 
 
 \subsection{Deriving a rule using tactics and meta-level assumptions} 
 \label{deriving-example}
-\index{examples!of deriving rules}
+\index{examples!of deriving rules}\index{assumptions!of main goal}
 
 The subgoal module supports the derivation of rules, as discussed in
 \S\ref{deriving}.  The \ttindex{goal} command, when supplied a goal of the
 form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates $\phi\Imp\phi$
 as the initial proof state and returns a list consisting of the theorems
 ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$.  These meta-assumptions
-are also recorded internally, allowing \ttindex{result} to discharge them
+are also recorded internally, allowing {\tt result} to discharge them
 in the original order.
 
 Let us derive $\conj$ elimination using Isabelle.
-Until now, calling \ttindex{goal} has returned an empty list, which we have
+Until now, calling {\tt goal} has returned an empty list, which we have
 thrown away.  In this example, the list contains the two premises of the
 rule.  We bind them to the \ML\ identifiers {\tt major} and {\tt
 minor}:\footnote{Some ML compilers will print a message such as {\em
 binding not exhaustive}.  This warns that {\tt goal} must return a
 2-element list.  Otherwise, the pattern-match will fail; ML will
-raise exception \ttindex{Match}.}
+raise exception \xdx{Match}.}
 \begin{ttbox}
 val [major,minor] = goal FOL.thy
     "[| P&Q;  [| P; Q |] ==> R |] ==> R";
@@ -104,9 +104,8 @@
 
 
 \subsection{Definitions and derived rules} \label{definitions}
-\index{rules!derived}
-\index{Isabelle!definitions in}
-\index{definitions!reasoning about|bold}
+\index{rules!derived}\index{definitions!and derived rules|(}
+
 Definitions are expressed as meta-level equalities.  Let us define negation
 and the if-and-only-if connective:
 \begin{eqnarray*}
@@ -114,8 +113,7 @@
   \Var{P}\bimp \Var{Q}  & \equiv & 
                 (\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P})
 \end{eqnarray*}
-\index{rewriting!meta-level|bold}
-\index{unfolding|bold}\index{folding|bold}
+\index{meta-rewriting}
 Isabelle permits {\bf meta-level rewriting} using definitions such as
 these.  {\bf Unfolding} replaces every instance
 of $\neg \Var{P}$ by the corresponding instance of $\Var{P}\imp\bot$.  For
@@ -147,7 +145,7 @@
 
 
 \subsection{Deriving the $\neg$ introduction rule}
-To derive $(\neg I)$, we may call \ttindex{goal} with the appropriate
+To derive $(\neg I)$, we may call {\tt goal} with the appropriate
 formula.  Again, {\tt goal} returns a list consisting of the rule's
 premises.  We bind this one-element list to the \ML\ identifier {\tt
   prems}.
@@ -158,7 +156,7 @@
 {\out  1. ~P}
 {\out val prems = ["P ==> False  [P ==> False]"] : thm list}
 \end{ttbox}
-Calling \ttindex{rewrite_goals_tac} with \ttindex{not_def}, which is the
+Calling \ttindex{rewrite_goals_tac} with \tdx{not_def}, which is the
 definition of negation, unfolds that definition in the subgoals.  It leaves
 the main goal alone.
 \begin{ttbox}
@@ -169,7 +167,7 @@
 {\out ~P}
 {\out  1. P --> False}
 \end{ttbox}
-Using \ttindex{impI} and the premise, we reduce subgoal~1 to a triviality:
+Using \tdx{impI} and the premise, we reduce subgoal~1 to a triviality:
 \begin{ttbox}
 by (resolve_tac [impI] 1);
 {\out Level 2}
@@ -191,10 +189,10 @@
 val notI = result();
 {\out val notI = "(?P ==> False) ==> ~?P" : thm}
 \end{ttbox}
-\indexbold{*notI}
+\indexbold{*notI theorem}
 
 There is a simpler way of conducting this proof.  The \ttindex{goalw}
-command starts a backward proof, as does \ttindex{goal}, but it also
+command starts a backward proof, as does {\tt goal}, but it also
 unfolds definitions.  Thus there is no need to call
 \ttindex{rewrite_goals_tac}:
 \begin{ttbox}
@@ -211,8 +209,8 @@
 Let us derive the rule $(\neg E)$.  The proof follows that of~{\tt conjE}
 above, with an additional step to unfold negation in the major premise.
 Although the {\tt goalw} command is best for this, let us
-try~\ttindex{goal} to see another way of unfolding definitions.  After
-binding the premises to \ML\ identifiers, we apply \ttindex{FalseE}:
+try~{\tt goal} to see another way of unfolding definitions.  After
+binding the premises to \ML\ identifiers, we apply \tdx{FalseE}:
 \begin{ttbox}
 val [major,minor] = goal FOL.thy "[| ~P;  P |] ==> R";
 {\out Level 0}
@@ -257,7 +255,7 @@
 val notE = result();
 {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
 \end{ttbox}
-\indexbold{*notE}
+\indexbold{*notE theorem}
 
 \medskip
 Again, there is a simpler way of conducting this proof.  Recall that
@@ -282,8 +280,9 @@
 {\out R}
 {\out No subgoals!}
 \end{ttbox}
+\index{definitions!and derived rules|)}
 
-\goodbreak\medskip
+\goodbreak\medskip\index{*"!"! symbol!in main goal}
 Finally, here is a trick that is sometimes useful.  If the goal
 has an outermost meta-quantifier, then \ttindex{goal} and \ttindex{goalw}
 do not return the rule's premises in the list of theorems;  instead, the
@@ -297,8 +296,8 @@
 val it = [] : thm list
 \end{ttbox}
 The proof continues as before.  But instead of referring to \ML\
-identifiers, we refer to assumptions using \ttindex{eresolve_tac} or
-\ttindex{assume_tac}: 
+identifiers, we refer to assumptions using {\tt eresolve_tac} or
+{\tt assume_tac}: 
 \begin{ttbox}
 by (resolve_tac [FalseE] 1);
 {\out Level 1}
@@ -329,6 +328,7 @@
 
 \section{Defining theories}\label{sec:defining-theories}
 \index{theories!defining|(}
+
 Isabelle makes no distinction between simple extensions of a logic --- like
 defining a type~$bool$ with constants~$true$ and~$false$ --- and defining
 an entire logic.  A theory definition has the form
@@ -350,7 +350,8 @@
 default sort for type variables.  A constant declaration can specify an
 associated concrete syntax.  The translations section specifies rewrite
 rules on abstract syntax trees, for defining notations and abbreviations.
-The {\ML} section contains code to perform arbitrary syntactic
+\index{*ML section}
+The {\tt ML} section contains code to perform arbitrary syntactic
 transformations.  The main declaration forms are discussed below.
 The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
   appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.
@@ -358,7 +359,7 @@
 All the declaration parts can be omitted.  In the simplest case, $T$ is
 just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one
 or more other theories, inheriting their types, constants, syntax, etc.
-The theory \ttindexbold{Pure} contains nothing but Isabelle's meta-logic.
+The theory \thydx{Pure} contains nothing but Isabelle's meta-logic.
 
 Each theory definition must reside in a separate file, whose name is
 determined as follows: the theory name, say {\tt ListFn}, is converted to
@@ -388,7 +389,8 @@
 
 
 \subsection{Declaring constants and rules}
-\indexbold{constants!declaring}\indexbold{rules!declaring}
+\indexbold{constants!declaring}\index{rules!declaring}
+
 Most theories simply declare constants and rules.  The {\bf constant
 declaration part} has the form
 \begin{ttbox}
@@ -414,6 +416,7 @@
 $rule@n$ are expressions of type~$prop$.  Each rule {\em must\/} be
 enclosed in quotation marks.
 
+\indexbold{definitions}
 {\bf Definitions} are rules of the form $t\equiv u$.  Normally definitions
 should be conservative, serving only as abbreviations.  As of this writing,
 Isabelle does not provide a separate declaration part for definitions; it
@@ -544,9 +547,11 @@
        negate :: "signal => signal"
 \end{ttbox}
 
-\subsection{Infixes and Mixfixes}
-\indexbold{infix operators}\index{examples!of theories}
-The constant declaration part of the theory
+\subsection{Infix and Mixfix operators}
+\index{infixes}\index{examples!of theories}
+
+Infix or mixfix syntax may be attached to constants.  Consider the
+following theory:
 \begin{ttbox}
 Gate2 = FOL +
 consts  "~&"     :: "[o,o] => o"         (infixl 35)
@@ -555,55 +560,63 @@
         xor_def  "P # Q  == P & ~Q | ~P & Q"
 end
 \end{ttbox}
-declares two left-associating infix operators: $\nand$ of precedence~35 and
-$\xor$ of precedence~30.  Hence $P \xor Q \xor R$ is parsed as $(P\xor
-Q) \xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$.  Note the
-quotation marks in \verb|"~&"| and \verb|"#"|.
+The constant declaration part declares two left-associating infix operators
+with their priorities, or precedences; they are $\nand$ of priority~35 and
+$\xor$ of priority~30.  Hence $P \xor Q \xor R$ is parsed as $(P\xor Q)
+\xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$.  Note the quotation
+marks in \verb|"~&"| and \verb|"#"|.
 
 The constants \hbox{\verb|op ~&|} and \hbox{\verb|op #|} are declared
 automatically, just as in \ML.  Hence you may write propositions like
 \verb|op #(True) == op ~&(True)|, which asserts that the functions $\lambda
 Q.True \xor Q$ and $\lambda Q.True \nand Q$ are identical.
 
-\indexbold{mixfix operators}
-{\bf Mixfix} operators may have arbitrary context-free syntaxes.  For example
+\bigskip\index{mixfix declarations}
+{\bf Mixfix} operators may have arbitrary context-free syntaxes.  Let us
+add a line to the constant declaration part:
 \begin{ttbox}
         If :: "[o,o,o] => o"       ("if _ then _ else _")
 \end{ttbox}
-declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
+This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
   if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}.  Underscores
-denote argument positions.  Pretty-printing information can be specified in
-order to improve the layout of formulae with mixfix operations.  For
-details, see {\em Isabelle's Object-Logics}.
+denote argument positions.  
 
-Mixfix declarations can be annotated with precedences, just like
+The declaration above does not allow the {\tt if}-{\tt then}-{\tt else}
+construct to be split across several lines, even if it is too long to fit
+on one line.  Pretty-printing information can be added to specify the
+layout of mixfix operators.  For details, see
+\iflabelundefined{Defining-Logics}%
+    {the {\it Reference Manual}, chapter `Defining Logics'}%
+    {Chap.\ts\ref{Defining-Logics}}.
+
+Mixfix declarations can be annotated with priorities, just like
 infixes.  The example above is just a shorthand for
 \begin{ttbox}
         If :: "[o,o,o] => o"       ("if _ then _ else _" [0,0,0] 1000)
 \end{ttbox}
-The numeric components determine precedences.  The list of integers
-defines, for each argument position, the minimal precedence an expression
-at that position must have.  The final integer is the precedence of the
+The numeric components determine priorities.  The list of integers
+defines, for each argument position, the minimal priority an expression
+at that position must have.  The final integer is the priority of the
 construct itself.  In the example above, any argument expression is
-acceptable because precedences are non-negative, and conditionals may
-appear everywhere because 1000 is the highest precedence.  On the other
-hand,
+acceptable because priorities are non-negative, and conditionals may
+appear everywhere because 1000 is the highest priority.  On the other
+hand, the declaration
 \begin{ttbox}
         If :: "[o,o,o] => o"       ("if _ then _ else _" [100,0,0] 99)
 \end{ttbox}
 defines concrete syntax for a conditional whose first argument cannot have
-the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a precedence
-of at least~100.  Since expressions put in parentheses have maximal
-precedence, we may of course write
+the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a priority
+of at least~100.  We may of course write
 \begin{quote}\tt
 if (if $P$ then $Q$ else $R$) then $S$ else $T$
 \end{quote}
+because expressions in parentheses have maximal priority.  
 
 Binary type constructors, like products and sums, may also be declared as
 infixes.  The type declaration below introduces a type constructor~$*$ with
 infix notation $\alpha*\beta$, together with the mixfix notation
 ${<}\_,\_{>}$ for pairs.  
-\index{examples!of theories}
+\index{examples!of theories}\index{mixfix declarations}
 \begin{ttbox}
 Prod = FOL +
 types   ('a,'b) "*"                           (infixl 20)
@@ -643,7 +656,7 @@
 types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::}
 \alpha$, for $\alpha{::}arith$.  We introduce $arith$ as a subclass of
 $term$ and add the three polymorphic constants of this class.
-\index{examples!of theories}
+\index{examples!of theories}\index{constants!overloaded}
 \begin{ttbox}
 Arith = FOL +
 classes arith < term
@@ -696,7 +709,7 @@
 Section\ts\ref{sec:logical-syntax} has formalized a first-order logic,
 including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.
 Let us introduce the Peano axioms for mathematical induction and the
-freeness of $0$ and~$Suc$:
+freeness of $0$ and~$Suc$:\index{axioms!Peano}
 \[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}
  \qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$}
 \]
@@ -748,12 +761,12 @@
 
 \subsection{Declaring the theory to Isabelle}
 \index{examples!of theories}
-Let us create the theory \ttindexbold{Nat} starting from theory~\verb$FOL$,
+Let us create the theory \thydx{Nat} starting from theory~\verb$FOL$,
 which contains only classical logic with no natural numbers.  We declare
 the 0-place type constructor $nat$ and the associated constants.  Note that
 the constant~0 requires a mixfix annotation because~0 is not a legal
 identifier, and could not otherwise be written in terms:
-\begin{ttbox}
+\begin{ttbox}\index{mixfix declarations}
 Nat = FOL +
 types   nat
 arities nat         :: term
@@ -811,8 +824,9 @@
 
 
 \section{Refinement with explicit instantiation}
-\index{refinement!with instantiation|bold}
-\index{instantiation!explicit|bold}
+\index{resolution!with instantiation}
+\index{instantiation|(}
+
 In order to employ mathematical induction, we need to refine a subgoal by
 the rule~$(induct)$.  The conclusion of this rule is $\Var{P}(\Var{n})$,
 which is highly ambiguous in higher-order unification.  It matches every
@@ -825,12 +839,12 @@
 a rule.  But it also accepts explicit instantiations for the rule's
 schematic variables.  
 \begin{description}
-\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
+\item[\ttindex{res_inst_tac} {\it insts} {\it thm} {\it i}]
 instantiates the rule {\it thm} with the instantiations {\it insts}, and
 then performs resolution on subgoal~$i$.
 
-\item[\ttindexbold{eres_inst_tac}] 
-and \ttindexbold{dres_inst_tac} are similar, but perform elim-resolution
+\item[\ttindex{eres_inst_tac}] 
+and \ttindex{dres_inst_tac} are similar, but perform elim-resolution
 and destruct-resolution, respectively.
 \end{description}
 The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$,
@@ -844,7 +858,7 @@
 whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$.
 
 \subsection{A simple proof by induction}
-\index{proof!by induction}\index{examples!of induction}
+\index{examples!of induction}
 Let us prove that no natural number~$k$ equals its own successor.  To
 use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good
 instantiation for~$\Var{P}$.
@@ -863,8 +877,8 @@
 We should check that Isabelle has correctly applied induction.  Subgoal~1
 is the base case, with $k$ replaced by~0.  Subgoal~2 is the inductive step,
 with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$.
-The rest of the proof demonstrates~\ttindex{notI}, \ttindex{notE} and the
-other rules of~\ttindex{Nat.thy}.  The base case holds by~\ttindex{Suc_neq_0}:
+The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the
+other rules of theory {\tt Nat}.  The base case holds by~\ttindex{Suc_neq_0}:
 \begin{ttbox}
 by (resolve_tac [notI] 1);
 {\out Level 2}
@@ -949,23 +963,26 @@
 \end{ttbox}
 Inspecting subgoal~1 reveals that induction has been applied to just the
 second occurrence of~$n$.  This perfectly legitimate induction is useless
-here.  The main goal admits fourteen different applications of induction.
-The number is exponential in the size of the formula.
+here.  
+
+The main goal admits fourteen different applications of induction.  The
+number is exponential in the size of the formula.
 
 \subsection{Proving that addition is associative}
-Let us invoke the induction rule properly properly,
-using~\ttindex{res_inst_tac}.  At the same time, we shall have a glimpse at
-Isabelle's rewriting tactics, which are described in the {\em Reference
-  Manual}.
+Let us invoke the induction rule properly properly, using~{\tt
+  res_inst_tac}.  At the same time, we shall have a glimpse at Isabelle's
+simplification tactics, which are described in 
+\iflabelundefined{simp-chap}%
+    {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}.
 
-\index{rewriting!object-level}\index{examples!of rewriting} 
+\index{simplification}\index{examples!of simplification} 
 
-Isabelle's rewriting tactics repeatedly applies equations to a subgoal,
-simplifying or proving it.  For efficiency, the rewriting rules must be
-packaged into a \bfindex{simplification set}, or {\bf simpset}.  We take
-the standard simpset for first-order logic and insert the equations
-for~{\tt add} proved in the previous section, namely $0+n=n$ and ${\tt
-  Suc}(m)+n={\tt Suc}(m+n)$:
+Isabelle's simplification tactics repeatedly apply equations to a subgoal,
+perhaps proving it.  For efficiency, the rewrite rules must be
+packaged into a {\bf simplification set},\index{simplification sets} 
+or {\bf simpset}.  We take the standard simpset for first-order logic and
+insert the equations for~{\tt add} proved in the previous section, namely
+$0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
 \begin{ttbox}
 val add_ss = FOL_ss addrews [add_0, add_Suc];
 \end{ttbox}
@@ -1004,6 +1021,7 @@
 {\out k + m + n = k + (m + n)}
 {\out No subgoals!}
 \end{ttbox}
+\index{instantiation|)}
 
 
 \section{A Prolog interpreter}
@@ -1037,9 +1055,9 @@
 \]
 
 \index{examples!of theories}
-Theory \ttindex{Prolog} extends first-order logic in order to make use
+Theory \thydx{Prolog} extends first-order logic in order to make use
 of the class~$term$ and the type~$o$.  The interpreter does not use the
-rules of~\ttindex{FOL}.
+rules of~{\tt FOL}.
 \begin{ttbox}
 Prolog = FOL +
 types   'a list
@@ -1103,7 +1121,7 @@
 \end{ttbox}
 
 
-\subsection{Backtracking}\index{backtracking}
+\subsection{Backtracking}\index{backtracking!Prolog style}
 Prolog backtracking can answer questions that have multiple solutions.
 Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$?  This
 question has five solutions.  Using \ttindex{REPEAT} to apply the rules, we
@@ -1196,11 +1214,12 @@
 {\out rev(c : b : a : Nil, a : b : c : Nil)}
 {\out No subgoals!}
 \end{ttbox}
-\ttindex{REPEAT} stops when it cannot continue, regardless of which state
-is reached.  The tactical \ttindex{DEPTH_FIRST} searches for a satisfactory
-state, as specified by an \ML{} predicate.  Below,
+\ttindex{REPEAT} goes wrong because it is only a repetition tactical, not a
+search tactical.  {\tt REPEAT} stops when it cannot continue, regardless of
+which state is reached.  The tactical \ttindex{DEPTH_FIRST} searches for a
+satisfactory state, as specified by an \ML{} predicate.  Below,
 \ttindex{has_fewer_prems} specifies that the proof state should have no
-subgoals.  
+subgoals.
 \begin{ttbox}
 val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) 
                              (resolve_tac rules 1);




