doc-src/ZF/ZF.tex

 \end{figure}
 
 
 \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. f`x) = 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. f`x) = f
 \end{ttbox}
 \caption{$\lambda$-abstraction} \label{zf-lam}
 \end{figure}
 
 

 
 \begin{ttbox}
 \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))
 
 \tdx{nat_0I}        0 : nat

 
 \tdx{mult_type}     [| m:nat;  n:nat |] ==> m #* n : nat
 \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}
     [| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m
 \end{ttbox}

 
 Isabelle/{\ZF} provides simple tactics to help automate those proofs that are
 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
 
 ?a : ?A ==> Inl(?a) : ?A + ?B  
 \end{ttbox}

 \texttt{TF}.  The rule \texttt{tree_forest.induct} performs induction over a
 single predicate~\texttt{P}, which is presumed to be defined for both trees
 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)
 \end{ttbox}
 The rule \texttt{tree_forest.mutual_induct} performs induction over two

 For datatypes with nested recursion, such as the \texttt{term} example from
 above, things are a bit more complicated.  The rule \texttt{term.induct}
 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
 which is particularly useful for proving equations:
 \begin{ttbox}

 by (induct_tac "l" 1);
 {\out Level 1}
 {\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}
 Both subgoals are proved using \texttt{Auto_tac}, which performs the necessary
 freeness reasoning. 

 
 When there are only a few constructors, we might prefer to prove the freenness
 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}
 \end{ttbox}
 

 information from the premise $\texttt{Br}(a,l,r)\in\texttt{bt}(A)$:
 \begin{ttbox}
 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}
 
 
 \subsubsection{Mixfix syntax in datatypes}
 

   con_defs   {\it constructor definitions}
   type_intrs {\it introduction rules for type-checking}
   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
 identifiers or as a string.  If the latter, then the string must be a valid
 \textsc{ml} expression of type {\tt thm list}.  The string is simply inserted
 into the {\tt _thy.ML} file; if it is ill-formed, it will trigger \textsc{ml}
 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.)
 
 \item[\it introduction rules] specify one or more introduction rules in