*** empty log message ***
authorwenzelm
Thu Oct 21 18:04:07 1999 +0200 (1999-10-21)
changeset 78977f18f5ffbb92
parent 7896 36865f14e5ce
child 7898 d7e65a52acf9
*** empty log message ***
doc-src/IsarRef/generic.tex
doc-src/IsarRef/refcard.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Thu Oct 21 17:42:42 1999 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Thu Oct 21 18:04:07 1999 +0200
     1.3 @@ -29,29 +29,30 @@
     1.4    plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
     1.5    $\PROOFNAME$ alone.
     1.6  \item [$assumption$] solves some goal by assumption.  Any facts given are
     1.7 -  guaranteed to participate in the refinement.
     1.8 +  guaranteed to participate in the refinement.  Note that ``$\DOT$'' (dot)
     1.9 +  abbreviates $\BY{assumption}$.
    1.10  \item [$rule~thms$] applies some rule given as argument in backward manner;
    1.11    facts are used to reduce the rule before applying it to the goal.  Thus
    1.12    $rule$ without facts is plain \emph{introduction}, while with facts it
    1.13 -  becomes an \emph{elimination}.
    1.14 +  becomes a (generalized) \emph{elimination}.
    1.15    
    1.16    Note that the classical reasoner introduces another version of $rule$ that
    1.17    is able to pick appropriate rules automatically, whenever explicit $thms$
    1.18    are omitted (see \S\ref{sec:classical-basic}); that method is the default
    1.19 -  one for initial proof steps, such as $\PROOFNAME$ and ``$\DDOT$'' (two
    1.20 -  dots).
    1.21 +  for $\PROOFNAME$ steps.  Note that ``$\DDOT$'' (double-dot) abbreviates
    1.22 +  $\BY{default}$.
    1.23  \item [$erule~thms$] is similar to $rule$, but applies rules by
    1.24    elim-resolution.  This is an improper method, mainly for experimentation and
    1.25    porting of old scripts.  Actual elimination proofs are usually done with
    1.26 -  $rule$ (single step, involving facts) or $elim$ (multiple steps, see
    1.27 +  $rule$ (single step, involving facts) or $elim$ (repeated steps, see
    1.28    \S\ref{sec:classical-basic}).
    1.29  \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
    1.30    meta-level definitions throughout all goals; any facts provided are
    1.31    \emph{ignored}.
    1.32  \item [$succeed$] yields a single (unchanged) result; it is the identify of
    1.33 -  the ``\texttt{,}'' method combinator.
    1.34 +  the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
    1.35  \item [$fail$] yields an empty result sequence; it is the identify of the
    1.36 -  ``\texttt{|}'' method combinator.
    1.37 +  ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
    1.38  \end{descr}
    1.39  
    1.40  
    1.41 @@ -91,9 +92,9 @@
    1.42  \end{rail}
    1.43  
    1.44  \begin{descr}
    1.45 -\item [$tag~tags$ and $untag~tags$] add and remove $tags$ to the theorem,
    1.46 +\item [$tag~tags$ and $untag~tags$] add and remove $tags$ of the theorem,
    1.47    respectively.  Tags may be any list of strings that serve as comment for
    1.48 -  some tools (e.g.\ $\LEMMANAME$ causes tag ``$lemma$'' to be added to the
    1.49 +  some tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
    1.50    result).
    1.51  \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
    1.52    $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
    1.53 @@ -102,8 +103,7 @@
    1.54    
    1.55    $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$
    1.56    that does not include the automatic lifting process that is normally
    1.57 -  intended (see also \texttt{RS} and \texttt{COMP} in
    1.58 -  \cite[\S5]{isabelle-ref}).
    1.59 +  intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).
    1.60    
    1.61  \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
    1.62    instantiation, respectively.  The terms given in $of$ are substituted for
    1.63 @@ -113,7 +113,8 @@
    1.64  \item [$standard$] puts a theorem into the standard form of object-rules, just
    1.65    as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
    1.66    
    1.67 -\item [$elimify$] turns an destruction rule into an elimination.
    1.68 +\item [$elimify$] turns an destruction rule into an elimination, just as the
    1.69 +  ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
    1.70    
    1.71  \item [$export$] lifts a local result out of the current proof context,
    1.72    generalizing all fixed variables and discharging all assumptions.  Note that
    1.73 @@ -139,12 +140,12 @@
    1.74  Calculational proof is forward reasoning with implicit application of
    1.75  transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
    1.76  an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
    1.77 -results obtained by transitivity obtained together with the current result.
    1.78 -Command $\ALSO$ updates $calculation$ from the most recent result, while
    1.79 -$\FINALLY$ exhibits the final result by forward chaining towards the next goal
    1.80 -statement.  Both commands require valid current facts, i.e.\ may occur only
    1.81 -after commands that produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or
    1.82 -some finished $\HAVENAME$ or $\SHOWNAME$.
    1.83 +results obtained by transitivity composed with the current result.  Command
    1.84 +$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
    1.85 +final $calculation$ by forward chaining towards the next goal statement.  Both
    1.86 +commands require valid current facts, i.e.\ may occur only after commands that
    1.87 +produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
    1.88 +$\HAVENAME$, $\SHOWNAME$ etc.
    1.89  
    1.90  Also note that the automatic term abbreviation ``$\dots$'' has its canonical
    1.91  application with calculational proofs.  It automatically refers to the
    1.92 @@ -179,17 +180,19 @@
    1.93  \item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
    1.94    $\ALSO$, and concludes the current calculational thread.  The final result
    1.95    is exhibited as fact for forward chaining towards the next goal. Basically,
    1.96 -  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  A typical proof
    1.97 -  idiom is ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$''.
    1.98 +  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Typical proof
    1.99 +  idioms are``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
   1.100 +  ``$\FINALLY~\HAVE{}{\phi}~\DOT$''.
   1.101    
   1.102  \item [$trans$] maintains the set of transitivity rules of the theory or proof
   1.103    context, by adding or deleting theorems (the default is to add).
   1.104  \end{descr}
   1.105  
   1.106 -See theory \texttt{HOL/Isar_examples/Group} for a simple application of
   1.107 -calculations for basic equational reasoning.
   1.108 -\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
   1.109 -calculational steps in combination with natural deduction.
   1.110 +%FIXME
   1.111 +%See theory \texttt{HOL/Isar_examples/Group} for a simple application of
   1.112 +%calculations for basic equational reasoning.
   1.113 +%\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
   1.114 +%calculational steps in combination with natural deduction.
   1.115  
   1.116  
   1.117  \section{Axiomatic Type Classes}\label{sec:axclass}
   1.118 @@ -231,7 +234,7 @@
   1.119    establish the characteristic theorems of the type classes involved.  After
   1.120    finishing the proof the theory will be augmented by a type signature
   1.121    declaration corresponding to the resulting theorem.
   1.122 -\item [$intro_classes$] iteratively expands the class introduction rules of
   1.123 +\item [$intro_classes$] repeatedly expands the class introduction rules of
   1.124    this theory.
   1.125  \end{descr}
   1.126  
   1.127 @@ -243,17 +246,13 @@
   1.128  
   1.129  \subsection{Simplification methods}\label{sec:simp}
   1.130  
   1.131 -\indexisarmeth{simp}\indexisarmeth{asm-simp}
   1.132 +\indexisarmeth{simp}
   1.133  \begin{matharray}{rcl}
   1.134    simp & : & \isarmeth \\
   1.135 -  asm_simp & : & \isarmeth \\
   1.136  \end{matharray}
   1.137  
   1.138 -\railalias{asmsimp}{asm\_simp}
   1.139 -\railterm{asmsimp}
   1.140 -
   1.141  \begin{rail}
   1.142 -  ('simp' | asmsimp) (simpmod * )
   1.143 +  'simp' (simpmod * )
   1.144    ;
   1.145  
   1.146    simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
   1.147 @@ -261,15 +260,20 @@
   1.148  \end{rail}
   1.149  
   1.150  \begin{descr}
   1.151 -\item [$simp$ and $asm_simp$] invoke Isabelle's simplifier, after modifying
   1.152 -  the context by adding or deleting given rules.  The \railtoken{only}
   1.153 -  modifier first removes all other rewrite rules and congruences, and then is
   1.154 -  like \railtoken{add}.  In contrast, \railtoken{other} ignores its arguments;
   1.155 +\item [$simp$] invokes Isabelle's simplifier, after modifying the context by
   1.156 +  adding or deleting rules as specified.  The \railtoken{only} modifier first
   1.157 +  removes all other rewrite rules and congruences, and then is like
   1.158 +  \railtoken{add}.  In contrast, \railtoken{other} ignores its arguments;
   1.159    nevertheless there may be side-effects on the context via attributes.  This
   1.160    provides a back door for arbitrary context manipulation.
   1.161    
   1.162 -  Both of these methods are based on \texttt{asm_full_simp_tac}, see
   1.163 -  \cite[\S10]{isabelle-ref}; $simp$ removes any premises of the goal, before
   1.164 +  The $simp$ method is based on \texttt{asm_full_simp_tac} (see also
   1.165 +  \cite[\S10]{isabelle-ref}), but is much better behaved in practice.  Only
   1.166 +  the local premises of the actual goal are involved by default.  Additional
   1.167 +  facts may be insert via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).
   1.168 +  The full context of assumptions is
   1.169 +
   1.170 +; $simp$ removes any premises of the goal, before
   1.171    inserting the goal facts; $asm_simp$ leaves the premises.  Thus $asm_simp$
   1.172    may refer to premises that are not explicitly spelled out, potentially
   1.173    obscuring the reasoning.  The plain $simp$ method is more faithful in the
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/IsarRef/refcard.tex	Thu Oct 21 18:04:07 1999 +0200
     2.3 @@ -0,0 +1,8 @@
     2.4 +
     2.5 +\chapter{Isabelle/Isar Quick Reference}
     2.6 +
     2.7 +
     2.8 +%%% Local Variables: 
     2.9 +%%% mode: latex
    2.10 +%%% TeX-master: "isar-ref"
    2.11 +%%% End: