--- a/doc-src/Logics/CTT.tex Thu Nov 11 13:24:47 1993 +0100
+++ b/doc-src/Logics/CTT.tex Fri Nov 12 10:41:13 1993 +0100
@@ -775,6 +775,7 @@
{\out Level 0}
{\out ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
{\out 1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\ttbreak
{\out val prems = ["A type [A type]",}
{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
{\out "?x : A ==> C(?x) type [!!x. x : A ==> C(x) type]",}
@@ -808,6 +809,7 @@
{\out 1. !!x y xa.}
{\out [| x : A; xa : B(x) |] ==>}
{\out ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\ttbreak
{\out 2. !!x y ya.}
{\out [| x : A; ya : C(x) |] ==>}
{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
@@ -824,6 +826,7 @@
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
{\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)}
{\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
+\ttbreak
{\out 3. !!x y ya.}
{\out [| x : A; ya : C(x) |] ==>}
{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
@@ -906,6 +909,7 @@
{\out ?a : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
{\out 1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
{\out (PROD x:A. PROD y:B(x). C(<x,y>))}
+\ttbreak
{\out val prems = ["A type [A type]",}
{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
{\out "?z : SUM x:A. B(x) ==> C(?z) type}
@@ -995,9 +999,11 @@
{\out lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>}
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
{\out 1. !!uu x.}
{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
{\out ?b7(uu,x) : B(x)}
+\ttbreak
{\out 2. !!uu x.}
{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
{\out ?b8(uu,x) : C(x,(lam x. ?b7(uu,x)) ` x)}
@@ -1013,6 +1019,7 @@
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
{\out 1. !!uu x. x : A ==> x : A}
{\out 2. !!uu x.}
{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
@@ -1040,9 +1047,11 @@
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
{\out 1. !!uu x.}
{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
{\out C(x,(lam x. fst(uu ` x)) ` x) = ?A13(uu,x)}
+\ttbreak
{\out 2. !!uu x.}
{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
{\out ?b8(uu,x) : ?A13(uu,x)}
@@ -1055,13 +1064,16 @@
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
{\out 1. !!uu x.}
{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
{\out (lam x. fst(uu ` x)) ` x = ?c14(uu,x) : ?A14(uu,x)}
+\ttbreak
{\out 2. !!uu x z.}
{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;}
{\out z : ?A14(uu,x) |] ==>}
{\out C(x,z) type}
+\ttbreak
{\out 3. !!uu x.}
{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
{\out ?b8(uu,x) : C(x,?c14(uu,x))}
@@ -1074,16 +1086,20 @@
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
{\out 1. !!uu x.}
{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> x : ?A15(uu,x)}
+\ttbreak
{\out 2. !!uu x xa.}
{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;}
{\out xa : ?A15(uu,x) |] ==>}
{\out fst(uu ` xa) : ?B15(uu,x,xa)}
+\ttbreak
{\out 3. !!uu x z.}
{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;}
{\out z : ?B15(uu,x,x) |] ==>}
{\out C(x,z) type}
+\ttbreak
{\out 4. !!uu x.}
{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
{\out ?b8(uu,x) : C(x,fst(uu ` x))}
--- a/doc-src/Logics/Old_HOL.tex Thu Nov 11 13:24:47 1993 +0100
+++ b/doc-src/Logics/Old_HOL.tex Fri Nov 12 10:41:13 1993 +0100
@@ -525,7 +525,7 @@
\idx{Collect_mem_eq} \{x.x:A\} = A
\subcaption{Isomorphisms between predicates and sets}
-\idx{empty_def} \{\} == \{x.x= False\}
+\idx{empty_def} \{\} == \{x.x= False\}
\idx{insert_def} insert(a,B) == \{x.x=a\} Un B
\idx{Ball_def} Ball(A,P) == ! x. x:A --> P(x)
\idx{Bex_def} Bex(A,P) == ? x. x:A & P(x)
@@ -599,7 +599,7 @@
\idx{insertI1} a : insert(a,B)
\idx{insertI2} a : B ==> a : insert(b,B)
-\idx{insertE} [| a : insert(b,A); a=b ==> P; a:A ==> P |] ==>
+\idx{insertE} [| a : insert(b,A); a=b ==> P; a:A ==> P |] ==> P
\idx{ComplI} [| c:A ==> False |] ==> c : Compl(A)
\idx{ComplD} [| c : Compl(A) |] ==> ~ c:A
@@ -1144,7 +1144,7 @@
\section{The examples directories}
Directory {\tt Subst} contains Martin Coen's mechanization of a theory of
substitutions and unifiers. It is based on Paulson's previous
-mechanization in {\LCF}~\cite{paulson85} of theory Manna and Waldinger's
+mechanization in {\LCF}~\cite{paulson85} of Manna and Waldinger's
theory~\cite{mw81}.
Directory {\tt ex} contains other examples and experimental proofs in
@@ -1268,8 +1268,8 @@
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
+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}
\begin{ttbox}
--- a/doc-src/Logics/ZF.tex Thu Nov 11 13:24:47 1993 +0100
+++ b/doc-src/Logics/ZF.tex Fri Nov 12 10:41:13 1993 +0100
@@ -753,11 +753,10 @@
\ttindexbold{Pair_inject1} and \ttindexbold{Pair_inject2}, and equivalently
as the elimination rule \ttindexbold{Pair_inject}.
-Note the rule \ttindexbold{Pair_neq_0}, which asserts
-$\pair{a,b}\neq\emptyset$. This is no arbitrary property of
-$\{\{a\},\{a,b\}\}$, but one that we can reasonably expect to hold for any
-encoding of ordered pairs. It turns out to be useful for constructing
-Lisp-style S-expressions in set theory.
+The rule \ttindexbold{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$. This
+is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other
+encoding of ordered pairs. The non-standard ordered pairs mentioned below
+satisfy $\pair{\emptyset;\emptyset}=\emptyset$.
The natural deduction rules \ttindexbold{SigmaI} and \ttindexbold{SigmaE}
assert that \ttindex{Sigma}$(A,B)$ consists of all pairs of the form
@@ -1193,14 +1192,13 @@
\idx{Fin_0I} 0 : Fin(A)
\idx{Fin_consI} [| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)
-\idx{Fin_mono} A<=B ==> Fin(A) <= Fin(B)
-
\idx{Fin_induct}
[| b: Fin(A);
P(0);
!!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y))
|] ==> P(b)
+\idx{Fin_mono} A<=B ==> Fin(A) <= Fin(B)
\idx{Fin_UnI} [| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)
\idx{Fin_UnionI} C : Fin(Fin(A)) ==> Union(C) : Fin(A)
\idx{Fin_subset} [| c<=b; b: Fin(A) |] ==> c: Fin(A)
@@ -1254,6 +1252,10 @@
some of the further constants and infixes that are declared in the various
theory extensions.
+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}.
+
Figure~\ref{zf-sum} defines $\{0,1\}$ as a set of booleans, with a
conditional operator. It also defines the disjoint union of two sets, with
injections and a case analysis operator. See files
@@ -1265,16 +1267,13 @@
\ttindexbold{qconverse}, and the summation operator \ttindexbold{QSigma}.
These are completely analogous to the corresponding versions for standard
ordered pairs. The theory goes on to define a non-standard notion of
-disjoint sum using non-standard pairs. See file \ttindexbold{qpair.thy}.
+disjoint sum using non-standard pairs. This will support co-inductive
+definitions, for example of infinite lists. See file \ttindexbold{qpair.thy}.
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}.
-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}.
-
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.
@@ -1302,7 +1301,7 @@
where $\alpha$ is any ordinal.
The file \ttindexbold{ZF/quniv.ML} defines a ``universe'' ${\tt quniv}(A)$,
-for constructing co-datatypes such as streams. It is similar to ${\tt
+for constructing co-datatypes such as streams. It is analogous to ${\tt
univ}(A)$ but is closed under the non-standard product and sum.
Figure~\ref{zf-fin} presents the finite set operator; ${\tt Fin}(A)$ is the
@@ -1392,39 +1391,68 @@
``Composition of homomorphisms'' challenge~\cite{boyer86}.
\item[\ttindexbold{ZF/ex/ramsey.ML}]
-proves the finite exponent 2 version of Ramsey's Theorem.
+proves the finite exponent 2 version of Ramsey's Theorem, following Basin
+and Kaufmann's presentation~\cite{basin91}.
+
+\item[\ttindexbold{ZF/ex/equiv.ML}]
+develops a ZF theory of equivalence classes, not using the Axiom of Choice.
+
+\item[\ttindexbold{ZF/ex/integ.ML}]
+develops a theory of the integers as equivalence classes of pairs of
+natural numbers.
+
+\item[\ttindexbold{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
+arithmetic. For instance, $1359\times {-}2468 = {-}3354012$ takes under
+14 seconds.
\item[\ttindexbold{ZF/ex/bt.ML}]
defines the recursive data structure ${\tt bt}(A)$, labelled binary trees.
-\item[\ttindexbold{ZF/ex/sexp.ML}]
-defines the set of Lisp $S$-expressions over~$A$, ${\tt sexp}(A)$. These
-are unlabelled binary trees whose leaves contain elements of $(A)$.
-
-\item[\ttindexbold{ZF/ex/term.ML}]
-defines a recursive data structure for terms and term lists.
+\item[\ttindexbold{ZF/ex/term.ML}]
+ and \ttindexbold{ZF/ex/termfn.ML} define a recursive data structure for
+ terms and term lists. These are simply finite branching trees.
\item[\ttindexbold{ZF/ex/tf.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.
+ and \ttindexbold{ZF/ex/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
+ propositional logic. This illustrates datatype definitions, inductive
+ definitions, structural induction and rule induction.
+
+\item[\ttindexbold{ZF/ex/listn.ML}]
+presents the inductive definition of the lists of $n$ elements~\cite{paulin92}.
-\item[\ttindexbold{ZF/ex/finite.ML}]
-inductively defines a finite powerset operator.
+\item[\ttindexbold{ZF/ex/acc.ML}]
+presents the inductive definition of the accessible part of a
+relation~\cite{paulin92}.
-\item[\ttindexbold{ZF/ex/proplog.ML}]
-proves soundness and completeness of propositional logic. This illustrates
-the main forms of induction.
+\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
+ 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
+ of co-induction for proving equations between them.
\end{description}
\section{A proof about powersets}
-To demonstrate high-level reasoning about subsets, let us prove the equation
-${Pow(A)\cap Pow(B)}= Pow(A\cap B)$. Compared with first-order logic, set
-theory involves a maze of rules, and theorems have many different proofs.
-Attempting other proofs of the theorem might be instructive. This proof
-exploits the lattice properties of intersection. It also uses the
-monotonicity of the powerset operation, from {\tt ZF/mono.ML}:
+To demonstrate high-level reasoning about subsets, let us prove the
+equation ${{\tt Pow}(A)\cap {\tt Pow}(B)}= {\tt Pow}(A\cap B)$. Compared
+with first-order logic, set theory involves a maze of rules, and theorems
+have many different proofs. Attempting other proofs of the theorem might
+be instructive. This proof exploits the lattice properties of
+intersection. It also uses the monotonicity of the powerset operation,
+from {\tt ZF/mono.ML}:
\begin{ttbox}
\idx{Pow_mono} A<=B ==> Pow(A) <= Pow(B)
\end{ttbox}
@@ -1536,6 +1564,8 @@
{\out Level 0}
{\out Union(C) <= Union(D)}
{\out 1. Union(C) <= Union(D)}
+{\out val prem = "C <= D [C <= D]" : thm}
+\ttbreak
by (resolve_tac [subsetI] 1);
{\out Level 1}
{\out Union(C) <= Union(D)}
@@ -1613,6 +1643,11 @@
{\out Level 0}
{\out (f Un g) ` a = f ` a}
{\out 1. (f Un g) ` a = f ` a}
+\ttbreak
+{\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.
--- a/doc-src/Logics/logics.bbl Thu Nov 11 13:24:47 1993 +0100
+++ b/doc-src/Logics/logics.bbl Fri Nov 12 10:41:13 1993 +0100
@@ -6,11 +6,24 @@
Through Proof}.
\newblock Academic Press, 1986.
+\bibitem{basin91}
+David Basin and Matt Kaufmann.
+\newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison.
+\newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical
+ Frameworks}, pages 89--119. Cambridge University Press, 1991.
+
\bibitem{boyer86}
Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and
Lawrence Wos.
\newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms.
-\newblock {\em Journal of Automated Reasoning}, 2:287--327, 1986.
+\newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986.
+
+\bibitem{camilleri92}
+J.~Camilleri and T.~F. Melham.
+\newblock Reasoning with inductively defined relations in the {HOL} theorem
+ prover.
+\newblock Technical Report 265, University of Cambridge Computer Laboratory,
+ August 1992.
\bibitem{church40}
Alonzo Church.
@@ -20,7 +33,7 @@
\bibitem{dummett}
Michael Dummett.
\newblock {\em Elements of Intuitionism}.
-\newblock Oxford, 1977.
+\newblock Oxford University Press, 1977.
\bibitem{dyckhoff}
Roy Dyckhoff.
@@ -35,6 +48,12 @@
Programming}, pages 157--178. Springer, 1991.
\newblock LNAI 475.
+\bibitem{frost93}
+Jacob Frost.
+\newblock A case study of co-induction in {Isabelle HOL}.
+\newblock Technical Report 308, University of Cambridge Computer Laboratory,
+ August 1993.
+
\bibitem{OBJ}
K.~Futatsugi, J.A. Goguen, Jean-Pierre Jouannaud, and J.~Meseguer.
\newblock Principles of {OBJ2}.
@@ -47,7 +66,7 @@
Proving}.
\newblock Harper \& Row, 1986.
-\bibitem{gordon88a}
+\bibitem{mgordon88a}
Michael J.~C. Gordon.
\newblock {HOL}: A proof generating system for higher-order logic.
\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em {VLSI}
@@ -65,27 +84,48 @@
second-order patterns.
\newblock {\em Acta Informatica}, 11:31--55, 1978.
+\bibitem{mw81}
+Zohar Manna and Richard Waldinger.
+\newblock Deductive synthesis of the unification algorithm.
+\newblock {\em Science of Computer Programming}, 1(1):5--48, 1981.
+
\bibitem{martinlof84}
Per Martin-L\"of.
\newblock {\em Intuitionistic type theory}.
\newblock Bibliopolis, 1984.
-\bibitem{nipkow-prehofer}
-Tobias Nipkow and Christian Prehofer.
-\newblock Type checking type classes.
-\newblock In {\em 20th ACM Symp.\ Principles of Programming Languages}, 1993.
-\newblock To appear.
+\bibitem{milner-coind}
+Robin Milner and Mads Tofte.
+\newblock Co-induction in relational semantics.
+\newblock {\em Theoretical Computer Science}, 87:209--220, 1991.
\bibitem{noel}
Philippe {No\"el}.
\newblock Experimenting with {Isabelle} in {ZF} set theory.
-\newblock {\em Journal of Automated Reasoning}.
-\newblock In press.
+\newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993.
\bibitem{nordstrom90}
Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
-\newblock Oxford, 1990.
+\newblock Oxford University Press, 1990.
+
+\bibitem{paulin92}
+Christine Paulin-Mohring.
+\newblock Inductive definitions in the system {Coq}: Rules and properties.
+\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon,
+ December 1992.
+
+\bibitem{paulson-set-I}
+Lawrence~C. Paulson.
+\newblock Set theory for verification: {I}. {From} foundations to functions.
+\newblock {\em Journal of Automated Reasoning}.
+\newblock In press; draft available as Report 271, University of Cambridge
+ Computer Laboratory.
+
+\bibitem{paulson85}
+Lawrence~C. Paulson.
+\newblock Verifying the unification algorithm in {LCF}.
+\newblock {\em Science of Computer Programming}, 5:143--170, 1985.
\bibitem{paulson87}
Lawrence~C. Paulson.
@@ -100,6 +140,29 @@
of Sciences, Springer.
\newblock LNCS 417.
+\bibitem{paulson91}
+Lawrence~C. Paulson.
+\newblock {\em {ML} for the Working Programmer}.
+\newblock Cambridge University Press, 1991.
+
+\bibitem{paulson-coind}
+Lawrence~C. Paulson.
+\newblock Co-induction and co-recursion in higher-order logic.
+\newblock Technical Report 304, University of Cambridge Computer Laboratory,
+ July 1993.
+
+\bibitem{paulson-fixedpt}
+Lawrence~C. Paulson.
+\newblock A fixedpoint approach to implementing (co-)inductive definitions.
+\newblock Technical report, University of Cambridge Computer Laboratory, 1993.
+\newblock Draft.
+
+\bibitem{paulson-set-II}
+Lawrence~C. Paulson.
+\newblock Set theory for verification: {II}. {Induction} and recursion.
+\newblock Technical Report 312, University of Cambridge Computer Laboratory,
+ 1993.
+
\bibitem{pelletier86}
F.~J. Pelletier.
\newblock Seventy-five problems for testing automatic theorem provers.