author wenzelm Thu, 21 Oct 1999 18:04:07 +0200 changeset 7897 7f18f5ffbb92 parent 7896 36865f14e5ce child 7898 d7e65a52acf9
*** empty log message ***
 doc-src/IsarRef/generic.tex file | annotate | diff | comparison | revisions doc-src/IsarRef/refcard.tex file | annotate | diff | comparison | revisions
--- a/doc-src/IsarRef/generic.tex	Thu Oct 21 17:42:42 1999 +0200
+++ b/doc-src/IsarRef/generic.tex	Thu Oct 21 18:04:07 1999 +0200
@@ -29,29 +29,30 @@
plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
$\PROOFNAME$ alone.
\item [$assumption$] solves some goal by assumption.  Any facts given are
-  guaranteed to participate in the refinement.
+  guaranteed to participate in the refinement.  Note that $\DOT$'' (dot)
+  abbreviates $\BY{assumption}$.
\item [$rule~thms$] applies some rule given as argument in backward manner;
facts are used to reduce the rule before applying it to the goal.  Thus
$rule$ without facts is plain \emph{introduction}, while with facts it
-  becomes an \emph{elimination}.
+  becomes a (generalized) \emph{elimination}.

Note that the classical reasoner introduces another version of $rule$ that
is able to pick appropriate rules automatically, whenever explicit $thms$
are omitted (see \S\ref{sec:classical-basic}); that method is the default
-  one for initial proof steps, such as $\PROOFNAME$ and $\DDOT$'' (two
-  dots).
+  for $\PROOFNAME$ steps.  Note that $\DDOT$'' (double-dot) abbreviates
+  $\BY{default}$.
\item [$erule~thms$] is similar to $rule$, but applies rules by
elim-resolution.  This is an improper method, mainly for experimentation and
porting of old scripts.  Actual elimination proofs are usually done with
-  $rule$ (single step, involving facts) or $elim$ (multiple steps, see
+  $rule$ (single step, involving facts) or $elim$ (repeated steps, see
\S\ref{sec:classical-basic}).
\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
meta-level definitions throughout all goals; any facts provided are
\emph{ignored}.
\item [$succeed$] yields a single (unchanged) result; it is the identify of
-  the \texttt{,}'' method combinator.
+  the \texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
\item [$fail$] yields an empty result sequence; it is the identify of the
-  \texttt{|}'' method combinator.
+  \texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
\end{descr}

@@ -91,9 +92,9 @@
\end{rail}

\begin{descr}
-\item [$tag~tags$ and $untag~tags$] add and remove $tags$ to the theorem,
+\item [$tag~tags$ and $untag~tags$] add and remove $tags$ of the theorem,
respectively.  Tags may be any list of strings that serve as comment for
-  some tools (e.g.\ $\LEMMANAME$ causes tag $lemma$'' to be added to the
+  some tools (e.g.\ $\LEMMANAME$ causes the tag $lemma$'' to be added to the
result).
\item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
$thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
@@ -102,8 +103,7 @@

$RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$
that does not include the automatic lifting process that is normally
-  \cite[\S5]{isabelle-ref}).
+  intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).

\item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
instantiation, respectively.  The terms given in $of$ are substituted for
@@ -113,7 +113,8 @@
\item [$standard$] puts a theorem into the standard form of object-rules, just
as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).

-\item [$elimify$] turns an destruction rule into an elimination.
+\item [$elimify$] turns an destruction rule into an elimination, just as the
+  ML function \texttt{make\_elim} (see \cite{isabelle-ref}).

\item [$export$] lifts a local result out of the current proof context,
generalizing all fixed variables and discharging all assumptions.  Note that
@@ -139,12 +140,12 @@
Calculational proof is forward reasoning with implicit application of
transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
-results obtained by transitivity obtained together with the current result.
-Command $\ALSO$ updates $calculation$ from the most recent result, while
-$\FINALLY$ exhibits the final result by forward chaining towards the next goal
-statement.  Both commands require valid current facts, i.e.\ may occur only
-after commands that produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or
-some finished $\HAVENAME$ or $\SHOWNAME$.
+results obtained by transitivity composed with the current result.  Command
+$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
+final $calculation$ by forward chaining towards the next goal statement.  Both
+commands require valid current facts, i.e.\ may occur only after commands that
+produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
+$\HAVENAME$, $\SHOWNAME$ etc.

