# HG changeset patch # User lcp # Date 753020329 -3600 # Node ID 1b3cddf41b2dfa04c915ded2997cbadfe450f9c3 # Parent a931f1b451511ebc17a94fb936d57d57bd889ad9 Various updates for Isabelle-93 diff -r a931f1b45151 -r 1b3cddf41b2d doc-src/Logics/CTT.tex --- a/doc-src/Logics/CTT.tex Thu Nov 11 12:44:43 1993 +0100 +++ b/doc-src/Logics/CTT.tex Thu Nov 11 13:18:49 1993 +0100 @@ -24,9 +24,9 @@ $\Imp$: \[ \begin{array}{r@{}l} \Forall x@1\ldots x@n. & - \List{x@1\in A@1; - x@2\in A@2(x@1); \cdots \; - x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\ + \List{x@1\in A@1; + x@2\in A@2(x@1); \cdots \; + x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\ & \qquad\qquad a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) \end{array} \] @@ -64,31 +64,31 @@ \begin{figure} \tabcolsep=1em %wider spacing in tables \begin{center} \begin{tabular}{rrr} - \it symbol & \it meta-type & \it description \\ - \idx{Type} & $t \to prop$ & judgement form \\ - \idx{Eqtype} & $[t,t]\to prop$ & judgement form\\ - \idx{Elem} & $[i, t]\to prop$ & judgement form\\ - \idx{Eqelem} & $[i, i, t]\to prop$ & judgement form\\ - \idx{Reduce} & $[i, i]\to prop$ & extra judgement form\\[2ex] + \it symbol & \it meta-type & \it description \\ + \idx{Type} & $t \to prop$ & judgement form \\ + \idx{Eqtype} & $[t,t]\to prop$ & judgement form\\ + \idx{Elem} & $[i, t]\to prop$ & judgement form\\ + \idx{Eqelem} & $[i, i, t]\to prop$ & judgement form\\ + \idx{Reduce} & $[i, i]\to prop$ & extra judgement form\\[2ex] - \idx{N} & $t$ & natural numbers type\\ - \idx{0} & $i$ & constructor\\ - \idx{succ} & $i\to i$ & constructor\\ + \idx{N} & $t$ & natural numbers type\\ + \idx{0} & $i$ & constructor\\ + \idx{succ} & $i\to i$ & constructor\\ \idx{rec} & $[i,i,[i,i]\to i]\to i$ & eliminator\\[2ex] - \idx{Prod} & $[t,i\to t]\to t$ & general product type\\ - \idx{lambda} & $(i\to i)\to i$ & constructor\\[2ex] - \idx{Sum} & $[t, i\to t]\to t$ & general sum type\\ - \idx{pair} & $[i,i]\to i$ & constructor\\ - \idx{split} & $[i,[i,i]\to i]\to i$ & eliminator\\ - \idx{fst} snd & $i\to i$ & projections\\[2ex] - \idx{inl} inr & $i\to i$ & constructors for $+$\\ + \idx{Prod} & $[t,i\to t]\to t$ & general product type\\ + \idx{lambda} & $(i\to i)\to i$ & constructor\\[2ex] + \idx{Sum} & $[t, i\to t]\to t$ & general sum type\\ + \idx{pair} & $[i,i]\to i$ & constructor\\ + \idx{split} & $[i,[i,i]\to i]\to i$ & eliminator\\ + \idx{fst} snd & $i\to i$ & projections\\[2ex] + \idx{inl} inr & $i\to i$ & constructors for $+$\\ \idx{when} & $[i,i\to i, i\to i]\to i$ & eliminator for $+$\\[2ex] - \idx{Eq} & $[t,i,i]\to t$ & equality type\\ - \idx{eq} & $i$ & constructor\\[2ex] - \idx{F} & $t$ & empty type\\ - \idx{contr} & $i\to i$ & eliminator\\[2ex] - \idx{T} & $t$ & singleton type\\ - \idx{tt} & $i$ & constructor + \idx{Eq} & $[t,i,i]\to t$ & equality type\\ + \idx{eq} & $i$ & constructor\\[2ex] + \idx{F} & $t$ & empty type\\ + \idx{contr} & $i\to i$ & eliminator\\[2ex] + \idx{T} & $t$ & singleton type\\ + \idx{tt} & $i$ & constructor \end{tabular} \end{center} \caption{The constants of {\CTT}} \label{ctt-constants} @@ -98,7 +98,7 @@ \begin{figure} \tabcolsep=1em %wider spacing in tables \begin{center} \begin{tabular}{llrrr} - \it symbol &\it name &\it meta-type & \it precedence & \it description \\ + \it symbol &\it name &\it meta-type & \it precedence & \it description \\ \idx{lam} & \idx{lambda} & $(i\To o)\To i$ & 10 & $\lambda$-abstraction \end{tabular} \end{center} @@ -109,8 +109,8 @@ \indexbold{*"+} \begin{tabular}{rrrr} \it symbol & \it meta-type & \it precedence & \it description \\ - \tt ` & $[i,i]\to i$ & Left 55 & function application\\ - \tt + & $[t,t]\to t$ & Right 30 & sum of two types + \tt ` & $[i,i]\to i$ & Left 55 & function application\\ + \tt + & $[t,t]\to t$ & Right 30 & sum of two types \end{tabular} \end{center} \subcaption{Infixes} @@ -119,15 +119,15 @@ \indexbold{*"-"-">} \begin{center} \tt\frenchspacing \begin{tabular}{rrr} - \it external & \it internal & \it standard notation \\ - \idx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x.B[x]$) & - \rm product $\prod@{x\in A}B[x]$ \\ - \idx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x.B[x]$) & - \rm sum $\sum@{x\in A}B[x]$ \\ + \it external & \it internal & \it standard notation \\ + \idx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x.B[x]$) & + \rm product $\prod@{x\in A}B[x]$ \\ + \idx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x.B[x]$) & + \rm sum $\sum@{x\in A}B[x]$ \\ $A$ --> $B$ & Prod($A$, $\lambda x.B$) & - \rm function space $A\to B$ \\ + \rm function space $A\to B$ \\ $A$ * $B$ & Sum($A$, $\lambda x.B$) & - \rm binary product $A\times B$ + \rm binary product $A\times B$ \end{tabular} \end{center} \subcaption{Translations} @@ -136,18 +136,18 @@ \begin{center} \dquotes \[ \begin{array}{rcl} -prop & = & type " type" \\ - & | & type " = " type \\ - & | & term " : " type \\ - & | & term " = " term " : " type +prop & = & type " type" \\ + & | & type " = " type \\ + & | & term " : " type \\ + & | & term " = " term " : " type \\[2ex] -type & = & \hbox{expression of type~$t$} \\ - & | & "PROD~" id " : " type " . " type \\ - & | & "SUM~~" id " : " type " . " type +type & = & \hbox{expression of type~$t$} \\ + & | & "PROD~" id " : " type " . " type \\ + & | & "SUM~~" id " : " type " . " type \\[2ex] -term & = & \hbox{expression of type~$i$} \\ - & | & "lam " id~id^* " . " term \\ - & | & "< " term " , " term " >" +term & = & \hbox{expression of type~$i$} \\ + & | & "lam " id~id^* " . " term \\ + & | & "< " term " , " term " >" \end{array} \] \end{center} @@ -594,11 +594,11 @@ \idx{absdiff_def} a|-|b == (a-b) #+ (b-a) \idx{mult_def} a#*b == rec(a, 0, %u v. b #+ v) -\idx{mod_def} a//b == rec(a, 0, +\idx{mod_def} a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y.succ(v))) -\idx{quo_def} a/b == rec(a, 0, - %u v. rec(succ(u) // b, succ(v), %x y.v)) +\idx{div_def} a div b == rec(a, 0, + %u v. rec(succ(u) mod b, succ(v), %x y.v)) \end{ttbox} \subcaption{Definitions of the operators} @@ -645,20 +645,20 @@ theory has the {\ML} identifier \ttindexbold{arith.thy}. All proofs are on the file \ttindexbold{CTT/arith.ML}. -The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'//' -and~\verb'/' stand for sum, difference, absolute difference, product, +The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod' +and~\verb'div' stand for sum, difference, absolute difference, product, remainder and quotient, respectively. Since Type Theory has only primitive recursion, some of their definitions may be obscure. The difference~$a-b$ is computed by taking $b$ predecessors of~$a$, where the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y.x)$. -The remainder $a//b$ counts up to~$a$ in a cyclic fashion, using 0 as the -successor of~$b-1$. Absolute difference is used to test the equality -$succ(v)=b$. +The remainder $a\bmod b$ counts up to~$a$ in a cyclic fashion, using 0 +as the successor of~$b-1$. Absolute difference is used to test the +equality $succ(v)=b$. -The quotient $a//b$ is computed by adding one for every number $x$ such -that $0\leq x \leq a$ and $x//b = 0$. +The quotient $a/b$ is computed by adding one for every number $x$ +such that $0\leq x \leq a$ and $x\bmod b = 0$. @@ -775,6 +775,11 @@ {\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))} +{\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]",} +{\out "p : SUM x:A. B(x) + C(x) [p : SUM x:A. B(x) + C(x)]"]} +{\out : thm list} \end{ttbox} One of the premises involves summation ($\Sigma$). Since it is a premise rather than the assumption of a goal, it cannot be found by @@ -901,6 +906,10 @@ {\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())} +{\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} +{\out [!!z. z : SUM x:A. B(x) ==> C(z) type]"] : thm list} \end{ttbox} This is an opportunity to demonstrate \ttindex{intr_tac}. Here, the tactic repeatedly applies $\Pi$-introduction, automatically proving the rather @@ -970,6 +979,12 @@ {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} {\out 1. ?a : (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 val prems = ["A type [A type]",} +{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",} +{\out "[| ?x : A; ?y : B(?x) |] ==> C(?x, ?y) type} +{\out [!!x y. [| x : A; y : B(x) |] ==> C(x, y) type]"]} +{\out : thm list} \end{ttbox} First, \ttindex{intr_tac} applies introduction rules and performs routine type checking. This instantiates~$\Var{a}$ to a construction involving diff -r a931f1b45151 -r 1b3cddf41b2d doc-src/Logics/FOL.tex --- a/doc-src/Logics/FOL.tex Thu Nov 11 12:44:43 1993 +0100 +++ b/doc-src/Logics/FOL.tex Thu Nov 11 13:18:49 1993 +0100 @@ -47,30 +47,30 @@ (see~\S\ref{fol-int-prover}). See the files \ttindexbold{FOL/ifol.thy}, \ttindexbold{FOL/ifol.ML} and -\ttindexbold{FOL/int-prover.ML} for complete listings of the rules and +\ttindexbold{FOL/intprover.ML} for complete listings of the rules and derived rules. \begin{figure} \begin{center} \begin{tabular}{rrr} - \it name &\it meta-type & \it description \\ - \idx{Trueprop}& $o\To prop$ & coercion to $prop$\\ - \idx{Not} & $o\To o$ & negation ($\neg$) \\ - \idx{True} & $o$ & tautology ($\top$) \\ - \idx{False} & $o$ & absurdity ($\bot$) + \it name &\it meta-type & \it description \\ + \idx{Trueprop}& $o\To prop$ & coercion to $prop$\\ + \idx{Not} & $o\To o$ & negation ($\neg$) \\ + \idx{True} & $o$ & tautology ($\top$) \\ + \idx{False} & $o$ & absurdity ($\bot$) \end{tabular} \end{center} \subcaption{Constants} \begin{center} \begin{tabular}{llrrr} - \it symbol &\it name &\it meta-type & \it precedence & \it description \\ + \it symbol &\it name &\it meta-type & \it precedence & \it description \\ \idx{ALL} & \idx{All} & $(\alpha\To o)\To o$ & 10 & - universal quantifier ($\forall$) \\ + universal quantifier ($\forall$) \\ \idx{EX} & \idx{Ex} & $(\alpha\To o)\To o$ & 10 & - existential quantifier ($\exists$) \\ + existential quantifier ($\exists$) \\ \idx{EX!} & \idx{Ex1} & $(\alpha\To o)\To o$ & 10 & - unique existence ($\exists!$) + unique existence ($\exists!$) \end{tabular} \end{center} \subcaption{Binders} @@ -82,12 +82,12 @@ \indexbold{*"-"-">} \indexbold{*"<"-">} \begin{tabular}{rrrr} - \it symbol & \it meta-type & \it precedence & \it description \\ - \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\ - \tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\ - \tt | & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\ - \tt --> & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\ - \tt <-> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$) + \it symbol & \it meta-type & \it precedence & \it description \\ + \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\ + \tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\ + \tt | & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\ + \tt --> & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\ + \tt <-> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$) \end{tabular} \end{center} \subcaption{Infixes} @@ -95,16 +95,16 @@ \dquotes \[\begin{array}{rcl} formula & = & \hbox{expression of type~$o$} \\ - & | & term " = " term \\ - & | & term " \ttilde= " term \\ - & | & "\ttilde\ " formula \\ - & | & formula " \& " formula \\ - & | & formula " | " formula \\ - & | & formula " --> " formula \\ - & | & formula " <-> " formula \\ - & | & "ALL~" id~id^* " . " formula \\ - & | & "EX~~" id~id^* " . " formula \\ - & | & "EX!~" id~id^* " . " formula + & | & term " = " term \\ + & | & term " \ttilde= " term \\ + & | & "\ttilde\ " formula \\ + & | & formula " \& " formula \\ + & | & formula " | " formula \\ + & | & formula " --> " formula \\ + & | & formula " <-> " formula \\ + & | & "ALL~" id~id^* " . " formula \\ + & | & "EX~~" id~id^* " . " formula \\ + & | & "EX!~" id~id^* " . " formula \end{array} \] \subcaption{Grammar} @@ -735,8 +735,8 @@ and~\ttindex{ifE}. They permit natural proofs of theorems such as the following: \begin{eqnarray*} - if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\ - if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B)) + if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\ + if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B)) \end{eqnarray*} Proofs also require the classical reasoning rules and the $\bimp$ introduction rule (called~\ttindex{iffI}: do not confuse with~\ttindex{ifI}). diff -r a931f1b45151 -r 1b3cddf41b2d doc-src/Logics/LK.tex --- a/doc-src/Logics/LK.tex Thu Nov 11 12:44:43 1993 +0100 +++ b/doc-src/Logics/LK.tex Thu Nov 11 13:18:49 1993 +0100 @@ -40,7 +40,7 @@ This technique lets Isabelle formalize sequent calculus rules, where the comma is the associative operator: \[ \infer[\conj\hbox{-left}] - {\Gamma,P\conj Q,\Delta \turn \Theta} + {\Gamma,P\conj Q,\Delta \turn \Theta} {\Gamma,P,Q,\Delta \turn \Theta} \] Multiple unifiers occur whenever this is resolved against a goal containing more than one conjunction on the left. Explicit formalization of sequents @@ -56,25 +56,25 @@ \begin{figure} \begin{center} \begin{tabular}{rrr} - \it name &\it meta-type & \it description \\ - \idx{Trueprop}& $o\To prop$ & coercion to $prop$ \\ - \idx{Seqof} & $[o,sobj]\To sobj$ & singleton sequence \\ - \idx{Not} & $o\To o$ & negation ($\neg$) \\ - \idx{True} & $o$ & tautology ($\top$) \\ - \idx{False} & $o$ & absurdity ($\bot$) + \it name &\it meta-type & \it description \\ + \idx{Trueprop}& $o\To prop$ & coercion to $prop$ \\ + \idx{Seqof} & $[o,sobj]\To sobj$ & singleton sequence \\ + \idx{Not} & $o\To o$ & negation ($\neg$) \\ + \idx{True} & $o$ & tautology ($\top$) \\ + \idx{False} & $o$ & absurdity ($\bot$) \end{tabular} \end{center} \subcaption{Constants} \begin{center} \begin{tabular}{llrrr} - \it symbol &\it name &\it meta-type & \it precedence & \it description \\ + \it symbol &\it name &\it meta-type & \it precedence & \it description \\ \idx{ALL} & \idx{All} & $(\alpha\To o)\To o$ & 10 & - universal quantifier ($\forall$) \\ + universal quantifier ($\forall$) \\ \idx{EX} & \idx{Ex} & $(\alpha\To o)\To o$ & 10 & - existential quantifier ($\exists$) \\ + existential quantifier ($\exists$) \\ \idx{THE} & \idx{The} & $(\alpha\To o)\To \alpha$ & 10 & - definite description ($\iota$) + definite description ($\iota$) \end{tabular} \end{center} \subcaption{Binders} @@ -98,7 +98,7 @@ \begin{center} \begin{tabular}{rrr} - \it external & \it internal & \it description \\ + \it external & \it internal & \it description \\ \tt $\Gamma$ |- $\Delta$ & \tt Trueprop($\Gamma$, $\Delta$) & sequent $\Gamma\turn \Delta$ \end{tabular} @@ -121,15 +121,15 @@ & | & formula \\[2ex] formula & = & \hbox{expression of type~$o$} \\ - & | & term " = " term \\ - & | & "\ttilde\ " formula \\ - & | & formula " \& " formula \\ - & | & formula " | " formula \\ - & | & formula " --> " formula \\ - & | & formula " <-> " formula \\ - & | & "ALL~" id~id^* " . " formula \\ - & | & "EX~~" id~id^* " . " formula \\ - & | & "THE~" id~ " . " formula + & | & term " = " term \\ + & | & "\ttilde\ " formula \\ + & | & formula " \& " formula \\ + & | & formula " | " formula \\ + & | & formula " --> " formula \\ + & | & formula " <-> " formula \\ + & | & "ALL~" id~id^* " . " formula \\ + & | & "EX~~" id~id^* " . " formula \\ + & | & "THE~" id~ " . " formula \end{array} \] \caption{Grammar of {\tt LK}} \label{lk-grammar} @@ -166,8 +166,13 @@ \idx{notL} $H, $G |- $E, P ==> $H, ~P, $G |- $E \idx{FalseL} $H, False, $G |- $E +\end{ttbox} \subcaption{Propositional rules} +\caption{Rules of {\tt LK}} \label{lk-rules} +\end{figure} +\begin{figure} +\begin{ttbox} \idx{allR} (!!x.$H|- $E, P(x), $F) ==> $H|- $E, ALL x.P(x), $F \idx{allL} $H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G|- $E @@ -176,10 +181,10 @@ \idx{The} [| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> $H |- $E, P(THE x.P(x)), $F +\end{ttbox} \subcaption{Quantifier rules} -\end{ttbox} -\caption{Rules of {\tt LK}} \label{lk-rules} +\caption{Rules of {\tt LK} (continued)} \label{lk-rules2} \end{figure} @@ -223,13 +228,13 @@ as a formula. The theory has the \ML\ identifier \ttindexbold{LK.thy}. -Figure~\ref{lk-rules} presents the rules. The connective $\bimp$ is -defined using $\conj$ and $\imp$. The axiom for basic sequents is -expressed in a form that provides automatic thinning: redundant formulae -are simply ignored. The other rules are expressed in the form most -suitable for backward proof --- they do not require exchange or contraction -rules. The contraction rules are actually derivable (via cut) in this -formulation. +Figures~\ref{lk-rules} and~\ref{lk-rules2} present the rules. The +connective $\bimp$ is defined using $\conj$ and $\imp$. The axiom for +basic sequents is expressed in a form that provides automatic thinning: +redundant formulae are simply ignored. The other rules are expressed in +the form most suitable for backward proof --- they do not require exchange +or contraction rules. The contraction rules are actually derivable (via +cut) in this formulation. Figure~\ref{lk-derived} presents derived rules, including rules for $\bimp$. The weakened quantifier rules discard each quantification after a diff -r a931f1b45151 -r 1b3cddf41b2d doc-src/Logics/Old_HOL.tex --- a/doc-src/Logics/Old_HOL.tex Thu Nov 11 12:44:43 1993 +0100 +++ b/doc-src/Logics/Old_HOL.tex Thu Nov 11 13:18:49 1993 +0100 @@ -1,7 +1,7 @@ %% $Id$ \chapter{Higher-order logic} The directory~\ttindexbold{HOL} contains a theory for higher-order logic -based on Gordon's~{\sc hol} system~\cite{gordon88a}, which itself is based on +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 @@ -31,13 +31,13 @@ \begin{figure} \begin{center} \begin{tabular}{rrr} - \it name &\it meta-type & \it description \\ - \idx{Trueprop}& $bool\To prop$ & coercion to $prop$\\ - \idx{not} & $bool\To bool$ & negation ($\neg$) \\ - \idx{True} & $bool$ & tautology ($\top$) \\ - \idx{False} & $bool$ & absurdity ($\bot$) \\ - \idx{if} & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\ - \idx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion + \it name &\it meta-type & \it description \\ + \idx{Trueprop}& $bool\To prop$ & coercion to $prop$\\ + \idx{not} & $bool\To bool$ & negation ($\neg$) \\ + \idx{True} & $bool$ & tautology ($\top$) \\ + \idx{False} & $bool$ & absurdity ($\bot$) \\ + \idx{if} & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\ + \idx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion \end{tabular} \end{center} \subcaption{Constants} @@ -45,28 +45,28 @@ \index{"@@{\tt\at}} \begin{center} \begin{tabular}{llrrr} - \it symbol &\it name &\it meta-type & \it prec & \it description \\ + \it symbol &\it name &\it meta-type & \it prec & \it description \\ \tt\at & \idx{Eps} & $(\alpha\To bool)\To\alpha::term$ & 10 & - Hilbert description ($\epsilon$) \\ + Hilbert description ($\epsilon$) \\ \idx{!} & \idx{All} & $(\alpha::term\To bool)\To bool$ & 10 & - universal quantifier ($\forall$) \\ + universal quantifier ($\forall$) \\ \idx{?} & \idx{Ex} & $(\alpha::term\To bool)\To bool$ & 10 & - existential quantifier ($\exists$) \\ + existential quantifier ($\exists$) \\ \idx{?!} & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 & - unique existence ($\exists!$) + unique existence ($\exists!$) \end{tabular} \end{center} \subcaption{Binders} \begin{center} \begin{tabular}{llrrr} - \it symbol &\it name &\it meta-type & \it prec & \it description \\ + \it symbol &\it name &\it meta-type & \it prec & \it description \\ \idx{ALL} & \idx{All} & $(\alpha::term\To bool)\To bool$ & 10 & - universal quantifier ($\forall$) \\ + universal quantifier ($\forall$) \\ \idx{EX} & \idx{Ex} & $(\alpha::term\To bool)\To bool$ & 10 & - existential quantifier ($\exists$) \\ + existential quantifier ($\exists$) \\ \idx{EX!} & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 & - unique existence ($\exists!$) + unique existence ($\exists!$) \end{tabular} \end{center} \subcaption{Alternative quantifiers} @@ -77,16 +77,16 @@ \indexbold{*"|} \indexbold{*"-"-">} \begin{tabular}{rrrr} - \it symbol & \it meta-type & \it precedence & \it description \\ - \idx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & - Right 50 & composition ($\circ$) \\ - \tt = & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\ - \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\ - \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\ - \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) \\ - \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\ - \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 & - less than or equals ($\leq$) + \it symbol & \it meta-type & \it precedence & \it description \\ + \idx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & + Right 50 & composition ($\circ$) \\ + \tt = & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\ + \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\ + \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\ + \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) \\ + \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\ + \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 & + less than or equals ($\leq$) \end{tabular} \end{center} \subcaption{Infixes} @@ -98,22 +98,22 @@ \dquotes \[\begin{array}{rcl} term & = & \hbox{expression of class~$term$} \\ - & | & "\at~~" id~id^* " . " formula \\[2ex] + & | & "\at~~" id~id^* " . " formula \\[2ex] formula & = & \hbox{expression of type~$bool$} \\ - & | & term " = " term \\ - & | & term " \ttilde= " term \\ - & | & term " < " term \\ - & | & term " <= " term \\ - & | & "\ttilde\ " formula \\ - & | & formula " \& " formula \\ - & | & formula " | " formula \\ - & | & formula " --> " formula \\ - & | & "!~~~" id~id^* " . " formula \\ - & | & "?~~~" id~id^* " . " formula \\ - & | & "?!~~" id~id^* " . " formula \\ - & | & "ALL~" id~id^* " . " formula \\ - & | & "EX~~" id~id^* " . " formula \\ - & | & "EX!~" id~id^* " . " formula + & | & term " = " term \\ + & | & term " \ttilde= " term \\ + & | & term " < " term \\ + & | & term " <= " term \\ + & | & "\ttilde\ " formula \\ + & | & formula " \& " formula \\ + & | & formula " | " formula \\ + & | & formula " --> " formula \\ + & | & "!~~~" id~id^* " . " formula \\ + & | & "?~~~" id~id^* " . " formula \\ + & | & "?!~~" id~id^* " . " formula \\ + & | & "ALL~" id~id^* " . " formula \\ + & | & "EX~~" id~id^* " . " formula \\ + & | & "EX!~" id~id^* " . " formula \end{array} \] \subcaption{Grammar} @@ -401,44 +401,44 @@ \begin{figure} \begin{center} \begin{tabular}{rrr} - \it name &\it meta-type & \it description \\ + \it name &\it meta-type & \it description \\ \index{"{"}@{\tt\{\}}} - {\tt\{\}} & $\alpha\,set$ & the empty set \\ - \idx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$ - & insertion of element \\ - \idx{Collect} & $(\alpha\To bool)\To\alpha\,set$ - & comprehension \\ - \idx{Compl} & $(\alpha\,set)\To\alpha\,set$ - & complement \\ + {\tt\{\}} & $\alpha\,set$ & the empty set \\ + \idx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$ + & insertion of element \\ + \idx{Collect} & $(\alpha\To bool)\To\alpha\,set$ + & comprehension \\ + \idx{Compl} & $(\alpha\,set)\To\alpha\,set$ + & complement \\ \idx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ - & intersection over a set\\ + & intersection over a set\\ \idx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ - & union over a set\\ + & union over a set\\ \idx{Inter} & $((\alpha\,set)set)\To\alpha\,set$ - &set of sets intersection \\ + &set of sets intersection \\ \idx{Union} & $((\alpha\,set)set)\To\alpha\,set$ - &set of sets union \\ - \idx{range} & $(\alpha\To\beta )\To\beta\,set$ - & range of a function \\[1ex] - \idx{Ball}~~\idx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$ - & bounded quantifiers \\ - \idx{mono} & $(\alpha\,set\To\beta\,set)\To bool$ - & monotonicity \\ + &set of sets union \\ + \idx{range} & $(\alpha\To\beta )\To\beta\,set$ + & range of a function \\[1ex] + \idx{Ball}~~\idx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$ + & bounded quantifiers \\ + \idx{mono} & $(\alpha\,set\To\beta\,set)\To bool$ + & monotonicity \\ \idx{inj}~~\idx{surj}& $(\alpha\To\beta )\To bool$ - & injective/surjective \\ - \idx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$ - & injective over subset + & injective/surjective \\ + \idx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$ + & injective over subset \end{tabular} \end{center} \subcaption{Constants} \begin{center} \begin{tabular}{llrrr} - \it symbol &\it name &\it meta-type & \it prec & \it description \\ + \it symbol &\it name &\it meta-type & \it prec & \it description \\ \idx{INT} & \idx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & - intersection over a type\\ + intersection over a type\\ \idx{UN} & \idx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & - union over a type + union over a type \end{tabular} \end{center} \subcaption{Binders} @@ -448,17 +448,17 @@ \indexbold{*":} \indexbold{*"<"=} \begin{tabular}{rrrr} - \it symbol & \it meta-type & \it precedence & \it description \\ - \tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$ - & Left 90 & image \\ - \idx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ - & Left 70 & intersection ($\inter$) \\ - \idx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ - & Left 65 & union ($\union$) \\ - \tt: & $[\alpha ,\alpha\,set]\To bool$ - & Left 50 & membership ($\in$) \\ - \tt <= & $[\alpha\,set,\alpha\,set]\To bool$ - & Left 50 & subset ($\subseteq$) + \it symbol & \it meta-type & \it precedence & \it description \\ + \tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$ + & Left 90 & image \\ + \idx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ + & Left 70 & intersection ($\inter$) \\ + \idx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ + & Left 65 & union ($\union$) \\ + \tt: & $[\alpha ,\alpha\,set]\To bool$ + & Left 50 & membership ($\in$) \\ + \tt <= & $[\alpha\,set,\alpha\,set]\To bool$ + & Left 50 & subset ($\subseteq$) \end{tabular} \end{center} \subcaption{Infixes} @@ -469,24 +469,24 @@ \begin{figure} \begin{center} \tt\frenchspacing \begin{tabular}{rrr} - \it external & \it internal & \it description \\ + \it external & \it internal & \it description \\ $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\ \{$a@1$, $\ldots$, $a@n$\} & insert($a@1$,$\cdots$,insert($a@n$,0)) & \rm finite set \\ - \{$x$.$P[x]$\} & Collect($\lambda x.P[x]$) & + \{$x$.$P[x]$\} & Collect($\lambda x.P[x]$) & \rm comprehension \\ - \idx{INT} $x$:$A$.$B[x]$ & INTER($A$,$\lambda x.B[x]$) & - \rm intersection over a set \\ - \idx{UN} $x$:$A$.$B[x]$ & UNION($A$,$\lambda x.B[x]$) & - \rm union over a set \\ - \idx{!} $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) & - \rm bounded $\forall$ \\ - \idx{?} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) & - \rm bounded $\exists$ \\[1ex] - \idx{ALL} $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) & - \rm bounded $\forall$ \\ - \idx{EX} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) & - \rm bounded $\exists$ + \idx{INT} $x$:$A$.$B[x]$ & INTER($A$,$\lambda x.B[x]$) & + \rm intersection over a set \\ + \idx{UN} $x$:$A$.$B[x]$ & UNION($A$,$\lambda x.B[x]$) & + \rm union over a set \\ + \idx{!} $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) & + \rm bounded $\forall$ \\ + \idx{?} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) & + \rm bounded $\exists$ \\[1ex] + \idx{ALL} $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) & + \rm bounded $\forall$ \\ + \idx{EX} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) & + \rm bounded $\exists$ \end{tabular} \end{center} \subcaption{Translations} @@ -494,24 +494,24 @@ \dquotes \[\begin{array}{rcl} term & = & \hbox{other terms\ldots} \\ - & | & "\{\}" \\ - & | & "\{ " term\; ("," term)^* " \}" \\ - & | & "\{ " id " . " formula " \}" \\ - & | & term " `` " term \\ - & | & term " Int " term \\ - & | & term " Un " term \\ - & | & "INT~~" id ":" term " . " term \\ - & | & "UN~~~" id ":" term " . " term \\ - & | & "INT~~" id~id^* " . " term \\ - & | & "UN~~~" id~id^* " . " term \\[2ex] + & | & "\{\}" \\ + & | & "\{ " term\; ("," term)^* " \}" \\ + & | & "\{ " id " . " formula " \}" \\ + & | & term " `` " term \\ + & | & term " Int " term \\ + & | & term " Un " term \\ + & | & "INT~~" id ":" term " . " term \\ + & | & "UN~~~" id ":" term " . " term \\ + & | & "INT~~" id~id^* " . " term \\ + & | & "UN~~~" id~id^* " . " term \\[2ex] formula & = & \hbox{other formulae\ldots} \\ - & | & term " : " term \\ - & | & term " \ttilde: " term \\ - & | & term " <= " term \\ - & | & "!~~~" id ":" term " . " formula \\ - & | & "?~~~" id ":" term " . " formula \\ - & | & "ALL " id ":" term " . " formula \\ - & | & "EX~~" id ":" term " . " formula + & | & term " : " term \\ + & | & term " \ttilde: " term \\ + & | & term " <= " term \\ + & | & "!~~~" id ":" term " . " formula \\ + & | & "?~~~" id ":" term " . " formula \\ + & | & "ALL " id ":" term " . " formula \\ + & | & "EX~~" id ":" term " . " formula \end{array} \] \subcaption{Full Grammar} @@ -828,13 +828,13 @@ \begin{figure} \makeatother \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{snd} & $\alpha\times\beta \To \beta$ & second projection\\ - \idx{split} & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$ - & generalized projection + \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{snd} & $\alpha\times\beta \To \beta$ & second projection\\ + \idx{split} & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$ + & generalized projection \end{tabular} \end{center} \subcaption{Constants} @@ -862,11 +862,11 @@ \begin{figure} \makeatother \begin{center} \begin{tabular}{rrr} - \it name &\it meta-type & \it description \\ - \idx{Inl} & $\alpha \To \alpha+\beta$ & first injection\\ - \idx{Inr} & $\beta \To \alpha+\beta$ & second injection\\ - \idx{case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$ - & conditional + \it name &\it meta-type & \it description \\ + \idx{Inl} & $\alpha \To \alpha+\beta$ & first injection\\ + \idx{Inr} & $\beta \To \alpha+\beta$ & second injection\\ + \idx{case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$ + & conditional \end{tabular} \end{center} \subcaption{Constants} @@ -916,13 +916,13 @@ \indexbold{*"<} \begin{center} \begin{tabular}{rrr} - \it symbol & \it meta-type & \it description \\ - \idx{0} & $nat$ & zero \\ - \idx{Suc} & $nat \To nat$ & successor function\\ + \it symbol & \it meta-type & \it description \\ + \idx{0} & $nat$ & zero \\ + \idx{Suc} & $nat \To nat$ & successor function\\ \idx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$ - & conditional\\ + & conditional\\ \idx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$ - & primitive recursor\\ + & primitive recursor\\ \idx{pred_nat} & $(nat\times nat) set$ & predecessor relation \end{tabular} \end{center} @@ -935,12 +935,12 @@ \index{+@{\tt+}|bold} \index{-@{\tt-}|bold} \begin{tabular}{rrrr} - \it symbol & \it meta-type & \it precedence & \it description \\ - \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\ - \tt / & $[nat,nat]\To nat$ & Left 70 & division\\ - \tt // & $[nat,nat]\To nat$ & Left 70 & modulus\\ - \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\ - \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction + \it symbol & \it meta-type & \it precedence & \it description \\ + \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\ + \tt / & $[nat,nat]\To nat$ & Left 70 & division\\ + \tt // & $[nat,nat]\To nat$ & Left 70 & modulus\\ + \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\ + \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction \end{tabular} \end{center} \subcaption{Constants and infixes} @@ -1040,15 +1040,15 @@ \begin{figure} \makeatother \begin{center} \begin{tabular}{rrr} - \it symbol & \it meta-type & \it description \\ - \idx{Nil} & $\alpha list$ & the empty list\\ - \idx{Cons} & $[\alpha, \alpha list] \To \alpha list$ - & list constructor\\ - \idx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list, + \it symbol & \it meta-type & \it description \\ + \idx{Nil} & $\alpha list$ & the empty list\\ + \idx{Cons} & $[\alpha, \alpha list] \To \alpha list$ + & list constructor\\ + \idx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list, \beta]\To\beta] \To \beta$ - & list recursor\\ - \idx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$ - & mapping functional + & list recursor\\ + \idx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$ + & mapping functional \end{tabular} \end{center} \subcaption{Constants} @@ -1141,35 +1141,44 @@ methods. -\section{The examples directory} -This directory contains examples and experimental proofs in {\HOL}. Here -is an overview of the more interesting files. +\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 +theory~\cite{mw81}. + +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}] 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/meson-test.ML}] +\item[\ttindexbold{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[\ttindexbold{HOL/ex/prop-log.ML}] +\item[\ttindexbold{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}] -is an experimental recursive type definition, where the recursion goes -through the type constructor~$list$. +\item[\ttindexbold{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}] 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}] +contains Jacob Frost's formalization~\cite{frost93} of a co-induction +example by Milner and Tofte~\cite{milner-coind}. \end{description} @@ -1193,6 +1202,7 @@ {\out Level 0} {\out P & Q} {\out 1. P & Q} +{\out val prems = ["P [P]", "Q [Q]"] : thm list} \end{ttbox} The next step is to unfold the definition of conjunction. But \ttindex{and_def} uses {\HOL}'s internal equality, so @@ -1244,6 +1254,7 @@ {\out Level 0} {\out P} {\out 1. P} +{\out val prems = ["P & Q [P & Q]"] : thm list} \end{ttbox} Working with premises that involve defined constants can be tricky. We must expand the definition of conjunction in the meta-assumption $P\conj @@ -1255,7 +1266,11 @@ {\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: +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} \begin{ttbox} prems RL [and_def RS subst] RL [spec] RL [mp]; diff -r a931f1b45151 -r 1b3cddf41b2d doc-src/Logics/ZF.tex --- a/doc-src/Logics/ZF.tex Thu Nov 11 12:44:43 1993 +0100 +++ b/doc-src/Logics/ZF.tex Thu Nov 11 13:18:49 1993 +0100 @@ -16,7 +16,7 @@ recursion equations over monotonic functors; these have been applied to yield constructions of lists and trees. Thus, we may even regard set theory as a computational logic. It admits recursive definitions of -functions and types. It has similarities with Martin-L\"of type theory, +functions and types. It has much in common with Martin-L\"of type theory, although of course it is classical. Because {\ZF} is an extension of {\FOL}, it provides the same packages, @@ -26,6 +26,17 @@ \ttindexbold{upair_cs} and~\ttindexbold{ZF_cs}. See the files on directory {\tt ZF} for details. +Isabelle/ZF now has a flexible package for handling inductive definitions, +such as inference systems, and datatype definitions, such as lists and +trees. Moreover it also handles co-inductive definitions, such as +bisimulation relations, and co-datatype definitions, such as streams. A +recent paper describes the package~\cite{paulson-fixedpt}. + +Recent reports describe Isabelle/ZF less formally than this +chapter~\cite{paulson-set-I,paulson-set-II}. Isabelle/ZF employs a novel +treatment of non-well-founded data structures within the standard ZF axioms +including the Axiom of Foundation, but no report describes this treatment. + \section{Which version of axiomatic set theory?} Resolution theorem provers can work in set theory, using the @@ -53,31 +64,31 @@ \begin{figure} \begin{center} \begin{tabular}{rrr} - \it name &\it meta-type & \it description \\ - \idx{0} & $i$ & empty set\\ - \idx{cons} & $[i,i]\To i$ & finite set constructor\\ - \idx{Upair} & $[i,i]\To i$ & unordered pairing\\ - \idx{Pair} & $[i,i]\To i$ & ordered pairing\\ - \idx{Inf} & $i$ & infinite set\\ - \idx{Pow} & $i\To i$ & powerset\\ - \idx{Union} \idx{Inter} & $i\To i$ & set union/intersection \\ - \idx{split} & $[i, [i,i]\To i] \To i$ & generalized projection\\ - \idx{fst} \idx{snd} & $i\To i$ & projections\\ - \idx{converse}& $i\To i$ & converse of a relation\\ - \idx{succ} & $i\To i$ & successor\\ - \idx{Collect} & $[i,i\To o]\To i$ & separation\\ - \idx{Replace} & $[i, [i,i]\To o] \To i$ & replacement\\ - \idx{PrimReplace} & $[i, [i,i]\To o] \To i$ & primitive replacement\\ - \idx{RepFun} & $[i, i\To i] \To i$ & functional replacement\\ - \idx{Pi} \idx{Sigma} & $[i,i\To i]\To i$ & general product/sum\\ - \idx{domain} & $i\To i$ & domain of a relation\\ - \idx{range} & $i\To i$ & range of a relation\\ - \idx{field} & $i\To i$ & field of a relation\\ - \idx{Lambda} & $[i, i\To i]\To i$ & $\lambda$-abstraction\\ - \idx{restrict}& $[i, i] \To i$ & restriction of a function\\ - \idx{The} & $[i\To o]\To i$ & definite description\\ - \idx{if} & $[o,i,i]\To i$ & conditional\\ - \idx{Ball} \idx{Bex} & $[i, i\To o]\To o$ & bounded quantifiers + \it name &\it meta-type & \it description \\ + \idx{0} & $i$ & empty set\\ + \idx{cons} & $[i,i]\To i$ & finite set constructor\\ + \idx{Upair} & $[i,i]\To i$ & unordered pairing\\ + \idx{Pair} & $[i,i]\To i$ & ordered pairing\\ + \idx{Inf} & $i$ & infinite set\\ + \idx{Pow} & $i\To i$ & powerset\\ + \idx{Union} \idx{Inter} & $i\To i$ & set union/intersection \\ + \idx{split} & $[[i,i]\To i, i] \To i$ & generalized projection\\ + \idx{fst} \idx{snd} & $i\To i$ & projections\\ + \idx{converse}& $i\To i$ & converse of a relation\\ + \idx{succ} & $i\To i$ & successor\\ + \idx{Collect} & $[i,i\To o]\To i$ & separation\\ + \idx{Replace} & $[i, [i,i]\To o] \To i$ & replacement\\ + \idx{PrimReplace} & $[i, [i,i]\To o] \To i$ & primitive replacement\\ + \idx{RepFun} & $[i, i\To i] \To i$ & functional replacement\\ + \idx{Pi} \idx{Sigma} & $[i,i\To i]\To i$ & general product/sum\\ + \idx{domain} & $i\To i$ & domain of a relation\\ + \idx{range} & $i\To i$ & range of a relation\\ + \idx{field} & $i\To i$ & field of a relation\\ + \idx{Lambda} & $[i, i\To i]\To i$ & $\lambda$-abstraction\\ + \idx{restrict}& $[i, i] \To i$ & restriction of a function\\ + \idx{The} & $[i\To o]\To i$ & definite description\\ + \idx{if} & $[o,i,i]\To i$ & conditional\\ + \idx{Ball} \idx{Bex} & $[i, i\To o]\To o$ & bounded quantifiers \end{tabular} \end{center} \subcaption{Constants} @@ -91,14 +102,14 @@ \indexbold{*"<"=} \begin{tabular}{rrrr} \it symbol & \it meta-type & \it precedence & \it description \\ - \tt `` & $[i,i]\To i$ & Left 90 & image \\ - \tt -`` & $[i,i]\To i$ & Left 90 & inverse image \\ - \tt ` & $[i,i]\To i$ & Left 90 & application \\ - \idx{Int} & $[i,i]\To i$ & Left 70 & intersection ($\inter$) \\ - \idx{Un} & $[i,i]\To i$ & Left 65 & union ($\union$) \\ - \tt - & $[i,i]\To i$ & Left 65 & set difference ($-$) \\[1ex] - \tt: & $[i,i]\To o$ & Left 50 & membership ($\in$) \\ - \tt <= & $[i,i]\To o$ & Left 50 & subset ($\subseteq$) + \tt `` & $[i,i]\To i$ & Left 90 & image \\ + \tt -`` & $[i,i]\To i$ & Left 90 & inverse image \\ + \tt ` & $[i,i]\To i$ & Left 90 & application \\ + \idx{Int} & $[i,i]\To i$ & Left 70 & intersection ($\inter$) \\ + \idx{Un} & $[i,i]\To i$ & Left 65 & union ($\union$) \\ + \tt - & $[i,i]\To i$ & Left 65 & set difference ($-$) \\[1ex] + \tt: & $[i,i]\To o$ & Left 50 & membership ($\in$) \\ + \tt <= & $[i,i]\To o$ & Left 50 & subset ($\subseteq$) \end{tabular} \end{center} \subcaption{Infixes} @@ -139,8 +150,8 @@ binary union. The Isabelle version goes on to define the constant \ttindexbold{cons}: \begin{eqnarray*} - A\cup B & \equiv & \bigcup({\tt Upair}(A,B)) \\ - {\tt cons}(a,B) & \equiv & {\tt Upair}(a,a) \union B + A\cup B & \equiv & \bigcup({\tt Upair}(A,B)) \\ + {\tt cons}(a,B) & \equiv & {\tt Upair}(a,a) \union B \end{eqnarray*} The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the obvious manner using~{\tt cons} and~$\emptyset$ (the empty set): @@ -150,7 +161,9 @@ 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$>}. +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)}. 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 @@ -164,38 +177,39 @@ \indexbold{*"*} \begin{center} \tt\frenchspacing \begin{tabular}{rrr} - \it external & \it internal & \it description \\ + \it external & \it internal & \it description \\ $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\ \{$a@1$, $\ldots$, $a@n$\} & cons($a@1$,$\cdots$,cons($a@n$,0)) & \rm finite set \\ - <$a$, $b$> & Pair($a$,$b$) & \rm ordered pair \\ - <$a$, $b$, $c$> & <$a$, <$b$, $c$>> & \rm nested pairs (any depth) \\ - \{$x$:$A . P[x]$\} & Collect($A$,$\lambda x.P[x]$) & + <$a@1$, $\ldots$, $a@{n-1}$, $a@n$> & + Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) & + \rm ordered $n$-tuple \\ + \{$x$:$A . P[x]$\} & Collect($A$,$\lambda x.P[x]$) & \rm separation \\ \{$y . x$:$A$, $Q[x,y]$\} & Replace($A$,$\lambda x\,y.Q[x,y]$) & \rm replacement \\ \{$b[x] . x$:$A$\} & RepFun($A$,$\lambda x.b[x]$) & \rm functional replacement \\ - \idx{INT} $x$:$A . B[x]$ & Inter(\{$B[x] . x$:$A$\}) & - \rm general intersection \\ - \idx{UN} $x$:$A . B[x]$ & Union(\{$B[x] . x$:$A$\}) & - \rm general union \\ - \idx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x.B[x]$) & - \rm general product \\ - \idx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x.B[x]$) & - \rm general sum \\ - $A$ -> $B$ & Pi($A$,$\lambda x.B$) & - \rm function space \\ - $A$ * $B$ & Sigma($A$,$\lambda x.B$) & - \rm binary product \\ - \idx{THE} $x . P[x]$ & The($\lambda x.P[x]$) & - \rm definite description \\ - \idx{lam} $x$:$A . b[x]$ & Lambda($A$,$\lambda x.b[x]$) & - \rm $\lambda$-abstraction\\[1ex] - \idx{ALL} $x$:$A . P[x]$ & Ball($A$,$\lambda x.P[x]$) & - \rm bounded $\forall$ \\ - \idx{EX} $x$:$A . P[x]$ & Bex($A$,$\lambda x.P[x]$) & - \rm bounded $\exists$ + \idx{INT} $x$:$A . B[x]$ & Inter(\{$B[x] . x$:$A$\}) & + \rm general intersection \\ + \idx{UN} $x$:$A . B[x]$ & Union(\{$B[x] . x$:$A$\}) & + \rm general union \\ + \idx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x.B[x]$) & + \rm general product \\ + \idx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x.B[x]$) & + \rm general sum \\ + $A$ -> $B$ & Pi($A$,$\lambda x.B$) & + \rm function space \\ + $A$ * $B$ & Sigma($A$,$\lambda x.B$) & + \rm binary product \\ + \idx{THE} $x . P[x]$ & The($\lambda x.P[x]$) & + \rm definite description \\ + \idx{lam} $x$:$A . b[x]$ & Lambda($A$,$\lambda x.b[x]$) & + \rm $\lambda$-abstraction\\[1ex] + \idx{ALL} $x$:$A . P[x]$ & Ball($A$,$\lambda x.P[x]$) & + \rm bounded $\forall$ \\ + \idx{EX} $x$:$A . P[x]$ & Bex($A$,$\lambda x.P[x]$) & + \rm bounded $\exists$ \end{tabular} \end{center} \caption{Translations for {\ZF}} \label{ZF-trans} @@ -206,39 +220,39 @@ \dquotes \[\begin{array}{rcl} term & = & \hbox{expression of type~$i$} \\ - & | & "\{ " term\; ("," term)^* " \}" \\ - & | & "< " term ", " term " >" \\ - & | & "\{ " id ":" term " . " formula " \}" \\ - & | & "\{ " id " . " id ":" term "," formula " \}" \\ - & | & "\{ " term " . " id ":" term " \}" \\ - & | & term " `` " term \\ - & | & term " -`` " term \\ - & | & term " ` " term \\ - & | & term " * " term \\ - & | & term " Int " term \\ - & | & term " Un " term \\ - & | & term " - " term \\ - & | & term " -> " term \\ - & | & "THE~~" id " . " formula\\ - & | & "lam~~" id ":" term " . " term \\ - & | & "INT~~" id ":" term " . " term \\ - & | & "UN~~~" id ":" term " . " term \\ - & | & "PROD~" id ":" term " . " term \\ - & | & "SUM~~" id ":" term " . " term \\[2ex] + & | & "\{ " term\; ("," term)^* " \}" \\ + & | & "< " term ", " term " >" \\ + & | & "\{ " id ":" term " . " formula " \}" \\ + & | & "\{ " id " . " id ":" term "," formula " \}" \\ + & | & "\{ " term " . " id ":" term " \}" \\ + & | & term " `` " term \\ + & | & term " -`` " term \\ + & | & term " ` " term \\ + & | & term " * " term \\ + & | & term " Int " term \\ + & | & term " Un " term \\ + & | & term " - " term \\ + & | & term " -> " term \\ + & | & "THE~~" id " . " formula\\ + & | & "lam~~" id ":" term " . " term \\ + & | & "INT~~" id ":" term " . " term \\ + & | & "UN~~~" id ":" term " . " term \\ + & | & "PROD~" id ":" term " . " term \\ + & | & "SUM~~" id ":" term " . " term \\[2ex] formula & = & \hbox{expression of type~$o$} \\ - & | & term " : " term \\ - & | & term " <= " term \\ - & | & term " = " term \\ - & | & "\ttilde\ " formula \\ - & | & formula " \& " formula \\ - & | & formula " | " formula \\ - & | & formula " --> " formula \\ - & | & formula " <-> " formula \\ - & | & "ALL " id ":" term " . " formula \\ - & | & "EX~~" id ":" term " . " formula \\ - & | & "ALL~" id~id^* " . " formula \\ - & | & "EX~~" id~id^* " . " formula \\ - & | & "EX!~" id~id^* " . " formula + & | & term " : " term \\ + & | & term " <= " term \\ + & | & term " = " term \\ + & | & "\ttilde\ " formula \\ + & | & formula " \& " formula \\ + & | & formula " | " formula \\ + & | & formula " --> " formula \\ + & | & formula " <-> " formula \\ + & | & "ALL " id ":" term " . " formula \\ + & | & "EX~~" id ":" term " . " formula \\ + & | & "ALL~" id~id^* " . " formula \\ + & | & "EX~~" id~id^* " . " formula \\ + & | & "EX!~" id~id^* " . " formula \end{array} \] \caption{Full grammar for {\ZF}} \label{ZF-syntax} @@ -355,11 +369,6 @@ \idx{Int_def} A Int B == Inter(Upair(A,B)) \idx{Diff_def} A - B == \{ x:A . ~(x:B) \} \subcaption{Union, intersection, difference} - -\idx{cons_def} cons(a,A) == Upair(a,a) Un A -\idx{succ_def} succ(i) == cons(i,i) -\idx{infinity} 0:Inf & (ALL y:Inf. succ(y): Inf) -\subcaption{Finite and infinite sets} \end{ttbox} \caption{Rules and axioms of {\ZF}} \label{ZF-rules} \end{figure} @@ -367,10 +376,15 @@ \begin{figure} \begin{ttbox} +\idx{cons_def} cons(a,A) == Upair(a,a) Un A +\idx{succ_def} succ(i) == cons(i,i) +\idx{infinity} 0:Inf & (ALL y:Inf. succ(y): Inf) +\subcaption{Finite and infinite sets} + \idx{Pair_def} == \{\{a,a\}, \{a,b\}\} -\idx{split_def} split(p,c) == THE y. EX a b. p= & y=c(a,b) -\idx{fst_def} fst(A) == split(p, %x y.x) -\idx{snd_def} snd(A) == split(p, %x y.y) +\idx{split_def} split(c,p) == THE y. EX a b. p= & 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{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{\} \subcaption{Ordered pairs and Cartesian products} @@ -512,7 +526,7 @@ successor (\ttindexbold{succ}). Although this set is not uniquely defined, 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 defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$. Recall that \ttindexbold{Sigma}$(A,B)$ generalizes the Cartesian product of two @@ -525,7 +539,7 @@ often easier to use than \ttindex{fst} and~\ttindex{snd}. It is defined using a description for convenience, but could equivalently be defined by \begin{ttbox} -split(p,c) == c(fst(p),snd(p)) +split(c,p) == c(fst(p),snd(p)) \end{ttbox} Operations on relations include converse, domain, range, and image. The set ${\tt Pi}(A,B)$ generalizes the space of functions between two sets. @@ -717,7 +731,7 @@ \idx{fst} fst() = a \idx{snd} snd() = b -\idx{split} split(, %x y.c(x,y)) = c(a,b) +\idx{split} split(%x y.c(x,y), ) = c(a,b) \idx{SigmaI} [| a:A; b:B(a) |] ==> : Sigma(A,B) @@ -893,30 +907,30 @@ \begin{figure} \begin{center} \begin{tabular}{rrr} - \it name &\it meta-type & \it description \\ - \idx{id} & $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 - \\[1ex] - \idx{1} & $i$ & $\{\emptyset\}$ \\ - \idx{bool} & $i$ & the set $\{\emptyset,1\}$ \\ - \idx{cond} & $[i,i,i]\To i$ & conditional for {\tt bool} - \\[1ex] - \idx{Inl}~~\idx{Inr} & $i\To i$ & injections\\ - \idx{case} & $[i,i\To i,i\To i]\To i$ & conditional for $+$ - \\[1ex] - \idx{nat} & $i$ & set of natural numbers \\ - \idx{nat_case}& $[i,i,i\To i]\To i$ & conditional for $nat$\\ - \idx{rec} & $[i,i,[i,i]\To i]\To i$ & recursor for $nat$ - \\[1ex] - \idx{list} & $i\To i$ & lists over some set\\ - \idx{list_case} & $[i, i, [i,i]\To i] \To i$ & conditional for $list(A)$ \\ - \idx{list_rec} & $[i, i, [i,i,i]\To i] \To i$ & recursor for $list(A)$ \\ - \idx{map} & $[i\To i, i] \To i$ & mapping functional\\ - \idx{length} & $i\To i$ & length of a list\\ - \idx{rev} & $i\To i$ & reverse of a list\\ - \idx{flat} & $i\To i$ & flatting a list of lists\\ + \it name &\it meta-type & \it description \\ + \idx{id} & $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 + \\[1ex] + \idx{1} & $i$ & $\{\emptyset\}$ \\ + \idx{bool} & $i$ & the set $\{\emptyset,1\}$ \\ + \idx{cond} & $[i,i,i]\To i$ & conditional for {\tt bool} + \\[1ex] + \idx{Inl}~~\idx{Inr} & $i\To i$ & injections\\ + \idx{case} & $[i\To i,i\To i, i]\To i$ & conditional for $+$ + \\[1ex] + \idx{nat} & $i$ & set of natural numbers \\ + \idx{nat_case}& $[i,i\To i,i]\To i$ & conditional for $nat$\\ + \idx{rec} & $[i,i,[i,i]\To i]\To i$ & recursor for $nat$ + \\[1ex] + \idx{list} & $i\To i$ & lists over some set\\ + \idx{list_case} & $[i, [i,i]\To i, i] \To i$ & conditional for $list(A)$ \\ + \idx{list_rec} & $[i, i, [i,i,i]\To i] \To i$ & recursor for $list(A)$ \\ + \idx{map} & $[i\To i, i] \To i$ & mapping functional\\ + \idx{length} & $i\To i$ & length of a list\\ + \idx{rev} & $i\To i$ & reverse of a list\\ + \idx{flat} & $i\To i$ & flatting a list of lists\\ \end{tabular} \end{center} \subcaption{Constants} @@ -929,14 +943,14 @@ \index{#+@{\tt\#+}|bold} \index{#-@{\tt\#-}|bold} \begin{tabular}{rrrr} - \idx{O} & $[i,i]\To i$ & Right 60 & composition ($\circ$) \\ - \tt + & $[i,i]\To i$ & Right 65 & disjoint union \\ - \tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\ - \tt div & $[i,i]\To i$ & Left 70 & division\\ - \tt mod & $[i,i]\To i$ & Left 70 & modulus\\ - \tt \#+ & $[i,i]\To i$ & Left 65 & addition\\ - \tt \#- & $[i,i]\To i$ & Left 65 & subtraction\\ - \tt \@ & $[i,i]\To i$ & Right 60 & append for lists + \idx{O} & $[i,i]\To i$ & Right 60 & composition ($\circ$) \\ + \tt + & $[i,i]\To i$ & Right 65 & disjoint union \\ + \tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\ + \tt div & $[i,i]\To i$ & Left 70 & division\\ + \tt mod & $[i,i]\To i$ & Left 70 & modulus\\ + \tt \#+ & $[i,i]\To i$ & Left 65 & addition\\ + \tt \#- & $[i,i]\To i$ & Left 65 & subtraction\\ + \tt \@ & $[i,i]\To i$ & Right 60 & append for lists \end{tabular} \end{center} \subcaption{Infixes} @@ -987,6 +1001,55 @@ \caption{Equalities} \label{zf-equalities} \end{figure} + +\begin{figure} +\begin{ttbox} +\idx{bnd_mono_def} bnd_mono(D,h) == + h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X)) + +\idx{lfp_def} lfp(D,h) == Inter({X: Pow(D). h(X) <= X}) +\idx{gfp_def} gfp(D,h) == Union({X: Pow(D). X <= h(X)}) +\subcaption{Definitions} + +\idx{lfp_lowerbound} [| h(A) <= A; A<=D |] ==> lfp(D,h) <= A + +\idx{lfp_subset} lfp(D,h) <= D + +\idx{lfp_greatest} [| bnd_mono(D,h); + !!X. [| h(X) <= X; X<=D |] ==> A<=X + |] ==> A <= lfp(D,h) + +\idx{lfp_Tarski} bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h)) + +\idx{induct} [| a : lfp(D,h); bnd_mono(D,h); + !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) + |] ==> P(a) + +\idx{lfp_mono} [| bnd_mono(D,h); bnd_mono(E,i); + !!X. X<=D ==> h(X) <= i(X) + |] ==> lfp(D,h) <= lfp(E,i) + +\idx{gfp_upperbound} [| A <= h(A); A<=D |] ==> A <= gfp(D,h) + +\idx{gfp_subset} gfp(D,h) <= D + +\idx{gfp_least} [| bnd_mono(D,h); + !!X. [| X <= h(X); X<=D |] ==> X<=A + |] ==> gfp(D,h) <= A + +\idx{gfp_Tarski} bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h)) + +\idx{coinduct} [| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D + |] ==> a : gfp(D,h) + +\idx{gfp_mono} [| bnd_mono(D,h); D <= E; + !!X. X<=D ==> h(X) <= i(X) + |] ==> gfp(D,h) <= gfp(E,i) +\end{ttbox} +\caption{Least and greatest fixedpoints} \label{zf-fixedpt} +\end{figure} + + \begin{figure} \begin{ttbox} \idx{comp_def} r O s == \{xz : domain(s)*range(r) . @@ -1038,7 +1101,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(u,c,d) == split(u, %y z. cond(y, d(z), c(z))) +\idx{case_def} case(c,d,u) == split(%y z. cond(y, d(z), c(z)), u) \subcaption{Definitions} \idx{bool_1I} 1 : bool @@ -1057,27 +1120,44 @@ \idx{sumE2} u: A+B ==> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y)) -\idx{case_Inl} case(Inl(a),c,d) = c(a) -\idx{case_Inr} case(Inr(b),c,d) = d(b) +\idx{case_Inl} case(c,d,Inl(a)) = c(a) +\idx{case_Inr} case(c,d,Inr(b)) = d(b) \end{ttbox} \caption{Booleans and disjoint unions} \label{zf-sum} \end{figure} \begin{figure} \begin{ttbox} +\idx{QPair_def} == a+b +\idx{qsplit_def} qsplit(c,p) == THE y. EX a b. p= & y=c(a,b) +\idx{qfsplit_def} qfsplit(R,z) == EX x y. z= & R(x,y) +\idx{qconverse_def} qconverse(r) == {z. w:r, EX x y. w= & z=} +\idx{QSigma_def} QSigma(A,B) == UN x:A. UN y:B(x). {} + +\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))) +\end{ttbox} +\caption{Non-standard pairs, products and sums} \label{zf-qpair} +\end{figure} + + +\begin{figure} +\begin{ttbox} \idx{nat_def} nat == lfp(lam r: Pow(Inf). \{0\} Un \{succ(x). x:r\} -\idx{nat_case_def} nat_case(n,a,b) == - THE y. n=0 & y=a | (EX x. n=succ(x) & y=b(x)) +\idx{nat_case_def} nat_case(a,b,k) == + 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(n, a, %m. b(m, f`m))) + 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{quo_def} m div n == transrec(m, %j f. if(j:n, 0, succ(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 @@ -1087,8 +1167,8 @@ [| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |] ==> P(n) -\idx{nat_case_0} nat_case(0,a,b) = a -\idx{nat_case_succ} nat_case(succ(m),a,b) = b(m) +\idx{nat_case_0} nat_case(a,b,0) = a +\idx{nat_case_succ} nat_case(a,b,succ(m)) = b(m) \idx{rec_0} rec(0,a,b) = a \idx{rec_succ} rec(succ(m),a,b) = b(m, rec(m,a,b)) @@ -1108,15 +1188,30 @@ \caption{The natural numbers} \label{zf-nat} \end{figure} +\begin{figure} +\begin{ttbox} +\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_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) +\end{ttbox} +\caption{The finite set operator} \label{zf-fin} +\end{figure} + \begin{figure}\underscoreon %%because @ is used here \begin{ttbox} -\idx{list_def} list(A) == lfp(univ(A), %X. {0} Un A*X) - -\idx{list_case_def} list_case(l,c,h) == - THE z. l=0 & z=c | (EX x y. l = & z=h(x,y)) - \idx{list_rec_def} list_rec(l,c,h) == - Vrec(l, %l g.list_case(l, c, %x xs. h(x, xs, g`xs))) + 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. ) \idx{length_def} length(l) == list_rec(l, 0, %x xs r. succ(r)) @@ -1125,20 +1220,22 @@ \idx{flat_def} flat(ls) == list_rec(ls, 0, %l ls r. l @ r) \subcaption{Definitions} -\idx{list_0I} 0 : list(A) -\idx{list_PairI} [| a: A; l: list(A) |] ==> : list(A) +\idx{NilI} Nil : list(A) +\idx{ConsI} [| a: A; l: list(A) |] ==> Cons(a,l) : list(A) -\idx{list_induct} +\idx{List.induct} [| l: list(A); - P(0); - !!x y. [| x: A; y: list(A); P(y) |] ==> P() + P(Nil); + !!x y. [| x: A; y: list(A); P(y) |] ==> P(Cons(x,y)) |] ==> P(l) -\idx{list_case_0} list_case(0,c,h) = c -\idx{list_case_Pair} list_case(, c, h) = h(a,l) +\idx{Cons_iff} Cons(a,l)=Cons(a',l') <-> a=a' & l=l' +\idx{Nil_Cons_iff} ~ Nil=Cons(a,l) -\idx{list_rec_0} list_rec(0,c,h) = c -\idx{list_rec_Pair} list_rec(, c, h) = h(a, l, list_rec(l,c,h)) +\idx{list_mono} A<=B ==> list(A) <= list(B) + +\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) @@ -1162,6 +1259,14 @@ injections and a case analysis operator. See files \ttindexbold{ZF/bool.ML} and \ttindexbold{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 +defines the eliminator \ttindexbold{qsplit}, the converse operator +\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}. + 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}. @@ -1170,6 +1275,13 @@ 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. +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}. + 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}. @@ -1182,23 +1294,34 @@ remainder are defined by repeated subtraction, which requires well-founded rather than primitive recursion. -Figure~\ref{zf-list} presents defines the set of lists over~$A$, ${\tt -list}(A)$ as the least solution of the equation ${\tt list}(A)\equiv \{0\} -\union (A\times{\tt list}(A))$. Structural induction and recursion are -derived, with some of the usual list functions. See file -\ttindexbold{ZF/list.ML}. +The file \ttindexbold{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)$, +for constructing co-datatypes such as streams. It is similar 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 +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}. + +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 +recursion and the usual list functions. The constructions of the natural numbers and lists make use of a suite of -operators for handling recursive definitions. The developments are +operators for handling recursive function definitions. The developments are summarized below: \begin{description} -\item[\ttindexbold{ZF/lfp.ML}] -proves the Knaster-Tarski Fixedpoint Theorem in the lattice of subsets of a -set. The file defines a least fixedpoint operator with corresponding -induction rules. These are used repeatedly in the sequel to define sets -inductively. As a simple application, the file contains a short proof of -the Schr\"oder-Bernstein Theorem. - \item[\ttindexbold{ZF/trancl.ML}] defines the transitive closure of a relation (as a least fixedpoint). @@ -1207,9 +1330,11 @@ approach of Tobias Nipkow. This theorem permits general recursive definitions within set theory. -\item[\ttindexbold{ZF/ordinal.ML}] -defines the notions of transitive set and ordinal number. It derives -transfinite induction. +\item[\ttindexbold{ZF/ord.ML}] defines the notions of transitive set and + ordinal number. It derives transfinite induction. A key definition is + {\bf less than}: $i