even more stuff;
authorwenzelm
Fri Jul 30 18:27:25 1999 +0200 (1999-07-30)
changeset 7141a67dde8820c0
parent 7140 2c02c8e212fa
child 7142 89e0ff71d113
even more stuff;
doc-src/IsarRef/generic.tex
doc-src/IsarRef/hol.tex
doc-src/IsarRef/pure.tex
doc-src/IsarRef/syntax.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Fri Jul 30 15:59:00 1999 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Fri Jul 30 18:27:25 1999 +0200
     1.3 @@ -28,8 +28,8 @@
     1.4  \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
     1.5    c@2$] setup up a goal stating the class relation or type arity.  The proof
     1.6    would usually proceed by the $expand_classes$ method, and then establish the
     1.7 -  characteristic theorems of the type classes involved.  After the final
     1.8 -  $\QED{}$, the theory will be augmented by a type signature declaration
     1.9 +  characteristic theorems of the type classes involved.  After finishing the
    1.10 +  proof the theory will be augmented by a type signature declaration
    1.11    corresponding to the resulting theorem.
    1.12  \end{description}
    1.13  
     2.1 --- a/doc-src/IsarRef/hol.tex	Fri Jul 30 15:59:00 1999 +0200
     2.2 +++ b/doc-src/IsarRef/hol.tex	Fri Jul 30 18:27:25 1999 +0200
     2.3 @@ -1,16 +1,143 @@
     2.4  
     2.5 -\chapter{Isabelle/HOL specific tools and packages}
     2.6 +\chapter{Isabelle/HOL Tools and Packages}
     2.7  
     2.8  \section{Primitive types}
     2.9  
    2.10 -\section{Records}
    2.11 +\indexisarcmd{typedecl}\indexisarcmd{typedef}
    2.12 +\begin{matharray}{rcl}
    2.13 +  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
    2.14 +  \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
    2.15 +\end{matharray}
    2.16 +
    2.17 +\begin{rail}
    2.18 +  'typedecl' typespec infix? comment?
    2.19 +  ;
    2.20 +  'typedef' parname? typespec infix? \\ '=' term comment?
    2.21 +  ;
    2.22 +\end{rail}
    2.23 +
    2.24 +\begin{description}
    2.25 +\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
    2.26 +  $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
    2.27 +  also declares type arity $t :: (term, \dots, term) term$, making $t$ an
    2.28 +  actual HOL type constructor.
    2.29 +\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
    2.30 +  non-emptiness of the set $A$.  After finishing the proof, the theory will be
    2.31 +  augmented by a Gordon/HOL-style type definitions.  See \cite{isabelle-HOL}
    2.32 +  for more information.  Note that user-level work usually does not directly
    2.33 +  refer to the HOL $\isarkeyword{typedef}$ primitive, but uses more advanced
    2.34 +  packages such as $\isarkeyword{record}$ (\S\ref{sec:record}) or
    2.35 +  $\isarkeyword{datatype}$ (\S\ref{sec:datatype}).
    2.36 +\end{description}
    2.37 +
    2.38 +
    2.39 +\section{Records}\label{sec:record}
    2.40 +
    2.41 +%FIXME record_split method
    2.42 +\indexisarcmd{record}
    2.43 +\begin{matharray}{rcl}
    2.44 +  \isarcmd{record} & : & \isartrans{theory}{theory} \\
    2.45 +\end{matharray}
    2.46 +
    2.47 +\begin{rail}
    2.48 +  'record' typespec '=' (type '+')? (field +)
    2.49 +  ;
    2.50  
    2.51 -\section{Datatypes}
    2.52 +  field: name '::' type comment?
    2.53 +  ;
    2.54 +\end{rail}
    2.55 +
    2.56 +\begin{description}
    2.57 +\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
    2.58 +  defines extensible record type $(\vec\alpha)t$, derived from the optional
    2.59 +  parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
    2.60 +  See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only
    2.61 +  simply-typed records.
    2.62 +\end{description}
    2.63 +
    2.64 +
    2.65 +\section{Datatypes}\label{sec:datatype}
    2.66 +
    2.67 +\indexisarcmd{datatype}\indexisarcmd{rep_datatype}
    2.68 +\begin{matharray}{rcl}
    2.69 +  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
    2.70 +  \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
    2.71 +\end{matharray}
    2.72 +
    2.73 +\railalias{repdatatype}{rep\_datatype}
    2.74 +\railterm{repdatatype}
    2.75 +
    2.76 +\begin{rail}
    2.77 +  'datatype' (parname? typespec infix? \\ '=' (cons + '|') + 'and')
    2.78 +  ;
    2.79 +  repdatatype (name * ) \\ 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
    2.80 +  ;
    2.81 +
    2.82 +  cons: name (type * ) mixfix? comment?
    2.83 +  ;
    2.84 +\end{rail}
    2.85 +
    2.86 +\begin{description}
    2.87 +\item [$\isarkeyword{datatype}$] FIXME
    2.88 +\item [$\isarkeyword{rep_datatype}$] FIXME
    2.89 +\end{description}
    2.90 +
    2.91  
    2.92  \section{Recursive functions}
    2.93  
    2.94 +\indexisarcmd{primrec}\indexisarcmd{recdef}
    2.95 +\begin{matharray}{rcl}
    2.96 +  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
    2.97 +  \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
    2.98 +%FIXME
    2.99 +%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
   2.100 +\end{matharray}
   2.101 +
   2.102 +\begin{rail}
   2.103 +  'primrec' parname? (thmdecl? prop comment? + )
   2.104 +  ;
   2.105 +  'recdef' name term (term comment? +) \\ ('congs' thmrefs)? ('simpset' name)?
   2.106 +  ;
   2.107 +\end{rail}
   2.108 +
   2.109 +\begin{description}
   2.110 +\item [$\isarkeyword{primrec}$] FIXME
   2.111 +\item [$\isarkeyword{recdef}$] FIXME
   2.112 +\end{description}
   2.113 +
   2.114 +
   2.115  \section{(Co)Inductive sets}
   2.116  
   2.117 +\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive\_cases}
   2.118 +\begin{matharray}{rcl}
   2.119 +  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
   2.120 +  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
   2.121 +  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
   2.122 +\end{matharray}
   2.123 +
   2.124 +\railalias{condefs}{con\_defs}
   2.125 +\railalias{indcases}{inductive\_cases}
   2.126 +\railterm{condefs,indcases}
   2.127 +
   2.128 +\begin{rail}
   2.129 +  ('inductive' | 'coinductive') (term comment? +) \\
   2.130 +    'intrs' attributes? (thmdecl? prop comment? +) \\
   2.131 +    'monos' thmrefs comment? \\ condefs thmrefs comment?
   2.132 +  ;
   2.133 +  indcases thmdef? nameref ':' \\ (prop +) comment?
   2.134 +  ;
   2.135 +\end{rail}
   2.136 +
   2.137 +\begin{description}
   2.138 +\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] FIXME
   2.139 +\item [$\isarkeyword{inductive_cases}$] FIXME
   2.140 +\end{description}
   2.141 +
   2.142 +
   2.143 +\section{Proof by induction}
   2.144 +
   2.145 +%FIXME induct proof method
   2.146 +
   2.147  
   2.148  %%% Local Variables: 
   2.149  %%% mode: latex
     3.1 --- a/doc-src/IsarRef/pure.tex	Fri Jul 30 15:59:00 1999 +0200
     3.2 +++ b/doc-src/IsarRef/pure.tex	Fri Jul 30 18:27:25 1999 +0200
     3.3 @@ -136,7 +136,7 @@
     3.4  \end{description}
     3.5  
     3.6  
     3.7 -\subsection{Types}
     3.8 +\subsection{Types}\label{sec:types-pure}
     3.9  
    3.10  \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
    3.11  \begin{matharray}{rcl}
    3.12 @@ -327,9 +327,9 @@
    3.13  
    3.14  \subsection{ML translation functions}
    3.15  
    3.16 -\indexisarcmd{parse_ast_translation}\indexisarcmd{parse_translation}
    3.17 -\indexisarcmd{print_translation}\indexisarcmd{typed_print_translation}
    3.18 -\indexisarcmd{print_ast_translation}\indexisarcmd{token_translation}
    3.19 +\indexisarcmd{parse\_ast\_translation}\indexisarcmd{parse\_translation}
    3.20 +\indexisarcmd{print\_translation}\indexisarcmd{typed\_print\_translation}
    3.21 +\indexisarcmd{print\_ast\_translation}\indexisarcmd{token\_translation}
    3.22  \begin{matharray}{rcl}
    3.23    \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
    3.24    \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
    3.25 @@ -367,7 +367,8 @@
    3.26  
    3.27  \subsection{Goal statements}
    3.28  
    3.29 -\indexisarcmd{}
    3.30 +\indexisarcmd{theorem}\indexisarcmd{lemma}
    3.31 +\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
    3.32  \begin{matharray}{rcl}
    3.33    \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
    3.34    \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
    3.35 @@ -495,15 +496,6 @@
    3.36    \isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\
    3.37  \end{matharray}
    3.38  
    3.39 -\begin{rail}
    3.40 -  llbrace
    3.41 -  ;
    3.42 -  rrbrace
    3.43 -  ;
    3.44 -  'next'
    3.45 -  ;
    3.46 -\end{rail}
    3.47 -
    3.48  \begin{description}
    3.49  \item [$ $] FIXME
    3.50  \end{description}
    3.51 @@ -533,7 +525,7 @@
    3.52  
    3.53  \subsection{Improper proof steps}
    3.54  
    3.55 -\indexisarcmd{apply}\indexisarcmd{then_apply}\indexisarcmd{back}
    3.56 +\indexisarcmd{apply}\indexisarcmd{then\_apply}\indexisarcmd{back}
    3.57  \begin{matharray}{rcl}
    3.58    \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\
    3.59    \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\
    3.60 @@ -593,8 +585,8 @@
    3.61  
    3.62  \subsection{System operations}
    3.63  
    3.64 -\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use_thy}\indexisarcmd{use_thy_only}
    3.65 -\indexisarcmd{update_thy}\indexisarcmd{update_thy_only}
    3.66 +\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use\_thy}\indexisarcmd{use\_thy\_only}
    3.67 +\indexisarcmd{update\_thy}\indexisarcmd{update\_thy\_only}
    3.68  \begin{matharray}{rcl}
    3.69    \isarcmd{cd} & : & \isarkeep{\cdot} \\
    3.70    \isarcmd{pwd} & : & \isarkeep{\cdot} \\
     4.1 --- a/doc-src/IsarRef/syntax.tex	Fri Jul 30 15:59:00 1999 +0200
     4.2 +++ b/doc-src/IsarRef/syntax.tex	Fri Jul 30 18:27:25 1999 +0200
     4.3 @@ -35,10 +35,12 @@
     4.4  \verb|"let"|).  Already existing objects are usually referenced by
     4.5  \railqtoken{nameref}.
     4.6  
     4.7 -\indexoutertoken{name}\indexoutertoken{nameref}
     4.8 +\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
     4.9  \begin{rail}
    4.10    name : ident | symident | string
    4.11    ;
    4.12 +  parname : '(' name ')'
    4.13 +  ;
    4.14    nameref : name | longident
    4.15    ;
    4.16  \end{rail}