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}