# HG changeset patch # User lcp # Date 753097273 -3600 # Node ID 96c627d2815ea78c41f2b91f9b0f7d3d97b63512 # Parent 1e669b5a75f9684a1829c52f09cf6ff1c5a0a6a3 Misc updates diff -r 1e669b5a75f9 -r 96c627d2815e doc-src/Logics/CTT.tex --- 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())} {\out 1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->} {\out (PROD x:A. PROD y:B(x). C())} +\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. } {\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. } {\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. } {\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. } {\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. } {\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))} diff -r 1e669b5a75f9 -r 96c627d2815e doc-src/Logics/Old_HOL.tex --- 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} diff -r 1e669b5a75f9 -r 96c627d2815e doc-src/Logics/ZF.tex --- 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. diff -r 1e669b5a75f9 -r 96c627d2815e doc-src/Logics/logics.bbl --- 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.