more;
authorwenzelm
Fri Jul 30 15:40:54 1999 +0200 (1999-07-30)
changeset 71358eabfd7e6b9b
parent 7134 320b412e5800
child 7136 71f6eef45713
more;
doc-src/IsarRef/Makefile
doc-src/IsarRef/basics.tex
doc-src/IsarRef/clasimp.tex
doc-src/IsarRef/generic.tex
doc-src/IsarRef/hol.tex
doc-src/IsarRef/isar-ref.tex
doc-src/IsarRef/pure.tex
doc-src/IsarRef/syntax.tex
     1.1 --- a/doc-src/IsarRef/Makefile	Fri Jul 30 14:59:32 1999 +0200
     1.2 +++ b/doc-src/IsarRef/Makefile	Fri Jul 30 15:40:54 1999 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  NAME = isar-ref
     1.5  
     1.6  FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \
     1.7 -	clasimp.tex hol.tex ../isar.sty \
     1.8 +	generic.tex hol.tex ../isar.sty \
     1.9  	../rail.sty ../railsetup.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
    1.10  
    1.11  dvi: $(NAME).dvi
     2.1 --- a/doc-src/IsarRef/basics.tex	Fri Jul 30 14:59:32 1999 +0200
     2.2 +++ b/doc-src/IsarRef/basics.tex	Fri Jul 30 15:40:54 1999 +0200
     2.3 @@ -1,11 +1,13 @@
     2.4  
     2.5 -\chapter{Basic concepts}
     2.6 +\chapter{Basic Concepts}
     2.7  
     2.8  \section{Isabelle/Isar Theories}
     2.9  
    2.10  \section{The Isar proof language}
    2.11  
    2.12 -\subsection{Proof methods}
    2.13 +\subsection{Proof commands}
    2.14 +
    2.15 +\subsection{Methods}
    2.16  
    2.17  \subsection{Attributes}
    2.18  
     3.1 --- a/doc-src/IsarRef/clasimp.tex	Fri Jul 30 14:59:32 1999 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,7 +0,0 @@
     3.4 -
     3.5 -\chapter{The Simplifier and Classical Reasoner}
     3.6 -
     3.7 -%%% Local Variables: 
     3.8 -%%% mode: latex
     3.9 -%%% TeX-master: "isar-ref"
    3.10 -%%% End: 
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/IsarRef/generic.tex	Fri Jul 30 15:40:54 1999 +0200
     4.3 @@ -0,0 +1,60 @@
     4.4 +
     4.5 +\chapter{Generic Tools and Packages}
     4.6 +
     4.7 +\section{Axiomatic Type Classes}\label{sec:axclass}
     4.8 +
     4.9 +\indexisarcmd{axclass}\indexisarcmd{instance}
    4.10 +\begin{matharray}{rcl}
    4.11 +  \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
    4.12 +  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
    4.13 +\end{matharray}
    4.14 +
    4.15 +Axiomatic type classes are provided by Isabelle/Pure as a purely
    4.16 +\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}).  Thus
    4.17 +any object logic may make use of this light-weight mechanism for abstract
    4.18 +theories.  See \cite{Wenzel:1997:TPHOL} for more information.  There is also a
    4.19 +tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
    4.20 +the standard Isabelle documentation.
    4.21 +
    4.22 +\begin{rail}
    4.23 +  'axclass' classdecl (axmdecl prop comment? +)
    4.24 +  ;
    4.25 +  'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
    4.26 +  ;
    4.27 +\end{rail}
    4.28 +
    4.29 +\begin{description}
    4.30 +\item [$\isarkeyword{axclass}~$] FIXME
    4.31 +\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
    4.32 +  c@2$] setup up a goal stating the class relation or type arity.  The proof
    4.33 +  would usually proceed by the $expand_classes$ method, and then establish the
    4.34 +  characteristic theorems of the type classes involved.  After the final
    4.35 +  $\QED{}$, the theory will be augmented by a type signature declaration
    4.36 +  corresponding to the resulting theorem.
    4.37 +\end{description}
    4.38 +
    4.39 +
    4.40 +
    4.41 +\section{The Simplifier}
    4.42 +
    4.43 +\section{The Classical Reasoner}
    4.44 +
    4.45 +
    4.46 +%\indexisarcmd{}
    4.47 +%\begin{matharray}{rcl}
    4.48 +%  \isarcmd{} & : & \isartrans{}{} \\
    4.49 +%\end{matharray}
    4.50 +
    4.51 +%\begin{rail}
    4.52 +  
    4.53 +%\end{rail}
    4.54 +
    4.55 +%\begin{description}
    4.56 +%\item [$ $]
    4.57 +%\end{description}
    4.58 +
    4.59 +
    4.60 +%%% Local Variables: 
    4.61 +%%% mode: latex
    4.62 +%%% TeX-master: "isar-ref"
    4.63 +%%% End: 
     5.1 --- a/doc-src/IsarRef/hol.tex	Fri Jul 30 14:59:32 1999 +0200
     5.2 +++ b/doc-src/IsarRef/hol.tex	Fri Jul 30 15:40:54 1999 +0200
     5.3 @@ -1,5 +1,16 @@
     5.4  
     5.5 -\chapter{Isabelle/HOL specific elements}
     5.6 +\chapter{Isabelle/HOL specific tools and packages}
     5.7 +
     5.8 +\section{Primitive types}
     5.9 +
    5.10 +\section{Records}
    5.11 +
    5.12 +\section{Datatypes}
    5.13 +
    5.14 +\section{Recursive functions}
    5.15 +
    5.16 +\section{(Co)Inductive sets}
    5.17 +
    5.18  
    5.19  %%% Local Variables: 
    5.20  %%% mode: latex
     6.1 --- a/doc-src/IsarRef/isar-ref.tex	Fri Jul 30 14:59:32 1999 +0200
     6.2 +++ b/doc-src/IsarRef/isar-ref.tex	Fri Jul 30 15:40:54 1999 +0200
     6.3 @@ -56,7 +56,7 @@
     6.4  \include{basics}
     6.5  \include{syntax}
     6.6  \include{pure}
     6.7 -\include{clasimp}
     6.8 +\include{generic}
     6.9  \include{hol}
    6.10  
    6.11  \begingroup
     7.1 --- a/doc-src/IsarRef/pure.tex	Fri Jul 30 14:59:32 1999 +0200
     7.2 +++ b/doc-src/IsarRef/pure.tex	Fri Jul 30 15:40:54 1999 +0200
     7.3 @@ -105,7 +105,7 @@
     7.4  \end{description}
     7.5  
     7.6  
     7.7 -\subsection{Type classes and sorts}
     7.8 +\subsection{Type classes and sorts}\label{sec:classes}
     7.9  
    7.10  \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
    7.11  \begin{matharray}{rcl}
    7.12 @@ -115,7 +115,7 @@
    7.13  \end{matharray}
    7.14  
    7.15  \begin{rail}
    7.16 -  'classes' (name ('<' (nameref ',' +))? comment? +)
    7.17 +  'classes' (classdecl +)
    7.18    ;
    7.19    'classrel' nameref '<' nameref comment?
    7.20    ;
    7.21 @@ -253,7 +253,7 @@
    7.22  \end{matharray}
    7.23  
    7.24  \begin{rail}
    7.25 -  'axioms' (name attributes? ':' prop comment? +)
    7.26 +  'axioms' (axmdecl prop comment? +)
    7.27    ;
    7.28    ('theorems' | 'lemmas') thmdef? thmrefs
    7.29    ;
     8.1 --- a/doc-src/IsarRef/syntax.tex	Fri Jul 30 14:59:32 1999 +0200
     8.2 +++ b/doc-src/IsarRef/syntax.tex	Fri Jul 30 15:40:54 1999 +0200
     8.3 @@ -74,6 +74,7 @@
     8.4  ever refer to sorts or arities explicitly.
     8.5  
     8.6  \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
     8.7 +\indexouternonterm{classdecl}
     8.8  \begin{rail}
     8.9    sort : nameref | lbrace (nameref * ',') rbrace
    8.10    ;
    8.11 @@ -81,6 +82,7 @@
    8.12    ;
    8.13    simplearity : ( () | '(' (sort + ',') ')' ) nameref
    8.14    ;
    8.15 +  classdecl: name ('<' (nameref ',' +))? comment?
    8.16  \end{rail}
    8.17  
    8.18  
    8.19 @@ -181,10 +183,13 @@
    8.20  as proof method arguments).  Any of these may include lists of attributes,
    8.21  which are applied to the preceding theorem or list of theorems.
    8.22  
    8.23 -\indexouternonterm{thmdecl}\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
    8.24 +\indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
    8.25 +\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
    8.26  \begin{rail}
    8.27    thmname : name attributes | name | attributes
    8.28    ;
    8.29 +  axmdecl : name attributes? ':'
    8.30 +  ;
    8.31    thmdecl : thmname ':'
    8.32    ;
    8.33    thmdef : thmname '='