tuned;
authorwenzelm
Sun Oct 31 15:20:35 1999 +0100 (1999-10-31)
changeset 7987d9aef93c0e32
parent 7986 9d319a76dbeb
child 7988 feea893b47c7
tuned;
doc-src/IsarRef/generic.tex
doc-src/IsarRef/hol.tex
doc-src/IsarRef/intro.tex
doc-src/IsarRef/pure.tex
doc-src/IsarRef/refcard.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Sat Oct 30 20:41:30 1999 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sun Oct 31 15:20:35 1999 +0100
     1.3 @@ -37,9 +37,9 @@
     1.4    becomes a (generalized) \emph{elimination}.
     1.5    
     1.6    Note that the classical reasoner introduces another version of $rule$ that
     1.7 -  is able to pick appropriate rules automatically, whenever explicit $thms$
     1.8 -  are omitted (see \S\ref{sec:classical-basic}); that method is the default
     1.9 -  for $\PROOFNAME$ steps.  Note that ``$\DDOT$'' (double-dot) abbreviates
    1.10 +  is able to pick appropriate rules automatically, whenever $thms$ are omitted
    1.11 +  (see \S\ref{sec:classical-basic}); that method is the default for
    1.12 +  $\PROOFNAME$ steps.  Note that ``$\DDOT$'' (double-dot) abbreviates
    1.13    $\BY{default}$.
    1.14  \item [$erule~thms$] is similar to $rule$, but applies rules by
    1.15    elim-resolution.  This is an improper method, mainly for experimentation and
    1.16 @@ -47,11 +47,11 @@
    1.17    $rule$ (single step, involving facts) or $elim$ (repeated steps, see
    1.18    \S\ref{sec:classical-basic}).
    1.19  \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
    1.20 -  meta-level definitions throughout all goals; any facts provided are
    1.21 -  \emph{ignored}.
    1.22 -\item [$succeed$] yields a single (unchanged) result; it is the identify of
    1.23 +  meta-level definitions throughout all goals; any facts provided are inserted
    1.24 +  into the goal and subject to rewriting as well.
    1.25 +\item [$succeed$] yields a single (unchanged) result; it is the identity of
    1.26    the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
    1.27 -\item [$fail$] yields an empty result sequence; it is the identify of the
    1.28 +\item [$fail$] yields an empty result sequence; it is the identity of the
    1.29    ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
    1.30  \end{descr}
    1.31  
    1.32 @@ -98,12 +98,12 @@
    1.33    result).
    1.34  \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
    1.35    $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
    1.36 -  the reversed order).  Note that premises may be skipped by including $\_$
    1.37 -  (underscore) as argument.
    1.38 +  the reversed order).  Note that premises may be skipped by including
    1.39 +  ``$\_$'' (underscore) as argument.
    1.40    
    1.41    $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$
    1.42 -  that does not include the automatic lifting process that is normally
    1.43 -  intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).
    1.44 +  that skips the automatic lifting process that is normally intended (cf.\ 
    1.45 +  \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).
    1.46    
    1.47  \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
    1.48    instantiation, respectively.  The terms given in $of$ are substituted for
    1.49 @@ -180,9 +180,10 @@
    1.50  \item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
    1.51    $\ALSO$, and concludes the current calculational thread.  The final result
    1.52    is exhibited as fact for forward chaining towards the next goal. Basically,
    1.53 -  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Typical proof
    1.54 -  idioms are``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
    1.55 -  ``$\FINALLY~\HAVE{}{\phi}~\DOT$''.
    1.56 +  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Note that
    1.57 +  ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
    1.58 +  ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
    1.59 +  calculational proofs.
    1.60    
    1.61  \item [$trans$] maintains the set of transitivity rules of the theory or proof
    1.62    context, by adding or deleting theorems (the default is to add).
    1.63 @@ -204,12 +205,12 @@
    1.64    intro_classes & : & \isarmeth \\
    1.65  \end{matharray}
    1.66  
    1.67 -Axiomatic type classes are provided by Isabelle/Pure as a purely
    1.68 -\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}).  Thus
    1.69 -any object logic may make use of this light-weight mechanism for abstract
    1.70 -theories.  See \cite{Wenzel:1997:TPHOL} for more information.  There is also a
    1.71 -tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
    1.72 -the standard Isabelle documentation.
    1.73 +Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
    1.74 +interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic
    1.75 +may make use of this light-weight mechanism of abstract theories.  See
    1.76 +\cite{Wenzel:1997:TPHOL} for more information.  There is also a tutorial on
    1.77 +\emph{Using Axiomatic Type Classes in Isabelle} that is part of the standard
    1.78 +Isabelle documentation.
    1.79  %FIXME cite
    1.80  
    1.81  \begin{rail}
    1.82 @@ -225,21 +226,22 @@
    1.83    holding.  Class axioms may not contain more than one type variable.  The
    1.84    class axioms (with implicit sort constraints added) are bound to the given
    1.85    names.  Furthermore a class introduction rule is generated, which is
    1.86 -  employed by method $intro_classes$ in support instantiation proofs of this
    1.87 +  employed by method $intro_classes$ to support instantiation proofs of this
    1.88    class.
    1.89    
    1.90  \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
    1.91    (\vec s)c$] setup up a goal stating the class relation or type arity.  The
    1.92 -  proof would usually proceed by the $intro_classes$ method, and then
    1.93 -  establish the characteristic theorems of the type classes involved.  After
    1.94 -  finishing the proof the theory will be augmented by a type signature
    1.95 -  declaration corresponding to the resulting theorem.
    1.96 -\item [$intro_classes$] repeatedly expands the class introduction rules of
    1.97 +  proof would usually proceed by $intro_classes$, and then establish the
    1.98 +  characteristic theorems of the type classes involved.  After finishing the
    1.99 +  proof, the theory will be augmented by a type signature declaration
   1.100 +  corresponding to the resulting theorem.
   1.101 +\item [$intro_classes$] repeatedly expands all class introduction rules of
   1.102    this theory.
   1.103  \end{descr}
   1.104  
   1.105 -See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
   1.106 -axiomatic type classes, including instantiation proofs.
   1.107 +%FIXME
   1.108 +%See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
   1.109 +%axiomatic type classes, including instantiation proofs.
   1.110  
   1.111  
   1.112  \section{The Simplifier}
   1.113 @@ -345,7 +347,7 @@
   1.114    given ones may be applied.  The latter form admits better control of what
   1.115    actually happens, thus it is very appropriate as an initial method for
   1.116    $\PROOFNAME$ that splits up certain connectives of the goal, before entering
   1.117 -  the actual proof.
   1.118 +  the actual sub-proof.
   1.119    
   1.120  \item [$contradiction$] solves some goal by contradiction, deriving any result
   1.121    from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
   1.122 @@ -388,7 +390,10 @@
   1.123  
   1.124  Any of above methods support additional modifiers of the context of classical
   1.125  rules.  There semantics is analogous to the attributes given in
   1.126 -\S\ref{sec:classical-mod}.
   1.127 +\S\ref{sec:classical-mod}.  Facts provided by forward chaining are inserted
   1.128 +into the goal before doing the search.  The ``!''~argument causes the full
   1.129 +context of assumptions to be included as well.\footnote{This is slightly less
   1.130 +  hazardous than for the Simplifier (see \S\ref{sec:simp}).}
   1.131  
   1.132  
   1.133  \subsection{Combined automated methods}
   1.134 @@ -403,7 +408,7 @@
   1.135    ('force' | 'auto') ('!' ?) (clasimpmod * )
   1.136    ;
   1.137  
   1.138 -  clasimpmod: ('simp' ('add' | 'del' | 'only') | other |
   1.139 +  clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' |
   1.140      (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
   1.141  \end{rail}
   1.142  
   1.143 @@ -414,8 +419,13 @@
   1.144    modifier arguments correspond to those given in \S\ref{sec:simp} and
   1.145    \S\ref{sec:classical-auto}.  Just note that the ones related to the
   1.146    Simplifier are prefixed by \railtoken{simp} here.
   1.147 +  
   1.148 +  Facts provided by forward chaining are inserted into the goal before doing
   1.149 +  the search.  The ``!''~argument causes the full context of assumptions to be
   1.150 +  included as well.
   1.151  \end{descr}
   1.152  
   1.153 +
   1.154  \subsection{Modifying the context}\label{sec:classical-mod}
   1.155  
   1.156  \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
     2.1 --- a/doc-src/IsarRef/hol.tex	Sat Oct 30 20:41:30 1999 +0200
     2.2 +++ b/doc-src/IsarRef/hol.tex	Sun Oct 31 15:20:35 1999 +0100
     2.3 @@ -146,8 +146,8 @@
     2.4  \end{descr}
     2.5  
     2.6  See \cite{isabelle-HOL} for more information.  Note that
     2.7 -$\isarkeyword{inductive_cases}$ corresponds to the ML function
     2.8 -\texttt{mk_cases}.
     2.9 +$\isarkeyword{inductive_cases}$ corresponds to the \texttt{mk_cases} ML
    2.10 +function.
    2.11  
    2.12  
    2.13  \section{Proof by induction}
     3.1 --- a/doc-src/IsarRef/intro.tex	Sat Oct 30 20:41:30 1999 +0200
     3.2 +++ b/doc-src/IsarRef/intro.tex	Sun Oct 31 15:20:35 1999 +0100
     3.3 @@ -149,7 +149,7 @@
     3.4    \end{tabular}
     3.5  \end{center}
     3.6  
     3.7 -See \texttt{HOL/Isar_examples} for a collection of introductory examples.
     3.8 +See \texttt{HOL/Isar_examples} for a collection of introductory examples, and
     3.9  \texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application.  Apart from
    3.10  browsable HTML sources, both sessions provide actual documents (in PDF).
    3.11  
     4.1 --- a/doc-src/IsarRef/pure.tex	Sat Oct 30 20:41:30 1999 +0200
     4.2 +++ b/doc-src/IsarRef/pure.tex	Sun Oct 31 15:20:35 1999 +0100
     4.3 @@ -370,10 +370,9 @@
     4.4    afterwards.  Thus $text$ may actually change the theory as a side effect.
     4.5    
     4.6  \item [$\isarkeyword{setup}~text$] changes the current theory context by
     4.7 -  applying setup functions from $text$, which refers to an ML expression of
     4.8 -  type $(theory \to theory)~list$.  The $\isarkeyword{setup}$ command is the
     4.9 -  canonical way to initialize object-logic specific tools and packages written
    4.10 -  in ML.
    4.11 +  applying $text$, which refers to an ML expression of type $(theory \to
    4.12 +  theory)~list$.  The $\isarkeyword{setup}$ command is the canonical way to
    4.13 +  initialize object-logic specific tools and packages written in ML.
    4.14  \end{descr}
    4.15  
    4.16  
    4.17 @@ -424,7 +423,7 @@
    4.18  
    4.19  \section{Proof commands}
    4.20  
    4.21 -Proof commands provide transitions of Isar/VM machine configurations, which
    4.22 +Proof commands perform transitions of Isar/VM machine configurations, which
    4.23  are block-structured, consisting of a stack of nodes with three main
    4.24  components: logical proof context, current facts, and open goals.  Isar/VM
    4.25  transitions are \emph{typed} according to the following three three different
    4.26 @@ -434,16 +433,18 @@
    4.27    to be \emph{proven}; the next command may refine it by some proof method
    4.28    (read: tactic), and enter a sub-proof to establish the actual result.
    4.29  \item [$proof(state)$] is like an internal theory mode: the context may be
    4.30 -  augmented by \emph{stating} additional assumptions, intermediate result etc.
    4.31 +  augmented by \emph{stating} additional assumptions, intermediate results
    4.32 +  etc.
    4.33  \item [$proof(chain)$] is intermediate between $proof(state)$ and
    4.34 -  $proof(prove)$: existing facts (i.e.\ the contents of $this$) have been just
    4.35 -  picked up in order to be used when refining the goal claimed next.
    4.36 +  $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$''
    4.37 +  register) have been just picked up in order to be used when refining the
    4.38 +  goal claimed next.
    4.39  \end{descr}
    4.40  
    4.41  
    4.42  \subsection{Proof markup commands}\label{sec:markup-prf}
    4.43  
    4.44 -\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}
    4.45 +\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
    4.46  \indexisarcmd{txt}\indexisarcmd{txt-raw}
    4.47  \begin{matharray}{rcl}
    4.48    \isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\
    4.49 @@ -480,10 +481,10 @@
    4.50  former closely correspond to Skolem constants, or meta-level universal
    4.51  quantification as provided by the Isabelle/Pure logical framework.
    4.52  Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
    4.53 -a local object that may be used in the subsequent proof as any other variable
    4.54 +a local value that may be used in the subsequent proof as any other variable
    4.55  or constant.  Furthermore, any result $\edrv \phi[x]$ exported from the
    4.56 -current context will be universally closed wrt.\ $x$ at the outermost level:
    4.57 -$\edrv \All x \phi$; this is expressed using Isabelle's meta-variables.
    4.58 +context will be universally closed wrt.\ $x$ at the outermost level: $\edrv
    4.59 +\All x \phi$ (this is expressed using Isabelle's meta-variables).
    4.60  
    4.61  Similarly, introducing some assumption $\chi$ has two effects.  On the one
    4.62  hand, a local theorem is created that may be used as a fact in subsequent
    4.63 @@ -497,9 +498,9 @@
    4.64  user.
    4.65  
    4.66  Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
    4.67 -combining $\FIX x$ with another kind of assumption that causes any
    4.68 -hypothetical equation $x \equiv t$ to be eliminated by reflexivity.  Thus,
    4.69 -exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
    4.70 +combining $\FIX x$ with another version of assumption that causes any
    4.71 +hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.
    4.72 +Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
    4.73  
    4.74  \begin{rail}
    4.75    'fix' (vars + 'and') comment?
    4.76 @@ -530,7 +531,7 @@
    4.77    these concatenated.
    4.78  \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
    4.79    In results exported from the context, $x$ is replaced by $t$.  Basically,
    4.80 -  $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$, with the
    4.81 +  $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the
    4.82    resulting hypothetical equation solved by reflexivity.
    4.83    
    4.84    The default name for the definitional equation is $x_def$.
    4.85 @@ -554,7 +555,7 @@
    4.86  Any fact will usually be involved in further proofs, either as explicit
    4.87  arguments of proof methods or when forward chaining towards the next goal via
    4.88  $\THEN$ (and variants).  Note that the special theorem name
    4.89 -$this$.\indexisarthm{this} refers to the most recently established facts.
    4.90 +$this$\indexisarthm{this} refers to the most recently established facts.
    4.91  \begin{rail}
    4.92    'note' thmdef? thmrefs comment?
    4.93    ;
    4.94 @@ -596,8 +597,8 @@
    4.95  \begin{matharray}{rcl}
    4.96    \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
    4.97    \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
    4.98 -  \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\
    4.99 -  \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\
   4.100 +  \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
   4.101 +  \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
   4.102    \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
   4.103    \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
   4.104  \end{matharray}
   4.105 @@ -605,7 +606,7 @@
   4.106  Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
   4.107  and $\LEMMANAME$.  New local goals may be claimed within proof mode as well.
   4.108  Four variants are available, indicating whether the result is meant to solve
   4.109 -some pending goal and whether forward chaining is employed.
   4.110 +some pending goal or whether forward chaining is employed.
   4.111  
   4.112  \begin{rail}
   4.113    ('theorem' | 'lemma') goal
   4.114 @@ -620,7 +621,7 @@
   4.115  \begin{descr}
   4.116  \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,
   4.117    eventually resulting in some theorem $\turn \phi$ put back into the theory.
   4.118 -\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
   4.119 +\item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as
   4.120    ``lemma''.
   4.121  \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a
   4.122    theorem with the current assumption context as hypotheses.
   4.123 @@ -655,8 +656,8 @@
   4.124    goal to a number of sub-goals that are to be solved later.  Facts are passed
   4.125    to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.
   4.126    
   4.127 -\item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining goals
   4.128 -  completely.  No facts are passed to $m@2$.
   4.129 +\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve
   4.130 +  remaining goals.  No facts are passed to $m@2$.
   4.131  \end{enumerate}
   4.132  
   4.133  The only other proper way to affect pending goals is by $\SHOWNAME$ (or
   4.134 @@ -668,17 +669,19 @@
   4.135  or constitute some well-understood reduction to new sub-goals.  Arbitrary
   4.136  automatic proof tools that are prone leave a large number of badly structured
   4.137  sub-goals are no help in continuing the proof document in any intelligible
   4.138 -way.  A much better technique would be to $\SHOWNAME$ some non-trivial
   4.139 -reduction as an explicit rule, which is solved completely by some automated
   4.140 -method, and then applied to some pending goal.
   4.141 +way.
   4.142 +%FIXME
   4.143 +%A more appropriate technique would be to $\SHOWNAME$ some non-trivial
   4.144 +%reduction as an explicit rule, which is solved completely by some automated
   4.145 +%method, and then applied to some pending goal.
   4.146  
   4.147  \medskip
   4.148  
   4.149  Unless given explicitly by the user, the default initial method is
   4.150  ``$default$'', which is usually set up to apply a single standard elimination
   4.151  or introduction rule according to the topmost symbol involved.  There is no
   4.152 -separate default terminal method; in any case the final step is to solve all
   4.153 -remaining goals by assumption, though.
   4.154 +separate default terminal method.  In any case, any goals left after that are
   4.155 +solved by assumption as the very last step.
   4.156  
   4.157  \begin{rail}
   4.158    'proof' interest? meth? comment?
   4.159 @@ -708,8 +711,8 @@
   4.160    $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
   4.161    some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
   4.162  \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
   4.163 -  abbreviates $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both
   4.164 -  methods.  Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
   4.165 +  abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods,
   4.166 +  though.  Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
   4.167    by expanding its definition; in many cases $\PROOF{m@1}$ is already
   4.168    sufficient to see what is going wrong.
   4.169  \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
   4.170 @@ -717,12 +720,12 @@
   4.171  \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
   4.172    abbreviates $\BY{assumption}$.
   4.173  \item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake};
   4.174 -  provided that \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$
   4.175 -  pretends to solve the goal without further ado.  Of course, the result is a
   4.176 -  fake theorem only, involving some oracle in its internal derivation object
   4.177 -  (this is indicated as ``$[!]$'' in the printed result).  The main
   4.178 -  application of $\isarkeyword{sorry}$ is to support experimentation and
   4.179 -  top-down proof development.
   4.180 +  provided that the \texttt{quick_and_dirty} flag is enabled,
   4.181 +  $\isarkeyword{sorry}$ pretends to solve the goal without further ado.  Of
   4.182 +  course, the result is a fake theorem only, involving some oracle in its
   4.183 +  internal derivation object (this is indicated as ``$[!]$'' in the printed
   4.184 +  result).  The main application of $\isarkeyword{sorry}$ is to support
   4.185 +  experimentation and top-down proof development.
   4.186  \end{descr}
   4.187  
   4.188  
   4.189 @@ -772,13 +775,13 @@
   4.190  \end{matharray}
   4.191  
   4.192  Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
   4.193 -or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$
   4.194 -etc.) with a list of patterns $\ISS{p@1 \dots}{p@n}$.  In both cases,
   4.195 -higher-order matching is invoked to bind extra-logical term variables, which
   4.196 -may be either named schematic variables of the form $\Var{x}$, or nameless
   4.197 -dummies ``\texttt{_}'' (underscore).\indexisarvar{_@\texttt{_}} Note that in
   4.198 -the $\LETNAME$ form the patterns occur on the left-hand side, while the
   4.199 -$\ISNAME$ patterns are in postfix position.
   4.200 +or by annotating assumptions or goal statements with a list of patterns
   4.201 +$\ISS{p@1\;\dots}{p@n}$.  In both cases, higher-order matching is invoked to
   4.202 +bind extra-logical term variables, which may be either named schematic
   4.203 +variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}''
   4.204 +(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the
   4.205 +patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
   4.206 +postfix position.
   4.207  
   4.208  Term abbreviations are quite different from actual local definitions as
   4.209  introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}).  The latter are
   4.210 @@ -807,7 +810,7 @@
   4.211  (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
   4.212  (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its
   4.213  object-logical statement.  The latter two abstract over any meta-level
   4.214 -parameters bound by $\Forall$.
   4.215 +parameters.
   4.216  
   4.217  Fact statements resulting from assumptions or finished goals are bound as
   4.218  $\Var{this_prop}$\indexisarvar{this-prop},
   4.219 @@ -816,7 +819,7 @@
   4.220  $\Var{this}$ refers to an object-logic statement that is an application
   4.221  $f(t)$, then $t$ is bound to the special text variable
   4.222  ``$\dots$''\indexisarvar{\dots} (three dots).  The canonical application of
   4.223 -this feature are calculational proofs (see \S\ref{sec:calculation}).
   4.224 +the latter are calculational proofs (see \S\ref{sec:calculation}).
   4.225  
   4.226  
   4.227  \subsection{Block structure}
   4.228 @@ -834,8 +837,8 @@
   4.229  again when concluding the sub-proof (by $\QEDNAME$ etc.).  Sections of
   4.230  different context within a sub-proof may be switched via $\isarkeyword{next}$,
   4.231  which is just a single block-close followed by block-open again.  Thus the
   4.232 -effect of $\isarkeyword{next}$ is a local reset the proof
   4.233 -context.\footnote{There is no goal focus involved here!}
   4.234 +effect of $\isarkeyword{next}$ to reset the local proof context. There is no
   4.235 +goal focus involved here!
   4.236  
   4.237  For slightly more advanced applications, there are explicit block parentheses
   4.238  as well.  These typically achieve a stronger forward style of reasoning.
   4.239 @@ -887,8 +890,8 @@
   4.240    specifications are applied to a temporary context derived from the current
   4.241    theory or proof; the result is discarded, i.e.\ attributes involved in
   4.242    $thms$ do not have any permanent effect.
   4.243 -\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-checks
   4.244 -  and print terms or propositions according to the current theory or proof
   4.245 +\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-check and
   4.246 +  print terms or propositions according to the current theory or proof
   4.247    context; the inferred type of $t$ is output as well.  Note that these
   4.248    commands are also useful in inspecting the current environment of term
   4.249    abbreviations.
   4.250 @@ -915,17 +918,16 @@
   4.251    process.
   4.252  \item [$\isarkeyword{pwd}~$] prints the current working directory.
   4.253  \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
   4.254 -  $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some
   4.255 +  $\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some
   4.256    theory given as $name$ argument.  These commands are basically the same as
   4.257 -  the corresponding ML functions\footnote{For historic reasons, the original
   4.258 -    ML versions also change the theory context to that of the theory loaded.}
   4.259 -  (see also \cite[\S1,\S6]{isabelle-ref}).  Note that both the ML and Isar
   4.260 -  versions may load new- and old-style theories alike.
   4.261 +  the corresponding ML functions\footnote{The ML versions also change the
   4.262 +    implicit theory context to that of the theory loaded.}  (see also
   4.263 +  \cite[\S1,\S6]{isabelle-ref}).  Note that both the ML and Isar versions may
   4.264 +  load new- and old-style theories alike.
   4.265  \end{descr}
   4.266  
   4.267 -Note that these system commands are scarcely used when working with the
   4.268 -Proof~General interface, since loading of theories is done fully
   4.269 -transparently.
   4.270 +These system commands are scarcely used when working with the Proof~General
   4.271 +interface, since loading of theories is done fully transparently.
   4.272  
   4.273  %%% Local Variables: 
   4.274  %%% mode: latex
     5.1 --- a/doc-src/IsarRef/refcard.tex	Sat Oct 30 20:41:30 1999 +0200
     5.2 +++ b/doc-src/IsarRef/refcard.tex	Sun Oct 31 15:20:35 1999 +0100
     5.3 @@ -14,13 +14,13 @@
     5.4    $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\
     5.5    $\BG~\dots~\EN$ & declare explicit blocks \\
     5.6    $\isarcmd{next}$ & switch implicit blocks \\
     5.7 -  $\NOTE{a}{a@1~\dots~a@n}$ & reconsider facts \\
     5.8 -  $\LET{p = t}$ & \text{abbreviate terms by matching} \\
     5.9 +  $\NOTE{a}{a@1\;\dots\;a@n}$ & reconsider facts \\
    5.10 +  $\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\
    5.11  \end{tabular}
    5.12  
    5.13  \begin{matharray}{rcl}
    5.14 -  theory{\dsh}stmt & = & \THEOREM{name}{form} ~proof \\
    5.15 -  & \Or & \LEMMA{name}{form}~proof \\
    5.16 +  theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\
    5.17 +  & \Or & \LEMMA{name}{prop}~proof \\
    5.18    & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex]
    5.19    proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex]
    5.20    stmt & = & \BG~stmt^*~\EN \\
    5.21 @@ -28,11 +28,11 @@
    5.22    & \Or & \NOTE{name}{name^+} \\
    5.23    & \Or & \LET{term = term} \\[0.5ex]
    5.24    & \Or & \FIX{var^+} \\
    5.25 -  & \Or & \ASSUME{name}{form^+}\\
    5.26 +  & \Or & \ASSUME{name}{prop^+}\\
    5.27    & \Or & \THEN~goal{\dsh}stmt \\
    5.28    & \Or & goal{\dsh}stmt \\
    5.29 -  goal{\dsh}stmt & = & \HAVE{name}{form}~proof \\
    5.30 -  & \Or & \SHOW{name}{form}~proof \\
    5.31 +  goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\
    5.32 +  & \Or & \SHOW{name}{prop}~proof \\
    5.33  \end{matharray}
    5.34  
    5.35  
    5.36 @@ -44,8 +44,8 @@
    5.37    \DOT & \equiv & \BY{assumption} \\
    5.38    \HENCENAME & \equiv & \THEN~\HAVENAME \\
    5.39    \THUSNAME & \equiv & \THEN~\SHOWNAME \\
    5.40 -  \FROM{a@1~\dots~a@n} & \equiv & \NOTE{this}{a@1~\dots~a@n}~\THEN \\
    5.41 -  \WITH{a@1~\dots~a@n} & \equiv & \FROM{a@1~\dots~a@n~this} \\[1ex]
    5.42 +  \FROM{a@1\;\dots\;a@n} & \equiv & \NOTE{this}{a@1\;\dots\;a@n}~\THEN \\
    5.43 +  \WITH{a@1\;\dots\;a@n} & \equiv & \FROM{a@1\;\dots\;a@n~this} \\[1ex]
    5.44    \FROM{this} & \equiv & \THEN \\
    5.45    \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\
    5.46    \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\
    5.47 @@ -67,7 +67,7 @@
    5.48  \subsection{Diagnostic commands}
    5.49  
    5.50  \begin{matharray}{ll}
    5.51 -  \isarcmd{thm}~a@1~\dots~a@n & \text{print theorems} \\
    5.52 +  \isarcmd{thm}~a@1\;\dots\;a@n & \text{print theorems} \\
    5.53    \isarcmd{term}~t & \text{print term} \\
    5.54    \isarcmd{prop}~\phi & \text{print meta-level proposition} \\
    5.55    \isarcmd{typ}~\tau & \text{print meta-level type} \\
    5.56 @@ -78,22 +78,22 @@
    5.57  
    5.58  \begin{tabular}{ll}
    5.59    \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
    5.60 -  $assumption$ & apply assumption \\
    5.61 -  $rule~a@1~\dots~a@n$ & apply some rule  \\
    5.62 +  $assumption$ & apply some assumption \\
    5.63 +  $rule~a@1\;\dots\;a@n$ & apply some rule  \\
    5.64    $rule$ & apply standard rule (default for $\PROOFNAME$) \\
    5.65    $induct~x$ & apply induction rule \\
    5.66 -  $contradiction$ & apply $\neg{}$ elimination rule \\[2ex]
    5.67 +  $contradiction$ & apply $\neg{}$ elimination rule (any order) \\[2ex]
    5.68  
    5.69    \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
    5.70    $-$ & \text{no rules} \\
    5.71 -  $intro~a@1~\dots~a@n$ & \text{introduction rules} \\
    5.72 -  $elim~a@1~\dots~a@n$ & \text{elimination rules} \\
    5.73 -  $unfold~a@1~\dots~a@n$ & \text{definitions} \\[2ex]
    5.74 +  $intro~a@1\;\dots\;a@n$ & \text{introduction rules} \\
    5.75 +  $elim~a@1\;\dots\;a@n$ & \text{elimination rules} \\
    5.76 +  $unfold~a@1\;\dots\;a@n$ & \text{definitions} \\[2ex]
    5.77  
    5.78    \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
    5.79    $simp$ & Simplifier \\
    5.80 -  $blast$, $fast$ & Classical reasoner \\
    5.81 -  $force$, $auto$ & Simplifier + Classical reasoner \\
    5.82 +  $blast$, $fast$ & Classical Reasoner \\
    5.83 +  $force$, $auto$ & Simplifier + Classical Reasoner \\
    5.84    $arith$ & Arithmetic procedure \\
    5.85  \end{tabular}
    5.86  
    5.87 @@ -102,8 +102,8 @@
    5.88  
    5.89  \begin{tabular}{ll}
    5.90    \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex]
    5.91 -  $OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\
    5.92 -  $of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\
    5.93 +  $OF~a@1\;\dots\;a@n$ & apply rule to facts (skipping ``$_$'') \\
    5.94 +  $of~t@1\;\dots\;t@n$ & apply rule to terms (skipping ``$_$'') \\
    5.95    $RS~b$ & resolve fact with rule \\
    5.96    $standard$ & put into standard result form \\
    5.97    $rulify$ & put into object-rule form \\
    5.98 @@ -111,12 +111,11 @@
    5.99  
   5.100    \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]
   5.101    $simp$ & declare Simplifier rules \\
   5.102 -  $intro$, $elim$, $dest$ & declare Classical reasoner rules (also ``$!$'' or ``$!!$'') \\
   5.103 -  $iff$ & declare Simplifier + Classical reasoner rules \\
   5.104 -  $trans$ & calculational rules (general transitivity) \\
   5.105 +  $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``$!$'' or ``$!!$'') \\
   5.106 +  $iff$ & declare Simplifier + Classical Reasoner rules \\
   5.107 +  $trans$ & declare calculational rules (general transitivity) \\
   5.108  \end{tabular}
   5.109  
   5.110 -
   5.111  %%% Local Variables: 
   5.112  %%% mode: latex
   5.113  %%% TeX-master: "isar-ref"