1.1 --- a/doc-src/IsarRef/generic.tex Mon Aug 23 09:36:05 1999 +0200
1.2 +++ b/doc-src/IsarRef/generic.tex Mon Aug 23 11:43:21 1999 +0200
1.3 @@ -154,6 +154,7 @@
1.4 \begin{matharray}{rcl}
1.5 \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
1.6 \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
1.7 + expand_classes & : & \isarmeth \\
1.8 \end{matharray}
1.9
1.10 Axiomatic type classes are provided by Isabelle/Pure as a purely
1.11 @@ -178,8 +179,12 @@
1.12 characteristic theorems of the type classes involved. After finishing the
1.13 proof the theory will be augmented by a type signature declaration
1.14 corresponding to the resulting theorem.
1.15 +\item [Method $expand_classes$] iteratively expands the class introduction
1.16 + rules
1.17 \end{descr}
1.18
1.19 +See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
1.20 +axiomatic type classes, including instantiation proofs.
1.21
1.22
1.23 \section{The Simplifier}
1.24 @@ -194,13 +199,15 @@
1.25 \end{matharray}
1.26
1.27 \begin{rail}
1.28 - 'simp' (simpmod+)?
1.29 + 'simp' (simpmod * )
1.30 ;
1.31
1.32 simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
1.33 ;
1.34 \end{rail}
1.35
1.36 +FIXME
1.37 +
1.38
1.39 \subsection{Forward simplification}
1.40
2.1 --- a/doc-src/IsarRef/hol.tex Mon Aug 23 09:36:05 1999 +0200
2.2 +++ b/doc-src/IsarRef/hol.tex Mon Aug 23 11:43:21 1999 +0200
2.3 @@ -51,10 +51,11 @@
2.4 \item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
2.5 defines extensible record type $(\vec\alpha)t$, derived from the optional
2.6 parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
2.7 - See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only
2.8 - simply-typed extensible records.
2.9 \end{descr}
2.10
2.11 +See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only
2.12 +simply-typed extensible records.
2.13 +
2.14
2.15 \section{Datatypes}\label{sec:datatype}
2.16
2.17 @@ -78,10 +79,15 @@
2.18 \end{rail}
2.19
2.20 \begin{descr}
2.21 -\item [$\isarkeyword{datatype}$] FIXME
2.22 -\item [$\isarkeyword{rep_datatype}$] FIXME
2.23 +\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
2.24 +\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
2.25 + ones, generating the standard infrastructure of derived concepts (primitive
2.26 + recursion etc.).
2.27 \end{descr}
2.28
2.29 +See \cite{isabelle-HOL} for more details on datatypes. Note that the theory
2.30 +syntax above has been slightly simplified over the old version.
2.31 +
2.32
2.33 \section{Recursive functions}
2.34
2.35 @@ -101,10 +107,14 @@
2.36 \end{rail}
2.37
2.38 \begin{descr}
2.39 -\item [$\isarkeyword{primrec}$] FIXME
2.40 -\item [$\isarkeyword{recdef}$] FIXME
2.41 +\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
2.42 + datatypes.
2.43 +\item [$\isarkeyword{recdef}$] defines general well-founded recursive
2.44 + functions (using the TFL package).
2.45 \end{descr}
2.46
2.47 +See \cite{isabelle-HOL} for more information.
2.48 +
2.49
2.50 \section{(Co)Inductive sets}
2.51
2.52 @@ -129,14 +139,47 @@
2.53 \end{rail}
2.54
2.55 \begin{descr}
2.56 -\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] FIXME
2.57 -\item [$\isarkeyword{inductive_cases}$] FIXME
2.58 +\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
2.59 + (co)inductive sets from the given introduction rules.
2.60 +\item [$\isarkeyword{inductive_cases}$] creates simplified instances of
2.61 + elimination rules of (co)inductive sets.
2.62 \end{descr}
2.63
2.64 +See \cite{isabelle-HOL} for more information. Note that
2.65 +$\isarkeyword{inductive_cases}$ corresponds to the ML function
2.66 +\texttt{mk_cases}.
2.67 +
2.68
2.69 \section{Proof by induction}
2.70
2.71 -FIXME induct proof method
2.72 +\indexisarmeth{induct}
2.73 +\begin{matharray}{rcl}
2.74 + induct & : & \isarmeth \\
2.75 +\end{matharray}
2.76 +
2.77 +The $induct$ method provides a uniform interface to induction over datatypes,
2.78 +inductive sets, and recursive functions. Basically, it is just an interface
2.79 +to the $rule$ method applied to appropriate instances of the corresponding
2.80 +induction rules.
2.81 +
2.82 +\begin{rail}
2.83 + 'induct' (inst * 'and') kind?
2.84 + ;
2.85 +
2.86 + inst: term term?
2.87 + ;
2.88 + kind: ('type' | 'set' | 'function') ':' nameref
2.89 + ;
2.90 +\end{rail}
2.91 +
2.92 +\begin{descr}
2.93 +\item [$induct~insts~kind$] abbreviates method $rule~R$, where $R$ is the
2.94 + induction rule of the type/set/function specified by $kind$ and instantiated
2.95 + by $insts$. The latter either consists of pairs $P$ $x$ (induction
2.96 + predicate and variable), where $P$ is optional. If $kind$ is omitted, the
2.97 + default is to pick a datatype induction rule according to the type of some
2.98 + induction variable (at least one has to be given in that case).
2.99 +\end{descr}
2.100
2.101
2.102 %%% Local Variables:
3.1 --- a/doc-src/IsarRef/pure.tex Mon Aug 23 09:36:05 1999 +0200
3.2 +++ b/doc-src/IsarRef/pure.tex Mon Aug 23 11:43:21 1999 +0200
3.3 @@ -117,8 +117,9 @@
3.4 mark chapter and section headings.
3.5 \item [$\TEXT~text$] specifies an actual body of prose text, including
3.6 references to formal entities.\footnote{The latter feature is not yet
3.7 - exploited. Nevertheless, any text of the form \texttt{\at\{\dots\}}
3.8 - should be considered as reserved for future use.}
3.9 + exploited. Nevertheless, any text of the form
3.10 + \texttt{\at\ttlbrace\dots\ttrbrace} should be considered as reserved for
3.11 + future use.}
3.12 \end{descr}
3.13
3.14
3.15 @@ -444,7 +445,7 @@
3.16 former closely correspond to Skolem constants, or meta-level universal
3.17 quantification as provided by the Isabelle/Pure logical framework.
3.18 Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
3.19 -a local entity that may be used in the subsequent proof as any other variable
3.20 +a local object that may be used in the subsequent proof as any other variable
3.21 or constant. Furthermore, any result $\phi[x]$ exported from the current
3.22 context will be universally closed wrt.\ $x$ at the outermost level (this is
3.23 expressed using Isabelle's meta-variables).
3.24 @@ -459,8 +460,8 @@
3.25 with some premise of the goal, $\PRESUMENAME$ leaves the subgoal unchanged to
3.26 be proved later by the user.
3.27
3.28 -Local definitions, introduced by $\DEF{a}{x \equiv t}$, are achieved by
3.29 -combining $\FIX x$ with another version of assumption that causes any
3.30 +Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
3.31 +combining $\FIX x$ with another kind of assumption that causes any
3.32 hypothetical equation $x = t$ to be eliminated by reflexivity. Thus,
3.33 exporting some result $\phi[x]$ simply yields $\phi[t]$.
3.34
3.35 @@ -481,20 +482,20 @@
3.36 \begin{descr}
3.37 \item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$.
3.38 \item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems
3.39 - $\Phi$. Subsequent results used to solve some enclosing goal (e.g.\ via
3.40 + $\Phi$. Subsequent results applied to some enclosing goal (e.g.\ via
3.41 $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be able to
3.42 unify with existing premises in the goal, while $\PRESUMENAME$ leaves $\Phi$
3.43 as new subgoals. Note that several lists of assumptions may be given
3.44 - (separated by \railterm{and}); the resulting list of current facts consists
3.45 - of all of these.
3.46 + (separated by $\isarkeyword{and}$); the resulting list of facts consists of
3.47 + all of these concatenated.
3.48 \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
3.49 In results exported from the context, $x$ is replaced by $t$. Basically,
3.50 $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$ (the
3.51 resulting hypothetical equation is solved by reflexivity, though).
3.52 \end{descr}
3.53
3.54 -The internal register $prems$\indexisarreg{prems} refers to all current
3.55 -assumptions as a list of theorems.
3.56 +The internal register $prems$\indexisarreg{prems} refers to the current list
3.57 +of assumptions.
3.58
3.59
3.60 \subsection{Facts and forward chaining}
3.61 @@ -507,10 +508,12 @@
3.62 \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
3.63 \end{matharray}
3.64
3.65 -New facts are established either by assumption or proof of local statements
3.66 -(via $\HAVENAME$ or $\SHOWNAME$). Any facts will usually be involved in
3.67 -proofs of further results: either as explicit arguments of proof methods or
3.68 -when forward chaining towards the next goal via $\THEN$ (and variants).
3.69 +New facts are established either by assumption or proof of local statements.
3.70 +Any facts will usually be involved in proofs of further results: either as
3.71 +explicit arguments of proof methods or when forward chaining towards the next
3.72 +goal via $\THEN$ (and variants). Note that the internal register of
3.73 +\emph{current facts} may be referred as theorem list
3.74 +$facts$.\indexisarreg{facts}
3.75
3.76 \begin{rail}
3.77 'note' thmdef? thmrefs comment?
3.78 @@ -536,9 +539,6 @@
3.79 chaining is from earlier facts together with the current ones.
3.80 \end{descr}
3.81
3.82 -Note that the internal register of \emph{current facts} may be referred as
3.83 -theorem list $facts$.\indexisarreg{facts}
3.84 -
3.85
3.86 \subsection{Goal statements}
3.87
3.88 @@ -666,7 +666,7 @@
3.89 \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve
3.90 the goal without much ado. Of course, the result is a fake theorem only,
3.91 involving some oracle in its internal derivation object (this is indicated
3.92 - as $[!]$ in the printed result. The main application of
3.93 + as $[!]$ in the printed result). The main application of
3.94 $\isarkeyword{sorry}$ is to support top-down proof development.
3.95 \end{descr}
3.96
3.97 @@ -725,8 +725,8 @@
3.98 $\LETNAME$ form the patterns occur on the left-hand side, while the $\ISNAME$
3.99 patterns are in postfix position.
3.100
3.101 -Note that term abbreviations are quite different from actual local definitions
3.102 -as introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are
3.103 +Term abbreviations are quite different from actual local definitions as
3.104 +introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are
3.105 visible within the logic as actual equations, while abbreviations disappear
3.106 during the input process just after type checking.
3.107
3.108 @@ -746,10 +746,11 @@
3.109 but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
3.110 \end{descr}
3.111
3.112 -Furthermore, a few automatic term abbreviations\index{automatic abbreviation}
3.113 -for goals and facts are available. For any open goal, $\VVar{thesis}$ refers
3.114 -to its object-logic statement, $\VVar{thesis_prop}$ to the full proposition
3.115 -(which may be a rule), and $\VVar{thesis_concl}$ to its (atomic) conclusion.
3.116 +A few \emph{automatic} term abbreviations\index{automatic abbreviation} for
3.117 +goals and facts are available as well. For any open goal, $\VVar{thesis}$
3.118 +refers to its object-logical statement, $\VVar{thesis_prop}$ to the full
3.119 +proposition (which may be a rule), and $\VVar{thesis_concl}$ to its (atomic)
3.120 +conclusion.
3.121
3.122 Facts (i.e.\ assumptions and finished goals) that have an application $f(x)$
3.123 as object-logic statement get $x$ bound to the special text variable
4.1 --- a/doc-src/IsarRef/syntax.tex Mon Aug 23 09:36:05 1999 +0200
4.2 +++ b/doc-src/IsarRef/syntax.tex Mon Aug 23 11:43:21 1999 +0200
4.3 @@ -13,9 +13,8 @@
4.4 \emph{outer} syntax. Inner syntax is that of Isabelle types and terms of the
4.5 logic, while outer syntax is that of Isabelle/Isar theories (and proofs). As
4.6 a general rule, inner syntax entities may occur only as \emph{atomic entities}
4.7 -within outer syntax. For example, quoted string \texttt{"x + y"} and
4.8 -identifier \texttt{z} are legal term specifications, while \texttt{x + y} is
4.9 -not.
4.10 +within outer syntax. Thus, string \texttt{"x + y"} and identifier \texttt{z}
4.11 +are legal term specifications, while \texttt{x + y} is not.
4.12
4.13 \begin{warn}
4.14 Note that old-style Isabelle theories used to fake parts of the inner type
4.15 @@ -42,15 +41,16 @@
4.16 typefree & = & \verb,',ident \\
4.17 typevar & = & \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
4.18 string & = & \verb,", ~\dots~ \verb,", \\
4.19 - verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\[2ex]
4.20 -
4.21 + verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\
4.22 +\end{matharray}
4.23 +\begin{matharray}{rcl}
4.24 letter & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
4.25 digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
4.26 quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
4.27 sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~ %$
4.28 - \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \verb,<, ~|~
4.29 - \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \mathtt{\at} ~|~ \verb,^, ~|~ \verb,_, ~|~
4.30 - \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
4.31 + \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~
4.32 + \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \mathtt{\at} ~|~ \\
4.33 + & & \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
4.34 \end{matharray}
4.35
4.36 The syntax of \texttt{string} admits any characters, including newlines;