--- a/doc-src/Logics/FOL.tex Mon Mar 21 11:02:57 1994 +0100
+++ b/doc-src/Logics/FOL.tex Mon Mar 21 11:41:41 1994 +0100
@@ -1,5 +1,5 @@
%% $Id$
-\chapter{First-order logic}
+\chapter{First-Order logic}
The directory~\ttindexbold{FOL} contains theories for first-order logic
based on Gentzen's natural deduction systems (which he called {\sc nj} and
{\sc nk}). Intuitionistic logic is defined first; then classical logic is
@@ -34,7 +34,7 @@
exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
Some intuitionistic derived rules are shown in
-Figure~\ref{fol-int-derived}, again with their \ML\ names. These include
+Fig.\ts\ref{fol-int-derived}, again with their \ML\ names. These include
rules for the defined symbols $\neg$, $\bimp$ and $\exists!$. Natural
deduction typically involves a combination of forwards and backwards
reasoning, particularly with the destruction rules $(\conj E)$,
@@ -46,8 +46,8 @@
conj_impE}, etc., support the intuitionistic proof procedure
(see~\S\ref{fol-int-prover}).
-See the files \ttindexbold{FOL/ifol.thy}, \ttindexbold{FOL/ifol.ML} and
-\ttindexbold{FOL/intprover.ML} for complete listings of the rules and
+See the files {\tt FOL/ifol.thy}, {\tt FOL/ifol.ML} and
+{\tt FOL/intprover.ML} for complete listings of the rules and
derived rules.
\begin{figure}
@@ -194,7 +194,7 @@
\section{Generic packages}
\FOL{} instantiates most of Isabelle's generic packages;
-see \ttindexbold{FOL/ROOT.ML} for details.
+see {\tt FOL/ROOT.ML} for details.
\begin{itemize}
\item
Because it includes a general substitution rule, \FOL{} instantiates the
@@ -205,7 +205,7 @@
set for intuitionistic first-order logic, while \ttindexbold{FOL_ss} is the
simplification set for classical logic. Both equality ($=$) and the
biconditional ($\bimp$) may be used for rewriting. See the file
-\ttindexbold{FOL/simpdata.ML} for a complete listing of the simplification
+{\tt FOL/simpdata.ML} for a complete listing of the simplification
rules.
\item
It instantiates the classical reasoning module. See~\S\ref{fol-cla-prover}
@@ -228,7 +228,7 @@
\]
The theorem prover for intuitionistic logic does not use~{\tt impE}.\@
Instead, it simplifies implications using derived rules
-(Figure~\ref{fol-int-derived}). It reduces the antecedents of implications
+(Fig.\ts\ref{fol-int-derived}). It reduces the antecedents of implications
to atoms and then uses Modus Ponens: from $P\imp Q$ and $P$ deduce~$Q$.
The rules \ttindex{conj_impE} and \ttindex{disj_impE} are
straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and
@@ -254,7 +254,7 @@
\end{ttbox}
Most of these belong to the structure \ttindexbold{Int}. They are
similar or identical to tactics (with the same names) provided by
-Isabelle's classical module (see {\em The Isabelle Reference Manual\/}).
+Isabelle's classical module (see the {\em Reference Manual\/}).
\begin{description}
\item[\ttindexbold{mp_tac} {\it i}]
@@ -328,7 +328,7 @@
Natural deduction in classical logic is not really all that natural.
{\FOL} derives classical introduction rules for $\disj$ and~$\exists$, as
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
-rule (see Figure~\ref{fol-cla-derived}).
+rule (see Fig.\ts\ref{fol-cla-derived}).
The classical reasoning module is set up for \FOL, as the
structure~\ttindexbold{Cla}. This structure is open, so \ML{} identifiers
@@ -361,7 +361,7 @@
generally unsuitable for depth-first search.
\end{description}
\noindent
-See the file \ttindexbold{FOL/fol.ML} for derivations of the
+See the file {\tt FOL/fol.ML} for derivations of the
classical rules, and the {\em Reference Manual} for more discussion of
classical proof methods.
@@ -537,6 +537,7 @@
{\out Level 5}
{\out ~ ~ ((P --> Q) | (Q --> P))}
{\out 1. [| P; Q --> False; Q; P --> False |] ==> P}
+\ttbreak
by (assume_tac 1);
{\out Level 6}
{\out ~ ~ ((P --> Q) | (Q --> P))}
@@ -835,13 +836,17 @@
{\out Level 0}
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
-\ttbreak
+\end{ttbox}
+This time, simply unfold using the definition of $if$:
+\begin{ttbox}
by (rewrite_goals_tac [if_def]);
{\out Level 1}
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
{\out 1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
{\out P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)}
-\ttbreak
+\end{ttbox}
+We are left with a subgoal in pure first-order logic:
+\begin{ttbox}
by (fast_tac FOL_cs 1);
{\out Level 2}
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
--- a/doc-src/Logics/Old_HOL.tex Mon Mar 21 11:02:57 1994 +0100
+++ b/doc-src/Logics/Old_HOL.tex Mon Mar 21 11:41:41 1994 +0100
@@ -1,13 +1,13 @@
%% $Id$
-\chapter{Higher-order logic}
-The directory~\ttindexbold{HOL} contains a theory for higher-order logic
-based on Gordon's~{\sc hol} system~\cite{mgordon88a}, which itself is based on
-Church~\cite{church40}. Andrews~\cite{andrews86} is a full description of
-higher-order logic. Gordon's work has demonstrated that higher-order logic
-is useful for hardware verification; beyond this, it is widely applicable
-in many areas of mathematics. It is weaker than {\ZF} set theory but for
-most applications this does not matter. If you prefer {\ML} to Lisp, you
-will probably prefer {\HOL} to~{\ZF}.
+\chapter{Higher-Order logic}
+The directory~\ttindexbold{HOL} contains a theory for higher-order logic.
+It is based on Gordon's~{\sc hol} system~\cite{mgordon88a}, which itself is
+based on Church~\cite{church40}. Andrews~\cite{andrews86} is a full
+description of higher-order logic. Gordon's work has demonstrated that
+higher-order logic is useful for hardware verification; beyond this, it is
+widely applicable in many areas of mathematics. It is weaker than {\ZF}
+set theory but for most applications this does not matter. If you prefer
+{\ML} to Lisp, you will probably prefer {\HOL} to~{\ZF}.
Previous releases of Isabelle included a completely different version
of~{\HOL}, with explicit type inference rules~\cite{paulson-COLOG}. This
@@ -136,16 +136,17 @@
\index{*"+}\index{-@{\tt-}}\index{*@{\tt*}}
Figure~\ref{hol-constants} lists the constants (including infixes and
-binders), while Figure~\ref{hol-grammar} presents the grammar. Note that
-$a$\verb|~=|$b$ is translated to \verb|~(|$a$=$b$\verb|)|.
+binders), while Fig.\ts \ref{hol-grammar} presents the grammar of
+higher-order logic. Note that $a$\verb|~=|$b$ is translated to
+\verb|~(|$a$=$b$\verb|)|.
-\subsection{Types}
+\subsection{Types}\label{HOL-types}
The type of formulae, {\it bool} belongs to class {\it term}; thus,
formulae are terms. The built-in type~$fun$, which constructs function
types, is overloaded such that $\sigma\To\tau$ belongs to class~$term$ if
$\sigma$ and~$\tau$ do; this allows quantification over functions. Types
-in {\HOL} must be non-empty because of the form of quantifier
-rules~\cite[\S7]{paulson-COLOG}.
+in {\HOL} must be non-empty; otherwise the quantifier rules would be
+unsound~\cite[\S7]{paulson-COLOG}.
Gordon's {\sc hol} system supports {\bf type definitions}. A type is
defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To
@@ -198,11 +199,11 @@
\hbox{\tt \at $x\,y$.$P[x,y]$}.
\end{warn}
-\begin{figure} \makeatother
-\begin{ttbox}
+\begin{figure}
+\begin{ttbox}\makeatother
\idx{refl} t = t::'a
\idx{subst} [| s=t; P(s) |] ==> P(t::'a)
-\idx{ext} (!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x))
+\idx{ext} (!!x::'a. f(x)::'b = g(x)) ==> (\%x.f(x)) = (\%x.g(x))
\idx{impI} (P ==> Q) ==> P-->Q
\idx{mp} [| P-->Q; P |] ==> Q
\idx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
@@ -210,26 +211,26 @@
\idx{True_or_False} (P=True) | (P=False)
\subcaption{basic rules}
-\idx{True_def} True = ((%x.x)=(%x.x))
-\idx{All_def} All = (%P. P = (%x.True))
-\idx{Ex_def} Ex = (%P. P(@x.P(x)))
+\idx{True_def} True = ((\%x.x)=(\%x.x))
+\idx{All_def} All = (\%P. P = (\%x.True))
+\idx{Ex_def} Ex = (\%P. P(@x.P(x)))
\idx{False_def} False = (!P.P)
-\idx{not_def} not = (%P. P-->False)
-\idx{and_def} op & = (%P Q. !R. (P-->Q-->R) --> R)
-\idx{or_def} op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)
-\idx{Ex1_def} Ex1 = (%P. ? x. P(x) & (! y. P(y) --> y=x))
+\idx{not_def} not = (\%P. P-->False)
+\idx{and_def} op & = (\%P Q. !R. (P-->Q-->R) --> R)
+\idx{or_def} op | = (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
+\idx{Ex1_def} Ex1 = (\%P. ? x. P(x) & (! y. P(y) --> y=x))
\subcaption{Definitions of the logical constants}
-\idx{Inv_def} Inv = (%(f::'a=>'b) y. @x. f(x)=y)
-\idx{o_def} op o = (%(f::'b=>'c) g (x::'a). f(g(x)))
-\idx{if_def} if = (%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
+\idx{Inv_def} Inv = (\%(f::'a=>'b) y. @x. f(x)=y)
+\idx{o_def} op o = (\%(f::'b=>'c) g (x::'a). f(g(x)))
+\idx{if_def} if = (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
\subcaption{Further definitions}
\end{ttbox}
\caption{Rules of {\tt HOL}} \label{hol-rules}
\end{figure}
-\begin{figure} \makeatother
+\begin{figure}
\begin{ttbox}
\idx{sym} s=t ==> t=s
\idx{trans} [| r=s; s=t |] ==> r=t
@@ -270,8 +271,8 @@
\end{figure}
-\begin{figure} \makeatother
-\begin{ttbox}
+\begin{figure}
+\begin{ttbox}\makeatother
\idx{allI} (!!x::'a. P(x)) ==> !x. P(x)
\idx{spec} !x::'a.P(x) ==> P(x)
\idx{allE} [| !x.P(x); P(x) ==> R |] ==> R
@@ -294,7 +295,7 @@
\idx{disjCI} (~Q ==> P) ==> P|Q
\idx{exCI} (! x. ~ P(x) ==> P(a)) ==> ? x.P(x)
\idx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
-\idx{iffCE} [| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
+\idx{iffCE} [| P=Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
\idx{notnotD} ~~P ==> P
\idx{swap} ~P ==> (~Q ==> P) ==> Q
\subcaption{Classical logic}
@@ -319,11 +320,12 @@
They follow standard practice in higher-order logic: only a few connectives
are taken as primitive, with the remainder defined obscurely.
-Unusually, the definitions use object-equality~({\tt=}) rather than
-meta-equality~({\tt==}). This is possible because equality in higher-order
-logic may equate formulae and even functions over formulae. On the other
-hand, meta-equality is Isabelle's usual symbol for making definitions.
-Take care to note which form of equality is used before attempting a proof.
+Unusually, the definitions are expressed using object-equality~({\tt=})
+rather than meta-equality~({\tt==}). This is possible because equality in
+higher-order logic may equate formulae and even functions over formulae.
+On the other hand, meta-equality is Isabelle's usual symbol for making
+definitions. Take care to note which form of equality is used before
+attempting a proof.
Some of the rules mention type variables; for example, {\tt refl} mentions
the type variable~{\tt'a}. This facilitates explicit instantiation of the
@@ -373,14 +375,14 @@
backward proofs, while \ttindexbold{box_equals} supports reasoning by
simplifying both sides of an equation.
-See the files \ttindexbold{HOL/hol.thy} and
-\ttindexbold{HOL/hol.ML} for complete listings of the rules and
+See the files {\tt HOL/hol.thy} and
+{\tt HOL/hol.ML} for complete listings of the rules and
derived rules.
\section{Generic packages}
{\HOL} instantiates most of Isabelle's generic packages;
-see \ttindexbold{HOL/ROOT.ML} for details.
+see {\tt HOL/ROOT.ML} for details.
\begin{itemize}
\item
Because it includes a general substitution rule, {\HOL} instantiates the
@@ -390,7 +392,7 @@
It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
simplification set for higher-order logic. Equality~($=$), which also
expresses logical equivalence, may be used for rewriting. See the file
-\ttindexbold{HOL/simpdata.ML} for a complete listing of the simplification
+{\tt HOL/simpdata.ML} for a complete listing of the simplification
rules.
\item
It instantiates the classical reasoning module. See~\S\ref{hol-cla-prover}
@@ -519,7 +521,7 @@
\end{figure}
-\begin{figure} \makeatother
+\begin{figure} \underscoreon
\begin{ttbox}
\idx{mem_Collect_eq} (a : \{x.P(x)\}) = P(a)
\idx{Collect_mem_eq} \{x.x:A\} = A
@@ -552,7 +554,7 @@
\end{figure}
-\begin{figure} \makeatother
+\begin{figure} \underscoreon
\begin{ttbox}
\idx{CollectI} [| P(a) |] ==> a : \{x.P(x)\}
\idx{CollectD} [| a : \{x.P(x)\} |] ==> P(a)
@@ -593,7 +595,7 @@
\end{figure}
-\begin{figure} \makeatother
+\begin{figure} \underscoreon
\begin{ttbox}
\idx{emptyE} a : \{\} ==> P
@@ -653,13 +655,13 @@
denoting the universal set for the given type.
\subsection{Syntax of set theory}
-The type $\alpha\,set$ is essentially the same as $\alpha\To bool$. The new
-type is defined for clarity and to avoid complications involving function
-types in unification. Since Isabelle does not support type definitions (as
-discussed above), the isomorphisms between the two types are declared
-explicitly. Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
-$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
-argument order).
+The type $\alpha\,set$ is essentially the same as $\alpha\To bool$. The
+new type is defined for clarity and to avoid complications involving
+function types in unification. Since Isabelle does not support type
+definitions (as mentioned in \S\ref{HOL-types}), the isomorphisms between
+the two types are declared explicitly. Here they are natural: {\tt
+ Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :}
+maps in the other direction (ignoring argument order).
Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
@@ -709,13 +711,13 @@
The axioms \ttindexbold{mem_Collect_eq} and
\ttindexbold{Collect_mem_eq} assert that the functions {\tt Collect} and
\hbox{\tt op :} are isomorphisms.
-All the other axioms are definitions; see Figure~\ref{hol-set-rules}.
+All the other axioms are definitions; see Fig.\ts \ref{hol-set-rules}.
These include straightforward properties of functions: image~({\tt``}) and
{\tt range}, and predicates concerning monotonicity, injectiveness, etc.
{\HOL}'s set theory has the {\ML} identifier \ttindexbold{Set.thy}.
-\begin{figure} \makeatother
+\begin{figure} \underscoreon
\begin{ttbox}
\idx{imageI} [| x:A |] ==> f(x) : f``A
\idx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P
@@ -752,7 +754,7 @@
\end{figure}
-\begin{figure} \makeatother
+\begin{figure} \underscoreon
\begin{ttbox}
\idx{Union_upper} B:A ==> B <= Union(A)
\idx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
@@ -772,7 +774,7 @@
\end{figure}
-\begin{figure} \makeatother
+\begin{figure} \underscoreon
\begin{ttbox}
\idx{Int_absorb} A Int A = A
\idx{Int_commute} A Int B = B Int A
@@ -791,12 +793,12 @@
\idx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)
\idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)
-\idx{Int_Union_image} A Int Union(B) = (UN C:B. A Int C)
+\idx{Int_Union} A Int Union(B) = (UN C:B. A Int C)
\idx{Un_Union_image}
(UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
\idx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)
-\idx{Un_Inter_image} A Un Inter(B) = (INT C:B. A Un C)
+\idx{Un_Inter} A Un Inter(B) = (INT C:B. A Un C)
\idx{Int_Inter_image}
(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
\end{ttbox}
@@ -813,36 +815,40 @@
\ttindexbold{bexI}, \ttindexbold{Un1} and~\ttindexbold{Un2} are not
strictly necessary. Similarly, \ttindexbold{equalityCE} supports classical
reasoning about extensionality, after the fashion of \ttindex{iffCE}. See
-the file \ttindexbold{HOL/set.ML} for proofs pertaining to set theory.
+the file {\tt HOL/set.ML} for proofs pertaining to set theory.
-Figure~\ref{hol-fun} presents derived rules involving functions. See
-the file \ttindexbold{HOL/fun.ML} for a complete listing.
+Figure~\ref{hol-fun} presents derived inference rules involving functions. See
+the file {\tt HOL/fun.ML} for a complete listing.
Figure~\ref{hol-subset} presents lattice properties of the subset relation.
-See \ttindexbold{HOL/subset.ML}.
+See the file {\tt HOL/subset.ML}.
Figure~\ref{hol-equalities} presents set equalities. See
-\ttindexbold{HOL/equalities.ML}.
+{\tt HOL/equalities.ML}.
-\begin{figure} \makeatother
+\begin{figure}
\begin{center}
\begin{tabular}{rrr}
\it name &\it meta-type & \it description \\
\idx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
& ordered pairs $\langle a,b\rangle$ \\
- \idx{fst} & $\alpha\times\beta \To \alpha$ & first projection\\
+ \idx{fst} & $\alpha\times\beta \To \alpha$ & first projection\\
\idx{snd} & $\alpha\times\beta \To \beta$ & second projection\\
\idx{split} & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$
- & generalized projection
+ & generalized projection\\
+ \idx{Sigma} &
+ $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
+ general sum of sets
\end{tabular}
\end{center}
\subcaption{Constants}
-\begin{ttbox}
+\begin{ttbox}\makeatletter
\idx{fst_def} fst(p) == @a. ? b. p = <a,b>
\idx{snd_def} snd(p) == @b. ? a. p = <a,b>
\idx{split_def} split(p,c) == c(fst(p),snd(p))
+\idx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
\subcaption{Definitions}
\idx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
@@ -852,6 +858,11 @@
\idx{split} split(<a,b>, c) = c(a,b)
\idx{surjective_pairing} p = <fst(p),snd(p)>
+
+\idx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)
+
+\idx{SigmaE} [| c: Sigma(A,B);
+ !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
\subcaption{Derived rules}
\end{ttbox}
\caption{Type $\alpha\times\beta$}
@@ -859,7 +870,7 @@
\end{figure}
-\begin{figure} \makeatother
+\begin{figure}
\begin{center}
\begin{tabular}{rrr}
\it name &\it meta-type & \it description \\
@@ -871,8 +882,8 @@
\end{center}
\subcaption{Constants}
-\begin{ttbox}
-\idx{case_def} case == (%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
+\begin{ttbox}\makeatletter
+\idx{case_def} case == (\%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
(!y. p=Inr(y) --> z=g(y)))
\subcaption{Definition}
@@ -903,16 +914,16 @@
\subsection{Product and sum types}
{\HOL} defines the product type $\alpha\times\beta$ and the sum type
$\alpha+\beta$, with the ordered pair syntax {\tt<$a$,$b$>}, using fairly
-standard constructions (Figures~\ref{hol-prod} and~\ref{hol-sum}). Because
-Isabelle does not support type definitions, the isomorphisms between these
-types and their representations are made explicitly.
+standard constructions (Figs.~\ref{hol-prod} and~\ref{hol-sum}). Because
+Isabelle does not support abstract type definitions, the isomorphisms
+between these types and their representations are made explicitly.
Most of the definitions are suppressed, but observe that the projections
and conditionals are defined as descriptions. Their properties are easily
-proved using \ttindex{select_equality}. See \ttindexbold{HOL/prod.thy} and
-\ttindexbold{HOL/sum.thy} for details.
+proved using \ttindex{select_equality}. See {\tt HOL/prod.thy} and
+{\tt HOL/sum.thy} for details.
-\begin{figure} \makeatother
+\begin{figure}
\indexbold{*"<}
\begin{center}
\begin{tabular}{rrr}
@@ -945,27 +956,27 @@
\end{center}
\subcaption{Constants and infixes}
-\begin{ttbox}
-\idx{nat_case_def} nat_case == (%n a f. @z. (n=0 --> z=a) &
+\begin{ttbox}\makeatother
+\idx{nat_case_def} nat_case == (\%n a f. @z. (n=0 --> z=a) &
(!x. n=Suc(x) --> z=f(x)))
\idx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\}
\idx{less_def} m<n == <m,n>:pred_nat^+
\idx{nat_rec_def} nat_rec(n,c,d) ==
- wfrec(pred_nat, n, %l g.nat_case(l, c, %m.d(m,g(m))))
+ wfrec(pred_nat, n, \%l g.nat_case(l, c, \%m.d(m,g(m))))
-\idx{add_def} m+n == nat_rec(m, n, %u v.Suc(v))
-\idx{diff_def} m-n == nat_rec(n, m, %u v. nat_rec(v, 0, %x y.x))
-\idx{mult_def} m*n == nat_rec(m, 0, %u v. n + v)
-\idx{mod_def} m//n == wfrec(trancl(pred_nat), m, %j f. if(j<n,j,f(j-n)))
+\idx{add_def} m+n == nat_rec(m, n, \%u v.Suc(v))
+\idx{diff_def} m-n == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
+\idx{mult_def} m*n == nat_rec(m, 0, \%u v. n + v)
+\idx{mod_def} m//n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
\idx{quo_def} m/n == wfrec(trancl(pred_nat),
- m, %j f. if(j<n,0,Suc(f(j-n))))
+ m, \%j f. if(j<n,0,Suc(f(j-n))))
\subcaption{Definitions}
\end{ttbox}
\caption{Defining $nat$, the type of natural numbers} \label{hol-nat1}
\end{figure}
-\begin{figure} \makeatother
+\begin{figure} \underscoreon
\begin{ttbox}
\idx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n)
@@ -1015,8 +1026,8 @@
The definition makes use of a least fixed point operator \ttindex{lfp},
defined using the Knaster-Tarski theorem. This in turn defines an operator
\ttindex{trancl} for taking the transitive closure of a relation. See
-files \ttindexbold{HOL/lfp.thy} and \ttindexbold{HOL/trancl.thy} for
-details. The definition of~$nat$ resides on \ttindexbold{HOL/nat.thy}.
+files {\tt HOL/lfp.thy} and {\tt HOL/trancl.thy} for
+details. The definition of~$nat$ resides on {\tt HOL/nat.thy}.
Type $nat$ is postulated to belong to class~$ord$, which overloads $<$ and
$\leq$ on the natural numbers. As of this writing, Isabelle provides no
@@ -1024,20 +1035,20 @@
the {\HOL} theory includes no polymorphic axioms stating general properties
of $<$ and $\leq$.
-File \ttindexbold{HOL/arith.ML} develops arithmetic on the natural numbers.
+File {\tt HOL/arith.ML} develops arithmetic on the natural numbers.
It defines addition, multiplication, subtraction, division, and remainder,
proving the theorem $a \bmod b + (a/b)\times b = a$. Division and
remainder are defined by repeated subtraction, which requires well-founded
rather than primitive recursion.
Primitive recursion makes use of \ttindex{wfrec}, an operator for recursion
-along arbitrary well-founded relations; see \ttindexbold{HOL/wf.ML} for the
+along arbitrary well-founded relations; see {\tt HOL/wf.ML} for the
development. The predecessor relation, \ttindexbold{pred_nat}, is shown to
be well-founded; recursion along this relation is primitive recursion,
while its transitive closure is~$<$.
-\begin{figure} \makeatother
+\begin{figure}
\begin{center}
\begin{tabular}{rrr}
\it symbol & \it meta-type & \it description \\
@@ -1054,7 +1065,7 @@
\subcaption{Constants}
\begin{ttbox}
-\idx{map_def} map(f,xs) == list_rec(xs, Nil, %x l r. Cons(f(x), r))
+\idx{map_def} map(f,xs) == list_rec(xs, Nil, \%x l r. Cons(f(x), r))
\subcaption{Definition}
\idx{list_induct}
@@ -1076,7 +1087,7 @@
\subsection{The type constructor for lists, $\alpha\,list$}
{\HOL}'s definition of lists is an example of an experimental method for
handling recursive data types. The details need not concern us here; see
-the file \ttindexbold{HOL/list.ML}. Figure~\ref{hol-list} presents the
+the file {\tt HOL/list.ML}. Figure~\ref{hol-list} presents the
basic list operations, with their types and properties. In particular,
\ttindexbold{list_rec} is a primitive recursion operator for lists, in the
style of Martin-L\"of type theory. It is derived from well-founded
@@ -1092,7 +1103,7 @@
operations such as filter, which can compute indefinitely before yielding
the next element (if any!) of the lazy list. A co-induction principle is
defined for proving equations on lazy lists. See the files
-\ttindexbold{HOL/llist.thy} and \ttindexbold{HOL/llist.ML} for the formal
+{\tt HOL/llist.thy} and {\tt HOL/llist.ML} for the formal
derivations. I have written a report discussing the treatment of lazy
lists, and finite lists also~\cite{paulson-coind}.
@@ -1100,7 +1111,7 @@
\section{Classical proof procedures} \label{hol-cla-prover}
{\HOL} derives classical introduction rules for $\disj$ and~$\exists$, as
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
-rule (Figure~\ref{hol-lemmas2}).
+rule (Fig.~\ref{hol-lemmas2}).
The classical reasoning module is set up for \HOL, as the structure
\ttindexbold{Classical}. This structure is open, so {\ML} identifiers such
@@ -1150,33 +1161,34 @@
Directory {\tt ex} contains other examples and experimental proofs in
{\HOL}. Here is an overview of the more interesting files.
\begin{description}
-\item[\ttindexbold{HOL/ex/meson.ML}]
+\item[{\tt HOL/ex/meson.ML}]
contains an experimental implementation of the MESON proof procedure,
inspired by Plaisted~\cite{plaisted90}. It is much more powerful than
Isabelle's classical module.
-\item[\ttindexbold{HOL/ex/mesontest.ML}]
+\item[{\tt HOL/ex/mesontest.ML}]
contains test data for the MESON proof procedure.
-\item[\ttindexbold{HOL/ex/set.ML}]
-proves Cantor's Theorem (see below) and the Schr\"oder-Bernstein Theorem.
+\item[{\tt HOL/ex/set.ML}]
+ proves Cantor's Theorem, which is presented below, and the
+ Schr\"oder-Bernstein Theorem.
-\item[\ttindexbold{HOL/ex/pl.ML}]
+\item[{\tt HOL/ex/pl.ML}]
proves the soundness and completeness of classical propositional logic,
given a truth table semantics. The only connective is $\imp$. A
Hilbert-style axiom system is specified, and its set of theorems defined
inductively.
-\item[\ttindexbold{HOL/ex/term.ML}]
+\item[{\tt HOL/ex/term.ML}]
contains proofs about an experimental recursive type definition;
the recursion goes through the type constructor~$list$.
-\item[\ttindexbold{HOL/ex/simult.ML}]
+\item[{\tt HOL/ex/simult.ML}]
defines primitives for solving mutually recursive equations over sets.
It constructs sets of trees and forests as an example, including induction
and recursion rules that handle the mutual recursion.
-\item[\ttindexbold{HOL/ex/mt.ML}]
+\item[{\tt HOL/ex/mt.ML}]
contains Jacob Frost's formalization~\cite{frost93} of a co-induction
example by Milner and Tofte~\cite{milner-coind}.
\end{description}
@@ -1220,6 +1232,7 @@
{\out Level 2}
{\out P & Q}
{\out 1. !!R. (P --> Q --> R) --> R}
+\ttbreak
by (resolve_tac [impI] 1);
{\out Level 3}
{\out P & Q}
@@ -1259,19 +1272,20 @@
Working with premises that involve defined constants can be tricky. We
must expand the definition of conjunction in the meta-assumption $P\conj
Q$. The rule \ttindex{subst} performs substitution in forward proofs.
-We get two resolvents, since the vacuous substitution is valid:
+We get {\it two\/} resolvents since the vacuous substitution is valid:
\begin{ttbox}
prems RL [and_def RS subst];
{\out val it = ["! R. (P --> Q --> R) --> R [P & Q]",}
{\out "P & Q [P & Q]"] : thm list}
\end{ttbox}
By applying $(\forall E)$ and $({\imp}E)$ to the resolvents, we dispose of
-the vacuous one and put the other into a convenient form:\footnote
-{In higher-order logic, {\tt spec RS mp} fails because the resolution yields
-two results, namely ${\List{\forall x.x; P}\Imp Q}$ and ${\List{\forall
- x.P(x)\imp Q(x); P(x)}\Imp Q(x)}$. In first-order logic, the resolution
-yields only the latter result.}
-\index{*RL}
+the vacuous one and put the other into a convenient form:\footnote {Why use
+ {\tt [spec] RL [mp]} instead of {\tt [spec RS mp]} to join the rules? In
+ higher-order logic, {\tt spec RS mp} fails because the resolution yields
+ two results, namely ${\List{\forall x.x; P}\Imp Q}$ and ${\List{\forall
+ x.P(x)\imp Q(x); P(x)}\Imp Q(x)}$. In first-order logic, the
+ resolution yields only the latter result because $\forall x.x$ is not a
+ first-order formula; in fact, it is equivalent to falsity.} \index{*RL}
\begin{ttbox}
prems RL [and_def RS subst] RL [spec] RL [mp];
{\out val it = ["P --> Q --> ?Q ==> ?Q [P & Q]"] : thm list}
@@ -1304,7 +1318,6 @@
Viewing types as sets, $\alpha\To bool$ represents the powerset
of~$\alpha$. This version states that for every function from $\alpha$ to
its powerset, some subset is outside its range.
-
The Isabelle proof uses {\HOL}'s set theory, with the type $\alpha\,set$ and
the operator \ttindex{range}. Since it avoids quantification, we may
inspect the subset found by the proof.
@@ -1321,6 +1334,7 @@
{\out Level 1}
{\out ~ ?S : range(f)}
{\out 1. ?S : range(f) ==> False}
+\ttbreak
by (eresolve_tac [rangeE] 1);
{\out Level 2}
{\out ~ ?S : range(f)}
@@ -1347,8 +1361,8 @@
{\out 2. !!x. [| ~ ?c3(x) : \{x. ?P7(x)\}; ~ ?c3(x) : f(x) |] ==> False}
\end{ttbox}
Forcing a contradiction between the two assumptions of subgoal~1 completes
-the instantiation of~$S$. It is now $\{x. x\not\in f(x)\}$, the standard
-diagonal construction.
+the instantiation of~$S$. It is now the set $\{x. x\not\in f(x)\}$, the
+standard diagonal construction.
\begin{ttbox}
by (contr_tac 1);
{\out Level 5}
@@ -1362,6 +1376,7 @@
{\out Level 6}
{\out ~ \{x. ~ x : f(x)\} : range(f)}
{\out 1. !!x. [| ~ x : f(x); ~ False |] ==> ~ x : f(x)}
+\ttbreak
by (assume_tac 1);
{\out Level 7}
{\out ~ \{x. ~ x : f(x)\} : range(f)}
@@ -1378,6 +1393,7 @@
{\out Level 0}
{\out ~ ?S : range(f)}
{\out 1. ~ ?S : range(f)}
+\ttbreak
by (best_tac (set_cs addSEs [equalityCE]) 1);
{\out Level 1}
{\out ~ \{x. ~ x : f(x)\} : range(f)}
--- a/doc-src/Logics/ZF.tex Mon Mar 21 11:02:57 1994 +0100
+++ b/doc-src/Logics/ZF.tex Mon Mar 21 11:41:41 1994 +0100
@@ -1,6 +1,6 @@
%% $Id$
%%%See grant/bra/Lib/ZF.tex for lfp figure
-\chapter{Zermelo-Fraenkel set theory}
+\chapter{Zermelo-Fraenkel Set Theory}
The directory~\ttindexbold{ZF} implements Zermelo-Fraenkel set
theory~\cite{halmos60,suppes72} as an extension of~\ttindex{FOL}, classical
first-order logic. The theory includes a collection of derived natural
@@ -162,8 +162,10 @@
The constant \ttindexbold{Pair} constructs ordered pairs, as in {\tt
Pair($a$,$b$)}. Ordered pairs may also be written within angle brackets,
as {\tt<$a$,$b$>}. The $n$-tuple {\tt<$a@1$,\ldots,$a@{n-1}$,$a@n$>}
-abbreviates the nest of pairs {\tt
- Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots)}.
+abbreviates the nest of pairs
+\begin{quote}
+ \tt Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).
+\end{quote}
In {\ZF}, a function is a set of pairs. A {\ZF} function~$f$ is simply an
individual as far as Isabelle is concerned: its Isabelle type is~$i$, not
@@ -175,7 +177,7 @@
\begin{figure}
\indexbold{*"-">}
\indexbold{*"*}
-\begin{center} \tt\frenchspacing
+\begin{center} \footnotesize\tt\frenchspacing
\begin{tabular}{rrr}
\it external & \it internal & \it description \\
$a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\
@@ -280,16 +282,18 @@
The constant \ttindexbold{RepFun} expresses a special case of replacement,
where $Q[x,y]$ has the form $y=b[x]$. Such a $Q$ is trivially
single-valued, since it is just the graph of the meta-level
-function~$\lambda x.b[x]$. The syntax is \hbox{\tt\{$b[x]$.$x$:$A$\}},
-denoting set {\tt RepFun($A$,$\lambda x.b[x]$)} of all $b[x]$ for~$x\in A$.
-This is analogous to the \ML{} functional {\tt map}, since it applies a
-function to every element of a set.
+function~$\lambda x.b[x]$. The resulting set consists of all $b[x]$
+for~$x\in A$. This is analogous to the \ML{} functional {\tt map}, since
+it applies a function to every element of a set. The syntax is
+\hbox{\tt\{$b[x]$.$x$:$A$\}}, which expands to {\tt RepFun($A$,$\lambda
+ x.b[x]$)}.
-\indexbold{*INT}\indexbold{*UN}
-General unions and intersections of families, namely $\bigcup@{x\in A}B[x]$ and
-$\bigcap@{x\in A}B[x]$, are written \hbox{\tt UN $x$:$A$.$B[x]$} and
-\hbox{\tt INT $x$:$A$.$B[x]$}. Their meaning is expressed using {\tt
-RepFun} as
+
+\indexbold{*INT}\indexbold{*UN}
+General unions and intersections of indexed
+families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$,
+are written \hbox{\tt UN $x$:$A$.$B[x]$} and \hbox{\tt INT $x$:$A$.$B[x]$}.
+Their meaning is expressed using {\tt RepFun} as
\[ \bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad
\bigcap(\{B[x]. x\in A\}).
\]
@@ -355,7 +359,7 @@
\subcaption{The Zermelo-Fraenkel Axioms}
\idx{Replace_def} Replace(A,P) ==
- PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))
+ PrimReplace(A, \%x y. (EX!z.P(x,z)) & P(x,y))
\idx{RepFun_def} RepFun(A,f) == \{y . x:A, y=f(x)\}
\idx{the_def} The(P) == Union(\{y . x:\{0\}, P(y)\})
\idx{if_def} if(P,a,b) == THE z. P & z=a | ~P & z=b
@@ -383,8 +387,8 @@
\idx{Pair_def} <a,b> == \{\{a,a\}, \{a,b\}\}
\idx{split_def} split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b)
-\idx{fst_def} fst(A) == split(%x y.x, p)
-\idx{snd_def} snd(A) == split(%x y.y, p)
+\idx{fst_def} fst(A) == split(\%x y.x, p)
+\idx{snd_def} snd(A) == split(\%x y.y, p)
\idx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
\subcaption{Ordered pairs and Cartesian products}
@@ -495,12 +499,12 @@
\section{The Zermelo-Fraenkel axioms}
-The axioms appear in Figure~\ref{ZF-rules}. They resemble those
+The axioms appear in Fig.\ts \ref{ZF-rules}. They resemble those
presented by Suppes~\cite{suppes72}. Most of the theory consists of
definitions. In particular, bounded quantifiers and the subset relation
appear in other axioms. Object-level quantifiers and implications have
been replaced by meta-level ones wherever possible, to simplify use of the
-axioms. See the file \ttindexbold{ZF/zf.thy} for details.
+axioms. See the file {\tt ZF/zf.thy} for details.
The traditional replacement axiom asserts
\[ y \in {\tt PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \]
@@ -527,7 +531,7 @@
the theory names it (\ttindexbold{Inf}) in order to simplify the
construction of the natural numbers.
-Further definitions appear in Figure~\ref{ZF-defs}. Ordered pairs are
+Further definitions appear in Fig.\ts\ref{ZF-defs}. Ordered pairs are
defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$. Recall
that \ttindexbold{Sigma}$(A,B)$ generalizes the Cartesian product of two
sets. It is defined to be the union of all singleton sets
@@ -584,7 +588,7 @@
\ttindex{CollectD1} and \ttindex{CollectD2}, but each rule is suited to
particular circumstances. Although too many rules can be confusing, there
is no reason to aim for a minimal set of rules. See the file
-\ttindexbold{ZF/zf.ML} for a complete listing.
+{\tt ZF/zf.ML} for a complete listing.
Figure~\ref{ZF-lemmas3} presents rules for general union and intersection.
The empty intersection should be undefined. We cannot have
@@ -684,7 +688,7 @@
(\ttindex{mem_anti_sym}) is proved by applying the axiom of foundation to
the set $\{a,b\}$. The impossibility of $a\in a$ is a trivial consequence.
-See the file \ttindexbold{ZF/upair.ML} for full details.
+See the file {\tt ZF/upair.ML} for full details.
%%% subset.ML
@@ -718,7 +722,7 @@
Figure~\ref{ZF-subset} shows that the subset relation is a complete
lattice. Unions form least upper bounds; non-empty intersections form
greatest lower bounds. A few other laws involving subsets are included.
-See the file \ttindexbold{ZF/subset.ML}.
+See the file {\tt ZF/subset.ML}.
%%% pair.ML
@@ -731,7 +735,7 @@
\idx{fst} fst(<a,b>) = a
\idx{snd} snd(<a,b>) = b
-\idx{split} split(%x y.c(x,y), <a,b>) = c(a,b)
+\idx{split} split(\%x y.c(x,y), <a,b>) = c(a,b)
\idx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)
@@ -747,7 +751,7 @@
\subsection{Ordered pairs}
Figure~\ref{ZF-pair} presents the rules governing ordered pairs,
-projections and general sums. File \ttindexbold{ZF/pair.ML} contains the
+projections and general sums. File {\tt ZF/pair.ML} contains the
full (and tedious) proof that $\{\{a\},\{a,b\}\}$ functions as an ordered
pair. This property is expressed as two destruction rules,
\ttindexbold{Pair_inject1} and \ttindexbold{Pair_inject2}, and equivalently
@@ -811,7 +815,7 @@
the field of a relation is merely the union of its domain and range. Note
that image and inverse image are generalizations of range and domain,
respectively. See the file
-\ttindexbold{ZF/domrange.ML} for derivations of the rules.
+{\tt ZF/domrange.ML} for derivations of the rules.
%%% func.ML
@@ -876,7 +880,7 @@
\subsection{Functions}
Functions, represented by graphs, are notoriously difficult to reason
-about. The file \ttindexbold{ZF/func.ML} derives many rules, which overlap
+about. The file {\tt ZF/func.ML} derives many rules, which overlap
more than they ought. One day these rules will be tidied up; this section
presents only the more important ones.
@@ -907,7 +911,7 @@
\begin{center}
\begin{tabular}{rrr}
\it name &\it meta-type & \it description \\
- \idx{id} & $i$ & identity function \\
+ \idx{id} & $\To i$ & identity function \\
\idx{inj} & $[i,i]\To i$ & injective function space\\
\idx{surj} & $[i,i]\To i$ & surjective function space\\
\idx{bij} & $[i,i]\To i$ & bijective function space
@@ -1104,7 +1108,7 @@
\idx{sum_def} A+B == \{0\}*A Un \{1\}*B
\idx{Inl_def} Inl(a) == <0,a>
\idx{Inr_def} Inr(b) == <1,b>
-\idx{case_def} case(c,d,u) == split(%y z. cond(y, d(z), c(z)), u)
+\idx{case_def} case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u)
\subcaption{Definitions}
\idx{bool_1I} 1 : bool
@@ -1140,7 +1144,7 @@
\idx{qsum_def} A <+> B == (\{0\} <*> A) Un (\{1\} <*> B)
\idx{QInl_def} QInl(a) == <0;a>
\idx{QInr_def} QInr(b) == <1;b>
-\idx{qcase_def} qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))
+\idx{qcase_def} qcase(c,d) == qsplit(\%y z. cond(y, d(z), c(z)))
\end{ttbox}
\caption{Non-standard pairs, products and sums} \label{zf-qpair}
\end{figure}
@@ -1154,13 +1158,13 @@
THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))
\idx{rec_def} rec(k,a,b) ==
- transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))
+ transrec(k, \%n f. nat_case(a, \%m. b(m, f`m), n))
-\idx{add_def} m#+n == rec(m, n, %u v.succ(v))
-\idx{diff_def} m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))
-\idx{mult_def} m#*n == rec(m, 0, %u v. n #+ v)
-\idx{mod_def} m mod n == transrec(m, %j f. if(j:n, j, f`(j#-n)))
-\idx{div_def} m div n == transrec(m, %j f. if(j:n, 0, succ(f`(j#-n))))
+\idx{add_def} m#+n == rec(m, n, \%u v.succ(v))
+\idx{diff_def} m#-n == rec(n, m, \%u v. rec(v, 0, \%x y.x))
+\idx{mult_def} m#*n == rec(m, 0, \%u v. n #+ v)
+\idx{mod_def} m mod n == transrec(m, \%j f. if(j:n, j, f`(j#-n)))
+\idx{div_def} m div n == transrec(m, \%j f. if(j:n, 0, succ(f`(j#-n))))
\subcaption{Definitions}
\idx{nat_0I} 0 : nat
@@ -1213,13 +1217,13 @@
\begin{figure}\underscoreon %%because @ is used here
\begin{ttbox}
\idx{list_rec_def} list_rec(l,c,h) ==
- Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))
+ Vrec(l, \%l g.list_case(c, \%x xs. h(x, xs, g`xs), l))
-\idx{map_def} map(f,l) == list_rec(l, 0, %x xs r. <f(x), r>)
-\idx{length_def} length(l) == list_rec(l, 0, %x xs r. succ(r))
-\idx{app_def} xs@ys == list_rec(xs, ys, %x xs r. <x,r>)
-\idx{rev_def} rev(l) == list_rec(l, 0, %x xs r. r @ <x,0>)
-\idx{flat_def} flat(ls) == list_rec(ls, 0, %l ls r. l @ r)
+\idx{map_def} map(f,l) == list_rec(l, 0, \%x xs r. <f(x), r>)
+\idx{length_def} length(l) == list_rec(l, 0, \%x xs r. succ(r))
+\idx{app_def} xs@ys == list_rec(xs, ys, \%x xs r. <x,r>)
+\idx{rev_def} rev(l) == list_rec(l, 0, \%x xs r. r @ <x,0>)
+\idx{flat_def} flat(ls) == list_rec(ls, 0, \%l ls r. l @ r)
\subcaption{Definitions}
\idx{NilI} Nil : list(A)
@@ -1239,8 +1243,8 @@
\idx{list_rec_Nil} list_rec(Nil,c,h) = c
\idx{list_rec_Cons} list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))
-\idx{map_ident} l: list(A) ==> map(%u.u, l) = l
-\idx{map_compose} l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)
+\idx{map_ident} l: list(A) ==> map(\%u.u, l) = l
+\idx{map_compose} l: list(A) ==> map(h, map(j,l)) = map(\%u.h(j(u)), l)
\idx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)
\idx{map_type}
[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)
@@ -1258,12 +1262,12 @@
Figure~\ref{zf-equalities} presents commutative, associative, distributive,
and idempotency laws of union and intersection, along with other equations.
-See file \ttindexbold{ZF/equalities.ML}.
+See file {\tt ZF/equalities.ML}.
Figure~\ref{zf-sum} defines $\{0,1\}$ as a set of booleans, with the usual
operators including a conditional. It also defines the disjoint union of
two sets, with injections and a case analysis operator. See files
-\ttindexbold{ZF/bool.ML} and \ttindexbold{ZF/sum.ML}.
+{\tt ZF/bool.ML} and {\tt ZF/sum.ML}.
Figure~\ref{zf-qpair} defines a notion of ordered pair that admits
non-well-founded tupling. Such pairs are written {\tt<$a$;$b$>}. It also
@@ -1276,35 +1280,35 @@
Monotonicity properties of most of the set-forming operations are proved.
These are useful for applying the Knaster-Tarski Fixedpoint Theorem.
-See file \ttindexbold{ZF/mono.ML}.
+See file {\tt ZF/mono.ML}.
Figure~\ref{zf-fixedpt} presents the Knaster-Tarski Fixedpoint Theorem, proved
for the lattice of subsets of a set. The theory defines least and greatest
fixedpoint operators with corresponding induction and co-induction rules.
Later definitions use these, such as the natural numbers and
the transitive closure operator. The (co-)inductive definition
-package also uses them. See file \ttindexbold{ZF/fixedpt.ML}.
+package also uses them. See file {\tt ZF/fixedpt.ML}.
Figure~\ref{zf-perm} defines composition and injective, surjective and
bijective function spaces, with proofs of many of their properties.
-See file \ttindexbold{ZF/perm.ML}.
+See file {\tt ZF/perm.ML}.
Figure~\ref{zf-nat} presents the natural numbers, with induction and a
-primitive recursion operator. See file \ttindexbold{ZF/nat.ML}. File
-\ttindexbold{ZF/arith.ML} develops arithmetic on the natural numbers. It
+primitive recursion operator. See file {\tt ZF/nat.ML}. File
+{\tt ZF/arith.ML} develops arithmetic on the natural numbers. It
defines addition, multiplication, subtraction, division, and remainder,
proving the theorem $a \bmod b + (a/b)\times b = a$. Division and
remainder are defined by repeated subtraction, which requires well-founded
rather than primitive recursion.
-The file \ttindexbold{ZF/univ.ML} defines a ``universe'' ${\tt univ}(A)$,
+The file {\tt ZF/univ.ML} defines a ``universe'' ${\tt univ}(A)$,
for constructing datatypes such as trees. This set contains $A$ and the
natural numbers. Vitally, it is closed under finite products: ${\tt
univ}(A)\times{\tt univ}(A)\subseteq{\tt univ}(A)$. This file also
defines set theory's cumulative hierarchy, traditionally written $V@\alpha$
where $\alpha$ is any ordinal.
-The file \ttindexbold{ZF/quniv.ML} defines a ``universe'' ${\tt quniv}(A)$,
+The file {\tt ZF/quniv.ML} defines a ``universe'' ${\tt quniv}(A)$,
for constructing co-datatypes such as streams. It is analogous to ${\tt
univ}(A)$ but is closed under the non-standard product and sum.
@@ -1312,34 +1316,34 @@
set of all finite sets over~$A$. The definition employs Isabelle's
inductive definition package, which proves the introduction rules
automatically. The induction rule shown is stronger than the one proved by
-the package. See file \ttindexbold{ZF/fin.ML}.
+the package. See file {\tt ZF/fin.ML}.
Figure~\ref{zf-list} presents the set of lists over~$A$, ${\tt list}(A)$.
The definition employs Isabelle's datatype package, which defines the
introduction and induction rules automatically, as well as the constructors
-and case operator (\verb|list_case|). See file \ttindexbold{ZF/list.ML}.
-The file \ttindexbold{ZF/listfn.thy} proceeds to define structural
+and case operator (\verb|list_case|). See file {\tt ZF/list.ML}.
+The file {\tt ZF/listfn.thy} proceeds to define structural
recursion and the usual list functions.
The constructions of the natural numbers and lists make use of a suite of
operators for handling recursive function definitions. The developments are
summarized below:
\begin{description}
-\item[\ttindexbold{ZF/trancl.ML}]
+\item[{\tt ZF/trancl.ML}]
defines the transitive closure of a relation (as a least fixedpoint).
-\item[\ttindexbold{ZF/wf.ML}]
+\item[{\tt ZF/wf.ML}]
proves the Well-Founded Recursion Theorem, using an elegant
approach of Tobias Nipkow. This theorem permits general recursive
definitions within set theory.
-\item[\ttindexbold{ZF/ord.ML}] defines the notions of transitive set and
+\item[{\tt ZF/ord.ML}] defines the notions of transitive set and
ordinal number. It derives transfinite induction. A key definition is
{\bf less than}: $i<j$ if and only if $i$ and $j$ are both ordinals and
$i\in j$. As a special case, it includes less than on the natural
numbers.
-\item[\ttindexbold{ZF/epsilon.ML}]
+\item[{\tt ZF/epsilon.ML}]
derives $\epsilon$-induction and $\epsilon$-recursion, which are
generalizations of transfinite induction. It also defines
\ttindexbold{rank}$(x)$, which is the least ordinal $\alpha$ such that $x$
@@ -1367,7 +1371,7 @@
\section{Simplification rules}
{\ZF} does not merely inherit simplification from \FOL, but instantiates
-the rewriting package new. File \ttindexbold{ZF/simpdata.ML} contains the
+the rewriting package new. File {\tt ZF/simpdata.ML} contains the
details; here is a summary of the key differences:
\begin{itemize}
\item
@@ -1379,7 +1383,7 @@
\ttindexbold{ZF_ss} contains congruence rules for all the operators of
{\ZF}, including the binding operators. It contains all the conversion
rules, such as \ttindex{fst} and \ttindex{snd}, as well as the
-rewrites shown in Figure~\ref{ZF-simpdata}.
+rewrites shown in Fig.\ts\ref{ZF-simpdata}.
\item
\ttindexbold{FOL_ss} is redeclared with the same {\FOL} rules as the
previous version, so that it may still be used.
@@ -1390,61 +1394,61 @@
This directory contains further developments in {\ZF} set theory. Here is
an overview; see the files themselves for more details.
\begin{description}
-\item[\ttindexbold{ZF/ex/misc.ML}] contains miscellaneous examples such as
+\item[{\tt ZF/ex/misc.ML}] contains miscellaneous examples such as
Cantor's Theorem, the Schr\"oder-Bernstein Theorem. and the
``Composition of homomorphisms'' challenge~\cite{boyer86}.
-\item[\ttindexbold{ZF/ex/ramsey.ML}]
+\item[{\tt ZF/ex/ramsey.ML}]
proves the finite exponent 2 version of Ramsey's Theorem, following Basin
and Kaufmann's presentation~\cite{basin91}.
-\item[\ttindexbold{ZF/ex/equiv.ML}]
+\item[{\tt ZF/ex/equiv.ML}]
develops a ZF theory of equivalence classes, not using the Axiom of Choice.
-\item[\ttindexbold{ZF/ex/integ.ML}]
+\item[{\tt ZF/ex/integ.ML}]
develops a theory of the integers as equivalence classes of pairs of
natural numbers.
-\item[\ttindexbold{ZF/ex/bin.ML}]
+\item[{\tt ZF/ex/bin.ML}]
defines a datatype for two's complement binary integers. File
-\ttindexbold{ZF/ex/binfn.ML} then develops rewrite rules for binary
+{\tt binfn.ML} then develops rewrite rules for binary
arithmetic. For instance, $1359\times {-}2468 = {-}3354012$ takes under
14 seconds.
-\item[\ttindexbold{ZF/ex/bt.ML}]
+\item[{\tt ZF/ex/bt.ML}]
defines the recursive data structure ${\tt bt}(A)$, labelled binary trees.
-\item[\ttindexbold{ZF/ex/term.ML}]
- and \ttindexbold{ZF/ex/termfn.ML} define a recursive data structure for
+\item[{\tt ZF/ex/term.ML}]
+ and {\tt termfn.ML} define a recursive data structure for
terms and term lists. These are simply finite branching trees.
-\item[\ttindexbold{ZF/ex/tf.ML}]
- and \ttindexbold{ZF/ex/tf_fn.ML} define primitives for solving mutually
+\item[{\tt ZF/ex/tf.ML}]
+ and {\tt tf_fn.ML} define primitives for solving mutually
recursive equations over sets. It constructs sets of trees and forests
as an example, including induction and recursion rules that handle the
mutual recursion.
-\item[\ttindexbold{ZF/ex/prop.ML}]
- and \ttindexbold{ZF/ex/proplog.ML} proves soundness and completeness of
+\item[{\tt ZF/ex/prop.ML}]
+ and {\tt proplog.ML} proves soundness and completeness of
propositional logic. This illustrates datatype definitions, inductive
definitions, structural induction and rule induction.
-\item[\ttindexbold{ZF/ex/listn.ML}]
+\item[{\tt ZF/ex/listn.ML}]
presents the inductive definition of the lists of $n$ elements~\cite{paulin92}.
-\item[\ttindexbold{ZF/ex/acc.ML}]
+\item[{\tt ZF/ex/acc.ML}]
presents the inductive definition of the accessible part of a
relation~\cite{paulin92}.
-\item[\ttindexbold{ZF/ex/comb.ML}]
- presents the datatype definition of combinators. File
- \ttindexbold{ZF/ex/contract0.ML} defines contraction, while file
- \ttindexbold{ZF/ex/parcontract.ML} defines parallel contraction and
+\item[{\tt ZF/ex/comb.ML}]
+ presents the datatype definition of combinators. The file
+ {\tt contract0.ML} defines contraction, while file
+ {\tt parcontract.ML} defines parallel contraction and
proves the Church-Rosser Theorem. This case study follows Camilleri and
Melham~\cite{camilleri92}.
-\item[\ttindexbold{ZF/ex/llist.ML}]
- and \ttindexbold{ZF/ex/llist_eq.ML} develop lazy lists in ZF and a notion
+\item[{\tt ZF/ex/llist.ML}]
+ and {\tt llist_eq.ML} develop lazy lists in ZF and a notion
of co-induction for proving equations between them.
\end{description}
@@ -1467,6 +1471,7 @@
{\out Level 0}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out 1. Pow(A Int B) = Pow(A) Int Pow(B)}
+\ttbreak
by (resolve_tac [equalityI] 1);
{\out Level 1}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
@@ -1493,6 +1498,7 @@
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out 1. Pow(A Int B) <= Pow(B)}
{\out 2. Pow(A) Int Pow(B) <= Pow(A Int B)}
+\ttbreak
by (resolve_tac [Int_lower2 RS Pow_mono] 1);
{\out Level 4}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
@@ -1507,8 +1513,9 @@
{\out 1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)}
\end{ttbox}
The subgoal is to show $x\in {\tt Pow}(A\cap B)$ assuming $x\in{\tt
-Pow}(A)\cap {\tt Pow}(B)$. Eliminating this assumption produces two
-subgoals, since intersection is like conjunction.\index{*IntE}
+Pow}(A)\cap {\tt Pow}(B)$; eliminating this assumption produces two
+subgoals. The rule \ttindex{IntE} treats the intersection like a conjunction
+instead of unfolding its definition.
\begin{ttbox}
by (eresolve_tac [IntE] 1);
{\out Level 6}
@@ -1523,41 +1530,52 @@
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B}
\end{ttbox}
-We perform the same replacement in the assumptions:\index{*PowD}
+We perform the same replacement in the assumptions. This is a good
+demonstration of the tactic \ttindex{dresolve_tac}:\index{*PowD}
\begin{ttbox}
by (REPEAT (dresolve_tac [PowD] 1));
{\out Level 8}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out 1. !!x. [| x <= A; x <= B |] ==> x <= A Int B}
\end{ttbox}
-Here, $x$ is a lower bound of $A$ and~$B$, but $A\inter B$ is the greatest
-lower bound:\index{*Int_greatest}
+The assumptions are that $x$ is a lower bound of both $A$ and~$B$, but
+$A\inter B$ is the greatest lower bound:\index{*Int_greatest}
\begin{ttbox}
by (resolve_tac [Int_greatest] 1);
{\out Level 9}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out 1. !!x. [| x <= A; x <= B |] ==> x <= A}
{\out 2. !!x. [| x <= A; x <= B |] ==> x <= B}
+\end{ttbox}
+To conclude the proof, we clear up the trivial subgoals:
+\begin{ttbox}
by (REPEAT (assume_tac 1));
{\out Level 10}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out No subgoals!}
\end{ttbox}
+\medskip
We could have performed this proof in one step by applying
-\ttindex{fast_tac} with the classical rule set \ttindex{ZF_cs}. But we
-must add \ttindex{equalityI} as an introduction rule, since extensionality
-is not used by default:
+\ttindex{fast_tac} with the classical rule set \ttindex{ZF_cs}. Let us
+go back to the start:
\begin{ttbox}
choplev 0;
{\out Level 0}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out 1. Pow(A Int B) = Pow(A) Int Pow(B)}
+\end{ttbox}
+We must add \ttindex{equalityI} to {\tt ZF_cs} as an introduction rule.
+Extensionality is not used by default because many equalities can be proved
+by rewriting.
+\begin{ttbox}
by (fast_tac (ZF_cs addIs [equalityI]) 1);
{\out Level 1}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out No subgoals!}
\end{ttbox}
-
+In the past this was regarded as a difficult proof, as indeed it is if all
+the symbols are replaced by their definitions.
+\goodbreak
\section{Monotonicity of the union operator}
For another example, we prove that general union is monotonic:
@@ -1619,10 +1637,10 @@
this premise to the assumptions using \ttindex{cut_facts_tac}, or add
\hbox{\tt prem RS subsetD} to \ttindex{ZF_cs} as an introduction rule.
-The file \ttindex{ZF/equalities.ML} has many similar proofs.
+The file {\tt ZF/equalities.ML} has many similar proofs.
Reasoning about general intersection can be difficult because of its anomalous
behavior on the empty set. However, \ttindex{fast_tac} copes well with
-these. Here is a typical example:
+these. Here is a typical example, borrowed from Devlin[page 12]{devlin79}:
\begin{ttbox}
a:C ==> (INT x:C. A(x) Int B(x)) = (INT x:C.A(x)) Int (INT x:C.B(x))
\end{ttbox}
@@ -1639,7 +1657,7 @@
underlying representation, as in the following proof
of~\ttindex{fun_disjoint_apply1}. This states that if $f$ and~$g$ are
functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then
-$(f\union g)`a = f`a$:
+$(f\un g)`a = f`a$:
\begin{ttbox}
val prems = goal ZF.thy
"[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ttback
@@ -1647,14 +1665,17 @@
{\out Level 0}
{\out (f Un g) ` a = f ` a}
{\out 1. (f Un g) ` a = f ` a}
-\ttbreak
+\end{ttbox}
+Isabelle has produced the output above; the \ML{} top-level now echoes the
+binding of {\tt prems}.
+\begin{ttbox}
{\out val prems = ["a : A [a : A]",}
{\out "f : A -> B [f : A -> B]",}
{\out "g : C -> D [g : C -> D]",}
{\out "A Int C = 0 [A Int C = 0]"] : thm list}
\end{ttbox}
Using \ttindex{apply_equality}, we reduce the equality to reasoning about
-ordered pairs.
+ordered pairs. The second subgoal is to verify that $f\un g$ is a function.
\begin{ttbox}
by (resolve_tac [apply_equality] 1);
{\out Level 1}
@@ -1722,5 +1743,5 @@
{\out (f Un g) ` a = f ` a}
{\out No subgoals!}
\end{ttbox}
-See the files \ttindex{ZF/func.ML} and \ttindex{ZF/wf.ML} for more
+See the files {\tt ZF/func.ML} and {\tt ZF/wf.ML} for more
examples of reasoning about functions.
--- a/doc-src/Logics/intro.tex Mon Mar 21 11:02:57 1994 +0100
+++ b/doc-src/Logics/intro.tex Mon Mar 21 11:41:41 1994 +0100
@@ -1,5 +1,5 @@
%% $Id$
-\chapter{Introduction}
+\chapter{Basic Concepts}
Several logics come with Isabelle. Many of them are sufficiently developed
to serve as comfortable reasoning environments. They are also good
starting points for defining new logics. Each logic is distributed with
@@ -35,14 +35,13 @@
\end{quote}
The logics {\tt Modal}, {\tt Cube} and {\tt LCF} are currently undocumented.
-This manual assumes that you have read the {\em Introduction to Isabelle\/}
-and have some experience of using Isabelle to perform interactive proofs.
-It refers to packages defined in the {\em Reference Manual}, which you
-should keep at hand.
+You should not read this before reading {\em Introduction to Isabelle\/}
+and performing some Isabelle proofs. Consult the {\em Reference Manual}
+for more information on tactics, packages, etc.
\section{Syntax definitions}
-This manual defines each logic's syntax using a context-free grammar.
+The syntax of each logic syntax is defined using a context-free grammar.
These grammars obey the following conventions:
\begin{itemize}
\item identifiers denote nonterminal symbols
--- a/doc-src/Logics/logics.tex Mon Mar 21 11:02:57 1994 +0100
+++ b/doc-src/Logics/logics.tex Mon Mar 21 11:41:41 1994 +0100
@@ -1,4 +1,4 @@
-\documentstyle[a4,12pt,proof,iman,alltt]{report}
+\documentstyle[a4,12pt,proof,iman,extra]{report}
%% $Id$
%%%STILL NEEDS MODAL, LCF
%%%\includeonly{ZF}
@@ -34,6 +34,9 @@
\let\idx=\ttindexbold
%%%%\newcommand\idx[1]{\indexbold{*#1}#1}
+%%\newenvironment{example}{\begin{Example}\rm}{\end{Example}}
+%%\newtheorem{Example}{Example}[chapter]
+
\underscoreoff
\setcounter{secnumdepth}{1} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???