--- 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(<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>))}
+{\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
--- 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}).
--- 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
--- 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];
--- 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,b> == \{\{a,a\}, \{a,b\}\}
-\idx{split_def} split(p,c) == THE y. EX a b. p=<a,b> & 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=<a,b> & y=c(a,b)
+\idx{fst_def} fst(A) == split(%x y.x, p)
+\idx{snd_def} snd(A) == split(%x y.y, p)
\idx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
\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,b>) = a
\idx{snd} snd(<a,b>) = b
-\idx{split} split(<a,b>, %x y.c(x,y)) = c(a,b)
+\idx{split} split(%x y.c(x,y), <a,b>) = c(a,b)
\idx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)
@@ -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> == a+b
+\idx{qsplit_def} qsplit(c,p) == THE y. EX a b. p=<a;b> & y=c(a,b)
+\idx{qfsplit_def} qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)
+\idx{qconverse_def} qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}
+\idx{QSigma_def} QSigma(A,B) == UN x:A. UN y:B(x). {<x;y>}
+
+\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 = <x,y> & 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. <f(x), 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) |] ==> <a,l> : 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(<x,y>)
+ 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(<a,l>, 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(<a,l>, 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<j$ if and only if $i$ and $j$ are both ordinals and
+ $i\in j$. As a special case, it includes less than on the natural
+ numbers.
\item[\ttindexbold{ZF/epsilon.ML}]
derives $\epsilon$-induction and $\epsilon$-recursion, which are
@@ -1217,30 +1342,21 @@
\ttindexbold{rank}$(x)$, which is the least ordinal $\alpha$ such that $x$
is constructed at stage $\alpha$ of the cumulative hierarchy (thus $x\in
V@{\alpha+1}$).
-
-\item[\ttindexbold{ZF/univ.ML}]
-defines a ``universe'' ${\tt univ}(A)$, for constructing sets inductively.
-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.
\end{description}
\begin{figure}
\begin{eqnarray*}
- a\in a & \bimp & \bot\\
- a\in \emptyset & \bimp & \bot\\
- a \in A \union B & \bimp & a\in A \disj a\in B\\
- a \in A \inter B & \bimp & a\in A \conj a\in B\\
- a \in A-B & \bimp & a\in A \conj \neg (a\in B)\\
+ a\in \emptyset & \bimp & \bot\\
+ a \in A \union B & \bimp & a\in A \disj a\in B\\
+ a \in A \inter B & \bimp & a\in A \conj a\in B\\
+ a \in A-B & \bimp & a\in A \conj \neg (a\in B)\\
a \in {\tt cons}(b,B) & \bimp & a=b \disj a\in B\\
- i \in {\tt succ}(j) & \bimp & i=j \disj i\in j\\
+ i \in {\tt succ}(j) & \bimp & i=j \disj i\in j\\
\pair{a,b}\in {\tt Sigma}(A,B)
- & \bimp & a\in A \conj b\in B(a)\\
- a \in {\tt Collect}(A,P) & \bimp & a\in A \conj P(a)\\
- (\forall x \in A. \top) & \bimp & \top
+ & \bimp & a\in A \conj b\in B(a)\\
+ a \in {\tt Collect}(A,P) & \bimp & a\in A \conj P(a)\\
+ (\forall x \in A. \top) & \bimp & \top
\end{eqnarray*}
\caption{Rewrite rules for set theory} \label{ZF-simpdata}
\end{figure}
@@ -1271,9 +1387,9 @@
This directory contains further developments in {\ZF} set theory. Here is
an overview; see the files themselves for more details.
\begin{description}
-\item[\ttindexbold{ZF/ex/misc.ML}]
-contains miscellaneous examples such as Cantor's Theorem and the
-``Composition of homomorphisms'' challenge.
+\item[\ttindexbold{ZF/ex/misc.ML}] contains miscellaneous examples such as
+ Cantor's Theorem, the Schr\"oder-Bernstein Theorem. and the
+ ``Composition of homomorphisms'' challenge~\cite{boyer86}.
\item[\ttindexbold{ZF/ex/ramsey.ML}]
proves the finite exponent 2 version of Ramsey's Theorem.
@@ -1288,7 +1404,7 @@
\item[\ttindexbold{ZF/ex/term.ML}]
defines a recursive data structure for terms and term lists.
-\item[\ttindexbold{ZF/ex/simult.ML}]
+\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.
@@ -1296,7 +1412,7 @@
\item[\ttindexbold{ZF/ex/finite.ML}]
inductively defines a finite powerset operator.
-\item[\ttindexbold{ZF/ex/prop-log.ML}]
+\item[\ttindexbold{ZF/ex/proplog.ML}]
proves soundness and completeness of propositional logic. This illustrates
the main forms of induction.
\end{description}
--- a/doc-src/Logics/intro.tex Thu Nov 11 12:44:43 1993 +0100
+++ b/doc-src/Logics/intro.tex Thu Nov 11 13:18:49 1993 +0100
@@ -13,7 +13,7 @@
axioms~\cite{suppes72}. It is built upon classical~\FOL{}.
{\ttindexbold{HOL}} is the higher-order logic of Church~\cite{church40},
-which is also implemented by Gordon's~{\sc hol} system~\cite{gordon88a}. This
+which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon88a}. This
object-logic should not be confused with Isabelle's meta-logic, which is
also a form of higher-order logic.
--- a/doc-src/Logics/logics.tex Thu Nov 11 12:44:43 1993 +0100
+++ b/doc-src/Logics/logics.tex Thu Nov 11 13:18:49 1993 +0100
@@ -1,7 +1,7 @@
\documentstyle[a4,12pt,proof,iman,alltt]{report}
%% $Id$
%%%STILL NEEDS MODAL, LCF
-\includeonly{HOL}
+%%%\includeonly{ZF}
%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\idx{\1}
%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\idx{\1}
%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\idx{\1}
@@ -56,6 +56,6 @@
%%\include{LCF}
\include{defining}
\bibliographystyle{plain}
-\bibliography{atp,theory,funprog,logicprog}
+\bibliography{atp,theory,funprog,logicprog,isabelle}
\input{logics.ind}
\end{document}