1.1 --- a/doc-src/ZF/FOL.tex Wed Feb 16 10:50:57 2000 +0100
1.2 +++ b/doc-src/ZF/FOL.tex Wed Feb 16 10:51:23 2000 +0100
1.3 @@ -578,12 +578,12 @@
1.4 {\out 1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)}
1.5 \end{ttbox}
1.6 In classical logic, a negated assumption is equivalent to a conclusion. To
1.7 -get this effect, we create a swapped version of~$(\forall I)$ and apply it
1.8 -using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall
1.9 +get this effect, we create a swapped version of $(\forall I)$ and apply it
1.10 +using \ttindex{eresolve_tac}; we could equivalently have applied $(\forall
1.11 I)$ using \ttindex{swap_res_tac}.
1.12 \begin{ttbox}
1.13 allI RSN (2,swap);
1.14 -{\out val it = "[| ~ (ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm}
1.15 +{\out val it = "[| ~(ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm}
1.16 by (eresolve_tac [it] 1);
1.17 {\out Level 5}
1.18 {\out EX y. ALL x. P(y) --> P(x)}
2.1 --- a/doc-src/ZF/ZF.tex Wed Feb 16 10:50:57 2000 +0100
2.2 +++ b/doc-src/ZF/ZF.tex Wed Feb 16 10:51:23 2000 +0100
2.3 @@ -909,14 +909,14 @@
2.4
2.5 \begin{figure}
2.6 \begin{ttbox}
2.7 -\tdx{lamI} a:A ==> <a,b(a)> : (lam x:A. b(x))
2.8 -\tdx{lamE} [| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P
2.9 - |] ==> P
2.10 -
2.11 -\tdx{lam_type} [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)
2.12 -
2.13 -\tdx{beta} a : A ==> (lam x:A. b(x)) ` a = b(a)
2.14 -\tdx{eta} f : Pi(A,B) ==> (lam x:A. f`x) = f
2.15 +\tdx{lamI} a:A ==> <a,b(a)> : (lam x:A. b(x))
2.16 +\tdx{lamE} [| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P
2.17 + |] ==> P
2.18 +
2.19 +\tdx{lam_type} [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)
2.20 +
2.21 +\tdx{beta} a : A ==> (lam x:A. b(x)) ` a = b(a)
2.22 +\tdx{eta} f : Pi(A,B) ==> (lam x:A. f`x) = f
2.23 \end{ttbox}
2.24 \caption{$\lambda$-abstraction} \label{zf-lam}
2.25 \end{figure}
2.26 @@ -1263,7 +1263,8 @@
2.27 \tdx{nat_def} nat == lfp(lam r: Pow(Inf). {\ttlbrace}0{\ttrbrace} Un {\ttlbrace}succ(x). x:r{\ttrbrace}
2.28
2.29 \tdx{mod_def} m mod n == transrec(m, \%j f. if j:n then j else f`(j#-n))
2.30 -\tdx{div_def} m div n == transrec(m, \%j f. if j:n then 0 else succ(f`(j#-n)))
2.31 +\tdx{div_def} m div n == transrec(m, \%j f. if j:n then 0
2.32 + else succ(f`(j#-n)))
2.33
2.34 \tdx{nat_case_def} nat_case(a,b,k) ==
2.35 THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))
2.36 @@ -1285,7 +1286,8 @@
2.37 \tdx{mult_0} 0 #* n = 0
2.38 \tdx{mult_succ} succ(m) #* n = n #+ (m #* n)
2.39 \tdx{mult_commute} [| m:nat; n:nat |] ==> m #* n = n #* m
2.40 -\tdx{add_mult_dist} [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k){\thinspace}#+{\thinspace}(n #* k)
2.41 +\tdx{add_mult_dist} [| m:nat; k:nat |] ==>
2.42 + (m #+ n) #* k = (m #* k) #+ (n #* k)
2.43 \tdx{mult_assoc}
2.44 [| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)
2.45 \tdx{mod_quo_equality}
2.46 @@ -1452,7 +1454,7 @@
2.47 essentially type-checking. Such proofs are built by applying rules such as
2.48 these:
2.49 \begin{ttbox}
2.50 -[| ?P ==> ?a : ?A; ~ ?P ==> ?b : ?A |] ==> (if ?P then ?a else ?b) : ?A
2.51 +[| ?P ==> ?a: ?A; ~?P ==> ?b: ?A |] ==> (if ?P then ?a else ?b): ?A
2.52
2.53 [| ?m : nat; ?n : nat |] ==> ?m #+ ?n : nat
2.54
2.55 @@ -1625,7 +1627,8 @@
2.56 and forests:
2.57 \begin{ttbox}
2.58 [| x : tree_forest(A);
2.59 - !!a f. [| a : A; f : forest(A); P(f) |] ==> P(Tcons(a, f)); P(Fnil);
2.60 + !!a f. [| a : A; f : forest(A); P(f) |] ==> P(Tcons(a, f));
2.61 + P(Fnil);
2.62 !!f t. [| t : tree(A); P(t); f : forest(A); P(f) |]
2.63 ==> P(Fcons(t, f))
2.64 |] ==> P(x)
2.65 @@ -1647,7 +1650,7 @@
2.66 refers to the monotonic operator, \texttt{list}:
2.67 \begin{ttbox}
2.68 [| x : term(A);
2.69 - !!a l. [| a : A; l : list(Collect(term(A), P)) |] ==> P(Apply(a, l))
2.70 + !!a l. [| a: A; l: list(Collect(term(A), P)) |] ==> P(Apply(a, l))
2.71 |] ==> P(x)
2.72 \end{ttbox}
2.73 The file \texttt{ex/Term.ML} derives two higher-level induction rules, one of
2.74 @@ -1797,7 +1800,8 @@
2.75 {\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l}
2.76 {\out 1. ALL x r. Br(x, Lf, r) ~= Lf}
2.77 {\out 2. !!a t1 t2.}
2.78 -{\out [| a : A; t1 : bt(A); ALL x r. Br(x, t1, r) ~= t1; t2 : bt(A);}
2.79 +{\out [| a : A; t1 : bt(A);}
2.80 +{\out ALL x r. Br(x, t1, r) ~= t1; t2 : bt(A);}
2.81 {\out ALL x r. Br(x, t2, r) ~= t2 |]}
2.82 {\out ==> ALL x r. Br(x, Br(a, t1, t2), r) ~= Br(a, t1, t2)}
2.83 \end{ttbox}
2.84 @@ -1820,7 +1824,8 @@
2.85 theorems for each constructor. This is trivial, using the function given us
2.86 for that purpose:
2.87 \begin{ttbox}
2.88 -val Br_iff = bt.mk_free "Br(a,l,r)=Br(a',l',r') <-> a=a' & l=l' & r=r'";
2.89 +val Br_iff =
2.90 + bt.mk_free "Br(a,l,r)=Br(a',l',r') <-> a=a' & l=l' & r=r'";
2.91 {\out val Br_iff =}
2.92 {\out "Br(?a, ?l, ?r) = Br(?a', ?l', ?r') <->}
2.93 {\out ?a = ?a' & ?l = ?l' & ?r = ?r'" : thm}
2.94 @@ -1834,7 +1839,8 @@
2.95 val BrE = bt.mk_cases "Br(a,l,r) : bt(A)";
2.96 {\out val BrE =}
2.97 {\out "[| Br(?a, ?l, ?r) : bt(?A);}
2.98 -{\out [| ?a : ?A; ?l : bt(?A); ?r : bt(?A) |] ==> ?Q |] ==> ?Q" : thm}
2.99 +{\out [| ?a : ?A; ?l : bt(?A); ?r : bt(?A) |] ==> ?Q |]}
2.100 +{\out ==> ?Q" : thm}
2.101 \end{ttbox}
2.102
2.103
2.104 @@ -2021,7 +2027,7 @@
2.105 type_elims {\it elimination rules for type-checking}
2.106 \end{ttbox}
2.107 A coinductive definition is identical, but starts with the keyword
2.108 -{\tt coinductive}.
2.109 +{\tt co\-inductive}.
2.110
2.111 The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}
2.112 sections are optional. If present, each is specified either as a list of
2.113 @@ -2031,7 +2037,7 @@
2.114 error messages. You can then inspect the file on the temporary directory.
2.115
2.116 \begin{description}
2.117 -\item[\it domain declarations] consist of one or more items of the form
2.118 +\item[\it domain declarations] are items of the form
2.119 {\it string\/}~{\tt <=}~{\it string}, associating each recursive set with
2.120 its domain. (The domain is some existing set that is large enough to
2.121 hold the new set being defined.)