--- 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: