--- a/doc-src/Logics/Old_HOL.tex Tue Jul 12 09:28:00 1994 +0200
+++ b/doc-src/Logics/Old_HOL.tex Tue Jul 12 12:49:15 1994 +0200
@@ -1268,14 +1268,14 @@
\[ c_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \]
These functions have certain {\em freeness} properties:
\begin{description}
+\item[\tt distinct] They are distinct:
+\[ c_i(x_1,\dots,x_{k_i}) \neq c_j(y_1,\dots,y_{k_j}) \qquad
+ \mbox{for all}~ i \neq j.
+\]
\item[\tt inject] They are injective:
\[ (c_j(x_1,\dots,x_{k_j}) = c_j(y_1,\dots,y_{k_j})) =
(x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j})
\]
-\item[\tt ineq] They are distinct:
-\[ c_i(x_1,\dots,x_{k_i}) \neq c_j(y_1,\dots,y_{k_j}) \qquad
- \mbox{for all}~ i \neq j.
-\]
\end{description}
Because the number of inequalities is quadratic in the number of
constructors, a different method is used if their number exceeds
@@ -1288,7 +1288,7 @@
\mbox{\it t\_ord}(c_m(x_1,\dots,x_{k_m})) & = & m-1
\end{array}
\]
-and inequality of constructors is expressed by:
+and distinctness of constructors is expressed by:
\[
\mbox{\it t\_ord}(x) \neq \mbox{\it t\_ord}(y) \Imp x \neq y.
\]
@@ -1309,12 +1309,12 @@
= (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for
all arguments of the recursive type.
-The type also comes with an \ML-like {\tt case}-construct:
+The type also comes with an \ML-like \sdx{case}-construct:
\[
\begin{array}{rrcl}
-\mbox{\tt case}~e~\mbox{\tt of} & c_1(y_{11},\dots,y_{1k_1}) & \To & e_1 \\
+\mbox{\tt case}~e~\mbox{\tt of} & c_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\
\vdots \\
- \mid & c_m(y_{m1},\dots,y_{mk_m}) & \To & e_m
+ \mid & c_m(x_{m1},\dots,x_{mk_m}) & \To & e_m
\end{array}
\]
In contrast to \ML, {\em all} constructors must be present, their order is
@@ -1346,27 +1346,28 @@
\label{datatype-grammar}
\end{figure}
-Reading the theory file produces a structure which, in addtion to the usual
+Reading the theory file produces a structure which, in addition to the usual
components, contains a structure named $t$ for each datatype $t$ defined in
-the file\footnote{Otherwise multiple datatypes in the same theory file would
- lead to name clashes.}. Each structure $t$ contains the following elements:
+the file.\footnote{Otherwise multiple datatypes in the same theory file would
+ lead to name clashes.} Each structure $t$ contains the following elements:
\begin{ttbox}
-val induct : thm
+val distinct : thm list
val inject : thm list
-val ineq : thm list
+val induct : thm
val cases : thm list
val simps : thm list
val induct_tac : string -> int -> tactic
\end{ttbox}
-{\tt induct}, {\tt inject} and {\tt ineq} contain the theorems described
-above. For convenience {\tt ineq} contains inequalities in both directions.
+{\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described
+above. For convenience {\tt distinct} contains inequalities in both
+directions.
\begin{warn}
If there are five or more constructors, the {\em t\_ord} scheme is used for
- {\tt ineq}. In this case the theory {\tt Arith} must be contained
- in the current theory, if necessary by adding it explicitly.
+ {\tt distinct}. In this case the theory {\tt Arith} must be contained
+ in the current theory, if necessary by including it explicitly.
\end{warn}
-The reduction rules of the {\tt case}-construct can be found in {\tt cases}.
-All theorems from {\tt inject}, {\tt ineq} and {\tt cases} are combined in
+The reduction rules of the {\tt case}-construct are in {\tt cases}. All
+theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in
{\tt simps} for use with the simplifier. The tactic ``{\verb$induct_tac$~{\em
var i}\/}'' applies structural induction over variable {\em var} to
subgoal {\em i}.
@@ -1376,19 +1377,16 @@
\subsubsection{The datatype $\alpha~list$}
-We want to define the type $\alpha~list$.\footnote{Of course there is
-a list type in HOL already. But for now let us assume that we have to define
-a new type.} To do this we have to build a new theory that contains the
-type definition. We start from {\tt HOL}.
+We want to define the type $\alpha~list$.\footnote{Of course there is a list
+ type in HOL already. This is only an example.} To do this we have to build
+a new theory that contains the type definition. We start from {\tt HOL}.
\begin{ttbox}
MyList = HOL +
datatype 'a list = Nil | Cons ('a, 'a list)
end
\end{ttbox}
-After loading the theory with \verb$use_thy "MyList"$, we can prove
-$Cons(x,xs)\neq xs$ using the new theory. First we build a suitable simpset
-for the simplifier:
-
+After loading the theory (\verb$use_thy "MyList"$), we can prove
+$Cons(x,xs)\neq xs$. First we build a suitable simpset for the simplifier:
\begin{ttbox}
val mylist_ss = HOL_ss addsimps MyList.list.simps;
goal MyList.thy "!x. Cons(x,xs) ~= xs";
@@ -1406,8 +1404,8 @@
{\out ! x. Cons(x, list) ~= list ==>}
{\out ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)}
\end{ttbox}
-The first subgoal can be proved with the simplifier and the {\tt ineq} axiom
-that is part of \verb$mylist_ss$.
+The first subgoal can be proved with the simplifier and the distinctness
+axioms which are part of \verb$mylist_ss$.
\begin{ttbox}
by (simp_tac mylist_ss 1);
{\out Level 2}
@@ -1416,7 +1414,7 @@
{\out ! x. Cons(x, list) ~= list ==>}
{\out ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)}
\end{ttbox}
-Using the {\tt inject} axiom we can quickly prove the remaining goal.
+Using the freeness axioms we can quickly prove the remaining goal.
\begin{ttbox}
by (asm_simp_tac mylist_ss 1);
{\out Level 3}
@@ -1450,8 +1448,7 @@
Normally one wants to define functions dealing with a newly defined type and
prove properties of these functions. As an example let us define \verb|@| for
concatenation and {\tt ttl} for the (total) tail of a list, i.e.\ the list
-without its first element. We do this in theory \verb|List_fun| which is an
-extension of {\tt MyList}:
+without its first element:
\begin{ttbox}
List_fun = MyList +
consts ttl :: "'a list => 'a list"
@@ -1513,8 +1510,8 @@
\end{ttbox}
Because there are more than four constructors, the theory must be based on
{\tt Arith}. Inequality is defined via a function \verb|days_ord|. Although
-the expression \verb|Mo ~= Tu| is not directly contained in {\tt ineq}, it
-can be proved by the simplifier if \verb$arith_ss$ is used:
+the expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct},
+it can be proved by the simplifier if \verb$arith_ss$ is used:
\begin{ttbox}
val days_ss = arith_ss addsimps Days.days.simps;
--- a/doc-src/Logics/logics.toc Tue Jul 12 09:28:00 1994 +0200
+++ b/doc-src/Logics/logics.toc Tue Jul 12 12:49:15 1994 +0200
@@ -10,22 +10,22 @@
\contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12}
\contentsline {section}{\numberline {2.7}A classical example}{14}
\contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{15}
-\contentsline {subsection}{Deriving the introduction rule}{16}
-\contentsline {subsection}{Deriving the elimination rule}{17}
-\contentsline {subsection}{Using the derived rules}{17}
-\contentsline {subsection}{Derived rules versus definitions}{19}
+\contentsline {subsection}{\numberline {2.8.1}Deriving the introduction rule}{16}
+\contentsline {subsection}{\numberline {2.8.2}Deriving the elimination rule}{17}
+\contentsline {subsection}{\numberline {2.8.3}Using the derived rules}{17}
+\contentsline {subsection}{\numberline {2.8.4}Derived rules versus definitions}{19}
\contentsline {chapter}{\numberline {3}Zermelo-Fraenkel Set Theory}{22}
\contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{22}
\contentsline {section}{\numberline {3.2}The syntax of set theory}{23}
\contentsline {section}{\numberline {3.3}Binding operators}{25}
\contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{27}
\contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{30}
-\contentsline {subsection}{Fundamental lemmas}{30}
-\contentsline {subsection}{Unordered pairs and finite sets}{32}
-\contentsline {subsection}{Subset and lattice properties}{32}
-\contentsline {subsection}{Ordered pairs}{36}
-\contentsline {subsection}{Relations}{36}
-\contentsline {subsection}{Functions}{37}
+\contentsline {subsection}{\numberline {3.5.1}Fundamental lemmas}{30}
+\contentsline {subsection}{\numberline {3.5.2}Unordered pairs and finite sets}{32}
+\contentsline {subsection}{\numberline {3.5.3}Subset and lattice properties}{32}
+\contentsline {subsection}{\numberline {3.5.4}Ordered pairs}{36}
+\contentsline {subsection}{\numberline {3.5.5}Relations}{36}
+\contentsline {subsection}{\numberline {3.5.6}Functions}{37}
\contentsline {section}{\numberline {3.6}Further developments}{38}
\contentsline {section}{\numberline {3.7}Simplification rules}{47}
\contentsline {section}{\numberline {3.8}The examples directory}{47}
@@ -34,42 +34,50 @@
\contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{52}
\contentsline {chapter}{\numberline {4}Higher-Order Logic}{55}
\contentsline {section}{\numberline {4.1}Syntax}{55}
-\contentsline {subsection}{Types}{57}
-\contentsline {subsection}{Binders}{58}
-\contentsline {subsection}{The {\ptt let} and {\ptt case} constructions}{58}
+\contentsline {subsection}{\numberline {4.1.1}Types}{57}
+\contentsline {subsection}{\numberline {4.1.2}Binders}{58}
+\contentsline {subsection}{\numberline {4.1.3}The {\ptt let} and {\ptt case} constructions}{58}
\contentsline {section}{\numberline {4.2}Rules of inference}{58}
\contentsline {section}{\numberline {4.3}A formulation of set theory}{60}
-\contentsline {subsection}{Syntax of set theory}{65}
-\contentsline {subsection}{Axioms and rules of set theory}{69}
+\contentsline {subsection}{\numberline {4.3.1}Syntax of set theory}{65}
+\contentsline {subsection}{\numberline {4.3.2}Axioms and rules of set theory}{69}
\contentsline {section}{\numberline {4.4}Generic packages and classical reasoning}{71}
\contentsline {section}{\numberline {4.5}Types}{73}
-\contentsline {subsection}{Product and sum types}{73}
-\contentsline {subsection}{The type of natural numbers, {\ptt nat}}{73}
-\contentsline {subsection}{The type constructor for lists, {\ptt list}}{76}
-\contentsline {subsection}{The type constructor for lazy lists, {\ptt llist}}{76}
-\contentsline {section}{\numberline {4.6}The examples directories}{79}
-\contentsline {section}{\numberline {4.7}Example: Cantor's Theorem}{80}
-\contentsline {chapter}{\numberline {5}First-Order Sequent Calculus}{82}
-\contentsline {section}{\numberline {5.1}Unification for lists}{82}
-\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{84}
-\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{86}
-\contentsline {section}{\numberline {5.4}Tactics for sequents}{87}
-\contentsline {section}{\numberline {5.5}Packaging sequent rules}{88}
-\contentsline {section}{\numberline {5.6}Proof procedures}{88}
-\contentsline {subsection}{Method A}{89}
-\contentsline {subsection}{Method B}{89}
-\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{90}
-\contentsline {section}{\numberline {5.8}A more complex proof}{91}
-\contentsline {chapter}{\numberline {6}Constructive Type Theory}{93}
-\contentsline {section}{\numberline {6.1}Syntax}{95}
-\contentsline {section}{\numberline {6.2}Rules of inference}{95}
-\contentsline {section}{\numberline {6.3}Rule lists}{101}
-\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{101}
-\contentsline {section}{\numberline {6.5}Rewriting tactics}{102}
-\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{103}
-\contentsline {section}{\numberline {6.7}A theory of arithmetic}{105}
-\contentsline {section}{\numberline {6.8}The examples directory}{105}
-\contentsline {section}{\numberline {6.9}Example: type inference}{105}
-\contentsline {section}{\numberline {6.10}An example of logical reasoning}{107}
-\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{110}
-\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{111}
+\contentsline {subsection}{\numberline {4.5.1}Product and sum types}{73}
+\contentsline {subsection}{\numberline {4.5.2}The type of natural numbers, {\ptt nat}}{73}
+\contentsline {subsection}{\numberline {4.5.3}The type constructor for lists, {\ptt list}}{76}
+\contentsline {subsection}{\numberline {4.5.4}The type constructor for lazy lists, {\ptt llist}}{76}
+\contentsline {section}{\numberline {4.6}Datatype declarations}{79}
+\contentsline {subsection}{\numberline {4.6.1}Foundations}{79}
+\contentsline {subsection}{\numberline {4.6.2}Defining datatypes}{80}
+\contentsline {subsection}{\numberline {4.6.3}Examples}{82}
+\contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$}{82}
+\contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$ with mixfix syntax}{83}
+\contentsline {subsubsection}{Defining functions on datatypes}{83}
+\contentsline {subsubsection}{A datatype for weekdays}{84}
+\contentsline {section}{\numberline {4.7}The examples directories}{84}
+\contentsline {section}{\numberline {4.8}Example: Cantor's Theorem}{85}
+\contentsline {chapter}{\numberline {5}First-Order Sequent Calculus}{88}
+\contentsline {section}{\numberline {5.1}Unification for lists}{88}
+\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{90}
+\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{92}
+\contentsline {section}{\numberline {5.4}Tactics for sequents}{93}
+\contentsline {section}{\numberline {5.5}Packaging sequent rules}{94}
+\contentsline {section}{\numberline {5.6}Proof procedures}{94}
+\contentsline {subsection}{\numberline {5.6.1}Method A}{95}
+\contentsline {subsection}{\numberline {5.6.2}Method B}{95}
+\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{96}
+\contentsline {section}{\numberline {5.8}A more complex proof}{97}
+\contentsline {chapter}{\numberline {6}Constructive Type Theory}{99}
+\contentsline {section}{\numberline {6.1}Syntax}{101}
+\contentsline {section}{\numberline {6.2}Rules of inference}{101}
+\contentsline {section}{\numberline {6.3}Rule lists}{107}
+\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{107}
+\contentsline {section}{\numberline {6.5}Rewriting tactics}{108}
+\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{109}
+\contentsline {section}{\numberline {6.7}A theory of arithmetic}{111}
+\contentsline {section}{\numberline {6.8}The examples directory}{111}
+\contentsline {section}{\numberline {6.9}Example: type inference}{111}
+\contentsline {section}{\numberline {6.10}An example of logical reasoning}{113}
+\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{116}
+\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{117}