author paulson Wed, 16 Feb 2000 10:51:23 +0100 changeset 8249 3fc32155372c parent 8248 d7e85fd09291 child 8250 f4029c34adef
fixed some overfull lines
 doc-src/ZF/FOL.tex file | annotate | diff | comparison | revisions doc-src/ZF/ZF.tex file | annotate | diff | comparison | revisions
--- a/doc-src/ZF/FOL.tex	Wed Feb 16 10:50:57 2000 +0100
+++ b/doc-src/ZF/FOL.tex	Wed Feb 16 10:51:23 2000 +0100
@@ -578,12 +578,12 @@
{\out  1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)}
\end{ttbox}
In classical logic, a negated assumption is equivalent to a conclusion.  To
-get this effect, we create a swapped version of~$(\forall I)$ and apply it
-using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall +get this effect, we create a swapped version of$(\forall I)$and apply it +using \ttindex{eresolve_tac}; we could equivalently have applied$(\forall
I)$using \ttindex{swap_res_tac}. \begin{ttbox} allI RSN (2,swap); -{\out val it = "[| ~ (ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm} +{\out val it = "[| ~(ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm} by (eresolve_tac [it] 1); {\out Level 5} {\out EX y. ALL x. P(y) --> P(x)} --- a/doc-src/ZF/ZF.tex Wed Feb 16 10:50:57 2000 +0100 +++ b/doc-src/ZF/ZF.tex Wed Feb 16 10:51:23 2000 +0100 @@ -909,14 +909,14 @@ \begin{figure} \begin{ttbox} -\tdx{lamI} a:A ==> <a,b(a)> : (lam x:A. b(x)) -\tdx{lamE} [| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P - |] ==> P - -\tdx{lam_type} [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B) - -\tdx{beta} a : A ==> (lam x:A. b(x))  a = b(a) -\tdx{eta} f : Pi(A,B) ==> (lam x:A. fx) = f +\tdx{lamI} a:A ==> <a,b(a)> : (lam x:A. b(x)) +\tdx{lamE} [| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P + |] ==> P + +\tdx{lam_type} [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B) + +\tdx{beta} a : A ==> (lam x:A. b(x))  a = b(a) +\tdx{eta} f : Pi(A,B) ==> (lam x:A. fx) = f \end{ttbox} \caption{$\lambda\$-abstraction} \label{zf-lam}
\end{figure}
@@ -1263,7 +1263,8 @@
\tdx{nat_def}  nat == lfp(lam r: Pow(Inf). {\ttlbrace}0{\ttrbrace} Un {\ttlbrace}succ(x). x:r{\ttrbrace}

\tdx{mod_def}  m mod n == transrec(m, \%j f. if j:n then j else f(j#-n))
-\tdx{div_def}  m div n == transrec(m, \%j f. if j:n then 0 else succ(f(j#-n)))
+\tdx{div_def}  m div n == transrec(m, \%j f. if j:n then 0
+                                       else succ(f`(j#-n)))

\tdx{nat_case_def}  nat_case(a,b,k) ==
THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))
@@ -1285,7 +1286,8 @@
\tdx{mult_0}        0 #* n = 0
\tdx{mult_succ}     succ(m) #* n = n #+ (m #* n)
\tdx{mult_commute}  [| m:nat; n:nat |] ==> m #* n = n #* m
-\tdx{add_mult_dist} [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k){\thinspace}#+{\thinspace}(n #* k)
+\tdx{add_mult_dist} [| m:nat; k:nat |] ==>
+              (m #+ n) #* k = (m #* k) #+ (n #* k)
\tdx{mult_assoc}
[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)
\tdx{mod_quo_equality}
@@ -1452,7 +1454,7 @@
essentially type-checking.  Such proofs are built by applying rules such as
these:
\begin{ttbox}
-[| ?P ==> ?a : ?A; ~ ?P ==> ?b : ?A |] ==> (if ?P then ?a else ?b) : ?A
+[| ?P ==> ?a: ?A; ~?P ==> ?b: ?A |] ==> (if ?P then ?a else ?b): ?A

[| ?m : nat; ?n : nat |] ==> ?m #+ ?n : nat

@@ -1625,7 +1627,8 @@
and forests:
\begin{ttbox}
[| x : tree_forest(A);
-   !!a f. [| a : A; f : forest(A); P(f) |] ==> P(Tcons(a, f)); P(Fnil);
+   !!a f. [| a : A; f : forest(A); P(f) |] ==> P(Tcons(a, f));
+   P(Fnil);
!!f t. [| t : tree(A); P(t); f : forest(A); P(f) |]
==> P(Fcons(t, f))
|] ==> P(x)
@@ -1647,7 +1650,7 @@
refers to the monotonic operator, \texttt{list}:
\begin{ttbox}
[| x : term(A);
-   !!a l. [| a : A; l : list(Collect(term(A), P)) |] ==> P(Apply(a, l))
+   !!a l. [| a: A; l: list(Collect(term(A), P)) |] ==> P(Apply(a, l))
|] ==> P(x)
\end{ttbox}
The file \texttt{ex/Term.ML} derives two higher-level induction rules, one of
@@ -1797,7 +1800,8 @@
{\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l}
{\out  1. ALL x r. Br(x, Lf, r) ~= Lf}
{\out  2. !!a t1 t2.}
-{\out        [| a : A; t1 : bt(A); ALL x r. Br(x, t1, r) ~= t1; t2 : bt(A);}
+{\out        [| a : A; t1 : bt(A);}
+{\out           ALL x r. Br(x, t1, r) ~= t1; t2 : bt(A);}
{\out           ALL x r. Br(x, t2, r) ~= t2 |]}
{\out        ==> ALL x r. Br(x, Br(a, t1, t2), r) ~= Br(a, t1, t2)}
\end{ttbox}
@@ -1820,7 +1824,8 @@
theorems for each constructor.  This is trivial, using the function given us
for that purpose:
\begin{ttbox}
-val Br_iff = bt.mk_free "Br(a,l,r)=Br(a',l',r') <-> a=a' & l=l' & r=r'";
+val Br_iff =
+    bt.mk_free "Br(a,l,r)=Br(a',l',r') <-> a=a' & l=l' & r=r'";
{\out val Br_iff =}
{\out   "Br(?a, ?l, ?r) = Br(?a', ?l', ?r') <->}
{\out                     ?a = ?a' & ?l = ?l' & ?r = ?r'" : thm}
@@ -1834,7 +1839,8 @@
val BrE = bt.mk_cases "Br(a,l,r) : bt(A)";
{\out val BrE =}
{\out   "[| Br(?a, ?l, ?r) : bt(?A);}
-{\out       [| ?a : ?A; ?l : bt(?A); ?r : bt(?A) |] ==> ?Q |] ==> ?Q" : thm}
+{\out       [| ?a : ?A; ?l : bt(?A); ?r : bt(?A) |] ==> ?Q |]}
+{\out    ==> ?Q" : thm}
\end{ttbox}

@@ -2021,7 +2027,7 @@
type_elims {\it elimination rules for type-checking}
\end{ttbox}
A coinductive definition is identical, but starts with the keyword
-{\tt coinductive}.
+{\tt co\-inductive}.

The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}
sections are optional.  If present, each is specified either as a list of
@@ -2031,7 +2037,7 @@
error messages.  You can then inspect the file on the temporary directory.

\begin{description}
-\item[\it domain declarations] consist of one or more items of the form
+\item[\it domain declarations] are items of the form
{\it string\/}~{\tt <=}~{\it string}, associating each recursive set with
its domain.  (The domain is some existing set that is large enough to
hold the new set being defined.)