--- a/doc-src/IsarRef/conversion.tex Tue Mar 05 18:54:55 2002 +0100
+++ b/doc-src/IsarRef/conversion.tex Tue Mar 05 18:55:46 2002 +0100
@@ -221,7 +221,7 @@
$simp$, $blast$, or $auto$. This would work as follows:
\begin{matharray}{l}
\LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\
- \quad \APPLY{unfold~defs} \quad \CMT{or ``$\APPLY{insert~facts}$''} \\
+ \quad \APPLY{unfold~defs} \\
\quad \APPLY{blast} \\
\quad \DONE \\
\end{matharray}
--- a/doc-src/IsarRef/generic.tex Tue Mar 05 18:54:55 2002 +0100
+++ b/doc-src/IsarRef/generic.tex Tue Mar 05 18:55:46 2002 +0100
@@ -16,7 +16,7 @@
interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic
may make use of this light-weight mechanism of abstract theories
\cite{Wenzel:1997:TPHOL}. There is also a tutorial on using axiomatic type
-classes in isabelle \cite{isabelle-axclass} that is part of the standard
+classes in Isabelle \cite{isabelle-axclass} that is part of the standard
Isabelle documentation.
\begin{rail}
@@ -27,7 +27,7 @@
\end{rail}
\begin{descr}
-\item [$\AXCLASS~c \subseteq \vec c~axms$] defines an axiomatic type class as
+\item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
the intersection of existing classes, with additional axioms holding. Class
axioms may not contain more than one type variable. The class axioms (with
implicit sort constraints added) are bound to the given names. Furthermore
@@ -37,7 +37,7 @@
The ``axioms'' are stored as theorems according to the given name
specifications, adding the class name $c$ as name space prefix; these facts
- are stored collectively as $c.axioms$, too.
+ are stored collectively as $c{\dtt}axioms$, too.
\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a
goal stating a class relation or type arity. The proof would usually
@@ -132,8 +132,8 @@
\item [$\LOCALE~loc~=~import~+~body$] defines new locale $loc$ as a context
consisting of a certain view of existing locales ($import$) plus some
additional elements ($body$). Both $import$ and $body$ are optional; the
- trivial $\LOCALE~loc$ defines an empty locale, which may still be useful to
- collect declarations of facts later on. Type-inference on locale
+ degenerate form $\LOCALE~loc$ defines an empty locale, which may still be
+ useful to collect declarations of facts later on. Type-inference on locale
expressions automatically takes care of the most general typing that the
combined context elements may acquire.
@@ -299,16 +299,14 @@
\end{matharray}
\begin{rail}
- ('also' | 'finally') transrules?
+ ('also' | 'finally') ('(' thmrefs ')')?
;
'trans' (() | 'add' | 'del')
;
-
- transrules: '(' thmrefs ')'
- ;
\end{rail}
\begin{descr}
+
\item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as
follows. The first occurrence of $\ALSO$ in some calculational thread
initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
@@ -328,22 +326,23 @@
\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
but collect results only, without applying rules.
-\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity (and
- symmetry) rules declared in the current context.
-
+\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity
+ rules (for calculational commands $\ALSO$ and $\FINALLY$) and symmetry rules
+ (for the $symmetric$ operation and single step elimination patters) of the
+ current context.
+
\item [$trans$] declares theorems as transitivity rules.
-\item [$sym$] declares symmetry rules, to be used either with the $symmetric$
- operation (see below), or in canonical single-step eliminations (such as
- ``$\ASSUME{}{x = y}~\HENCE{}{y = x}~\DDOT$'').
-
- Isabelle/Pure declares symmetry of $\equiv$, common object-logics add
- further standard rules, such as symmetry of $=$ and $\not=$.
+\item [$sym$] declares symmetry rules.
\item [$symmetric$] resolves a theorem with some rule declared as $sym$ in the
current context. For example, ``$\ASSUME{[symmetric]}{x = y}$'' produces a
swapped fact derived from that assumption.
-
+
+ In structured proof texts it is often more appropriate to use an explicit
+ single-step elimination proof, such as ``$\ASSUME{}{x = y}~\HENCE{}{y =
+ x}~\DDOT$''. Note that the very same rules known to $symmetric$ are
+ declared as $elim$ at the same time.
\end{descr}
@@ -360,7 +359,7 @@
insert & : & \isarmeth \\[0.5ex]
erule^* & : & \isarmeth \\
drule^* & : & \isarmeth \\
- frule^* & : & \isarmeth \\[0.5ex]
+ frule^* & : & \isarmeth \\
succeed & : & \isarmeth \\
fail & : & \isarmeth \\
\end{matharray}
@@ -373,11 +372,14 @@
\end{rail}
\begin{descr}
-\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
- meta-level definitions throughout all goals; any facts provided are inserted
- into the goal and subject to rewriting as well.
+
+\item [$unfold~\vec a$ and $fold~\vec a$] expand (or fold back again) the
+ given meta-level definitions throughout all goals; any chained facts
+ provided are inserted into the goal and subject to rewriting as well.
+
\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
state. Note that current facts indicated for forward chaining are ignored.
+
\item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the
basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
elim-resolution, destruct-resolution, and forward-resolution, respectively
@@ -390,17 +392,20 @@
rather than via implicit proof state manipulations. For example, a proper
single-step elimination would be done using the basic $rule$ method, with
forward chaining of current facts.
+
\item [$succeed$] yields a single (unchanged) result; it is the identity of
the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
+
\item [$fail$] yields an empty result sequence; it is the identity of the
``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
+
\end{descr}
\indexisaratt{tagged}\indexisaratt{untagged}
\indexisaratt{THEN}\indexisaratt{COMP}
\indexisaratt{where}\indexisaratt{unfolded}\indexisaratt{folded}
\indexisaratt{standard}\indexisaratt{elim-format}
-\indexisaratt{no-vars}\indexisaratt{exported}
+\indexisaratt{no-vars}
\begin{matharray}{rcl}
tagged & : & \isaratt \\
untagged & : & \isaratt \\[0.5ex]
@@ -412,7 +417,6 @@
standard & : & \isaratt \\
elim_format & : & \isaratt \\
no_vars^* & : & \isaratt \\
- exported^* & : & \isaratt \\
\end{matharray}
\begin{rail}
@@ -450,10 +454,6 @@
see also the ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
\item [$no_vars$] replaces schematic variables by free ones; this is mainly
for tuning output of pretty printed theorems.
-\item [$exported$] lifts a local result out of the current proof context,
- generalizing all fixed variables and discharging all assumptions. Note that
- proper incremental export is already done as part of the basic Isar
- machinery. This attribute is mainly for experimentation.
\end{descr}
@@ -547,7 +547,7 @@
\cite[\S3]{isabelle-ref}).
\item [$cut_tac$] inserts facts into the proof state as assumption of a
subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}. Note
- that the scope of schmatic variables is spread over the main goal statement.
+ that the scope of schematic variables is spread over the main goal statement.
Instantiations may be given as well, see also ML tactic
\texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.
\item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note
@@ -567,7 +567,6 @@
implicit theory context, the ML code may refer to the following locally
bound values:
-%%FIXME ttbox produces too much trailing space (why?)
{\footnotesize\begin{verbatim}
val ctxt : Proof.context
val facts : thm list
@@ -637,7 +636,7 @@
By default the Simplifier methods take local assumptions fully into account,
using equational assumptions in the subsequent normalization process, or
-simplifying assumptions themselvess (cf.\ \texttt{asm_full_simp_tac} in
+simplifying assumptions themselves (cf.\ \texttt{asm_full_simp_tac} in
\cite[\S10]{isabelle-ref}). In structured proofs this is usually quite well
behaved in practice: just the local premises of the actual goal are involved,
additional facts may inserted via explicit forward-chaining (using $\THEN$,
@@ -665,7 +664,7 @@
\indexisarcmd{print-simpset}
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
\begin{matharray}{rcl}
- print_simpset^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{print_simpset}^* & : & \isarkeep{theory~|~proof} \\
simp & : & \isaratt \\
cong & : & \isaratt \\
split & : & \isaratt \\
@@ -677,12 +676,17 @@
\end{rail}
\begin{descr}
-\item [$print_simpset$] prints the collection of rules declared to the
- Simplifier, which is also known as ``simpset'' internally
+
+\item [$\isarcmd{print_simpset}$] prints the collection of rules declared to
+ the Simplifier, which is also known as ``simpset'' internally
\cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply.
+
\item [$simp$] declares simplification rules.
+
\item [$cong$] declares congruence rules.
+
\item [$split$] declares case split rules.
+
\end{descr}
@@ -762,13 +766,13 @@
\subsubsection{Basic methods}\label{sec:classical-basic}
-\indexisarmeth{rule}\indexisarmeth{intro}
-\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}
+\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
+\indexisarmeth{intro}\indexisarmeth{elim}
\begin{matharray}{rcl}
rule & : & \isarmeth \\
+ contradiction & : & \isarmeth \\
intro & : & \isarmeth \\
elim & : & \isarmeth \\
- contradiction & : & \isarmeth \\
\end{matharray}
\begin{rail}
@@ -777,13 +781,20 @@
\end{rail}
\begin{descr}
+
\item [$rule$] as offered by the classical reasoner is a refinement over the
- primitive one (see \S\ref{sec:pure-meth-att}). In case that no rules are
- provided as arguments, it automatically determines elimination and
- introduction rules from the context (see also \S\ref{sec:classical-mod}).
- This is made the default method for basic proof steps, such as $\PROOFNAME$
- and ``$\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and
- \S\ref{sec:pure-meth-att}.
+ primitive one (see \S\ref{sec:pure-meth-att}). Both versions essentially
+ work the same, but the classical version observes the classical rule context
+ in addition to the Isabelle/Pure one.
+
+ The library of common object logics (HOL, ZF, etc.) usually declare a rich
+ collection of classical rules (even if these perfectly OK from the
+ intuitionistic viewpoint), but only few declarations to the rule context of
+ Isabelle/Pure (\S\ref{sec:pure-meth-att}).
+
+\item [$contradiction$] solves some goal by contradiction, deriving any result
+ from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may
+ appear in either order.
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or
elim-resolution, after having inserted any facts. Omitting the arguments
@@ -792,10 +803,7 @@
of what actually happens, thus it is very appropriate as an initial method
for $\PROOFNAME$ that splits up certain connectives of the goal, before
entering the actual sub-proof.
-
-\item [$contradiction$] solves some goal by contradiction, deriving any result
- from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may
- appear in either order.
+
\end{descr}
@@ -891,7 +899,7 @@
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
\indexisaratt{iff}\indexisaratt{rule}
\begin{matharray}{rcl}
- print_claset^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{print_claset}^* & : & \isarkeep{theory~|~proof} \\
intro & : & \isaratt \\
elim & : & \isaratt \\
dest & : & \isaratt \\
@@ -909,31 +917,31 @@
\end{rail}
\begin{descr}
-\item [$print_claset$] prints the collection of rules declared to the
- Classical Reasoner, which is also known as ``simpset'' internally
+
+\item [$\isarcmd{print_claset}$] prints the collection of rules declared to
+ the Classical Reasoner, which is also known as ``simpset'' internally
\cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply.
+
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
destruction rules, respectively. By default, rules are considered as
\emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not
applied in the search-oriented automated methods, but only in single-step
methods such as $rule$).
+
\item [$rule~del$] deletes introduction, elimination, or destruction rules from
the context.
-\item [$iff$] declares a (possibly conditional) ``safe'' rule to the context in
- several ways. The rule is declared as a rewrite rule to the Simplifier.
- Furthermore, it is
- declared in several ways (depending on its structure) to the Classical
- Reasoner for aggressive use, which would normally be indicated by ``!'').
- If the rule is an equivalence, the two corresponding implications are
- declared as introduction and destruction rules. Otherwise,
- if the rule is an inequality, the corresponding negation elimination rule
- is declared, else the rule itself is declared as an introduction rule.
- The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only,
- and omits the Simplifier declaration. Thus the declaration does not have
- any effect on automated proof tools, but only on simple methods such as
- $rule$ (see \S\ref{sec:misc-meth-att}).
+\item [$iff$] declares a logical equivalences to the Simplifier and the
+ Classical reasoner at the same time. Non-conditional rules result in a
+ ``safe'' introduction and elimination pair; conditional ones are considered
+ ``unsafe''. Rules with negative conclusion are automatically inverted
+ (using $\neg$-elimination).
+
+ The ``?'' version of $iff$ declares rules to the Pure context only, and
+ omits the Simplifier declaration. Thus the declaration does not have any
+ effect on automated proof tools, but only on the single-step $rule$ method
+ (see \S\ref{sec:misc-meth-att}).
\end{descr}
@@ -986,8 +994,11 @@
\railterm{casenames}
\begin{rail}
- 'case' nameref attributes?
+ 'case' caseref | ('(' caseref ((name | underscore) +) ')')
;
+ caseref: nameref attributes?
+ ;
+
casenames (name + )
;
'params' ((name * ) + 'and')
@@ -1189,17 +1200,24 @@
;
\end{rail}
-The $cases$ and $induct$ attributes augment the corresponding context of rules
-for reasoning about inductive sets and types. The standard rules are already
-declared by advanced definitional packages. For special applications, these
-may be replaced manually by variant versions.
+\begin{descr}
+
+\item [$\isarkeyword{print_induct_rules}$] prints cases and induct rules for
+ sets and types of the current context.
-Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:rule-cases}) to
-adjust names of cases and parameters of a rule.
-
-The $consumes$ declaration (cf.\ \S\ref{sec:rule-cases}) is taken care of
-automatically (if none had been given already): $consumes~0$ is specified for
-``type'' rules and $consumes~1$ for ``set'' rules.
+\item [$cases$ and $induct$] (as attributes) augment the corresponding context
+ of rules for reasoning about inductive sets and types, using the
+ corresponding methods of the same name. Certain definitional packages of
+ object-logics usually declare emerging cases and induction rules as
+ expected, so users rarely need to intervene.
+
+ Manual rule declarations usually include the the $case_names$ and $ps$
+ attributes to adjust names of cases and parameters of a rule (see
+ \S\ref{sec:rule-cases}); the $consumes$ declaration is taken care of
+ automatically: $consumes~0$ is specified for ``type'' rules and $consumes~1$
+ for ``set'' rules.
+
+\end{descr}
%%% Local Variables:
%%% mode: latex
--- a/doc-src/IsarRef/logics.tex Tue Mar 05 18:54:55 2002 +0100
+++ b/doc-src/IsarRef/logics.tex Tue Mar 05 18:55:46 2002 +0100
@@ -149,7 +149,7 @@
\railterm{complete}
\begin{rail}
- splitformat (((name * ) + 'and') | ('(' complete ')'))
+ splitformat (((name *) + 'and') | ('(' complete ')'))
;
\end{rail}
@@ -396,12 +396,12 @@
\begin{rail}
'datatype' (dtspec + 'and')
;
- repdatatype (name * ) dtrules
+ repdatatype (name *) dtrules
;
dtspec: parname? typespec infix? '=' (cons + '|')
;
- cons: name (type * ) mixfix?
+ cons: name (type *) mixfix?
;
dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
\end{rail}
@@ -421,8 +421,9 @@
old-style theory syntax being used there! Apart from proper proof methods for
case-analysis and induction, there are also emulations of ML tactics
\texttt{case_tac} and \texttt{induct_tac} available, see
-\S\ref{sec:induct_tac}; these admit to refer directly to the internal
-structure of subgoals (including internally bound parameters).
+\S\ref{sec:hol-induct-tac} or \S\ref{sec:zf-induct-tac}; these admit to refer
+directly to the internal structure of subgoals (including internally bound
+parameters).
\subsection{Recursive functions}\label{sec:recursion}
@@ -432,8 +433,7 @@
\isarcmd{primrec} & : & \isartrans{theory}{theory} \\
\isarcmd{recdef} & : & \isartrans{theory}{theory} \\
\isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
-%FIXME
-% \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
+% \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\ %FIXME
\end{matharray}
\railalias{recdefsimp}{recdef\_simp}
@@ -449,16 +449,16 @@
\railterm{recdeftc}
\begin{rail}
- 'primrec' parname? (equation + )
+ 'primrec' parname? (equation +)
;
- 'recdef' ('(' 'permissive' ')')? \\ name term (prop + ) hints?
+ 'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
;
recdeftc thmdecl? tc
;
equation: thmdecl? prop
;
- hints: '(' 'hints' (recdefmod * ) ')'
+ hints: '(' 'hints' (recdefmod *) ')'
;
recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
;
@@ -467,23 +467,27 @@
\end{rail}
\begin{descr}
+
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
- datatypes, see also \cite{isabelle-HOL} FIXME.
+ datatypes, see also \cite{isabelle-HOL}.
+
\item [$\isarkeyword{recdef}$] defines general well-founded recursive
- functions (using the TFL package), see also \cite{isabelle-HOL} FIXME. The
+ functions (using the TFL package), see also \cite{isabelle-HOL}. The
$(permissive)$ option tells TFL to recover from failed proof attempts,
returning unfinished results. The $recdef_simp$, $recdef_cong$, and
$recdef_wf$ hints refer to auxiliary rules to be used in the internal
- automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\
+ automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\
\S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
- (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
+ (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
\S\ref{sec:classical}).
+
\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
termination condition number $i$ (default $1$) as generated by a
$\isarkeyword{recdef}$ definition of constant $c$.
-
+
Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
internal proofs without manual intervention.
+
\end{descr}
Both kinds of recursive definitions accommodate reasoning by induction (cf.\
@@ -533,9 +537,6 @@
mono & : & \isaratt \\
\end{matharray}
-\railalias{condefs}{con\_defs}
-\railterm{condefs}
-
\begin{rail}
('inductive' | 'coinductive') sets intros monos?
;
@@ -557,8 +558,8 @@
automated monotonicity proof of $\isarkeyword{inductive}$.
\end{descr}
-See \cite{isabelle-HOL} FIXME for further information on inductive definitions
-in HOL.
+See \cite{isabelle-HOL} for further information on inductive definitions in
+HOL, but note that this covers the old-style theory format.
\subsection{Arithmetic proof support}
@@ -584,7 +585,7 @@
performed by the Simplifier.
-\subsection{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
+\subsection{Cases and induction: emulating tactic scripts}\label{sec:hol-induct-tac}
The following important tactical tools of Isabelle/HOL have been ported to
Isar. These should be never used in proper proof texts!
@@ -681,7 +682,7 @@
dmspec: typespec '=' (cons + '|')
;
- cons: name (type * ) mixfix?
+ cons: name (type *) mixfix?
;
dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
\end{rail}
@@ -698,11 +699,142 @@
\subsection{Type checking}
-FIXME
+The ZF logic is essentially untyped, so the concept of ``type checking'' is
+performed as logical reasoning about set-membership statements. A special
+method assists users in this task; a version of this is already declared as a
+``solver'' in the default Simplifier context.
+
+\indexisarcmd{print-tcset}\indexisaratt{typecheck}\indexisaratt{TC}
+
+\begin{matharray}{rcl}
+ \isarcmd{print_tcset}^* & : & \isarkeep{theory~|~proof} \\
+ typecheck & : & \isarmeth \\
+ TC & : & \isaratt \\
+\end{matharray}
+
+\begin{rail}
+ 'TC' (() | 'add' | 'del')
+ ;
+\end{rail}
+
+\begin{descr}
+
+\item [$\isarcmd{print_tcset}$] prints the collection of typechecking rules of
+ the current context.
+
+ Note that the component built into the Simplifier only knows about those
+ rules being declared globally in the theory!
+
+\item [$typecheck$] attempts to solve any pending type-checking problems in
+ subgoals.
+
+\item [$TC$] adds or deletes type-checking rules from the context.
+
+\end{descr}
+
+
+\subsection{(Co)Inductive sets and datatypes}
+
+\subsubsection{Set definitions}
+
+In ZF everything is a set. The generic inductive package also provides a
+specific view for ``datatype'' specifications. Coinductive definitions are
+available as well.
+
+\indexisarcmdof{ZF}{inductive}\indexisarcmdof{ZF}{coinductive}
+\indexisarcmdof{ZF}{datatype}\indexisarcmdof{ZF}{codatatype}
+\begin{matharray}{rcl}
+ \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
+ \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
+ \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
+ \isarcmd{codatatype} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\railalias{CONDEFS}{con\_defs}
+\railterm{CONDEFS}
+
+\railalias{TYPEINTROS}{type\_intros}
+\railterm{TYPEINTROS}
+
+\railalias{TYPEELIMS}{type\_elims}
+\railterm{TYPEELIMS}
+
+\begin{rail}
+ ('inductive' | 'coinductive') domains intros hints
+ ;
-\subsection{Inductive sets and datatypes}
+ domains: 'domains' (term + '+') ('<=' | subseteq) term
+ ;
+ intros: 'intros' (thmdecl? prop +)
+ ;
+ hints: monos? condefs? typeintros? typeelims?
+ ;
+ monos: ('monos' thmrefs)?
+ ;
+ condefs: (CONDEFS thmrefs)?
+ ;
+ typeintros: (TYPEINTROS thmrefs)?
+ ;
+ typeelims: (TYPEELIMS thmrefs)?
+ ;
+\end{rail}
+
+In the following diagram $monos$, $typeintros$, and $typeelims$ are the same
+as above.
+
+\begin{rail}
+ ('datatype' | 'codatatype') domain? (dtspec + 'and') hints
+ ;
+
+ domain: ('<=' | subseteq) term
+ ;
+ dtspec: term '=' (con + '|')
+ ;
+ con: name ('(' (term ',' +) ')')?
+ ;
+ hints: monos? typeintros? typeelims?
+ ;
+\end{rail}
+
+See \cite{isabelle-ZF} for further information on inductive definitions in
+HOL, but note that this covers the old-style theory format.
-FIXME
+
+\subsubsection{Primitive recursive functions}
+
+\indexisarcmdof{ZF}{primrec}
+\begin{matharray}{rcl}
+ \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\begin{rail}
+ 'primrec' (thmdecl? prop +)
+ ;
+\end{rail}
+
+
+\subsubsection{Cases and induction: emulating tactic scripts}\label{sec:zf-induct-tac}
+
+The following important tactical tools of Isabelle/ZF have been ported to
+Isar. These should be never used in proper proof texts!
+
+\indexisarmethof{ZF}{case-tac}\indexisarmethof{ZF}{induct-tac}
+\indexisarmethof{ZF}{ind-cases}\indexisarcmdof{ZF}{inductive-cases}
+\begin{matharray}{rcl}
+ case_tac^* & : & \isarmeth \\
+ induct_tac^* & : & \isarmeth \\
+ ind_cases^* & : & \isarmeth \\
+ \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\begin{rail}
+ (casetac | inducttac) goalspec? name
+ ;
+ indcases (prop +)
+ ;
+ inductivecases (thmdecl? (prop +) + 'and')
+ ;
+\end{rail}
%%% Local Variables:
--- a/doc-src/IsarRef/pure.tex Tue Mar 05 18:54:55 2002 +0100
+++ b/doc-src/IsarRef/pure.tex Tue Mar 05 18:55:46 2002 +0100
@@ -291,19 +291,20 @@
\end{rail}
\begin{descr}
+
\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
except that the actual logical signature extension is omitted. Thus the
context free grammar of Isabelle's inner syntax may be augmented in
arbitrary ways, independently of the logic. The $mode$ argument refers to
- the print mode that the grammar rules belong; unless the \texttt{output}
- flag is given, all productions are added both to the input and output
- grammar.
+ the print mode that the grammar rules belong; unless the
+ $\isarkeyword{output}$ indicator is given, all productions are added both to
+ the input and output grammar.
+
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation
- rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==} or
- \isasymrightleftharpoons), parse rules (\texttt{=>} or
- \isasymrightharpoonup), or print rules (\texttt{<=} or
- \isasymleftharpoondown). Translation patterns may be prefixed by the
- syntactic category to be used for parsing; the default is \texttt{logic}.
+ rules (i.e.\ macros): parse~/ print rules (\isasymrightleftharpoons), parse
+ rules (\isasymrightharpoonup), or print rules (\isasymleftharpoondown).
+ Translation patterns may be prefixed by the syntactic category to be used
+ for parsing; the default is $logic$.
\end{descr}
@@ -333,7 +334,7 @@
Everyday work is typically done the hard way, with proper definitions and
actual proven theorems.
-\item [$\isarkeyword{lemmas}~a = \vec b$] restrieves and stores existing facts
+\item [$\isarkeyword{lemmas}~a = \vec b$] retrieves and stores existing facts
in the theory context, or the specified locale (see also
\S\ref{sec:locale}). Typical applications would also involve attributes, to
declare Simplifier rules, for example.
@@ -933,43 +934,59 @@
object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and
\ref{ch:logics}).
-\indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$}
-\indexisaratt{OF}\indexisaratt{of}
+\indexisarmeth{$-$}\indexisarmeth{assumption}
+\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{rules}
\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
+\indexisaratt{OF}\indexisaratt{of}
\begin{matharray}{rcl}
+ - & : & \isarmeth \\
assumption & : & \isarmeth \\
this & : & \isarmeth \\
rule & : & \isarmeth \\
- - & : & \isarmeth \\
- OF & : & \isaratt \\
- of & : & \isaratt \\
+ rules & : & \isarmeth \\[0.5ex]
intro & : & \isaratt \\
elim & : & \isaratt \\
dest & : & \isaratt \\
- rule & : & \isaratt \\
+ rule & : & \isaratt \\[0.5ex]
+ OF & : & \isaratt \\
+ of & : & \isaratt \\
\end{matharray}
-%FIXME intro!, intro, intro?
-
\begin{rail}
'rule' thmrefs?
;
+ 'rules' ('!' ?) (rulemod *)
+ ;
+ rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
+ ;
+ ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
+ ;
+ 'rule' 'del'
+ ;
'OF' thmrefs
;
'of' insts ('concl' ':' insts)?
;
- 'rule' 'del'
- ;
\end{rail}
\begin{descr}
+
+\item [``$-$''] does nothing but insert the forward chaining facts as premises
+ into the goal. Note that command $\PROOFNAME$ without any method actually
+ performs a single reduction step using the $rule$ method; thus a plain
+ \emph{do-nothing} proof step would be $\PROOF{-}$ rather than $\PROOFNAME$
+ alone.
+
\item [$assumption$] solves some goal by a single assumption step. Any facts
given (${} \le 1$) are guaranteed to participate in the refinement. Recall
that $\QEDNAME$ (see \S\ref{sec:proof-steps}) already concludes any
- remaining sub-goals by assumption.
+ remaining sub-goals by assumption, so structured proofs usually need not
+ quote the $assumption$ method at all.
+
\item [$this$] applies all of the current facts directly as rules. Recall
that ``$\DOT$'' (dot) abbreviates $\BY{this}$.
+
\item [$rule~\vec a$] 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
@@ -980,27 +997,41 @@
$elim$, $dest$ attributes (see below). This is the default behavior of
$\PROOFNAME$ and ``$\DDOT$'' (double-dot) steps (see
\S\ref{sec:proof-steps}).
-\item [``$-$''] does nothing but insert the forward chaining facts as premises
- into the goal. Note that command $\PROOFNAME$ without any method actually
- performs a single reduction step using the $rule$ method; thus a plain
- \emph{do-nothing} proof step would be $\PROOF{-}$ rather than $\PROOFNAME$
- alone.
+
+\item [$rules$] performs intuitionistic proof search, depending on
+ specifically declared rules from the context, or given as explicit
+ arguments. Chained facts are inserted into the goal before commencing proof
+ search; $rules!$ means to include the current $prems$ as well.
+
+ Rules need to be classified as $intro$, $elim$, or $dest$; here the ``$!$''
+ indicator refers to ``safe'' rules, which may be applied aggressively
+ (without considering back-tracking later). Rules declared with ``$?$'' are
+ ignored in proof search (the single-step $rule$ method still observes
+ these). An explicit weight annotation may be given as well; otherwise the
+ number of rule premises will be taken into account.
+
+\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
+ destruct rules, to be used with the $rule$ and $rules$ methods. Note that
+ the latter will ignore rules declare with ``$?$'', while ``$!$'' are used
+ most aggressively.
+
+ The classical reasoner (see \S\ref{sec:classical-basic}) introduces its own
+ variants of these attributes; use qualified names to access the present
+ versions of Isabelle/Pure, i.e.\ $Pure{\dtt}intro$ or $CPure{\dtt}intro$.
+
+\item [$rule~del$] undeclares introduction, elimination, or destruct rules.
+
\item [$OF~\vec a$] applies some theorem to given rules $\vec a$ (in
parallel). This corresponds to the \texttt{MRS} operator in ML
\cite[\S5]{isabelle-ref}, but note the reversed order. Positions may be
skipped by including ``$\_$'' (underscore) as argument.
+
\item [$of~\vec t$] performs positional instantiation. The terms $\vec t$ are
substituted for any schematic variables occurring in a theorem from left to
right; ``\texttt{_}'' (underscore) indicates to skip a position. Arguments
following a ``$concl\colon$'' specification refer to positions of the
conclusion of a rule.
-\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
- destruct rules, respectively. Note that the classical reasoner (see
- \S\ref{sec:classical-basic}) introduces different versions of these
- attributes, and the $rule$ method, too. In object-logics with classical
- reasoning enabled, the latter version should be used all the time to avoid
- confusion!
-\item [$rule~del$] undeclares introduction, elimination, or destruct rules.
+
\end{descr}
--- a/doc-src/IsarRef/refcard.tex Tue Mar 05 18:54:55 2002 +0100
+++ b/doc-src/IsarRef/refcard.tex Tue Mar 05 18:55:46 2002 +0100
@@ -23,7 +23,9 @@
theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\
& \Or & \LEMMA{name}{prop}~proof \\
& \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex]
- proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex]
+ proof & = & prfx^*~\PROOF{method}~stmt^*~\QED{method} \\[1ex]
+ prfx & = & \APPLY{method} \\
+ & \Or & \USING{name^+} \\
stmt & = & \BG~stmt^*~\EN \\
& \Or & \NEXT \\
& \Or & \NOTE{name}{name^+} \\
@@ -31,8 +33,8 @@
& \Or & \FIX{var^+} \\
& \Or & \ASSUME{name}{prop^+}\\
& \Or & \THEN~goal{\dsh}stmt \\
- & \Or & goal{\dsh}stmt \\
- goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\
+ & \Or & goal \\
+ goal & = & \HAVE{name}{prop}~proof \\
& \Or & \SHOW{name}{prop}~proof \\
\end{matharray}
@@ -104,6 +106,7 @@
$unfold~\vec a$ & \Text{definitions} \\[2ex]
\multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
+ $rules$ & \Text{intuitionistic proof search} \\
$simp$, $simp_all$ & Simplifier (+ Splitter) \\
$blast$, $fast$ & Classical Reasoner \\
$auto$, $force$ & Simplifier + Classical Reasoner \\