summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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 - intended (see also \texttt{RS} and \texttt{COMP} in - \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 context, by adding or deleting theorems (the default is to add). \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