--- a/doc-src/Logics/HOL.tex Sat Oct 24 17:16:20 1998 +0200
+++ b/doc-src/Logics/HOL.tex Sat Oct 24 20:22:45 1998 +0200
@@ -1065,14 +1065,12 @@
$\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General
tuples are simulated by pairs nested to the right:
\begin{center}
-\begin{tabular}{|c|c|}
-\hline
+\begin{tabular}{c|c}
external & internal \\
\hline
$\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\
\hline
$(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\
-\hline
\end{tabular}
\end{center}
In addition, it is possible to use tuples
@@ -1459,6 +1457,7 @@
\begin{figure}[htbp]
\begin{rail}
typedef : 'typedef' ( () | '(' name ')') type '=' set witness;
+
type : typevarlist name ( () | '(' infix ')' );
set : string;
witness : () | '(' id ')';
@@ -1542,68 +1541,71 @@
\section{Records}
-At a first approximation, records are just a minor generalization of tuples,
-where components may be addressed by labels instead of just position. The
-version of records offered by Isabelle/HOL is slightly more advanced, though,
-supporting \emph{extensible record schemes}. This admits operations that are
-polymorphic wrt.\ record extensions, yielding ``object-oriented'' effects like
-(single) inheritance. See also \cite{Naraschewski-Wenzel:1998:TPHOL} for more
-details on object-oriented verification and record subtyping in HOL.
+At a first approximation, records are just a minor generalisation of tuples,
+where components may be addressed by labels instead of just position (think of
+{\ML}, for example). The version of records offered by Isabelle/HOL is
+slightly more advanced, though, supporting \emph{extensible record schemes}.
+This admits operations that are polymorphic with respect to record extension,
+yielding ``object-oriented'' effects like (single) inheritance. See also
+\cite{Naraschewski-Wenzel:1998:TPHOL} for more details on object-oriented
+verification and record subtyping in HOL.
+
\subsection{Basics}
-Isabelle/HOL supports concrete syntax for both fixed and schematic record
-terms and types:
-
+Isabelle/HOL supports fixed and schematic records both at the level of terms
+and types. The concrete syntax is as follows:
+
+\begin{center}
\begin{tabular}{l|l|l}
- & terms & types \\ \hline
+ & record terms & record types \\ \hline
fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\
- scheme & $\record{x = a\fs y = b\fs \more = more}$ &
- $\record{x \ty A\fs y \ty B\fs \more \ty \mu}$ \\
+ schematic & $\record{x = a\fs y = b\fs \more = m}$ &
+ $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\
\end{tabular}
-
-The \textsc{ascii} representation of $\record{~}$ is \texttt{(|~|)}.
+\end{center}
+
+\noindent The \textsc{ascii} representation of $\record{x = a}$ is \texttt{(| x = a |)}.
A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field
$y$ of value $b$. The corresponding type is $\record{x \ty A\fs y \ty B}$,
-assuming $a \ty A$ and $b \ty B$.
-
-A record scheme like $\record{x = a\fs y = b\fs \more = more}$ contains fields
-$x$ and $y$ as before, but also possibly further fields as indicated by above
-``$\more$'' notation. We call ``$\more$'' the \emph{more part}; logically it
-is just a free variable. In the literature this is also referred to as
-\emph{row variable}. The more part of record schemes may be instantiated by
-zero or more further components. For example, above scheme might get
-instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = more'}$, where
-$more'$ refers to a different more part.
-
-Fixed records are special instances of record schemes, where $more$ is
-properly terminated by the $unit$ element $()$. Thus $\record{x = a\fs y =
- b}$ is just an abbreviation of $\record{x = a\fs y = b\fs \more = ()}$.
+assuming that $a \ty A$ and $b \ty B$.
+
+A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields
+$x$ and $y$ as before, but also possibly further fields as indicated by the
+``$\more$'' notation (which is actually part of the syntax). The improper
+field ``$\more$'' of a record scheme is called the \emph{more part}.
+Logically it is just a free variable, which is occasionally referred to as
+\emph{row variable} in the literature. The more part of a record scheme may
+be instantiated by zero or more further components. For example, above scheme
+might get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = m'}$,
+where $m'$ refers to a different more part. Fixed records are special
+instances of record schemes, where ``$\more$'' is properly terminated by the
+$() :: unit$ element. Actually, $\record{x = a\fs y = b}$ is just an
+abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.
\medskip
There are two key features that make extensible records in a simply typed
language like HOL feasible:
\begin{enumerate}
-\item the ``more'' part is internalized (as a free term or type variable),
-\item field names are externalized, i.e.\ cannot be reasoned about within the
- logic as first class values.
+\item the more part is internalised, as a free term or type variable,
+\item field names are externalised, they cannot be accessed within the logic
+ as first-class values.
\end{enumerate}
\medskip
-Records have to be defined explicitly, fixing their field names and types,
-and (optional) parent record scheme (see \S\ref{sec:HOL:record-def}).
-Afterwards, records may be formed using above syntax, while obeying the
-canonical order of fields according to the declaration hierarchy.
-
-The record package also provides several operations like selectors and updates
-(see \S\ref{sec:HOL:record-ops}, together with their characteristics properties
-(see \S\ref{sec:HOL:record-thms}).
-
-There is a simple example exhibiting most basic aspects of extensible records
-available. See theory \texttt{HOL/ex/Points} in the Isabelle sources.
+In Isabelle/HOL record types have to be defined explicitly, fixing their field
+names and types, and their (optional) parent record (see
+\S\ref{sec:HOL:record-def}). Afterwards, records may be formed using above
+syntax, while obeying the canonical order of fields as given by their
+declaration. The record package also provides several operations like
+selectors and updates (see \S\ref{sec:HOL:record-ops}), together with
+characteristic properties (see \S\ref{sec:HOL:record-thms}).
+
+There is an example theory demonstrating most basic aspects of extensible
+records (see theory \texttt{HOL/ex/Points} in the Isabelle sources).
\subsection{Defining records}\label{sec:HOL:record-def}
@@ -1617,6 +1619,7 @@
\begin{figure}[htbp]
\begin{rail}
record : 'record' typevarlist name '=' parent (field +);
+
parent : ( () | type '+');
field : name '::' type;
\end{rail}
@@ -1627,131 +1630,179 @@
A general \ttindex{record} specification is of the following form:
\[
\mathtt{record}~(\alpha@1, \dots, \alpha@n) \, t ~=~
- (\tau@1, \dots, \tau@m) \, s + c@1 :: \sigma@1 ~ \dots c@l :: \sigma@k
+ (\tau@1, \dots, \tau@m) \, s ~+~ c@1 :: \sigma@1 ~ \dots ~ c@l :: \sigma@l
\]
-where $\alpha@i$ are distinct type variables, and $\tau@i$, $\sigma@i$ types
-containing at most variables $\alpha@1, \dots, \alpha@n$; type constructor $t$
-has to be new, while $s$ specifies an existing one. Also, the $c@i$ have to
-be distinct fields names (which may be safely reused from other records).
-Note that there has to be at least one field.
+where $\vec\alpha@n$ are distinct type variables, and $\vec\tau@m$,
+$\vec\sigma@l$ are types containing at most variables from $\vec\alpha@n$.
+Type constructor $t$ has to be new, while $s$ has to specify an existing
+record type. Furthermore, the $\vec c@l$ have to be distinct field names.
+There has to be at least one field.
+
+In principle, field names may never be shared with other records. This is no
+actual restriction in practice, since $\vec c@l$ are internally declared
+within a separate name space qualified by the name $t$ of the record.
\medskip
-Above definition introduces a new record type $(\alpha@1, \dots, \alpha@n) \,
-t$ by extending an existing one $(\tau@1, \dots, \tau@m) \, s$ by new fields
-$c@1, \dots, c@n$. The parent record specification is optional. By omitting
-it, $(\alpha@1, \dots, \alpha@n) \,t$ becomes a root record which is not
-derived from any other one. The hierarchy of records declared within any
-theory forms a forest structure.
-
-The new type $(\alpha@1, \dots, \alpha@n) \, t$ is made an abbreviation for
-the fixed record type $\record{c@1 \ty \sigma@1\fs \dots\fs c@k \ty
- \sigma@k}$, and $(\alpha@1\fs \dots\fs \alpha@n\fs \mu) \, t_scheme$ is made
-an abbreviation for $\record{c@1 \ty \sigma@1\fs \dots\fs c@k \ty \sigma@k\fs
- \more \ty \mu}$.
+Above definition introduces a new record type $(\vec\alpha@n) \, t$ by
+extending an existing one $(\vec\tau@m) \, s$ by new fields $\vec c@l \ty
+\vec\sigma@l$. The parent record specification is optional, by omitting it
+$t$ becomes a \emph{root record}. The hierarchy of all records declared
+within a theory forms a forest structure, i.e.\ a set of trees, where any of
+these is rooted by some root record.
+
+For convenience, $(\vec\alpha@n) \, t$ is made a type abbreviation for the
+fixed record type $\record{\vec c@l \ty \vec\sigma@l}$, and $(\vec\alpha@n,
+\zeta) \, t_scheme$ is made an abbreviation for $\record{\vec c@l \ty
+ \vec\sigma@l\fs \more \ty \zeta}$.
+
+\medskip
+
+The following simple example defines a root record type $point$ with fields $x
+\ty nat$ and $y \ty nat$, and record type $cpoint$ by extending $point$ with
+an additional $colour$ component.
+
+\begin{ttbox}
+ record point =
+ x :: nat
+ y :: nat
+
+ record cpoint = point +
+ colour :: string
+\end{ttbox}
\subsection{Record operations}\label{sec:HOL:record-ops}
-Any record definition as above produces selectors, updates and derived
-constructors (make). To simplify the presentation we assume that $(\alpha@1,
-\dots, \alpha@n) \, t$ is a root record with fields $c@i \ty \sigma@i$.
-
-Selectors and updates are available for any field proper field and the
-pseudo-field $more$ as follows:
+Any record definition of the form presented above produces certain standard
+operations. Selectors and updates are provided for any field, including the
+improper one ``$more$''. There are also cumulative record constructor
+functions.
+
+To simplify the presentation below, we first assume that $(\vec\alpha@n) \, t$
+is a root record with fields $\vec c@l \ty \vec\sigma@l$.
+
+\medskip
+
+\textbf{Selectors} and \textbf{updates} are available for any field (including
+``$more$'') as follows:
\begin{matharray}{lll}
- c@i & \ty & (\alpha@1, \dots, \alpha@n, \mu) \, t_scheme \To \sigma@i \\
- c@i_update & \ty & \sigma@i \To (\alpha@1, \dots, \alpha@n, \mu) \, t_scheme \To
- (\alpha@1, \dots, \alpha@n, \mu) \, t_scheme \To
+ c@i & \ty & \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To \sigma@i \\
+ c@i_update & \ty & \sigma@i \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To
+ \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta}
\end{matharray}
-There is special syntax for updates: $r \, \record{x \asn a}$ abbreviates
-$x_update \, a \, r$. Repeated updates are also supported like $r \,
+There is some special syntax for updates: $r \, \record{x \asn a}$ abbreviates
+term $x_update \, a \, r$. Repeated updates are also supported: $r \,
\record{x \asn a} \, \record{y \asn b} \, \record{z \asn c}$ may be written as
$r \, \record{x \asn a\fs y \asn b\fs z \asn c}$. Note that because of
-postfix notation the order of fields printed is reverse in the actual term.
-This might be confusion under rare circumstances in conjunction with proof
-tools like ordered rewriting.
-
-Updates are just function applications, so fields may be freely permuted in
-the $\record{x \asn a\fs y \asn b}$ notation, as far as the logic is
-concerned. Thus commutativity of updates can be proven within the logic for
-any two fields, not as a general theorem (remember that fields are not
-first-class).
+postfix notation the order of fields shown here is reverse than in the actual
+term. This might lead to confusion in conjunction with proof tools like
+ordered rewriting.
+
+Since repeated updates are just function applications, fields may be freely
+permuted in $\record{x \asn a\fs y \asn b\fs z \asn c}$, as far as the logic
+is concerned. Thus commutativity of updates can be proven within the logic
+for any two fields, but not as a general theorem: fields are not first-class
+values.
+
+\medskip
+
+\textbf{Make} operations provide cumulative record constructor functions:
+\begin{matharray}{lll}
+ make & \ty & \vec\sigma@l \To \record{\vec c@l \ty \vec \sigma@l} \\
+ make_scheme & \ty & \vec\sigma@l \To
+ \zeta \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \\
+\end{matharray}
+\noindent
+These functions are curried. The corresponding definitions in terms of actual
+record terms are part of the standard simpset. Thus $point\dtt make\,a\,b$
+rewrites to $\record{x = a\fs y = b}$.
\medskip
-For convenience there are also derived record constructors as follows:
+Any of above selector, update and make operations are declared within a local
+name space prefixed by the name $t$ of the record. In case that different
+records share base names of fields, one has to qualify names explicitly (e.g.\
+$t\dtt c@i_update$). This is recommended especially for operations like
+$make$ or $update_more$ that always have the same base name. Just use $t\dtt
+make$ etc.\ to avoid confusion.
+
+\bigskip
+
+We reconsider the case of non-root records, which are derived of some parent
+record. In general, the latter may depend on another parent as well,
+resulting in a list of \emph{ancestor records}. Appending the lists of fields
+of all ancestors results in a certain field prefix. The record package
+automatically takes care of this by lifting operations over this context of
+ancestor fields. Assuming that $(\vec\alpha@n) \, t$ has ancestor fields
+$\vec d@k \ty \vec\rho@k$, selectors will get the following types:
\begin{matharray}{lll}
- make & \ty & \sigma@1 \To \dots \To \sigma@k \To
- (\alpha@1, \dots, \alpha@n) \, t \\
- make_scheme & \ty & \sigma@1 \To \dots \To \sigma@k \To \mu \To
- (\alpha@1, \dots, \alpha@n, \mu) \, t_scheme \\
+ c@i & \ty & \record{\vec d@k \ty \vec\rho@k, \vec c@l \ty \vec \sigma@l, \more \ty \zeta}
+ \To \sigma@i
\end{matharray}
-
-\medskip
-
-Any of these operations are declared within a local name space for $t$. In
-case that different records share field (base) names, one has to qualify
-explicitly, e.g.\ $t.c_update$. This is recommended especially for generic
-names like $make$, which should be rather $t.make$ to avoid confusion.
-
-\medskip
-
-Reconsider the case of records that are derived of some parent record. In
-general, the latter may depend on another parent as well, resulting in a list
-of ancestor records. Appending the lists of fields of all ancestors results
-in a certain field prefix. The Isabelle/HOL record package automatically
-takes care of this context of parent fields when defining selectors, updates
-etc.
+\noindent
+Update and make operations are analogous.
\subsection{Proof tools}\label{sec:HOL:record-thms}
-The record package provides the following proof rules for any record $t$:
+The record package provides the following proof rules for any record type $t$.
\begin{enumerate}
-
-\item standard conversions (selectors or updates applied to record constructor
- terms) are part of the standard simpset,
-\item inject equations of the form analogous to $((x, y) = (x', y')) \equiv
- x=x' \conj y=y'$ are made part of standard simpset and claset (via
- \texttt{addIffs}),
+\item Standard conversions (selectors or updates applied to record constructor
+ terms, make function definitions) are part of the standard simpset (via
+ \texttt{addsimps}).
+
+\item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'
+ \conj y=y'$ are made part of the standard simpset and claset (via
+ \texttt{addIffs}).
-\item a tactic for record field splitting (\ttindex{record_split_tac}) is made
- part of the standard claset (as sage wrapper); this is based on a rule like
- this: $(\all x PROP~P~x) \equiv (\all{a~b} PROP~P(a, b))$.
+\item A tactic for record field splitting (\ttindex{record_split_tac}) is made
+ part of the standard claset (via \texttt{addSWrapper}). This tactic is
+ based on rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a,
+ b))$ for any field.
\end{enumerate}
-The first two kinds of rules are also stored within the theory as $t.simps$
-and $t.iffs$, respectively.
-
-The example \texttt{HOL/ex/Points} demonstrates typical proofs concerning
-records. The basic idea is to make \ttindex{record_split_tac} expand
-quantified record variables and then simplify by the conversion rules. By
-using a combination of the simplifier and classical prover together with the
-default simpset and claset, record problems should be solved (e.g.\
-\texttt{Auto_tac} or \texttt{Force_tac}) with a single stroke.
+The first two kinds of rules are stored within the theory as $t\dtt simps$ and
+$t\dtt iffs$, respectively. In some situations it might be appropriate to
+expand the definitions of updates: $t\dtt updates$. Following a new trend in
+Isabelle system architecture, these names are \emph{not} bound at the {\ML}
+level, though.
+
+\medskip
+
+The example theory \texttt{HOL/ex/Points} demonstrates typical proofs
+concerning records. The basic idea is to make \ttindex{record_split_tac}
+expand quantified record variables and then simplify by the conversion rules.
+By using a combination of the simplifier and classical prover together with
+the default simpset and claset, record problems should be solved with a single
+stroke of \texttt{Auto_tac} or \texttt{Force_tac}.
\section{Datatype definitions}
\label{sec:HOL:datatype}
\index{*datatype|(}
-Inductive datatypes, similar to those of \ML, frequently appear in
-non-trivial applications of \HOL. In principle, such types could be
-defined by hand via \texttt{typedef} (see \S\ref{sec:typedef}), but
-this would be far too tedious. The \ttindex{datatype} definition
-package of \HOL\ automates such chores. It generates and proves
-freeness theorems and induction rules, as well as theorems for
-recursion and case combinators from a very simple description of the new type
-provided by the user.
+Inductive datatypes, similar to those of \ML, frequently appear in actual
+applications of Isabelle/HOL. In principle, such types could be defined by
+hand via \texttt{typedef} (see \S\ref{sec:typedef}), but this would be far too
+tedious. The \ttindex{datatype} definition package of \HOL\ automates such
+chores. It generates an appropriate \texttt{typedef} based on a least
+fixed-point construction, and proves freeness theorems and induction rules, as
+well as theorems for recursion and case combinators. The user just has to
+give a simple specification of new inductive types using a notation similar to
+{\ML} or Haskell.
+
+The current datatype package can handle both mutual and indirect recursion.
+It also offers to represent existing types as datatypes giving the advantage
+of a more uniform view on standard theories.
\subsection{Basics}
\label{subsec:datatype:basics}
-The general \HOL\ \texttt{datatype} definition is of the following form:
+A general \texttt{datatype} definition is of the following form:
\[
\begin{array}{llcl}
\mathtt{datatype} & (\alpha@1,\ldots,\alpha@h)t@1 & = &
@@ -1766,9 +1817,9 @@
where $\alpha@i$ are type variables, $C^j@i$ are distinct constructor
names and $\tau^j@{i,i'}$ are {\em admissible} types containing at
most the type variables $\alpha@1, \ldots, \alpha@h$. A type $\tau$
-occurring in a \texttt{datatype} definition is {\em admissible} if
+occurring in a \texttt{datatype} definition is {\em admissible} iff
\begin{itemize}
-\item $\tau$ is non-recursive, i.e. $\tau$ does not contain any of the
+\item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the
newly defined type constructors $t@1,\ldots,t@n$, or
\item $\tau = (\alpha@1,\ldots,\alpha@h)t@{j'}$ where $1 \leq j' \leq n$, or
\item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is
@@ -1780,8 +1831,8 @@
\[
(\ldots,\ldots ~ (\alpha@1,\ldots,\alpha@h)t@{j'} ~ \ldots,\ldots)t'
\]
-this is called a {\em nested} occurrence. A very simple example of a datatype
-is the type {\tt list}, which can be defined by
+this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple
+example of a datatype is the type {\tt list}, which can be defined by
\begin{ttbox}
datatype 'a list = Nil
| Cons 'a ('a list)
@@ -1805,26 +1856,26 @@
\end{ttbox}
is an example for a datatype with nested recursion.
-Types in HOL must be nonempty. Each of the new datatypes
-$(\alpha@1,\ldots,\alpha@h)t@j$ with $1 \le j \le n$ is nonempty iff
-it has a constructor $C^j@i$ with the following property: For all
-argument types $\tau^j@{i,i'}$ of the form $(\alpha@1,\ldots,\alpha@h)t@{j'}$
-the datatype $(\alpha@1,\ldots,\alpha@h)t@{j'}$ is nonempty.
-
-If there are no nested occurrences of the newly defined datatypes,
-obviously at least one of the newly defined datatypes
-$(\alpha@1,\ldots,\alpha@h)t@j$ must have a constructor $C^j@i$ without
-recursive arguments -- a so-called {\em base case} -- to ensure that
-the new types are nonempty. If there are nested occurrences, a datatype
-can even be nonempty without having a base case itself: Since {\tt list}
-is a nonempty datatype, {\tt datatype t = C (t list)} is nonempty
-as well.
-
-The constructors are automatically defined as functions of their respective
-type:
+\medskip
+
+Types in HOL must be non-empty. Each of the new datatypes
+$(\alpha@1,\ldots,\alpha@h)t@j$ with $1 \le j \le n$ is non-empty iff it has a
+constructor $C^j@i$ with the following property: for all argument types
+$\tau^j@{i,i'}$ of the form $(\alpha@1,\ldots,\alpha@h)t@{j'}$ the datatype
+$(\alpha@1,\ldots,\alpha@h)t@{j'}$ is non-empty.
+
+If there are no nested occurrences of the newly defined datatypes, obviously
+at least one of the newly defined datatypes $(\alpha@1,\ldots,\alpha@h)t@j$
+must have a constructor $C^j@i$ without recursive arguments, a \emph{base
+ case}, to ensure that the new types are non-empty. If there are nested
+occurrences, a datatype can even be non-empty without having a base case
+itself. Since {\tt list} is a non-empty datatype, {\tt datatype t = C (t
+ list)} is non-empty as well.
+
+The datatype constructors are automatically defined as functions of their
+respective type:
\[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \]
-These functions have certain {\em freeness} properties --- they are
-distinct:
+These functions have certain {\em freeness} properties. They are distinct:
\[
C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad
\mbox{for all}~ i \neq i'.
@@ -1834,10 +1885,9 @@
(C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) =
(x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i})
\]
-Because the number of inequalities is quadratic in the number of
-constructors, a different representation is used if there are $7$ or
-more of them. In that case every constructor term is mapped to a
-natural number:
+Because the number of distinctness inequalities is quadratic in the number of
+constructors, a different representation is used if there are $7$ or more of
+them. In that case every constructor term is mapped to a natural number:
\[
t@j_ord \, (C^j@i \, x@1 \, \dots \, x@{m^j@i}) = i - 1
\]
@@ -1846,8 +1896,8 @@
t@j_ord \, x \neq t@j_ord \, y \Imp x \neq y.
\]
-\medskip For datatypes without nested recursion, the following
-structural induction rule is provided:
+\medskip The datatype package also provides structural induction rules. For
+datatypes without nested recursion, this is of the following form:
\[
\infer{P@1~x@1 \wedge \dots \wedge P@n~x@n}
{\begin{array}{lcl}
@@ -1883,25 +1933,27 @@
\tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\}
\end{array}
\]
-i.e.\ the properties $P@j$ can be assumed for all recursive arguments. For
-datatypes with nested recursion such as {\tt term}, things are a bit more
-complicated. Isabelle's datatype package unfolds the definition
+i.e.\ the properties $P@j$ can be assumed for all recursive arguments.
+
+For datatypes with nested recursion, such as the {\tt term} example from
+above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds
+a definition like
\begin{ttbox}
datatype ('a, 'b) term = Var 'a
| App 'b ((('a, 'b) term) list)
\end{ttbox}
-to the equivalent definition
+to an equivalent definition without nesting:
\begin{ttbox}
datatype ('a, 'b) term = Var
| App 'b (('a, 'b) term_list)
and ('a, 'b) term_list = Nil'
| Cons' (('a,'b) term) (('a,'b) term_list)
\end{ttbox}
-having no nestings. However, note that the type {\tt ('a,'b) term_list}
-and the constructors {\tt Nil'} and {\tt Cons'} are not really introduced by the datatype
-package. Instead, you can simply use the -- isomorphic -- type {\tt (('a, 'b) term) list}
-and the constructors {\tt Nil} and {\tt Cons}. Thus, the structural induction rule
-for {\tt term} has the form
+Note however, that the type {\tt ('a,'b) term_list} and the constructors {\tt
+ Nil'} and {\tt Cons'} are not really introduced. One can directly work the
+original (isomorphic) type {\tt (('a, 'b) term) list} and its existing
+constructors {\tt Nil} and {\tt Cons}. Thus, the structural induction rule for
+{\tt term} gets the form
\[
\infer{P@1~x@1 \wedge P@2~x@2}
{\begin{array}{l}
@@ -1914,9 +1966,10 @@
Note that there are two predicates $P@1$ and $P@2$, one for the type {\tt ('a,'b) term}
and one for the type {\tt (('a, 'b) term) list}.
-\medskip
-For convenience, the following additional constructions are predefined for
-each datatype.
+\medskip In principle, inductive types are already fully determined by
+freeness and structural induction. For convenience in actual applications,
+the following derived constructions are automatically provided for any
+datatype.
\subsubsection{The \sdx{case} construct}
@@ -1931,9 +1984,9 @@
where the $x@{i,j}$ are either identifiers or nested tuple patterns as in
\S\ref{subsec:prod-sum}.
\begin{warn}
-In contrast to \ML, {\em all} constructors must be present, their order is
-fixed, and nested patterns are not supported (with the exception of tuples).
-Violating this restriction results in strange error messages.
+ All constructors must be present, their order is fixed, and nested patterns
+ are not supported (with the exception of tuples). Violating this
+ restriction results in strange error messages.
\end{warn}
To perform case distinction on a goal containing a \texttt{case}-construct,
@@ -1954,9 +2007,9 @@
\subsubsection{The function \cdx{size}}\label{sec:HOL:size}
-Theory \texttt{Arith} declares an overloaded function \texttt{size} of type
+Theory \texttt{Arith} declares a generic function \texttt{size} of type
$\alpha\To nat$. Each datatype defines a particular instance of \texttt{size}
-according to the following scheme:
+by overloading according to the following scheme:
\[
size(C^j@i~x@1~\dots~x@{m^j@i}) = \!
\left\{
@@ -1971,24 +2024,25 @@
\end{array}
\right.
\]
-where $Rec^j@i$ is defined above. Viewing datatypes as generalized trees, the
+where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the
size of a leaf is 0 and the size of a node is the sum of the sizes of its
-subtrees $+1$.
+subtrees ${}+1$.
\subsection{Defining datatypes}
-Datatypes are defined in a theory definition file using the keyword
-{\tt datatype}. The definition following this must conform to the
-syntax of {\em typedecl} specified in Fig.~\ref{datatype-grammar} and
-must obey the rules in the previous section. As a result the theory is
-extended with the new types, the constructors, and the theorems listed
-in the previous section.
+The theory syntax for datatype definitions is shown in
+Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype
+definition has to obey the rules stated in the previous section. As a result
+the theory is extended with the new types, the constructors, and the theorems
+listed in the previous section.
\begin{figure}
\begin{rail}
-typedecl : ( type '=' (cons + '|') ) + 'and'
+datatype : 'datatype' typedecls;
+
+typedecls: ( newtype '=' (cons + '|') ) + 'and'
;
-type : typevarlist id ( () | '(' infix ')' )
+newtype : typevarlist id ( () | '(' infix ')' )
;
cons : name (argtype *) ( () | ( '(' mixfix ')' ) )
;
@@ -1999,26 +2053,22 @@
\label{datatype-grammar}
\end{figure}
-\begin{warn}
- Every theory containing a datatype declaration must be based, directly or
- indirectly, on the theory \texttt{Datatype}, if necessary by including it
- explicitly as a parent.
-\end{warn}
-
-Most of the theorems about the datatypes become part of the default simpset
-and you never need to see them again because the simplifier applies them
-automatically. Only induction is invoked by hand:
+Most of the theorems about datatypes become part of the default simpset and
+you never need to see them again because the simplifier applies them
+automatically. Only induction or exhaustion are usually invoked by hand.
\begin{ttdescription}
\item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$]
applies structural induction on variable $x$ to subgoal $i$, provided the
type of $x$ is a datatype.
-\item[\ttindexbold{mutual_induct_tac} {\tt["}$x@1${\tt",}$\ldots${\tt,"}$x@n${\tt"]} $i$]
- applies simultaneous structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$.
- This is needed to prove properties of mutually recursive datatypes such as {\tt aexp} and
- {\tt bexp} or datatypes with nested recursion such as {\tt term}.
+\item[\ttindexbold{mutual_induct_tac}
+ {\tt["}$x@1${\tt",}$\ldots${\tt,"}$x@n${\tt"]} $i$] applies simultaneous
+ structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This
+ is the canonical way to prove properties of mutually recursive datatypes
+ such as {\tt aexp} and {\tt bexp}, or datatypes with nested recursion such as
+ {\tt term}.
\end{ttdescription}
In some cases, induction is overkill and a case distinction over all
-constructors of the datatype suffices:
+constructors of the datatype suffices.
\begin{ttdescription}
\item[\ttindexbold{exhaust_tac} {\tt"}$u${\tt"} $i$]
performs an exhaustive case analysis for the term $u$ whose type
@@ -2027,18 +2077,17 @@
contain the additional assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for
$i'=1$, $\dots$,~$k@j$.
\end{ttdescription}
-\begin{warn}
- Induction is only allowed on free variables that should not occur among
- the premises of the subgoal. Exhaustion works for arbitrary terms.
-\end{warn}
+
+Note that induction is only allowed on free variables that should not occur
+among the premises of the subgoal. Exhaustion applies to arbitrary terms.
+
\bigskip
-For the technically minded, we give a more detailed description.
-Reading the theory file produces an \ML\ structure which, in addition to the
-usual components, contains a structure named $t$ for each datatype $t$
-defined in the file. Each structure $t$ contains the following
-elements:
+For the technically minded, we exhibit some more details. Processing the
+theory file produces an \ML\ structure which, in addition to the usual
+components, contains a structure named $t$ for each datatype $t$ defined in
+the file. Each structure $t$ contains the following elements:
\begin{ttbox}
val distinct : thm list
val inject : thm list
@@ -2060,41 +2109,45 @@
In case of mutually recursive datatypes, {\tt recs}, {\tt size}, {\tt induct}
and {\tt simps} are contained in a separate structure named $t@1_\ldots_t@n$.
-\subsection{Representing types as datatypes}
-For technical reasons, some types such as {\tt nat}, {\tt *}, {\tt +},
-{\tt bool} and {\tt unit} are not directly defined in a {\tt datatype}
-section. To be able to use the tactics {\tt induct_tac} and
-{\tt exhaust_tac} and to define functions by primitive recursion
-on these types, they have to be represented as datatypes.
-This is done by specifying an induction rule, as well as theorems
-stating the distinctness and injectivity of constructors
-in a {\tt rep_datatype} section, e.g.
+
+\subsection{Representing existing types as datatypes}
+
+For foundational reasons, some basic types such as {\tt nat}, {\tt *}, {\tt
+ +}, {\tt bool} and {\tt unit} are not defined in a {\tt datatype} section,
+but by more primitive means using \texttt{typedef}. To be able to use the
+tactics {\tt induct_tac} and {\tt exhaust_tac} and to define functions by
+primitive recursion on these types, such types may be represented as actual
+datatypes. This is done by specifying an induction rule, as well as theorems
+stating the distinctness and injectivity of constructors in a {\tt
+ rep_datatype} section. For type \texttt{nat} this works as follows:
\begin{ttbox}
rep_datatype nat
distinct Suc_not_Zero, Zero_not_Suc
inject Suc_Suc_eq
induct nat_induct
\end{ttbox}
-The datatype package automatically derives additional theorems
-for recursion and case combinators from these rules.
+The datatype package automatically derives additional theorems for recursion
+and case combinators from these rules. Any of the basic HOL types mentioned
+above are represented as datatypes. Try an induction on \texttt{bool}
+today.
+
\subsection{Examples}
\subsubsection{The datatype $\alpha~mylist$}
-We want to define the type $\alpha~mylist$.\footnote{This is just an
- example, there is already a list type in \HOL, of course.} To do
-this we have to build a new theory that contains the type definition.
-We start from the theory \texttt{Datatype}.
+We want to define a type $\alpha~mylist$. To do this we have to build a new
+theory that contains the type definition. We start from the theory
+\texttt{Datatype} instead of \texttt{Main} in order to avoid clashes with the
+\texttt{List} theory of Isabelle/HOL.
\begin{ttbox}
MyList = Datatype +
datatype 'a mylist = Nil | Cons 'a ('a mylist)
end
\end{ttbox}
-After loading the theory (with \verb$use_thy "MyList"$), we can prove
-$Cons~x~xs\neq xs$. To ease the induction applied below, we state the
-goal with $x$ quantified at the object-level. This will be stripped
-later using \ttindex{qed_spec_mp}.
+After loading the theory, we can prove $Cons~x~xs\neq xs$, for example. To
+ease the induction applied below, we state the goal with $x$ quantified at the
+object-level. This will be stripped later using \ttindex{qed_spec_mp}.
\begin{ttbox}
Goal "!x. Cons x xs ~= xs";
{\out Level 0}
@@ -2111,9 +2164,9 @@
{\out ! x. Cons x mylist ~= mylist ==>}
{\out ! x. Cons x (Cons a mylist) ~= Cons a mylist}
\end{ttbox}
-The first subgoal can be proved using the simplifier.
-Isabelle has already added the freeness properties of lists to the
-default simplification set.
+The first subgoal can be proved using the simplifier. Isabelle/HOL has
+already added the freeness properties of lists to the default simplification
+set.
\begin{ttbox}
by (Simp_tac 1);
{\out Level 2}
@@ -2152,8 +2205,7 @@
Cons 'a ('a mylist) (infixr "#" 70)
end
\end{ttbox}
-Now the theorem in the previous example can be written \verb|x#xs ~= xs|. The
-proof is the same.
+Now the theorem in the previous example can be written \verb|x#xs ~= xs|.
\subsubsection{A datatype for weekdays}
@@ -2180,10 +2232,10 @@
\section{Recursive function definitions}\label{sec:HOL:recursive}
\index{recursive functions|see{recursion}}
-Isabelle/HOL provides two means of declaring recursive functions.
-\begin{itemize}
+Isabelle/HOL provides two main mechanisms of defining recursive functions.
+\begin{enumerate}
\item \textbf{Primitive recursion} is available only for datatypes, and it is
- highly restrictive. Recursive calls are only allowed on the argument's
+ somewhat restrictive. Recursive calls are only allowed on the argument's
immediate constituents. On the other hand, it is the form of recursion most
often wanted, and it is easy to use.
@@ -2196,19 +2248,15 @@
\footnote{This facility is based on Konrad Slind's TFL
package~\cite{slind-tfl}. Thanks are due to Konrad for implementing TFL
and assisting with its installation.}
-\end{itemize}
-
-
-A theory file may contain any number of recursive function definitions, which
-may be intermixed with other declarations. Every recursive function must
-already have been declared as a constant.
-
-These declarations do not assert new axioms. Instead, they define the
-function using a recursion operator. Both HOL and ZF derive the theory of
-well-founded recursion from first principles~\cite{paulson-set-II}. Primitive
-recursion over some datatype relies on the recursion operator provided by the
-datatype package. With either form of function definition, Isabelle proves
-the desired recursion equations as theorems.
+\end{enumerate}
+
+Following good HOL tradition, these declarations do not assert arbitrary
+axioms. Instead, they define the function using a recursion operator. Both
+HOL and ZF derive the theory of well-founded recursion from first
+principles~\cite{paulson-set-II}. Primitive recursion over some datatype
+relies on the recursion operator provided by the datatype package. With
+either form of function definition, Isabelle proves the desired recursion
+equations as theorems.
\subsection{Primitive recursive functions}
@@ -2216,38 +2264,38 @@
\index{recursion!primitive|(}
\index{*primrec|(}
-Datatypes come with a uniform way of defining functions, {\bf
- primitive recursion}. In principle, one can define
-primitive recursive functions by asserting their reduction rules as
-new axioms. Here is an example:
+Datatypes come with a uniform way of defining functions, {\bf primitive
+ recursion}. In principle, one could introduce primitive recursive functions
+by asserting their reduction rules as new axioms. Here is a counter-example
+(you should not do such things yourself):
\begin{ttbox}
-Append = MyList +
-consts app :: ['a mylist, 'a mylist] => 'a mylist
+Append = Main +
+consts app :: ['a list, 'a list] => 'a list
rules
app_Nil "app [] ys = ys"
app_Cons "app (x#xs) ys = x#app xs ys"
end
\end{ttbox}
-But asserting axioms brings the danger of accidentally asserting an
-inconsistency, as in \verb$app [] ys = us$.
+But asserting axioms brings the danger of accidentally asserting nonsense, as
+in \verb$app [] ys = us$.
The \ttindex{primrec} declaration is a safe means of defining primitive
recursive functions on datatypes:
\begin{ttbox}
-Append = MyList +
-consts app :: ['a mylist, 'a mylist] => 'a mylist
+Append = Main +
+consts app :: ['a list, 'a list] => 'a list
primrec
"app [] ys = ys"
"app (x#xs) ys = x#app xs ys"
end
\end{ttbox}
Isabelle will now check that the two rules do indeed form a primitive
-recursive definition, preserving consistency. For example
+recursive definition. For example
\begin{ttbox}
primrec
"app [] ys = us"
\end{ttbox}
-is rejected with an error message \texttt{Extra variables on rhs}.
+is rejected with an error message ``\texttt{Extra variables on rhs}''.
\bigskip
@@ -2258,13 +2306,13 @@
\end{ttbox}
where \textit{reduction rules} specify one or more equations of the form
\[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,
-\dots \, z@n = r \] such that $C$ is a constructor of the datatype,
-$r$ contains only the free variables on the left-hand side, and all
-recursive calls in $r$ are of the form $f \, \dots \, y@i \, \dots$
-for some $i$. There must be at most one reduction rule for each
-constructor. The order is immaterial. For missing constructors,
-the function is defined to return an arbitrary value.
-Also note that all reduction rules are added to the default simpset.
+\dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$
+contains only the free variables on the left-hand side, and all recursive
+calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. There
+must be at most one reduction rule for each constructor. The order is
+immaterial. For missing constructors, the function is defined to return a
+default value. Also note that all reduction rules are added to the default
+simpset.
If you would like to refer to some rule by name, then you must prefix
the rule with an identifier. These identifiers, like those in the
@@ -2272,8 +2320,8 @@
The primitive recursive function can have infix or mixfix syntax:
\begin{ttbox}\underscoreon
-Append = MyList +
-consts "@" :: ['a mylist, 'a mylist] => 'a mylist (infixr 60)
+Append = List +
+consts "@" :: ['a list, 'a list] => 'a list (infixr 60)
primrec
"[] @ ys = ys"
"(x#xs) @ ys = x#(xs @ ys)"
@@ -2281,7 +2329,7 @@
\end{ttbox}
The reduction rules for {\tt\at} become part of the default simpset, which
-leads to short proofs:
+leads to short proof scripts:
\begin{ttbox}\underscoreon
Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
by (induct\_tac "xs" 1);
@@ -2337,8 +2385,8 @@
\end{ttbox}
In textbooks about semantics one often finds {\em substitution theorems},
which express the relationship between substitution and evaluation. For
-{'a aexp} and {'a bexp}, we can prove such a theorem by mutual induction,
-followed by simplification:
+\texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual
+induction, followed by simplification:
\begin{ttbox}
Goal
"eval_aexp env (subst_aexp (Var(v := a')) a) =
@@ -2370,10 +2418,9 @@
"subst_term_list f (t # ts) =
subst_term f t # subst_term_list f ts"
\end{ttbox}
-Since datatypes with nested recursion are unfolded, the recursion scheme
-follows the structure of the unfolded definition of type {\tt term}
-shown in \S\ref{subsec:datatype:basics}. To prove properties of this
-substitution function, mutual induction is needed:
+The recursion scheme follows the structure of the unfolded definition of type
+{\tt term} shown in \S\ref{subsec:datatype:basics}. To prove properties of
+this substitution function, mutual induction is needed:
\begin{ttbox}
Goal
"(subst_term ((subst_term f1) o f2) t) =
@@ -2414,26 +2461,27 @@
With \texttt{recdef}, function definitions may be incomplete, and patterns may
overlap, as in functional programming. The \texttt{recdef} package
disambiguates overlapping patterns by taking the order of rules into account.
-For missing patterns, the function is defined to return an arbitrary value.
-For example, here is a declaration of the list function \cdx{hd}:
-\begin{ttbox}
-consts hd :: 'a list => 'a
-recdef hd "\{\}"
- "hd (x#l) = x"
-\end{ttbox}
-Because this function is not recursive, we may supply the empty well-founded
-relation, $\{\}$.
+For missing patterns, the function is defined to return a default value.
+
+%For example, here is a declaration of the list function \cdx{hd}:
+%\begin{ttbox}
+%consts hd :: 'a list => 'a
+%recdef hd "\{\}"
+% "hd (x#l) = x"
+%\end{ttbox}
+%Because this function is not recursive, we may supply the empty well-founded
+%relation, $\{\}$.
The well-founded relation defines a notion of ``smaller'' for the function's
argument type. The relation $\prec$ is \textbf{well-founded} provided it
admits no infinitely decreasing chains
\[ \cdots\prec x@n\prec\cdots\prec x@1. \]
-If the function's argument has type~$\tau$, then $\prec$ should be a relation
+If the function's argument has type~$\tau$, then $\prec$ has to be a relation
over~$\tau$: it must have type $(\tau\times\tau)set$.
-Proving well-foundedness can be tricky, so {\HOL} provides a collection of
-operators for building well-founded relations. The package recognizes these
-operators and automatically proves that the constructed relation is
+Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection
+of operators for building well-founded relations. The package recognises
+these operators and automatically proves that the constructed relation is
well-founded. Here are those operators, in order of importance:
\begin{itemize}
\item \texttt{less_than} is ``less than'' on the natural numbers.
@@ -2446,7 +2494,7 @@
called a \textbf{measure function}. Recall that \texttt{size} is overloaded
and is defined on all datatypes (see \S\ref{sec:HOL:size}).
-\item $\mathop{\mathtt{inv_image}} f\;R$ is a generalization of
+\item $\mathop{\mathtt{inv_image}} f\;R$ is a generalisation of
\texttt{measure}. It specifies a relation such that $x\prec y$ iff $f(x)$
is less than $f(y)$ according to~$R$, which must itself be a well-founded
relation.
@@ -2485,7 +2533,7 @@
\item \textit{congruence rules} are required only in highly exceptional
circumstances.
-\item the \textit{simplification set} is used to prove that the supplied
+\item The \textit{simplification set} is used to prove that the supplied
relation is well-founded. It is also used to prove the \textbf{termination
conditions}: assertions that arguments of recursive calls decrease under
\textit{rel}. By default, simplification uses \texttt{simpset()}, which
@@ -2504,21 +2552,20 @@
as a list of theorems.
\end{itemize}
-With the definition of \texttt{gcd} shown above, Isabelle is unable to prove
-one termination condition. It remains as a precondition of the recursion
-theorems.
+With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to
+prove one termination condition. It remains as a precondition of the
+recursion theorems.
\begin{ttbox}
gcd.rules;
{\out ["! m n. n ~= 0 --> m mod n < n}
{\out ==> gcd (?m, ?n) = (if ?n = 0 then ?m else gcd (?n, ?m mod ?n))"] }
{\out : thm list}
\end{ttbox}
-The theory \texttt{Primes} (on the examples directory \texttt{HOL/ex})
-illustrates how to prove termination conditions afterwards. The function
-\texttt{Tfl.tgoalw} is like the standard function \texttt{goalw}, which sets
-up a goal to prove, but its argument should be the identifier
-$f$\texttt{.rules} and its effect is to set up a proof of the termination
-conditions:
+The theory \texttt{HOL/ex/Primes} illustrates how to prove termination
+conditions afterwards. The function \texttt{Tfl.tgoalw} is like the standard
+function \texttt{goalw}, which sets up a goal to prove, but its argument
+should be the identifier $f$\texttt{.rules} and its effect is to set up a
+proof of the termination conditions:
\begin{ttbox}
Tfl.tgoalw thy [] gcd.rules;
{\out Level 0}
@@ -2527,12 +2574,12 @@
\end{ttbox}
This subgoal has a one-step proof using \texttt{simp_tac}. Once the theorem
is proved, it can be used to eliminate the termination conditions from
-elements of \texttt{gcd.rules}. Theory \texttt{Unify} on directory
-\texttt{HOL/Subst} is a much more complicated example of this process, where
-the termination conditions can only be proved by complicated reasoning
-involving the recursive function itself.
-
-Isabelle can prove the \texttt{gcd} function's termination condition
+elements of \texttt{gcd.rules}. Theory \texttt{HOL/Subst/Unify} is a much
+more complicated example of this process, where the termination conditions can
+only be proved by complicated reasoning involving the recursive function
+itself.
+
+Isabelle/HOL can prove the \texttt{gcd} function's termination condition
automatically if supplied with the right simpset.
\begin{ttbox}
recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"
@@ -2540,7 +2587,7 @@
"gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
\end{ttbox}
-A \texttt{recdef} definition also returns an induction rule specialized for
+A \texttt{recdef} definition also returns an induction rule specialised for
the recursive function. For the \texttt{gcd} function above, the induction
rule is
\begin{ttbox}
@@ -2549,8 +2596,8 @@
\end{ttbox}
This rule should be used to reason inductively about the \texttt{gcd}
function. It usually makes the induction hypothesis available at all
-recursive calls, leading to very direct proofs. If any termination
-conditions remain unproved, they will be additional premises of this rule.
+recursive calls, leading to very direct proofs. If any termination conditions
+remain unproved, they will become additional premises of this rule.
\index{recursion!general|)}
\index{*recdef|)}
@@ -2566,7 +2613,7 @@
evaluation relation. Dually, a {\bf coinductive definition} specifies the
greatest set~$R$ consistent with given rules. (Every element of~$R$ can be
seen as arising by applying a rule to elements of~$R$.) An important example
-is using bisimulation relations to formalize equivalence of processes and
+is using bisimulation relations to formalise equivalence of processes and
infinite data structures.
A theory file may contain any number of inductive and coinductive
@@ -2578,14 +2625,14 @@
proves some theorems. Each definition creates an \ML\ structure, which is a
substructure of the main theory structure.
-This package is derived from the \ZF\ one, described in a separate
+This package is related to the \ZF\ one, described in a separate
paper,%
\footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
distributed with Isabelle.} %
which you should refer to in case of difficulties. The package is simpler
-than \ZF's thanks to \HOL's automatic type-checking. The types of the
-(co)inductive sets determine the domain of the fixedpoint definition, and the
-package does not use inference rules for type-checking.
+than \ZF's thanks to \HOL's extra-logical automatic type-checking. The types
+of the (co)inductive sets determine the domain of the fixedpoint definition,
+and the package does not have to use inference rules for type-checking.
\subsection{The result structure}
@@ -2615,7 +2662,7 @@
rule \texttt{induct}. For a
coinductive definition, it contains the rule \verb|coinduct|.
-Figure~\ref{def-result-fig} summarizes the two result signatures,
+Figure~\ref{def-result-fig} summarises the two result signatures,
specifying the types of all these components.
\begin{figure}
@@ -2630,21 +2677,21 @@
val mk_cases : thm list -> string -> thm
{\it(Inductive definitions only)}
val induct : thm
-{\it(Coinductive definitions only)}
-val coinduct : thm
+{\it(coinductive definitions only)}
+val coinduct : thm
end
\end{ttbox}
\hrule
-\caption{The result of a (co)inductive definition} \label{def-result-fig}
+\caption{The {\ML} result of a (co)inductive definition} \label{def-result-fig}
\end{figure}
\subsection{The syntax of a (co)inductive definition}
An inductive definition has the form
\begin{ttbox}
-inductive \textit{inductive sets}
- intrs \textit{introduction rules}
- monos \textit{monotonicity theorems}
- con_defs \textit{constructor definitions}
+inductive {\it inductive sets}
+ intrs {\it introduction rules}
+ monos {\it monotonicity theorems}
+ con_defs {\it constructor definitions}
\end{ttbox}
A coinductive definition is identical, except that it starts with the keyword
{\tt coinductive}.
@@ -2668,14 +2715,6 @@
appearing in the introduction rules. In most cases it can be omitted.
\end{itemize}
-The package has a few notable restrictions:
-\begin{itemize}
-\item The theory must separately declare the recursive sets as
- constants.
-
-\item The names of the recursive sets should be alphanumeric identifiers.
-\end{itemize}
-
\subsection{Example of an inductive definition}
Two declarations, included in a theory file, define the finite powerset
@@ -2710,11 +2749,11 @@
monos Pow_mono
end
\end{ttbox}
-The \HOL{} distribution contains many other inductive definitions.
-Simple examples are collected on subdirectory \texttt{Induct}. The
-theory \texttt{HOL/Induct/LList.thy} contains coinductive definitions.
-Larger examples may be found on other subdirectories, such as {\tt
- IMP}, \texttt{Lambda} and \texttt{Auth}.
+The Isabelle distribution contains many other inductive definitions. Simple
+examples are collected on subdirectory \texttt{HOL/Induct}. The theory
+\texttt{HOL/Induct/LList} contains coinductive definitions. Larger examples
+may be found on other subdirectories of \texttt{HOL}, such as {\tt IMP},
+\texttt{Lambda} and \texttt{Auth}.
\index{*coinductive|)} \index{*inductive|)}
--- a/doc-src/Logics/logics.ind Sat Oct 24 17:16:20 1998 +0200
+++ b/doc-src/Logics/logics.ind Sat Oct 24 20:22:45 1998 +0200
@@ -1,960 +1,960 @@
\begin{theindex}
- \item {\tt !} symbol, 60, 62, 69, 70, 82
- \item {\tt[]} symbol, 82
- \item {\tt\#} symbol, 82
- \item {\tt\#*} symbol, 48, 136
- \item {\tt\#+} symbol, 48, 136
- \item {\tt\#-} symbol, 48
- \item {\tt\&} symbol, 7, 60, 113
- \item {\tt *} symbol, 27, 61, 79, 127
- \item {\tt *} type, 77
- \item {\tt +} symbol, 44, 61, 79, 127
- \item {\tt +} type, 77
- \item {\tt -} symbol, 26, 61, 79, 136
- \item {\tt -->} symbol, 7, 60, 113, 127
- \item {\tt ->} symbol, 27
- \item {\tt -``} symbol, 26
- \item {\tt :} symbol, 26, 68
- \item {\tt <} constant, 80
- \item {\tt <} symbol, 79
- \item {\tt <->} symbol, 7, 113
- \item {\tt <=} constant, 80
- \item {\tt <=} symbol, 26, 68
- \item {\tt =} symbol, 7, 60, 113, 127
- \item {\tt ?} symbol, 60, 62, 69, 70
- \item {\tt ?!} symbol, 60
- \item {\tt\at} symbol, 60, 82
- \item {\tt `} symbol, 26, 127
- \item {\tt ``} symbol, 26, 68
- \item \verb'{}' symbol, 68
- \item {\tt |} symbol, 7, 60, 113
- \item {\tt |-|} symbol, 136
+ \item {\tt !} symbol, 52, 54, 59, 60, 71
+ \item {\tt[]} symbol, 71
+ \item {\tt\#} symbol, 71
+ \item {\tt\#*} symbol, 41, 118
+ \item {\tt\#+} symbol, 41, 118
+ \item {\tt\#-} symbol, 41
+ \item {\tt\&} symbol, 5, 52, 98
+ \item {\tt *} symbol, 23, 53, 69, 109
+ \item {\tt *} type, 66
+ \item {\tt +} symbol, 37, 53, 69, 109
+ \item {\tt +} type, 66
+ \item {\tt -} symbol, 22, 53, 69, 118
+ \item {\tt -->} symbol, 5, 52, 98, 109
+ \item {\tt ->} symbol, 23
+ \item {\tt -``} symbol, 22
+ \item {\tt :} symbol, 22, 58
+ \item {\tt <} constant, 68
+ \item {\tt <} symbol, 69
+ \item {\tt <->} symbol, 5, 98
+ \item {\tt <=} constant, 68
+ \item {\tt <=} symbol, 22, 58
+ \item {\tt =} symbol, 5, 52, 98, 109
+ \item {\tt ?} symbol, 52, 54, 59, 60
+ \item {\tt ?!} symbol, 52
+ \item {\tt\at} symbol, 52, 71
+ \item {\tt `} symbol, 22, 109
+ \item {\tt ``} symbol, 22, 58
+ \item \verb'{}' symbol, 58
+ \item {\tt |} symbol, 5, 52, 98
+ \item {\tt |-|} symbol, 118
\indexspace
- \item {\tt 0} constant, 26, 79, 125
+ \item {\tt 0} constant, 22, 69, 108
\indexspace
- \item {\tt absdiff_def} theorem, 136
- \item {\tt add_assoc} theorem, 136
- \item {\tt add_commute} theorem, 136
- \item {\tt add_def} theorem, 48, 136
- \item {\tt add_inverse_diff} theorem, 136
- \item {\tt add_mp_tac}, \bold{134}
- \item {\tt add_mult_dist} theorem, 48, 136
- \item {\tt add_safes}, \bold{119}
- \item {\tt add_typing} theorem, 136
- \item {\tt add_unsafes}, \bold{119}
- \item {\tt addC0} theorem, 136
- \item {\tt addC_succ} theorem, 136
- \item {\tt Addsplits}, \bold{76}
- \item {\tt addsplits}, \bold{76}, 81, 92
- \item {\tt ALL} symbol, 7, 27, 60, 62, 69, 70, 113
- \item {\tt All} constant, 7, 60, 113
- \item {\tt All_def} theorem, 64
- \item {\tt all_dupE} theorem, 5, 9, 66
- \item {\tt all_impE} theorem, 9
- \item {\tt allE} theorem, 5, 9, 66
- \item {\tt allI} theorem, 8, 66
- \item {\tt allL} theorem, 115, 119
- \item {\tt allL_thin} theorem, 116
- \item {\tt allR} theorem, 115
- \item {\tt and_def} theorem, 43, 64
- \item {\tt app_def} theorem, 50
- \item {\tt apply_def} theorem, 32
- \item {\tt apply_equality} theorem, 40, 41, 57, 58
- \item {\tt apply_equality2} theorem, 40
- \item {\tt apply_iff} theorem, 40
- \item {\tt apply_Pair} theorem, 40, 58
- \item {\tt apply_type} theorem, 40
- \item {\tt arg_cong} theorem, 65
- \item {\tt Arith} theory, 47, 80, 135
+ \item {\tt absdiff_def} theorem, 118
+ \item {\tt add_assoc} theorem, 118
+ \item {\tt add_commute} theorem, 118
+ \item {\tt add_def} theorem, 41, 118
+ \item {\tt add_inverse_diff} theorem, 118
+ \item {\tt add_mp_tac}, \bold{116}
+ \item {\tt add_mult_dist} theorem, 41, 118
+ \item {\tt add_safes}, \bold{103}
+ \item {\tt add_typing} theorem, 118
+ \item {\tt add_unsafes}, \bold{103}
+ \item {\tt addC0} theorem, 118
+ \item {\tt addC_succ} theorem, 118
+ \item {\tt Addsplits}, \bold{66}
+ \item {\tt addsplits}, \bold{65}, 70, 81
+ \item {\tt ALL} symbol, 5, 23, 52, 54, 59, 60, 98
+ \item {\tt All} constant, 5, 52, 98
+ \item {\tt All_def} theorem, 55
+ \item {\tt all_dupE} theorem, 4, 7, 57
+ \item {\tt all_impE} theorem, 7
+ \item {\tt allE} theorem, 4, 7, 57
+ \item {\tt allI} theorem, 6, 57
+ \item {\tt allL} theorem, 100, 103
+ \item {\tt allL_thin} theorem, 101
+ \item {\tt allR} theorem, 100
+ \item {\tt and_def} theorem, 36, 55
+ \item {\tt app_def} theorem, 43
+ \item {\tt apply_def} theorem, 27
+ \item {\tt apply_equality} theorem, 34, 35, 49
+ \item {\tt apply_equality2} theorem, 34
+ \item {\tt apply_iff} theorem, 34
+ \item {\tt apply_Pair} theorem, 34, 49
+ \item {\tt apply_type} theorem, 34
+ \item {\tt arg_cong} theorem, 56
+ \item {\tt Arith} theory, 38, 68, 117
\item assumptions
- \subitem contradictory, 16
- \subitem in {\CTT}, 124, 134
+ \subitem contradictory, 14
+ \subitem in {\CTT}, 107, 116
\indexspace
- \item {\tt Ball} constant, 26, 30, 68, 70
- \item {\tt ball_cong} theorem, 33, 34
- \item {\tt Ball_def} theorem, 31, 71
- \item {\tt ballE} theorem, 33, 34, 72
- \item {\tt ballI} theorem, 34, 72
- \item {\tt basic} theorem, 115
- \item {\tt basic_defs}, \bold{132}
- \item {\tt best_tac}, \bold{120}
- \item {\tt beta} theorem, 40, 41
- \item {\tt Bex} constant, 26, 30, 68, 70
- \item {\tt bex_cong} theorem, 33, 34
- \item {\tt Bex_def} theorem, 31, 71
- \item {\tt bexCI} theorem, 34, 70, 72
- \item {\tt bexE} theorem, 34, 72
- \item {\tt bexI} theorem, 34, 70, 72
- \item {\tt bij} constant, 46
- \item {\tt bij_converse_bij} theorem, 46
- \item {\tt bij_def} theorem, 46
- \item {\tt bij_disjoint_Un} theorem, 46
- \item {\tt Blast_tac}, 17, 55, 56
- \item {\tt blast_tac}, 18, 19, 21
- \item {\tt bnd_mono_def} theorem, 45
- \item {\tt Bool} theory, 41
- \item {\textit {bool}} type, 61
- \item {\tt bool_0I} theorem, 43
- \item {\tt bool_1I} theorem, 43
- \item {\tt bool_def} theorem, 43
- \item {\tt boolE} theorem, 43
- \item {\tt box_equals} theorem, 65, 67
- \item {\tt bspec} theorem, 34, 72
- \item {\tt butlast} constant, 82
+ \item {\tt Ball} constant, 22, 25, 58, 60
+ \item {\tt ball_cong} theorem, 28, 29
+ \item {\tt Ball_def} theorem, 26, 61
+ \item {\tt ballE} theorem, 28, 29, 62
+ \item {\tt ballI} theorem, 29, 62
+ \item {\tt basic} theorem, 100
+ \item {\tt basic_defs}, \bold{115}
+ \item {\tt best_tac}, \bold{104}
+ \item {\tt beta} theorem, 34, 35
+ \item {\tt Bex} constant, 22, 25, 58, 60
+ \item {\tt bex_cong} theorem, 28, 29
+ \item {\tt Bex_def} theorem, 26, 61
+ \item {\tt bexCI} theorem, 29, 61, 62
+ \item {\tt bexE} theorem, 29, 62
+ \item {\tt bexI} theorem, 29, 61, 62
+ \item {\tt bij} constant, 40
+ \item {\tt bij_converse_bij} theorem, 40
+ \item {\tt bij_def} theorem, 40
+ \item {\tt bij_disjoint_Un} theorem, 40
+ \item {\tt Blast_tac}, 14, 47, 48
+ \item {\tt blast_tac}, 15--18
+ \item {\tt bnd_mono_def} theorem, 39
+ \item {\tt Bool} theory, 35
+ \item {\textit {bool}} type, 51
+ \item {\tt bool_0I} theorem, 36
+ \item {\tt bool_1I} theorem, 36
+ \item {\tt bool_def} theorem, 36
+ \item {\tt boolE} theorem, 36
+ \item {\tt box_equals} theorem, 55, 56
+ \item {\tt bspec} theorem, 29, 62
+ \item {\tt butlast} constant, 71
\indexspace
- \item {\tt case} constant, 44
- \item {\tt case} symbol, 63, 80, 81, 92
- \item {\tt case_def} theorem, 44
- \item {\tt case_Inl} theorem, 44
- \item {\tt case_Inr} theorem, 44
- \item {\tt case_tac}, \bold{67}
+ \item {\tt case} constant, 37
+ \item {\tt case} symbol, 54, 68, 70, 80
+ \item {\tt case_def} theorem, 37
+ \item {\tt case_Inl} theorem, 37
+ \item {\tt case_Inr} theorem, 37
+ \item {\tt case_tac}, \bold{58}
\item {\tt CCL} theory, 1
- \item {\tt ccontr} theorem, 66
- \item {\tt classical} theorem, 66
- \item {\tt coinduct} theorem, 45
- \item {\tt coinductive}, 104--107
- \item {\tt Collect} constant, 26, 27, 30, 68, 70
- \item {\tt Collect_def} theorem, 31
- \item {\tt Collect_mem_eq} theorem, 70, 71
- \item {\tt Collect_subset} theorem, 37
- \item {\tt CollectD} theorem, 72, 110
- \item {\tt CollectD1} theorem, 33, 35
- \item {\tt CollectD2} theorem, 33, 35
- \item {\tt CollectE} theorem, 33, 35, 72
- \item {\tt CollectI} theorem, 35, 72, 110
- \item {\tt comp_assoc} theorem, 46
- \item {\tt comp_bij} theorem, 46
- \item {\tt comp_def} theorem, 46
- \item {\tt comp_func} theorem, 46
- \item {\tt comp_func_apply} theorem, 46
- \item {\tt comp_inj} theorem, 46
- \item {\tt comp_rls}, \bold{132}
- \item {\tt comp_surj} theorem, 46
- \item {\tt comp_type} theorem, 46
- \item {\tt Compl} constant, 68
- \item {\tt Compl_def} theorem, 71
- \item {\tt Compl_disjoint} theorem, 74
- \item {\tt Compl_Int} theorem, 74
- \item {\tt Compl_partition} theorem, 74
- \item {\tt Compl_Un} theorem, 74
- \item {\tt ComplD} theorem, 73
- \item {\tt ComplI} theorem, 73
- \item {\tt concat} constant, 82
- \item {\tt cond_0} theorem, 43
- \item {\tt cond_1} theorem, 43
- \item {\tt cond_def} theorem, 43
- \item {\tt cong} theorem, 65
- \item congruence rules, 33
- \item {\tt conj_cong}, 6, 75
- \item {\tt conj_impE} theorem, 9, 10
- \item {\tt conjE} theorem, 9, 65
- \item {\tt conjI} theorem, 8, 65
- \item {\tt conjL} theorem, 115
- \item {\tt conjR} theorem, 115
- \item {\tt conjunct1} theorem, 8, 65
- \item {\tt conjunct2} theorem, 8, 65
- \item {\tt conL} theorem, 116
- \item {\tt conR} theorem, 116
- \item {\tt cons} constant, 26, 27
- \item {\tt cons_def} theorem, 32
- \item {\tt Cons_iff} theorem, 50
- \item {\tt consCI} theorem, 36
- \item {\tt consE} theorem, 36
- \item {\tt ConsI} theorem, 50
- \item {\tt consI1} theorem, 36
- \item {\tt consI2} theorem, 36
- \item Constructive Type Theory, 124--146
- \item {\tt contr} constant, 125
- \item {\tt converse} constant, 26, 40
- \item {\tt converse_def} theorem, 32
- \item {\tt could_res}, \bold{118}
- \item {\tt could_resolve_seq}, \bold{118}
- \item {\tt CTT} theory, 1, 124
+ \item {\tt ccontr} theorem, 57
+ \item {\tt classical} theorem, 57
+ \item {\tt coinduct} theorem, 39
+ \item {\tt coinductive}, 90--92
+ \item {\tt Collect} constant, 22, 23, 25, 58, 60
+ \item {\tt Collect_def} theorem, 26
+ \item {\tt Collect_mem_eq} theorem, 61
+ \item {\tt Collect_subset} theorem, 32
+ \item {\tt CollectD} theorem, 62, 95
+ \item {\tt CollectD1} theorem, 28, 30
+ \item {\tt CollectD2} theorem, 28, 30
+ \item {\tt CollectE} theorem, 28, 30, 62
+ \item {\tt CollectI} theorem, 30, 62, 95
+ \item {\tt comp_assoc} theorem, 40
+ \item {\tt comp_bij} theorem, 40
+ \item {\tt comp_def} theorem, 40
+ \item {\tt comp_func} theorem, 40
+ \item {\tt comp_func_apply} theorem, 40
+ \item {\tt comp_inj} theorem, 40
+ \item {\tt comp_rls}, \bold{115}
+ \item {\tt comp_surj} theorem, 40
+ \item {\tt comp_type} theorem, 40
+ \item {\tt Compl} constant, 58
+ \item {\tt Compl_def} theorem, 61
+ \item {\tt Compl_disjoint} theorem, 64
+ \item {\tt Compl_Int} theorem, 64
+ \item {\tt Compl_partition} theorem, 64
+ \item {\tt Compl_Un} theorem, 64
+ \item {\tt ComplD} theorem, 63
+ \item {\tt ComplI} theorem, 63
+ \item {\tt concat} constant, 71
+ \item {\tt cond_0} theorem, 36
+ \item {\tt cond_1} theorem, 36
+ \item {\tt cond_def} theorem, 36
+ \item {\tt cong} theorem, 56
+ \item congruence rules, 28
+ \item {\tt conj_cong}, 8, 65
+ \item {\tt conj_impE} theorem, 7, 8
+ \item {\tt conjE} theorem, 7, 56
+ \item {\tt conjI} theorem, 6, 56
+ \item {\tt conjL} theorem, 100
+ \item {\tt conjR} theorem, 100
+ \item {\tt conjunct1} theorem, 6, 56
+ \item {\tt conjunct2} theorem, 6, 56
+ \item {\tt conL} theorem, 101
+ \item {\tt conR} theorem, 101
+ \item {\tt cons} constant, 21, 22
+ \item {\tt cons_def} theorem, 27
+ \item {\tt Cons_iff} theorem, 43
+ \item {\tt consCI} theorem, 31
+ \item {\tt consE} theorem, 31
+ \item {\tt ConsI} theorem, 43
+ \item {\tt consI1} theorem, 31
+ \item {\tt consI2} theorem, 31
+ \item Constructive Type Theory, 107--126
+ \item {\tt contr} constant, 108
+ \item {\tt converse} constant, 22, 34
+ \item {\tt converse_def} theorem, 27
+ \item {\tt could_res}, \bold{102}
+ \item {\tt could_resolve_seq}, \bold{102}
+ \item {\tt CTT} theory, 1, 107
\item {\tt Cube} theory, 1
- \item {\tt cut} theorem, 115
- \item {\tt cut_facts_tac}, 19
- \item {\tt cutL_tac}, \bold{117}
- \item {\tt cutR_tac}, \bold{117}
+ \item {\tt cut} theorem, 100
+ \item {\tt cut_facts_tac}, 16
+ \item {\tt cutL_tac}, \bold{101}
+ \item {\tt cutR_tac}, \bold{101}
\indexspace
- \item {\tt datatype}, 89--97
- \item {\tt Delsplits}, \bold{76}
- \item {\tt delsplits}, \bold{76}
- \item {\tt diff_0_eq_0} theorem, 136
- \item {\tt Diff_cancel} theorem, 42
- \item {\tt Diff_contains} theorem, 37
- \item {\tt Diff_def} theorem, 31
- \item {\tt diff_def} theorem, 48, 136
- \item {\tt Diff_disjoint} theorem, 42
- \item {\tt Diff_Int} theorem, 42
- \item {\tt Diff_partition} theorem, 42
- \item {\tt diff_self_eq_0} theorem, 136
- \item {\tt Diff_subset} theorem, 37
- \item {\tt diff_succ_succ} theorem, 136
- \item {\tt diff_typing} theorem, 136
- \item {\tt Diff_Un} theorem, 42
- \item {\tt diffC0} theorem, 136
- \item {\tt DiffD1} theorem, 36
- \item {\tt DiffD2} theorem, 36
- \item {\tt DiffE} theorem, 36
- \item {\tt DiffI} theorem, 36
- \item {\tt disj_impE} theorem, 9, 10, 14
- \item {\tt disjCI} theorem, 11, 66
- \item {\tt disjE} theorem, 8, 65
- \item {\tt disjI1} theorem, 8, 65
- \item {\tt disjI2} theorem, 8, 65
- \item {\tt disjL} theorem, 115
- \item {\tt disjR} theorem, 115
- \item {\tt div} symbol, 48, 79, 136
- \item {\tt div_def} theorem, 48, 136
- \item {\tt div_geq} theorem, 80
- \item {\tt div_less} theorem, 80
- \item {\tt Divides} theory, 80
- \item {\tt domain} constant, 26, 40
- \item {\tt domain_def} theorem, 32
- \item {\tt domain_of_fun} theorem, 40
- \item {\tt domain_subset} theorem, 39
- \item {\tt domain_type} theorem, 40
- \item {\tt domainE} theorem, 39, 40
- \item {\tt domainI} theorem, 39, 40
- \item {\tt double_complement} theorem, 42, 74
- \item {\tt dresolve_tac}, 54
- \item {\tt drop} constant, 82
- \item {\tt dropWhile} constant, 82
+ \item {\tt datatype}, 78--85
+ \item {\tt Delsplits}, \bold{66}
+ \item {\tt delsplits}, \bold{66}
+ \item {\tt diff_0_eq_0} theorem, 118
+ \item {\tt Diff_cancel} theorem, 36
+ \item {\tt Diff_contains} theorem, 32
+ \item {\tt Diff_def} theorem, 26
+ \item {\tt diff_def} theorem, 41, 118
+ \item {\tt Diff_disjoint} theorem, 36
+ \item {\tt Diff_Int} theorem, 36
+ \item {\tt Diff_partition} theorem, 36
+ \item {\tt diff_self_eq_0} theorem, 118
+ \item {\tt Diff_subset} theorem, 32
+ \item {\tt diff_succ_succ} theorem, 118
+ \item {\tt diff_typing} theorem, 118
+ \item {\tt Diff_Un} theorem, 36
+ \item {\tt diffC0} theorem, 118
+ \item {\tt DiffD1} theorem, 30
+ \item {\tt DiffD2} theorem, 30
+ \item {\tt DiffE} theorem, 30
+ \item {\tt DiffI} theorem, 30
+ \item {\tt disj_impE} theorem, 7, 8, 12
+ \item {\tt disjCI} theorem, 9, 57
+ \item {\tt disjE} theorem, 6, 56
+ \item {\tt disjI1} theorem, 6, 56
+ \item {\tt disjI2} theorem, 6, 56
+ \item {\tt disjL} theorem, 100
+ \item {\tt disjR} theorem, 100
+ \item {\tt div} symbol, 41, 69, 118
+ \item {\tt div_def} theorem, 41, 118
+ \item {\tt div_geq} theorem, 69
+ \item {\tt div_less} theorem, 69
+ \item {\tt Divides} theory, 68
+ \item {\tt domain} constant, 22, 34
+ \item {\tt domain_def} theorem, 27
+ \item {\tt domain_of_fun} theorem, 34
+ \item {\tt domain_subset} theorem, 33
+ \item {\tt domain_type} theorem, 34
+ \item {\tt domainE} theorem, 33, 34
+ \item {\tt domainI} theorem, 33, 34
+ \item {\tt double_complement} theorem, 36, 64
+ \item {\tt dresolve_tac}, 46
+ \item {\tt drop} constant, 71
+ \item {\tt dropWhile} constant, 71
\indexspace
- \item {\tt Elem} constant, 125
- \item {\tt elim_rls}, \bold{132}
- \item {\tt elimL_rls}, \bold{132}
- \item {\tt empty_def} theorem, 71
- \item {\tt empty_pack}, \bold{118}
- \item {\tt empty_subsetI} theorem, 34
- \item {\tt emptyE} theorem, 34, 73
- \item {\tt Eps} constant, 60, 62
- \item {\tt Eq} constant, 125
- \item {\tt eq} constant, 125, 130
- \item {\tt eq_mp_tac}, \bold{10}
- \item {\tt EqC} theorem, 131
- \item {\tt EqE} theorem, 131
- \item {\tt Eqelem} constant, 125
- \item {\tt EqF} theorem, 131
- \item {\tt EqFL} theorem, 131
- \item {\tt EqI} theorem, 131
- \item {\tt Eqtype} constant, 125
- \item {\tt equal_tac}, \bold{133}
- \item {\tt equal_types} theorem, 128
- \item {\tt equal_typesL} theorem, 128
- \item {\tt equalityCE} theorem, 70, 72, 110, 111
- \item {\tt equalityD1} theorem, 34, 72
- \item {\tt equalityD2} theorem, 34, 72
- \item {\tt equalityE} theorem, 34, 72
- \item {\tt equalityI} theorem, 34, 53, 72
- \item {\tt equals0D} theorem, 34
- \item {\tt equals0I} theorem, 34
- \item {\tt eresolve_tac}, 16
- \item {\tt eta} theorem, 40, 41
- \item {\tt EX} symbol, 7, 27, 60, 62, 69, 70, 113
- \item {\tt Ex} constant, 7, 60, 113
- \item {\tt EX!} symbol, 7, 60
- \item {\tt Ex1} constant, 7, 60
- \item {\tt Ex1_def} theorem, 64
- \item {\tt ex1_def} theorem, 8
- \item {\tt ex1E} theorem, 9, 66
- \item {\tt ex1I} theorem, 9, 66
- \item {\tt Ex_def} theorem, 64
- \item {\tt ex_impE} theorem, 9
- \item {\tt exCI} theorem, 11, 15, 66
- \item {\tt excluded_middle} theorem, 11, 66
- \item {\tt exE} theorem, 8, 66
- \item {\tt exhaust_tac}, \bold{93}
- \item {\tt exI} theorem, 8, 66
- \item {\tt exL} theorem, 115
- \item {\tt Exp} theory, 108
- \item {\tt exR} theorem, 115, 119, 120
- \item {\tt exR_thin} theorem, 116, 120, 121
- \item {\tt ext} theorem, 63, 64
- \item {\tt extension} theorem, 31
+ \item {\tt Elem} constant, 108
+ \item {\tt elim_rls}, \bold{115}
+ \item {\tt elimL_rls}, \bold{115}
+ \item {\tt empty_def} theorem, 61
+ \item {\tt empty_pack}, \bold{102}
+ \item {\tt empty_subsetI} theorem, 29
+ \item {\tt emptyE} theorem, 29, 63
+ \item {\tt Eps} constant, 52, 54
+ \item {\tt Eq} constant, 108
+ \item {\tt eq} constant, 108, 114
+ \item {\tt eq_mp_tac}, \bold{9}
+ \item {\tt EqC} theorem, 113
+ \item {\tt EqE} theorem, 113
+ \item {\tt Eqelem} constant, 108
+ \item {\tt EqF} theorem, 113
+ \item {\tt EqFL} theorem, 113
+ \item {\tt EqI} theorem, 113
+ \item {\tt Eqtype} constant, 108
+ \item {\tt equal_tac}, \bold{115}
+ \item {\tt equal_types} theorem, 110
+ \item {\tt equal_typesL} theorem, 110
+ \item {\tt equalityCE} theorem, 61, 62, 95
+ \item {\tt equalityD1} theorem, 29, 62
+ \item {\tt equalityD2} theorem, 29, 62
+ \item {\tt equalityE} theorem, 29, 62
+ \item {\tt equalityI} theorem, 29, 45, 62
+ \item {\tt equals0D} theorem, 29
+ \item {\tt equals0I} theorem, 29
+ \item {\tt eresolve_tac}, 13
+ \item {\tt eta} theorem, 34, 35
+ \item {\tt EX} symbol, 5, 23, 52, 54, 59, 60, 98
+ \item {\tt Ex} constant, 5, 52, 98
+ \item {\tt EX!} symbol, 5, 52
+ \item {\tt Ex1} constant, 5, 52
+ \item {\tt Ex1_def} theorem, 55
+ \item {\tt ex1_def} theorem, 6
+ \item {\tt ex1E} theorem, 7, 57
+ \item {\tt ex1I} theorem, 7, 57
+ \item {\tt Ex_def} theorem, 55
+ \item {\tt ex_impE} theorem, 7
+ \item {\tt exCI} theorem, 9, 13, 57
+ \item {\tt excluded_middle} theorem, 9, 57
+ \item {\tt exE} theorem, 6, 57
+ \item {\tt exhaust_tac}, \bold{81}
+ \item {\tt exI} theorem, 6, 57
+ \item {\tt exL} theorem, 100
+ \item {\tt Exp} theory, 93
+ \item {\tt exR} theorem, 100, 103, 104
+ \item {\tt exR_thin} theorem, 101, 104, 105
+ \item {\tt ext} theorem, 55
+ \item {\tt extension} theorem, 26
\indexspace
- \item {\tt F} constant, 125
- \item {\tt False} constant, 7, 60, 113
- \item {\tt False_def} theorem, 64
- \item {\tt FalseE} theorem, 8, 65
- \item {\tt FalseL} theorem, 115
- \item {\tt fast_tac}, \bold{120}
- \item {\tt FE} theorem, 131, 135
- \item {\tt FEL} theorem, 131
- \item {\tt FF} theorem, 131
- \item {\tt field} constant, 26
- \item {\tt field_def} theorem, 32
- \item {\tt field_subset} theorem, 39
- \item {\tt fieldCI} theorem, 39
- \item {\tt fieldE} theorem, 39
- \item {\tt fieldI1} theorem, 39
- \item {\tt fieldI2} theorem, 39
- \item {\tt filseq_resolve_tac}, \bold{118}
- \item {\tt filt_resolve_tac}, 118, 133
- \item {\tt filter} constant, 82
- \item {\tt Fin.consI} theorem, 49
- \item {\tt Fin.emptyI} theorem, 49
- \item {\tt Fin_induct} theorem, 49
- \item {\tt Fin_mono} theorem, 49
- \item {\tt Fin_subset} theorem, 49
- \item {\tt Fin_UnI} theorem, 49
- \item {\tt Fin_UnionI} theorem, 49
- \item first-order logic, 5--23
- \item {\tt Fixedpt} theory, 43
- \item {\tt flat} constant, 50
- \item {\tt flat_def} theorem, 50
- \item flex-flex constraints, 114
- \item {\tt FOL} theory, 1, 5, 11, 134
- \item {\tt FOL_cs}, \bold{11}
- \item {\tt FOL_ss}, \bold{6}
- \item {\tt foldl} constant, 82
- \item {\tt form_rls}, \bold{132}
- \item {\tt formL_rls}, \bold{132}
- \item {\tt forms_of_seq}, \bold{117}
- \item {\tt foundation} theorem, 31
- \item {\tt fst} constant, 26, 33, 77, 125, 130
- \item {\tt fst_conv} theorem, 38, 77
- \item {\tt fst_def} theorem, 32, 130
- \item {\tt Fun} theory, 75
- \item {\textit {fun}} type, 61
- \item {\tt fun_cong} theorem, 65
- \item {\tt fun_disjoint_apply1} theorem, 41, 57
- \item {\tt fun_disjoint_apply2} theorem, 41
- \item {\tt fun_disjoint_Un} theorem, 41, 58
- \item {\tt fun_empty} theorem, 41
- \item {\tt fun_extension} theorem, 40, 41
- \item {\tt fun_is_rel} theorem, 40
- \item {\tt fun_single} theorem, 41
+ \item {\tt F} constant, 108
+ \item {\tt False} constant, 5, 52, 98
+ \item {\tt False_def} theorem, 55
+ \item {\tt FalseE} theorem, 6, 56
+ \item {\tt FalseL} theorem, 100
+ \item {\tt fast_tac}, \bold{104}
+ \item {\tt FE} theorem, 113, 117
+ \item {\tt FEL} theorem, 113
+ \item {\tt FF} theorem, 113
+ \item {\tt field} constant, 22
+ \item {\tt field_def} theorem, 27
+ \item {\tt field_subset} theorem, 33
+ \item {\tt fieldCI} theorem, 33
+ \item {\tt fieldE} theorem, 33
+ \item {\tt fieldI1} theorem, 33
+ \item {\tt fieldI2} theorem, 33
+ \item {\tt filseq_resolve_tac}, \bold{102}
+ \item {\tt filt_resolve_tac}, 102, 115
+ \item {\tt filter} constant, 71
+ \item {\tt Fin.consI} theorem, 42
+ \item {\tt Fin.emptyI} theorem, 42
+ \item {\tt Fin_induct} theorem, 42
+ \item {\tt Fin_mono} theorem, 42
+ \item {\tt Fin_subset} theorem, 42
+ \item {\tt Fin_UnI} theorem, 42
+ \item {\tt Fin_UnionI} theorem, 42
+ \item first-order logic, 4--19
+ \item {\tt Fixedpt} theory, 38
+ \item {\tt flat} constant, 43
+ \item {\tt flat_def} theorem, 43
+ \item flex-flex constraints, 97
+ \item {\tt FOL} theory, 1, 4, 9, 116
+ \item {\tt FOL_cs}, \bold{9}
+ \item {\tt FOL_ss}, \bold{4}
+ \item {\tt foldl} constant, 71
+ \item {\tt form_rls}, \bold{114}
+ \item {\tt formL_rls}, \bold{115}
+ \item {\tt forms_of_seq}, \bold{102}
+ \item {\tt foundation} theorem, 26
+ \item {\tt fst} constant, 22, 28, 67, 108, 114
+ \item {\tt fst_conv} theorem, 32, 67
+ \item {\tt fst_def} theorem, 27, 112
+ \item {\tt Fun} theory, 64
+ \item {\textit {fun}} type, 51
+ \item {\tt fun_cong} theorem, 56
+ \item {\tt fun_disjoint_apply1} theorem, 35, 48
+ \item {\tt fun_disjoint_apply2} theorem, 35
+ \item {\tt fun_disjoint_Un} theorem, 35, 49
+ \item {\tt fun_empty} theorem, 35
+ \item {\tt fun_extension} theorem, 34, 35
+ \item {\tt fun_is_rel} theorem, 34
+ \item {\tt fun_single} theorem, 35
\item function applications
- \subitem in \CTT, 127
- \subitem in \ZF, 26
+ \subitem in \CTT, 109
+ \subitem in \ZF, 22
\indexspace
- \item {\tt gfp_def} theorem, 45
- \item {\tt gfp_least} theorem, 45
- \item {\tt gfp_mono} theorem, 45
- \item {\tt gfp_subset} theorem, 45
- \item {\tt gfp_Tarski} theorem, 45
- \item {\tt gfp_upperbound} theorem, 45
- \item {\tt Goalw}, 18, 19
+ \item {\tt gfp_def} theorem, 39
+ \item {\tt gfp_least} theorem, 39
+ \item {\tt gfp_mono} theorem, 39
+ \item {\tt gfp_subset} theorem, 39
+ \item {\tt gfp_Tarski} theorem, 39
+ \item {\tt gfp_upperbound} theorem, 39
+ \item {\tt Goalw}, 15, 16
\indexspace
- \item {\tt hd} constant, 82, 102
- \item higher-order logic, 59--111
- \item {\tt HOL} theory, 1, 59
- \item {\sc hol} system, 59, 62
- \item {\tt HOL_basic_ss}, \bold{75}
- \item {\tt HOL_cs}, \bold{76}
- \item {\tt HOL_quantifiers}, \bold{62}, 70
- \item {\tt HOL_ss}, \bold{75}
+ \item {\tt hd} constant, 71
+ \item higher-order logic, 51--96
+ \item {\tt HOL} theory, 1, 51
+ \item {\sc hol} system, 51, 54
+ \item {\tt HOL_basic_ss}, \bold{65}
+ \item {\tt HOL_cs}, \bold{66}
+ \item {\tt HOL_quantifiers}, \bold{54}, 60
+ \item {\tt HOL_ss}, \bold{65}
\item {\tt HOLCF} theory, 1
- \item {\tt hyp_rew_tac}, \bold{134}
- \item {\tt hyp_subst_tac}, 6, 75
+ \item {\tt hyp_rew_tac}, \bold{116}
+ \item {\tt hyp_subst_tac}, 8, 65
\indexspace
- \item {\textit {i}} type, 25, 124
- \item {\tt id} constant, 46
- \item {\tt id_def} theorem, 46
- \item {\tt If} constant, 60
- \item {\tt if} constant, 26
- \item {\tt if_def} theorem, 18, 31, 64
- \item {\tt if_not_P} theorem, 36, 66
- \item {\tt if_P} theorem, 36, 66
- \item {\tt ifE} theorem, 19
- \item {\tt iff} theorem, 63, 64
- \item {\tt iff_def} theorem, 8, 115
- \item {\tt iff_impE} theorem, 9
- \item {\tt iffCE} theorem, 11, 66, 70
- \item {\tt iffD1} theorem, 9, 65
- \item {\tt iffD2} theorem, 9, 65
- \item {\tt iffE} theorem, 9, 65
- \item {\tt iffI} theorem, 9, 19, 65
- \item {\tt iffL} theorem, 116, 122
- \item {\tt iffR} theorem, 116
- \item {\tt ifI} theorem, 19
- \item {\tt IFOL} theory, 5
- \item {\tt IFOL_ss}, \bold{6}
- \item {\tt image_def} theorem, 32, 71
- \item {\tt imageE} theorem, 39, 73
- \item {\tt imageI} theorem, 39, 73
- \item {\tt imp_impE} theorem, 9, 14
- \item {\tt impCE} theorem, 11, 66
- \item {\tt impE} theorem, 9, 10, 65
- \item {\tt impI} theorem, 8, 63
- \item {\tt impL} theorem, 115
- \item {\tt impR} theorem, 115
- \item {\tt in} symbol, 28, 61
- \item {\textit {ind}} type, 78
- \item {\tt induct} theorem, 45
- \item {\tt induct_tac}, 80, \bold{93}
- \item {\tt inductive}, 104--107
- \item {\tt Inf} constant, 26, 30
- \item {\tt infinity} theorem, 32
- \item {\tt inj} constant, 46, 75
- \item {\tt inj_converse_inj} theorem, 46
- \item {\tt inj_def} theorem, 46, 75
- \item {\tt inj_Inl} theorem, 79
- \item {\tt inj_Inr} theorem, 79
- \item {\tt inj_on} constant, 75
- \item {\tt inj_on_def} theorem, 75
- \item {\tt inj_Suc} theorem, 79
- \item {\tt Inl} constant, 44, 79
- \item {\tt inl} constant, 125, 130, 140
- \item {\tt Inl_def} theorem, 44
- \item {\tt Inl_inject} theorem, 44
- \item {\tt Inl_neq_Inr} theorem, 44
- \item {\tt Inl_not_Inr} theorem, 79
- \item {\tt Inr} constant, 44, 79
- \item {\tt inr} constant, 125, 130
- \item {\tt Inr_def} theorem, 44
- \item {\tt Inr_inject} theorem, 44
- \item {\tt insert} constant, 68
- \item {\tt insert_def} theorem, 71
- \item {\tt insertE} theorem, 73
- \item {\tt insertI1} theorem, 73
- \item {\tt insertI2} theorem, 73
- \item {\tt INT} symbol, 27, 29, 68--70
- \item {\tt Int} symbol, 26, 68
- \item {\tt Int_absorb} theorem, 42, 74
- \item {\tt Int_assoc} theorem, 42, 74
- \item {\tt Int_commute} theorem, 42, 74
- \item {\tt INT_D} theorem, 73
- \item {\tt Int_def} theorem, 31, 71
- \item {\tt INT_E} theorem, 35, 73
- \item {\tt Int_greatest} theorem, 37, 53, 55, 74
- \item {\tt INT_I} theorem, 35, 73
- \item {\tt Int_Inter_image} theorem, 74
- \item {\tt Int_lower1} theorem, 37, 54, 74
- \item {\tt Int_lower2} theorem, 37, 54, 74
- \item {\tt Int_Un_distrib} theorem, 42, 74
- \item {\tt Int_Union} theorem, 74
- \item {\tt Int_Union_RepFun} theorem, 42
- \item {\tt IntD1} theorem, 36, 73
- \item {\tt IntD2} theorem, 36, 73
- \item {\tt IntE} theorem, 36, 54, 73
- \item {\tt INTER} constant, 68
- \item {\tt Inter} constant, 26, 68
- \item {\tt INTER1} constant, 68
- \item {\tt INTER1_def} theorem, 71
- \item {\tt INTER_def} theorem, 71
- \item {\tt Inter_def} theorem, 31, 71
- \item {\tt Inter_greatest} theorem, 37, 74
- \item {\tt Inter_lower} theorem, 37, 74
- \item {\tt Inter_Un_distrib} theorem, 42, 74
- \item {\tt InterD} theorem, 35, 73
- \item {\tt InterE} theorem, 35, 73
- \item {\tt InterI} theorem, 33, 35, 73
- \item {\tt IntI} theorem, 36, 73
- \item {\tt IntPr.best_tac}, \bold{11}
- \item {\tt IntPr.fast_tac}, \bold{10}, 13
- \item {\tt IntPr.inst_step_tac}, \bold{10}
- \item {\tt IntPr.safe_step_tac}, \bold{10}
- \item {\tt IntPr.safe_tac}, \bold{10}
- \item {\tt IntPr.step_tac}, \bold{10}
- \item {\tt intr_rls}, \bold{132}
- \item {\tt intr_tac}, \bold{133}, 142, 143
- \item {\tt intrL_rls}, \bold{132}
- \item {\tt inv} constant, 75
- \item {\tt inv_def} theorem, 75
+ \item {\textit {i}} type, 21, 107
+ \item {\tt id} constant, 40
+ \item {\tt id_def} theorem, 40
+ \item {\tt If} constant, 52
+ \item {\tt if} constant, 22
+ \item {\tt if_def} theorem, 15, 26, 55
+ \item {\tt if_not_P} theorem, 31, 57
+ \item {\tt if_P} theorem, 31, 57
+ \item {\tt ifE} theorem, 16
+ \item {\tt iff} theorem, 55
+ \item {\tt iff_def} theorem, 6, 100
+ \item {\tt iff_impE} theorem, 7
+ \item {\tt iffCE} theorem, 9, 57, 61
+ \item {\tt iffD1} theorem, 7, 56
+ \item {\tt iffD2} theorem, 7, 56
+ \item {\tt iffE} theorem, 7, 56
+ \item {\tt iffI} theorem, 7, 16, 56
+ \item {\tt iffL} theorem, 101, 106
+ \item {\tt iffR} theorem, 101
+ \item {\tt ifI} theorem, 16
+ \item {\tt IFOL} theory, 4
+ \item {\tt IFOL_ss}, \bold{4}
+ \item {\tt image_def} theorem, 27, 61
+ \item {\tt imageE} theorem, 34, 63
+ \item {\tt imageI} theorem, 34, 63
+ \item {\tt imp_impE} theorem, 7, 12
+ \item {\tt impCE} theorem, 9, 57
+ \item {\tt impE} theorem, 7, 8, 56
+ \item {\tt impI} theorem, 6, 55
+ \item {\tt impL} theorem, 100
+ \item {\tt impR} theorem, 100
+ \item {\tt in} symbol, 24, 53
+ \item {\textit {ind}} type, 68
+ \item {\tt induct} theorem, 39
+ \item {\tt induct_tac}, 70, \bold{81}
+ \item {\tt inductive}, 90--92
+ \item {\tt Inf} constant, 22, 25
+ \item {\tt infinity} theorem, 27
+ \item {\tt inj} constant, 40, 64
+ \item {\tt inj_converse_inj} theorem, 40
+ \item {\tt inj_def} theorem, 40, 64
+ \item {\tt inj_Inl} theorem, 68
+ \item {\tt inj_Inr} theorem, 68
+ \item {\tt inj_on} constant, 64
+ \item {\tt inj_on_def} theorem, 64
+ \item {\tt inj_Suc} theorem, 69
+ \item {\tt Inl} constant, 37, 68
+ \item {\tt inl} constant, 108, 114, 121
+ \item {\tt Inl_def} theorem, 37
+ \item {\tt Inl_inject} theorem, 37
+ \item {\tt Inl_neq_Inr} theorem, 37
+ \item {\tt Inl_not_Inr} theorem, 68
+ \item {\tt Inr} constant, 37, 68
+ \item {\tt inr} constant, 108, 114
+ \item {\tt Inr_def} theorem, 37
+ \item {\tt Inr_inject} theorem, 37
+ \item {\tt insert} constant, 58
+ \item {\tt insert_def} theorem, 61
+ \item {\tt insertE} theorem, 63
+ \item {\tt insertI1} theorem, 63
+ \item {\tt insertI2} theorem, 63
+ \item {\tt INT} symbol, 23, 58--60
+ \item {\tt Int} symbol, 22, 58
+ \item {\tt Int_absorb} theorem, 36, 64
+ \item {\tt Int_assoc} theorem, 36, 64
+ \item {\tt Int_commute} theorem, 36, 64
+ \item {\tt INT_D} theorem, 63
+ \item {\tt Int_def} theorem, 26, 61
+ \item {\tt INT_E} theorem, 30, 63
+ \item {\tt Int_greatest} theorem, 32, 46, 47, 63
+ \item {\tt INT_I} theorem, 30, 63
+ \item {\tt Int_Inter_image} theorem, 64
+ \item {\tt Int_lower1} theorem, 32, 46, 63
+ \item {\tt Int_lower2} theorem, 32, 46, 63
+ \item {\tt Int_Un_distrib} theorem, 36, 64
+ \item {\tt Int_Union} theorem, 64
+ \item {\tt Int_Union_RepFun} theorem, 36
+ \item {\tt IntD1} theorem, 30, 63
+ \item {\tt IntD2} theorem, 30, 63
+ \item {\tt IntE} theorem, 30, 46, 63
+ \item {\tt INTER} constant, 58
+ \item {\tt Inter} constant, 22, 58
+ \item {\tt INTER1} constant, 58
+ \item {\tt INTER1_def} theorem, 61
+ \item {\tt INTER_def} theorem, 61
+ \item {\tt Inter_def} theorem, 26, 61
+ \item {\tt Inter_greatest} theorem, 32, 63
+ \item {\tt Inter_lower} theorem, 32, 63
+ \item {\tt Inter_Un_distrib} theorem, 36, 64
+ \item {\tt InterD} theorem, 30, 63
+ \item {\tt InterE} theorem, 30, 63
+ \item {\tt InterI} theorem, 28, 30, 63
+ \item {\tt IntI} theorem, 30, 63
+ \item {\tt IntPr.best_tac}, \bold{9}
+ \item {\tt IntPr.fast_tac}, \bold{9}, 11
+ \item {\tt IntPr.inst_step_tac}, \bold{9}
+ \item {\tt IntPr.safe_step_tac}, \bold{9}
+ \item {\tt IntPr.safe_tac}, \bold{9}
+ \item {\tt IntPr.step_tac}, \bold{9}
+ \item {\tt intr_rls}, \bold{115}
+ \item {\tt intr_tac}, \bold{115}, 123, 124
+ \item {\tt intrL_rls}, \bold{115}
+ \item {\tt inv} constant, 64
+ \item {\tt inv_def} theorem, 64
\indexspace
- \item {\tt lam} symbol, 27, 29, 127
- \item {\tt lam_def} theorem, 32
- \item {\tt lam_type} theorem, 40
- \item {\tt Lambda} constant, 26, 30
- \item {\tt lambda} constant, 125, 127
+ \item {\tt lam} symbol, 23, 25, 109
+ \item {\tt lam_def} theorem, 27
+ \item {\tt lam_type} theorem, 34
+ \item {\tt Lambda} constant, 22, 25
+ \item {\tt lambda} constant, 108, 109
\item $\lambda$-abstractions
- \subitem in \CTT, 127
- \subitem in \ZF, 27
- \item {\tt lamE} theorem, 40, 41
- \item {\tt lamI} theorem, 40, 41
- \item {\tt last} constant, 82
+ \subitem in \CTT, 109
+ \subitem in \ZF, 23
+ \item {\tt lamE} theorem, 34, 35
+ \item {\tt lamI} theorem, 34, 35
+ \item {\tt last} constant, 71
\item {\tt LCF} theory, 1
- \item {\tt le_cs}, \bold{24}
- \item {\tt LEAST} constant, 61, 62, 80
- \item {\tt Least} constant, 60
- \item {\tt Least_def} theorem, 64
- \item {\tt left_comp_id} theorem, 46
- \item {\tt left_comp_inverse} theorem, 46
- \item {\tt left_inverse} theorem, 46
- \item {\tt length} constant, 50, 82
- \item {\tt length_def} theorem, 50
- \item {\tt less_induct} theorem, 81
- \item {\tt Let} constant, 25, 26, 60, 63
- \item {\tt let} symbol, 28, 61, 63
- \item {\tt Let_def} theorem, 25, 31, 63, 64
- \item {\tt LFilter} theory, 108
- \item {\tt lfp_def} theorem, 45
- \item {\tt lfp_greatest} theorem, 45
- \item {\tt lfp_lowerbound} theorem, 45
- \item {\tt lfp_mono} theorem, 45
- \item {\tt lfp_subset} theorem, 45
- \item {\tt lfp_Tarski} theorem, 45
- \item {\tt List} theory, 81, 82
- \item {\textit{list}} type, 81
- \item {\tt list} constant, 50
- \item {\tt List.induct} theorem, 50
- \item {\tt list_case} constant, 50
- \item {\tt list_mono} theorem, 50
- \item {\tt list_rec} constant, 50
- \item {\tt list_rec_Cons} theorem, 50
- \item {\tt list_rec_def} theorem, 50
- \item {\tt list_rec_Nil} theorem, 50
- \item {\tt LK} theory, 1, 112, 116
- \item {\tt LK_dup_pack}, \bold{119}, 120
- \item {\tt LK_pack}, \bold{119}
- \item {\tt LList} theory, 108
- \item {\tt logic} class, 5
+ \item {\tt le_cs}, \bold{20}
+ \item {\tt LEAST} constant, 53, 54, 68
+ \item {\tt Least} constant, 52
+ \item {\tt Least_def} theorem, 55
+ \item {\tt left_comp_id} theorem, 40
+ \item {\tt left_comp_inverse} theorem, 40
+ \item {\tt left_inverse} theorem, 40
+ \item {\tt length} constant, 43, 71
+ \item {\tt length_def} theorem, 43
+ \item {\tt less_induct} theorem, 70
+ \item {\tt Let} constant, 21, 22, 52, 54
+ \item {\tt let} symbol, 24, 53, 54
+ \item {\tt Let_def} theorem, 21, 26, 54, 55
+ \item {\tt LFilter} theory, 93
+ \item {\tt lfp_def} theorem, 39
+ \item {\tt lfp_greatest} theorem, 39
+ \item {\tt lfp_lowerbound} theorem, 39
+ \item {\tt lfp_mono} theorem, 39
+ \item {\tt lfp_subset} theorem, 39
+ \item {\tt lfp_Tarski} theorem, 39
+ \item {\tt List} theory, 70, 71
+ \item {\textit{list}} type, 70
+ \item {\tt list} constant, 43
+ \item {\tt List.induct} theorem, 43
+ \item {\tt list_case} constant, 43
+ \item {\tt list_mono} theorem, 43
+ \item {\tt list_rec} constant, 43
+ \item {\tt list_rec_Cons} theorem, 43
+ \item {\tt list_rec_def} theorem, 43
+ \item {\tt list_rec_Nil} theorem, 43
+ \item {\tt LK} theory, 1, 97, 99
+ \item {\tt LK_dup_pack}, \bold{103}, 104
+ \item {\tt LK_pack}, \bold{103}
+ \item {\tt LList} theory, 93
+ \item {\tt logic} class, 4
\indexspace
- \item {\tt map} constant, 50, 82
- \item {\tt map_app_distrib} theorem, 50
- \item {\tt map_compose} theorem, 50
- \item {\tt map_def} theorem, 50
- \item {\tt map_flat} theorem, 50
- \item {\tt map_ident} theorem, 50
- \item {\tt map_type} theorem, 50
- \item {\tt max} constant, 61, 80
- \item {\tt mem} symbol, 82
- \item {\tt mem_asym} theorem, 36, 37
- \item {\tt mem_Collect_eq} theorem, 70, 71
- \item {\tt mem_irrefl} theorem, 36
- \item {\tt min} constant, 61, 80
- \item {\tt minus} class, 61
- \item {\tt mod} symbol, 48, 79, 136
- \item {\tt mod_def} theorem, 48, 136
- \item {\tt mod_geq} theorem, 80
- \item {\tt mod_less} theorem, 80
- \item {\tt mod_quo_equality} theorem, 48
+ \item {\tt map} constant, 43, 71
+ \item {\tt map_app_distrib} theorem, 43
+ \item {\tt map_compose} theorem, 43
+ \item {\tt map_def} theorem, 43
+ \item {\tt map_flat} theorem, 43
+ \item {\tt map_ident} theorem, 43
+ \item {\tt map_type} theorem, 43
+ \item {\tt max} constant, 53, 68
+ \item {\tt mem} symbol, 71
+ \item {\tt mem_asym} theorem, 31
+ \item {\tt mem_Collect_eq} theorem, 61
+ \item {\tt mem_irrefl} theorem, 31
+ \item {\tt min} constant, 53, 68
+ \item {\tt minus} class, 53
+ \item {\tt mod} symbol, 41, 69, 118
+ \item {\tt mod_def} theorem, 41, 118
+ \item {\tt mod_geq} theorem, 69
+ \item {\tt mod_less} theorem, 69
+ \item {\tt mod_quo_equality} theorem, 41
\item {\tt Modal} theory, 1
- \item {\tt mono} constant, 61
- \item {\tt mp} theorem, 8, 63
- \item {\tt mp_tac}, \bold{10}, \bold{134}
- \item {\tt mult_0} theorem, 48
- \item {\tt mult_assoc} theorem, 48, 136
- \item {\tt mult_commute} theorem, 48, 136
- \item {\tt mult_def} theorem, 48, 136
- \item {\tt mult_succ} theorem, 48
- \item {\tt mult_type} theorem, 48
- \item {\tt mult_typing} theorem, 136
- \item {\tt multC0} theorem, 136
- \item {\tt multC_succ} theorem, 136
- \item {\tt mutual_induct_tac}, \bold{93}
+ \item {\tt mono} constant, 53
+ \item {\tt mp} theorem, 6, 55
+ \item {\tt mp_tac}, \bold{8}, \bold{116}
+ \item {\tt mult_0} theorem, 41
+ \item {\tt mult_assoc} theorem, 41, 118
+ \item {\tt mult_commute} theorem, 41, 118
+ \item {\tt mult_def} theorem, 41, 118
+ \item {\tt mult_succ} theorem, 41
+ \item {\tt mult_type} theorem, 41
+ \item {\tt mult_typing} theorem, 118
+ \item {\tt multC0} theorem, 118
+ \item {\tt multC_succ} theorem, 118
+ \item {\tt mutual_induct_tac}, \bold{81}
\indexspace
- \item {\tt N} constant, 125
- \item {\tt n_not_Suc_n} theorem, 79
- \item {\tt Nat} theory, 47, 80
- \item {\textit {nat}} type, 79, 80
- \item {\textit{nat}} type, 78--81
- \item {\tt nat} constant, 48
- \item {\tt nat_0I} theorem, 48
- \item {\tt nat_case} constant, 48
- \item {\tt nat_case_0} theorem, 48
- \item {\tt nat_case_def} theorem, 48
- \item {\tt nat_case_succ} theorem, 48
- \item {\tt nat_def} theorem, 48
- \item {\tt nat_induct} theorem, 48, 79
- \item {\tt nat_rec} constant, 80
- \item {\tt nat_succI} theorem, 48
- \item {\tt NatDef} theory, 78
- \item {\tt NC0} theorem, 129
- \item {\tt NC_succ} theorem, 129
- \item {\tt NE} theorem, 128, 129, 137
- \item {\tt NEL} theorem, 129
- \item {\tt NF} theorem, 129, 138
- \item {\tt NI0} theorem, 129
- \item {\tt NI_succ} theorem, 129
- \item {\tt NI_succL} theorem, 129
- \item {\tt Nil_Cons_iff} theorem, 50
- \item {\tt NilI} theorem, 50
- \item {\tt NIO} theorem, 137
- \item {\tt Not} constant, 7, 60, 113
- \item {\tt not_def} theorem, 8, 43, 64
- \item {\tt not_impE} theorem, 9
- \item {\tt not_sym} theorem, 65
- \item {\tt notE} theorem, 9, 10, 65
- \item {\tt notI} theorem, 9, 65
- \item {\tt notL} theorem, 115
- \item {\tt notnotD} theorem, 11, 66
- \item {\tt notR} theorem, 115
- \item {\tt null} constant, 82
+ \item {\tt N} constant, 108
+ \item {\tt n_not_Suc_n} theorem, 69
+ \item {\tt Nat} theory, 38, 68
+ \item {\textit {nat}} type, 68, 69
+ \item {\textit{nat}} type, 68--70
+ \item {\tt nat} constant, 41
+ \item {\tt nat_0I} theorem, 41
+ \item {\tt nat_case} constant, 41
+ \item {\tt nat_case_0} theorem, 41
+ \item {\tt nat_case_def} theorem, 41
+ \item {\tt nat_case_succ} theorem, 41
+ \item {\tt nat_def} theorem, 41
+ \item {\tt nat_induct} theorem, 41, 69
+ \item {\tt nat_rec} constant, 70
+ \item {\tt nat_succI} theorem, 41
+ \item {\tt NatDef} theory, 68
+ \item {\tt NC0} theorem, 111
+ \item {\tt NC_succ} theorem, 111
+ \item {\tt NE} theorem, 111, 114, 119
+ \item {\tt NEL} theorem, 111
+ \item {\tt NF} theorem, 111, 119
+ \item {\tt NI0} theorem, 111
+ \item {\tt NI_succ} theorem, 111
+ \item {\tt NI_succL} theorem, 111
+ \item {\tt Nil_Cons_iff} theorem, 43
+ \item {\tt NilI} theorem, 43
+ \item {\tt NIO} theorem, 119
+ \item {\tt Not} constant, 5, 52, 98
+ \item {\tt not_def} theorem, 6, 36, 55
+ \item {\tt not_impE} theorem, 7
+ \item {\tt not_sym} theorem, 56
+ \item {\tt notE} theorem, 7, 8, 56
+ \item {\tt notI} theorem, 7, 56
+ \item {\tt notL} theorem, 100
+ \item {\tt notnotD} theorem, 9, 57
+ \item {\tt notR} theorem, 100
+ \item {\tt null} constant, 71
\indexspace
- \item {\tt O} symbol, 46
- \item {\textit {o}} type, 5, 112
- \item {\tt o} symbol, 60, 71
- \item {\tt o_def} theorem, 64
- \item {\tt of} symbol, 63
- \item {\tt or_def} theorem, 43, 64
- \item {\tt Ord} theory, 61
- \item {\tt ord} class, 61, 62, 80
- \item {\tt order} class, 61, 80
+ \item {\tt O} symbol, 40
+ \item {\textit {o}} type, 4, 97
+ \item {\tt o} symbol, 52, 65
+ \item {\tt o_def} theorem, 55
+ \item {\tt of} symbol, 54
+ \item {\tt or_def} theorem, 36, 55
+ \item {\tt Ord} theory, 53
+ \item {\tt ord} class, 53, 54, 68
+ \item {\tt order} class, 53, 68
\indexspace
- \item {\tt pack} ML type, 118
- \item {\tt Pair} constant, 26, 27, 77
- \item {\tt pair} constant, 125
- \item {\tt Pair_def} theorem, 32
- \item {\tt Pair_eq} theorem, 77
- \item {\tt Pair_inject} theorem, 38, 77
- \item {\tt Pair_inject1} theorem, 38
- \item {\tt Pair_inject2} theorem, 38
- \item {\tt Pair_neq_0} theorem, 38
- \item {\tt PairE} theorem, 77
- \item {\tt pairing} theorem, 35
- \item {\tt pc_tac}, \bold{120}, \bold{135}, 141, 142
- \item {\tt Perm} theory, 43
- \item {\tt Pi} constant, 26, 29, 41
- \item {\tt Pi_def} theorem, 32
- \item {\tt Pi_type} theorem, 40, 41
- \item {\tt plus} class, 61
- \item {\tt PlusC_inl} theorem, 131
- \item {\tt PlusC_inr} theorem, 131
- \item {\tt PlusE} theorem, 131, 135, 139
- \item {\tt PlusEL} theorem, 131
- \item {\tt PlusF} theorem, 131
- \item {\tt PlusFL} theorem, 131
- \item {\tt PlusI_inl} theorem, 131, 140
- \item {\tt PlusI_inlL} theorem, 131
- \item {\tt PlusI_inr} theorem, 131
- \item {\tt PlusI_inrL} theorem, 131
- \item {\tt Pow} constant, 26, 68
- \item {\tt Pow_def} theorem, 71
- \item {\tt Pow_iff} theorem, 31
- \item {\tt Pow_mono} theorem, 53
- \item {\tt PowD} theorem, 34, 54, 73
- \item {\tt PowI} theorem, 34, 54, 73
- \item {\tt primrec}, 98--101
- \item {\tt primrec} symbol, 80
- \item {\tt PrimReplace} constant, 26, 30
+ \item {\tt pack} ML type, 102
+ \item {\tt Pair} constant, 21, 22, 67
+ \item {\tt pair} constant, 108
+ \item {\tt Pair_def} theorem, 27
+ \item {\tt Pair_eq} theorem, 67
+ \item {\tt Pair_inject} theorem, 32, 33, 67
+ \item {\tt Pair_inject1} theorem, 32, 33
+ \item {\tt Pair_inject2} theorem, 32, 33
+ \item {\tt Pair_neq_0} theorem, 32, 33
+ \item {\tt PairE} theorem, 67
+ \item {\tt pairing} theorem, 30
+ \item {\tt pc_tac}, \bold{103}, \bold{117}, 122, 123
+ \item {\tt Perm} theory, 38
+ \item {\tt Pi} constant, 22, 23, 35
+ \item {\tt Pi_def} theorem, 27
+ \item {\tt Pi_type} theorem, 34, 35
+ \item {\tt plus} class, 53
+ \item {\tt PlusC_inl} theorem, 112
+ \item {\tt PlusC_inr} theorem, 112
+ \item {\tt PlusE} theorem, 112, 117, 121
+ \item {\tt PlusEL} theorem, 112
+ \item {\tt PlusF} theorem, 112
+ \item {\tt PlusFL} theorem, 112
+ \item {\tt PlusI_inl} theorem, 112, 121
+ \item {\tt PlusI_inlL} theorem, 112
+ \item {\tt PlusI_inr} theorem, 112
+ \item {\tt PlusI_inrL} theorem, 112
+ \item {\tt Pow} constant, 22, 58
+ \item {\tt Pow_def} theorem, 61
+ \item {\tt Pow_iff} theorem, 26
+ \item {\tt Pow_mono} theorem, 45
+ \item {\tt PowD} theorem, 29, 46, 63
+ \item {\tt PowI} theorem, 29, 46, 63
+ \item {\tt primrec}, 85--88
+ \item {\tt primrec} symbol, 68
+ \item {\tt PrimReplace} constant, 22, 25
\item priorities, 2
- \item {\tt PROD} symbol, 27, 29, 126, 127
- \item {\tt Prod} constant, 125
- \item {\tt Prod} theory, 77
- \item {\tt ProdC} theorem, 129, 145
- \item {\tt ProdC2} theorem, 129
- \item {\tt ProdE} theorem, 129, 142, 144, 146
- \item {\tt ProdEL} theorem, 129
- \item {\tt ProdF} theorem, 129
- \item {\tt ProdFL} theorem, 129
- \item {\tt ProdI} theorem, 129, 135, 137
- \item {\tt ProdIL} theorem, 129
- \item {\tt prop_cs}, \bold{11}, \bold{76}
- \item {\tt prop_pack}, \bold{118}
+ \item {\tt PROD} symbol, 23, 109, 110
+ \item {\tt Prod} constant, 108
+ \item {\tt Prod} theory, 66
+ \item {\tt ProdC} theorem, 111, 125
+ \item {\tt ProdC2} theorem, 111
+ \item {\tt ProdE} theorem, 111, 123, 124, 126
+ \item {\tt ProdEL} theorem, 111
+ \item {\tt ProdF} theorem, 111
+ \item {\tt ProdFL} theorem, 111
+ \item {\tt ProdI} theorem, 111, 117, 119
+ \item {\tt ProdIL} theorem, 111
+ \item {\tt prop_cs}, \bold{9}, \bold{66}
+ \item {\tt prop_pack}, \bold{102}
\indexspace
- \item {\tt qcase_def} theorem, 44
- \item {\tt qconverse} constant, 43
- \item {\tt qconverse_def} theorem, 44
- \item {\tt qed_spec_mp}, 96
- \item {\tt qfsplit_def} theorem, 44
- \item {\tt QInl_def} theorem, 44
- \item {\tt QInr_def} theorem, 44
- \item {\tt QPair} theory, 43
- \item {\tt QPair_def} theorem, 44
- \item {\tt QSigma} constant, 43
- \item {\tt QSigma_def} theorem, 44
- \item {\tt qsplit} constant, 43
- \item {\tt qsplit_def} theorem, 44
- \item {\tt qsum_def} theorem, 44
- \item {\tt QUniv} theory, 47
+ \item {\tt qcase_def} theorem, 37
+ \item {\tt qconverse} constant, 35
+ \item {\tt qconverse_def} theorem, 37
+ \item {\tt qed_spec_mp}, 84
+ \item {\tt qfsplit_def} theorem, 37
+ \item {\tt QInl_def} theorem, 37
+ \item {\tt QInr_def} theorem, 37
+ \item {\tt QPair} theory, 35
+ \item {\tt QPair_def} theorem, 37
+ \item {\tt QSigma} constant, 35
+ \item {\tt QSigma_def} theorem, 37
+ \item {\tt qsplit} constant, 35
+ \item {\tt qsplit_def} theorem, 37
+ \item {\tt qsum_def} theorem, 37
+ \item {\tt QUniv} theory, 38
\indexspace
- \item {\tt range} constant, 26, 68, 109
- \item {\tt range_def} theorem, 32, 71
- \item {\tt range_of_fun} theorem, 40, 41
- \item {\tt range_subset} theorem, 39
- \item {\tt range_type} theorem, 40
- \item {\tt rangeE} theorem, 39, 73, 110
- \item {\tt rangeI} theorem, 39, 73
- \item {\tt rank} constant, 49
- \item {\tt rank_ss}, \bold{24}
- \item {\tt rec} constant, 48, 125, 128
- \item {\tt rec_0} theorem, 48
- \item {\tt rec_def} theorem, 48
- \item {\tt rec_succ} theorem, 48
- \item {\tt recdef}, 101--104
- \item {\tt record}, 87
- \item {\tt record_split_tac}, 89
+ \item {\tt range} constant, 22, 58, 94
+ \item {\tt range_def} theorem, 27, 61
+ \item {\tt range_of_fun} theorem, 34, 35
+ \item {\tt range_subset} theorem, 33
+ \item {\tt range_type} theorem, 34
+ \item {\tt rangeE} theorem, 33, 63, 95
+ \item {\tt rangeI} theorem, 33, 63
+ \item {\tt rank} constant, 42
+ \item {\tt rank_ss}, \bold{20}
+ \item {\tt rec} constant, 41, 108, 114
+ \item {\tt rec_0} theorem, 41
+ \item {\tt rec_def} theorem, 41
+ \item {\tt rec_succ} theorem, 41
+ \item {\tt recdef}, 88--90
+ \item {\tt record}, 75
+ \item {\tt record_split_tac}, 77
\item recursion
- \subitem general, 101--104
- \subitem primitive, 98--101
- \item recursive functions, \see{recursion}{97}
- \item {\tt red_if_equal} theorem, 128
- \item {\tt Reduce} constant, 125, 128, 134
- \item {\tt refl} theorem, 8, 63, 115
- \item {\tt refl_elem} theorem, 128, 132
- \item {\tt refl_red} theorem, 128
- \item {\tt refl_type} theorem, 128, 132
- \item {\tt REPEAT_FIRST}, 133
- \item {\tt repeat_goal_tac}, \bold{120}
- \item {\tt RepFun} constant, 26, 29, 30, 33
- \item {\tt RepFun_def} theorem, 31
- \item {\tt RepFunE} theorem, 35
- \item {\tt RepFunI} theorem, 35
- \item {\tt Replace} constant, 26, 29, 30, 33
- \item {\tt Replace_def} theorem, 31
- \item {\tt replace_type} theorem, 132, 144
- \item {\tt ReplaceE} theorem, 35
- \item {\tt ReplaceI} theorem, 35
- \item {\tt replacement} theorem, 31
- \item {\tt reresolve_tac}, \bold{120}
- \item {\tt res_inst_tac}, 62
- \item {\tt restrict} constant, 26, 33
- \item {\tt restrict} theorem, 40
- \item {\tt restrict_bij} theorem, 46
- \item {\tt restrict_def} theorem, 32
- \item {\tt restrict_type} theorem, 40
- \item {\tt rev} constant, 50, 82
- \item {\tt rev_def} theorem, 50
- \item {\tt rew_tac}, 19, \bold{134}
- \item {\tt rewrite_rule}, 19
- \item {\tt right_comp_id} theorem, 46
- \item {\tt right_comp_inverse} theorem, 46
- \item {\tt right_inverse} theorem, 46
- \item {\tt RL}, 139
- \item {\tt RS}, 144, 146
+ \subitem general, 88--90
+ \subitem primitive, 85--88
+ \item recursive functions, \see{recursion}{85}
+ \item {\tt red_if_equal} theorem, 110
+ \item {\tt Reduce} constant, 108, 114, 116
+ \item {\tt refl} theorem, 6, 55, 100
+ \item {\tt refl_elem} theorem, 110, 115
+ \item {\tt refl_red} theorem, 110
+ \item {\tt refl_type} theorem, 110, 115
+ \item {\tt REPEAT_FIRST}, 115
+ \item {\tt repeat_goal_tac}, \bold{103}
+ \item {\tt RepFun} constant, 22, 23, 25, 28
+ \item {\tt RepFun_def} theorem, 26
+ \item {\tt RepFunE} theorem, 30
+ \item {\tt RepFunI} theorem, 30
+ \item {\tt Replace} constant, 22, 23, 25, 28
+ \item {\tt Replace_def} theorem, 26
+ \item {\tt replace_type} theorem, 113, 125
+ \item {\tt ReplaceE} theorem, 30
+ \item {\tt ReplaceI} theorem, 30
+ \item {\tt replacement} theorem, 26
+ \item {\tt reresolve_tac}, \bold{103}
+ \item {\tt res_inst_tac}, 53
+ \item {\tt restrict} constant, 22, 28
+ \item {\tt restrict} theorem, 34
+ \item {\tt restrict_bij} theorem, 40
+ \item {\tt restrict_def} theorem, 27
+ \item {\tt restrict_type} theorem, 34
+ \item {\tt rev} constant, 43, 71
+ \item {\tt rev_def} theorem, 43
+ \item {\tt rew_tac}, 16, \bold{116}
+ \item {\tt rewrite_rule}, 16
+ \item {\tt right_comp_id} theorem, 40
+ \item {\tt right_comp_inverse} theorem, 40
+ \item {\tt right_inverse} theorem, 40
+ \item {\tt RL}, 121
+ \item {\tt RS}, 124, 126
\indexspace
- \item {\tt safe_goal_tac}, \bold{120}
- \item {\tt safe_tac}, \bold{135}
- \item {\tt safestep_tac}, \bold{135}
+ \item {\tt safe_goal_tac}, \bold{104}
+ \item {\tt safe_tac}, \bold{117}
+ \item {\tt safestep_tac}, \bold{117}
\item search
- \subitem best-first, 111
- \item {\tt select_equality} theorem, 64, 66
- \item {\tt selectI} theorem, 63, 64
- \item {\tt separation} theorem, 35
- \item {\tt Seqof} constant, 113
- \item sequent calculus, 112--123
- \item {\tt Set} theory, 67, 70
- \item {\tt set} constant, 82
- \item {\tt set} type, 67
- \item set theory, 24--58
- \item {\tt set_current_thy}, 111
- \item {\tt set_diff_def} theorem, 71
- \item {\tt show_sorts}, 62
- \item {\tt show_types}, 62
- \item {\tt Sigma} constant, 26, 29, 30, 38, 77
- \item {\tt Sigma_def} theorem, 32, 77
- \item {\tt SigmaE} theorem, 38, 77
- \item {\tt SigmaE2} theorem, 38
- \item {\tt SigmaI} theorem, 38, 77
+ \subitem best-first, 96
+ \item {\tt select_equality} theorem, 55, 57
+ \item {\tt selectI} theorem, 55
+ \item {\tt separation} theorem, 30
+ \item {\tt Seqof} constant, 98
+ \item sequent calculus, 97--106
+ \item {\tt Set} theory, 60, 61
+ \item {\tt set} constant, 71
+ \item {\tt set} type, 60
+ \item set theory, 20--50
+ \item {\tt set_current_thy}, 96
+ \item {\tt set_diff_def} theorem, 61
+ \item {\tt show_sorts}, 53
+ \item {\tt show_types}, 53
+ \item {\tt Sigma} constant, 22, 23, 25, 33, 67
+ \item {\tt Sigma_def} theorem, 27, 67
+ \item {\tt SigmaE} theorem, 32, 33, 67
+ \item {\tt SigmaE2} theorem, 32, 33
+ \item {\tt SigmaI} theorem, 32, 33, 67
\item simplification
- \subitem of conjunctions, 6, 75
- \item {\tt singletonE} theorem, 36
- \item {\tt singletonI} theorem, 36
- \item {\tt size} constant, 93
- \item {\tt snd} constant, 26, 33, 77, 125, 130
- \item {\tt snd_conv} theorem, 38, 77
- \item {\tt snd_def} theorem, 32, 130
- \item {\tt sobj} type, 116
- \item {\tt spec} theorem, 8, 66
- \item {\tt split} constant, 26, 33, 77, 125, 139
- \item {\tt split} theorem, 38, 77
- \item {\tt split_all_tac}, \bold{78}
- \item {\tt split_def} theorem, 32
- \item {\tt split_if} theorem, 66, 76
- \item {\tt split_list_case} theorem, 81
- \item {\tt split_split} theorem, 77
- \item {\tt split_sum_case} theorem, 79
- \item {\tt ssubst} theorem, 9, 65, 67
- \item {\tt stac}, \bold{75}
- \item {\tt Step_tac}, 22
- \item {\tt step_tac}, 23, \bold{120}, \bold{135}
- \item {\tt strip_tac}, \bold{67}
- \item {\tt subset_def} theorem, 31, 71
- \item {\tt subset_refl} theorem, 34, 72
- \item {\tt subset_trans} theorem, 34, 72
- \item {\tt subsetCE} theorem, 34, 70, 72
- \item {\tt subsetD} theorem, 34, 56, 70, 72
- \item {\tt subsetI} theorem, 34, 54, 55, 72
- \item {\tt subst} theorem, 8, 63
- \item {\tt subst_elem} theorem, 128
- \item {\tt subst_elemL} theorem, 128
- \item {\tt subst_eqtyparg} theorem, 132, 144
- \item {\tt subst_prodE} theorem, 130, 132
- \item {\tt subst_type} theorem, 128
- \item {\tt subst_typeL} theorem, 128
- \item {\tt Suc} constant, 79
- \item {\tt Suc_not_Zero} theorem, 79
- \item {\tt succ} constant, 26, 30, 125
- \item {\tt succ_def} theorem, 32
- \item {\tt succ_inject} theorem, 36
- \item {\tt succ_neq_0} theorem, 36
- \item {\tt succCI} theorem, 36
- \item {\tt succE} theorem, 36
- \item {\tt succI1} theorem, 36
- \item {\tt succI2} theorem, 36
- \item {\tt SUM} symbol, 27, 29, 126, 127
- \item {\tt Sum} constant, 125
- \item {\tt Sum} theory, 43, 78
- \item {\tt sum_case} constant, 79
- \item {\tt sum_case_Inl} theorem, 79
- \item {\tt sum_case_Inr} theorem, 79
- \item {\tt sum_def} theorem, 44
- \item {\tt sum_InlI} theorem, 44
- \item {\tt sum_InrI} theorem, 44
- \item {\tt SUM_Int_distrib1} theorem, 42
- \item {\tt SUM_Int_distrib2} theorem, 42
- \item {\tt SUM_Un_distrib1} theorem, 42
- \item {\tt SUM_Un_distrib2} theorem, 42
- \item {\tt SumC} theorem, 130
- \item {\tt SumE} theorem, 130, 135, 139
- \item {\tt sumE} theorem, 79
- \item {\tt sumE2} theorem, 44
- \item {\tt SumE_fst} theorem, 130, 132, 144, 145
- \item {\tt SumE_snd} theorem, 130, 132, 146
- \item {\tt SumEL} theorem, 130
- \item {\tt SumF} theorem, 130
- \item {\tt SumFL} theorem, 130
- \item {\tt SumI} theorem, 130, 140
- \item {\tt SumIL} theorem, 130
- \item {\tt SumIL2} theorem, 132
- \item {\tt surj} constant, 46, 71, 75
- \item {\tt surj_def} theorem, 46, 75
- \item {\tt surjective_pairing} theorem, 77
- \item {\tt surjective_sum} theorem, 79
- \item {\tt swap} theorem, 11, 66
- \item {\tt swap_res_tac}, 16, 111
- \item {\tt sym} theorem, 9, 65, 115
- \item {\tt sym_elem} theorem, 128
- \item {\tt sym_type} theorem, 128
- \item {\tt symL} theorem, 116
+ \subitem of conjunctions, 8, 65
+ \item {\tt singletonE} theorem, 31
+ \item {\tt singletonI} theorem, 31
+ \item {\tt size} constant, 81
+ \item {\tt snd} constant, 22, 28, 67, 108, 114
+ \item {\tt snd_conv} theorem, 32, 67
+ \item {\tt snd_def} theorem, 27, 112
+ \item {\tt sobj} type, 99
+ \item {\tt spec} theorem, 6, 57
+ \item {\tt split} constant, 22, 28, 67, 108, 121
+ \item {\tt split} theorem, 32, 67
+ \item {\tt split_all_tac}, \bold{67}
+ \item {\tt split_def} theorem, 27
+ \item {\tt split_if} theorem, 57, 65
+ \item {\tt split_list_case} theorem, 70
+ \item {\tt split_split} theorem, 67
+ \item {\tt split_sum_case} theorem, 68
+ \item {\tt ssubst} theorem, 7, 55, 56
+ \item {\tt stac}, \bold{65}
+ \item {\tt Step_tac}, 18
+ \item {\tt step_tac}, 19, \bold{104}, \bold{117}
+ \item {\tt strip_tac}, \bold{58}
+ \item {\tt subset_def} theorem, 26, 61
+ \item {\tt subset_refl} theorem, 29, 62
+ \item {\tt subset_trans} theorem, 29, 62
+ \item {\tt subsetCE} theorem, 29, 61, 62
+ \item {\tt subsetD} theorem, 29, 48, 61, 62
+ \item {\tt subsetI} theorem, 29, 46, 47, 62
+ \item {\tt subst} theorem, 6, 55
+ \item {\tt subst_elem} theorem, 110
+ \item {\tt subst_elemL} theorem, 110
+ \item {\tt subst_eqtyparg} theorem, 113, 125
+ \item {\tt subst_prodE} theorem, 113, 114
+ \item {\tt subst_type} theorem, 110
+ \item {\tt subst_typeL} theorem, 110
+ \item {\tt Suc} constant, 69
+ \item {\tt Suc_not_Zero} theorem, 69
+ \item {\tt succ} constant, 22, 25, 108
+ \item {\tt succ_def} theorem, 27
+ \item {\tt succ_inject} theorem, 31
+ \item {\tt succ_neq_0} theorem, 31
+ \item {\tt succCI} theorem, 31
+ \item {\tt succE} theorem, 31
+ \item {\tt succI1} theorem, 31
+ \item {\tt succI2} theorem, 31
+ \item {\tt SUM} symbol, 23, 109, 110
+ \item {\tt Sum} constant, 108
+ \item {\tt Sum} theory, 35, 68
+ \item {\tt sum_case} constant, 68
+ \item {\tt sum_case_Inl} theorem, 68
+ \item {\tt sum_case_Inr} theorem, 68
+ \item {\tt sum_def} theorem, 37
+ \item {\tt sum_InlI} theorem, 37
+ \item {\tt sum_InrI} theorem, 37
+ \item {\tt SUM_Int_distrib1} theorem, 36
+ \item {\tt SUM_Int_distrib2} theorem, 36
+ \item {\tt SUM_Un_distrib1} theorem, 36
+ \item {\tt SUM_Un_distrib2} theorem, 36
+ \item {\tt SumC} theorem, 112
+ \item {\tt SumE} theorem, 112, 117, 121
+ \item {\tt sumE} theorem, 68
+ \item {\tt sumE2} theorem, 37
+ \item {\tt SumE_fst} theorem, 113, 114, 124, 126
+ \item {\tt SumE_snd} theorem, 113, 114, 126
+ \item {\tt SumEL} theorem, 112
+ \item {\tt SumF} theorem, 112
+ \item {\tt SumFL} theorem, 112
+ \item {\tt SumI} theorem, 112, 121
+ \item {\tt SumIL} theorem, 112
+ \item {\tt SumIL2} theorem, 113
+ \item {\tt surj} constant, 40, 64, 65
+ \item {\tt surj_def} theorem, 40, 64
+ \item {\tt surjective_pairing} theorem, 67
+ \item {\tt surjective_sum} theorem, 68
+ \item {\tt swap} theorem, 9, 57
+ \item {\tt swap_res_tac}, 13, 95
+ \item {\tt sym} theorem, 7, 56, 100
+ \item {\tt sym_elem} theorem, 110
+ \item {\tt sym_type} theorem, 110
+ \item {\tt symL} theorem, 101
\indexspace
- \item {\tt T} constant, 125
- \item {\textit {t}} type, 124
- \item {\tt take} constant, 82
- \item {\tt takeWhile} constant, 82
- \item {\tt TC} theorem, 131
- \item {\tt TE} theorem, 131
- \item {\tt TEL} theorem, 131
- \item {\tt term} class, 5, 61, 112
- \item {\tt test_assume_tac}, \bold{133}
- \item {\tt TF} theorem, 131
- \item {\tt THE} symbol, 27, 29, 37, 113
- \item {\tt The} constant, 26, 29, 30, 113
- \item {\tt The} theorem, 115
- \item {\tt the_def} theorem, 31
- \item {\tt the_equality} theorem, 36, 37
- \item {\tt theI} theorem, 36, 37
- \item {\tt thinL} theorem, 115
- \item {\tt thinR} theorem, 115
- \item {\tt TI} theorem, 131
- \item {\tt times} class, 61
- \item {\tt tl} constant, 82
+ \item {\tt T} constant, 108
+ \item {\textit {t}} type, 107
+ \item {\tt take} constant, 71
+ \item {\tt takeWhile} constant, 71
+ \item {\tt TC} theorem, 113
+ \item {\tt TE} theorem, 113
+ \item {\tt TEL} theorem, 113
+ \item {\tt term} class, 4, 51, 97
+ \item {\tt test_assume_tac}, \bold{115}
+ \item {\tt TF} theorem, 113
+ \item {\tt THE} symbol, 23, 31, 98
+ \item {\tt The} constant, 22, 25, 98
+ \item {\tt The} theorem, 100
+ \item {\tt the_def} theorem, 26
+ \item {\tt the_equality} theorem, 31
+ \item {\tt theI} theorem, 31
+ \item {\tt thinL} theorem, 100
+ \item {\tt thinR} theorem, 100
+ \item {\tt TI} theorem, 113
+ \item {\tt times} class, 53
+ \item {\tt tl} constant, 71
\item tracing
- \subitem of unification, 62
- \item {\tt trans} theorem, 9, 65, 115
- \item {\tt trans_elem} theorem, 128
- \item {\tt trans_red} theorem, 128
- \item {\tt trans_tac}, 81
- \item {\tt trans_type} theorem, 128
- \item {\tt True} constant, 7, 60, 113
- \item {\tt True_def} theorem, 8, 64, 115
- \item {\tt True_or_False} theorem, 63, 64
- \item {\tt TrueI} theorem, 9, 65
- \item {\tt Trueprop} constant, 7, 60, 113
- \item {\tt TrueR} theorem, 116
- \item {\tt tt} constant, 125
- \item {\tt Type} constant, 125
- \item type definition, \bold{84}
- \item {\tt typechk_tac}, \bold{133}, 138, 141, 145, 146
- \item {\tt typedef}, 81
+ \subitem of unification, 53
+ \item {\tt trans} theorem, 7, 56, 100
+ \item {\tt trans_elem} theorem, 110
+ \item {\tt trans_red} theorem, 110
+ \item {\tt trans_tac}, 70
+ \item {\tt trans_type} theorem, 110
+ \item {\tt True} constant, 5, 52, 98
+ \item {\tt True_def} theorem, 6, 55, 100
+ \item {\tt True_or_False} theorem, 55
+ \item {\tt TrueI} theorem, 7, 56
+ \item {\tt Trueprop} constant, 5, 52, 98
+ \item {\tt TrueR} theorem, 101
+ \item {\tt tt} constant, 108
+ \item {\tt Type} constant, 108
+ \item type definition, \bold{73}
+ \item {\tt typechk_tac}, \bold{115}, 119, 122, 126
+ \item {\tt typedef}, 70
\indexspace
- \item {\tt UN} symbol, 27, 29, 68--70
- \item {\tt Un} symbol, 26, 68
- \item {\tt Un1} theorem, 70
- \item {\tt Un2} theorem, 70
- \item {\tt Un_absorb} theorem, 42, 74
- \item {\tt Un_assoc} theorem, 42, 74
- \item {\tt Un_commute} theorem, 42, 74
- \item {\tt Un_def} theorem, 31, 71
- \item {\tt UN_E} theorem, 35, 73
- \item {\tt UN_I} theorem, 35, 73
- \item {\tt Un_Int_distrib} theorem, 42, 74
- \item {\tt Un_Inter} theorem, 74
- \item {\tt Un_Inter_RepFun} theorem, 42
- \item {\tt Un_least} theorem, 37, 74
- \item {\tt Un_Union_image} theorem, 74
- \item {\tt Un_upper1} theorem, 37, 74
- \item {\tt Un_upper2} theorem, 37, 74
- \item {\tt UnCI} theorem, 36, 37, 70, 73
- \item {\tt UnE} theorem, 36, 73
- \item {\tt UnI1} theorem, 36, 37, 57, 73
- \item {\tt UnI2} theorem, 36, 37, 73
+ \item {\tt UN} symbol, 23, 58--60
+ \item {\tt Un} symbol, 22, 58
+ \item {\tt Un1} theorem, 61
+ \item {\tt Un2} theorem, 61
+ \item {\tt Un_absorb} theorem, 36, 64
+ \item {\tt Un_assoc} theorem, 36, 64
+ \item {\tt Un_commute} theorem, 36, 64
+ \item {\tt Un_def} theorem, 26, 61
+ \item {\tt UN_E} theorem, 30, 63
+ \item {\tt UN_I} theorem, 30, 63
+ \item {\tt Un_Int_distrib} theorem, 36, 64
+ \item {\tt Un_Inter} theorem, 64
+ \item {\tt Un_Inter_RepFun} theorem, 36
+ \item {\tt Un_least} theorem, 32, 63
+ \item {\tt Un_Union_image} theorem, 64
+ \item {\tt Un_upper1} theorem, 32, 63
+ \item {\tt Un_upper2} theorem, 32, 63
+ \item {\tt UnCI} theorem, 28, 30, 61, 63
+ \item {\tt UnE} theorem, 30, 63
+ \item {\tt UnI1} theorem, 28, 30, 49, 63
+ \item {\tt UnI2} theorem, 28, 30, 63
\item unification
- \subitem incompleteness of, 62
- \item {\tt Unify.trace_types}, 62
- \item {\tt UNION} constant, 68
- \item {\tt Union} constant, 26, 68
- \item {\tt UNION1} constant, 68
- \item {\tt UNION1_def} theorem, 71
- \item {\tt UNION_def} theorem, 71
- \item {\tt Union_def} theorem, 71
- \item {\tt Union_iff} theorem, 31
- \item {\tt Union_least} theorem, 37, 74
- \item {\tt Union_Un_distrib} theorem, 42, 74
- \item {\tt Union_upper} theorem, 37, 74
- \item {\tt UnionE} theorem, 35, 56, 73
- \item {\tt UnionI} theorem, 35, 56, 73
- \item {\tt unit_eq} theorem, 78
- \item {\tt Univ} theory, 47
- \item {\tt Upair} constant, 25, 26, 30
- \item {\tt Upair_def} theorem, 31
- \item {\tt UpairE} theorem, 35
- \item {\tt UpairI1} theorem, 35
- \item {\tt UpairI2} theorem, 35
+ \subitem incompleteness of, 53
+ \item {\tt Unify.trace_types}, 53
+ \item {\tt UNION} constant, 58
+ \item {\tt Union} constant, 22, 58
+ \item {\tt UNION1} constant, 58
+ \item {\tt UNION1_def} theorem, 61
+ \item {\tt UNION_def} theorem, 61
+ \item {\tt Union_def} theorem, 61
+ \item {\tt Union_iff} theorem, 26
+ \item {\tt Union_least} theorem, 32, 63
+ \item {\tt Union_Un_distrib} theorem, 36, 64
+ \item {\tt Union_upper} theorem, 32, 63
+ \item {\tt UnionE} theorem, 30, 47, 63
+ \item {\tt UnionI} theorem, 30, 48, 63
+ \item {\tt unit_eq} theorem, 67
+ \item {\tt Univ} theory, 38
+ \item {\tt Upair} constant, 21, 22, 25
+ \item {\tt Upair_def} theorem, 26
+ \item {\tt UpairE} theorem, 30
+ \item {\tt UpairI1} theorem, 30
+ \item {\tt UpairI2} theorem, 30
\indexspace
- \item {\tt vimage_def} theorem, 32
- \item {\tt vimageE} theorem, 39
- \item {\tt vimageI} theorem, 39
+ \item {\tt vimage_def} theorem, 27
+ \item {\tt vimageE} theorem, 34
+ \item {\tt vimageI} theorem, 34
\indexspace
- \item {\tt when} constant, 125, 130, 139
+ \item {\tt when} constant, 108, 114, 121
\indexspace
- \item {\tt xor_def} theorem, 43
+ \item {\tt xor_def} theorem, 36
\indexspace
- \item {\tt zero_ne_succ} theorem, 128, 129
- \item {\tt ZF} theory, 1, 24, 59
- \item {\tt ZF_cs}, \bold{24}
- \item {\tt ZF_ss}, \bold{24}
+ \item {\tt zero_ne_succ} theorem, 111, 114
+ \item {\tt ZF} theory, 1, 20, 51
+ \item {\tt ZF_cs}, \bold{20}
+ \item {\tt ZF_ss}, \bold{20}
\end{theindex}