Also note that the automatic term abbreviation $\dots$'' has its canonical
application with calculational proofs.  It automatically refers to the
@@ -179,17 +180,19 @@
\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
$\ALSO$, and concludes the current calculational thread.  The final result
is exhibited as fact for forward chaining towards the next goal. Basically,
-  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  A typical proof
-  idiom is $\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$''.
+  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Typical proof
+  idioms are$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
+  $\FINALLY~\HAVE{}{\phi}~\DOT$''.

\item [$trans$] maintains the set of transitivity rules of the theory or proof
\end{descr}

-See theory \texttt{HOL/Isar_examples/Group} for a simple application of
-calculations for basic equational reasoning.
-\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
-calculational steps in combination with natural deduction.
+%FIXME
+%See theory \texttt{HOL/Isar_examples/Group} for a simple application of
+%calculations for basic equational reasoning.
+%\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
+%calculational steps in combination with natural deduction.

\section{Axiomatic Type Classes}\label{sec:axclass}
@@ -231,7 +234,7 @@
establish the characteristic theorems of the type classes involved.  After
finishing the proof the theory will be augmented by a type signature
declaration corresponding to the resulting theorem.
-\item [$intro_classes$] iteratively expands the class introduction rules of
+\item [$intro_classes$] repeatedly expands the class introduction rules of
this theory.
\end{descr}

@@ -243,17 +246,13 @@

\subsection{Simplification methods}\label{sec:simp}

-\indexisarmeth{simp}\indexisarmeth{asm-simp}
+\indexisarmeth{simp}
\begin{matharray}{rcl}
simp & : & \isarmeth \\
-  asm_simp & : & \isarmeth \\
\end{matharray}

-\railalias{asmsimp}{asm\_simp}
-\railterm{asmsimp}
-
\begin{rail}
-  ('simp' | asmsimp) (simpmod * )
+  'simp' (simpmod * )
;

simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
@@ -261,15 +260,20 @@
\end{rail}

\begin{descr}
-\item [$simp$ and $asm_simp$] invoke Isabelle's simplifier, after modifying
-  the context by adding or deleting given rules.  The \railtoken{only}
-  modifier first removes all other rewrite rules and congruences, and then is
-  like \railtoken{add}.  In contrast, \railtoken{other} ignores its arguments;
+\item [$simp$] invokes Isabelle's simplifier, after modifying the context by
+  adding or deleting rules as specified.  The \railtoken{only} modifier first
+  removes all other rewrite rules and congruences, and then is like
+  \railtoken{add}.  In contrast, \railtoken{other} ignores its arguments;
nevertheless there may be side-effects on the context via attributes.  This
provides a back door for arbitrary context manipulation.

-  Both of these methods are based on \texttt{asm_full_simp_tac}, see
-  \cite[\S10]{isabelle-ref}; $simp$ removes any premises of the goal, before
+  The $simp$ method is based on \texttt{asm_full_simp_tac} (see also
+  \cite[\S10]{isabelle-ref}), but is much better behaved in practice.  Only
+  the local premises of the actual goal are involved by default.  Additional
+  facts may be insert via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).
+  The full context of assumptions is
+
+; $simp$ removes any premises of the goal, before
inserting the goal facts; $asm_simp$ leaves the premises.  Thus $asm_simp$
may refer to premises that are not explicitly spelled out, potentially
obscuring the reasoning.  The plain $simp$ method is more faithful in the
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/refcard.tex	Thu Oct 21 18:04:07 1999 +0200
@@ -0,0 +1,8 @@
+
+\chapter{Isabelle/Isar Quick Reference}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "isar-ref"
+%%% End: