the separate FOL and ZF logics manual, with new material on datatypes and
authorpaulson
Wed Jan 13 16:36:36 1999 +0100 (1999-01-13)
changeset 61215fe77b9b5185
parent 6120 f40d61cd6b32
child 6122 ebbea9e7aa9e
the separate FOL and ZF logics manual, with new material on datatypes and
inductive definitions
doc-src/ZF/FOL-eg.txt
doc-src/ZF/FOL.tex
doc-src/ZF/Makefile
doc-src/ZF/ZF-eg.txt
doc-src/ZF/ZF.tex
doc-src/ZF/logics-ZF.bbl
doc-src/ZF/logics-ZF.tex
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/ZF/FOL-eg.txt	Wed Jan 13 16:36:36 1999 +0100
     1.3 @@ -0,0 +1,245 @@
     1.4 +(**** FOL examples ****)
     1.5 +
     1.6 +Pretty.setmargin 72;  (*existing macros just allow this margin*)
     1.7 +print_depth 0;
     1.8 +
     1.9 +(*** Intuitionistic examples ***)
    1.10 +
    1.11 +context IFOL.thy;
    1.12 +
    1.13 +(*Quantifier example from Logic&Computation*)
    1.14 +Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
    1.15 +by (resolve_tac [impI] 1);
    1.16 +by (resolve_tac [allI] 1);
    1.17 +by (resolve_tac [exI] 1);
    1.18 +by (eresolve_tac [exE] 1);
    1.19 +choplev 2;
    1.20 +by (eresolve_tac [exE] 1);
    1.21 +by (resolve_tac [exI] 1);
    1.22 +by (eresolve_tac [allE] 1);
    1.23 +by (assume_tac 1);
    1.24 +
    1.25 +
    1.26 +(*Example of Dyckhoff's method*)
    1.27 +Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))";
    1.28 +by (resolve_tac [impI] 1);
    1.29 +by (eresolve_tac [disj_impE] 1);
    1.30 +by (eresolve_tac [imp_impE] 1);
    1.31 +by (eresolve_tac [imp_impE] 1);
    1.32 +by (REPEAT (eresolve_tac [FalseE] 2));
    1.33 +by (assume_tac 1);
    1.34 +
    1.35 +
    1.36 +
    1.37 +
    1.38 +
    1.39 +(*** Classical examples ***)
    1.40 +
    1.41 +context FOL.thy;
    1.42 +
    1.43 +Goal "EX y. ALL x. P(y)-->P(x)";
    1.44 +by (resolve_tac [exCI] 1);
    1.45 +by (resolve_tac [allI] 1);
    1.46 +by (resolve_tac [impI] 1);
    1.47 +by (eresolve_tac [allE] 1);
    1.48 +prth (allI RSN (2,swap));
    1.49 +by (eresolve_tac [it] 1);
    1.50 +by (resolve_tac [impI] 1);
    1.51 +by (eresolve_tac [notE] 1);
    1.52 +by (assume_tac 1);
    1.53 +Goal "EX y. ALL x. P(y)-->P(x)";
    1.54 +by (Blast_tac 1);
    1.55 +
    1.56 +
    1.57 +
    1.58 +- Goal "EX y. ALL x. P(y)-->P(x)";
    1.59 +Level 0
    1.60 +EX y. ALL x. P(y) --> P(x)
    1.61 + 1. EX y. ALL x. P(y) --> P(x)
    1.62 +- by (resolve_tac [exCI] 1);
    1.63 +Level 1
    1.64 +EX y. ALL x. P(y) --> P(x)
    1.65 + 1. ALL y. ~(ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)
    1.66 +- by (resolve_tac [allI] 1);
    1.67 +Level 2
    1.68 +EX y. ALL x. P(y) --> P(x)
    1.69 + 1. !!x. ALL y. ~(ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)
    1.70 +- by (resolve_tac [impI] 1);
    1.71 +Level 3
    1.72 +EX y. ALL x. P(y) --> P(x)
    1.73 + 1. !!x. [| ALL y. ~(ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)
    1.74 +- by (eresolve_tac [allE] 1);
    1.75 +Level 4
    1.76 +EX y. ALL x. P(y) --> P(x)
    1.77 + 1. !!x. [| P(?a); ~(ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)
    1.78 +- prth (allI RSN (2,swap));
    1.79 +[| ~(ALL x. ?P1(x)); !!x. ~?Q ==> ?P1(x) |] ==> ?Q
    1.80 +- by (eresolve_tac [it] 1);
    1.81 +Level 5
    1.82 +EX y. ALL x. P(y) --> P(x)
    1.83 + 1. !!x xa. [| P(?a); ~P(x) |] ==> P(?y3(x)) --> P(xa)
    1.84 +- by (resolve_tac [impI] 1);
    1.85 +Level 6
    1.86 +EX y. ALL x. P(y) --> P(x)
    1.87 + 1. !!x xa. [| P(?a); ~P(x); P(?y3(x)) |] ==> P(xa)
    1.88 +- by (eresolve_tac [notE] 1);
    1.89 +Level 7
    1.90 +EX y. ALL x. P(y) --> P(x)
    1.91 + 1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)
    1.92 +- by (assume_tac 1);
    1.93 +Level 8
    1.94 +EX y. ALL x. P(y) --> P(x)
    1.95 +No subgoals!
    1.96 +- Goal "EX y. ALL x. P(y)-->P(x)";
    1.97 +Level 0
    1.98 +EX y. ALL x. P(y) --> P(x)
    1.99 + 1. EX y. ALL x. P(y) --> P(x)
   1.100 +- by (best_tac FOL_dup_cs 1);
   1.101 +Level 1
   1.102 +EX y. ALL x. P(y) --> P(x)
   1.103 +No subgoals!
   1.104 +
   1.105 +
   1.106 +(**** finally, the example FOL/ex/if.ML ****)
   1.107 +
   1.108 +> val prems = goalw if_thy [if_def]
   1.109 +#    "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
   1.110 +Level 0
   1.111 +if(P,Q,R)
   1.112 + 1. P & Q | ~P & R
   1.113 +> by (Classical.fast_tac (FOL_cs addIs prems) 1);
   1.114 +Level 1
   1.115 +if(P,Q,R)
   1.116 +No subgoals!
   1.117 +> val ifI = result();
   1.118 +
   1.119 +
   1.120 +> val major::prems = goalw if_thy [if_def]
   1.121 +#    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
   1.122 +Level 0
   1.123 +S
   1.124 + 1. S
   1.125 +> by (cut_facts_tac [major] 1);
   1.126 +Level 1
   1.127 +S
   1.128 + 1. P & Q | ~P & R ==> S
   1.129 +> by (Classical.fast_tac (FOL_cs addIs prems) 1);
   1.130 +Level 2
   1.131 +S
   1.132 +No subgoals!
   1.133 +> val ifE = result();
   1.134 +
   1.135 +> goal if_thy "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
   1.136 +Level 0
   1.137 +if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.138 + 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.139 +> by (resolve_tac [iffI] 1);
   1.140 +Level 1
   1.141 +if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.142 + 1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))
   1.143 + 2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.144 +> by (eresolve_tac [ifE] 1);
   1.145 +Level 2
   1.146 +if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.147 + 1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.148 + 2. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.149 + 3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.150 +> by (eresolve_tac [ifE] 1);
   1.151 +Level 3
   1.152 +if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.153 + 1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.154 + 2. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.155 + 3. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.156 + 4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.157 +> by (resolve_tac [ifI] 1);
   1.158 +Level 4
   1.159 +if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.160 + 1. [| P; Q; A; Q |] ==> if(P,A,C)
   1.161 + 2. [| P; Q; A; ~Q |] ==> if(P,B,D)
   1.162 + 3. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.163 + 4. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.164 + 5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.165 +> by (resolve_tac [ifI] 1);
   1.166 +Level 5
   1.167 +if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.168 + 1. [| P; Q; A; Q; P |] ==> A
   1.169 + 2. [| P; Q; A; Q; ~P |] ==> C
   1.170 + 3. [| P; Q; A; ~Q |] ==> if(P,B,D)
   1.171 + 4. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.172 + 5. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.173 + 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.174 +
   1.175 +> choplev 0;
   1.176 +Level 0
   1.177 +if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.178 + 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.179 +> val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];
   1.180 +> by (Classical.fast_tac if_cs 1);
   1.181 +Level 1
   1.182 +if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.183 +No subgoals!
   1.184 +> val if_commute = result();
   1.185 +
   1.186 +> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
   1.187 +Level 0
   1.188 +if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.189 + 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.190 +> by (Classical.fast_tac if_cs 1);
   1.191 +Level 1
   1.192 +if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.193 +No subgoals!
   1.194 +> val nested_ifs = result();
   1.195 +
   1.196 +
   1.197 +> choplev 0;
   1.198 +Level 0
   1.199 +if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.200 + 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.201 +> by (rewrite_goals_tac [if_def]);
   1.202 +Level 1
   1.203 +if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.204 + 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->
   1.205 +    P & (Q & A | ~Q & B) | ~P & (R & A | ~R & B)
   1.206 +> by (Classical.fast_tac FOL_cs 1);
   1.207 +Level 2
   1.208 +if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.209 +No subgoals!
   1.210 +
   1.211 +
   1.212 +> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
   1.213 +Level 0
   1.214 +if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.215 + 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.216 +> by (REPEAT (Classical.step_tac if_cs 1));
   1.217 +Level 1
   1.218 +if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.219 + 1. [| A; ~P; R; ~P; R |] ==> B
   1.220 + 2. [| B; ~P; ~R; ~P; ~R |] ==> A
   1.221 + 3. [| ~P; R; B; ~P; R |] ==> A
   1.222 + 4. [| ~P; ~R; A; ~B; ~P |] ==> R
   1.223 +
   1.224 +> choplev 0;
   1.225 +Level 0
   1.226 +if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.227 + 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.228 +> by (rewrite_goals_tac [if_def]);
   1.229 +Level 1
   1.230 +if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.231 + 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->
   1.232 +    P & (Q & A | ~Q & B) | ~P & (R & B | ~R & A)
   1.233 +> by (Classical.fast_tac FOL_cs 1);
   1.234 +by: tactic failed
   1.235 +Exception- ERROR raised
   1.236 +Exception failure raised
   1.237 +
   1.238 +> by (REPEAT (Classical.step_tac FOL_cs 1));
   1.239 +Level 2
   1.240 +if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.241 + 1. [| A; ~P; R; ~P; R; ~False |] ==> B
   1.242 + 2. [| A; ~P; R; R; ~False; ~B; ~B |] ==> Q
   1.243 + 3. [| B; ~P; ~R; ~P; ~A |] ==> R
   1.244 + 4. [| B; ~P; ~R; ~Q; ~A |] ==> R
   1.245 + 5. [| B; ~R; ~P; ~A; ~R; Q; ~False |] ==> A
   1.246 + 6. [| ~P; R; B; ~P; R; ~False |] ==> A
   1.247 + 7. [| ~P; ~R; A; ~B; ~R |] ==> P
   1.248 + 8. [| ~P; ~R; A; ~B; ~R |] ==> Q
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/ZF/FOL.tex	Wed Jan 13 16:36:36 1999 +0100
     2.3 @@ -0,0 +1,936 @@
     2.4 +%% $Id$
     2.5 +\chapter{First-Order Logic}
     2.6 +\index{first-order logic|(}
     2.7 +
     2.8 +Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc
     2.9 +  nk}.  Intuitionistic first-order logic is defined first, as theory
    2.10 +\thydx{IFOL}.  Classical logic, theory \thydx{FOL}, is
    2.11 +obtained by adding the double negation rule.  Basic proof procedures are
    2.12 +provided.  The intuitionistic prover works with derived rules to simplify
    2.13 +implications in the assumptions.  Classical~\texttt{FOL} employs Isabelle's
    2.14 +classical reasoner, which simulates a sequent calculus.
    2.15 +
    2.16 +\section{Syntax and rules of inference}
    2.17 +The logic is many-sorted, using Isabelle's type classes.  The class of
    2.18 +first-order terms is called \cldx{term} and is a subclass of \texttt{logic}.
    2.19 +No types of individuals are provided, but extensions can define types such
    2.20 +as \texttt{nat::term} and type constructors such as \texttt{list::(term)term}
    2.21 +(see the examples directory, \texttt{FOL/ex}).  Below, the type variable
    2.22 +$\alpha$ ranges over class \texttt{term}; the equality symbol and quantifiers
    2.23 +are polymorphic (many-sorted).  The type of formulae is~\tydx{o}, which
    2.24 +belongs to class~\cldx{logic}.  Figure~\ref{fol-syntax} gives the syntax.
    2.25 +Note that $a$\verb|~=|$b$ is translated to $\neg(a=b)$.
    2.26 +
    2.27 +Figure~\ref{fol-rules} shows the inference rules with their~\ML\ names.
    2.28 +Negation is defined in the usual way for intuitionistic logic; $\neg P$
    2.29 +abbreviates $P\imp\bot$.  The biconditional~($\bimp$) is defined through
    2.30 +$\conj$ and~$\imp$; introduction and elimination rules are derived for it.
    2.31 +
    2.32 +The unique existence quantifier, $\exists!x.P(x)$, is defined in terms
    2.33 +of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested
    2.34 +quantifications.  For instance, $\exists!x\;y.P(x,y)$ abbreviates
    2.35 +$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
    2.36 +exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
    2.37 +
    2.38 +Some intuitionistic derived rules are shown in
    2.39 +Fig.\ts\ref{fol-int-derived}, again with their \ML\ names.  These include
    2.40 +rules for the defined symbols $\neg$, $\bimp$ and $\exists!$.  Natural
    2.41 +deduction typically involves a combination of forward and backward
    2.42 +reasoning, particularly with the destruction rules $(\conj E)$,
    2.43 +$({\imp}E)$, and~$(\forall E)$.  Isabelle's backward style handles these
    2.44 +rules badly, so sequent-style rules are derived to eliminate conjunctions,
    2.45 +implications, and universal quantifiers.  Used with elim-resolution,
    2.46 +\tdx{allE} eliminates a universal quantifier while \tdx{all_dupE}
    2.47 +re-inserts the quantified formula for later use.  The rules {\tt
    2.48 +conj_impE}, etc., support the intuitionistic proof procedure
    2.49 +(see~\S\ref{fol-int-prover}).
    2.50 +
    2.51 +See the files \texttt{FOL/IFOL.thy}, \texttt{FOL/IFOL.ML} and
    2.52 +\texttt{FOL/intprover.ML} for complete listings of the rules and
    2.53 +derived rules.
    2.54 +
    2.55 +\begin{figure} 
    2.56 +\begin{center}
    2.57 +\begin{tabular}{rrr} 
    2.58 +  \it name      &\it meta-type  & \it description \\ 
    2.59 +  \cdx{Trueprop}& $o\To prop$           & coercion to $prop$\\
    2.60 +  \cdx{Not}     & $o\To o$              & negation ($\neg$) \\
    2.61 +  \cdx{True}    & $o$                   & tautology ($\top$) \\
    2.62 +  \cdx{False}   & $o$                   & absurdity ($\bot$)
    2.63 +\end{tabular}
    2.64 +\end{center}
    2.65 +\subcaption{Constants}
    2.66 +
    2.67 +\begin{center}
    2.68 +\begin{tabular}{llrrr} 
    2.69 +  \it symbol &\it name     &\it meta-type & \it priority & \it description \\
    2.70 +  \sdx{ALL}  & \cdx{All}  & $(\alpha\To o)\To o$ & 10 & 
    2.71 +        universal quantifier ($\forall$) \\
    2.72 +  \sdx{EX}   & \cdx{Ex}   & $(\alpha\To o)\To o$ & 10 & 
    2.73 +        existential quantifier ($\exists$) \\
    2.74 +  \texttt{EX!}  & \cdx{Ex1}  & $(\alpha\To o)\To o$ & 10 & 
    2.75 +        unique existence ($\exists!$)
    2.76 +\end{tabular}
    2.77 +\index{*"E"X"! symbol}
    2.78 +\end{center}
    2.79 +\subcaption{Binders} 
    2.80 +
    2.81 +\begin{center}
    2.82 +\index{*"= symbol}
    2.83 +\index{&@{\tt\&} symbol}
    2.84 +\index{*"| symbol}
    2.85 +\index{*"-"-"> symbol}
    2.86 +\index{*"<"-"> symbol}
    2.87 +\begin{tabular}{rrrr} 
    2.88 +  \it symbol    & \it meta-type         & \it priority & \it description \\ 
    2.89 +  \tt =         & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\
    2.90 +  \tt \&        & $[o,o]\To o$          & Right 35 & conjunction ($\conj$) \\
    2.91 +  \tt |         & $[o,o]\To o$          & Right 30 & disjunction ($\disj$) \\
    2.92 +  \tt -->       & $[o,o]\To o$          & Right 25 & implication ($\imp$) \\
    2.93 +  \tt <->       & $[o,o]\To o$          & Right 25 & biconditional ($\bimp$) 
    2.94 +\end{tabular}
    2.95 +\end{center}
    2.96 +\subcaption{Infixes}
    2.97 +
    2.98 +\dquotes
    2.99 +\[\begin{array}{rcl}
   2.100 + formula & = & \hbox{expression of type~$o$} \\
   2.101 +         & | & term " = " term \quad| \quad term " \ttilde= " term \\
   2.102 +         & | & "\ttilde\ " formula \\
   2.103 +         & | & formula " \& " formula \\
   2.104 +         & | & formula " | " formula \\
   2.105 +         & | & formula " --> " formula \\
   2.106 +         & | & formula " <-> " formula \\
   2.107 +         & | & "ALL~" id~id^* " . " formula \\
   2.108 +         & | & "EX~~" id~id^* " . " formula \\
   2.109 +         & | & "EX!~" id~id^* " . " formula
   2.110 +  \end{array}
   2.111 +\]
   2.112 +\subcaption{Grammar}
   2.113 +\caption{Syntax of \texttt{FOL}} \label{fol-syntax}
   2.114 +\end{figure}
   2.115 +
   2.116 +
   2.117 +\begin{figure} 
   2.118 +\begin{ttbox}
   2.119 +\tdx{refl}        a=a
   2.120 +\tdx{subst}       [| a=b;  P(a) |] ==> P(b)
   2.121 +\subcaption{Equality rules}
   2.122 +
   2.123 +\tdx{conjI}       [| P;  Q |] ==> P&Q
   2.124 +\tdx{conjunct1}   P&Q ==> P
   2.125 +\tdx{conjunct2}   P&Q ==> Q
   2.126 +
   2.127 +\tdx{disjI1}      P ==> P|Q
   2.128 +\tdx{disjI2}      Q ==> P|Q
   2.129 +\tdx{disjE}       [| P|Q;  P ==> R;  Q ==> R |] ==> R
   2.130 +
   2.131 +\tdx{impI}        (P ==> Q) ==> P-->Q
   2.132 +\tdx{mp}          [| P-->Q;  P |] ==> Q
   2.133 +
   2.134 +\tdx{FalseE}      False ==> P
   2.135 +\subcaption{Propositional rules}
   2.136 +
   2.137 +\tdx{allI}        (!!x. P(x))  ==> (ALL x.P(x))
   2.138 +\tdx{spec}        (ALL x.P(x)) ==> P(x)
   2.139 +
   2.140 +\tdx{exI}         P(x) ==> (EX x.P(x))
   2.141 +\tdx{exE}         [| EX x.P(x);  !!x. P(x) ==> R |] ==> R
   2.142 +\subcaption{Quantifier rules}
   2.143 +
   2.144 +\tdx{True_def}    True        == False-->False
   2.145 +\tdx{not_def}     ~P          == P-->False
   2.146 +\tdx{iff_def}     P<->Q       == (P-->Q) & (Q-->P)
   2.147 +\tdx{ex1_def}     EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)
   2.148 +\subcaption{Definitions}
   2.149 +\end{ttbox}
   2.150 +
   2.151 +\caption{Rules of intuitionistic logic} \label{fol-rules}
   2.152 +\end{figure}
   2.153 +
   2.154 +
   2.155 +\begin{figure} 
   2.156 +\begin{ttbox}
   2.157 +\tdx{sym}       a=b ==> b=a
   2.158 +\tdx{trans}     [| a=b;  b=c |] ==> a=c
   2.159 +\tdx{ssubst}    [| b=a;  P(a) |] ==> P(b)
   2.160 +\subcaption{Derived equality rules}
   2.161 +
   2.162 +\tdx{TrueI}     True
   2.163 +
   2.164 +\tdx{notI}      (P ==> False) ==> ~P
   2.165 +\tdx{notE}      [| ~P;  P |] ==> R
   2.166 +
   2.167 +\tdx{iffI}      [| P ==> Q;  Q ==> P |] ==> P<->Q
   2.168 +\tdx{iffE}      [| P <-> Q;  [| P-->Q; Q-->P |] ==> R |] ==> R
   2.169 +\tdx{iffD1}     [| P <-> Q;  P |] ==> Q            
   2.170 +\tdx{iffD2}     [| P <-> Q;  Q |] ==> P
   2.171 +
   2.172 +\tdx{ex1I}      [| P(a);  !!x. P(x) ==> x=a |]  ==>  EX! x. P(x)
   2.173 +\tdx{ex1E}      [| EX! x.P(x);  !!x.[| P(x);  ALL y. P(y) --> y=x |] ==> R 
   2.174 +          |] ==> R
   2.175 +\subcaption{Derived rules for \(\top\), \(\neg\), \(\bimp\) and \(\exists!\)}
   2.176 +
   2.177 +\tdx{conjE}     [| P&Q;  [| P; Q |] ==> R |] ==> R
   2.178 +\tdx{impE}      [| P-->Q;  P;  Q ==> R |] ==> R
   2.179 +\tdx{allE}      [| ALL x.P(x);  P(x) ==> R |] ==> R
   2.180 +\tdx{all_dupE}  [| ALL x.P(x);  [| P(x); ALL x.P(x) |] ==> R |] ==> R
   2.181 +\subcaption{Sequent-style elimination rules}
   2.182 +
   2.183 +\tdx{conj_impE} [| (P&Q)-->S;  P-->(Q-->S) ==> R |] ==> R
   2.184 +\tdx{disj_impE} [| (P|Q)-->S;  [| P-->S; Q-->S |] ==> R |] ==> R
   2.185 +\tdx{imp_impE}  [| (P-->Q)-->S;  [| P; Q-->S |] ==> Q;  S ==> R |] ==> R
   2.186 +\tdx{not_impE}  [| ~P --> S;  P ==> False;  S ==> R |] ==> R
   2.187 +\tdx{iff_impE}  [| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P;
   2.188 +             S ==> R |] ==> R
   2.189 +\tdx{all_impE}  [| (ALL x.P(x))-->S;  !!x.P(x);  S ==> R |] ==> R
   2.190 +\tdx{ex_impE}   [| (EX x.P(x))-->S;  P(a)-->S ==> R |] ==> R
   2.191 +\end{ttbox}
   2.192 +\subcaption{Intuitionistic simplification of implication}
   2.193 +\caption{Derived rules for intuitionistic logic} \label{fol-int-derived}
   2.194 +\end{figure}
   2.195 +
   2.196 +
   2.197 +\section{Generic packages}
   2.198 +\FOL{} instantiates most of Isabelle's generic packages.
   2.199 +\begin{itemize}
   2.200 +\item 
   2.201 +It instantiates the simplifier.  Both equality ($=$) and the biconditional
   2.202 +($\bimp$) may be used for rewriting.  Tactics such as \texttt{Asm_simp_tac} and
   2.203 +\texttt{Full_simp_tac} refer to the default simpset (\texttt{simpset()}), which works for
   2.204 +most purposes.  Named simplification sets include \ttindexbold{IFOL_ss},
   2.205 +for intuitionistic first-order logic, and \ttindexbold{FOL_ss},
   2.206 +for classical logic.  See the file
   2.207 +\texttt{FOL/simpdata.ML} for a complete listing of the simplification
   2.208 +rules%
   2.209 +\iflabelundefined{sec:setting-up-simp}{}%
   2.210 +        {, and \S\ref{sec:setting-up-simp} for discussion}.
   2.211 +
   2.212 +\item 
   2.213 +It instantiates the classical reasoner.  See~\S\ref{fol-cla-prover}
   2.214 +for details. 
   2.215 +
   2.216 +\item \FOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
   2.217 +  for an equality throughout a subgoal and its hypotheses.  This tactic uses
   2.218 +  \FOL's general substitution rule.
   2.219 +\end{itemize}
   2.220 +
   2.221 +\begin{warn}\index{simplification!of conjunctions}%
   2.222 +  Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous.  The
   2.223 +  left part of a conjunction helps in simplifying the right part.  This effect
   2.224 +  is not available by default: it can be slow.  It can be obtained by
   2.225 +  including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
   2.226 +\end{warn}
   2.227 +
   2.228 +
   2.229 +\section{Intuitionistic proof procedures} \label{fol-int-prover}
   2.230 +Implication elimination (the rules~\texttt{mp} and~\texttt{impE}) pose
   2.231 +difficulties for automated proof.  In intuitionistic logic, the assumption
   2.232 +$P\imp Q$ cannot be treated like $\neg P\disj Q$.  Given $P\imp Q$, we may
   2.233 +use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated
   2.234 +use of $P\imp Q$.  If the proof of~$P$ fails then the whole branch of the
   2.235 +proof must be abandoned.  Thus intuitionistic propositional logic requires
   2.236 +backtracking.  
   2.237 +
   2.238 +For an elementary example, consider the intuitionistic proof of $Q$ from
   2.239 +$P\imp Q$ and $(P\imp Q)\imp P$.  The implication $P\imp Q$ is needed
   2.240 +twice:
   2.241 +\[ \infer[({\imp}E)]{Q}{P\imp Q &
   2.242 +       \infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}} 
   2.243 +\]
   2.244 +The theorem prover for intuitionistic logic does not use~\texttt{impE}.\@
   2.245 +Instead, it simplifies implications using derived rules
   2.246 +(Fig.\ts\ref{fol-int-derived}).  It reduces the antecedents of implications
   2.247 +to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$.
   2.248 +The rules \tdx{conj_impE} and \tdx{disj_impE} are 
   2.249 +straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and
   2.250 +$(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp
   2.251 +S$.  The other \ldots{\tt_impE} rules are unsafe; the method requires
   2.252 +backtracking.  All the rules are derived in the same simple manner.
   2.253 +
   2.254 +Dyckhoff has independently discovered similar rules, and (more importantly)
   2.255 +has demonstrated their completeness for propositional
   2.256 +logic~\cite{dyckhoff}.  However, the tactics given below are not complete
   2.257 +for first-order logic because they discard universally quantified
   2.258 +assumptions after a single use.
   2.259 +\begin{ttbox} 
   2.260 +mp_tac              : int -> tactic
   2.261 +eq_mp_tac           : int -> tactic
   2.262 +IntPr.safe_step_tac : int -> tactic
   2.263 +IntPr.safe_tac      :        tactic
   2.264 +IntPr.inst_step_tac : int -> tactic
   2.265 +IntPr.step_tac      : int -> tactic
   2.266 +IntPr.fast_tac      : int -> tactic
   2.267 +IntPr.best_tac      : int -> tactic
   2.268 +\end{ttbox}
   2.269 +Most of these belong to the structure \texttt{IntPr} and resemble the
   2.270 +tactics of Isabelle's classical reasoner.
   2.271 +
   2.272 +\begin{ttdescription}
   2.273 +\item[\ttindexbold{mp_tac} {\it i}] 
   2.274 +attempts to use \tdx{notE} or \tdx{impE} within the assumptions in
   2.275 +subgoal $i$.  For each assumption of the form $\neg P$ or $P\imp Q$, it
   2.276 +searches for another assumption unifiable with~$P$.  By
   2.277 +contradiction with $\neg P$ it can solve the subgoal completely; by Modus
   2.278 +Ponens it can replace the assumption $P\imp Q$ by $Q$.  The tactic can
   2.279 +produce multiple outcomes, enumerating all suitable pairs of assumptions.
   2.280 +
   2.281 +\item[\ttindexbold{eq_mp_tac} {\it i}] 
   2.282 +is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
   2.283 +is safe.
   2.284 +
   2.285 +\item[\ttindexbold{IntPr.safe_step_tac} $i$] performs a safe step on
   2.286 +subgoal~$i$.  This may include proof by assumption or Modus Ponens (taking
   2.287 +care not to instantiate unknowns), or \texttt{hyp_subst_tac}. 
   2.288 +
   2.289 +\item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all 
   2.290 +subgoals.  It is deterministic, with at most one outcome.
   2.291 +
   2.292 +\item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac},
   2.293 +but allows unknowns to be instantiated.
   2.294 +
   2.295 +\item[\ttindexbold{IntPr.step_tac} $i$] tries \texttt{safe_tac} or {\tt
   2.296 +    inst_step_tac}, or applies an unsafe rule.  This is the basic step of
   2.297 +  the intuitionistic proof procedure.
   2.298 +
   2.299 +\item[\ttindexbold{IntPr.fast_tac} $i$] applies \texttt{step_tac}, using
   2.300 +depth-first search, to solve subgoal~$i$.
   2.301 +
   2.302 +\item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using
   2.303 +best-first search (guided by the size of the proof state) to solve subgoal~$i$.
   2.304 +\end{ttdescription}
   2.305 +Here are some of the theorems that \texttt{IntPr.fast_tac} proves
   2.306 +automatically.  The latter three date from {\it Principia Mathematica}
   2.307 +(*11.53, *11.55, *11.61)~\cite{principia}.
   2.308 +\begin{ttbox}
   2.309 +~~P & ~~(P --> Q) --> ~~Q
   2.310 +(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))
   2.311 +(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))
   2.312 +(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))
   2.313 +\end{ttbox}
   2.314 +
   2.315 +
   2.316 +
   2.317 +\begin{figure} 
   2.318 +\begin{ttbox}
   2.319 +\tdx{excluded_middle}    ~P | P
   2.320 +
   2.321 +\tdx{disjCI}    (~Q ==> P) ==> P|Q
   2.322 +\tdx{exCI}      (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)
   2.323 +\tdx{impCE}     [| P-->Q; ~P ==> R; Q ==> R |] ==> R
   2.324 +\tdx{iffCE}     [| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R
   2.325 +\tdx{notnotD}   ~~P ==> P
   2.326 +\tdx{swap}      ~P ==> (~Q ==> P) ==> Q
   2.327 +\end{ttbox}
   2.328 +\caption{Derived rules for classical logic} \label{fol-cla-derived}
   2.329 +\end{figure}
   2.330 +
   2.331 +
   2.332 +\section{Classical proof procedures} \label{fol-cla-prover}
   2.333 +The classical theory, \thydx{FOL}, consists of intuitionistic logic plus
   2.334 +the rule
   2.335 +$$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$
   2.336 +\noindent
   2.337 +Natural deduction in classical logic is not really all that natural.
   2.338 +{\FOL} derives classical introduction rules for $\disj$ and~$\exists$, as
   2.339 +well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
   2.340 +rule (see Fig.\ts\ref{fol-cla-derived}).
   2.341 +
   2.342 +The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and {\tt
   2.343 +Best_tac} refer to the default claset (\texttt{claset()}), which works for most
   2.344 +purposes.  Named clasets include \ttindexbold{prop_cs}, which includes the
   2.345 +propositional rules, and \ttindexbold{FOL_cs}, which also includes quantifier
   2.346 +rules.  See the file \texttt{FOL/cladata.ML} for lists of the
   2.347 +classical rules, and 
   2.348 +\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
   2.349 +        {Chap.\ts\ref{chap:classical}} 
   2.350 +for more discussion of classical proof methods.
   2.351 +
   2.352 +
   2.353 +\section{An intuitionistic example}
   2.354 +Here is a session similar to one in {\em Logic and Computation}
   2.355 +\cite[pages~222--3]{paulson87}.  Isabelle treats quantifiers differently
   2.356 +from {\sc lcf}-based theorem provers such as {\sc hol}.  
   2.357 +
   2.358 +First, we specify that we are working in intuitionistic logic:
   2.359 +\begin{ttbox}
   2.360 +context IFOL.thy;
   2.361 +\end{ttbox}
   2.362 +The proof begins by entering the goal, then applying the rule $({\imp}I)$.
   2.363 +\begin{ttbox}
   2.364 +Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
   2.365 +{\out Level 0}
   2.366 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.367 +{\out  1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.368 +\ttbreak
   2.369 +by (resolve_tac [impI] 1);
   2.370 +{\out Level 1}
   2.371 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.372 +{\out  1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y)}
   2.373 +\end{ttbox}
   2.374 +In this example, we shall never have more than one subgoal.  Applying
   2.375 +$({\imp}I)$ replaces~\verb|-->| by~\verb|==>|, making
   2.376 +\(\ex{y}\all{x}Q(x,y)\) an assumption.  We have the choice of
   2.377 +$({\exists}E)$ and $({\forall}I)$; let us try the latter.
   2.378 +\begin{ttbox}
   2.379 +by (resolve_tac [allI] 1);
   2.380 +{\out Level 2}
   2.381 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.382 +{\out  1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
   2.383 +\end{ttbox}
   2.384 +Applying $({\forall}I)$ replaces the \texttt{ALL~x} by \hbox{\tt!!x},
   2.385 +changing the universal quantifier from object~($\forall$) to
   2.386 +meta~($\Forall$).  The bound variable is a {\bf parameter} of the
   2.387 +subgoal.  We now must choose between $({\exists}I)$ and $({\exists}E)$.  What
   2.388 +happens if the wrong rule is chosen?
   2.389 +\begin{ttbox}
   2.390 +by (resolve_tac [exI] 1);
   2.391 +{\out Level 3}
   2.392 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.393 +{\out  1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
   2.394 +\end{ttbox}
   2.395 +The new subgoal~1 contains the function variable {\tt?y2}.  Instantiating
   2.396 +{\tt?y2} can replace~{\tt?y2(x)} by a term containing~\texttt{x}, even
   2.397 +though~\texttt{x} is a bound variable.  Now we analyse the assumption
   2.398 +\(\exists y.\forall x. Q(x,y)\) using elimination rules:
   2.399 +\begin{ttbox}
   2.400 +by (eresolve_tac [exE] 1);
   2.401 +{\out Level 4}
   2.402 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.403 +{\out  1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
   2.404 +\end{ttbox}
   2.405 +Applying $(\exists E)$ has produced the parameter \texttt{y} and stripped the
   2.406 +existential quantifier from the assumption.  But the subgoal is unprovable:
   2.407 +there is no way to unify \texttt{?y2(x)} with the bound variable~\texttt{y}.
   2.408 +Using \texttt{choplev} we can return to the critical point.  This time we
   2.409 +apply $({\exists}E)$:
   2.410 +\begin{ttbox}
   2.411 +choplev 2;
   2.412 +{\out Level 2}
   2.413 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.414 +{\out  1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
   2.415 +\ttbreak
   2.416 +by (eresolve_tac [exE] 1);
   2.417 +{\out Level 3}
   2.418 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.419 +{\out  1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
   2.420 +\end{ttbox}
   2.421 +We now have two parameters and no scheme variables.  Applying
   2.422 +$({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are
   2.423 +applied to those parameters.  Parameters should be produced early, as this
   2.424 +example demonstrates.
   2.425 +\begin{ttbox}
   2.426 +by (resolve_tac [exI] 1);
   2.427 +{\out Level 4}
   2.428 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.429 +{\out  1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y))}
   2.430 +\ttbreak
   2.431 +by (eresolve_tac [allE] 1);
   2.432 +{\out Level 5}
   2.433 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.434 +{\out  1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))}
   2.435 +\end{ttbox}
   2.436 +The subgoal has variables \texttt{?y3} and \texttt{?x4} applied to both
   2.437 +parameters.  The obvious projection functions unify {\tt?x4(x,y)} with~{\tt
   2.438 +x} and \verb|?y3(x,y)| with~\texttt{y}.
   2.439 +\begin{ttbox}
   2.440 +by (assume_tac 1);
   2.441 +{\out Level 6}
   2.442 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.443 +{\out No subgoals!}
   2.444 +\end{ttbox}
   2.445 +The theorem was proved in six tactic steps, not counting the abandoned
   2.446 +ones.  But proof checking is tedious; \ttindex{IntPr.fast_tac} proves the
   2.447 +theorem in one step.
   2.448 +\begin{ttbox}
   2.449 +Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
   2.450 +{\out Level 0}
   2.451 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.452 +{\out  1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.453 +by (IntPr.fast_tac 1);
   2.454 +{\out Level 1}
   2.455 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   2.456 +{\out No subgoals!}
   2.457 +\end{ttbox}
   2.458 +
   2.459 +
   2.460 +\section{An example of intuitionistic negation}
   2.461 +The following example demonstrates the specialized forms of implication
   2.462 +elimination.  Even propositional formulae can be difficult to prove from
   2.463 +the basic rules; the specialized rules help considerably.  
   2.464 +
   2.465 +Propositional examples are easy to invent.  As Dummett notes~\cite[page
   2.466 +28]{dummett}, $\neg P$ is classically provable if and only if it is
   2.467 +intuitionistically provable;  therefore, $P$ is classically provable if and
   2.468 +only if $\neg\neg P$ is intuitionistically provable.%
   2.469 +\footnote{Of course this holds only for propositional logic, not if $P$ is
   2.470 +  allowed to contain quantifiers.} Proving $\neg\neg P$ intuitionistically is
   2.471 +much harder than proving~$P$ classically.
   2.472 +
   2.473 +Our example is the double negation of the classical tautology $(P\imp
   2.474 +Q)\disj (Q\imp P)$.  When stating the goal, we command Isabelle to expand
   2.475 +negations to implications using the definition $\neg P\equiv P\imp\bot$.
   2.476 +This allows use of the special implication rules.
   2.477 +\begin{ttbox}
   2.478 +Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))";
   2.479 +{\out Level 0}
   2.480 +{\out ~ ~ ((P --> Q) | (Q --> P))}
   2.481 +{\out  1. ((P --> Q) | (Q --> P) --> False) --> False}
   2.482 +\end{ttbox}
   2.483 +The first step is trivial.
   2.484 +\begin{ttbox}
   2.485 +by (resolve_tac [impI] 1);
   2.486 +{\out Level 1}
   2.487 +{\out ~ ~ ((P --> Q) | (Q --> P))}
   2.488 +{\out  1. (P --> Q) | (Q --> P) --> False ==> False}
   2.489 +\end{ttbox}
   2.490 +By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but
   2.491 +that formula is not a theorem of intuitionistic logic.  Instead we apply
   2.492 +the specialized implication rule \tdx{disj_impE}.  It splits the
   2.493 +assumption into two assumptions, one for each disjunct.
   2.494 +\begin{ttbox}
   2.495 +by (eresolve_tac [disj_impE] 1);
   2.496 +{\out Level 2}
   2.497 +{\out ~ ~ ((P --> Q) | (Q --> P))}
   2.498 +{\out  1. [| (P --> Q) --> False; (Q --> P) --> False |] ==> False}
   2.499 +\end{ttbox}
   2.500 +We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but
   2.501 +their negations are inconsistent.  Applying \tdx{imp_impE} breaks down
   2.502 +the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new
   2.503 +assumptions~$P$ and~$\neg Q$.
   2.504 +\begin{ttbox}
   2.505 +by (eresolve_tac [imp_impE] 1);
   2.506 +{\out Level 3}
   2.507 +{\out ~ ~ ((P --> Q) | (Q --> P))}
   2.508 +{\out  1. [| (Q --> P) --> False; P; Q --> False |] ==> Q}
   2.509 +{\out  2. [| (Q --> P) --> False; False |] ==> False}
   2.510 +\end{ttbox}
   2.511 +Subgoal~2 holds trivially; let us ignore it and continue working on
   2.512 +subgoal~1.  Thanks to the assumption~$P$, we could prove $Q\imp P$;
   2.513 +applying \tdx{imp_impE} is simpler.
   2.514 +\begin{ttbox}
   2.515 +by (eresolve_tac [imp_impE] 1);
   2.516 +{\out Level 4}
   2.517 +{\out ~ ~ ((P --> Q) | (Q --> P))}
   2.518 +{\out  1. [| P; Q --> False; Q; P --> False |] ==> P}
   2.519 +{\out  2. [| P; Q --> False; False |] ==> Q}
   2.520 +{\out  3. [| (Q --> P) --> False; False |] ==> False}
   2.521 +\end{ttbox}
   2.522 +The three subgoals are all trivial.
   2.523 +\begin{ttbox}
   2.524 +by (REPEAT (eresolve_tac [FalseE] 2));
   2.525 +{\out Level 5}
   2.526 +{\out ~ ~ ((P --> Q) | (Q --> P))}
   2.527 +{\out  1. [| P; Q --> False; Q; P --> False |] ==> P}
   2.528 +\ttbreak
   2.529 +by (assume_tac 1);
   2.530 +{\out Level 6}
   2.531 +{\out ~ ~ ((P --> Q) | (Q --> P))}
   2.532 +{\out No subgoals!}
   2.533 +\end{ttbox}
   2.534 +This proof is also trivial for \texttt{IntPr.fast_tac}.
   2.535 +
   2.536 +
   2.537 +\section{A classical example} \label{fol-cla-example}
   2.538 +To illustrate classical logic, we shall prove the theorem
   2.539 +$\ex{y}\all{x}P(y)\imp P(x)$.  Informally, the theorem can be proved as
   2.540 +follows.  Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
   2.541 +$\all{x}P(x)$ is true.  Either way the theorem holds.  First, we switch to
   2.542 +classical logic:
   2.543 +\begin{ttbox}
   2.544 +context FOL.thy;
   2.545 +\end{ttbox}
   2.546 +
   2.547 +The formal proof does not conform in any obvious way to the sketch given
   2.548 +above.  The key inference is the first one, \tdx{exCI}; this classical
   2.549 +version of~$(\exists I)$ allows multiple instantiation of the quantifier.
   2.550 +\begin{ttbox}
   2.551 +Goal "EX y. ALL x. P(y)-->P(x)";
   2.552 +{\out Level 0}
   2.553 +{\out EX y. ALL x. P(y) --> P(x)}
   2.554 +{\out  1. EX y. ALL x. P(y) --> P(x)}
   2.555 +\ttbreak
   2.556 +by (resolve_tac [exCI] 1);
   2.557 +{\out Level 1}
   2.558 +{\out EX y. ALL x. P(y) --> P(x)}
   2.559 +{\out  1. ALL y. ~ (ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)}
   2.560 +\end{ttbox}
   2.561 +We can either exhibit a term {\tt?a} to satisfy the conclusion of
   2.562 +subgoal~1, or produce a contradiction from the assumption.  The next
   2.563 +steps are routine.
   2.564 +\begin{ttbox}
   2.565 +by (resolve_tac [allI] 1);
   2.566 +{\out Level 2}
   2.567 +{\out EX y. ALL x. P(y) --> P(x)}
   2.568 +{\out  1. !!x. ALL y. ~ (ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)}
   2.569 +\ttbreak
   2.570 +by (resolve_tac [impI] 1);
   2.571 +{\out Level 3}
   2.572 +{\out EX y. ALL x. P(y) --> P(x)}
   2.573 +{\out  1. !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)}
   2.574 +\end{ttbox}
   2.575 +By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$
   2.576 +in effect applies~$(\exists I)$ again.
   2.577 +\begin{ttbox}
   2.578 +by (eresolve_tac [allE] 1);
   2.579 +{\out Level 4}
   2.580 +{\out EX y. ALL x. P(y) --> P(x)}
   2.581 +{\out  1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)}
   2.582 +\end{ttbox}
   2.583 +In classical logic, a negated assumption is equivalent to a conclusion.  To
   2.584 +get this effect, we create a swapped version of~$(\forall I)$ and apply it
   2.585 +using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall
   2.586 +I)$ using \ttindex{swap_res_tac}.
   2.587 +\begin{ttbox}
   2.588 +allI RSN (2,swap);
   2.589 +{\out val it = "[| ~ (ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm}
   2.590 +by (eresolve_tac [it] 1);
   2.591 +{\out Level 5}
   2.592 +{\out EX y. ALL x. P(y) --> P(x)}
   2.593 +{\out  1. !!x xa. [| P(?a); ~ P(x) |] ==> P(?y3(x)) --> P(xa)}
   2.594 +\end{ttbox}
   2.595 +The previous conclusion, \texttt{P(x)}, has become a negated assumption.
   2.596 +\begin{ttbox}
   2.597 +by (resolve_tac [impI] 1);
   2.598 +{\out Level 6}
   2.599 +{\out EX y. ALL x. P(y) --> P(x)}
   2.600 +{\out  1. !!x xa. [| P(?a); ~ P(x); P(?y3(x)) |] ==> P(xa)}
   2.601 +\end{ttbox}
   2.602 +The subgoal has three assumptions.  We produce a contradiction between the
   2.603 +\index{assumptions!contradictory} assumptions~\verb|~P(x)| and~{\tt
   2.604 +  P(?y3(x))}.  The proof never instantiates the unknown~{\tt?a}.
   2.605 +\begin{ttbox}
   2.606 +by (eresolve_tac [notE] 1);
   2.607 +{\out Level 7}
   2.608 +{\out EX y. ALL x. P(y) --> P(x)}
   2.609 +{\out  1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)}
   2.610 +\ttbreak
   2.611 +by (assume_tac 1);
   2.612 +{\out Level 8}
   2.613 +{\out EX y. ALL x. P(y) --> P(x)}
   2.614 +{\out No subgoals!}
   2.615 +\end{ttbox}
   2.616 +The civilised way to prove this theorem is through \ttindex{Blast_tac},
   2.617 +which automatically uses the classical version of~$(\exists I)$:
   2.618 +\begin{ttbox}
   2.619 +Goal "EX y. ALL x. P(y)-->P(x)";
   2.620 +{\out Level 0}
   2.621 +{\out EX y. ALL x. P(y) --> P(x)}
   2.622 +{\out  1. EX y. ALL x. P(y) --> P(x)}
   2.623 +by (Blast_tac 1);
   2.624 +{\out Depth = 0}
   2.625 +{\out Depth = 1}
   2.626 +{\out Depth = 2}
   2.627 +{\out Level 1}
   2.628 +{\out EX y. ALL x. P(y) --> P(x)}
   2.629 +{\out No subgoals!}
   2.630 +\end{ttbox}
   2.631 +If this theorem seems counterintuitive, then perhaps you are an
   2.632 +intuitionist.  In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$
   2.633 +requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$,
   2.634 +which we cannot do without further knowledge about~$P$.
   2.635 +
   2.636 +
   2.637 +\section{Derived rules and the classical tactics}
   2.638 +Classical first-order logic can be extended with the propositional
   2.639 +connective $if(P,Q,R)$, where 
   2.640 +$$ if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if) $$
   2.641 +Theorems about $if$ can be proved by treating this as an abbreviation,
   2.642 +replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals.  But
   2.643 +this duplicates~$P$, causing an exponential blowup and an unreadable
   2.644 +formula.  Introducing further abbreviations makes the problem worse.
   2.645 +
   2.646 +Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$
   2.647 +directly, without reference to its definition.  The simple identity
   2.648 +\[ if(P,Q,R) \,\bimp\, (P\imp Q)\conj (\neg P\imp R) \]
   2.649 +suggests that the
   2.650 +$if$-introduction rule should be
   2.651 +\[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]}  &  \infer*{R}{[\neg P]}} \]
   2.652 +The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the
   2.653 +elimination rules for~$\disj$ and~$\conj$.
   2.654 +\[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]}
   2.655 +                                  & \infer*{S}{[\neg P,R]}} 
   2.656 +\]
   2.657 +Having made these plans, we get down to work with Isabelle.  The theory of
   2.658 +classical logic, \texttt{FOL}, is extended with the constant
   2.659 +$if::[o,o,o]\To o$.  The axiom \tdx{if_def} asserts the
   2.660 +equation~$(if)$.
   2.661 +\begin{ttbox}
   2.662 +If = FOL +
   2.663 +consts  if     :: [o,o,o]=>o
   2.664 +rules   if_def "if(P,Q,R) == P&Q | ~P&R"
   2.665 +end
   2.666 +\end{ttbox}
   2.667 +We create the file \texttt{If.thy} containing these declarations.  (This file
   2.668 +is on directory \texttt{FOL/ex} in the Isabelle distribution.)  Typing
   2.669 +\begin{ttbox}
   2.670 +use_thy "If";  
   2.671 +\end{ttbox}
   2.672 +loads that theory and sets it to be the current context.
   2.673 +
   2.674 +
   2.675 +\subsection{Deriving the introduction rule}
   2.676 +
   2.677 +The derivations of the introduction and elimination rules demonstrate the
   2.678 +methods for rewriting with definitions.  Classical reasoning is required,
   2.679 +so we use \texttt{blast_tac}.
   2.680 +
   2.681 +The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$,
   2.682 +concludes $if(P,Q,R)$.  We propose the conclusion as the main goal
   2.683 +using~\ttindex{Goalw}, which uses \texttt{if_def} to rewrite occurrences
   2.684 +of $if$ in the subgoal.
   2.685 +\begin{ttbox}
   2.686 +val prems = Goalw [if_def]
   2.687 +    "[| P ==> Q; ~ P ==> R |] ==> if(P,Q,R)";
   2.688 +{\out Level 0}
   2.689 +{\out if(P,Q,R)}
   2.690 +{\out  1. P & Q | ~ P & R}
   2.691 +\end{ttbox}
   2.692 +The premises (bound to the {\ML} variable \texttt{prems}) are passed as
   2.693 +introduction rules to \ttindex{blast_tac}.  Remember that \texttt{claset()} refers
   2.694 +to the default classical set.
   2.695 +\begin{ttbox}
   2.696 +by (blast_tac (claset() addIs prems) 1);
   2.697 +{\out Level 1}
   2.698 +{\out if(P,Q,R)}
   2.699 +{\out No subgoals!}
   2.700 +qed "ifI";
   2.701 +\end{ttbox}
   2.702 +
   2.703 +
   2.704 +\subsection{Deriving the elimination rule}
   2.705 +The elimination rule has three premises, two of which are themselves rules.
   2.706 +The conclusion is simply $S$.
   2.707 +\begin{ttbox}
   2.708 +val major::prems = Goalw [if_def]
   2.709 +   "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~ P; R |] ==> S |] ==> S";
   2.710 +{\out Level 0}
   2.711 +{\out S}
   2.712 +{\out  1. S}
   2.713 +\end{ttbox}
   2.714 +The major premise contains an occurrence of~$if$, but the version returned
   2.715 +by \ttindex{Goalw} (and bound to the {\ML} variable~\texttt{major}) has the
   2.716 +definition expanded.  Now \ttindex{cut_facts_tac} inserts~\texttt{major} as an
   2.717 +assumption in the subgoal, so that \ttindex{blast_tac} can break it down.
   2.718 +\begin{ttbox}
   2.719 +by (cut_facts_tac [major] 1);
   2.720 +{\out Level 1}
   2.721 +{\out S}
   2.722 +{\out  1. P & Q | ~ P & R ==> S}
   2.723 +\ttbreak
   2.724 +by (blast_tac (claset() addIs prems) 1);
   2.725 +{\out Level 2}
   2.726 +{\out S}
   2.727 +{\out No subgoals!}
   2.728 +qed "ifE";
   2.729 +\end{ttbox}
   2.730 +As you may recall from
   2.731 +\iflabelundefined{definitions}{{\em Introduction to Isabelle}}%
   2.732 +        {\S\ref{definitions}}, there are other
   2.733 +ways of treating definitions when deriving a rule.  We can start the
   2.734 +proof using \texttt{Goal}, which does not expand definitions, instead of
   2.735 +\texttt{Goalw}.  We can use \ttindex{rew_tac}
   2.736 +to expand definitions in the subgoals---perhaps after calling
   2.737 +\ttindex{cut_facts_tac} to insert the rule's premises.  We can use
   2.738 +\ttindex{rewrite_rule}, which is a meta-inference rule, to expand
   2.739 +definitions in the premises directly.
   2.740 +
   2.741 +
   2.742 +\subsection{Using the derived rules}
   2.743 +The rules just derived have been saved with the {\ML} names \tdx{ifI}
   2.744 +and~\tdx{ifE}.  They permit natural proofs of theorems such as the
   2.745 +following:
   2.746 +\begin{eqnarray*}
   2.747 +    if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\
   2.748 +    if(if(P,Q,R), A, B)         & \bimp & if(P,if(Q,A,B),if(R,A,B))
   2.749 +\end{eqnarray*}
   2.750 +Proofs also require the classical reasoning rules and the $\bimp$
   2.751 +introduction rule (called~\tdx{iffI}: do not confuse with~\texttt{ifI}). 
   2.752 +
   2.753 +To display the $if$-rules in action, let us analyse a proof step by step.
   2.754 +\begin{ttbox}
   2.755 +Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
   2.756 +{\out Level 0}
   2.757 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   2.758 +{\out  1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   2.759 +\ttbreak
   2.760 +by (resolve_tac [iffI] 1);
   2.761 +{\out Level 1}
   2.762 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   2.763 +{\out  1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))}
   2.764 +{\out  2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
   2.765 +\end{ttbox}
   2.766 +The $if$-elimination rule can be applied twice in succession.
   2.767 +\begin{ttbox}
   2.768 +by (eresolve_tac [ifE] 1);
   2.769 +{\out Level 2}
   2.770 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   2.771 +{\out  1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))}
   2.772 +{\out  2. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
   2.773 +{\out  3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
   2.774 +\ttbreak
   2.775 +by (eresolve_tac [ifE] 1);
   2.776 +{\out Level 3}
   2.777 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   2.778 +{\out  1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))}
   2.779 +{\out  2. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
   2.780 +{\out  3. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
   2.781 +{\out  4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
   2.782 +\end{ttbox}
   2.783 +%
   2.784 +In the first two subgoals, all assumptions have been reduced to atoms.  Now
   2.785 +$if$-introduction can be applied.  Observe how the $if$-rules break down
   2.786 +occurrences of $if$ when they become the outermost connective.
   2.787 +\begin{ttbox}
   2.788 +by (resolve_tac [ifI] 1);
   2.789 +{\out Level 4}
   2.790 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   2.791 +{\out  1. [| P; Q; A; Q |] ==> if(P,A,C)}
   2.792 +{\out  2. [| P; Q; A; ~ Q |] ==> if(P,B,D)}
   2.793 +{\out  3. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
   2.794 +{\out  4. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
   2.795 +{\out  5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
   2.796 +\ttbreak
   2.797 +by (resolve_tac [ifI] 1);
   2.798 +{\out Level 5}
   2.799 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   2.800 +{\out  1. [| P; Q; A; Q; P |] ==> A}
   2.801 +{\out  2. [| P; Q; A; Q; ~ P |] ==> C}
   2.802 +{\out  3. [| P; Q; A; ~ Q |] ==> if(P,B,D)}
   2.803 +{\out  4. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
   2.804 +{\out  5. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
   2.805 +{\out  6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
   2.806 +\end{ttbox}
   2.807 +Where do we stand?  The first subgoal holds by assumption; the second and
   2.808 +third, by contradiction.  This is getting tedious.  We could use the classical
   2.809 +reasoner, but first let us extend the default claset with the derived rules
   2.810 +for~$if$.
   2.811 +\begin{ttbox}
   2.812 +AddSIs [ifI];
   2.813 +AddSEs [ifE];
   2.814 +\end{ttbox}
   2.815 +Now we can revert to the
   2.816 +initial proof state and let \ttindex{blast_tac} solve it.  
   2.817 +\begin{ttbox}
   2.818 +choplev 0;
   2.819 +{\out Level 0}
   2.820 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   2.821 +{\out  1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   2.822 +by (Blast_tac 1);
   2.823 +{\out Level 1}
   2.824 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   2.825 +{\out No subgoals!}
   2.826 +\end{ttbox}
   2.827 +This tactic also solves the other example.
   2.828 +\begin{ttbox}
   2.829 +Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
   2.830 +{\out Level 0}
   2.831 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   2.832 +{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   2.833 +\ttbreak
   2.834 +by (Blast_tac 1);
   2.835 +{\out Level 1}
   2.836 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   2.837 +{\out No subgoals!}
   2.838 +\end{ttbox}
   2.839 +
   2.840 +
   2.841 +\subsection{Derived rules versus definitions}
   2.842 +Dispensing with the derived rules, we can treat $if$ as an
   2.843 +abbreviation, and let \ttindex{blast_tac} prove the expanded formula.  Let
   2.844 +us redo the previous proof:
   2.845 +\begin{ttbox}
   2.846 +choplev 0;
   2.847 +{\out Level 0}
   2.848 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   2.849 +{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   2.850 +\end{ttbox}
   2.851 +This time, simply unfold using the definition of $if$:
   2.852 +\begin{ttbox}
   2.853 +by (rewtac if_def);
   2.854 +{\out Level 1}
   2.855 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   2.856 +{\out  1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
   2.857 +{\out     P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)}
   2.858 +\end{ttbox}
   2.859 +We are left with a subgoal in pure first-order logic, which is why the 
   2.860 +classical reasoner can prove it given \texttt{FOL_cs} alone.  (We could, of 
   2.861 +course, have used \texttt{Blast_tac}.)
   2.862 +\begin{ttbox}
   2.863 +by (blast_tac FOL_cs 1);
   2.864 +{\out Level 2}
   2.865 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   2.866 +{\out No subgoals!}
   2.867 +\end{ttbox}
   2.868 +Expanding definitions reduces the extended logic to the base logic.  This
   2.869 +approach has its merits --- especially if the prover for the base logic is
   2.870 +good --- but can be slow.  In these examples, proofs using the default
   2.871 +claset (which includes the derived rules) run about six times faster 
   2.872 +than proofs using \texttt{FOL_cs}.
   2.873 +
   2.874 +Expanding definitions also complicates error diagnosis.  Suppose we are having
   2.875 +difficulties in proving some goal.  If by expanding definitions we have
   2.876 +made it unreadable, then we have little hope of diagnosing the problem.
   2.877 +
   2.878 +Attempts at program verification often yield invalid assertions.
   2.879 +Let us try to prove one:
   2.880 +\begin{ttbox}
   2.881 +Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
   2.882 +{\out Level 0}
   2.883 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   2.884 +{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   2.885 +by (Blast_tac 1);
   2.886 +{\out by: tactic failed}
   2.887 +\end{ttbox}
   2.888 +This failure message is uninformative, but we can get a closer look at the
   2.889 +situation by applying \ttindex{Step_tac}.
   2.890 +\begin{ttbox}
   2.891 +by (REPEAT (Step_tac 1));
   2.892 +{\out Level 1}
   2.893 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   2.894 +{\out  1. [| A; ~ P; R; ~ P; R |] ==> B}
   2.895 +{\out  2. [| B; ~ P; ~ R; ~ P; ~ R |] ==> A}
   2.896 +{\out  3. [| ~ P; R; B; ~ P; R |] ==> A}
   2.897 +{\out  4. [| ~ P; ~ R; A; ~ B; ~ P |] ==> R}
   2.898 +\end{ttbox}
   2.899 +Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false
   2.900 +while~$R$ and~$A$ are true.  This truth assignment reduces the main goal to
   2.901 +$true\bimp false$, which is of course invalid.
   2.902 +
   2.903 +We can repeat this analysis by expanding definitions, using just
   2.904 +the rules of {\FOL}:
   2.905 +\begin{ttbox}
   2.906 +choplev 0;
   2.907 +{\out Level 0}
   2.908 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   2.909 +{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   2.910 +\ttbreak
   2.911 +by (rewtac if_def);
   2.912 +{\out Level 1}
   2.913 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   2.914 +{\out  1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
   2.915 +{\out     P & (Q & A | ~ Q & B) | ~ P & (R & B | ~ R & A)}
   2.916 +by (blast_tac FOL_cs 1);
   2.917 +{\out by: tactic failed}
   2.918 +\end{ttbox}
   2.919 +Again we apply \ttindex{step_tac}:
   2.920 +\begin{ttbox}
   2.921 +by (REPEAT (step_tac FOL_cs 1));
   2.922 +{\out Level 2}
   2.923 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   2.924 +{\out  1. [| A; ~ P; R; ~ P; R; ~ False |] ==> B}
   2.925 +{\out  2. [| A; ~ P; R; R; ~ False; ~ B; ~ B |] ==> Q}
   2.926 +{\out  3. [| B; ~ P; ~ R; ~ P; ~ A |] ==> R}
   2.927 +{\out  4. [| B; ~ P; ~ R; ~ Q; ~ A |] ==> R}
   2.928 +{\out  5. [| B; ~ R; ~ P; ~ A; ~ R; Q; ~ False |] ==> A}
   2.929 +{\out  6. [| ~ P; R; B; ~ P; R; ~ False |] ==> A}
   2.930 +{\out  7. [| ~ P; ~ R; A; ~ B; ~ R |] ==> P}
   2.931 +{\out  8. [| ~ P; ~ R; A; ~ B; ~ R |] ==> Q}
   2.932 +\end{ttbox}
   2.933 +Subgoal~1 yields the same countermodel as before.  But each proof step has
   2.934 +taken six times as long, and the final result contains twice as many subgoals.
   2.935 +
   2.936 +Expanding definitions causes a great increase in complexity.  This is why
   2.937 +the classical prover has been designed to accept derived rules.
   2.938 +
   2.939 +\index{first-order logic|)}
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/ZF/Makefile	Wed Jan 13 16:36:36 1999 +0100
     3.3 @@ -0,0 +1,34 @@
     3.4 +#  $Id$
     3.5 +#########################################################################
     3.6 +#									#
     3.7 +#	Makefile for the report "Isabelle's Logics: FOL and ZF"		#
     3.8 +#									#
     3.9 +#########################################################################
    3.10 +
    3.11 +
    3.12 +FILES =  logics-ZF.tex ../Logics/syntax.tex FOL.tex ZF.tex\
    3.13 +	 ../rail.sty ../proof.sty ../iman.sty ../extra.sty
    3.14 +
    3.15 +logics-ZF.dvi.gz:   $(FILES) 
    3.16 +	test -r isabelle.eps || ln -s ../gfx/isabelle.eps .
    3.17 +	-rm logics-ZF.dvi*
    3.18 +	latex logics-ZF
    3.19 +	rail logics-ZF
    3.20 +	bibtex logics-ZF
    3.21 +	latex logics-ZF
    3.22 +	latex logics-ZF
    3.23 +	../sedindex logics-ZF
    3.24 +	latex logics-ZF
    3.25 +	gzip -f logics-ZF.dvi
    3.26 +
    3.27 +dist:   $(FILES) 
    3.28 +	test -r isabelle.eps || ln -s ../gfx/isabelle.eps .
    3.29 +	-rm logics-ZF.dvi*
    3.30 +	latex logics-ZF
    3.31 +	latex logics-ZF
    3.32 +	../sedindex logics-ZF
    3.33 +	latex logics-ZF
    3.34 +
    3.35 +clean:
    3.36 +	@rm *.aux *.log *.toc *.idx *.rai
    3.37 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/ZF/ZF-eg.txt	Wed Jan 13 16:36:36 1999 +0100
     4.3 @@ -0,0 +1,230 @@
     4.4 +(**** ZF examples ****)
     4.5 +
     4.6 +Pretty.setmargin 72;  (*existing macros just allow this margin*)
     4.7 +print_depth 0;
     4.8 +
     4.9 +(*** Powerset example ***)
    4.10 +
    4.11 +val [prem] = goal ZF.thy "A<=B  ==>  Pow(A) <= Pow(B)";
    4.12 +by (resolve_tac [subsetI] 1);
    4.13 +by (resolve_tac [PowI] 1);
    4.14 +by (dresolve_tac [PowD] 1);
    4.15 +by (eresolve_tac [subset_trans] 1);
    4.16 +by (resolve_tac [prem] 1);
    4.17 +val Pow_mono = result();
    4.18 +
    4.19 +goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
    4.20 +by (resolve_tac [equalityI] 1);
    4.21 +by (resolve_tac [Int_greatest] 1);
    4.22 +by (resolve_tac [Int_lower1 RS Pow_mono] 1);
    4.23 +by (resolve_tac [Int_lower2 RS Pow_mono] 1);
    4.24 +by (resolve_tac [subsetI] 1);
    4.25 +by (eresolve_tac [IntE] 1);
    4.26 +by (resolve_tac [PowI] 1);
    4.27 +by (REPEAT (dresolve_tac [PowD] 1));
    4.28 +by (resolve_tac [Int_greatest] 1);
    4.29 +by (REPEAT (assume_tac 1));
    4.30 +choplev 0;
    4.31 +by (fast_tac (ZF_cs addIs [equalityI]) 1);
    4.32 +
    4.33 +Goal "C<=D ==> Union(C) <= Union(D)";
    4.34 +by (resolve_tac [subsetI] 1);
    4.35 +by (eresolve_tac [UnionE] 1);
    4.36 +by (resolve_tac [UnionI] 1);
    4.37 +by (eresolve_tac [subsetD] 1);
    4.38 +by (assume_tac 1);
    4.39 +by (assume_tac 1);
    4.40 +choplev 0;
    4.41 +by (resolve_tac [Union_least] 1);
    4.42 +by (resolve_tac [Union_upper] 1);
    4.43 +by (eresolve_tac [subsetD] 1);
    4.44 +
    4.45 +
    4.46 +val prems = goal ZF.thy
    4.47 +    "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
    4.48 +\    (f Un g)`a = f`a";
    4.49 +by (resolve_tac [apply_equality] 1);
    4.50 +by (resolve_tac [UnI1] 1);
    4.51 +by (resolve_tac [apply_Pair] 1);
    4.52 +by (resolve_tac prems 1);
    4.53 +by (resolve_tac prems 1);
    4.54 +by (resolve_tac [fun_disjoint_Un] 1);
    4.55 +by (resolve_tac prems 1);
    4.56 +by (resolve_tac prems 1);
    4.57 +by (resolve_tac prems 1);
    4.58 +
    4.59 +
    4.60 +Goal "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
    4.61 +\     (f Un g)`a = f`a";
    4.62 +by (resolve_tac [apply_equality] 1);
    4.63 +by (resolve_tac [UnI1] 1);
    4.64 +by (resolve_tac [apply_Pair] 1);
    4.65 +by (assume_tac 1);
    4.66 +by (assume_tac 1);
    4.67 +by (resolve_tac [fun_disjoint_Un] 1);
    4.68 +by (assume_tac 1);
    4.69 +by (assume_tac 1);
    4.70 +by (assume_tac 1);
    4.71 +
    4.72 +
    4.73 +
    4.74 +
    4.75 +goal ZF.thy "f``(UN x:A. B(x)) = (UN x:A. f``B(x))";
    4.76 +by (resolve_tac [equalityI] 1);
    4.77 +by (resolve_tac [subsetI] 1);
    4.78 +fe imageE;
    4.79 +
    4.80 +
    4.81 +goal ZF.thy "(UN x:C. A(x) Int B) = (UN x:C. A(x))  Int  B";
    4.82 +by (resolve_tac [equalityI] 1);
    4.83 +by (resolve_tac [Int_greatest] 1);
    4.84 +fr UN_mono;
    4.85 +by (resolve_tac [Int_lower1] 1);
    4.86 +fr UN_least;
    4.87 +????
    4.88 +
    4.89 +
    4.90 +> goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
    4.91 +Level 0
    4.92 +Pow(A Int B) = Pow(A) Int Pow(B)
    4.93 + 1. Pow(A Int B) = Pow(A) Int Pow(B)
    4.94 +> by (resolve_tac [equalityI] 1);
    4.95 +Level 1
    4.96 +Pow(A Int B) = Pow(A) Int Pow(B)
    4.97 + 1. Pow(A Int B) <= Pow(A) Int Pow(B)
    4.98 + 2. Pow(A) Int Pow(B) <= Pow(A Int B)
    4.99 +> by (resolve_tac [Int_greatest] 1);
   4.100 +Level 2
   4.101 +Pow(A Int B) = Pow(A) Int Pow(B)
   4.102 + 1. Pow(A Int B) <= Pow(A)
   4.103 + 2. Pow(A Int B) <= Pow(B)
   4.104 + 3. Pow(A) Int Pow(B) <= Pow(A Int B)
   4.105 +> by (resolve_tac [Int_lower1 RS Pow_mono] 1);
   4.106 +Level 3
   4.107 +Pow(A Int B) = Pow(A) Int Pow(B)
   4.108 + 1. Pow(A Int B) <= Pow(B)
   4.109 + 2. Pow(A) Int Pow(B) <= Pow(A Int B)
   4.110 +> by (resolve_tac [Int_lower2 RS Pow_mono] 1);
   4.111 +Level 4
   4.112 +Pow(A Int B) = Pow(A) Int Pow(B)
   4.113 + 1. Pow(A) Int Pow(B) <= Pow(A Int B)
   4.114 +> by (resolve_tac [subsetI] 1);
   4.115 +Level 5
   4.116 +Pow(A Int B) = Pow(A) Int Pow(B)
   4.117 + 1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)
   4.118 +> by (eresolve_tac [IntE] 1);
   4.119 +Level 6
   4.120 +Pow(A Int B) = Pow(A) Int Pow(B)
   4.121 + 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)
   4.122 +> by (resolve_tac [PowI] 1);
   4.123 +Level 7
   4.124 +Pow(A Int B) = Pow(A) Int Pow(B)
   4.125 + 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B
   4.126 +> by (REPEAT (dresolve_tac [PowD] 1));
   4.127 +Level 8
   4.128 +Pow(A Int B) = Pow(A) Int Pow(B)
   4.129 + 1. !!x. [| x <= A; x <= B |] ==> x <= A Int B
   4.130 +> by (resolve_tac [Int_greatest] 1);
   4.131 +Level 9
   4.132 +Pow(A Int B) = Pow(A) Int Pow(B)
   4.133 + 1. !!x. [| x <= A; x <= B |] ==> x <= A
   4.134 + 2. !!x. [| x <= A; x <= B |] ==> x <= B
   4.135 +> by (REPEAT (assume_tac 1));
   4.136 +Level 10
   4.137 +Pow(A Int B) = Pow(A) Int Pow(B)
   4.138 +No subgoals!
   4.139 +> choplev 0;
   4.140 +Level 0
   4.141 +Pow(A Int B) = Pow(A) Int Pow(B)
   4.142 + 1. Pow(A Int B) = Pow(A) Int Pow(B)
   4.143 +> by (fast_tac (ZF_cs addIs [equalityI]) 1);
   4.144 +Level 1
   4.145 +Pow(A Int B) = Pow(A) Int Pow(B)
   4.146 +No subgoals!
   4.147 +
   4.148 +
   4.149 +
   4.150 +
   4.151 +> val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";
   4.152 +Level 0
   4.153 +Union(C) <= Union(D)
   4.154 + 1. Union(C) <= Union(D)
   4.155 +> by (resolve_tac [subsetI] 1);
   4.156 +Level 1
   4.157 +Union(C) <= Union(D)
   4.158 + 1. !!x. x : Union(C) ==> x : Union(D)
   4.159 +> by (eresolve_tac [UnionE] 1);
   4.160 +Level 2
   4.161 +Union(C) <= Union(D)
   4.162 + 1. !!x B. [| x : B; B : C |] ==> x : Union(D)
   4.163 +> by (resolve_tac [UnionI] 1);
   4.164 +Level 3
   4.165 +Union(C) <= Union(D)
   4.166 + 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D
   4.167 + 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)
   4.168 +> by (resolve_tac [prem RS subsetD] 1);
   4.169 +Level 4
   4.170 +Union(C) <= Union(D)
   4.171 + 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C
   4.172 + 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)
   4.173 +> by (assume_tac 1);
   4.174 +Level 5
   4.175 +Union(C) <= Union(D)
   4.176 + 1. !!x B. [| x : B; B : C |] ==> x : B
   4.177 +> by (assume_tac 1);
   4.178 +Level 6
   4.179 +Union(C) <= Union(D)
   4.180 +No subgoals!
   4.181 +
   4.182 +
   4.183 +
   4.184 +> val prems = goal ZF.thy
   4.185 +#     "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
   4.186 +# \    (f Un g)`a = f`a";
   4.187 +Level 0
   4.188 +(f Un g) ` a = f ` a
   4.189 + 1. (f Un g) ` a = f ` a
   4.190 +> by (resolve_tac [apply_equality] 1);
   4.191 +Level 1
   4.192 +(f Un g) ` a = f ` a
   4.193 + 1. <a,f ` a> : f Un g
   4.194 + 2. f Un g : (PROD x:?A. ?B(x))
   4.195 +> by (resolve_tac [UnI1] 1);
   4.196 +Level 2
   4.197 +(f Un g) ` a = f ` a
   4.198 + 1. <a,f ` a> : f
   4.199 + 2. f Un g : (PROD x:?A. ?B(x))
   4.200 +> by (resolve_tac [apply_Pair] 1);
   4.201 +Level 3
   4.202 +(f Un g) ` a = f ` a
   4.203 + 1. f : (PROD x:?A2. ?B2(x))
   4.204 + 2. a : ?A2
   4.205 + 3. f Un g : (PROD x:?A. ?B(x))
   4.206 +> by (resolve_tac prems 1);
   4.207 +Level 4
   4.208 +(f Un g) ` a = f ` a
   4.209 + 1. a : A
   4.210 + 2. f Un g : (PROD x:?A. ?B(x))
   4.211 +> by (resolve_tac prems 1);
   4.212 +Level 5
   4.213 +(f Un g) ` a = f ` a
   4.214 + 1. f Un g : (PROD x:?A. ?B(x))
   4.215 +> by (resolve_tac [fun_disjoint_Un] 1);
   4.216 +Level 6
   4.217 +(f Un g) ` a = f ` a
   4.218 + 1. f : ?A3 -> ?B3
   4.219 + 2. g : ?C3 -> ?D3
   4.220 + 3. ?A3 Int ?C3 = 0
   4.221 +> by (resolve_tac prems 1);
   4.222 +Level 7
   4.223 +(f Un g) ` a = f ` a
   4.224 + 1. g : ?C3 -> ?D3
   4.225 + 2. A Int ?C3 = 0
   4.226 +> by (resolve_tac prems 1);
   4.227 +Level 8
   4.228 +(f Un g) ` a = f ` a
   4.229 + 1. A Int C = 0
   4.230 +> by (resolve_tac prems 1);
   4.231 +Level 9
   4.232 +(f Un g) ` a = f ` a
   4.233 +No subgoals!
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/ZF/ZF.tex	Wed Jan 13 16:36:36 1999 +0100
     5.3 @@ -0,0 +1,2616 @@
     5.4 +%% $Id$
     5.5 +\chapter{Zermelo-Fraenkel Set Theory}
     5.6 +\index{set theory|(}
     5.7 +
     5.8 +The theory~\thydx{ZF} implements Zermelo-Fraenkel set
     5.9 +theory~\cite{halmos60,suppes72} as an extension of~\texttt{FOL}, classical
    5.10 +first-order logic.  The theory includes a collection of derived natural
    5.11 +deduction rules, for use with Isabelle's classical reasoner.  Much
    5.12 +of it is based on the work of No\"el~\cite{noel}.
    5.13 +
    5.14 +A tremendous amount of set theory has been formally developed, including the
    5.15 +basic properties of relations, functions, ordinals and cardinals.  Significant
    5.16 +results have been proved, such as the Schr\"oder-Bernstein Theorem, the
    5.17 +Wellordering Theorem and a version of Ramsey's Theorem.  \texttt{ZF} provides
    5.18 +both the integers and the natural numbers.  General methods have been
    5.19 +developed for solving recursion equations over monotonic functors; these have
    5.20 +been applied to yield constructions of lists, trees, infinite lists, etc.
    5.21 +
    5.22 +\texttt{ZF} has a flexible package for handling inductive definitions,
    5.23 +such as inference systems, and datatype definitions, such as lists and
    5.24 +trees.  Moreover it handles coinductive definitions, such as
    5.25 +bisimulation relations, and codatatype definitions, such as streams.  It
    5.26 +provides a streamlined syntax for defining primitive recursive functions over
    5.27 +datatypes. 
    5.28 +
    5.29 +Because {\ZF} is an extension of {\FOL}, it provides the same
    5.30 +packages, namely \texttt{hyp_subst_tac}, the simplifier, and the
    5.31 +classical reasoner.  The default simpset and claset are usually
    5.32 +satisfactory.
    5.33 +
    5.34 +Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF}
    5.35 +less formally than this chapter.  Isabelle employs a novel treatment of
    5.36 +non-well-founded data structures within the standard {\sc zf} axioms including
    5.37 +the Axiom of Foundation~\cite{paulson-final}.
    5.38 +
    5.39 +
    5.40 +\section{Which version of axiomatic set theory?}
    5.41 +The two main axiom systems for set theory are Bernays-G\"odel~({\sc bg})
    5.42 +and Zermelo-Fraenkel~({\sc zf}).  Resolution theorem provers can use {\sc
    5.43 +  bg} because it is finite~\cite{boyer86,quaife92}.  {\sc zf} does not
    5.44 +have a finite axiom system because of its Axiom Scheme of Replacement.
    5.45 +This makes it awkward to use with many theorem provers, since instances
    5.46 +of the axiom scheme have to be invoked explicitly.  Since Isabelle has no
    5.47 +difficulty with axiom schemes, we may adopt either axiom system.
    5.48 +
    5.49 +These two theories differ in their treatment of {\bf classes}, which are
    5.50 +collections that are `too big' to be sets.  The class of all sets,~$V$,
    5.51 +cannot be a set without admitting Russell's Paradox.  In {\sc bg}, both
    5.52 +classes and sets are individuals; $x\in V$ expresses that $x$ is a set.  In
    5.53 +{\sc zf}, all variables denote sets; classes are identified with unary
    5.54 +predicates.  The two systems define essentially the same sets and classes,
    5.55 +with similar properties.  In particular, a class cannot belong to another
    5.56 +class (let alone a set).
    5.57 +
    5.58 +Modern set theorists tend to prefer {\sc zf} because they are mainly concerned
    5.59 +with sets, rather than classes.  {\sc bg} requires tiresome proofs that various
    5.60 +collections are sets; for instance, showing $x\in\{x\}$ requires showing that
    5.61 +$x$ is a set.
    5.62 +
    5.63 +
    5.64 +\begin{figure} \small
    5.65 +\begin{center}
    5.66 +\begin{tabular}{rrr} 
    5.67 +  \it name      &\it meta-type  & \it description \\ 
    5.68 +  \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder\\
    5.69 +  \cdx{0}       & $i$           & empty set\\
    5.70 +  \cdx{cons}    & $[i,i]\To i$  & finite set constructor\\
    5.71 +  \cdx{Upair}   & $[i,i]\To i$  & unordered pairing\\
    5.72 +  \cdx{Pair}    & $[i,i]\To i$  & ordered pairing\\
    5.73 +  \cdx{Inf}     & $i$   & infinite set\\
    5.74 +  \cdx{Pow}     & $i\To i$      & powerset\\
    5.75 +  \cdx{Union} \cdx{Inter} & $i\To i$    & set union/intersection \\
    5.76 +  \cdx{split}   & $[[i,i]\To i, i] \To i$ & generalized projection\\
    5.77 +  \cdx{fst} \cdx{snd}   & $i\To i$      & projections\\
    5.78 +  \cdx{converse}& $i\To i$      & converse of a relation\\
    5.79 +  \cdx{succ}    & $i\To i$      & successor\\
    5.80 +  \cdx{Collect} & $[i,i\To o]\To i$     & separation\\
    5.81 +  \cdx{Replace} & $[i, [i,i]\To o] \To i$       & replacement\\
    5.82 +  \cdx{PrimReplace} & $[i, [i,i]\To o] \To i$   & primitive replacement\\
    5.83 +  \cdx{RepFun}  & $[i, i\To i] \To i$   & functional replacement\\
    5.84 +  \cdx{Pi} \cdx{Sigma}  & $[i,i\To i]\To i$     & general product/sum\\
    5.85 +  \cdx{domain}  & $i\To i$      & domain of a relation\\
    5.86 +  \cdx{range}   & $i\To i$      & range of a relation\\
    5.87 +  \cdx{field}   & $i\To i$      & field of a relation\\
    5.88 +  \cdx{Lambda}  & $[i, i\To i]\To i$    & $\lambda$-abstraction\\
    5.89 +  \cdx{restrict}& $[i, i] \To i$        & restriction of a function\\
    5.90 +  \cdx{The}     & $[i\To o]\To i$       & definite description\\
    5.91 +  \cdx{if}      & $[o,i,i]\To i$        & conditional\\
    5.92 +  \cdx{Ball} \cdx{Bex}  & $[i, i\To o]\To o$    & bounded quantifiers
    5.93 +\end{tabular}
    5.94 +\end{center}
    5.95 +\subcaption{Constants}
    5.96 +
    5.97 +\begin{center}
    5.98 +\index{*"`"` symbol}
    5.99 +\index{*"-"`"` symbol}
   5.100 +\index{*"` symbol}\index{function applications!in \ZF}
   5.101 +\index{*"- symbol}
   5.102 +\index{*": symbol}
   5.103 +\index{*"<"= symbol}
   5.104 +\begin{tabular}{rrrr} 
   5.105 +  \it symbol  & \it meta-type & \it priority & \it description \\ 
   5.106 +  \tt ``        & $[i,i]\To i$  &  Left 90      & image \\
   5.107 +  \tt -``       & $[i,i]\To i$  &  Left 90      & inverse image \\
   5.108 +  \tt `         & $[i,i]\To i$  &  Left 90      & application \\
   5.109 +  \sdx{Int}     & $[i,i]\To i$  &  Left 70      & intersection ($\int$) \\
   5.110 +  \sdx{Un}      & $[i,i]\To i$  &  Left 65      & union ($\un$) \\
   5.111 +  \tt -         & $[i,i]\To i$  &  Left 65      & set difference ($-$) \\[1ex]
   5.112 +  \tt:          & $[i,i]\To o$  &  Left 50      & membership ($\in$) \\
   5.113 +  \tt <=        & $[i,i]\To o$  &  Left 50      & subset ($\subseteq$) 
   5.114 +\end{tabular}
   5.115 +\end{center}
   5.116 +\subcaption{Infixes}
   5.117 +\caption{Constants of {\ZF}} \label{zf-constants}
   5.118 +\end{figure} 
   5.119 +
   5.120 +
   5.121 +\section{The syntax of set theory}
   5.122 +The language of set theory, as studied by logicians, has no constants.  The
   5.123 +traditional axioms merely assert the existence of empty sets, unions,
   5.124 +powersets, etc.; this would be intolerable for practical reasoning.  The
   5.125 +Isabelle theory declares constants for primitive sets.  It also extends
   5.126 +\texttt{FOL} with additional syntax for finite sets, ordered pairs,
   5.127 +comprehension, general union/intersection, general sums/products, and
   5.128 +bounded quantifiers.  In most other respects, Isabelle implements precisely
   5.129 +Zermelo-Fraenkel set theory.
   5.130 +
   5.131 +Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while
   5.132 +Figure~\ref{zf-trans} presents the syntax translations.  Finally,
   5.133 +Figure~\ref{zf-syntax} presents the full grammar for set theory, including
   5.134 +the constructs of \FOL.
   5.135 +
   5.136 +Local abbreviations can be introduced by a \texttt{let} construct whose
   5.137 +syntax appears in Fig.\ts\ref{zf-syntax}.  Internally it is translated into
   5.138 +the constant~\cdx{Let}.  It can be expanded by rewriting with its
   5.139 +definition, \tdx{Let_def}.
   5.140 +
   5.141 +Apart from \texttt{let}, set theory does not use polymorphism.  All terms in
   5.142 +{\ZF} have type~\tydx{i}, which is the type of individuals and has class~{\tt
   5.143 +  term}.  The type of first-order formulae, remember, is~\textit{o}.
   5.144 +
   5.145 +Infix operators include binary union and intersection ($A\un B$ and
   5.146 +$A\int B$), set difference ($A-B$), and the subset and membership
   5.147 +relations.  Note that $a$\verb|~:|$b$ is translated to $\neg(a\in b)$.  The
   5.148 +union and intersection operators ($\bigcup A$ and $\bigcap A$) form the
   5.149 +union or intersection of a set of sets; $\bigcup A$ means the same as
   5.150 +$\bigcup@{x\in A}x$.  Of these operators, only $\bigcup A$ is primitive.
   5.151 +
   5.152 +The constant \cdx{Upair} constructs unordered pairs; thus {\tt
   5.153 +  Upair($A$,$B$)} denotes the set~$\{A,B\}$ and \texttt{Upair($A$,$A$)}
   5.154 +denotes the singleton~$\{A\}$.  General union is used to define binary
   5.155 +union.  The Isabelle version goes on to define the constant
   5.156 +\cdx{cons}:
   5.157 +\begin{eqnarray*}
   5.158 +   A\cup B              & \equiv &       \bigcup(\texttt{Upair}(A,B)) \\
   5.159 +   \texttt{cons}(a,B)      & \equiv &        \texttt{Upair}(a,a) \un B
   5.160 +\end{eqnarray*}
   5.161 +The $\{a@1, \ldots\}$ notation abbreviates finite sets constructed in the
   5.162 +obvious manner using~\texttt{cons} and~$\emptyset$ (the empty set):
   5.163 +\begin{eqnarray*}
   5.164 + \{a,b,c\} & \equiv & \texttt{cons}(a,\texttt{cons}(b,\texttt{cons}(c,\emptyset)))
   5.165 +\end{eqnarray*}
   5.166 +
   5.167 +The constant \cdx{Pair} constructs ordered pairs, as in {\tt
   5.168 +Pair($a$,$b$)}.  Ordered pairs may also be written within angle brackets,
   5.169 +as {\tt<$a$,$b$>}.  The $n$-tuple {\tt<$a@1$,\ldots,$a@{n-1}$,$a@n$>}
   5.170 +abbreviates the nest of pairs\par\nobreak
   5.171 +\centerline{\texttt{Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).}}
   5.172 +
   5.173 +In {\ZF}, a function is a set of pairs.  A {\ZF} function~$f$ is simply an
   5.174 +individual as far as Isabelle is concerned: its Isabelle type is~$i$, not
   5.175 +say $i\To i$.  The infix operator~{\tt`} denotes the application of a
   5.176 +function set to its argument; we must write~$f{\tt`}x$, not~$f(x)$.  The
   5.177 +syntax for image is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$.
   5.178 +
   5.179 +
   5.180 +\begin{figure} 
   5.181 +\index{lambda abs@$\lambda$-abstractions!in \ZF}
   5.182 +\index{*"-"> symbol}
   5.183 +\index{*"* symbol}
   5.184 +\begin{center} \footnotesize\tt\frenchspacing
   5.185 +\begin{tabular}{rrr} 
   5.186 +  \it external          & \it internal  & \it description \\ 
   5.187 +  $a$ \ttilde: $b$      & \ttilde($a$ : $b$)    & \rm negated membership\\
   5.188 +  \ttlbrace$a@1$, $\ldots$, $a@n$\ttrbrace  &  cons($a@1$,$\ldots$,cons($a@n$,0)) &
   5.189 +        \rm finite set \\
   5.190 +  <$a@1$, $\ldots$, $a@{n-1}$, $a@n$> & 
   5.191 +        Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) &
   5.192 +        \rm ordered $n$-tuple \\
   5.193 +  \ttlbrace$x$:$A . P[x]$\ttrbrace    &  Collect($A$,$\lambda x. P[x]$) &
   5.194 +        \rm separation \\
   5.195 +  \ttlbrace$y . x$:$A$, $Q[x,y]$\ttrbrace  &  Replace($A$,$\lambda x\,y. Q[x,y]$) &
   5.196 +        \rm replacement \\
   5.197 +  \ttlbrace$b[x] . x$:$A$\ttrbrace  &  RepFun($A$,$\lambda x. b[x]$) &
   5.198 +        \rm functional replacement \\
   5.199 +  \sdx{INT} $x$:$A . B[x]$      & Inter(\ttlbrace$B[x] . x$:$A$\ttrbrace) &
   5.200 +        \rm general intersection \\
   5.201 +  \sdx{UN}  $x$:$A . B[x]$      & Union(\ttlbrace$B[x] . x$:$A$\ttrbrace) &
   5.202 +        \rm general union \\
   5.203 +  \sdx{PROD} $x$:$A . B[x]$     & Pi($A$,$\lambda x. B[x]$) & 
   5.204 +        \rm general product \\
   5.205 +  \sdx{SUM}  $x$:$A . B[x]$     & Sigma($A$,$\lambda x. B[x]$) & 
   5.206 +        \rm general sum \\
   5.207 +  $A$ -> $B$            & Pi($A$,$\lambda x. B$) & 
   5.208 +        \rm function space \\
   5.209 +  $A$ * $B$             & Sigma($A$,$\lambda x. B$) & 
   5.210 +        \rm binary product \\
   5.211 +  \sdx{THE}  $x . P[x]$ & The($\lambda x. P[x]$) & 
   5.212 +        \rm definite description \\
   5.213 +  \sdx{lam}  $x$:$A . b[x]$     & Lambda($A$,$\lambda x. b[x]$) & 
   5.214 +        \rm $\lambda$-abstraction\\[1ex]
   5.215 +  \sdx{ALL} $x$:$A . P[x]$      & Ball($A$,$\lambda x. P[x]$) & 
   5.216 +        \rm bounded $\forall$ \\
   5.217 +  \sdx{EX}  $x$:$A . P[x]$      & Bex($A$,$\lambda x. P[x]$) & 
   5.218 +        \rm bounded $\exists$
   5.219 +\end{tabular}
   5.220 +\end{center}
   5.221 +\caption{Translations for {\ZF}} \label{zf-trans}
   5.222 +\end{figure} 
   5.223 +
   5.224 +
   5.225 +\begin{figure} 
   5.226 +\index{*let symbol}
   5.227 +\index{*in symbol}
   5.228 +\dquotes
   5.229 +\[\begin{array}{rcl}
   5.230 +    term & = & \hbox{expression of type~$i$} \\
   5.231 +         & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\
   5.232 +         & | & "if"~term~"then"~term~"else"~term \\
   5.233 +         & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\
   5.234 +         & | & "< "  term\; ("," term)^* " >"  \\
   5.235 +         & | & "{\ttlbrace} " id ":" term " . " formula " {\ttrbrace}" \\
   5.236 +         & | & "{\ttlbrace} " id " . " id ":" term ", " formula " {\ttrbrace}" \\
   5.237 +         & | & "{\ttlbrace} " term " . " id ":" term " {\ttrbrace}" \\
   5.238 +         & | & term " `` " term \\
   5.239 +         & | & term " -`` " term \\
   5.240 +         & | & term " ` " term \\
   5.241 +         & | & term " * " term \\
   5.242 +         & | & term " Int " term \\
   5.243 +         & | & term " Un " term \\
   5.244 +         & | & term " - " term \\
   5.245 +         & | & term " -> " term \\
   5.246 +         & | & "THE~~"  id  " . " formula\\
   5.247 +         & | & "lam~~"  id ":" term " . " term \\
   5.248 +         & | & "INT~~"  id ":" term " . " term \\
   5.249 +         & | & "UN~~~"  id ":" term " . " term \\
   5.250 +         & | & "PROD~"  id ":" term " . " term \\
   5.251 +         & | & "SUM~~"  id ":" term " . " term \\[2ex]
   5.252 + formula & = & \hbox{expression of type~$o$} \\
   5.253 +         & | & term " : " term \\
   5.254 +         & | & term " \ttilde: " term \\
   5.255 +         & | & term " <= " term \\
   5.256 +         & | & term " = " term \\
   5.257 +         & | & term " \ttilde= " term \\
   5.258 +         & | & "\ttilde\ " formula \\
   5.259 +         & | & formula " \& " formula \\
   5.260 +         & | & formula " | " formula \\
   5.261 +         & | & formula " --> " formula \\
   5.262 +         & | & formula " <-> " formula \\
   5.263 +         & | & "ALL " id ":" term " . " formula \\
   5.264 +         & | & "EX~~" id ":" term " . " formula \\
   5.265 +         & | & "ALL~" id~id^* " . " formula \\
   5.266 +         & | & "EX~~" id~id^* " . " formula \\
   5.267 +         & | & "EX!~" id~id^* " . " formula
   5.268 +  \end{array}
   5.269 +\]
   5.270 +\caption{Full grammar for {\ZF}} \label{zf-syntax}
   5.271 +\end{figure} 
   5.272 +
   5.273 +
   5.274 +\section{Binding operators}
   5.275 +The constant \cdx{Collect} constructs sets by the principle of {\bf
   5.276 +  separation}.  The syntax for separation is
   5.277 +\hbox{\tt\ttlbrace$x$:$A$.\ $P[x]$\ttrbrace}, where $P[x]$ is a formula
   5.278 +that may contain free occurrences of~$x$.  It abbreviates the set {\tt
   5.279 +  Collect($A$,$\lambda x. P[x]$)}, which consists of all $x\in A$ that
   5.280 +satisfy~$P[x]$.  Note that \texttt{Collect} is an unfortunate choice of
   5.281 +name: some set theories adopt a set-formation principle, related to
   5.282 +replacement, called collection.
   5.283 +
   5.284 +The constant \cdx{Replace} constructs sets by the principle of {\bf
   5.285 +  replacement}.  The syntax
   5.286 +\hbox{\tt\ttlbrace$y$.\ $x$:$A$,$Q[x,y]$\ttrbrace} denotes the set {\tt
   5.287 +  Replace($A$,$\lambda x\,y. Q[x,y]$)}, which consists of all~$y$ such
   5.288 +that there exists $x\in A$ satisfying~$Q[x,y]$.  The Replacement Axiom
   5.289 +has the condition that $Q$ must be single-valued over~$A$: for
   5.290 +all~$x\in A$ there exists at most one $y$ satisfying~$Q[x,y]$.  A
   5.291 +single-valued binary predicate is also called a {\bf class function}.
   5.292 +
   5.293 +The constant \cdx{RepFun} expresses a special case of replacement,
   5.294 +where $Q[x,y]$ has the form $y=b[x]$.  Such a $Q$ is trivially
   5.295 +single-valued, since it is just the graph of the meta-level
   5.296 +function~$\lambda x. b[x]$.  The resulting set consists of all $b[x]$
   5.297 +for~$x\in A$.  This is analogous to the \ML{} functional \texttt{map},
   5.298 +since it applies a function to every element of a set.  The syntax is
   5.299 +\hbox{\tt\ttlbrace$b[x]$.\ $x$:$A$\ttrbrace}, which expands to {\tt
   5.300 +  RepFun($A$,$\lambda x. b[x]$)}.
   5.301 +
   5.302 +\index{*INT symbol}\index{*UN symbol} 
   5.303 +General unions and intersections of indexed
   5.304 +families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$,
   5.305 +are written \hbox{\tt UN $x$:$A$.\ $B[x]$} and \hbox{\tt INT $x$:$A$.\ $B[x]$}.
   5.306 +Their meaning is expressed using \texttt{RepFun} as
   5.307 +\[
   5.308 +\bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad 
   5.309 +\bigcap(\{B[x]. x\in A\}). 
   5.310 +\]
   5.311 +General sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$ can be
   5.312 +constructed in set theory, where $B[x]$ is a family of sets over~$A$.  They
   5.313 +have as special cases $A\times B$ and $A\to B$, where $B$ is simply a set.
   5.314 +This is similar to the situation in Constructive Type Theory (set theory
   5.315 +has `dependent sets') and calls for similar syntactic conventions.  The
   5.316 +constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and
   5.317 +products.  Instead of \texttt{Sigma($A$,$B$)} and \texttt{Pi($A$,$B$)} we may
   5.318 +write 
   5.319 +\hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt PROD $x$:$A$.\ $B[x]$}.  
   5.320 +\index{*SUM symbol}\index{*PROD symbol}%
   5.321 +The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$->$B$} abbreviate
   5.322 +general sums and products over a constant family.\footnote{Unlike normal
   5.323 +infix operators, {\tt*} and {\tt->} merely define abbreviations; there are
   5.324 +no constants~\texttt{op~*} and~\hbox{\tt op~->}.} Isabelle accepts these
   5.325 +abbreviations in parsing and uses them whenever possible for printing.
   5.326 +
   5.327 +\index{*THE symbol} 
   5.328 +As mentioned above, whenever the axioms assert the existence and uniqueness
   5.329 +of a set, Isabelle's set theory declares a constant for that set.  These
   5.330 +constants can express the {\bf definite description} operator~$\iota
   5.331 +x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists.
   5.332 +Since all terms in {\ZF} denote something, a description is always
   5.333 +meaningful, but we do not know its value unless $P[x]$ defines it uniquely.
   5.334 +Using the constant~\cdx{The}, we may write descriptions as {\tt
   5.335 +  The($\lambda x. P[x]$)} or use the syntax \hbox{\tt THE $x$.\ $P[x]$}.
   5.336 +
   5.337 +\index{*lam symbol}
   5.338 +Function sets may be written in $\lambda$-notation; $\lambda x\in A. b[x]$
   5.339 +stands for the set of all pairs $\pair{x,b[x]}$ for $x\in A$.  In order for
   5.340 +this to be a set, the function's domain~$A$ must be given.  Using the
   5.341 +constant~\cdx{Lambda}, we may express function sets as {\tt
   5.342 +Lambda($A$,$\lambda x. b[x]$)} or use the syntax \hbox{\tt lam $x$:$A$.\ $b[x]$}.
   5.343 +
   5.344 +Isabelle's set theory defines two {\bf bounded quantifiers}:
   5.345 +\begin{eqnarray*}
   5.346 +   \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
   5.347 +   \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
   5.348 +\end{eqnarray*}
   5.349 +The constants~\cdx{Ball} and~\cdx{Bex} are defined
   5.350 +accordingly.  Instead of \texttt{Ball($A$,$P$)} and \texttt{Bex($A$,$P$)} we may
   5.351 +write
   5.352 +\hbox{\tt ALL $x$:$A$.\ $P[x]$} and \hbox{\tt EX $x$:$A$.\ $P[x]$}.
   5.353 +
   5.354 +
   5.355 +%%%% ZF.thy
   5.356 +
   5.357 +\begin{figure}
   5.358 +\begin{ttbox}
   5.359 +\tdx{Let_def}            Let(s, f) == f(s)
   5.360 +
   5.361 +\tdx{Ball_def}           Ball(A,P) == ALL x. x:A --> P(x)
   5.362 +\tdx{Bex_def}            Bex(A,P)  == EX x. x:A & P(x)
   5.363 +
   5.364 +\tdx{subset_def}         A <= B  == ALL x:A. x:B
   5.365 +\tdx{extension}          A = B  <->  A <= B & B <= A
   5.366 +
   5.367 +\tdx{Union_iff}          A : Union(C) <-> (EX B:C. A:B)
   5.368 +\tdx{Pow_iff}            A : Pow(B) <-> A <= B
   5.369 +\tdx{foundation}         A=0 | (EX x:A. ALL y:x. ~ y:A)
   5.370 +
   5.371 +\tdx{replacement}        (ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
   5.372 +                   b : PrimReplace(A,P) <-> (EX x:A. P(x,b))
   5.373 +\subcaption{The Zermelo-Fraenkel Axioms}
   5.374 +
   5.375 +\tdx{Replace_def}  Replace(A,P) == 
   5.376 +                   PrimReplace(A, \%x y. (EX!z. P(x,z)) & P(x,y))
   5.377 +\tdx{RepFun_def}   RepFun(A,f)  == {\ttlbrace}y . x:A, y=f(x)\ttrbrace
   5.378 +\tdx{the_def}      The(P)       == Union({\ttlbrace}y . x:{\ttlbrace}0{\ttrbrace}, P(y){\ttrbrace})
   5.379 +\tdx{if_def}       if(P,a,b)    == THE z. P & z=a | ~P & z=b
   5.380 +\tdx{Collect_def}  Collect(A,P) == {\ttlbrace}y . x:A, x=y & P(x){\ttrbrace}
   5.381 +\tdx{Upair_def}    Upair(a,b)   == 
   5.382 +                 {\ttlbrace}y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b){\ttrbrace}
   5.383 +\subcaption{Consequences of replacement}
   5.384 +
   5.385 +\tdx{Inter_def}    Inter(A) == {\ttlbrace}x:Union(A) . ALL y:A. x:y{\ttrbrace}
   5.386 +\tdx{Un_def}       A Un  B  == Union(Upair(A,B))
   5.387 +\tdx{Int_def}      A Int B  == Inter(Upair(A,B))
   5.388 +\tdx{Diff_def}     A - B    == {\ttlbrace}x:A . x~:B{\ttrbrace}
   5.389 +\subcaption{Union, intersection, difference}
   5.390 +\end{ttbox}
   5.391 +\caption{Rules and axioms of {\ZF}} \label{zf-rules}
   5.392 +\end{figure}
   5.393 +
   5.394 +
   5.395 +\begin{figure}
   5.396 +\begin{ttbox}
   5.397 +\tdx{cons_def}     cons(a,A) == Upair(a,a) Un A
   5.398 +\tdx{succ_def}     succ(i) == cons(i,i)
   5.399 +\tdx{infinity}     0:Inf & (ALL y:Inf. succ(y): Inf)
   5.400 +\subcaption{Finite and infinite sets}
   5.401 +
   5.402 +\tdx{Pair_def}       <a,b>      == {\ttlbrace}{\ttlbrace}a,a{\ttrbrace}, {\ttlbrace}a,b{\ttrbrace}{\ttrbrace}
   5.403 +\tdx{split_def}      split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b)
   5.404 +\tdx{fst_def}        fst(A)     == split(\%x y. x, p)
   5.405 +\tdx{snd_def}        snd(A)     == split(\%x y. y, p)
   5.406 +\tdx{Sigma_def}      Sigma(A,B) == UN x:A. UN y:B(x). {\ttlbrace}<x,y>{\ttrbrace}
   5.407 +\subcaption{Ordered pairs and Cartesian products}
   5.408 +
   5.409 +\tdx{converse_def}   converse(r) == {\ttlbrace}z. w:r, EX x y. w=<x,y> & z=<y,x>{\ttrbrace}
   5.410 +\tdx{domain_def}     domain(r)   == {\ttlbrace}x. w:r, EX y. w=<x,y>{\ttrbrace}
   5.411 +\tdx{range_def}      range(r)    == domain(converse(r))
   5.412 +\tdx{field_def}      field(r)    == domain(r) Un range(r)
   5.413 +\tdx{image_def}      r `` A      == {\ttlbrace}y : range(r) . EX x:A. <x,y> : r{\ttrbrace}
   5.414 +\tdx{vimage_def}     r -`` A     == converse(r)``A
   5.415 +\subcaption{Operations on relations}
   5.416 +
   5.417 +\tdx{lam_def}    Lambda(A,b) == {\ttlbrace}<x,b(x)> . x:A{\ttrbrace}
   5.418 +\tdx{apply_def}  f`a         == THE y. <a,y> : f
   5.419 +\tdx{Pi_def}     Pi(A,B) == {\ttlbrace}f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f{\ttrbrace}
   5.420 +\tdx{restrict_def}   restrict(f,A) == lam x:A. f`x
   5.421 +\subcaption{Functions and general product}
   5.422 +\end{ttbox}
   5.423 +\caption{Further definitions of {\ZF}} \label{zf-defs}
   5.424 +\end{figure}
   5.425 +
   5.426 +
   5.427 +
   5.428 +\section{The Zermelo-Fraenkel axioms}
   5.429 +The axioms appear in Fig.\ts \ref{zf-rules}.  They resemble those
   5.430 +presented by Suppes~\cite{suppes72}.  Most of the theory consists of
   5.431 +definitions.  In particular, bounded quantifiers and the subset relation
   5.432 +appear in other axioms.  Object-level quantifiers and implications have
   5.433 +been replaced by meta-level ones wherever possible, to simplify use of the
   5.434 +axioms.  See the file \texttt{ZF/ZF.thy} for details.
   5.435 +
   5.436 +The traditional replacement axiom asserts
   5.437 +\[ y \in \texttt{PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \]
   5.438 +subject to the condition that $P(x,y)$ is single-valued for all~$x\in A$.
   5.439 +The Isabelle theory defines \cdx{Replace} to apply
   5.440 +\cdx{PrimReplace} to the single-valued part of~$P$, namely
   5.441 +\[ (\exists!z. P(x,z)) \conj P(x,y). \]
   5.442 +Thus $y\in \texttt{Replace}(A,P)$ if and only if there is some~$x$ such that
   5.443 +$P(x,-)$ holds uniquely for~$y$.  Because the equivalence is unconditional,
   5.444 +\texttt{Replace} is much easier to use than \texttt{PrimReplace}; it defines the
   5.445 +same set, if $P(x,y)$ is single-valued.  The nice syntax for replacement
   5.446 +expands to \texttt{Replace}.
   5.447 +
   5.448 +Other consequences of replacement include functional replacement
   5.449 +(\cdx{RepFun}) and definite descriptions (\cdx{The}).
   5.450 +Axioms for separation (\cdx{Collect}) and unordered pairs
   5.451 +(\cdx{Upair}) are traditionally assumed, but they actually follow
   5.452 +from replacement~\cite[pages 237--8]{suppes72}.
   5.453 +
   5.454 +The definitions of general intersection, etc., are straightforward.  Note
   5.455 +the definition of \texttt{cons}, which underlies the finite set notation.
   5.456 +The axiom of infinity gives us a set that contains~0 and is closed under
   5.457 +successor (\cdx{succ}).  Although this set is not uniquely defined,
   5.458 +the theory names it (\cdx{Inf}) in order to simplify the
   5.459 +construction of the natural numbers.
   5.460 +                                             
   5.461 +Further definitions appear in Fig.\ts\ref{zf-defs}.  Ordered pairs are
   5.462 +defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$.  Recall
   5.463 +that \cdx{Sigma}$(A,B)$ generalizes the Cartesian product of two
   5.464 +sets.  It is defined to be the union of all singleton sets
   5.465 +$\{\pair{x,y}\}$, for $x\in A$ and $y\in B(x)$.  This is a typical usage of
   5.466 +general union.
   5.467 +
   5.468 +The projections \cdx{fst} and~\cdx{snd} are defined in terms of the
   5.469 +generalized projection \cdx{split}.  The latter has been borrowed from
   5.470 +Martin-L\"of's Type Theory, and is often easier to use than \cdx{fst}
   5.471 +and~\cdx{snd}.
   5.472 +
   5.473 +Operations on relations include converse, domain, range, and image.  The
   5.474 +set ${\tt Pi}(A,B)$ generalizes the space of functions between two sets.
   5.475 +Note the simple definitions of $\lambda$-abstraction (using
   5.476 +\cdx{RepFun}) and application (using a definite description).  The
   5.477 +function \cdx{restrict}$(f,A)$ has the same values as~$f$, but only
   5.478 +over the domain~$A$.
   5.479 +
   5.480 +
   5.481 +%%%% zf.ML
   5.482 +
   5.483 +\begin{figure}
   5.484 +\begin{ttbox}
   5.485 +\tdx{ballI}       [| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)
   5.486 +\tdx{bspec}       [| ALL x:A. P(x);  x: A |] ==> P(x)
   5.487 +\tdx{ballE}       [| ALL x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q
   5.488 +
   5.489 +\tdx{ball_cong}   [| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> 
   5.490 +            (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))
   5.491 +
   5.492 +\tdx{bexI}        [| P(x);  x: A |] ==> EX x:A. P(x)
   5.493 +\tdx{bexCI}       [| ALL x:A. ~P(x) ==> P(a);  a: A |] ==> EX x:A. P(x)
   5.494 +\tdx{bexE}        [| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q |] ==> Q
   5.495 +
   5.496 +\tdx{bex_cong}    [| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> 
   5.497 +            (EX x:A. P(x)) <-> (EX x:A'. P'(x))
   5.498 +\subcaption{Bounded quantifiers}
   5.499 +
   5.500 +\tdx{subsetI}       (!!x. x:A ==> x:B) ==> A <= B
   5.501 +\tdx{subsetD}       [| A <= B;  c:A |] ==> c:B
   5.502 +\tdx{subsetCE}      [| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P
   5.503 +\tdx{subset_refl}   A <= A
   5.504 +\tdx{subset_trans}  [| A<=B;  B<=C |] ==> A<=C
   5.505 +
   5.506 +\tdx{equalityI}     [| A <= B;  B <= A |] ==> A = B
   5.507 +\tdx{equalityD1}    A = B ==> A<=B
   5.508 +\tdx{equalityD2}    A = B ==> B<=A
   5.509 +\tdx{equalityE}     [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
   5.510 +\subcaption{Subsets and extensionality}
   5.511 +
   5.512 +\tdx{emptyE}          a:0 ==> P
   5.513 +\tdx{empty_subsetI}   0 <= A
   5.514 +\tdx{equals0I}        [| !!y. y:A ==> False |] ==> A=0
   5.515 +\tdx{equals0D}        [| A=0;  a:A |] ==> P
   5.516 +
   5.517 +\tdx{PowI}            A <= B ==> A : Pow(B)
   5.518 +\tdx{PowD}            A : Pow(B)  ==>  A<=B
   5.519 +\subcaption{The empty set; power sets}
   5.520 +\end{ttbox}
   5.521 +\caption{Basic derived rules for {\ZF}} \label{zf-lemmas1}
   5.522 +\end{figure}
   5.523 +
   5.524 +
   5.525 +\section{From basic lemmas to function spaces}
   5.526 +Faced with so many definitions, it is essential to prove lemmas.  Even
   5.527 +trivial theorems like $A \int B = B \int A$ would be difficult to
   5.528 +prove from the definitions alone.  Isabelle's set theory derives many
   5.529 +rules using a natural deduction style.  Ideally, a natural deduction
   5.530 +rule should introduce or eliminate just one operator, but this is not
   5.531 +always practical.  For most operators, we may forget its definition
   5.532 +and use its derived rules instead.
   5.533 +
   5.534 +\subsection{Fundamental lemmas}
   5.535 +Figure~\ref{zf-lemmas1} presents the derived rules for the most basic
   5.536 +operators.  The rules for the bounded quantifiers resemble those for the
   5.537 +ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption
   5.538 +in the style of Isabelle's classical reasoner.  The \rmindex{congruence
   5.539 +  rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's
   5.540 +simplifier, but have few other uses.  Congruence rules must be specially
   5.541 +derived for all binding operators, and henceforth will not be shown.
   5.542 +
   5.543 +Figure~\ref{zf-lemmas1} also shows rules for the subset and equality
   5.544 +relations (proof by extensionality), and rules about the empty set and the
   5.545 +power set operator.
   5.546 +
   5.547 +Figure~\ref{zf-lemmas2} presents rules for replacement and separation.
   5.548 +The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than
   5.549 +comparable rules for \texttt{PrimReplace} would be.  The principle of
   5.550 +separation is proved explicitly, although most proofs should use the
   5.551 +natural deduction rules for \texttt{Collect}.  The elimination rule
   5.552 +\tdx{CollectE} is equivalent to the two destruction rules
   5.553 +\tdx{CollectD1} and \tdx{CollectD2}, but each rule is suited to
   5.554 +particular circumstances.  Although too many rules can be confusing, there
   5.555 +is no reason to aim for a minimal set of rules.  See the file
   5.556 +\texttt{ZF/ZF.ML} for a complete listing.
   5.557 +
   5.558 +Figure~\ref{zf-lemmas3} presents rules for general union and intersection.
   5.559 +The empty intersection should be undefined.  We cannot have
   5.560 +$\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set.  All
   5.561 +expressions denote something in {\ZF} set theory; the definition of
   5.562 +intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is
   5.563 +arbitrary.  The rule \tdx{InterI} must have a premise to exclude
   5.564 +the empty intersection.  Some of the laws governing intersections require
   5.565 +similar premises.
   5.566 +
   5.567 +
   5.568 +%the [p] gives better page breaking for the book
   5.569 +\begin{figure}[p]
   5.570 +\begin{ttbox}
   5.571 +\tdx{ReplaceI}      [| x: A;  P(x,b);  !!y. P(x,y) ==> y=b |] ==> 
   5.572 +              b : {\ttlbrace}y. x:A, P(x,y){\ttrbrace}
   5.573 +
   5.574 +\tdx{ReplaceE}      [| b : {\ttlbrace}y. x:A, P(x,y){\ttrbrace};  
   5.575 +                 !!x. [| x: A;  P(x,b);  ALL y. P(x,y)-->y=b |] ==> R 
   5.576 +              |] ==> R
   5.577 +
   5.578 +\tdx{RepFunI}       [| a : A |] ==> f(a) : {\ttlbrace}f(x). x:A{\ttrbrace}
   5.579 +\tdx{RepFunE}       [| b : {\ttlbrace}f(x). x:A{\ttrbrace};  
   5.580 +                 !!x.[| x:A;  b=f(x) |] ==> P |] ==> P
   5.581 +
   5.582 +\tdx{separation}     a : {\ttlbrace}x:A. P(x){\ttrbrace} <-> a:A & P(a)
   5.583 +\tdx{CollectI}       [| a:A;  P(a) |] ==> a : {\ttlbrace}x:A. P(x){\ttrbrace}
   5.584 +\tdx{CollectE}       [| a : {\ttlbrace}x:A. P(x){\ttrbrace};  [| a:A; P(a) |] ==> R |] ==> R
   5.585 +\tdx{CollectD1}      a : {\ttlbrace}x:A. P(x){\ttrbrace} ==> a:A
   5.586 +\tdx{CollectD2}      a : {\ttlbrace}x:A. P(x){\ttrbrace} ==> P(a)
   5.587 +\end{ttbox}
   5.588 +\caption{Replacement and separation} \label{zf-lemmas2}
   5.589 +\end{figure}
   5.590 +
   5.591 +
   5.592 +\begin{figure}
   5.593 +\begin{ttbox}
   5.594 +\tdx{UnionI}    [| B: C;  A: B |] ==> A: Union(C)
   5.595 +\tdx{UnionE}    [| A : Union(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R
   5.596 +
   5.597 +\tdx{InterI}    [| !!x. x: C ==> A: x;  c:C |] ==> A : Inter(C)
   5.598 +\tdx{InterD}    [| A : Inter(C);  B : C |] ==> A : B
   5.599 +\tdx{InterE}    [| A : Inter(C);  A:B ==> R;  ~ B:C ==> R |] ==> R
   5.600 +
   5.601 +\tdx{UN_I}      [| a: A;  b: B(a) |] ==> b: (UN x:A. B(x))
   5.602 +\tdx{UN_E}      [| b : (UN x:A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R 
   5.603 +          |] ==> R
   5.604 +
   5.605 +\tdx{INT_I}     [| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))
   5.606 +\tdx{INT_E}     [| b : (INT x:A. B(x));  a: A |] ==> b : B(a)
   5.607 +\end{ttbox}
   5.608 +\caption{General union and intersection} \label{zf-lemmas3}
   5.609 +\end{figure}
   5.610 +
   5.611 +
   5.612 +%%% upair.ML
   5.613 +
   5.614 +\begin{figure}
   5.615 +\begin{ttbox}
   5.616 +\tdx{pairing}      a:Upair(b,c) <-> (a=b | a=c)
   5.617 +\tdx{UpairI1}      a : Upair(a,b)
   5.618 +\tdx{UpairI2}      b : Upair(a,b)
   5.619 +\tdx{UpairE}       [| a : Upair(b,c);  a = b ==> P;  a = c ==> P |] ==> P
   5.620 +\end{ttbox}
   5.621 +\caption{Unordered pairs} \label{zf-upair1}
   5.622 +\end{figure}
   5.623 +
   5.624 +
   5.625 +\begin{figure}
   5.626 +\begin{ttbox}
   5.627 +\tdx{UnI1}         c : A ==> c : A Un B
   5.628 +\tdx{UnI2}         c : B ==> c : A Un B
   5.629 +\tdx{UnCI}         (~c : B ==> c : A) ==> c : A Un B
   5.630 +\tdx{UnE}          [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P
   5.631 +
   5.632 +\tdx{IntI}         [| c : A;  c : B |] ==> c : A Int B
   5.633 +\tdx{IntD1}        c : A Int B ==> c : A
   5.634 +\tdx{IntD2}        c : A Int B ==> c : B
   5.635 +\tdx{IntE}         [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
   5.636 +
   5.637 +\tdx{DiffI}        [| c : A;  ~ c : B |] ==> c : A - B
   5.638 +\tdx{DiffD1}       c : A - B ==> c : A
   5.639 +\tdx{DiffD2}       c : A - B ==> c ~: B
   5.640 +\tdx{DiffE}        [| c : A - B;  [| c:A; ~ c:B |] ==> P |] ==> P
   5.641 +\end{ttbox}
   5.642 +\caption{Union, intersection, difference} \label{zf-Un}
   5.643 +\end{figure}
   5.644 +
   5.645 +
   5.646 +\begin{figure}
   5.647 +\begin{ttbox}
   5.648 +\tdx{consI1}       a : cons(a,B)
   5.649 +\tdx{consI2}       a : B ==> a : cons(b,B)
   5.650 +\tdx{consCI}       (~ a:B ==> a=b) ==> a: cons(b,B)
   5.651 +\tdx{consE}        [| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P
   5.652 +
   5.653 +\tdx{singletonI}   a : {\ttlbrace}a{\ttrbrace}
   5.654 +\tdx{singletonE}   [| a : {\ttlbrace}b{\ttrbrace}; a=b ==> P |] ==> P
   5.655 +\end{ttbox}
   5.656 +\caption{Finite and singleton sets} \label{zf-upair2}
   5.657 +\end{figure}
   5.658 +
   5.659 +
   5.660 +\begin{figure}
   5.661 +\begin{ttbox}
   5.662 +\tdx{succI1}       i : succ(i)
   5.663 +\tdx{succI2}       i : j ==> i : succ(j)
   5.664 +\tdx{succCI}       (~ i:j ==> i=j) ==> i: succ(j)
   5.665 +\tdx{succE}        [| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P
   5.666 +\tdx{succ_neq_0}   [| succ(n)=0 |] ==> P
   5.667 +\tdx{succ_inject}  succ(m) = succ(n) ==> m=n
   5.668 +\end{ttbox}
   5.669 +\caption{The successor function} \label{zf-succ}
   5.670 +\end{figure}
   5.671 +
   5.672 +
   5.673 +\begin{figure}
   5.674 +\begin{ttbox}
   5.675 +\tdx{the_equality}     [| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a
   5.676 +\tdx{theI}             EX! x. P(x) ==> P(THE x. P(x))
   5.677 +
   5.678 +\tdx{if_P}              P ==> (if P then a else b) = a
   5.679 +\tdx{if_not_P}         ~P ==> (if P then a else b) = b
   5.680 +
   5.681 +\tdx{mem_asym}         [| a:b;  b:a |] ==> P
   5.682 +\tdx{mem_irrefl}       a:a ==> P
   5.683 +\end{ttbox}
   5.684 +\caption{Descriptions; non-circularity} \label{zf-the}
   5.685 +\end{figure}
   5.686 +
   5.687 +
   5.688 +\subsection{Unordered pairs and finite sets}
   5.689 +Figure~\ref{zf-upair1} presents the principle of unordered pairing, along
   5.690 +with its derived rules.  Binary union and intersection are defined in terms
   5.691 +of ordered pairs (Fig.\ts\ref{zf-Un}).  Set difference is also included.  The
   5.692 +rule \tdx{UnCI} is useful for classical reasoning about unions,
   5.693 +like \texttt{disjCI}\@; it supersedes \tdx{UnI1} and
   5.694 +\tdx{UnI2}, but these rules are often easier to work with.  For
   5.695 +intersection and difference we have both elimination and destruction rules.
   5.696 +Again, there is no reason to provide a minimal rule set.
   5.697 +
   5.698 +Figure~\ref{zf-upair2} is concerned with finite sets: it presents rules
   5.699 +for~\texttt{cons}, the finite set constructor, and rules for singleton
   5.700 +sets.  Figure~\ref{zf-succ} presents derived rules for the successor
   5.701 +function, which is defined in terms of~\texttt{cons}.  The proof that {\tt
   5.702 +  succ} is injective appears to require the Axiom of Foundation.
   5.703 +
   5.704 +Definite descriptions (\sdx{THE}) are defined in terms of the singleton
   5.705 +set~$\{0\}$, but their derived rules fortunately hide this
   5.706 +(Fig.\ts\ref{zf-the}).  The rule~\tdx{theI} is difficult to apply
   5.707 +because of the two occurrences of~$\Var{P}$.  However,
   5.708 +\tdx{the_equality} does not have this problem and the files contain
   5.709 +many examples of its use.
   5.710 +
   5.711 +Finally, the impossibility of having both $a\in b$ and $b\in a$
   5.712 +(\tdx{mem_asym}) is proved by applying the Axiom of Foundation to
   5.713 +the set $\{a,b\}$.  The impossibility of $a\in a$ is a trivial consequence.
   5.714 +
   5.715 +See the file \texttt{ZF/upair.ML} for full proofs of the rules discussed in
   5.716 +this section.
   5.717 +
   5.718 +
   5.719 +%%% subset.ML
   5.720 +
   5.721 +\begin{figure}
   5.722 +\begin{ttbox}
   5.723 +\tdx{Union_upper}       B:A ==> B <= Union(A)
   5.724 +\tdx{Union_least}       [| !!x. x:A ==> x<=C |] ==> Union(A) <= C
   5.725 +
   5.726 +\tdx{Inter_lower}       B:A ==> Inter(A) <= B
   5.727 +\tdx{Inter_greatest}    [| a:A;  !!x. x:A ==> C<=x |] ==> C <= Inter(A)
   5.728 +
   5.729 +\tdx{Un_upper1}         A <= A Un B
   5.730 +\tdx{Un_upper2}         B <= A Un B
   5.731 +\tdx{Un_least}          [| A<=C;  B<=C |] ==> A Un B <= C
   5.732 +
   5.733 +\tdx{Int_lower1}        A Int B <= A
   5.734 +\tdx{Int_lower2}        A Int B <= B
   5.735 +\tdx{Int_greatest}      [| C<=A;  C<=B |] ==> C <= A Int B
   5.736 +
   5.737 +\tdx{Diff_subset}       A-B <= A
   5.738 +\tdx{Diff_contains}     [| C<=A;  C Int B = 0 |] ==> C <= A-B
   5.739 +
   5.740 +\tdx{Collect_subset}    Collect(A,P) <= A
   5.741 +\end{ttbox}
   5.742 +\caption{Subset and lattice properties} \label{zf-subset}
   5.743 +\end{figure}
   5.744 +
   5.745 +
   5.746 +\subsection{Subset and lattice properties}
   5.747 +The subset relation is a complete lattice.  Unions form least upper bounds;
   5.748 +non-empty intersections form greatest lower bounds.  Figure~\ref{zf-subset}
   5.749 +shows the corresponding rules.  A few other laws involving subsets are
   5.750 +included.  Proofs are in the file \texttt{ZF/subset.ML}.
   5.751 +
   5.752 +Reasoning directly about subsets often yields clearer proofs than
   5.753 +reasoning about the membership relation.  Section~\ref{sec:ZF-pow-example}
   5.754 +below presents an example of this, proving the equation ${{\tt Pow}(A)\cap
   5.755 +  {\tt Pow}(B)}= {\tt Pow}(A\cap B)$.
   5.756 +
   5.757 +%%% pair.ML
   5.758 +
   5.759 +\begin{figure}
   5.760 +\begin{ttbox}
   5.761 +\tdx{Pair_inject1}    <a,b> = <c,d> ==> a=c
   5.762 +\tdx{Pair_inject2}    <a,b> = <c,d> ==> b=d
   5.763 +\tdx{Pair_inject}     [| <a,b> = <c,d>;  [| a=c; b=d |] ==> P |] ==> P
   5.764 +\tdx{Pair_neq_0}      <a,b>=0 ==> P
   5.765 +
   5.766 +\tdx{fst_conv}        fst(<a,b>) = a
   5.767 +\tdx{snd_conv}        snd(<a,b>) = b
   5.768 +\tdx{split}           split(\%x y. c(x,y), <a,b>) = c(a,b)
   5.769 +
   5.770 +\tdx{SigmaI}          [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)
   5.771 +
   5.772 +\tdx{SigmaE}          [| c: Sigma(A,B);  
   5.773 +                   !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
   5.774 +
   5.775 +\tdx{SigmaE2}         [| <a,b> : Sigma(A,B);    
   5.776 +                   [| a:A;  b:B(a) |] ==> P   |] ==> P
   5.777 +\end{ttbox}
   5.778 +\caption{Ordered pairs; projections; general sums} \label{zf-pair}
   5.779 +\end{figure}
   5.780 +
   5.781 +
   5.782 +\subsection{Ordered pairs} \label{sec:pairs}
   5.783 +
   5.784 +Figure~\ref{zf-pair} presents the rules governing ordered pairs,
   5.785 +projections and general sums.  File \texttt{ZF/pair.ML} contains the
   5.786 +full (and tedious) proof that $\{\{a\},\{a,b\}\}$ functions as an ordered
   5.787 +pair.  This property is expressed as two destruction rules,
   5.788 +\tdx{Pair_inject1} and \tdx{Pair_inject2}, and equivalently
   5.789 +as the elimination rule \tdx{Pair_inject}.
   5.790 +
   5.791 +The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$.  This
   5.792 +is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other 
   5.793 +encodings of ordered pairs.  The non-standard ordered pairs mentioned below
   5.794 +satisfy $\pair{\emptyset;\emptyset}=\emptyset$.
   5.795 +
   5.796 +The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE}
   5.797 +assert that \cdx{Sigma}$(A,B)$ consists of all pairs of the form
   5.798 +$\pair{x,y}$, for $x\in A$ and $y\in B(x)$.  The rule \tdx{SigmaE2}
   5.799 +merely states that $\pair{a,b}\in \texttt{Sigma}(A,B)$ implies $a\in A$ and
   5.800 +$b\in B(a)$.
   5.801 +
   5.802 +In addition, it is possible to use tuples as patterns in abstractions:
   5.803 +\begin{center}
   5.804 +{\tt\%<$x$,$y$>. $t$} \quad stands for\quad \texttt{split(\%$x$ $y$.\ $t$)}
   5.805 +\end{center}
   5.806 +Nested patterns are translated recursively:
   5.807 +{\tt\%<$x$,$y$,$z$>. $t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>. $t$} $\leadsto$
   5.808 +\texttt{split(\%$x$.\%<$y$,$z$>. $t$)} $\leadsto$ \texttt{split(\%$x$. split(\%$y$
   5.809 +  $z$.\ $t$))}.  The reverse translation is performed upon printing.
   5.810 +\begin{warn}
   5.811 +  The translation between patterns and \texttt{split} is performed automatically
   5.812 +  by the parser and printer.  Thus the internal and external form of a term
   5.813 +  may differ, which affects proofs.  For example the term {\tt
   5.814 +    (\%<x,y>.<y,x>)<a,b>} requires the theorem \texttt{split} to rewrite to
   5.815 +  {\tt<b,a>}.
   5.816 +\end{warn}
   5.817 +In addition to explicit $\lambda$-abstractions, patterns can be used in any
   5.818 +variable binding construct which is internally described by a
   5.819 +$\lambda$-abstraction.  Here are some important examples:
   5.820 +\begin{description}
   5.821 +\item[Let:] \texttt{let {\it pattern} = $t$ in $u$}
   5.822 +\item[Choice:] \texttt{THE~{\it pattern}~.~$P$}
   5.823 +\item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}
   5.824 +\item[Comprehension:] \texttt{{\ttlbrace}~{\it pattern}:$A$~.~$P$~{\ttrbrace}}
   5.825 +\end{description}
   5.826 +
   5.827 +
   5.828 +%%% domrange.ML
   5.829 +
   5.830 +\begin{figure}
   5.831 +\begin{ttbox}
   5.832 +\tdx{domainI}        <a,b>: r ==> a : domain(r)
   5.833 +\tdx{domainE}        [| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P
   5.834 +\tdx{domain_subset}  domain(Sigma(A,B)) <= A
   5.835 +
   5.836 +\tdx{rangeI}         <a,b>: r ==> b : range(r)
   5.837 +\tdx{rangeE}         [| b : range(r);  !!x. <x,b>: r ==> P |] ==> P
   5.838 +\tdx{range_subset}   range(A*B) <= B
   5.839 +
   5.840 +\tdx{fieldI1}        <a,b>: r ==> a : field(r)
   5.841 +\tdx{fieldI2}        <a,b>: r ==> b : field(r)
   5.842 +\tdx{fieldCI}        (~ <c,a>:r ==> <a,b>: r) ==> a : field(r)
   5.843 +
   5.844 +\tdx{fieldE}         [| a : field(r);  
   5.845 +                  !!x. <a,x>: r ==> P;  
   5.846 +                  !!x. <x,a>: r ==> P      
   5.847 +               |] ==> P
   5.848 +
   5.849 +\tdx{field_subset}   field(A*A) <= A
   5.850 +\end{ttbox}
   5.851 +\caption{Domain, range and field of a relation} \label{zf-domrange}
   5.852 +\end{figure}
   5.853 +
   5.854 +\begin{figure}
   5.855 +\begin{ttbox}
   5.856 +\tdx{imageI}         [| <a,b>: r;  a:A |] ==> b : r``A
   5.857 +\tdx{imageE}         [| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P
   5.858 +
   5.859 +\tdx{vimageI}        [| <a,b>: r;  b:B |] ==> a : r-``B
   5.860 +\tdx{vimageE}        [| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P
   5.861 +\end{ttbox}
   5.862 +\caption{Image and inverse image} \label{zf-domrange2}
   5.863 +\end{figure}
   5.864 +
   5.865 +
   5.866 +\subsection{Relations}
   5.867 +Figure~\ref{zf-domrange} presents rules involving relations, which are sets
   5.868 +of ordered pairs.  The converse of a relation~$r$ is the set of all pairs
   5.869 +$\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then
   5.870 +{\cdx{converse}$(r)$} is its inverse.  The rules for the domain
   5.871 +operation, namely \tdx{domainI} and~\tdx{domainE}, assert that
   5.872 +\cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains
   5.873 +some pair of the form~$\pair{x,y}$.  The range operation is similar, and
   5.874 +the field of a relation is merely the union of its domain and range.  
   5.875 +
   5.876 +Figure~\ref{zf-domrange2} presents rules for images and inverse images.
   5.877 +Note that these operations are generalisations of range and domain,
   5.878 +respectively.  See the file \texttt{ZF/domrange.ML} for derivations of the
   5.879 +rules.
   5.880 +
   5.881 +
   5.882 +%%% func.ML
   5.883 +
   5.884 +\begin{figure}
   5.885 +\begin{ttbox}
   5.886 +\tdx{fun_is_rel}      f: Pi(A,B) ==> f <= Sigma(A,B)
   5.887 +
   5.888 +\tdx{apply_equality}  [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b
   5.889 +\tdx{apply_equality2} [| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c
   5.890 +
   5.891 +\tdx{apply_type}      [| f: Pi(A,B);  a:A |] ==> f`a : B(a)
   5.892 +\tdx{apply_Pair}      [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f
   5.893 +\tdx{apply_iff}       f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b
   5.894 +
   5.895 +\tdx{fun_extension}   [| f : Pi(A,B);  g: Pi(A,D);
   5.896 +                   !!x. x:A ==> f`x = g`x     |] ==> f=g
   5.897 +
   5.898 +\tdx{domain_type}     [| <a,b> : f;  f: Pi(A,B) |] ==> a : A
   5.899 +\tdx{range_type}      [| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)
   5.900 +
   5.901 +\tdx{Pi_type}         [| f: A->C;  !!x. x:A ==> f`x: B(x) |] ==> f: Pi(A,B)
   5.902 +\tdx{domain_of_fun}   f: Pi(A,B) ==> domain(f)=A
   5.903 +\tdx{range_of_fun}    f: Pi(A,B) ==> f: A->range(f)
   5.904 +
   5.905 +\tdx{restrict}        a : A ==> restrict(f,A) ` a = f`a
   5.906 +\tdx{restrict_type}   [| !!x. x:A ==> f`x: B(x) |] ==> 
   5.907 +                restrict(f,A) : Pi(A,B)
   5.908 +\end{ttbox}
   5.909 +\caption{Functions} \label{zf-func1}
   5.910 +\end{figure}
   5.911 +
   5.912 +
   5.913 +\begin{figure}
   5.914 +\begin{ttbox}
   5.915 +\tdx{lamI}         a:A ==> <a,b(a)> : (lam x:A. b(x))
   5.916 +\tdx{lamE}         [| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P 
   5.917 +             |] ==>  P
   5.918 +
   5.919 +\tdx{lam_type}     [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)
   5.920 +
   5.921 +\tdx{beta}         a : A ==> (lam x:A. b(x)) ` a = b(a)
   5.922 +\tdx{eta}          f : Pi(A,B) ==> (lam x:A. f`x) = f
   5.923 +\end{ttbox}
   5.924 +\caption{$\lambda$-abstraction} \label{zf-lam}
   5.925 +\end{figure}
   5.926 +
   5.927 +
   5.928 +\begin{figure}
   5.929 +\begin{ttbox}
   5.930 +\tdx{fun_empty}            0: 0->0
   5.931 +\tdx{fun_single}           {\ttlbrace}<a,b>{\ttrbrace} : {\ttlbrace}a{\ttrbrace} -> {\ttlbrace}b{\ttrbrace}
   5.932 +
   5.933 +\tdx{fun_disjoint_Un}      [| f: A->B;  g: C->D;  A Int C = 0  |] ==>  
   5.934 +                     (f Un g) : (A Un C) -> (B Un D)
   5.935 +
   5.936 +\tdx{fun_disjoint_apply1}  [| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  
   5.937 +                     (f Un g)`a = f`a
   5.938 +
   5.939 +\tdx{fun_disjoint_apply2}  [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  
   5.940 +                     (f Un g)`c = g`c
   5.941 +\end{ttbox}
   5.942 +\caption{Constructing functions from smaller sets} \label{zf-func2}
   5.943 +\end{figure}
   5.944 +
   5.945 +
   5.946 +\subsection{Functions}
   5.947 +Functions, represented by graphs, are notoriously difficult to reason
   5.948 +about.  The file \texttt{ZF/func.ML} derives many rules, which overlap more
   5.949 +than they ought.  This section presents the more important rules.
   5.950 +
   5.951 +Figure~\ref{zf-func1} presents the basic properties of \cdx{Pi}$(A,B)$,
   5.952 +the generalized function space.  For example, if $f$ is a function and
   5.953 +$\pair{a,b}\in f$, then $f`a=b$ (\tdx{apply_equality}).  Two functions
   5.954 +are equal provided they have equal domains and deliver equals results
   5.955 +(\tdx{fun_extension}).
   5.956 +
   5.957 +By \tdx{Pi_type}, a function typing of the form $f\in A\to C$ can be
   5.958 +refined to the dependent typing $f\in\prod@{x\in A}B(x)$, given a suitable
   5.959 +family of sets $\{B(x)\}@{x\in A}$.  Conversely, by \tdx{range_of_fun},
   5.960 +any dependent typing can be flattened to yield a function type of the form
   5.961 +$A\to C$; here, $C={\tt range}(f)$.
   5.962 +
   5.963 +Among the laws for $\lambda$-abstraction, \tdx{lamI} and \tdx{lamE}
   5.964 +describe the graph of the generated function, while \tdx{beta} and
   5.965 +\tdx{eta} are the standard conversions.  We essentially have a
   5.966 +dependently-typed $\lambda$-calculus (Fig.\ts\ref{zf-lam}).
   5.967 +
   5.968 +Figure~\ref{zf-func2} presents some rules that can be used to construct
   5.969 +functions explicitly.  We start with functions consisting of at most one
   5.970 +pair, and may form the union of two functions provided their domains are
   5.971 +disjoint.  
   5.972 +
   5.973 +
   5.974 +\begin{figure}
   5.975 +\begin{ttbox}
   5.976 +\tdx{Int_absorb}         A Int A = A
   5.977 +\tdx{Int_commute}        A Int B = B Int A
   5.978 +\tdx{Int_assoc}          (A Int B) Int C  =  A Int (B Int C)
   5.979 +\tdx{Int_Un_distrib}     (A Un B) Int C  =  (A Int C) Un (B Int C)
   5.980 +
   5.981 +\tdx{Un_absorb}          A Un A = A
   5.982 +\tdx{Un_commute}         A Un B = B Un A
   5.983 +\tdx{Un_assoc}           (A Un B) Un C  =  A Un (B Un C)
   5.984 +\tdx{Un_Int_distrib}     (A Int B) Un C  =  (A Un C) Int (B Un C)
   5.985 +
   5.986 +\tdx{Diff_cancel}        A-A = 0
   5.987 +\tdx{Diff_disjoint}      A Int (B-A) = 0
   5.988 +\tdx{Diff_partition}     A<=B ==> A Un (B-A) = B
   5.989 +\tdx{double_complement}  [| A<=B; B<= C |] ==> (B - (C-A)) = A
   5.990 +\tdx{Diff_Un}            A - (B Un C) = (A-B) Int (A-C)
   5.991 +\tdx{Diff_Int}           A - (B Int C) = (A-B) Un (A-C)
   5.992 +
   5.993 +\tdx{Union_Un_distrib}   Union(A Un B) = Union(A) Un Union(B)
   5.994 +\tdx{Inter_Un_distrib}   [| a:A;  b:B |] ==> 
   5.995 +                   Inter(A Un B) = Inter(A) Int Inter(B)
   5.996 +
   5.997 +\tdx{Int_Union_RepFun}   A Int Union(B) = (UN C:B. A Int C)
   5.998 +
   5.999 +\tdx{Un_Inter_RepFun}    b:B ==> 
  5.1000 +                   A Un Inter(B) = (INT C:B. A Un C)
  5.1001 +
  5.1002 +\tdx{SUM_Un_distrib1}    (SUM x:A Un B. C(x)) = 
  5.1003 +                   (SUM x:A. C(x)) Un (SUM x:B. C(x))
  5.1004 +
  5.1005 +\tdx{SUM_Un_distrib2}    (SUM x:C. A(x) Un B(x)) =
  5.1006 +                   (SUM x:C. A(x))  Un  (SUM x:C. B(x))
  5.1007 +
  5.1008 +\tdx{SUM_Int_distrib1}   (SUM x:A Int B. C(x)) =
  5.1009 +                   (SUM x:A. C(x)) Int (SUM x:B. C(x))
  5.1010 +
  5.1011 +\tdx{SUM_Int_distrib2}   (SUM x:C. A(x) Int B(x)) =
  5.1012 +                   (SUM x:C. A(x)) Int (SUM x:C. B(x))
  5.1013 +\end{ttbox}
  5.1014 +\caption{Equalities} \label{zf-equalities}
  5.1015 +\end{figure}
  5.1016 +
  5.1017 +
  5.1018 +\begin{figure}
  5.1019 +%\begin{constants} 
  5.1020 +%  \cdx{1}       & $i$           &       & $\{\emptyset\}$       \\
  5.1021 +%  \cdx{bool}    & $i$           &       & the set $\{\emptyset,1\}$     \\
  5.1022 +%  \cdx{cond}   & $[i,i,i]\To i$ &       & conditional for \texttt{bool}    \\
  5.1023 +%  \cdx{not}    & $i\To i$       &       & negation for \texttt{bool}       \\
  5.1024 +%  \sdx{and}    & $[i,i]\To i$   & Left 70 & conjunction for \texttt{bool}  \\
  5.1025 +%  \sdx{or}     & $[i,i]\To i$   & Left 65 & disjunction for \texttt{bool}  \\
  5.1026 +%  \sdx{xor}    & $[i,i]\To i$   & Left 65 & exclusive-or for \texttt{bool}
  5.1027 +%\end{constants}
  5.1028 +%
  5.1029 +\begin{ttbox}
  5.1030 +\tdx{bool_def}       bool == {\ttlbrace}0,1{\ttrbrace}
  5.1031 +\tdx{cond_def}       cond(b,c,d) == if b=1 then c else d
  5.1032 +\tdx{not_def}        not(b)  == cond(b,0,1)
  5.1033 +\tdx{and_def}        a and b == cond(a,b,0)
  5.1034 +\tdx{or_def}         a or b  == cond(a,1,b)
  5.1035 +\tdx{xor_def}        a xor b == cond(a,not(b),b)
  5.1036 +
  5.1037 +\tdx{bool_1I}        1 : bool
  5.1038 +\tdx{bool_0I}        0 : bool
  5.1039 +\tdx{boolE}          [| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P
  5.1040 +\tdx{cond_1}         cond(1,c,d) = c
  5.1041 +\tdx{cond_0}         cond(0,c,d) = d
  5.1042 +\end{ttbox}
  5.1043 +\caption{The booleans} \label{zf-bool}
  5.1044 +\end{figure}
  5.1045 +
  5.1046 +
  5.1047 +\section{Further developments}
  5.1048 +The next group of developments is complex and extensive, and only
  5.1049 +highlights can be covered here.  It involves many theories and ML files of
  5.1050 +proofs. 
  5.1051 +
  5.1052 +Figure~\ref{zf-equalities} presents commutative, associative, distributive,
  5.1053 +and idempotency laws of union and intersection, along with other equations.
  5.1054 +See file \texttt{ZF/equalities.ML}.
  5.1055 +
  5.1056 +Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual
  5.1057 +operators including a conditional (Fig.\ts\ref{zf-bool}).  Although {\ZF} is a
  5.1058 +first-order theory, you can obtain the effect of higher-order logic using
  5.1059 +\texttt{bool}-valued functions, for example.  The constant~\texttt{1} is
  5.1060 +translated to \texttt{succ(0)}.
  5.1061 +
  5.1062 +\begin{figure}
  5.1063 +\index{*"+ symbol}
  5.1064 +\begin{constants}
  5.1065 +  \it symbol    & \it meta-type & \it priority & \it description \\ 
  5.1066 +  \tt +         & $[i,i]\To i$  &  Right 65     & disjoint union operator\\
  5.1067 +  \cdx{Inl}~~\cdx{Inr}  & $i\To i$      &       & injections\\
  5.1068 +  \cdx{case}    & $[i\To i,i\To i, i]\To i$ &   & conditional for $A+B$
  5.1069 +\end{constants}
  5.1070 +\begin{ttbox}
  5.1071 +\tdx{sum_def}        A+B == {\ttlbrace}0{\ttrbrace}*A Un {\ttlbrace}1{\ttrbrace}*B
  5.1072 +\tdx{Inl_def}        Inl(a) == <0,a>
  5.1073 +\tdx{Inr_def}        Inr(b) == <1,b>
  5.1074 +\tdx{case_def}       case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u)
  5.1075 +
  5.1076 +\tdx{sum_InlI}       a : A ==> Inl(a) : A+B
  5.1077 +\tdx{sum_InrI}       b : B ==> Inr(b) : A+B
  5.1078 +
  5.1079 +\tdx{Inl_inject}     Inl(a)=Inl(b) ==> a=b
  5.1080 +\tdx{Inr_inject}     Inr(a)=Inr(b) ==> a=b
  5.1081 +\tdx{Inl_neq_Inr}    Inl(a)=Inr(b) ==> P
  5.1082 +
  5.1083 +\tdx{sumE2}   u: A+B ==> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))
  5.1084 +
  5.1085 +\tdx{case_Inl}       case(c,d,Inl(a)) = c(a)
  5.1086 +\tdx{case_Inr}       case(c,d,Inr(b)) = d(b)
  5.1087 +\end{ttbox}
  5.1088 +\caption{Disjoint unions} \label{zf-sum}
  5.1089 +\end{figure}
  5.1090 +
  5.1091 +
  5.1092 +Theory \thydx{Sum} defines the disjoint union of two sets, with
  5.1093 +injections and a case analysis operator (Fig.\ts\ref{zf-sum}).  Disjoint
  5.1094 +unions play a role in datatype definitions, particularly when there is
  5.1095 +mutual recursion~\cite{paulson-set-II}.
  5.1096 +
  5.1097 +\begin{figure}
  5.1098 +\begin{ttbox}
  5.1099 +\tdx{QPair_def}       <a;b> == a+b
  5.1100 +\tdx{qsplit_def}      qsplit(c,p)  == THE y. EX a b. p=<a;b> & y=c(a,b)
  5.1101 +\tdx{qfsplit_def}     qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)
  5.1102 +\tdx{qconverse_def}   qconverse(r) == {\ttlbrace}z. w:r, EX x y. w=<x;y> & z=<y;x>{\ttrbrace}
  5.1103 +\tdx{QSigma_def}      QSigma(A,B)  == UN x:A. UN y:B(x). {\ttlbrace}<x;y>{\ttrbrace}
  5.1104 +
  5.1105 +\tdx{qsum_def}        A <+> B      == ({\ttlbrace}0{\ttrbrace} <*> A) Un ({\ttlbrace}1{\ttrbrace} <*> B)
  5.1106 +\tdx{QInl_def}        QInl(a)      == <0;a>
  5.1107 +\tdx{QInr_def}        QInr(b)      == <1;b>
  5.1108 +\tdx{qcase_def}       qcase(c,d)   == qsplit(\%y z. cond(y, d(z), c(z)))
  5.1109 +\end{ttbox}
  5.1110 +\caption{Non-standard pairs, products and sums} \label{zf-qpair}
  5.1111 +\end{figure}
  5.1112 +
  5.1113 +Theory \thydx{QPair} defines a notion of ordered pair that admits
  5.1114 +non-well-founded tupling (Fig.\ts\ref{zf-qpair}).  Such pairs are written
  5.1115 +{\tt<$a$;$b$>}.  It also defines the eliminator \cdx{qsplit}, the
  5.1116 +converse operator \cdx{qconverse}, and the summation operator
  5.1117 +\cdx{QSigma}.  These are completely analogous to the corresponding
  5.1118 +versions for standard ordered pairs.  The theory goes on to define a
  5.1119 +non-standard notion of disjoint sum using non-standard pairs.  All of these
  5.1120 +concepts satisfy the same properties as their standard counterparts; in
  5.1121 +addition, {\tt<$a$;$b$>} is continuous.  The theory supports coinductive
  5.1122 +definitions, for example of infinite lists~\cite{paulson-final}.
  5.1123 +
  5.1124 +\begin{figure}
  5.1125 +\begin{ttbox}
  5.1126 +\tdx{bnd_mono_def}   bnd_mono(D,h) == 
  5.1127 +                 h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))
  5.1128 +
  5.1129 +\tdx{lfp_def}        lfp(D,h) == Inter({\ttlbrace}X: Pow(D). h(X) <= X{\ttrbrace})
  5.1130 +\tdx{gfp_def}        gfp(D,h) == Union({\ttlbrace}X: Pow(D). X <= h(X){\ttrbrace})
  5.1131 +
  5.1132 +
  5.1133 +\tdx{lfp_lowerbound} [| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A
  5.1134 +
  5.1135 +\tdx{lfp_subset}     lfp(D,h) <= D
  5.1136 +
  5.1137 +\tdx{lfp_greatest}   [| bnd_mono(D,h);  
  5.1138 +                  !!X. [| h(X) <= X;  X<=D |] ==> A<=X 
  5.1139 +               |] ==> A <= lfp(D,h)
  5.1140 +
  5.1141 +\tdx{lfp_Tarski}     bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))
  5.1142 +
  5.1143 +\tdx{induct}         [| a : lfp(D,h);  bnd_mono(D,h);
  5.1144 +                  !!x. x : h(Collect(lfp(D,h),P)) ==> P(x)
  5.1145 +               |] ==> P(a)
  5.1146 +
  5.1147 +\tdx{lfp_mono}       [| bnd_mono(D,h);  bnd_mono(E,i);
  5.1148 +                  !!X. X<=D ==> h(X) <= i(X)  
  5.1149 +               |] ==> lfp(D,h) <= lfp(E,i)
  5.1150 +
  5.1151 +\tdx{gfp_upperbound} [| A <= h(A);  A<=D |] ==> A <= gfp(D,h)
  5.1152 +
  5.1153 +\tdx{gfp_subset}     gfp(D,h) <= D
  5.1154 +
  5.1155 +\tdx{gfp_least}      [| bnd_mono(D,h);  
  5.1156 +                  !!X. [| X <= h(X);  X<=D |] ==> X<=A
  5.1157 +               |] ==> gfp(D,h) <= A
  5.1158 +
  5.1159 +\tdx{gfp_Tarski}     bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))
  5.1160 +
  5.1161 +\tdx{coinduct}       [| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D 
  5.1162 +               |] ==> a : gfp(D,h)
  5.1163 +
  5.1164 +\tdx{gfp_mono}       [| bnd_mono(D,h);  D <= E;
  5.1165 +                  !!X. X<=D ==> h(X) <= i(X)  
  5.1166 +               |] ==> gfp(D,h) <= gfp(E,i)
  5.1167 +\end{ttbox}
  5.1168 +\caption{Least and greatest fixedpoints} \label{zf-fixedpt}
  5.1169 +\end{figure}
  5.1170 +
  5.1171 +The Knaster-Tarski Theorem states that every monotone function over a
  5.1172 +complete lattice has a fixedpoint.  Theory \thydx{Fixedpt} proves the
  5.1173 +Theorem only for a particular lattice, namely the lattice of subsets of a
  5.1174 +set (Fig.\ts\ref{zf-fixedpt}).  The theory defines least and greatest
  5.1175 +fixedpoint operators with corresponding induction and coinduction rules.
  5.1176 +These are essential to many definitions that follow, including the natural
  5.1177 +numbers and the transitive closure operator.  The (co)inductive definition
  5.1178 +package also uses the fixedpoint operators~\cite{paulson-CADE}.  See
  5.1179 +Davey and Priestley~\cite{davey&priestley} for more on the Knaster-Tarski
  5.1180 +Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle
  5.1181 +proofs.
  5.1182 +
  5.1183 +Monotonicity properties are proved for most of the set-forming operations:
  5.1184 +union, intersection, Cartesian product, image, domain, range, etc.  These
  5.1185 +are useful for applying the Knaster-Tarski Fixedpoint Theorem.  The proofs
  5.1186 +themselves are trivial applications of Isabelle's classical reasoner.  See
  5.1187 +file \texttt{ZF/mono.ML}.
  5.1188 +
  5.1189 +
  5.1190 +\begin{figure}
  5.1191 +\begin{constants} 
  5.1192 +  \it symbol  & \it meta-type & \it priority & \it description \\ 
  5.1193 +  \sdx{O}       & $[i,i]\To i$  &  Right 60     & composition ($\circ$) \\
  5.1194 +  \cdx{id}      & $i\To i$      &       & identity function \\
  5.1195 +  \cdx{inj}     & $[i,i]\To i$  &       & injective function space\\
  5.1196 +  \cdx{surj}    & $[i,i]\To i$  &       & surjective function space\\
  5.1197 +  \cdx{bij}     & $[i,i]\To i$  &       & bijective function space
  5.1198 +\end{constants}
  5.1199 +
  5.1200 +\begin{ttbox}
  5.1201 +\tdx{comp_def}  r O s     == {\ttlbrace}xz : domain(s)*range(r) . 
  5.1202 +                        EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r{\ttrbrace}
  5.1203 +\tdx{id_def}    id(A)     == (lam x:A. x)
  5.1204 +\tdx{inj_def}   inj(A,B)  == {\ttlbrace} f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x {\ttrbrace}
  5.1205 +\tdx{surj_def}  surj(A,B) == {\ttlbrace} f: A->B . ALL y:B. EX x:A. f`x=y {\ttrbrace}
  5.1206 +\tdx{bij_def}   bij(A,B)  == inj(A,B) Int surj(A,B)
  5.1207 +
  5.1208 +
  5.1209 +\tdx{left_inverse}     [| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a
  5.1210 +\tdx{right_inverse}    [| f: inj(A,B);  b: range(f) |] ==> 
  5.1211 +                 f`(converse(f)`b) = b
  5.1212 +
  5.1213 +\tdx{inj_converse_inj} f: inj(A,B) ==> converse(f): inj(range(f), A)
  5.1214 +\tdx{bij_converse_bij} f: bij(A,B) ==> converse(f): bij(B,A)
  5.1215 +
  5.1216 +\tdx{comp_type}        [| s<=A*B;  r<=B*C |] ==> (r O s) <= A*C
  5.1217 +\tdx{comp_assoc}       (r O s) O t = r O (s O t)
  5.1218 +
  5.1219 +\tdx{left_comp_id}     r<=A*B ==> id(B) O r = r
  5.1220 +\tdx{right_comp_id}    r<=A*B ==> r O id(A) = r
  5.1221 +
  5.1222 +\tdx{comp_func}        [| g:A->B; f:B->C |] ==> (f O g):A->C
  5.1223 +\tdx{comp_func_apply}  [| g:A->B; f:B->C; a:A |] ==> (f O g)`a = f`(g`a)
  5.1224 +
  5.1225 +\tdx{comp_inj}         [| g:inj(A,B);  f:inj(B,C)  |] ==> (f O g):inj(A,C)
  5.1226 +\tdx{comp_surj}        [| g:surj(A,B); f:surj(B,C) |] ==> (f O g):surj(A,C)
  5.1227 +\tdx{comp_bij}         [| g:bij(A,B); f:bij(B,C) |] ==> (f O g):bij(A,C)
  5.1228 +
  5.1229 +\tdx{left_comp_inverse}     f: inj(A,B) ==> converse(f) O f = id(A)
  5.1230 +\tdx{right_comp_inverse}    f: surj(A,B) ==> f O converse(f) = id(B)
  5.1231 +
  5.1232 +\tdx{bij_disjoint_Un}   
  5.1233 +    [| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> 
  5.1234 +    (f Un g) : bij(A Un C, B Un D)
  5.1235 +
  5.1236 +\tdx{restrict_bij}  [| f:inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)
  5.1237 +\end{ttbox}
  5.1238 +\caption{Permutations} \label{zf-perm}
  5.1239 +\end{figure}
  5.1240 +
  5.1241 +The theory \thydx{Perm} is concerned with permutations (bijections) and
  5.1242 +related concepts.  These include composition of relations, the identity
  5.1243 +relation, and three specialized function spaces: injective, surjective and
  5.1244 +bijective.  Figure~\ref{zf-perm} displays many of their properties that
  5.1245 +have been proved.  These results are fundamental to a treatment of
  5.1246 +equipollence and cardinality.
  5.1247 +
  5.1248 +\begin{figure}\small
  5.1249 +\index{#*@{\tt\#*} symbol}
  5.1250 +\index{*div symbol}
  5.1251 +\index{*mod symbol}
  5.1252 +\index{#+@{\tt\#+} symbol}
  5.1253 +\index{#-@{\tt\#-} symbol}
  5.1254 +\begin{constants}
  5.1255 +  \it symbol  & \it meta-type & \it priority & \it description \\ 
  5.1256 +  \cdx{nat}     & $i$                   &       & set of natural numbers \\
  5.1257 +  \cdx{nat_case}& $[i,i\To i,i]\To i$     &     & conditional for $nat$\\
  5.1258 +  \tt \#*       & $[i,i]\To i$  &  Left 70      & multiplication \\
  5.1259 +  \tt div       & $[i,i]\To i$  &  Left 70      & division\\
  5.1260 +  \tt mod       & $[i,i]\To i$  &  Left 70      & modulus\\
  5.1261 +  \tt \#+       & $[i,i]\To i$  &  Left 65      & addition\\
  5.1262 +  \tt \#-       & $[i,i]\To i$  &  Left 65      & subtraction
  5.1263 +\end{constants}
  5.1264 +
  5.1265 +\begin{ttbox}
  5.1266 +\tdx{nat_def}  nat == lfp(lam r: Pow(Inf). {\ttlbrace}0{\ttrbrace} Un {\ttlbrace}succ(x). x:r{\ttrbrace}
  5.1267 +
  5.1268 +\tdx{mod_def}  m mod n == transrec(m, \%j f. if j:n then j else f`(j#-n))
  5.1269 +\tdx{div_def}  m div n == transrec(m, \%j f. if j:n then 0 else succ(f`(j#-n)))
  5.1270 +
  5.1271 +\tdx{nat_case_def}  nat_case(a,b,k) == 
  5.1272 +              THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))
  5.1273 +
  5.1274 +\tdx{nat_0I}        0 : nat
  5.1275 +\tdx{nat_succI}     n : nat ==> succ(n) : nat
  5.1276 +
  5.1277 +\tdx{nat_induct}        
  5.1278 +    [| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) 
  5.1279 +    |] ==> P(n)
  5.1280 +
  5.1281 +\tdx{nat_case_0}    nat_case(a,b,0) = a
  5.1282 +\tdx{nat_case_succ} nat_case(a,b,succ(m)) = b(m)
  5.1283 +
  5.1284 +\tdx{add_0}        0 #+ n = n
  5.1285 +\tdx{add_succ}     succ(m) #+ n = succ(m #+ n)
  5.1286 +
  5.1287 +\tdx{mult_type}     [| m:nat;  n:nat |] ==> m #* n : nat
  5.1288 +\tdx{mult_0}        0 #* n = 0
  5.1289 +\tdx{mult_succ}     succ(m) #* n = n #+ (m #* n)
  5.1290 +\tdx{mult_commute}  [| m:nat; n:nat |] ==> m #* n = n #* m
  5.1291 +\tdx{add_mult_dist} [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k){\thinspace}#+{\thinspace}(n #* k)
  5.1292 +\tdx{mult_assoc}
  5.1293 +    [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)
  5.1294 +\tdx{mod_quo_equality}
  5.1295 +    [| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m
  5.1296 +\end{ttbox}
  5.1297 +\caption{The natural numbers} \label{zf-nat}
  5.1298 +\end{figure}
  5.1299 +
  5.1300 +Theory \thydx{Nat} defines the natural numbers and mathematical
  5.1301 +induction, along with a case analysis operator.  The set of natural
  5.1302 +numbers, here called \texttt{nat}, is known in set theory as the ordinal~$\omega$.
  5.1303 +
  5.1304 +Theory \thydx{Arith} develops arithmetic on the natural numbers
  5.1305 +(Fig.\ts\ref{zf-nat}).  Addition, multiplication and subtraction are defined
  5.1306 +by primitive recursion.  Division and remainder are defined by repeated
  5.1307 +subtraction, which requires well-founded recursion; the termination argument
  5.1308 +relies on the divisor's being non-zero.  Many properties are proved:
  5.1309 +commutative, associative and distributive laws, identity and cancellation
  5.1310 +laws, etc.  The most interesting result is perhaps the theorem $a \bmod b +
  5.1311 +(a/b)\times b = a$.
  5.1312 +
  5.1313 +Theory \thydx{Univ} defines a `universe' $\texttt{univ}(A)$, which is used by
  5.1314 +the datatype package.  This set contains $A$ and the
  5.1315 +natural numbers.  Vitally, it is closed under finite products: ${\tt
  5.1316 +  univ}(A)\times{\tt univ}(A)\subseteq{\tt univ}(A)$.  This theory also
  5.1317 +defines the cumulative hierarchy of axiomatic set theory, which
  5.1318 +traditionally is written $V@\alpha$ for an ordinal~$\alpha$.  The
  5.1319 +`universe' is a simple generalization of~$V@\omega$.
  5.1320 +
  5.1321 +Theory \thydx{QUniv} defines a `universe' ${\tt quniv}(A)$, which is used by
  5.1322 +the datatype package to construct codatatypes such as streams.  It is
  5.1323 +analogous to ${\tt univ}(A)$ (and is defined in terms of it) but is closed
  5.1324 +under the non-standard product and sum.
  5.1325 +
  5.1326 +Theory \texttt{Finite} (Figure~\ref{zf-fin}) defines the finite set operator;
  5.1327 +${\tt Fin}(A)$ is the set of all finite sets over~$A$.  The theory employs
  5.1328 +Isabelle's inductive definition package, which proves various rules
  5.1329 +automatically.  The induction rule shown is stronger than the one proved by
  5.1330 +the package.  The theory also defines the set of all finite functions
  5.1331 +between two given sets.
  5.1332 +
  5.1333 +\begin{figure}
  5.1334 +\begin{ttbox}
  5.1335 +\tdx{Fin.emptyI}      0 : Fin(A)
  5.1336 +\tdx{Fin.consI}       [| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)
  5.1337 +
  5.1338 +\tdx{Fin_induct}
  5.1339 +    [| b: Fin(A);
  5.1340 +       P(0);
  5.1341 +       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y))
  5.1342 +    |] ==> P(b)
  5.1343 +
  5.1344 +\tdx{Fin_mono}        A<=B ==> Fin(A) <= Fin(B)
  5.1345 +\tdx{Fin_UnI}         [| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)
  5.1346 +\tdx{Fin_UnionI}      C : Fin(Fin(A)) ==> Union(C) : Fin(A)
  5.1347 +\tdx{Fin_subset}      [| c<=b;  b: Fin(A) |] ==> c: Fin(A)
  5.1348 +\end{ttbox}
  5.1349 +\caption{The finite set operator} \label{zf-fin}
  5.1350 +\end{figure}
  5.1351 +
  5.1352 +\begin{figure}
  5.1353 +\begin{constants}
  5.1354 +  \it symbol  & \it meta-type & \it priority & \it description \\ 
  5.1355 +  \cdx{list}    & $i\To i$      && lists over some set\\
  5.1356 +  \cdx{list_case} & $[i, [i,i]\To i, i] \To i$  && conditional for $list(A)$ \\
  5.1357 +  \cdx{map}     & $[i\To i, i] \To i$   &       & mapping functional\\
  5.1358 +  \cdx{length}  & $i\To i$              &       & length of a list\\
  5.1359 +  \cdx{rev}     & $i\To i$              &       & reverse of a list\\
  5.1360 +  \tt \at       & $[i,i]\To i$  &  Right 60     & append for lists\\
  5.1361 +  \cdx{flat}    & $i\To i$   &                  & append of list of lists
  5.1362 +\end{constants}
  5.1363 +
  5.1364 +\underscoreon %%because @ is used here
  5.1365 +\begin{ttbox}
  5.1366 +\tdx{NilI}            Nil : list(A)
  5.1367 +\tdx{ConsI}           [| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)
  5.1368 +
  5.1369 +\tdx{List.induct}
  5.1370 +    [| l: list(A);
  5.1371 +       P(Nil);
  5.1372 +       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(Cons(x,y))
  5.1373 +    |] ==> P(l)
  5.1374 +
  5.1375 +\tdx{Cons_iff}        Cons(a,l)=Cons(a',l') <-> a=a' & l=l'
  5.1376 +\tdx{Nil_Cons_iff}    ~ Nil=Cons(a,l)
  5.1377 +
  5.1378 +\tdx{list_mono}       A<=B ==> list(A) <= list(B)
  5.1379 +
  5.1380 +\tdx{map_ident}       l: list(A) ==> map(\%u. u, l) = l
  5.1381 +\tdx{map_compose}     l: list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l)
  5.1382 +\tdx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)
  5.1383 +\tdx{map_type}
  5.1384 +    [| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)
  5.1385 +\tdx{map_flat}
  5.1386 +    ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))
  5.1387 +\end{ttbox}
  5.1388 +\caption{Lists} \label{zf-list}
  5.1389 +\end{figure}
  5.1390 +
  5.1391 +
  5.1392 +Figure~\ref{zf-list} presents the set of lists over~$A$, ${\tt list}(A)$.  The
  5.1393 +definition employs Isabelle's datatype package, which defines the introduction
  5.1394 +and induction rules automatically, as well as the constructors, case operator
  5.1395 +(\verb|list_case|) and recursion operator.  The theory then defines the usual
  5.1396 +list functions by primitive recursion.  See theory \texttt{List}.
  5.1397 +
  5.1398 +
  5.1399 +\section{Simplification and classical reasoning}
  5.1400 +
  5.1401 +{\ZF} inherits simplification from {\FOL} but adopts it for set theory.  The
  5.1402 +extraction of rewrite rules takes the {\ZF} primitives into account.  It can
  5.1403 +strip bounded universal quantifiers from a formula; for example, ${\forall
  5.1404 +  x\in A. f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp
  5.1405 +f(x)=g(x)$.  Given $a\in\{x\in A. P(x)\}$ it extracts rewrite rules from $a\in
  5.1406 +A$ and~$P(a)$.  It can also break down $a\in A\int B$ and $a\in A-B$.
  5.1407 +
  5.1408 +Simplification tactics tactics such as \texttt{Asm_simp_tac} and
  5.1409 +\texttt{Full_simp_tac} use the default simpset (\texttt{simpset()}), which
  5.1410 +works for most purposes.  A small simplification set for set theory is
  5.1411 +called~\ttindexbold{ZF_ss}, and you can even use \ttindex{FOL_ss} as a minimal
  5.1412 +starting point.  \texttt{ZF_ss} contains congruence rules for all the binding
  5.1413 +operators of {\ZF}\@.  It contains all the conversion rules, such as
  5.1414 +\texttt{fst} and \texttt{snd}, as well as the rewrites shown in
  5.1415 +Fig.\ts\ref{zf-simpdata}.  See the file \texttt{ZF/simpdata.ML} for a fuller
  5.1416 +list.
  5.1417 +
  5.1418 +As for the classical reasoner, tactics such as \texttt{Blast_tac} and {\tt
  5.1419 +  Best_tac} refer to the default claset (\texttt{claset()}).  This works for
  5.1420 +most purposes.  Named clasets include \ttindexbold{ZF_cs} (basic set theory)
  5.1421 +and \ttindexbold{le_cs} (useful for reasoning about the relations $<$ and
  5.1422 +$\le$).  You can use \ttindex{FOL_cs} as a minimal basis for building your own
  5.1423 +clasets.  See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
  5.1424 +{Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.
  5.1425 +
  5.1426 +
  5.1427 +\begin{figure}
  5.1428 +\begin{eqnarray*}
  5.1429 +  a\in \emptyset        & \bimp &  \bot\\
  5.1430 +  a \in A \un B      & \bimp &  a\in A \disj a\in B\\
  5.1431 +  a \in A \int B      & \bimp &  a\in A \conj a\in B\\
  5.1432 +  a \in A-B             & \bimp &  a\in A \conj \neg (a\in B)\\
  5.1433 +  \pair{a,b}\in {\tt Sigma}(A,B)
  5.1434 +                        & \bimp &  a\in A \conj b\in B(a)\\
  5.1435 +  a \in {\tt Collect}(A,P)      & \bimp &  a\in A \conj P(a)\\
  5.1436 +  (\forall x \in \emptyset. P(x)) & \bimp &  \top\\
  5.1437 +  (\forall x \in A. \top)       & \bimp &  \top
  5.1438 +\end{eqnarray*}
  5.1439 +\caption{Some rewrite rules for set theory} \label{zf-simpdata}
  5.1440 +\end{figure}
  5.1441 +
  5.1442 +
  5.1443 +\section{Datatype definitions}
  5.1444 +\label{sec:ZF:datatype}
  5.1445 +\index{*datatype|(}
  5.1446 +
  5.1447 +The \ttindex{datatype} definition package of \ZF\ constructs inductive
  5.1448 +datatypes similar to those of \ML.  It can also construct coinductive
  5.1449 +datatypes (codatatypes), which are non-well-founded structures such as
  5.1450 +streams.  It defines the set using a fixed-point construction and proves
  5.1451 +induction rules, as well as theorems for recursion and case combinators.  It
  5.1452 +supplies mechanisms for reasoning about freeness.  The datatype package can
  5.1453 +handle both mutual and indirect recursion.
  5.1454 +
  5.1455 +
  5.1456 +\subsection{Basics}
  5.1457 +\label{subsec:datatype:basics}
  5.1458 +
  5.1459 +A \texttt{datatype} definition has the following form:
  5.1460 +\[
  5.1461 +\begin{array}{llcl}
  5.1462 +\mathtt{datatype} & t@1(A@1,\ldots,A@h) & = &
  5.1463 +  constructor^1@1 ~\mid~ \ldots ~\mid~ constructor^1@{k@1} \\
  5.1464 + & & \vdots \\
  5.1465 +\mathtt{and} & t@n(A@1,\ldots,A@h) & = &
  5.1466 +  constructor^n@1~ ~\mid~ \ldots ~\mid~ constructor^n@{k@n}
  5.1467 +\end{array}
  5.1468 +\]
  5.1469 +Here $t@1$, \ldots,~$t@n$ are identifiers and $A@1$, \ldots,~$A@h$ are
  5.1470 +variables: the datatype's parameters.  Each constructor specification has the
  5.1471 +form \dquotesoff
  5.1472 +\[ C \hbox{\tt~( } \hbox{\tt"} x@1 \hbox{\tt:} T@1 \hbox{\tt"},\;
  5.1473 +                   \ldots,\;
  5.1474 +                   \hbox{\tt"} x@m \hbox{\tt:} T@m \hbox{\tt"}
  5.1475 +     \hbox{\tt~)}
  5.1476 +\]
  5.1477 +Here $C$ is the constructor name, and variables $x@1$, \ldots,~$x@m$ are the
  5.1478 +constructor arguments, belonging to the sets $T@1$, \ldots, $T@m$,
  5.1479 +respectively.  Typically each $T@j$ is either a constant set, a datatype
  5.1480 +parameter (one of $A@1$, \ldots, $A@h$) or a recursive occurrence of one of
  5.1481 +the datatypes, say $t@i(A@1,\ldots,A@h)$.  More complex possibilities exist,
  5.1482 +but they are much harder to realize.  Often, additional information must be
  5.1483 +supplied in the form of theorems.
  5.1484 +
  5.1485 +A datatype can occur recursively as the argument of some function~$F$.  This
  5.1486 +is called a {\em nested} (or \emph{indirect}) occurrence.  It is only allowed
  5.1487 +if the datatype package is given a theorem asserting that $F$ is monotonic.
  5.1488 +If the datatype has indirect occurrences, then Isabelle/ZF does not support
  5.1489 +recursive function definitions.
  5.1490 +
  5.1491 +A simple example of a datatype is \texttt{list}, which is built-in, and is
  5.1492 +defined by
  5.1493 +\begin{ttbox}
  5.1494 +consts     list :: i=>i
  5.1495 +datatype  "list(A)" = Nil | Cons ("a:A", "l: list(A)")
  5.1496 +\end{ttbox}
  5.1497 +Note that the datatype operator must be declared as a constant first.
  5.1498 +However, the package declares the constructors.  Here, \texttt{Nil} gets type
  5.1499 +$i$ and \texttt{Cons} gets type $[i,i]\To i$.
  5.1500 +
  5.1501 +Trees and forests can be modelled by the mutually recursive datatype
  5.1502 +definition
  5.1503 +\begin{ttbox}
  5.1504 +consts     tree, forest, tree_forest :: i=>i
  5.1505 +datatype  "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
  5.1506 +and       "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
  5.1507 +\end{ttbox}
  5.1508 +Here $\texttt{tree}(A)$ is the set of trees over $A$, $\texttt{forest}(A)$ is
  5.1509 +the set of forests over $A$, and  $\texttt{tree_forest}(A)$ is the union of
  5.1510 +the previous two sets.  All three operators must be declared first.
  5.1511 +
  5.1512 +The datatype \texttt{term}, which is defined by
  5.1513 +\begin{ttbox}
  5.1514 +consts     term :: i=>i
  5.1515 +datatype  "term(A)" = Apply ("a: A", "l: list(term(A))")
  5.1516 +  monos "[list_mono]"
  5.1517 +\end{ttbox}
  5.1518 +is an example of nested recursion.  (The theorem \texttt{list_mono} is proved
  5.1519 +in file \texttt{List.ML}, and the \texttt{term} example is devaloped in theory
  5.1520 +\thydx{ex/Term}.)
  5.1521 +
  5.1522 +\subsubsection{Freeness of the constructors}
  5.1523 +
  5.1524 +Constructors satisfy {\em freeness} properties.  Constructions are distinct,
  5.1525 +for example $\texttt{Nil}\not=\texttt{Cons}(a,l)$, and they are injective, for
  5.1526 +example $\texttt{Cons}(a,l)=\texttt{Cons}(a',l') \bimp a=a' \conj l=l'$.
  5.1527 +Because the number of freeness is quadratic in the number of constructors, the
  5.1528 +datatype package does not prove them, but instead provides several means of
  5.1529 +proving them dynamically.  For the \texttt{list} datatype, freeness reasoning
  5.1530 +can be done in two ways: by simplifying with the theorems
  5.1531 +\texttt{list.free_iffs} or by invoking the classical reasoner with
  5.1532 +\texttt{list.free_SEs} as safe elimination rules.  Occasionally this exposes
  5.1533 +the underlying representation of some constructor, which can be rectified
  5.1534 +using the command \hbox{\tt fold_tac list.con_defs}.
  5.1535 +
  5.1536 +\subsubsection{Structural induction}
  5.1537 +
  5.1538 +The datatype package also provides structural induction rules.  For datatypes
  5.1539 +without mutual or nested recursion, the rule has the form exemplified by
  5.1540 +\texttt{list.induct} in Fig.\ts\ref{zf-list}.  For mutually recursive
  5.1541 +datatypes, the induction rule is supplied in two forms.  Consider datatype
  5.1542 +\texttt{TF}.  The rule \texttt{tree_forest.induct} performs induction over a
  5.1543 +single predicate~\texttt{P}, which is presumed to be defined for both trees
  5.1544 +and forests:
  5.1545 +\begin{ttbox}
  5.1546 +[| x : tree_forest(A);
  5.1547 +   !!a f. [| a : A; f : forest(A); P(f) |] ==> P(Tcons(a, f)); P(Fnil);
  5.1548 +   !!f t. [| t : tree(A); P(t); f : forest(A); P(f) |]
  5.1549 +          ==> P(Fcons(t, f)) 
  5.1550 +|] ==> P(x)
  5.1551 +\end{ttbox}
  5.1552 +The rule \texttt{tree_forest.mutual_induct} performs induction over two
  5.1553 +distinct predicates, \texttt{P_tree} and \texttt{P_forest}.
  5.1554 +\begin{ttbox}
  5.1555 +[| !!a f.
  5.1556 +      [| a : A; f : forest(A); P_forest(f) |] ==> P_tree(Tcons(a, f));
  5.1557 +   P_forest(Fnil);
  5.1558 +   !!f t. [| t : tree(A); P_tree(t); f : forest(A); P_forest(f) |]
  5.1559 +          ==> P_forest(Fcons(t, f)) 
  5.1560 +|] ==> (ALL za. za : tree(A) --> P_tree(za)) &
  5.1561 +    (ALL za. za : forest(A) --> P_forest(za))
  5.1562 +\end{ttbox}
  5.1563 +
  5.1564 +For datatypes with nested recursion, such as the \texttt{term} example from
  5.1565 +above, things are a bit more complicated.  The rule \texttt{term.induct}
  5.1566 +refers to the monotonic operator, \texttt{list}:
  5.1567 +\begin{ttbox}
  5.1568 +[| x : term(A);
  5.1569 +   !!a l. [| a : A; l : list(Collect(term(A), P)) |] ==> P(Apply(a, l)) 
  5.1570 +|] ==> P(x)
  5.1571 +\end{ttbox}
  5.1572 +The file \texttt{ex/Term.ML} derives two higher-level induction rules, one of
  5.1573 +which is particularly useful for proving equations:
  5.1574 +\begin{ttbox}
  5.1575 +[| t : term(A);
  5.1576 +   !!x zs. [| x : A; zs : list(term(A)); map(f, zs) = map(g, zs) |]
  5.1577 +           ==> f(Apply(x, zs)) = g(Apply(x, zs)) 
  5.1578 +|] ==> f(t) = g(t)  
  5.1579 +\end{ttbox}
  5.1580 +How this can be generalized to other nested datatypes is a matter for future
  5.1581 +research.
  5.1582 +
  5.1583 +
  5.1584 +\subsubsection{The \texttt{case} operator}
  5.1585 +
  5.1586 +The package defines an operator for performing case analysis over the
  5.1587 +datatype.  For \texttt{list}, it is called \texttt{list_case} and satisfies
  5.1588 +the equations
  5.1589 +\begin{ttbox}
  5.1590 +list_case(f_Nil, f_Cons, []) = f_Nil
  5.1591 +list_case(f_Nil, f_Cons, Cons(a, l)) = f_Cons(a, l)
  5.1592 +\end{ttbox}
  5.1593 +Here \texttt{f_Nil} is the value to return if the argument is \texttt{Nil} and
  5.1594 +\texttt{f_Cons} is a function that computes the value to return if the
  5.1595 +argument has the form $\texttt{Cons}(a,l)$.  The function can be expressed as
  5.1596 +an abstraction, over patterns if desired (\S\ref{sec:pairs}).
  5.1597 +
  5.1598 +For mutually recursive datatypes, there is a single \texttt{case} operator.
  5.1599 +In the tree/forest example, the constant \texttt{tree_forest_case} handles all
  5.1600 +of the constructors of the two datatypes.
  5.1601 +
  5.1602 +
  5.1603 +
  5.1604 +
  5.1605 +\subsection{Defining datatypes}
  5.1606 +
  5.1607 +The theory syntax for datatype definitions is shown in
  5.1608 +Fig.~\ref{datatype-grammar}.  In order to be well-formed, a datatype
  5.1609 +definition has to obey the rules stated in the previous section.  As a result
  5.1610 +the theory is extended with the new types, the constructors, and the theorems
  5.1611 +listed in the previous section.  The quotation marks are necessary because
  5.1612 +they enclose general Isabelle formul\ae.
  5.1613 +
  5.1614 +\begin{figure}
  5.1615 +\begin{rail}
  5.1616 +datatype : ( 'datatype' | 'codatatype' ) datadecls;
  5.1617 +
  5.1618 +datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and'
  5.1619 +         ;
  5.1620 +constructor : name ( () | consargs )  ( () | ( '(' mixfix ')' ) )
  5.1621 +         ;
  5.1622 +consargs : '(' ('"' var ':' term '"' + ',') ')'
  5.1623 +         ;
  5.1624 +\end{rail}
  5.1625 +\caption{Syntax of datatype declarations}
  5.1626 +\label{datatype-grammar}
  5.1627 +\end{figure}
  5.1628 +
  5.1629 +Codatatypes are declared like datatypes and are identical to them in every
  5.1630 +respect except that they have a coinduction rule instead of an induction rule.
  5.1631 +Note that while an induction rule has the effect of limiting the values
  5.1632 +contained in the set, a coinduction rule gives a way of constructing new
  5.1633 +values of the set.
  5.1634 +
  5.1635 +Most of the theorems about datatypes become part of the default simpset.  You
  5.1636 +never need to see them again because the simplifier applies them
  5.1637 +automatically.  Add freeness properties (\texttt{free_iffs}) to the simpset
  5.1638 +when you want them.  Induction or exhaustion are usually invoked by hand,
  5.1639 +usually via these special-purpose tactics:
  5.1640 +\begin{ttdescription}
  5.1641 +\item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] applies structural
  5.1642 +  induction on variable $x$ to subgoal $i$, provided the type of $x$ is a
  5.1643 +  datatype.  The induction variable should not occur among other assumptions
  5.1644 +  of the subgoal.
  5.1645 +\end{ttdescription}
  5.1646 +In some cases, induction is overkill and a case distinction over all
  5.1647 +constructors of the datatype suffices.
  5.1648 +\begin{ttdescription}
  5.1649 +\item[\ttindexbold{exhaust_tac} {\tt"}$x${\tt"} $i$]
  5.1650 + performs an exhaustive case analysis for the variable~$x$.
  5.1651 +\end{ttdescription}
  5.1652 +
  5.1653 +Both tactics can only be applied to a variable, whose typing must be given in
  5.1654 +some assumption, for example the assumption \texttt{x:\ list(A)}.  The tactics
  5.1655 +also work for the natural numbers (\texttt{nat}) and disjoint sums, although
  5.1656 +these sets were not defined using the datatype package.  (Disjoint sums are
  5.1657 +not recursive, so only \texttt{exhaust_tac} is available.)
  5.1658 +
  5.1659 +\bigskip
  5.1660 +Here are some more details for the technically minded.  Processing the
  5.1661 +theory file produces an \ML\ structure which, in addition to the usual
  5.1662 +components, contains a structure named $t$ for each datatype $t$ defined in
  5.1663 +the file.  Each structure $t$ contains the following elements:
  5.1664 +\begin{ttbox}
  5.1665 +val intrs         : thm list  \textrm{the introduction rules}
  5.1666 +val elim          : thm       \textrm{the elimination (case analysis) rule}
  5.1667 +val induct        : thm       \textrm{the standard induction rule}
  5.1668 +val mutual_induct : thm       \textrm{the mutual induction rule, or \texttt{True}}
  5.1669 +val case_eqns     : thm list  \textrm{equations for the case operator}
  5.1670 +val recursor_eqns : thm list  \textrm{equations for the recursor}
  5.1671 +val con_defs      : thm list  \textrm{definitions of the case operator and constructors}
  5.1672 +val free_iffs     : thm list  \textrm{logical equivalences for proving freeness}
  5.1673 +val free_SEs      : thm list  \textrm{elimination rules for proving freeness}
  5.1674 +val mk_free       : string -> thm  \textrm{A function for proving freeness theorems}
  5.1675 +val mk_cases      : thm list -> string -> thm  \textrm{case analysis, see below}
  5.1676 +val defs          : thm list  \textrm{definitions of operators}
  5.1677 +val bnd_mono      : thm list  \textrm{monotonicity property}
  5.1678 +val dom_subset    : thm list  \textrm{inclusion in `bounding set'}
  5.1679 +\end{ttbox}
  5.1680 +Furthermore there is the theorem $C$\texttt{_I} for every constructor~$C$; for
  5.1681 +example, the \texttt{list} datatype's introduction rules are bound to the
  5.1682 +identifiers \texttt{Nil_I} and \texttt{Cons_I}.
  5.1683 +
  5.1684 +For a codatatype, the component \texttt{coinduct} is the coinduction rule,
  5.1685 +replacing the \texttt{induct} component.
  5.1686 +
  5.1687 +See the theories \texttt{ex/Ntree} and \texttt{ex/Brouwer} for examples of
  5.1688 +infinitely branching datatypes.  See theory \texttt{ex/LList} for an example
  5.1689 +of a codatatype.  Some of these theories illustrate the use of additional,
  5.1690 +undocumented features of the datatype package.  Datatype definitions are
  5.1691 +reduced to inductive definitions, and the advanced features should be
  5.1692 +understood in that light.
  5.1693 +
  5.1694 +
  5.1695 +\subsection{Examples}
  5.1696 +
  5.1697 +\subsubsection{The datatype of binary trees}
  5.1698 +
  5.1699 +Let us define the set $\texttt{bt}(A)$ of binary trees over~$A$.  The theory
  5.1700 +must contain these lines:
  5.1701 +\begin{ttbox}
  5.1702 +consts   bt :: i=>i
  5.1703 +datatype "bt(A)"  =  Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
  5.1704 +\end{ttbox}
  5.1705 +After loading the theory, we can prove, for example, that no tree equals its
  5.1706 +left branch.  To ease the induction, we state the goal using quantifiers.
  5.1707 +\begin{ttbox}
  5.1708 +Goal "l : bt(A) ==> ALL x r. Br(x,l,r) ~= l";
  5.1709 +{\out Level 0}
  5.1710 +{\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l}
  5.1711 +{\out  1. l : bt(A) ==> ALL x r. Br(x, l, r) ~= l}
  5.1712 +\end{ttbox}
  5.1713 +This can be proved by the structural induction tactic:
  5.1714 +\begin{ttbox}
  5.1715 +by (induct_tac "l" 1);
  5.1716 +{\out Level 1}
  5.1717 +{\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l}
  5.1718 +{\out  1. ALL x r. Br(x, Lf, r) ~= Lf}
  5.1719 +{\out  2. !!a t1 t2.}
  5.1720 +{\out        [| a : A; t1 : bt(A); ALL x r. Br(x, t1, r) ~= t1; t2 : bt(A);}
  5.1721 +{\out           ALL x r. Br(x, t2, r) ~= t2 |]}
  5.1722 +{\out        ==> ALL x r. Br(x, Br(a, t1, t2), r) ~= Br(a, t1, t2)}
  5.1723 +\end{ttbox}
  5.1724 +Both subgoals are proved using the simplifier.  Tactic
  5.1725 +\texttt{asm_full_simp_tac} is used, rewriting the assumptions.
  5.1726 +This is because simplification using the freeness properties can unfold the
  5.1727 +definition of constructor~\texttt{Br}, so we arrange that all occurrences are
  5.1728 +unfolded. 
  5.1729 +\begin{ttbox}
  5.1730 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps bt.free_iffs)));
  5.1731 +{\out Level 2}
  5.1732 +{\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l}
  5.1733 +{\out No subgoals!}
  5.1734 +\end{ttbox}
  5.1735 +To remove the quantifiers from the induction formula, we save the theorem using
  5.1736 +\ttindex{qed_spec_mp}.
  5.1737 +\begin{ttbox}
  5.1738 +qed_spec_mp "Br_neq_left";
  5.1739 +{\out val Br_neq_left = "?l : bt(?A) ==> Br(?x, ?l, ?r) ~= ?l" : thm}
  5.1740 +\end{ttbox}
  5.1741 +
  5.1742 +When there are only a few constructors, we might prefer to prove the freenness
  5.1743 +theorems for each constructor.  This is trivial, using the function given us
  5.1744 +for that purpose:
  5.1745 +\begin{ttbox}
  5.1746 +val Br_iff = bt.mk_free "Br(a,l,r)=Br(a',l',r') <-> a=a' & l=l' & r=r'";
  5.1747 +{\out val Br_iff =}
  5.1748 +{\out   "Br(?a, ?l, ?r) = Br(?a', ?l', ?r') <->}
  5.1749 +{\out                     ?a = ?a' & ?l = ?l' & ?r = ?r'" : thm}
  5.1750 +\end{ttbox}
  5.1751 +
  5.1752 +The purpose of \ttindex{mk_cases} is to generate simplified instances of the
  5.1753 +elimination (case analysis) rule.  Its theorem list argument is a list of
  5.1754 +constructor definitions, which it uses for freeness reasoning.  For example,
  5.1755 +this instance of the elimination rule propagates type-checking information
  5.1756 +from the premise $\texttt{Br}(a,l,r)\in\texttt{bt}(A)$:
  5.1757 +\begin{ttbox}
  5.1758 +val BrE = bt.mk_cases bt.con_defs "Br(a,l,r) : bt(A)";
  5.1759 +{\out val BrE =}
  5.1760 +{\out   "[| Br(?a, ?l, ?r) : bt(?A);}
  5.1761 +{\out       [| ?a : ?A; ?l : bt(?A); ?r : bt(?A) |] ==> ?Q |] ==> ?Q" : thm}
  5.1762 +\end{ttbox}
  5.1763 +
  5.1764 +
  5.1765 +\subsubsection{Mixfix syntax in datatypes}
  5.1766 +
  5.1767 +Mixfix syntax is sometimes convenient.  The theory \texttt{ex/PropLog} makes a
  5.1768 +deep embedding of propositional logic:
  5.1769 +\begin{ttbox}
  5.1770 +consts     prop :: i
  5.1771 +datatype  "prop" = Fls
  5.1772 +                 | Var ("n: nat")                ("#_" [100] 100)
  5.1773 +                 | "=>" ("p: prop", "q: prop")   (infixr 90)
  5.1774 +\end{ttbox}
  5.1775 +The second constructor has a special $\#n$ syntax, while the third constructor
  5.1776 +is an infixed arrow.
  5.1777 +
  5.1778 +
  5.1779 +\subsubsection{A giant enumeration type}
  5.1780 +
  5.1781 +This example shows a datatype that consists of 60 constructors:
  5.1782 +\begin{ttbox}
  5.1783 +consts  enum :: i
  5.1784 +datatype
  5.1785 +  "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
  5.1786 +         | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19
  5.1787 +         | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29
  5.1788 +         | C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39
  5.1789 +         | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49
  5.1790 +         | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59
  5.1791 +end
  5.1792 +\end{ttbox}
  5.1793 +The datatype package scales well.  Even though all properties are proved
  5.1794 +rather than assumed, full processing of this definition takes under 15 seconds
  5.1795 +(on a 300 MHz Pentium).  The constructors have a balanced representation,
  5.1796 +essentially binary notation, so freeness properties can be proved fast.
  5.1797 +\begin{ttbox}
  5.1798 +Goal "C00 ~= C01";
  5.1799 +by (simp_tac (simpset() addsimps enum.free_iffs) 1);
  5.1800 +\end{ttbox}
  5.1801 +You need not derive such inequalities explicitly.  The simplifier will dispose
  5.1802 +of them automatically, given the theorem list \texttt{free_iffs}.
  5.1803 +
  5.1804 +\index{*datatype|)}
  5.1805 +
  5.1806 +
  5.1807 +\subsection{Recursive function definitions}\label{sec:ZF:recursive}
  5.1808 +\index{recursive functions|see{recursion}}
  5.1809 +\index{*primrec|(}
  5.1810 +
  5.1811 +Datatypes come with a uniform way of defining functions, {\bf primitive
  5.1812 +  recursion}.  Such definitions rely on the recursion operator defined by the
  5.1813 +datatype package.  Isabelle proves the desired recursion equations as
  5.1814 +theorems.
  5.1815 +
  5.1816 +In principle, one could introduce primitive recursive functions by asserting
  5.1817 +their reduction rules as new axioms.  Here is a dangerous way of defining the
  5.1818 +append function for lists:
  5.1819 +\begin{ttbox}\slshape
  5.1820 +consts  "\at" :: [i,i]=>i                        (infixr 60)
  5.1821 +rules 
  5.1822 +   app_Nil   "[] \at ys = ys"
  5.1823 +   app_Cons  "(Cons(a,l)) \at ys = Cons(a, l \at ys)"
  5.1824 +\end{ttbox}
  5.1825 +Asserting axioms brings the danger of accidentally asserting nonsense.  It
  5.1826 +should be avoided at all costs!
  5.1827 +
  5.1828 +The \ttindex{primrec} declaration is a safe means of defining primitive
  5.1829 +recursive functions on datatypes:
  5.1830 +\begin{ttbox}
  5.1831 +consts  "\at" :: [i,i]=>i                        (infixr 60)
  5.1832 +primrec 
  5.1833 +   "[] \at ys = ys"
  5.1834 +   "(Cons(a,l)) \at ys = Cons(a, l \at ys)"
  5.1835 +\end{ttbox}
  5.1836 +Isabelle will now check that the two rules do indeed form a primitive
  5.1837 +recursive definition.  For example, the declaration
  5.1838 +\begin{ttbox}
  5.1839 +primrec
  5.1840 +   "[] \at ys = us"
  5.1841 +\end{ttbox}
  5.1842 +is rejected with an error message ``\texttt{Extra variables on rhs}''.
  5.1843 +
  5.1844 +
  5.1845 +\subsubsection{Syntax of recursive definitions}
  5.1846 +
  5.1847 +The general form of a primitive recursive definition is
  5.1848 +\begin{ttbox}
  5.1849 +primrec
  5.1850 +    {\it reduction rules}
  5.1851 +\end{ttbox}
  5.1852 +where \textit{reduction rules} specify one or more equations of the form
  5.1853 +\[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,
  5.1854 +\dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$
  5.1855 +contains only the free variables on the left-hand side, and all recursive
  5.1856 +calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$.  
  5.1857 +There must be at most one reduction rule for each constructor.  The order is
  5.1858 +immaterial.  For missing constructors, the function is defined to return zero.
  5.1859 +
  5.1860 +All reduction rules are added to the default simpset.
  5.1861 +If you would like to refer to some rule by name, then you must prefix
  5.1862 +the rule with an identifier.  These identifiers, like those in the
  5.1863 +\texttt{rules} section of a theory, will be visible at the \ML\ level.
  5.1864 +
  5.1865 +The reduction rules for {\tt\at} become part of the default simpset, which
  5.1866 +leads to short proof scripts:
  5.1867 +\begin{ttbox}\underscoreon
  5.1868 +Goal "xs: list(A) ==> (xs @ ys) @ zs = xs @ (ys @ zs)";
  5.1869 +by (induct\_tac "xs" 1);
  5.1870 +by (ALLGOALS Asm\_simp\_tac);
  5.1871 +\end{ttbox}
  5.1872 +
  5.1873 +You can even use the \texttt{primrec} form with non-recursive datatypes and
  5.1874 +with codatatypes.  Recursion is not allowed, but it provides a convenient
  5.1875 +syntax for defining functions by cases.
  5.1876 +
  5.1877 +
  5.1878 +\subsubsection{Example: varying arguments}
  5.1879 +
  5.1880 +All arguments, other than the recursive one, must be the same in each equation
  5.1881 +and in each recursive call.  To get around this restriction, use explict
  5.1882 +$\lambda$-abstraction and function application.  Here is an example, drawn
  5.1883 +from the theory \texttt{Resid/Substitution}.  The type of redexes is declared
  5.1884 +as follows:
  5.1885 +\begin{ttbox}
  5.1886 +consts  redexes :: i
  5.1887 +datatype
  5.1888 +  "redexes" = Var ("n: nat")            
  5.1889 +            | Fun ("t: redexes")
  5.1890 +            | App ("b:bool" ,"f:redexes" , "a:redexes")
  5.1891 +\end{ttbox}
  5.1892 +
  5.1893 +The function \texttt{lift} takes a second argument, $k$, which varies in
  5.1894 +recursive calls.
  5.1895 +\begin{ttbox}
  5.1896 +primrec
  5.1897 +  "lift(Var(i)) = (lam k:nat. if i<k then Var(i) else Var(succ(i)))"
  5.1898 +  "lift(Fun(t)) = (lam k:nat. Fun(lift(t) ` succ(k)))"
  5.1899 +  "lift(App(b,f,a)) = (lam k:nat. App(b, lift(f)`k, lift(a)`k))"
  5.1900 +\end{ttbox}
  5.1901 +Now \texttt{lift(r)`k} satisfies the required recursion equations.
  5.1902 +
  5.1903 +\index{recursion!primitive|)}
  5.1904 +\index{*primrec|)}
  5.1905 +
  5.1906 +
  5.1907 +\section{Inductive and coinductive definitions}
  5.1908 +\index{*inductive|(}
  5.1909 +\index{*coinductive|(}
  5.1910 +
  5.1911 +An {\bf inductive definition} specifies the least set~$R$ closed under given
  5.1912 +rules.  (Applying a rule to elements of~$R$ yields a result within~$R$.)  For
  5.1913 +example, a structural operational semantics is an inductive definition of an
  5.1914 +evaluation relation.  Dually, a {\bf coinductive definition} specifies the
  5.1915 +greatest set~$R$ consistent with given rules.  (Every element of~$R$ can be
  5.1916 +seen as arising by applying a rule to elements of~$R$.)  An important example
  5.1917 +is using bisimulation relations to formalise equivalence of processes and
  5.1918 +infinite data structures.
  5.1919 +
  5.1920 +A theory file may contain any number of inductive and coinductive
  5.1921 +definitions.  They may be intermixed with other declarations; in
  5.1922 +particular, the (co)inductive sets {\bf must} be declared separately as
  5.1923 +constants, and may have mixfix syntax or be subject to syntax translations.
  5.1924 +
  5.1925 +Each (co)inductive definition adds definitions to the theory and also
  5.1926 +proves some theorems.  Each definition creates an \ML\ structure, which is a
  5.1927 +substructure of the main theory structure.
  5.1928 +This package is described in detail in a separate paper,%
  5.1929 +\footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
  5.1930 +  distributed with Isabelle as \emph{A Fixedpoint Approach to 
  5.1931 + (Co)Inductive and (Co)Datatype Definitions}.}  %
  5.1932 +which you might refer to for background information.
  5.1933 +
  5.1934 +
  5.1935 +\subsection{The syntax of a (co)inductive definition}
  5.1936 +An inductive definition has the form
  5.1937 +\begin{ttbox}
  5.1938 +inductive
  5.1939 +  domains    {\it domain declarations}
  5.1940 +  intrs      {\it introduction rules}
  5.1941 +  monos      {\it monotonicity theorems}
  5.1942 +  con_defs   {\it constructor definitions}
  5.1943 +  type_intrs {\it introduction rules for type-checking}
  5.1944 +  type_elims {\it elimination rules for type-checking}
  5.1945 +\end{ttbox}
  5.1946 +A coinductive definition is identical, but starts with the keyword
  5.1947 +{\tt coinductive}.  
  5.1948 +
  5.1949 +The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}
  5.1950 +sections are optional.  If present, each is specified either as a list of
  5.1951 +identifiers or as a string.  If the latter, then the string must be a valid
  5.1952 +\textsc{ml} expression of type {\tt thm list}.  The string is simply inserted
  5.1953 +into the {\tt _thy.ML} file; if it is ill-formed, it will trigger \textsc{ml}
  5.1954 +error messages.  You can then inspect the file on the temporary directory.
  5.1955 +
  5.1956 +\begin{description}
  5.1957 +\item[\it domain declarations] consist of one or more items of the form
  5.1958 +  {\it string\/}~{\tt <=}~{\it string}, associating each recursive set with
  5.1959 +  its domain.  (The domain is some existing set that is large enough to
  5.1960 +  hold the new set being defined.)
  5.1961 +
  5.1962 +\item[\it introduction rules] specify one or more introduction rules in
  5.1963 +  the form {\it ident\/}~{\it string}, where the identifier gives the name of
  5.1964 +  the rule in the result structure.
  5.1965 +
  5.1966 +\item[\it monotonicity theorems] are required for each operator applied to
  5.1967 +  a recursive set in the introduction rules.  There \textbf{must} be a theorem
  5.1968 +  of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each premise $t\in M(R_i)$
  5.1969 +  in an introduction rule!
  5.1970 +
  5.1971 +\item[\it constructor definitions] contain definitions of constants
  5.1972 +  appearing in the introduction rules.  The (co)datatype package supplies
  5.1973 +  the constructors' definitions here.  Most (co)inductive definitions omit
  5.1974 +  this section; one exception is the primitive recursive functions example;
  5.1975 +  see theory \texttt{ex/Primrec}.
  5.1976 +  
  5.1977 +\item[\it type\_intrs] consists of introduction rules for type-checking the
  5.1978 +  definition: for demonstrating that the new set is included in its domain.
  5.1979 +  (The proof uses depth-first search.)
  5.1980 +
  5.1981 +\item[\it type\_elims] consists of elimination rules for type-checking the
  5.1982 +  definition.  They are presumed to be safe and are applied as often as
  5.1983 +  possible prior to the {\tt type\_intrs} search.
  5.1984 +\end{description}
  5.1985 +
  5.1986 +The package has a few restrictions:
  5.1987 +\begin{itemize}
  5.1988 +\item The theory must separately declare the recursive sets as
  5.1989 +  constants.
  5.1990 +
  5.1991 +\item The names of the recursive sets must be identifiers, not infix
  5.1992 +operators.  
  5.1993 +
  5.1994 +\item Side-conditions must not be conjunctions.  However, an introduction rule
  5.1995 +may contain any number of side-conditions.
  5.1996 +
  5.1997 +\item Side-conditions of the form $x=t$, where the variable~$x$ does not
  5.1998 +  occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
  5.1999 +\end{itemize}
  5.2000 +
  5.2001 +
  5.2002 +\subsection{Example of an inductive definition}
  5.2003 +
  5.2004 +Two declarations, included in a theory file, define the finite powerset
  5.2005 +operator.  First we declare the constant~\texttt{Fin}.  Then we declare it
  5.2006 +inductively, with two introduction rules:
  5.2007 +\begin{ttbox}
  5.2008 +consts  Fin :: i=>i
  5.2009 +
  5.2010 +inductive
  5.2011 +  domains   "Fin(A)" <= "Pow(A)"
  5.2012 +  intrs
  5.2013 +    emptyI  "0 : Fin(A)"
  5.2014 +    consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
  5.2015 +  type_intrs empty_subsetI, cons_subsetI, PowI
  5.2016 +  type_elims "[make_elim PowD]"
  5.2017 +\end{ttbox}
  5.2018 +The resulting theory structure contains a substructure, called~\texttt{Fin}.
  5.2019 +It contains the \texttt{Fin}$~A$ introduction rules as the list
  5.2020 +\texttt{Fin.intrs}, and also individually as \texttt{Fin.emptyI} and
  5.2021 +\texttt{Fin.consI}.  The induction rule is \texttt{Fin.induct}.
  5.2022 +
  5.2023 +The chief problem with making (co)inductive definitions involves type-checking
  5.2024 +the rules.  Sometimes, additional theorems need to be supplied under
  5.2025 +\texttt{type_intrs} or \texttt{type_elims}.  If the package fails when trying
  5.2026 +to prove your introduction rules, then set the flag \ttindexbold{trace_induct}
  5.2027 +to \texttt{true} and try again.  (See the manual \emph{A Fixedpoint Approach
  5.2028 +  \ldots} for more discussion of type-checking.)
  5.2029 +
  5.2030 +In the example above, $\texttt{Pow}(A)$ is given as the domain of
  5.2031 +$\texttt{Fin}(A)$, for obviously every finite subset of~$A$ is a subset
  5.2032 +of~$A$.  However, the inductive definition package can only prove that given a
  5.2033 +few hints.
  5.2034 +Here is the output that results (with the flag set) when the
  5.2035 +\texttt{type_intrs} and \texttt{type_elims} are omitted from the inductive
  5.2036 +definition above:
  5.2037 +\begin{ttbox}
  5.2038 +Inductive definition Finite.Fin
  5.2039 +Fin(A) ==
  5.2040 +lfp(Pow(A),
  5.2041 +    \%X. {z: Pow(A) . z = 0 | (EX a b. z = cons(a, b) & a : A & b : X)})
  5.2042 +  Proving monotonicity...
  5.2043 +\ttbreak
  5.2044 +  Proving the introduction rules...
  5.2045 +The typechecking subgoal:
  5.2046 +0 : Fin(A)
  5.2047 + 1. 0 : Pow(A)
  5.2048 +\ttbreak
  5.2049 +The subgoal after monos, type_elims:
  5.2050 +0 : Fin(A)
  5.2051 + 1. 0 : Pow(A)
  5.2052 +*** prove_goal: tactic failed
  5.2053 +\end{ttbox}
  5.2054 +We see the need to supply theorems to let the package prove
  5.2055 +$\emptyset\in\texttt{Pow}(A)$.  Restoring the \texttt{type_intrs} but not the
  5.2056 +\texttt{type_elims}, we again get an error message:
  5.2057 +\begin{ttbox}
  5.2058 +The typechecking subgoal:
  5.2059 +0 : Fin(A)
  5.2060 + 1. 0 : Pow(A)
  5.2061 +\ttbreak
  5.2062 +The subgoal after monos, type_elims:
  5.2063 +0 : Fin(A)
  5.2064 + 1. 0 : Pow(A)
  5.2065 +\ttbreak
  5.2066 +The typechecking subgoal:
  5.2067 +cons(a, b) : Fin(A)
  5.2068 + 1. [| a : A; b : Fin(A) |] ==> cons(a, b) : Pow(A)
  5.2069 +\ttbreak
  5.2070 +The subgoal after monos, type_elims:
  5.2071 +cons(a, b) : Fin(A)
  5.2072 + 1. [| a : A; b : Pow(A) |] ==> cons(a, b) : Pow(A)
  5.2073 +*** prove_goal: tactic failed
  5.2074 +\end{ttbox}
  5.2075 +The first rule has been type-checked, but the second one has failed.  The
  5.2076 +simplest solution to such problems is to prove the failed subgoal separately
  5.2077 +and to supply it under \texttt{type_intrs}.  The solution actually used is
  5.2078 +to supply, under \texttt{type_elims}, a rule that changes
  5.2079 +$b\in\texttt{Pow}(A)$ to $b\subseteq A$; together with \texttt{cons_subsetI}
  5.2080 +and \texttt{PowI}, it is enough to complete the type-checking.
  5.2081 +
  5.2082 +
  5.2083 +
  5.2084 +\subsection{Further examples}
  5.2085 +
  5.2086 +An inductive definition may involve arbitrary monotonic operators.  Here is a
  5.2087 +standard example: the accessible part of a relation.  Note the use
  5.2088 +of~\texttt{Pow} in the introduction rule and the corresponding mention of the
  5.2089 +rule \verb|Pow_mono| in the \texttt{monos} list.  If the desired rule has a
  5.2090 +universally quantified premise, usually the effect can be obtained using
  5.2091 +\texttt{Pow}.
  5.2092 +\begin{ttbox}
  5.2093 +consts  acc :: i=>i
  5.2094 +inductive
  5.2095 +  domains "acc(r)" <= "field(r)"
  5.2096 +  intrs
  5.2097 +    vimage  "[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
  5.2098 +  monos      Pow_mono
  5.2099 +\end{ttbox}
  5.2100 +
  5.2101 +Finally, here is a coinductive definition.  It captures (as a bisimulation)
  5.2102 +the notion of equality on lazy lists, which are first defined as a codatatype:
  5.2103 +\begin{ttbox}
  5.2104 +consts  llist :: i=>i
  5.2105 +codatatype  "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
  5.2106 +\ttbreak
  5.2107 +
  5.2108 +consts  lleq :: i=>i
  5.2109 +coinductive
  5.2110 +  domains "lleq(A)" <= "llist(A) * llist(A)"
  5.2111 +  intrs
  5.2112 +    LNil  "<LNil, LNil> : lleq(A)"
  5.2113 +    LCons "[| a:A; <l,l'>: lleq(A) |] 
  5.2114 +           ==> <LCons(a,l), LCons(a,l')>: lleq(A)"
  5.2115 +  type_intrs  "llist.intrs"
  5.2116 +\end{ttbox}
  5.2117 +This use of \texttt{type_intrs} is typical: the relation concerns the
  5.2118 +codatatype \texttt{llist}, so naturally the introduction rules for that
  5.2119 +codatatype will be required for type-checking the rules.
  5.2120 +
  5.2121 +The Isabelle distribution contains many other inductive definitions.  Simple
  5.2122 +examples are collected on subdirectory \texttt{ZF/ex}.  The directory
  5.2123 +\texttt{Coind} and the theory \texttt{ZF/ex/LList} contain coinductive
  5.2124 +definitions.  Larger examples may be found on other subdirectories of
  5.2125 +\texttt{ZF}, such as \texttt{IMP}, and \texttt{Resid}.
  5.2126 +
  5.2127 +
  5.2128 +\subsection{The result structure}
  5.2129 +
  5.2130 +Each (co)inductive set defined in a theory file generates an \ML\ substructure
  5.2131 +having the same name.  The the substructure contains the following elements:
  5.2132 +
  5.2133 +\begin{ttbox}
  5.2134 +val intrs         : thm list  \textrm{the introduction rules}
  5.2135 +val elim          : thm       \textrm{the elimination (case analysis) rule}
  5.2136 +val mk_cases      : thm list -> string -> thm  \textrm{case analysis, see below}
  5.2137 +val induct        : thm       \textrm{the standard induction rule}
  5.2138 +val mutual_induct : thm       \textrm{the mutual induction rule, or \texttt{True}}
  5.2139 +val defs          : thm list  \textrm{definitions of operators}
  5.2140 +val bnd_mono      : thm list  \textrm{monotonicity property}
  5.2141 +val dom_subset    : thm list  \textrm{inclusion in `bounding set'}
  5.2142 +\end{ttbox}
  5.2143 +Furthermore there is the theorem $C$\texttt{_I} for every constructor~$C$; for
  5.2144 +example, the \texttt{list} datatype's introduction rules are bound to the
  5.2145 +identifiers \texttt{Nil_I} and \texttt{Cons_I}.
  5.2146 +
  5.2147 +For a codatatype, the component \texttt{coinduct} is the coinduction rule,
  5.2148 +replacing the \texttt{induct} component.
  5.2149 +
  5.2150 +Recall that \ttindex{mk_cases} generates simplified instances of the
  5.2151 +elimination (case analysis) rule.  It is as useful for inductive definitions
  5.2152 +as it is for datatypes.  There are many examples in the theory
  5.2153 +\texttt{ex/Comb}, which is discussed at length
  5.2154 +elsewhere~\cite{paulson-generic}.  The theory first defines the datatype
  5.2155 +\texttt{comb} of combinators:
  5.2156 +\begin{ttbox}
  5.2157 +consts comb :: i
  5.2158 +datatype  "comb" = K
  5.2159 +                 | S
  5.2160 +                 | "#" ("p: comb", "q: comb")   (infixl 90)
  5.2161 +\end{ttbox}
  5.2162 +The theory goes on to define contraction and parallel contraction
  5.2163 +inductively.  Then the file \texttt{ex/Comb.ML} defines special cases of
  5.2164 +contraction using \texttt{mk_cases}:
  5.2165 +\begin{ttbox}
  5.2166 +val K_contractE = contract.mk_cases comb.con_defs "K -1-> r";
  5.2167 +{\out val K_contractE = "K -1-> ?r ==> ?Q" : thm}
  5.2168 +\end{ttbox}
  5.2169 +We can read this as saying that the combinator \texttt{K} cannot reduce to
  5.2170 +anything.  Similar elimination rules for \texttt{S} and application are also
  5.2171 +generated and are supplied to the classical reasoner.  Note that
  5.2172 +\texttt{comb.con_defs} is given to \texttt{mk_cases} to allow freeness
  5.2173 +reasoning on datatype \texttt{comb}.
  5.2174 +
  5.2175 +\index{*coinductive|)} \index{*inductive|)}
  5.2176 +
  5.2177 +
  5.2178 +
  5.2179 +
  5.2180 +\section{The outer reaches of set theory}
  5.2181 +
  5.2182 +The constructions of the natural numbers and lists use a suite of
  5.2183 +operators for handling recursive function definitions.  I have described
  5.2184 +the developments in detail elsewhere~\cite{paulson-set-II}.  Here is a brief
  5.2185 +summary:
  5.2186 +\begin{itemize}
  5.2187 +  \item Theory \texttt{Trancl} defines the transitive closure of a relation
  5.2188 +    (as a least fixedpoint).
  5.2189 +
  5.2190 +  \item Theory \texttt{WF} proves the Well-Founded Recursion Theorem, using an
  5.2191 +    elegant approach of Tobias Nipkow.  This theorem permits general
  5.2192 +    recursive definitions within set theory.
  5.2193 +
  5.2194 +  \item Theory \texttt{Ord} defines the notions of transitive set and ordinal
  5.2195 +    number.  It derives transfinite induction.  A key definition is {\bf
  5.2196 +      less than}: $i<j$ if and only if $i$ and $j$ are both ordinals and
  5.2197 +    $i\in j$.  As a special case, it includes less than on the natural
  5.2198 +    numbers.
  5.2199 +    
  5.2200 +  \item Theory \texttt{Epsilon} derives $\varepsilon$-induction and
  5.2201 +    $\varepsilon$-recursion, which are generalisations of transfinite
  5.2202 +    induction and recursion.  It also defines \cdx{rank}$(x)$, which
  5.2203 +    is the least ordinal $\alpha$ such that $x$ is constructed at
  5.2204 +    stage $\alpha$ of the cumulative hierarchy (thus $x\in
  5.2205 +    V@{\alpha+1}$).
  5.2206 +\end{itemize}
  5.2207 +
  5.2208 +Other important theories lead to a theory of cardinal numbers.  They have
  5.2209 +not yet been written up anywhere.  Here is a summary:
  5.2210 +\begin{itemize}
  5.2211 +\item Theory \texttt{Rel} defines the basic properties of relations, such as
  5.2212 +  (ir)reflexivity, (a)symmetry, and transitivity.
  5.2213 +
  5.2214 +\item Theory \texttt{EquivClass} develops a theory of equivalence
  5.2215 +  classes, not using the Axiom of Choice.
  5.2216 +
  5.2217 +\item Theory \texttt{Order} defines partial orderings, total orderings and
  5.2218 +  wellorderings.
  5.2219 +
  5.2220 +\item Theory \texttt{OrderArith} defines orderings on sum and product sets.
  5.2221 +  These can be used to define ordinal arithmetic and have applications to
  5.2222 +  cardinal arithmetic.
  5.2223 +
  5.2224 +\item Theory \texttt{OrderType} defines order types.  Every wellordering is
  5.2225 +  equivalent to a unique ordinal, which is its order type.
  5.2226 +
  5.2227 +\item Theory \texttt{Cardinal} defines equipollence and cardinal numbers.
  5.2228 + 
  5.2229 +\item Theory \texttt{CardinalArith} defines cardinal addition and
  5.2230 +  multiplication, and proves their elementary laws.  It proves that there
  5.2231 +  is no greatest cardinal.  It also proves a deep result, namely
  5.2232 +  $\kappa\otimes\kappa=\kappa$ for every infinite cardinal~$\kappa$; see
  5.2233 +  Kunen~\cite[page 29]{kunen80}.  None of these results assume the Axiom of
  5.2234 +  Choice, which complicates their proofs considerably.  
  5.2235 +\end{itemize}
  5.2236 +
  5.2237 +The following developments involve the Axiom of Choice (AC):
  5.2238 +\begin{itemize}
  5.2239 +\item Theory \texttt{AC} asserts the Axiom of Choice and proves some simple
  5.2240 +  equivalent forms.
  5.2241 +
  5.2242 +\item Theory \texttt{Zorn} proves Hausdorff's Maximal Principle, Zorn's Lemma
  5.2243 +  and the Wellordering Theorem, following Abrial and
  5.2244 +  Laffitte~\cite{abrial93}.
  5.2245 +
  5.2246 +\item Theory \verb|Cardinal_AC| uses AC to prove simplified theorems about
  5.2247 +  the cardinals.  It also proves a theorem needed to justify
  5.2248 +  infinitely branching datatype declarations: if $\kappa$ is an infinite
  5.2249 +  cardinal and $|X(\alpha)| \le \kappa$ for all $\alpha<\kappa$ then
  5.2250 +  $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$.
  5.2251 +
  5.2252 +\item Theory \texttt{InfDatatype} proves theorems to justify infinitely
  5.2253 +  branching datatypes.  Arbitrary index sets are allowed, provided their
  5.2254 +  cardinalities have an upper bound.  The theory also justifies some
  5.2255 +  unusual cases of finite branching, involving the finite powerset operator
  5.2256 +  and the finite function space operator.
  5.2257 +\end{itemize}
  5.2258 +
  5.2259 +
  5.2260 +
  5.2261 +\section{The examples directories}
  5.2262 +Directory \texttt{HOL/IMP} contains a mechanised version of a semantic
  5.2263 +equivalence proof taken from Winskel~\cite{winskel93}.  It formalises the
  5.2264 +denotational and operational semantics of a simple while-language, then
  5.2265 +proves the two equivalent.  It contains several datatype and inductive
  5.2266 +definitions, and demonstrates their use.
  5.2267 +
  5.2268 +The directory \texttt{ZF/ex} contains further developments in {\ZF} set
  5.2269 +theory.  Here is an overview; see the files themselves for more details.  I
  5.2270 +describe much of this material in other
  5.2271 +publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}. 
  5.2272 +\begin{itemize}
  5.2273 +\item File \texttt{misc.ML} contains miscellaneous examples such as
  5.2274 +  Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the `Composition
  5.2275 +  of homomorphisms' challenge~\cite{boyer86}.
  5.2276 +
  5.2277 +\item Theory \texttt{Ramsey} proves the finite exponent 2 version of
  5.2278 +  Ramsey's Theorem, following Basin and Kaufmann's
  5.2279 +  presentation~\cite{basin91}.
  5.2280 +
  5.2281 +\item Theory \texttt{Integ} develops a theory of the integers as
  5.2282 +  equivalence classes of pairs of natural numbers.
  5.2283 +
  5.2284 +\item Theory \texttt{Primrec} develops some computation theory.  It
  5.2285 +  inductively defines the set of primitive recursive functions and presents a
  5.2286 +  proof that Ackermann's function is not primitive recursive.
  5.2287 +
  5.2288 +\item Theory \texttt{Primes} defines the Greatest Common Divisor of two
  5.2289 +  natural numbers and and the ``divides'' relation.
  5.2290 +
  5.2291 +\item Theory \texttt{Bin} defines a datatype for two's complement binary
  5.2292 +  integers, then proves rewrite rules to perform binary arithmetic.  For
  5.2293 +  instance, $1359\times {-}2468 = {-}3354012$ takes under 14 seconds.
  5.2294 +
  5.2295 +\item Theory \texttt{BT} defines the recursive data structure ${\tt
  5.2296 +    bt}(A)$, labelled binary trees.
  5.2297 +
  5.2298 +\item Theory \texttt{Term} defines a recursive data structure for terms
  5.2299 +  and term lists.  These are simply finite branching trees.
  5.2300 +
  5.2301 +\item Theory \texttt{TF} defines primitives for solving mutually
  5.2302 +  recursive equations over sets.  It constructs sets of trees and forests
  5.2303 +  as an example, including induction and recursion rules that handle the
  5.2304 +  mutual recursion.
  5.2305 +
  5.2306 +\item Theory \texttt{Prop} proves soundness and completeness of
  5.2307 +  propositional logic~\cite{paulson-set-II}.  This illustrates datatype
  5.2308 +  definitions, inductive definitions, structural induction and rule
  5.2309 +  induction.
  5.2310 +
  5.2311 +\item Theory \texttt{ListN} inductively defines the lists of $n$
  5.2312 +  elements~\cite{paulin92}.
  5.2313 +
  5.2314 +\item Theory \texttt{Acc} inductively defines the accessible part of a
  5.2315 +  relation~\cite{paulin92}.
  5.2316 +
  5.2317 +\item Theory \texttt{Comb} defines the datatype of combinators and
  5.2318 +  inductively defines contraction and parallel contraction.  It goes on to
  5.2319 +  prove the Church-Rosser Theorem.  This case study follows Camilleri and
  5.2320 +  Melham~\cite{camilleri92}.
  5.2321 +
  5.2322 +\item Theory \texttt{LList} defines lazy lists and a coinduction
  5.2323 +  principle for proving equations between them.
  5.2324 +\end{itemize}
  5.2325 +
  5.2326 +
  5.2327 +\section{A proof about powersets}\label{sec:ZF-pow-example}
  5.2328 +To demonstrate high-level reasoning about subsets, let us prove the
  5.2329 +equation ${{\tt Pow}(A)\cap {\tt Pow}(B)}= {\tt Pow}(A\cap B)$.  Compared
  5.2330 +with first-order logic, set theory involves a maze of rules, and theorems
  5.2331 +have many different proofs.  Attempting other proofs of the theorem might
  5.2332 +be instructive.  This proof exploits the lattice properties of
  5.2333 +intersection.  It also uses the monotonicity of the powerset operation,
  5.2334 +from \texttt{ZF/mono.ML}:
  5.2335 +\begin{ttbox}
  5.2336 +\tdx{Pow_mono}      A<=B ==> Pow(A) <= Pow(B)
  5.2337 +\end{ttbox}
  5.2338 +We enter the goal and make the first step, which breaks the equation into
  5.2339 +two inclusions by extensionality:\index{*equalityI theorem}
  5.2340 +\begin{ttbox}
  5.2341 +Goal "Pow(A Int B) = Pow(A) Int Pow(B)";
  5.2342 +{\out Level 0}
  5.2343 +{\out Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2344 +{\out  1. Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2345 +\ttbreak
  5.2346 +by (resolve_tac [equalityI] 1);
  5.2347 +{\out Level 1}
  5.2348 +{\out Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2349 +{\out  1. Pow(A Int B) <= Pow(A) Int Pow(B)}
  5.2350 +{\out  2. Pow(A) Int Pow(B) <= Pow(A Int B)}
  5.2351 +\end{ttbox}
  5.2352 +Both inclusions could be tackled straightforwardly using \texttt{subsetI}.
  5.2353 +A shorter proof results from noting that intersection forms the greatest
  5.2354 +lower bound:\index{*Int_greatest theorem}
  5.2355 +\begin{ttbox}
  5.2356 +by (resolve_tac [Int_greatest] 1);
  5.2357 +{\out Level 2}
  5.2358 +{\out Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2359 +{\out  1. Pow(A Int B) <= Pow(A)}
  5.2360 +{\out  2. Pow(A Int B) <= Pow(B)}
  5.2361 +{\out  3. Pow(A) Int Pow(B) <= Pow(A Int B)}
  5.2362 +\end{ttbox}
  5.2363 +Subgoal~1 follows by applying the monotonicity of \texttt{Pow} to $A\int
  5.2364 +B\subseteq A$; subgoal~2 follows similarly:
  5.2365 +\index{*Int_lower1 theorem}\index{*Int_lower2 theorem}
  5.2366 +\begin{ttbox}
  5.2367 +by (resolve_tac [Int_lower1 RS Pow_mono] 1);
  5.2368 +{\out Level 3}
  5.2369 +{\out Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2370 +{\out  1. Pow(A Int B) <= Pow(B)}
  5.2371 +{\out  2. Pow(A) Int Pow(B) <= Pow(A Int B)}
  5.2372 +\ttbreak
  5.2373 +by (resolve_tac [Int_lower2 RS Pow_mono] 1);
  5.2374 +{\out Level 4}
  5.2375 +{\out Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2376 +{\out  1. Pow(A) Int Pow(B) <= Pow(A Int B)}
  5.2377 +\end{ttbox}
  5.2378 +We are left with the opposite inclusion, which we tackle in the
  5.2379 +straightforward way:\index{*subsetI theorem}
  5.2380 +\begin{ttbox}
  5.2381 +by (resolve_tac [subsetI] 1);
  5.2382 +{\out Level 5}
  5.2383 +{\out Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2384 +{\out  1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)}
  5.2385 +\end{ttbox}
  5.2386 +The subgoal is to show $x\in {\tt Pow}(A\cap B)$ assuming $x\in{\tt
  5.2387 +Pow}(A)\cap {\tt Pow}(B)$; eliminating this assumption produces two
  5.2388 +subgoals.  The rule \tdx{IntE} treats the intersection like a conjunction
  5.2389 +instead of unfolding its definition.
  5.2390 +\begin{ttbox}
  5.2391 +by (eresolve_tac [IntE] 1);
  5.2392 +{\out Level 6}
  5.2393 +{\out Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2394 +{\out  1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)}
  5.2395 +\end{ttbox}
  5.2396 +The next step replaces the \texttt{Pow} by the subset
  5.2397 +relation~($\subseteq$).\index{*PowI theorem}
  5.2398 +\begin{ttbox}
  5.2399 +by (resolve_tac [PowI] 1);
  5.2400 +{\out Level 7}
  5.2401 +{\out Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2402 +{\out  1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B}
  5.2403 +\end{ttbox}
  5.2404 +We perform the same replacement in the assumptions.  This is a good
  5.2405 +demonstration of the tactic \ttindex{dresolve_tac}:\index{*PowD theorem}
  5.2406 +\begin{ttbox}
  5.2407 +by (REPEAT (dresolve_tac [PowD] 1));
  5.2408 +{\out Level 8}
  5.2409 +{\out Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2410 +{\out  1. !!x. [| x <= A; x <= B |] ==> x <= A Int B}
  5.2411 +\end{ttbox}
  5.2412 +The assumptions are that $x$ is a lower bound of both $A$ and~$B$, but
  5.2413 +$A\int B$ is the greatest lower bound:\index{*Int_greatest theorem}
  5.2414 +\begin{ttbox}
  5.2415 +by (resolve_tac [Int_greatest] 1);
  5.2416 +{\out Level 9}
  5.2417 +{\out Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2418 +{\out  1. !!x. [| x <= A; x <= B |] ==> x <= A}
  5.2419 +{\out  2. !!x. [| x <= A; x <= B |] ==> x <= B}
  5.2420 +\end{ttbox}
  5.2421 +To conclude the proof, we clear up the trivial subgoals:
  5.2422 +\begin{ttbox}
  5.2423 +by (REPEAT (assume_tac 1));
  5.2424 +{\out Level 10}
  5.2425 +{\out Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2426 +{\out No subgoals!}
  5.2427 +\end{ttbox}
  5.2428 +\medskip
  5.2429 +We could have performed this proof in one step by applying
  5.2430 +\ttindex{Blast_tac}.  Let us
  5.2431 +go back to the start:
  5.2432 +\begin{ttbox}
  5.2433 +choplev 0;
  5.2434 +{\out Level 0}
  5.2435 +{\out Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2436 +{\out  1. Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2437 +by (Blast_tac 1);
  5.2438 +{\out Depth = 0}
  5.2439 +{\out Depth = 1}
  5.2440 +{\out Depth = 2}
  5.2441 +{\out Depth = 3}
  5.2442 +{\out Level 1}
  5.2443 +{\out Pow(A Int B) = Pow(A) Int Pow(B)}
  5.2444 +{\out No subgoals!}
  5.2445 +\end{ttbox}
  5.2446 +Past researchers regarded this as a difficult proof, as indeed it is if all
  5.2447 +the symbols are replaced by their definitions.
  5.2448 +\goodbreak
  5.2449 +
  5.2450 +\section{Monotonicity of the union operator}
  5.2451 +For another example, we prove that general union is monotonic:
  5.2452 +${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$.  To begin, we
  5.2453 +tackle the inclusion using \tdx{subsetI}:
  5.2454 +\begin{ttbox}
  5.2455 +Goal "C<=D ==> Union(C) <= Union(D)";
  5.2456 +{\out Level 0}
  5.2457 +{\out C <= D ==> Union(C) <= Union(D)}
  5.2458 +{\out  1. C <= D ==> Union(C) <= Union(D)}
  5.2459 +\ttbreak
  5.2460 +by (resolve_tac [subsetI] 1);
  5.2461 +{\out Level 1}
  5.2462 +{\out C <= D ==> Union(C) <= Union(D)}
  5.2463 +{\out  1. !!x. [| C <= D; x : Union(C) |] ==> x : Union(D)}
  5.2464 +\end{ttbox}
  5.2465 +Big union is like an existential quantifier --- the occurrence in the
  5.2466 +assumptions must be eliminated early, since it creates parameters.
  5.2467 +\index{*UnionE theorem}
  5.2468 +\begin{ttbox}
  5.2469 +by (eresolve_tac [UnionE] 1);
  5.2470 +{\out Level 2}
  5.2471 +{\out C <= D ==> Union(C) <= Union(D)}
  5.2472 +{\out  1. !!x B. [| C <= D; x : B; B : C |] ==> x : Union(D)}
  5.2473 +\end{ttbox}
  5.2474 +Now we may apply \tdx{UnionI}, which creates an unknown involving the
  5.2475 +parameters.  To show $x\in \bigcup(D)$ it suffices to show that $x$ belongs
  5.2476 +to some element, say~$\Var{B2}(x,B)$, of~$D$.
  5.2477 +\begin{ttbox}
  5.2478 +by (resolve_tac [UnionI] 1);
  5.2479 +{\out Level 3}
  5.2480 +{\out C <= D ==> Union(C) <= Union(D)}
  5.2481 +{\out  1. !!x B. [| C <= D; x : B; B : C |] ==> ?B2(x,B) : D}
  5.2482 +{\out  2. !!x B. [| C <= D; x : B; B : C |] ==> x : ?B2(x,B)}
  5.2483 +\end{ttbox}
  5.2484 +Combining \tdx{subsetD} with the assumption $C\subseteq D$ yields 
  5.2485 +$\Var{a}\in C \Imp \Var{a}\in D$, which reduces subgoal~1.  Note that
  5.2486 +\texttt{eresolve_tac} has removed that assumption.
  5.2487 +\begin{ttbox}
  5.2488 +by (eresolve_tac [subsetD] 1);
  5.2489 +{\out Level 4}
  5.2490 +{\out C <= D ==> Union(C) <= Union(D)}
  5.2491 +{\out  1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C}
  5.2492 +{\out  2. !!x B. [| C <= D; x : B; B : C |] ==> x : ?B2(x,B)}
  5.2493 +\end{ttbox}
  5.2494 +The rest is routine.  Observe how~$\Var{B2}(x,B)$ is instantiated.
  5.2495 +\begin{ttbox}
  5.2496 +by (assume_tac 1);
  5.2497 +{\out Level 5}
  5.2498 +{\out C <= D ==> Union(C) <= Union(D)}
  5.2499 +{\out  1. !!x B. [| C <= D; x : B; B : C |] ==> x : B}
  5.2500 +by (assume_tac 1);
  5.2501 +{\out Level 6}
  5.2502 +{\out C <= D ==> Union(C) <= Union(D)}
  5.2503 +{\out No subgoals!}
  5.2504 +\end{ttbox}
  5.2505 +Again, \ttindex{Blast_tac} can prove the theorem in one step.
  5.2506 +\begin{ttbox}
  5.2507 +by (Blast_tac 1);
  5.2508 +{\out Depth = 0}
  5.2509 +{\out Depth = 1}
  5.2510 +{\out Depth = 2}
  5.2511 +{\out Level 1}
  5.2512 +{\out C <= D ==> Union(C) <= Union(D)}
  5.2513 +{\out No subgoals!}
  5.2514 +\end{ttbox}
  5.2515 +
  5.2516 +The file \texttt{ZF/equalities.ML} has many similar proofs.  Reasoning about
  5.2517 +general intersection can be difficult because of its anomalous behaviour on
  5.2518 +the empty set.  However, \ttindex{Blast_tac} copes well with these.  Here is
  5.2519 +a typical example, borrowed from Devlin~\cite[page 12]{devlin79}:
  5.2520 +\begin{ttbox}
  5.2521 +a:C ==> (INT x:C. A(x) Int B(x)) = (INT x:C. A(x)) Int (INT x:C. B(x))
  5.2522 +\end{ttbox}
  5.2523 +In traditional notation this is
  5.2524 +\[ a\in C \,\Imp\, \inter@{x\in C} \Bigl(A(x) \int B(x)\Bigr) =        
  5.2525 +       \Bigl(\inter@{x\in C} A(x)\Bigr)  \int  
  5.2526 +       \Bigl(\inter@{x\in C} B(x)\Bigr)  \]
  5.2527 +
  5.2528 +\section{Low-level reasoning about functions}
  5.2529 +The derived rules \texttt{lamI}, \texttt{lamE}, \texttt{lam_type}, \texttt{beta}
  5.2530 +and \texttt{eta} support reasoning about functions in a
  5.2531 +$\lambda$-calculus style.  This is generally easier than regarding
  5.2532 +functions as sets of ordered pairs.  But sometimes we must look at the
  5.2533 +underlying representation, as in the following proof
  5.2534 +of~\tdx{fun_disjoint_apply1}.  This states that if $f$ and~$g$ are
  5.2535 +functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then
  5.2536 +$(f\un g)`a = f`a$:
  5.2537 +\begin{ttbox}
  5.2538 +Goal "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \ttback
  5.2539 +\ttback    (f Un g)`a = f`a";
  5.2540 +{\out Level 0}
  5.2541 +{\out [| a : A; f : A -> B; g : C -> D; A Int C = 0 |]}
  5.2542 +{\out ==> (f Un g) ` a = f ` a}
  5.2543 +{\out  1. [| a : A; f : A -> B; g : C -> D; A Int C = 0 |]}
  5.2544 +{\out     ==> (f Un g) ` a = f ` a}
  5.2545 +\end{ttbox}
  5.2546 +Using \tdx{apply_equality}, we reduce the equality to reasoning about
  5.2547 +ordered pairs.  The second subgoal is to verify that $f\un g$ is a function.
  5.2548 +To save space, the assumptions will be abbreviated below.
  5.2549 +\begin{ttbox}
  5.2550 +by (resolve_tac [apply_equality] 1);
  5.2551 +{\out Level 1}
  5.2552 +{\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  5.2553 +{\out  1. [| \ldots |] ==> <a,f ` a> : f Un g}
  5.2554 +{\out  2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))}
  5.2555 +\end{ttbox}
  5.2556 +We must show that the pair belongs to~$f$ or~$g$; by~\tdx{UnI1} we
  5.2557 +choose~$f$:
  5.2558 +\begin{ttbox}
  5.2559 +by (resolve_tac [UnI1] 1);
  5.2560 +{\out Level 2}
  5.2561 +{\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  5.2562 +{\out  1. [| \ldots |] ==> <a,f ` a> : f}
  5.2563 +{\out  2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))}
  5.2564 +\end{ttbox}
  5.2565 +To show $\pair{a,f`a}\in f$ we use \tdx{apply_Pair}, which is
  5.2566 +essentially the converse of \tdx{apply_equality}:
  5.2567 +\begin{ttbox}
  5.2568 +by (resolve_tac [apply_Pair] 1);
  5.2569 +{\out Level 3}
  5.2570 +{\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  5.2571 +{\out  1. [| \ldots |] ==> f : (PROD x:?A2. ?B2(x))}
  5.2572 +{\out  2. [| \ldots |] ==> a : ?A2}
  5.2573 +{\out  3. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))}
  5.2574 +\end{ttbox}
  5.2575 +Using the assumptions $f\in A\to B$ and $a\in A$, we solve the two subgoals
  5.2576 +from \tdx{apply_Pair}.  Recall that a $\Pi$-set is merely a generalized
  5.2577 +function space, and observe that~{\tt?A2} is instantiated to~\texttt{A}.
  5.2578 +\begin{ttbox}
  5.2579 +by (assume_tac 1);
  5.2580 +{\out Level 4}
  5.2581 +{\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  5.2582 +{\out  1. [| \ldots |] ==> a : A}
  5.2583 +{\out  2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))}
  5.2584 +by (assume_tac 1);
  5.2585 +{\out Level 5}
  5.2586 +{\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  5.2587 +{\out  1. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))}
  5.2588 +\end{ttbox}
  5.2589 +To construct functions of the form $f\un g$, we apply
  5.2590 +\tdx{fun_disjoint_Un}:
  5.2591 +\begin{ttbox}
  5.2592 +by (resolve_tac [fun_disjoint_Un] 1);
  5.2593 +{\out Level 6}
  5.2594 +{\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  5.2595 +{\out  1. [| \ldots |] ==> f : ?A3 -> ?B3}
  5.2596 +{\out  2. [| \ldots |] ==> g : ?C3 -> ?D3}
  5.2597 +{\out  3. [| \ldots |] ==> ?A3 Int ?C3 = 0}
  5.2598 +\end{ttbox}
  5.2599 +The remaining subgoals are instances of the assumptions.  Again, observe how
  5.2600 +unknowns are instantiated:
  5.2601 +\begin{ttbox}
  5.2602 +by (assume_tac 1);
  5.2603 +{\out Level 7}
  5.2604 +{\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  5.2605 +{\out  1. [| \ldots |] ==> g : ?C3 -> ?D3}
  5.2606 +{\out  2. [| \ldots |] ==> A Int ?C3 = 0}
  5.2607 +by (assume_tac 1);
  5.2608 +{\out Level 8}
  5.2609 +{\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  5.2610 +{\out  1. [| \ldots |] ==> A Int C = 0}
  5.2611 +by (assume_tac 1);
  5.2612 +{\out Level 9}
  5.2613 +{\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  5.2614 +{\out No subgoals!}
  5.2615 +\end{ttbox}
  5.2616 +See the files \texttt{ZF/func.ML} and \texttt{ZF/WF.ML} for more
  5.2617 +examples of reasoning about functions.
  5.2618 +
  5.2619 +\index{set theory|)}
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/doc-src/ZF/logics-ZF.bbl	Wed Jan 13 16:36:36 1999 +0100
     6.3 @@ -0,0 +1,124 @@
     6.4 +\begin{thebibliography}{10}
     6.5 +
     6.6 +\bibitem{abrial93}
     6.7 +J.~R. Abrial and G.~Laffitte.
     6.8 +\newblock Towards the mechanization of the proofs of some classical theorems of
     6.9 +  set theory.
    6.10 +\newblock preprint, February 1993.
    6.11 +
    6.12 +\bibitem{basin91}
    6.13 +David Basin and Matt Kaufmann.
    6.14 +\newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison.
    6.15 +\newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical
    6.16 +  Frameworks}, pages 89--119. Cambridge University Press, 1991.
    6.17 +
    6.18 +\bibitem{boyer86}
    6.19 +Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and
    6.20 +  Lawrence Wos.
    6.21 +\newblock Set theory in first-order logic: Clauses for {G\"{o}del's} axioms.
    6.22 +\newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986.
    6.23 +
    6.24 +\bibitem{camilleri92}
    6.25 +J.~Camilleri and T.~F. Melham.
    6.26 +\newblock Reasoning with inductively defined relations in the {HOL} theorem
    6.27 +  prover.
    6.28 +\newblock Technical Report 265, Computer Laboratory, University of Cambridge,
    6.29 +  August 1992.
    6.30 +
    6.31 +\bibitem{davey&priestley}
    6.32 +B.~A. Davey and H.~A. Priestley.
    6.33 +\newblock {\em Introduction to Lattices and Order}.
    6.34 +\newblock Cambridge University Press, 1990.
    6.35 +
    6.36 +\bibitem{devlin79}
    6.37 +Keith~J. Devlin.
    6.38 +\newblock {\em Fundamentals of Contemporary Set Theory}.
    6.39 +\newblock Springer, 1979.
    6.40 +
    6.41 +\bibitem{dummett}
    6.42 +Michael Dummett.
    6.43 +\newblock {\em Elements of Intuitionism}.
    6.44 +\newblock Oxford University Press, 1977.
    6.45 +
    6.46 +\bibitem{dyckhoff}
    6.47 +Roy Dyckhoff.
    6.48 +\newblock Contraction-free sequent calculi for intuitionistic logic.
    6.49 +\newblock {\em Journal of Symbolic Logic}, 57(3):795--807, 1992.
    6.50 +
    6.51 +\bibitem{halmos60}
    6.52 +Paul~R. Halmos.
    6.53 +\newblock {\em Naive Set Theory}.
    6.54 +\newblock Van Nostrand, 1960.
    6.55 +
    6.56 +\bibitem{kunen80}
    6.57 +Kenneth Kunen.
    6.58 +\newblock {\em Set Theory: An Introduction to Independence Proofs}.
    6.59 +\newblock North-Holland, 1980.
    6.60 +
    6.61 +\bibitem{noel}
    6.62 +Philippe No{\"e}l.
    6.63 +\newblock Experimenting with {Isabelle} in {ZF} set theory.
    6.64 +\newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993.
    6.65 +
    6.66 +\bibitem{paulin92}
    6.67 +Christine Paulin-Mohring.
    6.68 +\newblock Inductive definitions in the system {Coq}: Rules and properties.
    6.69 +\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon,
    6.70 +  December 1992.
    6.71 +
    6.72 +\bibitem{paulson87}
    6.73 +Lawrence~C. Paulson.
    6.74 +\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
    6.75 +\newblock Cambridge University Press, 1987.
    6.76 +
    6.77 +\bibitem{paulson-set-I}
    6.78 +Lawrence~C. Paulson.
    6.79 +\newblock Set theory for verification: {I}. {From} foundations to functions.
    6.80 +\newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993.
    6.81 +
    6.82 +\bibitem{paulson-CADE}
    6.83 +Lawrence~C. Paulson.
    6.84 +\newblock A fixedpoint approach to implementing (co)inductive definitions.
    6.85 +\newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12
    6.86 +  International Conference}, LNAI 814, pages 148--161. Springer, 1994.
    6.87 +
    6.88 +\bibitem{paulson-final}
    6.89 +Lawrence~C. Paulson.
    6.90 +\newblock A concrete final coalgebra theorem for {ZF} set theory.
    6.91 +\newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em
    6.92 +  Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996,
    6.93 +  pages 120--139. Springer, 1995.
    6.94 +
    6.95 +\bibitem{paulson-set-II}
    6.96 +Lawrence~C. Paulson.
    6.97 +\newblock Set theory for verification: {II}. {Induction} and recursion.
    6.98 +\newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
    6.99 +
   6.100 +\bibitem{paulson-generic}
   6.101 +Lawrence~C. Paulson.
   6.102 +\newblock Generic automatic proof tools.
   6.103 +\newblock In Robert Veroff, editor, {\em Automated Reasoning and its
   6.104 +  Applications: Essays in Honor of {Larry Wos}}, chapter~3. MIT Press, 1997.
   6.105 +
   6.106 +\bibitem{quaife92}
   6.107 +Art Quaife.
   6.108 +\newblock Automated deduction in {von Neumann-Bernays-G\"{o}del} set theory.
   6.109 +\newblock {\em Journal of Automated Reasoning}, 8(1):91--147, 1992.
   6.110 +
   6.111 +\bibitem{suppes72}
   6.112 +Patrick Suppes.
   6.113 +\newblock {\em Axiomatic Set Theory}.
   6.114 +\newblock Dover, 1972.
   6.115 +
   6.116 +\bibitem{principia}
   6.117 +A.~N. Whitehead and B.~Russell.
   6.118 +\newblock {\em Principia Mathematica}.
   6.119 +\newblock Cambridge University Press, 1962.
   6.120 +\newblock Paperback edition to *56, abridged from the 2nd edition (1927).
   6.121 +
   6.122 +\bibitem{winskel93}
   6.123 +Glynn Winskel.
   6.124 +\newblock {\em The Formal Semantics of Programming Languages}.
   6.125 +\newblock MIT Press, 1993.
   6.126 +
   6.127 +\end{thebibliography}
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/doc-src/ZF/logics-ZF.tex	Wed Jan 13 16:36:36 1999 +0100
     7.3 @@ -0,0 +1,62 @@
     7.4 +%% $Id$
     7.5 +\documentclass[12pt]{report}
     7.6 +\usepackage{graphicx,a4,latexsym,../pdfsetup}
     7.7 +
     7.8 +\makeatletter
     7.9 +\input{../proof.sty}
    7.10 +\input{../rail.sty}
    7.11 +\input{../iman.sty}
    7.12 +\input{../extra.sty}
    7.13 +\makeatother
    7.14 +
    7.15 +%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
    7.16 +%%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
    7.17 +%%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
    7.18 +%%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
    7.19 +
    7.20 +\title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] 
    7.21 +       Isabelle's Logics: FOL and ZF}
    7.22 +
    7.23 +\author{{\em Lawrence C. Paulson}\\
    7.24 +        Computer Laboratory \\ University of Cambridge \\
    7.25 +        \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
    7.26 +        With Contributions by Tobias Nipkow and Markus Wenzel%
    7.27 +\thanks{Markus Wenzel made numerous improvements.
    7.28 +    Philippe de Groote and contributed to~\ZF{}.  Philippe No\"el and
    7.29 +    Martin Coen made many contributions to~\ZF{}.  The research has 
    7.30 +    been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381,
    7.31 +    GR/K77051) and by ESPRIT project 6453: Types.}
    7.32 +}
    7.33 +
    7.34 +\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
    7.35 +  \hrule\bigskip}
    7.36 +\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
    7.37 +
    7.38 +\makeindex
    7.39 +
    7.40 +\underscoreoff
    7.41 +
    7.42 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
    7.43 +
    7.44 +\pagestyle{headings}
    7.45 +\sloppy
    7.46 +\binperiod     %%%treat . like a binary operator
    7.47 +
    7.48 +\begin{document}
    7.49 +\maketitle 
    7.50 +
    7.51 +\begin{abstract}
    7.52 +This manual describes Isabelle's formalizations of many-sorted first-order
    7.53 +logic (\texttt{FOL}) and Zermelo-Fraenkel set theory (\texttt{ZF}).  See the
    7.54 +\emph{Reference Manual} for general Isabelle commands, and \emph{Introduction
    7.55 +  to Isabelle} for an overall tutorial.
    7.56 +\end{abstract}
    7.57 +
    7.58 +\pagenumbering{roman} \tableofcontents \clearfirst
    7.59 +\include{../Logics/syntax}
    7.60 +\include{FOL}
    7.61 +\include{ZF}
    7.62 +\bibliographystyle{plain}
    7.63 +\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref}
    7.64 +\input{logics-ZF.ind}
    7.65 +\end{document}