--- a/doc-src/IsarRef/generic.tex Fri Jul 30 15:59:00 1999 +0200
+++ b/doc-src/IsarRef/generic.tex Fri Jul 30 18:27:25 1999 +0200
@@ -28,8 +28,8 @@
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
c@2$] setup up a goal stating the class relation or type arity. The proof
would usually proceed by the $expand_classes$ method, and then establish the
- characteristic theorems of the type classes involved. After the final
- $\QED{}$, the theory will be augmented by a type signature declaration
+ 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.
\end{description}
--- a/doc-src/IsarRef/hol.tex Fri Jul 30 15:59:00 1999 +0200
+++ b/doc-src/IsarRef/hol.tex Fri Jul 30 18:27:25 1999 +0200
@@ -1,16 +1,143 @@
-\chapter{Isabelle/HOL specific tools and packages}
+\chapter{Isabelle/HOL Tools and Packages}
\section{Primitive types}
-\section{Records}
+\indexisarcmd{typedecl}\indexisarcmd{typedef}
+\begin{matharray}{rcl}
+ \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
+ \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
+\end{matharray}
+
+\begin{rail}
+ 'typedecl' typespec infix? comment?
+ ;
+ 'typedef' parname? typespec infix? \\ '=' term comment?
+ ;
+\end{rail}
+
+\begin{description}
+\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
+ $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
+ also declares type arity $t :: (term, \dots, term) term$, making $t$ an
+ actual HOL type constructor.
+\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
+ non-emptiness of the set $A$. After finishing the proof, the theory will be
+ augmented by a Gordon/HOL-style type definitions. See \cite{isabelle-HOL}
+ for more information. Note that user-level work usually does not directly
+ refer to the HOL $\isarkeyword{typedef}$ primitive, but uses more advanced
+ packages such as $\isarkeyword{record}$ (\S\ref{sec:record}) or
+ $\isarkeyword{datatype}$ (\S\ref{sec:datatype}).
+\end{description}
+
+
+\section{Records}\label{sec:record}
+
+%FIXME record_split method
+\indexisarcmd{record}
+\begin{matharray}{rcl}
+ \isarcmd{record} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\begin{rail}
+ 'record' typespec '=' (type '+')? (field +)
+ ;
-\section{Datatypes}
+ field: name '::' type comment?
+ ;
+\end{rail}
+
+\begin{description}
+\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
+ defines extensible record type $(\vec\alpha)t$, derived from the optional
+ parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
+ See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only
+ simply-typed records.
+\end{description}
+
+
+\section{Datatypes}\label{sec:datatype}
+
+\indexisarcmd{datatype}\indexisarcmd{rep_datatype}
+\begin{matharray}{rcl}
+ \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
+ \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\railalias{repdatatype}{rep\_datatype}
+\railterm{repdatatype}
+
+\begin{rail}
+ 'datatype' (parname? typespec infix? \\ '=' (cons + '|') + 'and')
+ ;
+ repdatatype (name * ) \\ 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
+ ;
+
+ cons: name (type * ) mixfix? comment?
+ ;
+\end{rail}
+
+\begin{description}
+\item [$\isarkeyword{datatype}$] FIXME
+\item [$\isarkeyword{rep_datatype}$] FIXME
+\end{description}
+
\section{Recursive functions}
+\indexisarcmd{primrec}\indexisarcmd{recdef}
+\begin{matharray}{rcl}
+ \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
+ \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
+%FIXME
+% \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\begin{rail}
+ 'primrec' parname? (thmdecl? prop comment? + )
+ ;
+ 'recdef' name term (term comment? +) \\ ('congs' thmrefs)? ('simpset' name)?
+ ;
+\end{rail}
+
+\begin{description}
+\item [$\isarkeyword{primrec}$] FIXME
+\item [$\isarkeyword{recdef}$] FIXME
+\end{description}
+
+
\section{(Co)Inductive sets}
+\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive\_cases}
+\begin{matharray}{rcl}
+ \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
+ \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
+ \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\railalias{condefs}{con\_defs}
+\railalias{indcases}{inductive\_cases}
+\railterm{condefs,indcases}
+
+\begin{rail}
+ ('inductive' | 'coinductive') (term comment? +) \\
+ 'intrs' attributes? (thmdecl? prop comment? +) \\
+ 'monos' thmrefs comment? \\ condefs thmrefs comment?
+ ;
+ indcases thmdef? nameref ':' \\ (prop +) comment?
+ ;
+\end{rail}
+
+\begin{description}
+\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] FIXME
+\item [$\isarkeyword{inductive_cases}$] FIXME
+\end{description}
+
+
+\section{Proof by induction}
+
+%FIXME induct proof method
+
%%% Local Variables:
%%% mode: latex
--- a/doc-src/IsarRef/pure.tex Fri Jul 30 15:59:00 1999 +0200
+++ b/doc-src/IsarRef/pure.tex Fri Jul 30 18:27:25 1999 +0200
@@ -136,7 +136,7 @@
\end{description}
-\subsection{Types}
+\subsection{Types}\label{sec:types-pure}
\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
\begin{matharray}{rcl}
@@ -327,9 +327,9 @@
\subsection{ML translation functions}
-\indexisarcmd{parse_ast_translation}\indexisarcmd{parse_translation}
-\indexisarcmd{print_translation}\indexisarcmd{typed_print_translation}
-\indexisarcmd{print_ast_translation}\indexisarcmd{token_translation}
+\indexisarcmd{parse\_ast\_translation}\indexisarcmd{parse\_translation}
+\indexisarcmd{print\_translation}\indexisarcmd{typed\_print\_translation}
+\indexisarcmd{print\_ast\_translation}\indexisarcmd{token\_translation}
\begin{matharray}{rcl}
\isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
\isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
@@ -367,7 +367,8 @@
\subsection{Goal statements}
-\indexisarcmd{}
+\indexisarcmd{theorem}\indexisarcmd{lemma}
+\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
\begin{matharray}{rcl}
\isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
\isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
@@ -495,15 +496,6 @@
\isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\
\end{matharray}
-\begin{rail}
- llbrace
- ;
- rrbrace
- ;
- 'next'
- ;
-\end{rail}
-
\begin{description}
\item [$ $] FIXME
\end{description}
@@ -533,7 +525,7 @@
\subsection{Improper proof steps}
-\indexisarcmd{apply}\indexisarcmd{then_apply}\indexisarcmd{back}
+\indexisarcmd{apply}\indexisarcmd{then\_apply}\indexisarcmd{back}
\begin{matharray}{rcl}
\isarcmd{apply}^* & : & \isartrans{proof}{proof} \\
\isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\
@@ -593,8 +585,8 @@
\subsection{System operations}
-\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use_thy}\indexisarcmd{use_thy_only}
-\indexisarcmd{update_thy}\indexisarcmd{update_thy_only}
+\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use\_thy}\indexisarcmd{use\_thy\_only}
+\indexisarcmd{update\_thy}\indexisarcmd{update\_thy\_only}
\begin{matharray}{rcl}
\isarcmd{cd} & : & \isarkeep{\cdot} \\
\isarcmd{pwd} & : & \isarkeep{\cdot} \\
--- a/doc-src/IsarRef/syntax.tex Fri Jul 30 15:59:00 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex Fri Jul 30 18:27:25 1999 +0200
@@ -35,10 +35,12 @@
\verb|"let"|). Already existing objects are usually referenced by
\railqtoken{nameref}.
-\indexoutertoken{name}\indexoutertoken{nameref}
+\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
\begin{rail}
name : ident | symident | string
;
+ parname : '(' name ')'
+ ;
nameref : name | longident
;
\end{rail}