# HG changeset patch # User paulson # Date 915800524 -3600 # Node ID 5583261db33db1d0f594703e33a532f2926215bf # Parent 1b2392ac575237639c07a77c60ce5ac630a93bed removal of FOL, ZF to a separate manual diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/CTT.tex --- a/doc-src/Logics/CTT.tex Fri Jan 08 13:20:59 1999 +0100 +++ b/doc-src/Logics/CTT.tex Fri Jan 08 14:02:04 1999 +0100 @@ -178,10 +178,10 @@ the one-element type is $T$; other finite types are built as $T+T+T$, etc. \index{*SUM symbol}\index{*PROD symbol} -Quantification is expressed using general sums $\sum@{x\in A}B[x]$ and +Quantification is expressed by sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$. Instead of {\tt Sum($A$,$B$)} and {\tt - Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$. $B[x]$} and \hbox{\tt - PROD $x$:$A$. $B[x]$}. For example, we may write + Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt + PROD $x$:$A$.\ $B[x]$}. For example, we may write \begin{ttbox} SUM y:B. PROD x:A. C(x,y) {\rm for} Sum(B, \%y. Prod(A, \%x. C(x,y))) \end{ttbox} diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/FOL-eg.txt --- a/doc-src/Logics/FOL-eg.txt Fri Jan 08 13:20:59 1999 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,245 +0,0 @@ -(**** FOL examples ****) - -Pretty.setmargin 72; (*existing macros just allow this margin*) -print_depth 0; - -(*** Intuitionistic examples ***) - -context IFOL.thy; - -(*Quantifier example from Logic&Computation*) -Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; -by (resolve_tac [impI] 1); -by (resolve_tac [allI] 1); -by (resolve_tac [exI] 1); -by (eresolve_tac [exE] 1); -choplev 2; -by (eresolve_tac [exE] 1); -by (resolve_tac [exI] 1); -by (eresolve_tac [allE] 1); -by (assume_tac 1); - - -(*Example of Dyckhoff's method*) -Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))"; -by (resolve_tac [impI] 1); -by (eresolve_tac [disj_impE] 1); -by (eresolve_tac [imp_impE] 1); -by (eresolve_tac [imp_impE] 1); -by (REPEAT (eresolve_tac [FalseE] 2)); -by (assume_tac 1); - - - - - -(*** Classical examples ***) - -context FOL.thy; - -Goal "EX y. ALL x. P(y)-->P(x)"; -by (resolve_tac [exCI] 1); -by (resolve_tac [allI] 1); -by (resolve_tac [impI] 1); -by (eresolve_tac [allE] 1); -prth (allI RSN (2,swap)); -by (eresolve_tac [it] 1); -by (resolve_tac [impI] 1); -by (eresolve_tac [notE] 1); -by (assume_tac 1); -Goal "EX y. ALL x. P(y)-->P(x)"; -by (Blast_tac 1); - - - -- Goal "EX y. ALL x. P(y)-->P(x)"; -Level 0 -EX y. ALL x. P(y) --> P(x) - 1. EX y. ALL x. P(y) --> P(x) -- by (resolve_tac [exCI] 1); -Level 1 -EX y. ALL x. P(y) --> P(x) - 1. ALL y. ~(ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x) -- by (resolve_tac [allI] 1); -Level 2 -EX y. ALL x. P(y) --> P(x) - 1. !!x. ALL y. ~(ALL x. P(y) --> P(x)) ==> P(?a) --> P(x) -- by (resolve_tac [impI] 1); -Level 3 -EX y. ALL x. P(y) --> P(x) - 1. !!x. [| ALL y. ~(ALL x. P(y) --> P(x)); P(?a) |] ==> P(x) -- by (eresolve_tac [allE] 1); -Level 4 -EX y. ALL x. P(y) --> P(x) - 1. !!x. [| P(?a); ~(ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x) -- prth (allI RSN (2,swap)); -[| ~(ALL x. ?P1(x)); !!x. ~?Q ==> ?P1(x) |] ==> ?Q -- by (eresolve_tac [it] 1); -Level 5 -EX y. ALL x. P(y) --> P(x) - 1. !!x xa. [| P(?a); ~P(x) |] ==> P(?y3(x)) --> P(xa) -- by (resolve_tac [impI] 1); -Level 6 -EX y. ALL x. P(y) --> P(x) - 1. !!x xa. [| P(?a); ~P(x); P(?y3(x)) |] ==> P(xa) -- by (eresolve_tac [notE] 1); -Level 7 -EX y. ALL x. P(y) --> P(x) - 1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x) -- by (assume_tac 1); -Level 8 -EX y. ALL x. P(y) --> P(x) -No subgoals! -- Goal "EX y. ALL x. P(y)-->P(x)"; -Level 0 -EX y. ALL x. P(y) --> P(x) - 1. EX y. ALL x. P(y) --> P(x) -- by (best_tac FOL_dup_cs 1); -Level 1 -EX y. ALL x. P(y) --> P(x) -No subgoals! - - -(**** finally, the example FOL/ex/if.ML ****) - -> val prems = goalw if_thy [if_def] -# "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"; -Level 0 -if(P,Q,R) - 1. P & Q | ~P & R -> by (Classical.fast_tac (FOL_cs addIs prems) 1); -Level 1 -if(P,Q,R) -No subgoals! -> val ifI = result(); - - -> val major::prems = goalw if_thy [if_def] -# "[| if(P,Q,R); [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S"; -Level 0 -S - 1. S -> by (cut_facts_tac [major] 1); -Level 1 -S - 1. P & Q | ~P & R ==> S -> by (Classical.fast_tac (FOL_cs addIs prems) 1); -Level 2 -S -No subgoals! -> val ifE = result(); - -> goal if_thy "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"; -Level 0 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D)) - 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D)) -> by (resolve_tac [iffI] 1); -Level 1 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D)) - 1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D)) - 2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D)) -> by (eresolve_tac [ifE] 1); -Level 2 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D)) - 1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D)) - 2. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D)) - 3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D)) -> by (eresolve_tac [ifE] 1); -Level 3 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D)) - 1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D)) - 2. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D)) - 3. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D)) - 4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D)) -> by (resolve_tac [ifI] 1); -Level 4 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D)) - 1. [| P; Q; A; Q |] ==> if(P,A,C) - 2. [| P; Q; A; ~Q |] ==> if(P,B,D) - 3. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D)) - 4. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D)) - 5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D)) -> by (resolve_tac [ifI] 1); -Level 5 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D)) - 1. [| P; Q; A; Q; P |] ==> A - 2. [| P; Q; A; Q; ~P |] ==> C - 3. [| P; Q; A; ~Q |] ==> if(P,B,D) - 4. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D)) - 5. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D)) - 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D)) - -> choplev 0; -Level 0 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D)) - 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D)) -> val if_cs = FOL_cs addSIs [ifI] addSEs[ifE]; -> by (Classical.fast_tac if_cs 1); -Level 1 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D)) -No subgoals! -> val if_commute = result(); - -> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"; -Level 0 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B)) - 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B)) -> by (Classical.fast_tac if_cs 1); -Level 1 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B)) -No subgoals! -> val nested_ifs = result(); - - -> choplev 0; -Level 0 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B)) - 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B)) -> by (rewrite_goals_tac [if_def]); -Level 1 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B)) - 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <-> - P & (Q & A | ~Q & B) | ~P & (R & A | ~R & B) -> by (Classical.fast_tac FOL_cs 1); -Level 2 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B)) -No subgoals! - - -> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"; -Level 0 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A)) - 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A)) -> by (REPEAT (Classical.step_tac if_cs 1)); -Level 1 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A)) - 1. [| A; ~P; R; ~P; R |] ==> B - 2. [| B; ~P; ~R; ~P; ~R |] ==> A - 3. [| ~P; R; B; ~P; R |] ==> A - 4. [| ~P; ~R; A; ~B; ~P |] ==> R - -> choplev 0; -Level 0 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A)) - 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A)) -> by (rewrite_goals_tac [if_def]); -Level 1 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A)) - 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <-> - P & (Q & A | ~Q & B) | ~P & (R & B | ~R & A) -> by (Classical.fast_tac FOL_cs 1); -by: tactic failed -Exception- ERROR raised -Exception failure raised - -> by (REPEAT (Classical.step_tac FOL_cs 1)); -Level 2 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A)) - 1. [| A; ~P; R; ~P; R; ~False |] ==> B - 2. [| A; ~P; R; R; ~False; ~B; ~B |] ==> Q - 3. [| B; ~P; ~R; ~P; ~A |] ==> R - 4. [| B; ~P; ~R; ~Q; ~A |] ==> R - 5. [| B; ~R; ~P; ~A; ~R; Q; ~False |] ==> A - 6. [| ~P; R; B; ~P; R; ~False |] ==> A - 7. [| ~P; ~R; A; ~B; ~R |] ==> P - 8. [| ~P; ~R; A; ~B; ~R |] ==> Q diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/FOL.tex --- a/doc-src/Logics/FOL.tex Fri Jan 08 13:20:59 1999 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,937 +0,0 @@ -%% $Id$ -\chapter{First-Order Logic} -\index{first-order logic|(} - -Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc - nk}. Intuitionistic first-order logic is defined first, as theory -\thydx{IFOL}. Classical logic, theory \thydx{FOL}, is -obtained by adding the double negation rule. Basic proof procedures are -provided. The intuitionistic prover works with derived rules to simplify -implications in the assumptions. Classical~\texttt{FOL} employs Isabelle's -classical reasoner, which simulates a sequent calculus. - -\section{Syntax and rules of inference} -The logic is many-sorted, using Isabelle's type classes. The class of -first-order terms is called \cldx{term} and is a subclass of \texttt{logic}. -No types of individuals are provided, but extensions can define types such -as \texttt{nat::term} and type constructors such as \texttt{list::(term)term} -(see the examples directory, \texttt{FOL/ex}). Below, the type variable -$\alpha$ ranges over class \texttt{term}; the equality symbol and quantifiers -are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which -belongs to class~\cldx{logic}. Figure~\ref{fol-syntax} gives the syntax. -Note that $a$\verb|~=|$b$ is translated to $\neg(a=b)$. - -Figure~\ref{fol-rules} shows the inference rules with their~\ML\ names. -Negation is defined in the usual way for intuitionistic logic; $\neg P$ -abbreviates $P\imp\bot$. The biconditional~($\bimp$) is defined through -$\conj$ and~$\imp$; introduction and elimination rules are derived for it. - -The unique existence quantifier, $\exists!x.P(x)$, is defined in terms -of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested -quantifications. For instance, $\exists!x\;y.P(x,y)$ abbreviates -$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there -exists a unique pair $(x,y)$ satisfying~$P(x,y)$. - -Some intuitionistic derived rules are shown in -Fig.\ts\ref{fol-int-derived}, again with their \ML\ names. These include -rules for the defined symbols $\neg$, $\bimp$ and $\exists!$. Natural -deduction typically involves a combination of forward and backward -reasoning, particularly with the destruction rules $(\conj E)$, -$({\imp}E)$, and~$(\forall E)$. Isabelle's backward style handles these -rules badly, so sequent-style rules are derived to eliminate conjunctions, -implications, and universal quantifiers. Used with elim-resolution, -\tdx{allE} eliminates a universal quantifier while \tdx{all_dupE} -re-inserts the quantified formula for later use. The rules {\tt -conj_impE}, etc., support the intuitionistic proof procedure -(see~\S\ref{fol-int-prover}). - -See the files \texttt{FOL/IFOL.thy}, \texttt{FOL/IFOL.ML} and -\texttt{FOL/intprover.ML} for complete listings of the rules and -derived rules. - -\begin{figure} -\begin{center} -\begin{tabular}{rrr} - \it name &\it meta-type & \it description \\ - \cdx{Trueprop}& $o\To prop$ & coercion to $prop$\\ - \cdx{Not} & $o\To o$ & negation ($\neg$) \\ - \cdx{True} & $o$ & tautology ($\top$) \\ - \cdx{False} & $o$ & absurdity ($\bot$) -\end{tabular} -\end{center} -\subcaption{Constants} - -\begin{center} -\begin{tabular}{llrrr} - \it symbol &\it name &\it meta-type & \it priority & \it description \\ - \sdx{ALL} & \cdx{All} & $(\alpha\To o)\To o$ & 10 & - universal quantifier ($\forall$) \\ - \sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 & - existential quantifier ($\exists$) \\ - \texttt{EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 & - unique existence ($\exists!$) -\end{tabular} -\index{*"E"X"! symbol} -\end{center} -\subcaption{Binders} - -\begin{center} -\index{*"= symbol} -\index{&@{\tt\&} symbol} -\index{*"| symbol} -\index{*"-"-"> symbol} -\index{*"<"-"> symbol} -\begin{tabular}{rrrr} - \it symbol & \it meta-type & \it priority & \it description \\ - \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\ - \tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\ - \tt | & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\ - \tt --> & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\ - \tt <-> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$) -\end{tabular} -\end{center} -\subcaption{Infixes} - -\dquotes -\[\begin{array}{rcl} - formula & = & \hbox{expression of type~$o$} \\ - & | & term " = " term \\ - & | & term " \ttilde= " term \\ - & | & "\ttilde\ " formula \\ - & | & formula " \& " formula \\ - & | & formula " | " formula \\ - & | & formula " --> " formula \\ - & | & formula " <-> " formula \\ - & | & "ALL~" id~id^* " . " formula \\ - & | & "EX~~" id~id^* " . " formula \\ - & | & "EX!~" id~id^* " . " formula - \end{array} -\] -\subcaption{Grammar} -\caption{Syntax of \texttt{FOL}} \label{fol-syntax} -\end{figure} - - -\begin{figure} -\begin{ttbox} -\tdx{refl} a=a -\tdx{subst} [| a=b; P(a) |] ==> P(b) -\subcaption{Equality rules} - -\tdx{conjI} [| P; Q |] ==> P&Q -\tdx{conjunct1} P&Q ==> P -\tdx{conjunct2} P&Q ==> Q - -\tdx{disjI1} P ==> P|Q -\tdx{disjI2} Q ==> P|Q -\tdx{disjE} [| P|Q; P ==> R; Q ==> R |] ==> R - -\tdx{impI} (P ==> Q) ==> P-->Q -\tdx{mp} [| P-->Q; P |] ==> Q - -\tdx{FalseE} False ==> P -\subcaption{Propositional rules} - -\tdx{allI} (!!x. P(x)) ==> (ALL x.P(x)) -\tdx{spec} (ALL x.P(x)) ==> P(x) - -\tdx{exI} P(x) ==> (EX x.P(x)) -\tdx{exE} [| EX x.P(x); !!x. P(x) ==> R |] ==> R -\subcaption{Quantifier rules} - -\tdx{True_def} True == False-->False -\tdx{not_def} ~P == P-->False -\tdx{iff_def} P<->Q == (P-->Q) & (Q-->P) -\tdx{ex1_def} EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x) -\subcaption{Definitions} -\end{ttbox} - -\caption{Rules of intuitionistic logic} \label{fol-rules} -\end{figure} - - -\begin{figure} -\begin{ttbox} -\tdx{sym} a=b ==> b=a -\tdx{trans} [| a=b; b=c |] ==> a=c -\tdx{ssubst} [| b=a; P(a) |] ==> P(b) -\subcaption{Derived equality rules} - -\tdx{TrueI} True - -\tdx{notI} (P ==> False) ==> ~P -\tdx{notE} [| ~P; P |] ==> R - -\tdx{iffI} [| P ==> Q; Q ==> P |] ==> P<->Q -\tdx{iffE} [| P <-> Q; [| P-->Q; Q-->P |] ==> R |] ==> R -\tdx{iffD1} [| P <-> Q; P |] ==> Q -\tdx{iffD2} [| P <-> Q; Q |] ==> P - -\tdx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x) -\tdx{ex1E} [| EX! x.P(x); !!x.[| P(x); ALL y. P(y) --> y=x |] ==> R - |] ==> R -\subcaption{Derived rules for \(\top\), \(\neg\), \(\bimp\) and \(\exists!\)} - -\tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R -\tdx{impE} [| P-->Q; P; Q ==> R |] ==> R -\tdx{allE} [| ALL x.P(x); P(x) ==> R |] ==> R -\tdx{all_dupE} [| ALL x.P(x); [| P(x); ALL x.P(x) |] ==> R |] ==> R -\subcaption{Sequent-style elimination rules} - -\tdx{conj_impE} [| (P&Q)-->S; P-->(Q-->S) ==> R |] ==> R -\tdx{disj_impE} [| (P|Q)-->S; [| P-->S; Q-->S |] ==> R |] ==> R -\tdx{imp_impE} [| (P-->Q)-->S; [| P; Q-->S |] ==> Q; S ==> R |] ==> R -\tdx{not_impE} [| ~P --> S; P ==> False; S ==> R |] ==> R -\tdx{iff_impE} [| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P; - S ==> R |] ==> R -\tdx{all_impE} [| (ALL x.P(x))-->S; !!x.P(x); S ==> R |] ==> R -\tdx{ex_impE} [| (EX x.P(x))-->S; P(a)-->S ==> R |] ==> R -\end{ttbox} -\subcaption{Intuitionistic simplification of implication} -\caption{Derived rules for intuitionistic logic} \label{fol-int-derived} -\end{figure} - - -\section{Generic packages} -\FOL{} instantiates most of Isabelle's generic packages. -\begin{itemize} -\item -It instantiates the simplifier. Both equality ($=$) and the biconditional -($\bimp$) may be used for rewriting. Tactics such as \texttt{Asm_simp_tac} and -\texttt{Full_simp_tac} refer to the default simpset (\texttt{simpset()}), which works for -most purposes. Named simplification sets include \ttindexbold{IFOL_ss}, -for intuitionistic first-order logic, and \ttindexbold{FOL_ss}, -for classical logic. See the file -\texttt{FOL/simpdata.ML} for a complete listing of the simplification -rules% -\iflabelundefined{sec:setting-up-simp}{}% - {, and \S\ref{sec:setting-up-simp} for discussion}. - -\item -It instantiates the classical reasoner. See~\S\ref{fol-cla-prover} -for details. - -\item \FOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes - for an equality throughout a subgoal and its hypotheses. This tactic uses - \FOL's general substitution rule. -\end{itemize} - -\begin{warn}\index{simplification!of conjunctions}% - Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The - left part of a conjunction helps in simplifying the right part. This effect - is not available by default: it can be slow. It can be obtained by - including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$. -\end{warn} - - -\section{Intuitionistic proof procedures} \label{fol-int-prover} -Implication elimination (the rules~\texttt{mp} and~\texttt{impE}) pose -difficulties for automated proof. In intuitionistic logic, the assumption -$P\imp Q$ cannot be treated like $\neg P\disj Q$. Given $P\imp Q$, we may -use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated -use of $P\imp Q$. If the proof of~$P$ fails then the whole branch of the -proof must be abandoned. Thus intuitionistic propositional logic requires -backtracking. - -For an elementary example, consider the intuitionistic proof of $Q$ from -$P\imp Q$ and $(P\imp Q)\imp P$. The implication $P\imp Q$ is needed -twice: -\[ \infer[({\imp}E)]{Q}{P\imp Q & - \infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}} -\] -The theorem prover for intuitionistic logic does not use~\texttt{impE}.\@ -Instead, it simplifies implications using derived rules -(Fig.\ts\ref{fol-int-derived}). It reduces the antecedents of implications -to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$. -The rules \tdx{conj_impE} and \tdx{disj_impE} are -straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and -$(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp -S$. The other \ldots{\tt_impE} rules are unsafe; the method requires -backtracking. All the rules are derived in the same simple manner. - -Dyckhoff has independently discovered similar rules, and (more importantly) -has demonstrated their completeness for propositional -logic~\cite{dyckhoff}. However, the tactics given below are not complete -for first-order logic because they discard universally quantified -assumptions after a single use. -\begin{ttbox} -mp_tac : int -> tactic -eq_mp_tac : int -> tactic -IntPr.safe_step_tac : int -> tactic -IntPr.safe_tac : tactic -IntPr.inst_step_tac : int -> tactic -IntPr.step_tac : int -> tactic -IntPr.fast_tac : int -> tactic -IntPr.best_tac : int -> tactic -\end{ttbox} -Most of these belong to the structure \texttt{IntPr} and resemble the -tactics of Isabelle's classical reasoner. - -\begin{ttdescription} -\item[\ttindexbold{mp_tac} {\it i}] -attempts to use \tdx{notE} or \tdx{impE} within the assumptions in -subgoal $i$. For each assumption of the form $\neg P$ or $P\imp Q$, it -searches for another assumption unifiable with~$P$. By -contradiction with $\neg P$ it can solve the subgoal completely; by Modus -Ponens it can replace the assumption $P\imp Q$ by $Q$. The tactic can -produce multiple outcomes, enumerating all suitable pairs of assumptions. - -\item[\ttindexbold{eq_mp_tac} {\it i}] -is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it -is safe. - -\item[\ttindexbold{IntPr.safe_step_tac} $i$] performs a safe step on -subgoal~$i$. This may include proof by assumption or Modus Ponens (taking -care not to instantiate unknowns), or \texttt{hyp_subst_tac}. - -\item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all -subgoals. It is deterministic, with at most one outcome. - -\item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac}, -but allows unknowns to be instantiated. - -\item[\ttindexbold{IntPr.step_tac} $i$] tries \texttt{safe_tac} or {\tt - inst_step_tac}, or applies an unsafe rule. This is the basic step of - the intuitionistic proof procedure. - -\item[\ttindexbold{IntPr.fast_tac} $i$] applies \texttt{step_tac}, using -depth-first search, to solve subgoal~$i$. - -\item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using -best-first search (guided by the size of the proof state) to solve subgoal~$i$. -\end{ttdescription} -Here are some of the theorems that \texttt{IntPr.fast_tac} proves -automatically. The latter three date from {\it Principia Mathematica} -(*11.53, *11.55, *11.61)~\cite{principia}. -\begin{ttbox} -~~P & ~~(P --> Q) --> ~~Q -(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y))) -(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y))) -(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y))) -\end{ttbox} - - - -\begin{figure} -\begin{ttbox} -\tdx{excluded_middle} ~P | P - -\tdx{disjCI} (~Q ==> P) ==> P|Q -\tdx{exCI} (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x) -\tdx{impCE} [| P-->Q; ~P ==> R; Q ==> R |] ==> R -\tdx{iffCE} [| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R -\tdx{notnotD} ~~P ==> P -\tdx{swap} ~P ==> (~Q ==> P) ==> Q -\end{ttbox} -\caption{Derived rules for classical logic} \label{fol-cla-derived} -\end{figure} - - -\section{Classical proof procedures} \label{fol-cla-prover} -The classical theory, \thydx{FOL}, consists of intuitionistic logic plus -the rule -$$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$ -\noindent -Natural deduction in classical logic is not really all that natural. -{\FOL} derives classical introduction rules for $\disj$ and~$\exists$, as -well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap -rule (see Fig.\ts\ref{fol-cla-derived}). - -The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt -Best_tac} refer to the default claset (\texttt{claset()}), which works for most -purposes. Named clasets include \ttindexbold{prop_cs}, which includes the -propositional rules, and \ttindexbold{FOL_cs}, which also includes quantifier -rules. See the file \texttt{FOL/cladata.ML} for lists of the -classical rules, and -\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% - {Chap.\ts\ref{chap:classical}} -for more discussion of classical proof methods. - - -\section{An intuitionistic example} -Here is a session similar to one in {\em Logic and Computation} -\cite[pages~222--3]{paulson87}. Isabelle treats quantifiers differently -from {\sc lcf}-based theorem provers such as {\sc hol}. - -First, we specify that we are working in intuitionistic logic: -\begin{ttbox} -context IFOL.thy; -\end{ttbox} -The proof begins by entering the goal, then applying the rule $({\imp}I)$. -\begin{ttbox} -Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; -{\out Level 0} -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -{\out 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -\ttbreak -by (resolve_tac [impI] 1); -{\out Level 1} -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -{\out 1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y)} -\end{ttbox} -In this example, we shall never have more than one subgoal. Applying -$({\imp}I)$ replaces~\verb|-->| by~\verb|==>|, making -\(\ex{y}\all{x}Q(x,y)\) an assumption. We have the choice of -$({\exists}E)$ and $({\forall}I)$; let us try the latter. -\begin{ttbox} -by (resolve_tac [allI] 1); -{\out Level 2} -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -{\out 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)} -\end{ttbox} -Applying $({\forall}I)$ replaces the \texttt{ALL~x} by \hbox{\tt!!x}, -changing the universal quantifier from object~($\forall$) to -meta~($\Forall$). The bound variable is a {\bf parameter} of the -subgoal. We now must choose between $({\exists}I)$ and $({\exists}E)$. What -happens if the wrong rule is chosen? -\begin{ttbox} -by (resolve_tac [exI] 1); -{\out Level 3} -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -{\out 1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))} -\end{ttbox} -The new subgoal~1 contains the function variable {\tt?y2}. Instantiating -{\tt?y2} can replace~{\tt?y2(x)} by a term containing~\texttt{x}, even -though~\texttt{x} is a bound variable. Now we analyse the assumption -\(\exists y.\forall x. Q(x,y)\) using elimination rules: -\begin{ttbox} -by (eresolve_tac [exE] 1); -{\out Level 4} -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -{\out 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))} -\end{ttbox} -Applying $(\exists E)$ has produced the parameter \texttt{y} and stripped the -existential quantifier from the assumption. But the subgoal is unprovable: -there is no way to unify \texttt{?y2(x)} with the bound variable~\texttt{y}. -Using \texttt{choplev} we can return to the critical point. This time we -apply $({\exists}E)$: -\begin{ttbox} -choplev 2; -{\out Level 2} -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -{\out 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)} -\ttbreak -by (eresolve_tac [exE] 1); -{\out Level 3} -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -{\out 1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y)} -\end{ttbox} -We now have two parameters and no scheme variables. Applying -$({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are -applied to those parameters. Parameters should be produced early, as this -example demonstrates. -\begin{ttbox} -by (resolve_tac [exI] 1); -{\out Level 4} -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -{\out 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y))} -\ttbreak -by (eresolve_tac [allE] 1); -{\out Level 5} -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -{\out 1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))} -\end{ttbox} -The subgoal has variables \texttt{?y3} and \texttt{?x4} applied to both -parameters. The obvious projection functions unify {\tt?x4(x,y)} with~{\tt -x} and \verb|?y3(x,y)| with~\texttt{y}. -\begin{ttbox} -by (assume_tac 1); -{\out Level 6} -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -{\out No subgoals!} -\end{ttbox} -The theorem was proved in six tactic steps, not counting the abandoned -ones. But proof checking is tedious; \ttindex{IntPr.fast_tac} proves the -theorem in one step. -\begin{ttbox} -Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; -{\out Level 0} -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -{\out 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -by (IntPr.fast_tac 1); -{\out Level 1} -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} -{\out No subgoals!} -\end{ttbox} - - -\section{An example of intuitionistic negation} -The following example demonstrates the specialized forms of implication -elimination. Even propositional formulae can be difficult to prove from -the basic rules; the specialized rules help considerably. - -Propositional examples are easy to invent. As Dummett notes~\cite[page -28]{dummett}, $\neg P$ is classically provable if and only if it is -intuitionistically provable; therefore, $P$ is classically provable if and -only if $\neg\neg P$ is intuitionistically provable.% -\footnote{Of course this holds only for propositional logic, not if $P$ is - allowed to contain quantifiers.} Proving $\neg\neg P$ intuitionistically is -much harder than proving~$P$ classically. - -Our example is the double negation of the classical tautology $(P\imp -Q)\disj (Q\imp P)$. When stating the goal, we command Isabelle to expand -negations to implications using the definition $\neg P\equiv P\imp\bot$. -This allows use of the special implication rules. -\begin{ttbox} -Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))"; -{\out Level 0} -{\out ~ ~ ((P --> Q) | (Q --> P))} -{\out 1. ((P --> Q) | (Q --> P) --> False) --> False} -\end{ttbox} -The first step is trivial. -\begin{ttbox} -by (resolve_tac [impI] 1); -{\out Level 1} -{\out ~ ~ ((P --> Q) | (Q --> P))} -{\out 1. (P --> Q) | (Q --> P) --> False ==> False} -\end{ttbox} -By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but -that formula is not a theorem of intuitionistic logic. Instead we apply -the specialized implication rule \tdx{disj_impE}. It splits the -assumption into two assumptions, one for each disjunct. -\begin{ttbox} -by (eresolve_tac [disj_impE] 1); -{\out Level 2} -{\out ~ ~ ((P --> Q) | (Q --> P))} -{\out 1. [| (P --> Q) --> False; (Q --> P) --> False |] ==> False} -\end{ttbox} -We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but -their negations are inconsistent. Applying \tdx{imp_impE} breaks down -the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new -assumptions~$P$ and~$\neg Q$. -\begin{ttbox} -by (eresolve_tac [imp_impE] 1); -{\out Level 3} -{\out ~ ~ ((P --> Q) | (Q --> P))} -{\out 1. [| (Q --> P) --> False; P; Q --> False |] ==> Q} -{\out 2. [| (Q --> P) --> False; False |] ==> False} -\end{ttbox} -Subgoal~2 holds trivially; let us ignore it and continue working on -subgoal~1. Thanks to the assumption~$P$, we could prove $Q\imp P$; -applying \tdx{imp_impE} is simpler. -\begin{ttbox} -by (eresolve_tac [imp_impE] 1); -{\out Level 4} -{\out ~ ~ ((P --> Q) | (Q --> P))} -{\out 1. [| P; Q --> False; Q; P --> False |] ==> P} -{\out 2. [| P; Q --> False; False |] ==> Q} -{\out 3. [| (Q --> P) --> False; False |] ==> False} -\end{ttbox} -The three subgoals are all trivial. -\begin{ttbox} -by (REPEAT (eresolve_tac [FalseE] 2)); -{\out Level 5} -{\out ~ ~ ((P --> Q) | (Q --> P))} -{\out 1. [| P; Q --> False; Q; P --> False |] ==> P} -\ttbreak -by (assume_tac 1); -{\out Level 6} -{\out ~ ~ ((P --> Q) | (Q --> P))} -{\out No subgoals!} -\end{ttbox} -This proof is also trivial for \texttt{IntPr.fast_tac}. - - -\section{A classical example} \label{fol-cla-example} -To illustrate classical logic, we shall prove the theorem -$\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as -follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise -$\all{x}P(x)$ is true. Either way the theorem holds. First, we switch to -classical logic: -\begin{ttbox} -context FOL.thy; -\end{ttbox} - -The formal proof does not conform in any obvious way to the sketch given -above. The key inference is the first one, \tdx{exCI}; this classical -version of~$(\exists I)$ allows multiple instantiation of the quantifier. -\begin{ttbox} -Goal "EX y. ALL x. P(y)-->P(x)"; -{\out Level 0} -{\out EX y. ALL x. P(y) --> P(x)} -{\out 1. EX y. ALL x. P(y) --> P(x)} -\ttbreak -by (resolve_tac [exCI] 1); -{\out Level 1} -{\out EX y. ALL x. P(y) --> P(x)} -{\out 1. ALL y. ~ (ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)} -\end{ttbox} -We can either exhibit a term {\tt?a} to satisfy the conclusion of -subgoal~1, or produce a contradiction from the assumption. The next -steps are routine. -\begin{ttbox} -by (resolve_tac [allI] 1); -{\out Level 2} -{\out EX y. ALL x. P(y) --> P(x)} -{\out 1. !!x. ALL y. ~ (ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)} -\ttbreak -by (resolve_tac [impI] 1); -{\out Level 3} -{\out EX y. ALL x. P(y) --> P(x)} -{\out 1. !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)} -\end{ttbox} -By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$ -in effect applies~$(\exists I)$ again. -\begin{ttbox} -by (eresolve_tac [allE] 1); -{\out Level 4} -{\out EX y. ALL x. P(y) --> P(x)} -{\out 1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)} -\end{ttbox} -In classical logic, a negated assumption is equivalent to a conclusion. To -get this effect, we create a swapped version of~$(\forall I)$ and apply it -using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall -I)$ using \ttindex{swap_res_tac}. -\begin{ttbox} -allI RSN (2,swap); -{\out val it = "[| ~ (ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm} -by (eresolve_tac [it] 1); -{\out Level 5} -{\out EX y. ALL x. P(y) --> P(x)} -{\out 1. !!x xa. [| P(?a); ~ P(x) |] ==> P(?y3(x)) --> P(xa)} -\end{ttbox} -The previous conclusion, \texttt{P(x)}, has become a negated assumption. -\begin{ttbox} -by (resolve_tac [impI] 1); -{\out Level 6} -{\out EX y. ALL x. P(y) --> P(x)} -{\out 1. !!x xa. [| P(?a); ~ P(x); P(?y3(x)) |] ==> P(xa)} -\end{ttbox} -The subgoal has three assumptions. We produce a contradiction between the -\index{assumptions!contradictory} assumptions~\verb|~P(x)| and~{\tt - P(?y3(x))}. The proof never instantiates the unknown~{\tt?a}. -\begin{ttbox} -by (eresolve_tac [notE] 1); -{\out Level 7} -{\out EX y. ALL x. P(y) --> P(x)} -{\out 1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)} -\ttbreak -by (assume_tac 1); -{\out Level 8} -{\out EX y. ALL x. P(y) --> P(x)} -{\out No subgoals!} -\end{ttbox} -The civilised way to prove this theorem is through \ttindex{Blast_tac}, -which automatically uses the classical version of~$(\exists I)$: -\begin{ttbox} -Goal "EX y. ALL x. P(y)-->P(x)"; -{\out Level 0} -{\out EX y. ALL x. P(y) --> P(x)} -{\out 1. EX y. ALL x. P(y) --> P(x)} -by (Blast_tac 1); -{\out Depth = 0} -{\out Depth = 1} -{\out Depth = 2} -{\out Level 1} -{\out EX y. ALL x. P(y) --> P(x)} -{\out No subgoals!} -\end{ttbox} -If this theorem seems counterintuitive, then perhaps you are an -intuitionist. In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$ -requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$, -which we cannot do without further knowledge about~$P$. - - -\section{Derived rules and the classical tactics} -Classical first-order logic can be extended with the propositional -connective $if(P,Q,R)$, where -$$ if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if) $$ -Theorems about $if$ can be proved by treating this as an abbreviation, -replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals. But -this duplicates~$P$, causing an exponential blowup and an unreadable -formula. Introducing further abbreviations makes the problem worse. - -Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$ -directly, without reference to its definition. The simple identity -\[ if(P,Q,R) \,\bimp\, (P\imp Q)\conj (\neg P\imp R) \] -suggests that the -$if$-introduction rule should be -\[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]} & \infer*{R}{[\neg P]}} \] -The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the -elimination rules for~$\disj$ and~$\conj$. -\[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]} - & \infer*{S}{[\neg P,R]}} -\] -Having made these plans, we get down to work with Isabelle. The theory of -classical logic, \texttt{FOL}, is extended with the constant -$if::[o,o,o]\To o$. The axiom \tdx{if_def} asserts the -equation~$(if)$. -\begin{ttbox} -If = FOL + -consts if :: [o,o,o]=>o -rules if_def "if(P,Q,R) == P&Q | ~P&R" -end -\end{ttbox} -We create the file \texttt{If.thy} containing these declarations. (This file -is on directory \texttt{FOL/ex} in the Isabelle distribution.) Typing -\begin{ttbox} -use_thy "If"; -\end{ttbox} -loads that theory and sets it to be the current context. - - -\subsection{Deriving the introduction rule} - -The derivations of the introduction and elimination rules demonstrate the -methods for rewriting with definitions. Classical reasoning is required, -so we use \texttt{blast_tac}. - -The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$, -concludes $if(P,Q,R)$. We propose the conclusion as the main goal -using~\ttindex{Goalw}, which uses \texttt{if_def} to rewrite occurrences -of $if$ in the subgoal. -\begin{ttbox} -val prems = Goalw [if_def] - "[| P ==> Q; ~ P ==> R |] ==> if(P,Q,R)"; -{\out Level 0} -{\out if(P,Q,R)} -{\out 1. P & Q | ~ P & R} -\end{ttbox} -The premises (bound to the {\ML} variable \texttt{prems}) are passed as -introduction rules to \ttindex{blast_tac}. Remember that \texttt{claset()} refers -to the default classical set. -\begin{ttbox} -by (blast_tac (claset() addIs prems) 1); -{\out Level 1} -{\out if(P,Q,R)} -{\out No subgoals!} -qed "ifI"; -\end{ttbox} - - -\subsection{Deriving the elimination rule} -The elimination rule has three premises, two of which are themselves rules. -The conclusion is simply $S$. -\begin{ttbox} -val major::prems = Goalw [if_def] - "[| if(P,Q,R); [| P; Q |] ==> S; [| ~ P; R |] ==> S |] ==> S"; -{\out Level 0} -{\out S} -{\out 1. S} -\end{ttbox} -The major premise contains an occurrence of~$if$, but the version returned -by \ttindex{Goalw} (and bound to the {\ML} variable~\texttt{major}) has the -definition expanded. Now \ttindex{cut_facts_tac} inserts~\texttt{major} as an -assumption in the subgoal, so that \ttindex{blast_tac} can break it down. -\begin{ttbox} -by (cut_facts_tac [major] 1); -{\out Level 1} -{\out S} -{\out 1. P & Q | ~ P & R ==> S} -\ttbreak -by (blast_tac (claset() addIs prems) 1); -{\out Level 2} -{\out S} -{\out No subgoals!} -qed "ifE"; -\end{ttbox} -As you may recall from -\iflabelundefined{definitions}{{\em Introduction to Isabelle}}% - {\S\ref{definitions}}, there are other -ways of treating definitions when deriving a rule. We can start the -proof using \texttt{Goal}, which does not expand definitions, instead of -\texttt{Goalw}. We can use \ttindex{rew_tac} -to expand definitions in the subgoals---perhaps after calling -\ttindex{cut_facts_tac} to insert the rule's premises. We can use -\ttindex{rewrite_rule}, which is a meta-inference rule, to expand -definitions in the premises directly. - - -\subsection{Using the derived rules} -The rules just derived have been saved with the {\ML} names \tdx{ifI} -and~\tdx{ifE}. They permit natural proofs of theorems such as the -following: -\begin{eqnarray*} - if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\ - if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B)) -\end{eqnarray*} -Proofs also require the classical reasoning rules and the $\bimp$ -introduction rule (called~\tdx{iffI}: do not confuse with~\texttt{ifI}). - -To display the $if$-rules in action, let us analyse a proof step by step. -\begin{ttbox} -Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"; -{\out Level 0} -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} -{\out 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} -\ttbreak -by (resolve_tac [iffI] 1); -{\out Level 1} -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} -{\out 1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))} -{\out 2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))} -\end{ttbox} -The $if$-elimination rule can be applied twice in succession. -\begin{ttbox} -by (eresolve_tac [ifE] 1); -{\out Level 2} -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} -{\out 1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))} -{\out 2. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))} -{\out 3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))} -\ttbreak -by (eresolve_tac [ifE] 1); -{\out Level 3} -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} -{\out 1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))} -{\out 2. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))} -{\out 3. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))} -{\out 4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))} -\end{ttbox} -% -In the first two subgoals, all assumptions have been reduced to atoms. Now -$if$-introduction can be applied. Observe how the $if$-rules break down -occurrences of $if$ when they become the outermost connective. -\begin{ttbox} -by (resolve_tac [ifI] 1); -{\out Level 4} -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} -{\out 1. [| P; Q; A; Q |] ==> if(P,A,C)} -{\out 2. [| P; Q; A; ~ Q |] ==> if(P,B,D)} -{\out 3. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))} -{\out 4. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))} -{\out 5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))} -\ttbreak -by (resolve_tac [ifI] 1); -{\out Level 5} -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} -{\out 1. [| P; Q; A; Q; P |] ==> A} -{\out 2. [| P; Q; A; Q; ~ P |] ==> C} -{\out 3. [| P; Q; A; ~ Q |] ==> if(P,B,D)} -{\out 4. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))} -{\out 5. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))} -{\out 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))} -\end{ttbox} -Where do we stand? The first subgoal holds by assumption; the second and -third, by contradiction. This is getting tedious. We could use the classical -reasoner, but first let us extend the default claset with the derived rules -for~$if$. -\begin{ttbox} -AddSIs [ifI]; -AddSEs [ifE]; -\end{ttbox} -Now we can revert to the -initial proof state and let \ttindex{blast_tac} solve it. -\begin{ttbox} -choplev 0; -{\out Level 0} -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} -{\out 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} -by (Blast_tac 1); -{\out Level 1} -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} -{\out No subgoals!} -\end{ttbox} -This tactic also solves the other example. -\begin{ttbox} -Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"; -{\out Level 0} -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} -{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} -\ttbreak -by (Blast_tac 1); -{\out Level 1} -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} -{\out No subgoals!} -\end{ttbox} - - -\subsection{Derived rules versus definitions} -Dispensing with the derived rules, we can treat $if$ as an -abbreviation, and let \ttindex{blast_tac} prove the expanded formula. Let -us redo the previous proof: -\begin{ttbox} -choplev 0; -{\out Level 0} -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} -{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} -\end{ttbox} -This time, simply unfold using the definition of $if$: -\begin{ttbox} -by (rewtac if_def); -{\out Level 1} -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} -{\out 1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->} -{\out P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)} -\end{ttbox} -We are left with a subgoal in pure first-order logic, which is why the -classical reasoner can prove it given \texttt{FOL_cs} alone. (We could, of -course, have used \texttt{Blast_tac}.) -\begin{ttbox} -by (blast_tac FOL_cs 1); -{\out Level 2} -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} -{\out No subgoals!} -\end{ttbox} -Expanding definitions reduces the extended logic to the base logic. This -approach has its merits --- especially if the prover for the base logic is -good --- but can be slow. In these examples, proofs using the default -claset (which includes the derived rules) run about six times faster -than proofs using \texttt{FOL_cs}. - -Expanding definitions also complicates error diagnosis. Suppose we are having -difficulties in proving some goal. If by expanding definitions we have -made it unreadable, then we have little hope of diagnosing the problem. - -Attempts at program verification often yield invalid assertions. -Let us try to prove one: -\begin{ttbox} -Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"; -{\out Level 0} -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} -{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} -by (Blast_tac 1); -{\out by: tactic failed} -\end{ttbox} -This failure message is uninformative, but we can get a closer look at the -situation by applying \ttindex{Step_tac}. -\begin{ttbox} -by (REPEAT (Step_tac 1)); -{\out Level 1} -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} -{\out 1. [| A; ~ P; R; ~ P; R |] ==> B} -{\out 2. [| B; ~ P; ~ R; ~ P; ~ R |] ==> A} -{\out 3. [| ~ P; R; B; ~ P; R |] ==> A} -{\out 4. [| ~ P; ~ R; A; ~ B; ~ P |] ==> R} -\end{ttbox} -Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false -while~$R$ and~$A$ are true. This truth assignment reduces the main goal to -$true\bimp false$, which is of course invalid. - -We can repeat this analysis by expanding definitions, using just -the rules of {\FOL}: -\begin{ttbox} -choplev 0; -{\out Level 0} -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} -{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} -\ttbreak -by (rewtac if_def); -{\out Level 1} -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} -{\out 1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->} -{\out P & (Q & A | ~ Q & B) | ~ P & (R & B | ~ R & A)} -by (blast_tac FOL_cs 1); -{\out by: tactic failed} -\end{ttbox} -Again we apply \ttindex{step_tac}: -\begin{ttbox} -by (REPEAT (step_tac FOL_cs 1)); -{\out Level 2} -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} -{\out 1. [| A; ~ P; R; ~ P; R; ~ False |] ==> B} -{\out 2. [| A; ~ P; R; R; ~ False; ~ B; ~ B |] ==> Q} -{\out 3. [| B; ~ P; ~ R; ~ P; ~ A |] ==> R} -{\out 4. [| B; ~ P; ~ R; ~ Q; ~ A |] ==> R} -{\out 5. [| B; ~ R; ~ P; ~ A; ~ R; Q; ~ False |] ==> A} -{\out 6. [| ~ P; R; B; ~ P; R; ~ False |] ==> A} -{\out 7. [| ~ P; ~ R; A; ~ B; ~ R |] ==> P} -{\out 8. [| ~ P; ~ R; A; ~ B; ~ R |] ==> Q} -\end{ttbox} -Subgoal~1 yields the same countermodel as before. But each proof step has -taken six times as long, and the final result contains twice as many subgoals. - -Expanding definitions causes a great increase in complexity. This is why -the classical prover has been designed to accept derived rules. - -\index{first-order logic|)} diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/HOL.tex --- a/doc-src/Logics/HOL.tex Fri Jan 08 13:20:59 1999 +0100 +++ b/doc-src/Logics/HOL.tex Fri Jan 08 14:02:04 1999 +0100 @@ -905,10 +905,10 @@ \subsection{Simplification and substitution} -The simplifier is available in \HOL. Tactics such as {\tt +Simplification tactics tactics such as {\tt Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset ({\tt simpset()}), which works for most purposes. A quite minimal -simplification set for higher-order logic is~\ttindexbold{HOL_ss}, +simplification set for higher-order logic is~\ttindexbold{HOL_ss}; even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which also expresses logical equivalence, may be used for rewriting. See the file \texttt{HOL/simpdata.ML} for a complete listing of the basic @@ -2010,6 +2010,7 @@ Theory \texttt{Arith} declares a generic function \texttt{size} of type $\alpha\To nat$. Each datatype defines a particular instance of \texttt{size} by overloading according to the following scheme: +%%% FIXME: This formula is too big and is completely unreadable \[ size(C^j@i~x@1~\dots~x@{m^j@i}) = \! \left\{ diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/LK.tex --- a/doc-src/Logics/LK.tex Fri Jan 08 13:20:59 1999 +0100 +++ b/doc-src/Logics/LK.tex Fri Jan 08 14:02:04 1999 +0100 @@ -333,12 +333,21 @@ \end{ttdescription} +\section{Packaging sequent rules} -\section{Packaging sequent rules} -Section~\ref{sec:safe} described the distinction between safe and unsafe -rules. An unsafe rule may reduce a provable goal to an unprovable set of -subgoals, and should only be used as a last resort. Typical examples are -the weakened quantifier rules {\tt allL_thin} and {\tt exR_thin}. +The sequent calculi come with simple proof procedures. These are incomplete +but are reasonably powerful for interactive use. They expect rules to be +classified as {\bf safe} or {\bf unsafe}. A rule is safe if applying it to a +provable goal always yields provable subgoals. If a rule is safe then it can +be applied automatically to a goal without destroying our chances of finding a +proof. For instance, all the standard rules of the classical sequent calculus +{\sc lk} are safe. An unsafe rule may render the goal unprovable; typical +examples are the weakened quantifier rules {\tt allL_thin} and {\tt exR_thin}. + +Proof procedures use safe rules whenever possible, using an unsafe rule as a +last resort. Those safe rules are preferred that generate the fewest +subgoals. Safe rules are (by definition) deterministic, while the unsafe +rules require a search strategy, such as backtracking. A {\bf pack} is a pair whose first component is a list of safe rules and whose second is a list of unsafe rules. Packs can be extended in an @@ -387,6 +396,7 @@ \section{Proof procedures} + The \LK{} proof procedure is similar to the classical reasoner described in \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% @@ -475,7 +485,7 @@ The theorem $\turn\ex{y}\all{x}P(y)\imp P(x)$ is a standard example of the classical treatment of the existential quantifier. Classical reasoning is easy using~{\LK}, as you can see by comparing this proof with the one -given in~\S\ref{fol-cla-example}. From a logical point of view, the +given in the FOL manual~\cite{isabelle-ZF}. From a logical point of view, the proofs are essentially the same; the key step here is to use \tdx{exR} rather than the weaker~\tdx{exR_thin}. \begin{ttbox} diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/Makefile --- a/doc-src/Logics/Makefile Fri Jan 08 13:20:59 1999 +0100 +++ b/doc-src/Logics/Makefile Fri Jan 08 14:02:04 1999 +0100 @@ -6,7 +6,7 @@ ######################################################################### -FILES = logics.tex intro.tex FOL.tex ZF.tex HOL.tex LK.tex CTT.tex\ +FILES = logics.tex preface.tex syntax.tex HOL.tex LK.tex CTT.tex\ ../rail.sty ../proof.sty ../iman.sty ../extra.sty logics.dvi.gz: $(FILES) diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/ZF-eg.txt --- a/doc-src/Logics/ZF-eg.txt Fri Jan 08 13:20:59 1999 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,230 +0,0 @@ -(**** ZF examples ****) - -Pretty.setmargin 72; (*existing macros just allow this margin*) -print_depth 0; - -(*** Powerset example ***) - -val [prem] = goal ZF.thy "A<=B ==> Pow(A) <= Pow(B)"; -by (resolve_tac [subsetI] 1); -by (resolve_tac [PowI] 1); -by (dresolve_tac [PowD] 1); -by (eresolve_tac [subset_trans] 1); -by (resolve_tac [prem] 1); -val Pow_mono = result(); - -goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)"; -by (resolve_tac [equalityI] 1); -by (resolve_tac [Int_greatest] 1); -by (resolve_tac [Int_lower1 RS Pow_mono] 1); -by (resolve_tac [Int_lower2 RS Pow_mono] 1); -by (resolve_tac [subsetI] 1); -by (eresolve_tac [IntE] 1); -by (resolve_tac [PowI] 1); -by (REPEAT (dresolve_tac [PowD] 1)); -by (resolve_tac [Int_greatest] 1); -by (REPEAT (assume_tac 1)); -choplev 0; -by (fast_tac (ZF_cs addIs [equalityI]) 1); - -Goal "C<=D ==> Union(C) <= Union(D)"; -by (resolve_tac [subsetI] 1); -by (eresolve_tac [UnionE] 1); -by (resolve_tac [UnionI] 1); -by (eresolve_tac [subsetD] 1); -by (assume_tac 1); -by (assume_tac 1); -choplev 0; -by (resolve_tac [Union_least] 1); -by (resolve_tac [Union_upper] 1); -by (eresolve_tac [subsetD] 1); - - -val prems = goal ZF.thy - "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ -\ (f Un g)`a = f`a"; -by (resolve_tac [apply_equality] 1); -by (resolve_tac [UnI1] 1); -by (resolve_tac [apply_Pair] 1); -by (resolve_tac prems 1); -by (resolve_tac prems 1); -by (resolve_tac [fun_disjoint_Un] 1); -by (resolve_tac prems 1); -by (resolve_tac prems 1); -by (resolve_tac prems 1); - - -Goal "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ -\ (f Un g)`a = f`a"; -by (resolve_tac [apply_equality] 1); -by (resolve_tac [UnI1] 1); -by (resolve_tac [apply_Pair] 1); -by (assume_tac 1); -by (assume_tac 1); -by (resolve_tac [fun_disjoint_Un] 1); -by (assume_tac 1); -by (assume_tac 1); -by (assume_tac 1); - - - - -goal ZF.thy "f``(UN x:A. B(x)) = (UN x:A. f``B(x))"; -by (resolve_tac [equalityI] 1); -by (resolve_tac [subsetI] 1); -fe imageE; - - -goal ZF.thy "(UN x:C. A(x) Int B) = (UN x:C. A(x)) Int B"; -by (resolve_tac [equalityI] 1); -by (resolve_tac [Int_greatest] 1); -fr UN_mono; -by (resolve_tac [Int_lower1] 1); -fr UN_least; -???? - - -> goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)"; -Level 0 -Pow(A Int B) = Pow(A) Int Pow(B) - 1. Pow(A Int B) = Pow(A) Int Pow(B) -> by (resolve_tac [equalityI] 1); -Level 1 -Pow(A Int B) = Pow(A) Int Pow(B) - 1. Pow(A Int B) <= Pow(A) Int Pow(B) - 2. Pow(A) Int Pow(B) <= Pow(A Int B) -> by (resolve_tac [Int_greatest] 1); -Level 2 -Pow(A Int B) = Pow(A) Int Pow(B) - 1. Pow(A Int B) <= Pow(A) - 2. Pow(A Int B) <= Pow(B) - 3. Pow(A) Int Pow(B) <= Pow(A Int B) -> by (resolve_tac [Int_lower1 RS Pow_mono] 1); -Level 3 -Pow(A Int B) = Pow(A) Int Pow(B) - 1. Pow(A Int B) <= Pow(B) - 2. Pow(A) Int Pow(B) <= Pow(A Int B) -> by (resolve_tac [Int_lower2 RS Pow_mono] 1); -Level 4 -Pow(A Int B) = Pow(A) Int Pow(B) - 1. Pow(A) Int Pow(B) <= Pow(A Int B) -> by (resolve_tac [subsetI] 1); -Level 5 -Pow(A Int B) = Pow(A) Int Pow(B) - 1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B) -> by (eresolve_tac [IntE] 1); -Level 6 -Pow(A Int B) = Pow(A) Int Pow(B) - 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B) -> by (resolve_tac [PowI] 1); -Level 7 -Pow(A Int B) = Pow(A) Int Pow(B) - 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B -> by (REPEAT (dresolve_tac [PowD] 1)); -Level 8 -Pow(A Int B) = Pow(A) Int Pow(B) - 1. !!x. [| x <= A; x <= B |] ==> x <= A Int B -> by (resolve_tac [Int_greatest] 1); -Level 9 -Pow(A Int B) = Pow(A) Int Pow(B) - 1. !!x. [| x <= A; x <= B |] ==> x <= A - 2. !!x. [| x <= A; x <= B |] ==> x <= B -> by (REPEAT (assume_tac 1)); -Level 10 -Pow(A Int B) = Pow(A) Int Pow(B) -No subgoals! -> choplev 0; -Level 0 -Pow(A Int B) = Pow(A) Int Pow(B) - 1. Pow(A Int B) = Pow(A) Int Pow(B) -> by (fast_tac (ZF_cs addIs [equalityI]) 1); -Level 1 -Pow(A Int B) = Pow(A) Int Pow(B) -No subgoals! - - - - -> val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)"; -Level 0 -Union(C) <= Union(D) - 1. Union(C) <= Union(D) -> by (resolve_tac [subsetI] 1); -Level 1 -Union(C) <= Union(D) - 1. !!x. x : Union(C) ==> x : Union(D) -> by (eresolve_tac [UnionE] 1); -Level 2 -Union(C) <= Union(D) - 1. !!x B. [| x : B; B : C |] ==> x : Union(D) -> by (resolve_tac [UnionI] 1); -Level 3 -Union(C) <= Union(D) - 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D - 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B) -> by (resolve_tac [prem RS subsetD] 1); -Level 4 -Union(C) <= Union(D) - 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C - 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B) -> by (assume_tac 1); -Level 5 -Union(C) <= Union(D) - 1. !!x B. [| x : B; B : C |] ==> x : B -> by (assume_tac 1); -Level 6 -Union(C) <= Union(D) -No subgoals! - - - -> val prems = goal ZF.thy -# "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ -# \ (f Un g)`a = f`a"; -Level 0 -(f Un g) ` a = f ` a - 1. (f Un g) ` a = f ` a -> by (resolve_tac [apply_equality] 1); -Level 1 -(f Un g) ` a = f ` a - 1. : f Un g - 2. f Un g : (PROD x:?A. ?B(x)) -> by (resolve_tac [UnI1] 1); -Level 2 -(f Un g) ` a = f ` a - 1. : f - 2. f Un g : (PROD x:?A. ?B(x)) -> by (resolve_tac [apply_Pair] 1); -Level 3 -(f Un g) ` a = f ` a - 1. f : (PROD x:?A2. ?B2(x)) - 2. a : ?A2 - 3. f Un g : (PROD x:?A. ?B(x)) -> by (resolve_tac prems 1); -Level 4 -(f Un g) ` a = f ` a - 1. a : A - 2. f Un g : (PROD x:?A. ?B(x)) -> by (resolve_tac prems 1); -Level 5 -(f Un g) ` a = f ` a - 1. f Un g : (PROD x:?A. ?B(x)) -> by (resolve_tac [fun_disjoint_Un] 1); -Level 6 -(f Un g) ` a = f ` a - 1. f : ?A3 -> ?B3 - 2. g : ?C3 -> ?D3 - 3. ?A3 Int ?C3 = 0 -> by (resolve_tac prems 1); -Level 7 -(f Un g) ` a = f ` a - 1. g : ?C3 -> ?D3 - 2. A Int ?C3 = 0 -> by (resolve_tac prems 1); -Level 8 -(f Un g) ` a = f ` a - 1. A Int C = 0 -> by (resolve_tac prems 1); -Level 9 -(f Un g) ` a = f ` a -No subgoals! diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/ZF-rules.txt --- a/doc-src/Logics/ZF-rules.txt Fri Jan 08 13:20:59 1999 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,468 +0,0 @@ -%%%% RULES.ML - -\idx{empty_set} ~(x:0) -\idx{union_iff} A:Union(C) <-> (EX B:C. A:B) -\idx{power_set} A : Pow(B) <-> A <= B -\idx{infinity} 0:Inf & (ALL y:Inf. succ(y): Inf) -\idx{foundation} A=0 | (EX x:A. ALL y:x. ~ y:A) - -\idx{replacement} (!!x y z.[| x:A; P(x,y); P(x,z) |] ==> y=z) ==> - y : PrimReplace(A,P) <-> (EX x:A. P(x,y)) - -\idx{Replace_def} Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y)) -\idx{RepFun_def} RepFun(A,f) == Replace(A, %x u. u=f(x)) -\idx{Collect_def} Collect(A,P) == \{ y . x:A, x=y & P(x)\} -\idx{the_def} The(P) == Union(\{y . x:\{0\}, P(y)\}) - -\idx{Upair_def} Upair(a,b) == - \{y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)\} - -\idx{Inter_def} Inter(A) == \{ x:Union(A) . ALL y:A. x:y\} - -\idx{Un_def} A Un B == Union(Upair(A,B)) -\idx{Int_def} A Int B == Inter(Upair(A,B)) -\idx{Diff_def} A - B == \{ x:A . ~(x:B) \} -\idx{cons_def} cons(a,A) == Upair(a,a) Un A -\idx{succ_def} succ(i) == cons(i,i) - -\idx{Pair_def} == \{\{a,a\}, \{a,b\}\} -\idx{fst_def} fst(A) == THE x. EX y. A= -\idx{snd_def} snd(A) == THE y. EX x. A= -\idx{split_def} split(p,c) == THE y. EX a b. p= & y=c(a,b) -\idx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{\} - -\idx{domain_def} domain(r) == \{a:Union(Union(r)) . EX b. : r\} -\idx{range_def} range(r) == \{b:Union(Union(r)) . EX a. : r\} -\idx{field_def} field(r) == domain(r) Un range(r) -\idx{image_def} r``A == \{y : range(r) . EX x:A. : r\} -\idx{vimage_def} r -`` A == \{x : domain(r) . EX y:A. : r\} - -\idx{lam_def} Lambda(A,f) == RepFun(A, %x. ) -\idx{apply_def} f`a == THE y. : f -\idx{restrict_def} restrict(f,A) == lam x:A.f`x -\idx{Pi_def} Pi(A,B) == \{f: Pow(Sigma(A,B)). ALL x:A. EX! y. : f\} - -\idx{subset_def} A <= B == ALL x:A. x:B -\idx{strict_subset_def} A A <= B & B <= A - -\idx{Ball_def} Ball(A,P) == ALL x. x:A --> P(x) -\idx{Bex_def} Bex(A,P) == EX x. x:A & P(x) - - -%%%% LEMMAS.ML - -\idx{ballI} [| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x) -\idx{bspec} [| ALL x:A. P(x); x: A |] ==> P(x) -\idx{ballE} [| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q - -\idx{ball_cong} [| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> - (ALL x:A. P(x)) <-> (ALL x:A'. P'(x)) - -\idx{bexI} [| P(x); x: A |] ==> EX x:A. P(x) -\idx{bexCI} [| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A.P(x) -\idx{bexE} [| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q - -\idx{bex_cong} [| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> - (EX x:A. P(x)) <-> (EX x:A'. P'(x)) - -\idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B -\idx{subsetD} [| A <= B; c:A |] ==> c:B -\idx{subsetCE} [| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P -\idx{subset_refl} A <= A -\idx{subset_trans} [| A<=B; B<=C |] ==> A<=C - -\idx{equalityI} [| A <= B; B <= A |] ==> A = B -\idx{equalityD1} A = B ==> A<=B -\idx{equalityD2} A = B ==> B<=A -\idx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P - -\idx{emptyE} a:0 ==> P -\idx{empty_subsetI} 0 <= A -\idx{equals0I} [| !!y. y:A ==> False |] ==> A=0 -\idx{equals0D} [| A=0; a:A |] ==> P - -\idx{PowI} A <= B ==> A : Pow(B) -\idx{PowD} A : Pow(B) ==> A<=B - -\idx{ReplaceI} [| x: A; P(x,b); !!y. P(x,y) ==> y=b |] ==> - b : \{y. x:A, P(x,y)\} - -\idx{ReplaceE} [| b : \{y. x:A, P(x,y)\}; - !!x. [| x: A; P(x,b); ALL y. P(x,y)-->y=b |] ==> R - |] ==> R - -\idx{Replace_cong} [| A=B; !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> - \{y. x:A, P(x,y)\} = \{y. x:B, Q(x,y)\} - -\idx{RepFunI} [| a : A |] ==> f(a) : RepFun(A,f) -\idx{RepFunE} [| b : RepFun(A, %x.f(x)); - !!x.[| x:A; b=f(x) |] ==> P |] ==> P - -\idx{RepFun_cong} [| A=B; !!x. x:B ==> f(x)=g(x) |] ==> - RepFun(A, %x.f(x)) = RepFun(B, %x.g(x)) - - -\idx{separation} x : Collect(A,P) <-> x:A & P(x) -\idx{CollectI} [| a:A; P(a) |] ==> a : \{x:A. P(x)\} -\idx{CollectE} [| a : \{x:A. P(x)\}; [| a:A; P(a) |] ==> R |] ==> R -\idx{CollectD1} a : \{x:A. P(x)\} ==> a:A -\idx{CollectD2} a : \{x:A. P(x)\} ==> P(a) - -\idx{Collect_cong} [| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> - \{x:A. P(x)\} = \{x:B. Q(x)\} - -\idx{UnionI} [| B: C; A: B |] ==> A: Union(C) -\idx{UnionE} [| A : Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R - -\idx{InterI} [| !!x. x: C ==> A: x; c:C |] ==> A : Inter(C) -\idx{InterD} [| A : Inter(C); B : C |] ==> A : B -\idx{InterE} [| A : Inter(C); A:B ==> R; ~ B:C ==> R |] ==> R - -\idx{UN_I} [| a: A; b: B(a) |] ==> b: (UN x:A. B(x)) -\idx{UN_E} [| b : (UN x:A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R - -\idx{INT_I} [| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x)) -\idx{INT_E} [| b : (INT x:A. B(x)); a: A |] ==> b : B(a) - - -%%%% UPAIR.ML - -\idx{pairing} a:Upair(b,c) <-> (a=b | a=c) -\idx{UpairI1} a : Upair(a,b) -\idx{UpairI2} b : Upair(a,b) -\idx{UpairE} [| a : Upair(b,c); a = b ==> P; a = c ==> P |] ==> P - -\idx{UnI1} c : A ==> c : A Un B -\idx{UnI2} c : B ==> c : A Un B -\idx{UnCI} (~c : B ==> c : A) ==> c : A Un B -\idx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P - -\idx{IntI} [| c : A; c : B |] ==> c : A Int B -\idx{IntD1} c : A Int B ==> c : A -\idx{IntD2} c : A Int B ==> c : B -\idx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P - -\idx{DiffI} [| c : A; ~ c : B |] ==> c : A - B -\idx{DiffD1} c : A - B ==> c : A -\idx{DiffD2} [| c : A - B; c : B |] ==> P -\idx{DiffE} [| c : A - B; [| c:A; ~ c:B |] ==> P |] ==> P - -\idx{consI1} a : cons(a,B) -\idx{consI2} a : B ==> a : cons(b,B) -\idx{consCI} (~ a:B ==> a=b) ==> a: cons(b,B) -\idx{consE} [| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P - -\idx{singletonI} a : \{a\} -\idx{singletonE} [| a : \{b\}; a=b ==> P |] ==> P - -\idx{succI1} i : succ(i) -\idx{succI2} i : j ==> i : succ(j) -\idx{succCI} (~ i:j ==> i=j) ==> i: succ(j) -\idx{succE} [| i : succ(j); i=j ==> P; i:j ==> P |] ==> P -\idx{succ_neq_0} [| succ(n)=0 |] ==> P -\idx{succ_inject} succ(m) = succ(n) ==> m=n - -\idx{the_equality} [| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a -\idx{theI} EX! x. P(x) ==> P(THE x. P(x)) - -\idx{mem_anti_sym} [| a:b; b:a |] ==> P -\idx{mem_anti_refl} a:a ==> P - - -%%% SUBSET.ML - -\idx{Union_upper} B:A ==> B <= Union(A) -\idx{Union_least} [| !!x. x:A ==> x<=C |] ==> Union(A) <= C - -\idx{Inter_lower} B:A ==> Inter(A) <= B -\idx{Inter_greatest} [| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A) - -\idx{Un_upper1} A <= A Un B -\idx{Un_upper2} B <= A Un B -\idx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C - -\idx{Int_lower1} A Int B <= A -\idx{Int_lower2} A Int B <= B -\idx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B - -\idx{Diff_subset} A-B <= A -\idx{Diff_contains} [| C<=A; C Int B = 0 |] ==> C <= A-B - -\idx{Collect_subset} Collect(A,P) <= A - -%%% PAIR.ML - -\idx{Pair_inject1} = ==> a=c -\idx{Pair_inject2} = ==> b=d -\idx{Pair_inject} [| = ; [| a=c; b=d |] ==> P |] ==> P -\idx{Pair_neq_0} =0 ==> P - -\idx{fst_conv} fst() = a -\idx{snd_conv} snd() = b -\idx{split_conv} split(, %x y.c(x,y)) = c(a,b) - -\idx{SigmaI} [| a:A; b:B(a) |] ==> : (SUM x:A. B(x)) - -\idx{SigmaE} [| c: (SUM x:A. B(x)); - !!x y.[| x:A; y:B(x); c= |] ==> P - |] ==> P - -\idx{SigmaE2} [| : (SUM x:A. B(x)); - [| a:A; b:B(a) |] ==> P - |] ==> P - - -%%% DOMRANGE.ML - -\idx{domainI} : r ==> a : domain(r) -\idx{domainE} [| a : domain(r); !!y. : r ==> P |] ==> P -\idx{domain_subset} domain(Sigma(A,B)) <= A - -\idx{rangeI} : r ==> b : range(r) -\idx{rangeE} [| b : range(r); !!x. : r ==> P |] ==> P -\idx{range_subset} range(A*B) <= B - -\idx{fieldI1} : r ==> a : field(r) -\idx{fieldI2} : r ==> b : field(r) -\idx{fieldCI} (~ :r ==> : r) ==> a : field(r) - -\idx{fieldE} [| a : field(r); - !!x. : r ==> P; - !!x. : r ==> P - |] ==> P - -\idx{field_subset} field(A*A) <= A - -\idx{imageI} [| : r; a:A |] ==> b : r``A -\idx{imageE} [| b: r``A; !!x.[| : r; x:A |] ==> P |] ==> P - -\idx{vimageI} [| : r; b:B |] ==> a : r-``B -\idx{vimageE} [| a: r-``B; !!x.[| : r; x:B |] ==> P |] ==> P - - -%%% FUNC.ML - -\idx{fun_is_rel} f: (PROD x:A.B(x)) ==> f <= Sigma(A,B) - -\idx{apply_equality} [| : f; f: (PROD x:A.B(x)) |] ==> f`a = b -\idx{apply_equality2} [| : f; : f; f: (PROD x:A.B(x)) |] ==> b=c - -\idx{apply_type} [| f: (PROD x:A.B(x)); a:A |] ==> f`a : B(a) -\idx{apply_Pair} [| f: (PROD x:A.B(x)); a:A |] ==> : f -\idx{apply_iff} [| f: (PROD x:A.B(x)); a:A |] ==> : f <-> f`a = b - -\idx{domain_type} [| : f; f: (PROD x:A.B(x)) |] ==> a : A -\idx{range_type} [| : f; f: (PROD x:A.B(x)) |] ==> b : B(a) - -\idx{Pi_type} [| f: A->C; !!x. x:A ==> f`x : B(x) |] ==> f: Pi(A,B) -\idx{domain_of_fun} f : Pi(A,B) ==> domain(f)=A -\idx{range_of_fun} f : Pi(A,B) ==> f: A->range(f) - -\idx{fun_extension} [| f : (PROD x:A.B(x)); g: (PROD x:A.D(x)); - !!x. x:A ==> f`x = g`x - |] ==> f=g - -\idx{lamI} a:A ==> : (lam x:A. b(x)) -\idx{lamE} [| p: (lam x:A. b(x)); !!x.[| x:A; p= |] ==> P - |] ==> P - -\idx{lam_type} [| !!x. x:A ==> b(x): B(x) |] ==> - (lam x:A.b(x)) : (PROD x:A.B(x)) - -\idx{beta_conv} a : A ==> (lam x:A.b(x)) ` a = b(a) -\idx{eta_conv} f : (PROD x:A.B(x)) ==> (lam x:A. f`x) = f - -\idx{lam_theI} (!!x. x:A ==> EX! y. Q(x,y)) ==> EX h. ALL x:A. Q(x, h`x) - -\idx{restrict_conv} a : A ==> restrict(f,A) ` a = f`a -\idx{restrict_type} [| !!x. x:A ==> f`x: B(x) |] ==> - restrict(f,A) : (PROD x:A.B(x)) - -\idx{fun_empty} 0: 0->0 -\idx{fun_single} \{\} : \{a\} -> \{b\} - -\idx{fun_disjoint_Un} [| f: A->B; g: C->D; A Int C = 0 |] ==> - (f Un g) : (A Un C) -> (B Un D) - -\idx{fun_disjoint_apply1} [| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> - (f Un g)`a = f`a - -\idx{fun_disjoint_apply2} [| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> - (f Un g)`c = g`c - - -%%% SIMPDATA.ML - - a\in a & \bimp & False\\ - a\in \emptyset & \bimp & False\\ - a \in A \union B & \bimp & a\in A \disj a\in B\\ - a \in A \inter B & \bimp & a\in A \conj a\in B\\ - a \in A-B & \bimp & a\in A \conj \neg (a\in B)\\ - a \in {\tt cons}(b,B) & \bimp & a=b \disj a\in B\\ - i \in {\tt succ}(j) & \bimp & i=j \disj i\in j\\ - A\in \bigcup(C) & \bimp & (\exists B. B\in C \conj A\in B)\\ - A\in \bigcap(C) & \bimp & (\forall B. B\in C \imp A\in B) - \qquad (\exists B. B\in C)\\ - a \in {\tt Collect}(A,P) & \bimp & a\in A \conj P(a)\\ - b \in {\tt RepFun}(A,f) & \bimp & (\exists x. x\in A \conj b=f(x)) - -equalities.ML perm.ML plus.ML nat.ML ----------------------------------------------------------------- -equalities.ML - -\idx{Int_absorb} A Int A = A -\idx{Int_commute} A Int B = B Int A -\idx{Int_assoc} (A Int B) Int C = A Int (B Int C) -\idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) - -\idx{Un_absorb} A Un A = A -\idx{Un_commute} A Un B = B Un A -\idx{Un_assoc} (A Un B) Un C = A Un (B Un C) -\idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) - -\idx{Diff_cancel} A-A = 0 -\idx{Diff_disjoint} A Int (B-A) = 0 -\idx{Diff_partition} A<=B ==> A Un (B-A) = B -\idx{double_complement} [| A<=B; B<= C |] ==> (B - (C-A)) = A -\idx{Diff_Un} A - (B Un C) = (A-B) Int (A-C) -\idx{Diff_Int} A - (B Int C) = (A-B) Un (A-C) - -\idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B) -\idx{Inter_Un_distrib} [| a:A; b:B |] ==> - Inter(A Un B) = Inter(A) Int Inter(B) - -\idx{Int_Union_RepFun} A Int Union(B) = (UN C:B. A Int C) - -\idx{Un_Inter_RepFun} b:B ==> - A Un Inter(B) = (INT C:B. A Un C) - -\idx{SUM_Un_distrib1} (SUM x:A Un B. C(x)) = - (SUM x:A. C(x)) Un (SUM x:B. C(x)) - -\idx{SUM_Un_distrib2} (SUM x:C. A(x) Un B(x)) = - (SUM x:C. A(x)) Un (SUM x:C. B(x)) - -\idx{SUM_Int_distrib1} (SUM x:A Int B. C(x)) = - (SUM x:A. C(x)) Int (SUM x:B. C(x)) - -\idx{SUM_Int_distrib2} (SUM x:C. A(x) Int B(x)) = - (SUM x:C. A(x)) Int (SUM x:C. B(x)) - - ----------------------------------------------------------------- -perm.ML - -\idx{comp_def} - r O s == \{xz : domain(s)*range(r) . - EX x y z. xz= & :s & :r\}), -\idx{id_def} (*the identity function for A*) - id(A) == (lam x:A. x)), -\idx{inj_def} - inj(A,B) == - \{ f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x\}), -\idx{surj_def} - surj(A,B) == \{ f: A->B . ALL y:B. EX x:A. f`x=y\}), -\idx{bij_def} - bij(A,B) == inj(A,B) Int surj(A,B)) - - -\idx{surj_is_fun} f: surj(A,B) ==> f: A->B -\idx{fun_is_surj} f : Pi(A,B) ==> f: surj(A,range(f)) - -\idx{inj_is_fun} f: inj(A,B) ==> f: A->B -\idx{inj_equality} [| :f; :f; f: inj(A,B) |] ==> a=c - -\idx{bij_is_fun} f: bij(A,B) ==> f: A->B - -\idx{inj_converse_surj} f: inj(A,B) ==> converse(f): surj(range(f), A) - -\idx{left_inverse} [| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a -\idx{right_inverse} [| f: inj(A,B); b: range(f) |] ==> - f`(converse(f)`b) = b - -\idx{inj_converse_inj} f: inj(A,B) ==> converse(f): inj(range(f), A) -\idx{bij_converse_bij} f: bij(A,B) ==> converse(f): bij(B,A) - -\idx{comp_type} [| s<=A*B; r<=B*C |] ==> (r O s) <= A*C -\idx{comp_assoc} (r O s) O t = r O (s O t) - -\idx{left_comp_id} r<=A*B ==> id(B) O r = r -\idx{right_comp_id} r<=A*B ==> r O id(A) = r - -\idx{comp_func} [| g: A->B; f: B->C |] ==> (f O g) : A->C -\idx{comp_func_apply} [| g: A->B; f: B->C; a:A |] ==> (f O g)`a = f`(g`a) - -\idx{comp_inj} [| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C) -\idx{comp_surj} [| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C) -\idx{comp_bij} [| g: bij(A,B); f: bij(B,C) |] ==> (f O g) : bij(A,C) - -\idx{left_comp_inverse} f: inj(A,B) ==> converse(f) O f = id(A) -\idx{right_comp_inverse} f: surj(A,B) ==> f O converse(f) = id(B) - -\idx{bij_disjoint_Un} - [| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |] ==> - (f Un g) : bij(A Un C, B Un D) - -\idx{restrict_bij} [| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C) - - ----------------------------------------------------------------- -plus.ML - -\idx{plus_def} A+B == \{0\}*A Un \{\{0\}\}*B -\idx{Inl_def} Inl(a) == < 0 ,a> -\idx{Inr_def} Inr(b) == <\{0\},b> -\idx{when_def} when(u,c,d) == - THE y. EX z.(u=Inl(z) & y=c(z)) | (u=Inr(z) & y=d(z)) - -\idx{plus_InlI} a : A ==> Inl(a) : A+B -\idx{plus_InrI} b : B ==> Inr(b) : A+B - -\idx{Inl_inject} Inl(a) = Inl(b) ==> a=b -\idx{Inr_inject} Inr(a) = Inr(b) ==> a=b -\idx{Inl_neq_Inr} Inl(a)=Inr(b) ==> P - -\idx{plusE2} u: A+B ==> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y)) - -\idx{when_Inl_conv} when(Inl(a),c,d) = c(a) -\idx{when_Inr_conv} when(Inr(b),c,d) = d(b) - -\idx{when_type} [| u: A+B; - !!x. x: A ==> c(x): C(Inl(x)); - !!y. y: B ==> d(y): C(Inr(y)) - |] ==> when(u,c,d) : C(u) - - ----------------------------------------------------------------- -nat.ML - - -\idx{nat_def} nat == lfp(lam r: Pow(Inf). \{0\} Un RepFun(r,succ)) -\idx{nat_case_def} nat_case(n,a,b) == - THE y. n=0 & y=a | (EX x. n=succ(x) & y=b(x)) -\idx{nat_rec_def} nat_rec(k,a,b) == - transrec(nat, k, %n f. nat_case(n, a, %m. b(m, f`m))) - -\idx{nat_0_I} 0 : nat -\idx{nat_succ_I} n : nat ==> succ(n) : nat - -\idx{nat_induct} - [| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) - |] ==> P(n) - -\idx{nat_case_0_conv} nat_case(0,a,b) = a -\idx{nat_case_succ_conv} nat_case(succ(m),a,b) = b(m) - -\idx{nat_case_type} - [| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) - |] ==> nat_case(n,a,b) : C(n) - -\idx{nat_rec_0_conv} nat_rec(0,a,b) = a -\idx{nat_rec_succ_conv} m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b)) - -\idx{nat_rec_type} - [| n: nat; - a: C(0); - !!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) - |] ==> nat_rec(n,a,b) : C(n) diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/ZF.tex --- a/doc-src/Logics/ZF.tex Fri Jan 08 13:20:59 1999 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1892 +0,0 @@ -%% $Id$ -\chapter{Zermelo-Fraenkel Set Theory} -\index{set theory|(} - -The theory~\thydx{ZF} implements Zermelo-Fraenkel set -theory~\cite{halmos60,suppes72} as an extension of~\texttt{FOL}, classical -first-order logic. The theory includes a collection of derived natural -deduction rules, for use with Isabelle's classical reasoner. Much -of it is based on the work of No\"el~\cite{noel}. - -A tremendous amount of set theory has been formally developed, including -the basic properties of relations, functions, ordinals and cardinals. -Significant results have been proved, such as the Schr\"oder-Bernstein -Theorem, the Wellordering Theorem and a version of Ramsey's Theorem. -General methods have been developed for solving recursion equations over -monotonic functors; these have been applied to yield constructions of -lists, trees, infinite lists, etc. The Recursion Theorem has been proved, -admitting recursive definitions of functions over well-founded relations. -Thus, we may even regard set theory as a computational logic, loosely -inspired by Martin-L\"of's Type Theory. - -Because {\ZF} is an extension of {\FOL}, it provides the same -packages, namely \texttt{hyp_subst_tac}, the simplifier, and the -classical reasoner. The default simpset and claset are usually -satisfactory. Named simpsets include \ttindexbold{ZF_ss} (basic set -theory rules) and \ttindexbold{rank_ss} (for proving termination of -well-founded recursion). Named clasets include \ttindexbold{ZF_cs} -(basic set theory) and \ttindexbold{le_cs} (useful for reasoning about -the relations $<$ and $\le$). - -\texttt{ZF} has a flexible package for handling inductive definitions, -such as inference systems, and datatype definitions, such as lists and -trees. Moreover it handles coinductive definitions, such as -bisimulation relations, and codatatype definitions, such as streams. -There is a paper \cite{paulson-CADE} describing the package, but its -examples use an obsolete declaration syntax. Please consult the -version of the paper distributed with Isabelle. - -Recent reports~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF} less -formally than this chapter. Isabelle employs a novel treatment of -non-well-founded data structures within the standard {\sc zf} axioms including -the Axiom of Foundation~\cite{paulson-final}. - - -\section{Which version of axiomatic set theory?} -The two main axiom systems for set theory are Bernays-G\"odel~({\sc bg}) -and Zermelo-Fraenkel~({\sc zf}). Resolution theorem provers can use {\sc - bg} because it is finite~\cite{boyer86,quaife92}. {\sc zf} does not -have a finite axiom system because of its Axiom Scheme of Replacement. -This makes it awkward to use with many theorem provers, since instances -of the axiom scheme have to be invoked explicitly. Since Isabelle has no -difficulty with axiom schemes, we may adopt either axiom system. - -These two theories differ in their treatment of {\bf classes}, which are -collections that are `too big' to be sets. The class of all sets,~$V$, -cannot be a set without admitting Russell's Paradox. In {\sc bg}, both -classes and sets are individuals; $x\in V$ expresses that $x$ is a set. In -{\sc zf}, all variables denote sets; classes are identified with unary -predicates. The two systems define essentially the same sets and classes, -with similar properties. In particular, a class cannot belong to another -class (let alone a set). - -Modern set theorists tend to prefer {\sc zf} because they are mainly concerned -with sets, rather than classes. {\sc bg} requires tiresome proofs that various -collections are sets; for instance, showing $x\in\{x\}$ requires showing that -$x$ is a set. - - -\begin{figure} \small -\begin{center} -\begin{tabular}{rrr} - \it name &\it meta-type & \it description \\ - \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder\\ - \cdx{0} & $i$ & empty set\\ - \cdx{cons} & $[i,i]\To i$ & finite set constructor\\ - \cdx{Upair} & $[i,i]\To i$ & unordered pairing\\ - \cdx{Pair} & $[i,i]\To i$ & ordered pairing\\ - \cdx{Inf} & $i$ & infinite set\\ - \cdx{Pow} & $i\To i$ & powerset\\ - \cdx{Union} \cdx{Inter} & $i\To i$ & set union/intersection \\ - \cdx{split} & $[[i,i]\To i, i] \To i$ & generalized projection\\ - \cdx{fst} \cdx{snd} & $i\To i$ & projections\\ - \cdx{converse}& $i\To i$ & converse of a relation\\ - \cdx{succ} & $i\To i$ & successor\\ - \cdx{Collect} & $[i,i\To o]\To i$ & separation\\ - \cdx{Replace} & $[i, [i,i]\To o] \To i$ & replacement\\ - \cdx{PrimReplace} & $[i, [i,i]\To o] \To i$ & primitive replacement\\ - \cdx{RepFun} & $[i, i\To i] \To i$ & functional replacement\\ - \cdx{Pi} \cdx{Sigma} & $[i,i\To i]\To i$ & general product/sum\\ - \cdx{domain} & $i\To i$ & domain of a relation\\ - \cdx{range} & $i\To i$ & range of a relation\\ - \cdx{field} & $i\To i$ & field of a relation\\ - \cdx{Lambda} & $[i, i\To i]\To i$ & $\lambda$-abstraction\\ - \cdx{restrict}& $[i, i] \To i$ & restriction of a function\\ - \cdx{The} & $[i\To o]\To i$ & definite description\\ - \cdx{if} & $[o,i,i]\To i$ & conditional\\ - \cdx{Ball} \cdx{Bex} & $[i, i\To o]\To o$ & bounded quantifiers -\end{tabular} -\end{center} -\subcaption{Constants} - -\begin{center} -\index{*"`"` symbol} -\index{*"-"`"` symbol} -\index{*"` symbol}\index{function applications!in \ZF} -\index{*"- symbol} -\index{*": symbol} -\index{*"<"= symbol} -\begin{tabular}{rrrr} - \it symbol & \it meta-type & \it priority & \it description \\ - \tt `` & $[i,i]\To i$ & Left 90 & image \\ - \tt -`` & $[i,i]\To i$ & Left 90 & inverse image \\ - \tt ` & $[i,i]\To i$ & Left 90 & application \\ - \sdx{Int} & $[i,i]\To i$ & Left 70 & intersection ($\int$) \\ - \sdx{Un} & $[i,i]\To i$ & Left 65 & union ($\un$) \\ - \tt - & $[i,i]\To i$ & Left 65 & set difference ($-$) \\[1ex] - \tt: & $[i,i]\To o$ & Left 50 & membership ($\in$) \\ - \tt <= & $[i,i]\To o$ & Left 50 & subset ($\subseteq$) -\end{tabular} -\end{center} -\subcaption{Infixes} -\caption{Constants of {\ZF}} \label{zf-constants} -\end{figure} - - -\section{The syntax of set theory} -The language of set theory, as studied by logicians, has no constants. The -traditional axioms merely assert the existence of empty sets, unions, -powersets, etc.; this would be intolerable for practical reasoning. The -Isabelle theory declares constants for primitive sets. It also extends -\texttt{FOL} with additional syntax for finite sets, ordered pairs, -comprehension, general union/intersection, general sums/products, and -bounded quantifiers. In most other respects, Isabelle implements precisely -Zermelo-Fraenkel set theory. - -Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while -Figure~\ref{zf-trans} presents the syntax translations. Finally, -Figure~\ref{zf-syntax} presents the full grammar for set theory, including -the constructs of \FOL. - -Local abbreviations can be introduced by a \texttt{let} construct whose -syntax appears in Fig.\ts\ref{zf-syntax}. Internally it is translated into -the constant~\cdx{Let}. It can be expanded by rewriting with its -definition, \tdx{Let_def}. - -Apart from \texttt{let}, set theory does not use polymorphism. All terms in -{\ZF} have type~\tydx{i}, which is the type of individuals and has class~{\tt - term}. The type of first-order formulae, remember, is~\textit{o}. - -Infix operators include binary union and intersection ($A\un B$ and -$A\int B$), set difference ($A-B$), and the subset and membership -relations. Note that $a$\verb|~:|$b$ is translated to $\neg(a\in b)$. The -union and intersection operators ($\bigcup A$ and $\bigcap A$) form the -union or intersection of a set of sets; $\bigcup A$ means the same as -$\bigcup@{x\in A}x$. Of these operators, only $\bigcup A$ is primitive. - -The constant \cdx{Upair} constructs unordered pairs; thus {\tt - Upair($A$,$B$)} denotes the set~$\{A,B\}$ and \texttt{Upair($A$,$A$)} -denotes the singleton~$\{A\}$. General union is used to define binary -union. The Isabelle version goes on to define the constant -\cdx{cons}: -\begin{eqnarray*} - A\cup B & \equiv & \bigcup(\texttt{Upair}(A,B)) \\ - \texttt{cons}(a,B) & \equiv & \texttt{Upair}(a,a) \un B -\end{eqnarray*} -The $\{a@1, \ldots\}$ notation abbreviates finite sets constructed in the -obvious manner using~\texttt{cons} and~$\emptyset$ (the empty set): -\begin{eqnarray*} - \{a,b,c\} & \equiv & \texttt{cons}(a,\texttt{cons}(b,\texttt{cons}(c,\emptyset))) -\end{eqnarray*} - -The constant \cdx{Pair} constructs ordered pairs, as in {\tt -Pair($a$,$b$)}. Ordered pairs may also be written within angle brackets, -as {\tt<$a$,$b$>}. The $n$-tuple {\tt<$a@1$,\ldots,$a@{n-1}$,$a@n$>} -abbreviates the nest of pairs\par\nobreak -\centerline\texttt{Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).} - -In {\ZF}, a function is a set of pairs. A {\ZF} function~$f$ is simply an -individual as far as Isabelle is concerned: its Isabelle type is~$i$, not -say $i\To i$. The infix operator~{\tt`} denotes the application of a -function set to its argument; we must write~$f{\tt`}x$, not~$f(x)$. The -syntax for image is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$. - - -\begin{figure} -\index{lambda abs@$\lambda$-abstractions!in \ZF} -\index{*"-"> symbol} -\index{*"* symbol} -\begin{center} \footnotesize\tt\frenchspacing -\begin{tabular}{rrr} - \it external & \it internal & \it description \\ - $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\ - \ttlbrace$a@1$, $\ldots$, $a@n$\ttrbrace & cons($a@1$,$\ldots$,cons($a@n$,0)) & - \rm finite set \\ - <$a@1$, $\ldots$, $a@{n-1}$, $a@n$> & - Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) & - \rm ordered $n$-tuple \\ - \ttlbrace$x$:$A . P[x]$\ttrbrace & Collect($A$,$\lambda x. P[x]$) & - \rm separation \\ - \ttlbrace$y . x$:$A$, $Q[x,y]$\ttrbrace & Replace($A$,$\lambda x\,y. Q[x,y]$) & - \rm replacement \\ - \ttlbrace$b[x] . x$:$A$\ttrbrace & RepFun($A$,$\lambda x. b[x]$) & - \rm functional replacement \\ - \sdx{INT} $x$:$A . B[x]$ & Inter(\ttlbrace$B[x] . x$:$A$\ttrbrace) & - \rm general intersection \\ - \sdx{UN} $x$:$A . B[x]$ & Union(\ttlbrace$B[x] . x$:$A$\ttrbrace) & - \rm general union \\ - \sdx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x. B[x]$) & - \rm general product \\ - \sdx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x. B[x]$) & - \rm general sum \\ - $A$ -> $B$ & Pi($A$,$\lambda x. B$) & - \rm function space \\ - $A$ * $B$ & Sigma($A$,$\lambda x. B$) & - \rm binary product \\ - \sdx{THE} $x . P[x]$ & The($\lambda x. P[x]$) & - \rm definite description \\ - \sdx{lam} $x$:$A . b[x]$ & Lambda($A$,$\lambda x. b[x]$) & - \rm $\lambda$-abstraction\\[1ex] - \sdx{ALL} $x$:$A . P[x]$ & Ball($A$,$\lambda x. P[x]$) & - \rm bounded $\forall$ \\ - \sdx{EX} $x$:$A . P[x]$ & Bex($A$,$\lambda x. P[x]$) & - \rm bounded $\exists$ -\end{tabular} -\end{center} -\caption{Translations for {\ZF}} \label{zf-trans} -\end{figure} - - -\begin{figure} -\index{*let symbol} -\index{*in symbol} -\dquotes -\[\begin{array}{rcl} - term & = & \hbox{expression of type~$i$} \\ - & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\ - & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\ - & | & "< " term\; ("," term)^* " >" \\ - & | & "{\ttlbrace} " id ":" term " . " formula " {\ttrbrace}" \\ - & | & "{\ttlbrace} " id " . " id ":" term ", " formula " {\ttrbrace}" \\ - & | & "{\ttlbrace} " term " . " id ":" term " {\ttrbrace}" \\ - & | & term " `` " term \\ - & | & term " -`` " term \\ - & | & term " ` " term \\ - & | & term " * " term \\ - & | & term " Int " term \\ - & | & term " Un " term \\ - & | & term " - " term \\ - & | & term " -> " term \\ - & | & "THE~~" id " . " formula\\ - & | & "lam~~" id ":" term " . " term \\ - & | & "INT~~" id ":" term " . " term \\ - & | & "UN~~~" id ":" term " . " term \\ - & | & "PROD~" id ":" term " . " term \\ - & | & "SUM~~" id ":" term " . " term \\[2ex] - formula & = & \hbox{expression of type~$o$} \\ - & | & term " : " term \\ - & | & term " \ttilde: " term \\ - & | & term " <= " term \\ - & | & term " = " term \\ - & | & term " \ttilde= " term \\ - & | & "\ttilde\ " formula \\ - & | & formula " \& " formula \\ - & | & formula " | " formula \\ - & | & formula " --> " formula \\ - & | & formula " <-> " formula \\ - & | & "ALL " id ":" term " . " formula \\ - & | & "EX~~" id ":" term " . " formula \\ - & | & "ALL~" id~id^* " . " formula \\ - & | & "EX~~" id~id^* " . " formula \\ - & | & "EX!~" id~id^* " . " formula - \end{array} -\] -\caption{Full grammar for {\ZF}} \label{zf-syntax} -\end{figure} - - -\section{Binding operators} -The constant \cdx{Collect} constructs sets by the principle of {\bf - separation}. The syntax for separation is -\hbox{\tt\ttlbrace$x$:$A$. $P[x]$\ttrbrace}, where $P[x]$ is a formula -that may contain free occurrences of~$x$. It abbreviates the set {\tt - Collect($A$,$\lambda x. P[x]$)}, which consists of all $x\in A$ that -satisfy~$P[x]$. Note that \texttt{Collect} is an unfortunate choice of -name: some set theories adopt a set-formation principle, related to -replacement, called collection. - -The constant \cdx{Replace} constructs sets by the principle of {\bf - replacement}. The syntax -\hbox{\tt\ttlbrace$y$. $x$:$A$,$Q[x,y]$\ttrbrace} denotes the set {\tt - Replace($A$,$\lambda x\,y. Q[x,y]$)}, which consists of all~$y$ such -that there exists $x\in A$ satisfying~$Q[x,y]$. The Replacement Axiom -has the condition that $Q$ must be single-valued over~$A$: for -all~$x\in A$ there exists at most one $y$ satisfying~$Q[x,y]$. A -single-valued binary predicate is also called a {\bf class function}. - -The constant \cdx{RepFun} expresses a special case of replacement, -where $Q[x,y]$ has the form $y=b[x]$. Such a $Q$ is trivially -single-valued, since it is just the graph of the meta-level -function~$\lambda x. b[x]$. The resulting set consists of all $b[x]$ -for~$x\in A$. This is analogous to the \ML{} functional \texttt{map}, -since it applies a function to every element of a set. The syntax is -\hbox{\tt\ttlbrace$b[x]$. $x$:$A$\ttrbrace}, which expands to {\tt - RepFun($A$,$\lambda x. b[x]$)}. - -\index{*INT symbol}\index{*UN symbol} -General unions and intersections of indexed -families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$, -are written \hbox{\tt UN $x$:$A$. $B[x]$} and \hbox{\tt INT $x$:$A$. $B[x]$}. -Their meaning is expressed using \texttt{RepFun} as -\[ -\bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad -\bigcap(\{B[x]. x\in A\}). -\] -General sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$ can be -constructed in set theory, where $B[x]$ is a family of sets over~$A$. They -have as special cases $A\times B$ and $A\to B$, where $B$ is simply a set. -This is similar to the situation in Constructive Type Theory (set theory -has `dependent sets') and calls for similar syntactic conventions. The -constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and -products. Instead of \texttt{Sigma($A$,$B$)} and \texttt{Pi($A$,$B$)} we may write -\hbox{\tt SUM $x$:$A$. $B[x]$} and \hbox{\tt PROD $x$:$A$. $B[x]$}. -\index{*SUM symbol}\index{*PROD symbol}% -The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$->$B$} abbreviate -general sums and products over a constant family.\footnote{Unlike normal -infix operators, {\tt*} and {\tt->} merely define abbreviations; there are -no constants~{\tt op~*} and~\hbox{\tt op~->}.} Isabelle accepts these -abbreviations in parsing and uses them whenever possible for printing. - -\index{*THE symbol} -As mentioned above, whenever the axioms assert the existence and uniqueness -of a set, Isabelle's set theory declares a constant for that set. These -constants can express the {\bf definite description} operator~$\iota -x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists. -Since all terms in {\ZF} denote something, a description is always -meaningful, but we do not know its value unless $P[x]$ defines it uniquely. -Using the constant~\cdx{The}, we may write descriptions as {\tt - The($\lambda x. P[x]$)} or use the syntax \hbox{\tt THE $x$. $P[x]$}. - -\index{*lam symbol} -Function sets may be written in $\lambda$-notation; $\lambda x\in A. b[x]$ -stands for the set of all pairs $\pair{x,b[x]}$ for $x\in A$. In order for -this to be a set, the function's domain~$A$ must be given. Using the -constant~\cdx{Lambda}, we may express function sets as {\tt -Lambda($A$,$\lambda x. b[x]$)} or use the syntax \hbox{\tt lam $x$:$A$. $b[x]$}. - -Isabelle's set theory defines two {\bf bounded quantifiers}: -\begin{eqnarray*} - \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ - \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] -\end{eqnarray*} -The constants~\cdx{Ball} and~\cdx{Bex} are defined -accordingly. Instead of \texttt{Ball($A$,$P$)} and \texttt{Bex($A$,$P$)} we may -write -\hbox{\tt ALL $x$:$A$. $P[x]$} and \hbox{\tt EX $x$:$A$. $P[x]$}. - - -%%%% ZF.thy - -\begin{figure} -\begin{ttbox} -\tdx{Let_def} Let(s, f) == f(s) - -\tdx{Ball_def} Ball(A,P) == ALL x. x:A --> P(x) -\tdx{Bex_def} Bex(A,P) == EX x. x:A & P(x) - -\tdx{subset_def} A <= B == ALL x:A. x:B -\tdx{extension} A = B <-> A <= B & B <= A - -\tdx{Union_iff} A : Union(C) <-> (EX B:C. A:B) -\tdx{Pow_iff} A : Pow(B) <-> A <= B -\tdx{foundation} A=0 | (EX x:A. ALL y:x. ~ y:A) - -\tdx{replacement} (ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> - b : PrimReplace(A,P) <-> (EX x:A. P(x,b)) -\subcaption{The Zermelo-Fraenkel Axioms} - -\tdx{Replace_def} Replace(A,P) == - PrimReplace(A, \%x y. (EX!z. P(x,z)) & P(x,y)) -\tdx{RepFun_def} RepFun(A,f) == {\ttlbrace}y . x:A, y=f(x)\ttrbrace -\tdx{the_def} The(P) == Union({\ttlbrace}y . x:{\ttlbrace}0{\ttrbrace}, P(y){\ttrbrace}) -\tdx{if_def} if(P,a,b) == THE z. P & z=a | ~P & z=b -\tdx{Collect_def} Collect(A,P) == {\ttlbrace}y . x:A, x=y & P(x){\ttrbrace} -\tdx{Upair_def} Upair(a,b) == - {\ttlbrace}y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b){\ttrbrace} -\subcaption{Consequences of replacement} - -\tdx{Inter_def} Inter(A) == {\ttlbrace}x:Union(A) . ALL y:A. x:y{\ttrbrace} -\tdx{Un_def} A Un B == Union(Upair(A,B)) -\tdx{Int_def} A Int B == Inter(Upair(A,B)) -\tdx{Diff_def} A - B == {\ttlbrace}x:A . x~:B{\ttrbrace} -\subcaption{Union, intersection, difference} -\end{ttbox} -\caption{Rules and axioms of {\ZF}} \label{zf-rules} -\end{figure} - - -\begin{figure} -\begin{ttbox} -\tdx{cons_def} cons(a,A) == Upair(a,a) Un A -\tdx{succ_def} succ(i) == cons(i,i) -\tdx{infinity} 0:Inf & (ALL y:Inf. succ(y): Inf) -\subcaption{Finite and infinite sets} - -\tdx{Pair_def} == {\ttlbrace}{\ttlbrace}a,a{\ttrbrace}, {\ttlbrace}a,b{\ttrbrace}{\ttrbrace} -\tdx{split_def} split(c,p) == THE y. EX a b. p= & y=c(a,b) -\tdx{fst_def} fst(A) == split(\%x y. x, p) -\tdx{snd_def} snd(A) == split(\%x y. y, p) -\tdx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). {\ttlbrace}{\ttrbrace} -\subcaption{Ordered pairs and Cartesian products} - -\tdx{converse_def} converse(r) == {\ttlbrace}z. w:r, EX x y. w= & z={\ttrbrace} -\tdx{domain_def} domain(r) == {\ttlbrace}x. w:r, EX y. w={\ttrbrace} -\tdx{range_def} range(r) == domain(converse(r)) -\tdx{field_def} field(r) == domain(r) Un range(r) -\tdx{image_def} r `` A == {\ttlbrace}y : range(r) . EX x:A. : r{\ttrbrace} -\tdx{vimage_def} r -`` A == converse(r)``A -\subcaption{Operations on relations} - -\tdx{lam_def} Lambda(A,b) == {\ttlbrace} . x:A{\ttrbrace} -\tdx{apply_def} f`a == THE y. : f -\tdx{Pi_def} Pi(A,B) == {\ttlbrace}f: Pow(Sigma(A,B)). ALL x:A. EX! y. : f{\ttrbrace} -\tdx{restrict_def} restrict(f,A) == lam x:A. f`x -\subcaption{Functions and general product} -\end{ttbox} -\caption{Further definitions of {\ZF}} \label{zf-defs} -\end{figure} - - - -\section{The Zermelo-Fraenkel axioms} -The axioms appear in Fig.\ts \ref{zf-rules}. They resemble those -presented by Suppes~\cite{suppes72}. Most of the theory consists of -definitions. In particular, bounded quantifiers and the subset relation -appear in other axioms. Object-level quantifiers and implications have -been replaced by meta-level ones wherever possible, to simplify use of the -axioms. See the file \texttt{ZF/ZF.thy} for details. - -The traditional replacement axiom asserts -\[ y \in \texttt{PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \] -subject to the condition that $P(x,y)$ is single-valued for all~$x\in A$. -The Isabelle theory defines \cdx{Replace} to apply -\cdx{PrimReplace} to the single-valued part of~$P$, namely -\[ (\exists!z. P(x,z)) \conj P(x,y). \] -Thus $y\in \texttt{Replace}(A,P)$ if and only if there is some~$x$ such that -$P(x,-)$ holds uniquely for~$y$. Because the equivalence is unconditional, -\texttt{Replace} is much easier to use than \texttt{PrimReplace}; it defines the -same set, if $P(x,y)$ is single-valued. The nice syntax for replacement -expands to \texttt{Replace}. - -Other consequences of replacement include functional replacement -(\cdx{RepFun}) and definite descriptions (\cdx{The}). -Axioms for separation (\cdx{Collect}) and unordered pairs -(\cdx{Upair}) are traditionally assumed, but they actually follow -from replacement~\cite[pages 237--8]{suppes72}. - -The definitions of general intersection, etc., are straightforward. Note -the definition of \texttt{cons}, which underlies the finite set notation. -The axiom of infinity gives us a set that contains~0 and is closed under -successor (\cdx{succ}). Although this set is not uniquely defined, -the theory names it (\cdx{Inf}) in order to simplify the -construction of the natural numbers. - -Further definitions appear in Fig.\ts\ref{zf-defs}. Ordered pairs are -defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$. Recall -that \cdx{Sigma}$(A,B)$ generalizes the Cartesian product of two -sets. It is defined to be the union of all singleton sets -$\{\pair{x,y}\}$, for $x\in A$ and $y\in B(x)$. This is a typical usage of -general union. - -The projections \cdx{fst} and~\cdx{snd} are defined in terms of the -generalized projection \cdx{split}. The latter has been borrowed from -Martin-L\"of's Type Theory, and is often easier to use than \cdx{fst} -and~\cdx{snd}. - -Operations on relations include converse, domain, range, and image. The -set ${\tt Pi}(A,B)$ generalizes the space of functions between two sets. -Note the simple definitions of $\lambda$-abstraction (using -\cdx{RepFun}) and application (using a definite description). The -function \cdx{restrict}$(f,A)$ has the same values as~$f$, but only -over the domain~$A$. - - -%%%% zf.ML - -\begin{figure} -\begin{ttbox} -\tdx{ballI} [| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x) -\tdx{bspec} [| ALL x:A. P(x); x: A |] ==> P(x) -\tdx{ballE} [| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q - -\tdx{ball_cong} [| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> - (ALL x:A. P(x)) <-> (ALL x:A'. P'(x)) - -\tdx{bexI} [| P(x); x: A |] ==> EX x:A. P(x) -\tdx{bexCI} [| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A. P(x) -\tdx{bexE} [| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q - -\tdx{bex_cong} [| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> - (EX x:A. P(x)) <-> (EX x:A'. P'(x)) -\subcaption{Bounded quantifiers} - -\tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B -\tdx{subsetD} [| A <= B; c:A |] ==> c:B -\tdx{subsetCE} [| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P -\tdx{subset_refl} A <= A -\tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C - -\tdx{equalityI} [| A <= B; B <= A |] ==> A = B -\tdx{equalityD1} A = B ==> A<=B -\tdx{equalityD2} A = B ==> B<=A -\tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P -\subcaption{Subsets and extensionality} - -\tdx{emptyE} a:0 ==> P -\tdx{empty_subsetI} 0 <= A -\tdx{equals0I} [| !!y. y:A ==> False |] ==> A=0 -\tdx{equals0D} [| A=0; a:A |] ==> P - -\tdx{PowI} A <= B ==> A : Pow(B) -\tdx{PowD} A : Pow(B) ==> A<=B -\subcaption{The empty set; power sets} -\end{ttbox} -\caption{Basic derived rules for {\ZF}} \label{zf-lemmas1} -\end{figure} - - -\section{From basic lemmas to function spaces} -Faced with so many definitions, it is essential to prove lemmas. Even -trivial theorems like $A \int B = B \int A$ would be difficult to -prove from the definitions alone. Isabelle's set theory derives many -rules using a natural deduction style. Ideally, a natural deduction -rule should introduce or eliminate just one operator, but this is not -always practical. For most operators, we may forget its definition -and use its derived rules instead. - -\subsection{Fundamental lemmas} -Figure~\ref{zf-lemmas1} presents the derived rules for the most basic -operators. The rules for the bounded quantifiers resemble those for the -ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption -in the style of Isabelle's classical reasoner. The \rmindex{congruence - rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's -simplifier, but have few other uses. Congruence rules must be specially -derived for all binding operators, and henceforth will not be shown. - -Figure~\ref{zf-lemmas1} also shows rules for the subset and equality -relations (proof by extensionality), and rules about the empty set and the -power set operator. - -Figure~\ref{zf-lemmas2} presents rules for replacement and separation. -The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than -comparable rules for \texttt{PrimReplace} would be. The principle of -separation is proved explicitly, although most proofs should use the -natural deduction rules for \texttt{Collect}. The elimination rule -\tdx{CollectE} is equivalent to the two destruction rules -\tdx{CollectD1} and \tdx{CollectD2}, but each rule is suited to -particular circumstances. Although too many rules can be confusing, there -is no reason to aim for a minimal set of rules. See the file -\texttt{ZF/ZF.ML} for a complete listing. - -Figure~\ref{zf-lemmas3} presents rules for general union and intersection. -The empty intersection should be undefined. We cannot have -$\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set. All -expressions denote something in {\ZF} set theory; the definition of -intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is -arbitrary. The rule \tdx{InterI} must have a premise to exclude -the empty intersection. Some of the laws governing intersections require -similar premises. - - -%the [p] gives better page breaking for the book -\begin{figure}[p] -\begin{ttbox} -\tdx{ReplaceI} [| x: A; P(x,b); !!y. P(x,y) ==> y=b |] ==> - b : {\ttlbrace}y. x:A, P(x,y){\ttrbrace} - -\tdx{ReplaceE} [| b : {\ttlbrace}y. x:A, P(x,y){\ttrbrace}; - !!x. [| x: A; P(x,b); ALL y. P(x,y)-->y=b |] ==> R - |] ==> R - -\tdx{RepFunI} [| a : A |] ==> f(a) : {\ttlbrace}f(x). x:A{\ttrbrace} -\tdx{RepFunE} [| b : {\ttlbrace}f(x). x:A{\ttrbrace}; - !!x.[| x:A; b=f(x) |] ==> P |] ==> P - -\tdx{separation} a : {\ttlbrace}x:A. P(x){\ttrbrace} <-> a:A & P(a) -\tdx{CollectI} [| a:A; P(a) |] ==> a : {\ttlbrace}x:A. P(x){\ttrbrace} -\tdx{CollectE} [| a : {\ttlbrace}x:A. P(x){\ttrbrace}; [| a:A; P(a) |] ==> R |] ==> R -\tdx{CollectD1} a : {\ttlbrace}x:A. P(x){\ttrbrace} ==> a:A -\tdx{CollectD2} a : {\ttlbrace}x:A. P(x){\ttrbrace} ==> P(a) -\end{ttbox} -\caption{Replacement and separation} \label{zf-lemmas2} -\end{figure} - - -\begin{figure} -\begin{ttbox} -\tdx{UnionI} [| B: C; A: B |] ==> A: Union(C) -\tdx{UnionE} [| A : Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R - -\tdx{InterI} [| !!x. x: C ==> A: x; c:C |] ==> A : Inter(C) -\tdx{InterD} [| A : Inter(C); B : C |] ==> A : B -\tdx{InterE} [| A : Inter(C); A:B ==> R; ~ B:C ==> R |] ==> R - -\tdx{UN_I} [| a: A; b: B(a) |] ==> b: (UN x:A. B(x)) -\tdx{UN_E} [| b : (UN x:A. B(x)); !!x.[| x: A; b: B(x) |] ==> R - |] ==> R - -\tdx{INT_I} [| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x)) -\tdx{INT_E} [| b : (INT x:A. B(x)); a: A |] ==> b : B(a) -\end{ttbox} -\caption{General union and intersection} \label{zf-lemmas3} -\end{figure} - - -%%% upair.ML - -\begin{figure} -\begin{ttbox} -\tdx{pairing} a:Upair(b,c) <-> (a=b | a=c) -\tdx{UpairI1} a : Upair(a,b) -\tdx{UpairI2} b : Upair(a,b) -\tdx{UpairE} [| a : Upair(b,c); a = b ==> P; a = c ==> P |] ==> P -\end{ttbox} -\caption{Unordered pairs} \label{zf-upair1} -\end{figure} - - -\begin{figure} -\begin{ttbox} -\tdx{UnI1} c : A ==> c : A Un B -\tdx{UnI2} c : B ==> c : A Un B -\tdx{UnCI} (~c : B ==> c : A) ==> c : A Un B -\tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P - -\tdx{IntI} [| c : A; c : B |] ==> c : A Int B -\tdx{IntD1} c : A Int B ==> c : A -\tdx{IntD2} c : A Int B ==> c : B -\tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P - -\tdx{DiffI} [| c : A; ~ c : B |] ==> c : A - B -\tdx{DiffD1} c : A - B ==> c : A -\tdx{DiffD2} c : A - B ==> c ~: B -\tdx{DiffE} [| c : A - B; [| c:A; ~ c:B |] ==> P |] ==> P -\end{ttbox} -\caption{Union, intersection, difference} \label{zf-Un} -\end{figure} - - -\begin{figure} -\begin{ttbox} -\tdx{consI1} a : cons(a,B) -\tdx{consI2} a : B ==> a : cons(b,B) -\tdx{consCI} (~ a:B ==> a=b) ==> a: cons(b,B) -\tdx{consE} [| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P - -\tdx{singletonI} a : {\ttlbrace}a{\ttrbrace} -\tdx{singletonE} [| a : {\ttlbrace}b{\ttrbrace}; a=b ==> P |] ==> P -\end{ttbox} -\caption{Finite and singleton sets} \label{zf-upair2} -\end{figure} - - -\begin{figure} -\begin{ttbox} -\tdx{succI1} i : succ(i) -\tdx{succI2} i : j ==> i : succ(j) -\tdx{succCI} (~ i:j ==> i=j) ==> i: succ(j) -\tdx{succE} [| i : succ(j); i=j ==> P; i:j ==> P |] ==> P -\tdx{succ_neq_0} [| succ(n)=0 |] ==> P -\tdx{succ_inject} succ(m) = succ(n) ==> m=n -\end{ttbox} -\caption{The successor function} \label{zf-succ} -\end{figure} - - -\begin{figure} -\begin{ttbox} -\tdx{the_equality} [| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a -\tdx{theI} EX! x. P(x) ==> P(THE x. P(x)) - -\tdx{if_P} P ==> if(P,a,b) = a -\tdx{if_not_P} ~P ==> if(P,a,b) = b - -\tdx{mem_asym} [| a:b; b:a |] ==> P -\tdx{mem_irrefl} a:a ==> P -\end{ttbox} -\caption{Descriptions; non-circularity} \label{zf-the} -\end{figure} - - -\subsection{Unordered pairs and finite sets} -Figure~\ref{zf-upair1} presents the principle of unordered pairing, along -with its derived rules. Binary union and intersection are defined in terms -of ordered pairs (Fig.\ts\ref{zf-Un}). Set difference is also included. The -rule \tdx{UnCI} is useful for classical reasoning about unions, -like \texttt{disjCI}\@; it supersedes \tdx{UnI1} and -\tdx{UnI2}, but these rules are often easier to work with. For -intersection and difference we have both elimination and destruction rules. -Again, there is no reason to provide a minimal rule set. - -Figure~\ref{zf-upair2} is concerned with finite sets: it presents rules -for~\texttt{cons}, the finite set constructor, and rules for singleton -sets. Figure~\ref{zf-succ} presents derived rules for the successor -function, which is defined in terms of~\texttt{cons}. The proof that {\tt - succ} is injective appears to require the Axiom of Foundation. - -Definite descriptions (\sdx{THE}) are defined in terms of the singleton -set~$\{0\}$, but their derived rules fortunately hide this -(Fig.\ts\ref{zf-the}). The rule~\tdx{theI} is difficult to apply -because of the two occurrences of~$\Var{P}$. However, -\tdx{the_equality} does not have this problem and the files contain -many examples of its use. - -Finally, the impossibility of having both $a\in b$ and $b\in a$ -(\tdx{mem_asym}) is proved by applying the Axiom of Foundation to -the set $\{a,b\}$. The impossibility of $a\in a$ is a trivial consequence. - -See the file \texttt{ZF/upair.ML} for full proofs of the rules discussed in -this section. - - -%%% subset.ML - -\begin{figure} -\begin{ttbox} -\tdx{Union_upper} B:A ==> B <= Union(A) -\tdx{Union_least} [| !!x. x:A ==> x<=C |] ==> Union(A) <= C - -\tdx{Inter_lower} B:A ==> Inter(A) <= B -\tdx{Inter_greatest} [| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A) - -\tdx{Un_upper1} A <= A Un B -\tdx{Un_upper2} B <= A Un B -\tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C - -\tdx{Int_lower1} A Int B <= A -\tdx{Int_lower2} A Int B <= B -\tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B - -\tdx{Diff_subset} A-B <= A -\tdx{Diff_contains} [| C<=A; C Int B = 0 |] ==> C <= A-B - -\tdx{Collect_subset} Collect(A,P) <= A -\end{ttbox} -\caption{Subset and lattice properties} \label{zf-subset} -\end{figure} - - -\subsection{Subset and lattice properties} -The subset relation is a complete lattice. Unions form least upper bounds; -non-empty intersections form greatest lower bounds. Figure~\ref{zf-subset} -shows the corresponding rules. A few other laws involving subsets are -included. Proofs are in the file \texttt{ZF/subset.ML}. - -Reasoning directly about subsets often yields clearer proofs than -reasoning about the membership relation. Section~\ref{sec:ZF-pow-example} -below presents an example of this, proving the equation ${{\tt Pow}(A)\cap - {\tt Pow}(B)}= {\tt Pow}(A\cap B)$. - -%%% pair.ML - -\begin{figure} -\begin{ttbox} -\tdx{Pair_inject1} = ==> a=c -\tdx{Pair_inject2} = ==> b=d -\tdx{Pair_inject} [| = ; [| a=c; b=d |] ==> P |] ==> P -\tdx{Pair_neq_0} =0 ==> P - -\tdx{fst_conv} fst() = a -\tdx{snd_conv} snd() = b -\tdx{split} split(\%x y. c(x,y), ) = c(a,b) - -\tdx{SigmaI} [| a:A; b:B(a) |] ==> : Sigma(A,B) - -\tdx{SigmaE} [| c: Sigma(A,B); - !!x y.[| x:A; y:B(x); c= |] ==> P |] ==> P - -\tdx{SigmaE2} [| : Sigma(A,B); - [| a:A; b:B(a) |] ==> P |] ==> P -\end{ttbox} -\caption{Ordered pairs; projections; general sums} \label{zf-pair} -\end{figure} - - -\subsection{Ordered pairs} -Figure~\ref{zf-pair} presents the rules governing ordered pairs, -projections and general sums. File \texttt{ZF/pair.ML} contains the -full (and tedious) proof that $\{\{a\},\{a,b\}\}$ functions as an ordered -pair. This property is expressed as two destruction rules, -\tdx{Pair_inject1} and \tdx{Pair_inject2}, and equivalently -as the elimination rule \tdx{Pair_inject}. - -The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$. This -is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other -encodings of ordered pairs. The non-standard ordered pairs mentioned below -satisfy $\pair{\emptyset;\emptyset}=\emptyset$. - -The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE} -assert that \cdx{Sigma}$(A,B)$ consists of all pairs of the form -$\pair{x,y}$, for $x\in A$ and $y\in B(x)$. The rule \tdx{SigmaE2} -merely states that $\pair{a,b}\in \texttt{Sigma}(A,B)$ implies $a\in A$ and -$b\in B(a)$. - -In addition, it is possible to use tuples as patterns in abstractions: -\begin{center} -{\tt\%<$x$,$y$>. $t$} \quad stands for\quad \texttt{split(\%$x$ $y$. $t$)} -\end{center} -Nested patterns are translated recursively: -{\tt\%<$x$,$y$,$z$>. $t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>. $t$} $\leadsto$ -\texttt{split(\%$x$.\%<$y$,$z$>. $t$)} $\leadsto$ \texttt{split(\%$x$. split(\%$y$ - $z$. $t$))}. The reverse translation is performed upon printing. -\begin{warn} - The translation between patterns and \texttt{split} is performed automatically - by the parser and printer. Thus the internal and external form of a term - may differ, which affects proofs. For example the term {\tt - (\%.)} requires the theorem \texttt{split} to rewrite to - {\tt}. -\end{warn} -In addition to explicit $\lambda$-abstractions, patterns can be used in any -variable binding construct which is internally described by a -$\lambda$-abstraction. Some important examples are -\begin{description} -\item[Let:] \texttt{let {\it pattern} = $t$ in $u$} -\item[Choice:] \texttt{THE~{\it pattern}~.~$P$} -\item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$} -\item[Comprehension:] \texttt{{\ttlbrace}~{\it pattern}:$A$~.~$P$~{\ttrbrace}} -\end{description} - - -%%% domrange.ML - -\begin{figure} -\begin{ttbox} -\tdx{domainI} : r ==> a : domain(r) -\tdx{domainE} [| a : domain(r); !!y. : r ==> P |] ==> P -\tdx{domain_subset} domain(Sigma(A,B)) <= A - -\tdx{rangeI} : r ==> b : range(r) -\tdx{rangeE} [| b : range(r); !!x. : r ==> P |] ==> P -\tdx{range_subset} range(A*B) <= B - -\tdx{fieldI1} : r ==> a : field(r) -\tdx{fieldI2} : r ==> b : field(r) -\tdx{fieldCI} (~ :r ==> : r) ==> a : field(r) - -\tdx{fieldE} [| a : field(r); - !!x. : r ==> P; - !!x. : r ==> P - |] ==> P - -\tdx{field_subset} field(A*A) <= A -\end{ttbox} -\caption{Domain, range and field of a relation} \label{zf-domrange} -\end{figure} - -\begin{figure} -\begin{ttbox} -\tdx{imageI} [| : r; a:A |] ==> b : r``A -\tdx{imageE} [| b: r``A; !!x.[| : r; x:A |] ==> P |] ==> P - -\tdx{vimageI} [| : r; b:B |] ==> a : r-``B -\tdx{vimageE} [| a: r-``B; !!x.[| : r; x:B |] ==> P |] ==> P -\end{ttbox} -\caption{Image and inverse image} \label{zf-domrange2} -\end{figure} - - -\subsection{Relations} -Figure~\ref{zf-domrange} presents rules involving relations, which are sets -of ordered pairs. The converse of a relation~$r$ is the set of all pairs -$\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then -{\cdx{converse}$(r)$} is its inverse. The rules for the domain -operation, namely \tdx{domainI} and~\tdx{domainE}, assert that -\cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains -some pair of the form~$\pair{x,y}$. The range operation is similar, and -the field of a relation is merely the union of its domain and range. - -Figure~\ref{zf-domrange2} presents rules for images and inverse images. -Note that these operations are generalisations of range and domain, -respectively. See the file \texttt{ZF/domrange.ML} for derivations of the -rules. - - -%%% func.ML - -\begin{figure} -\begin{ttbox} -\tdx{fun_is_rel} f: Pi(A,B) ==> f <= Sigma(A,B) - -\tdx{apply_equality} [| : f; f: Pi(A,B) |] ==> f`a = b -\tdx{apply_equality2} [| : f; : f; f: Pi(A,B) |] ==> b=c - -\tdx{apply_type} [| f: Pi(A,B); a:A |] ==> f`a : B(a) -\tdx{apply_Pair} [| f: Pi(A,B); a:A |] ==> : f -\tdx{apply_iff} f: Pi(A,B) ==> : f <-> a:A & f`a = b - -\tdx{fun_extension} [| f : Pi(A,B); g: Pi(A,D); - !!x. x:A ==> f`x = g`x |] ==> f=g - -\tdx{domain_type} [| : f; f: Pi(A,B) |] ==> a : A -\tdx{range_type} [| : f; f: Pi(A,B) |] ==> b : B(a) - -\tdx{Pi_type} [| f: A->C; !!x. x:A ==> f`x: B(x) |] ==> f: Pi(A,B) -\tdx{domain_of_fun} f: Pi(A,B) ==> domain(f)=A -\tdx{range_of_fun} f: Pi(A,B) ==> f: A->range(f) - -\tdx{restrict} a : A ==> restrict(f,A) ` a = f`a -\tdx{restrict_type} [| !!x. x:A ==> f`x: B(x) |] ==> - restrict(f,A) : Pi(A,B) -\end{ttbox} -\caption{Functions} \label{zf-func1} -\end{figure} - - -\begin{figure} -\begin{ttbox} -\tdx{lamI} a:A ==> : (lam x:A. b(x)) -\tdx{lamE} [| p: (lam x:A. b(x)); !!x.[| x:A; p= |] ==> P - |] ==> P - -\tdx{lam_type} [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B) - -\tdx{beta} a : A ==> (lam x:A. b(x)) ` a = b(a) -\tdx{eta} f : Pi(A,B) ==> (lam x:A. f`x) = f -\end{ttbox} -\caption{$\lambda$-abstraction} \label{zf-lam} -\end{figure} - - -\begin{figure} -\begin{ttbox} -\tdx{fun_empty} 0: 0->0 -\tdx{fun_single} {\ttlbrace}{\ttrbrace} : {\ttlbrace}a{\ttrbrace} -> {\ttlbrace}b{\ttrbrace} - -\tdx{fun_disjoint_Un} [| f: A->B; g: C->D; A Int C = 0 |] ==> - (f Un g) : (A Un C) -> (B Un D) - -\tdx{fun_disjoint_apply1} [| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> - (f Un g)`a = f`a - -\tdx{fun_disjoint_apply2} [| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> - (f Un g)`c = g`c -\end{ttbox} -\caption{Constructing functions from smaller sets} \label{zf-func2} -\end{figure} - - -\subsection{Functions} -Functions, represented by graphs, are notoriously difficult to reason -about. The file \texttt{ZF/func.ML} derives many rules, which overlap more -than they ought. This section presents the more important rules. - -Figure~\ref{zf-func1} presents the basic properties of \cdx{Pi}$(A,B)$, -the generalized function space. For example, if $f$ is a function and -$\pair{a,b}\in f$, then $f`a=b$ (\tdx{apply_equality}). Two functions -are equal provided they have equal domains and deliver equals results -(\tdx{fun_extension}). - -By \tdx{Pi_type}, a function typing of the form $f\in A\to C$ can be -refined to the dependent typing $f\in\prod@{x\in A}B(x)$, given a suitable -family of sets $\{B(x)\}@{x\in A}$. Conversely, by \tdx{range_of_fun}, -any dependent typing can be flattened to yield a function type of the form -$A\to C$; here, $C={\tt range}(f)$. - -Among the laws for $\lambda$-abstraction, \tdx{lamI} and \tdx{lamE} -describe the graph of the generated function, while \tdx{beta} and -\tdx{eta} are the standard conversions. We essentially have a -dependently-typed $\lambda$-calculus (Fig.\ts\ref{zf-lam}). - -Figure~\ref{zf-func2} presents some rules that can be used to construct -functions explicitly. We start with functions consisting of at most one -pair, and may form the union of two functions provided their domains are -disjoint. - - -\begin{figure} -\begin{ttbox} -\tdx{Int_absorb} A Int A = A -\tdx{Int_commute} A Int B = B Int A -\tdx{Int_assoc} (A Int B) Int C = A Int (B Int C) -\tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) - -\tdx{Un_absorb} A Un A = A -\tdx{Un_commute} A Un B = B Un A -\tdx{Un_assoc} (A Un B) Un C = A Un (B Un C) -\tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) - -\tdx{Diff_cancel} A-A = 0 -\tdx{Diff_disjoint} A Int (B-A) = 0 -\tdx{Diff_partition} A<=B ==> A Un (B-A) = B -\tdx{double_complement} [| A<=B; B<= C |] ==> (B - (C-A)) = A -\tdx{Diff_Un} A - (B Un C) = (A-B) Int (A-C) -\tdx{Diff_Int} A - (B Int C) = (A-B) Un (A-C) - -\tdx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B) -\tdx{Inter_Un_distrib} [| a:A; b:B |] ==> - Inter(A Un B) = Inter(A) Int Inter(B) - -\tdx{Int_Union_RepFun} A Int Union(B) = (UN C:B. A Int C) - -\tdx{Un_Inter_RepFun} b:B ==> - A Un Inter(B) = (INT C:B. A Un C) - -\tdx{SUM_Un_distrib1} (SUM x:A Un B. C(x)) = - (SUM x:A. C(x)) Un (SUM x:B. C(x)) - -\tdx{SUM_Un_distrib2} (SUM x:C. A(x) Un B(x)) = - (SUM x:C. A(x)) Un (SUM x:C. B(x)) - -\tdx{SUM_Int_distrib1} (SUM x:A Int B. C(x)) = - (SUM x:A. C(x)) Int (SUM x:B. C(x)) - -\tdx{SUM_Int_distrib2} (SUM x:C. A(x) Int B(x)) = - (SUM x:C. A(x)) Int (SUM x:C. B(x)) -\end{ttbox} -\caption{Equalities} \label{zf-equalities} -\end{figure} - - -\begin{figure} -%\begin{constants} -% \cdx{1} & $i$ & & $\{\emptyset\}$ \\ -% \cdx{bool} & $i$ & & the set $\{\emptyset,1\}$ \\ -% \cdx{cond} & $[i,i,i]\To i$ & & conditional for \texttt{bool} \\ -% \cdx{not} & $i\To i$ & & negation for \texttt{bool} \\ -% \sdx{and} & $[i,i]\To i$ & Left 70 & conjunction for \texttt{bool} \\ -% \sdx{or} & $[i,i]\To i$ & Left 65 & disjunction for \texttt{bool} \\ -% \sdx{xor} & $[i,i]\To i$ & Left 65 & exclusive-or for \texttt{bool} -%\end{constants} -% -\begin{ttbox} -\tdx{bool_def} bool == {\ttlbrace}0,1{\ttrbrace} -\tdx{cond_def} cond(b,c,d) == if(b=1,c,d) -\tdx{not_def} not(b) == cond(b,0,1) -\tdx{and_def} a and b == cond(a,b,0) -\tdx{or_def} a or b == cond(a,1,b) -\tdx{xor_def} a xor b == cond(a,not(b),b) - -\tdx{bool_1I} 1 : bool -\tdx{bool_0I} 0 : bool -\tdx{boolE} [| c: bool; c=1 ==> P; c=0 ==> P |] ==> P -\tdx{cond_1} cond(1,c,d) = c -\tdx{cond_0} cond(0,c,d) = d -\end{ttbox} -\caption{The booleans} \label{zf-bool} -\end{figure} - - -\section{Further developments} -The next group of developments is complex and extensive, and only -highlights can be covered here. It involves many theories and ML files of -proofs. - -Figure~\ref{zf-equalities} presents commutative, associative, distributive, -and idempotency laws of union and intersection, along with other equations. -See file \texttt{ZF/equalities.ML}. - -Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual -operators including a conditional (Fig.\ts\ref{zf-bool}). Although {\ZF} is a -first-order theory, you can obtain the effect of higher-order logic using -\texttt{bool}-valued functions, for example. The constant~\texttt{1} is -translated to \texttt{succ(0)}. - -\begin{figure} -\index{*"+ symbol} -\begin{constants} - \it symbol & \it meta-type & \it priority & \it description \\ - \tt + & $[i,i]\To i$ & Right 65 & disjoint union operator\\ - \cdx{Inl}~~\cdx{Inr} & $i\To i$ & & injections\\ - \cdx{case} & $[i\To i,i\To i, i]\To i$ & & conditional for $A+B$ -\end{constants} -\begin{ttbox} -\tdx{sum_def} A+B == {\ttlbrace}0{\ttrbrace}*A Un {\ttlbrace}1{\ttrbrace}*B -\tdx{Inl_def} Inl(a) == <0,a> -\tdx{Inr_def} Inr(b) == <1,b> -\tdx{case_def} case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u) - -\tdx{sum_InlI} a : A ==> Inl(a) : A+B -\tdx{sum_InrI} b : B ==> Inr(b) : A+B - -\tdx{Inl_inject} Inl(a)=Inl(b) ==> a=b -\tdx{Inr_inject} Inr(a)=Inr(b) ==> a=b -\tdx{Inl_neq_Inr} Inl(a)=Inr(b) ==> P - -\tdx{sumE2} u: A+B ==> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y)) - -\tdx{case_Inl} case(c,d,Inl(a)) = c(a) -\tdx{case_Inr} case(c,d,Inr(b)) = d(b) -\end{ttbox} -\caption{Disjoint unions} \label{zf-sum} -\end{figure} - - -Theory \thydx{Sum} defines the disjoint union of two sets, with -injections and a case analysis operator (Fig.\ts\ref{zf-sum}). Disjoint -unions play a role in datatype definitions, particularly when there is -mutual recursion~\cite{paulson-set-II}. - -\begin{figure} -\begin{ttbox} -\tdx{QPair_def} == a+b -\tdx{qsplit_def} qsplit(c,p) == THE y. EX a b. p= & y=c(a,b) -\tdx{qfsplit_def} qfsplit(R,z) == EX x y. z= & R(x,y) -\tdx{qconverse_def} qconverse(r) == {\ttlbrace}z. w:r, EX x y. w= & z={\ttrbrace} -\tdx{QSigma_def} QSigma(A,B) == UN x:A. UN y:B(x). {\ttlbrace}{\ttrbrace} - -\tdx{qsum_def} A <+> B == ({\ttlbrace}0{\ttrbrace} <*> A) Un ({\ttlbrace}1{\ttrbrace} <*> B) -\tdx{QInl_def} QInl(a) == <0;a> -\tdx{QInr_def} QInr(b) == <1;b> -\tdx{qcase_def} qcase(c,d) == qsplit(\%y z. cond(y, d(z), c(z))) -\end{ttbox} -\caption{Non-standard pairs, products and sums} \label{zf-qpair} -\end{figure} - -Theory \thydx{QPair} defines a notion of ordered pair that admits -non-well-founded tupling (Fig.\ts\ref{zf-qpair}). Such pairs are written -{\tt<$a$;$b$>}. It also defines the eliminator \cdx{qsplit}, the -converse operator \cdx{qconverse}, and the summation operator -\cdx{QSigma}. These are completely analogous to the corresponding -versions for standard ordered pairs. The theory goes on to define a -non-standard notion of disjoint sum using non-standard pairs. All of these -concepts satisfy the same properties as their standard counterparts; in -addition, {\tt<$a$;$b$>} is continuous. The theory supports coinductive -definitions, for example of infinite lists~\cite{paulson-final}. - -\begin{figure} -\begin{ttbox} -\tdx{bnd_mono_def} bnd_mono(D,h) == - h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X)) - -\tdx{lfp_def} lfp(D,h) == Inter({\ttlbrace}X: Pow(D). h(X) <= X{\ttrbrace}) -\tdx{gfp_def} gfp(D,h) == Union({\ttlbrace}X: Pow(D). X <= h(X){\ttrbrace}) - - -\tdx{lfp_lowerbound} [| h(A) <= A; A<=D |] ==> lfp(D,h) <= A - -\tdx{lfp_subset} lfp(D,h) <= D - -\tdx{lfp_greatest} [| bnd_mono(D,h); - !!X. [| h(X) <= X; X<=D |] ==> A<=X - |] ==> A <= lfp(D,h) - -\tdx{lfp_Tarski} bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h)) - -\tdx{induct} [| a : lfp(D,h); bnd_mono(D,h); - !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) - |] ==> P(a) - -\tdx{lfp_mono} [| bnd_mono(D,h); bnd_mono(E,i); - !!X. X<=D ==> h(X) <= i(X) - |] ==> lfp(D,h) <= lfp(E,i) - -\tdx{gfp_upperbound} [| A <= h(A); A<=D |] ==> A <= gfp(D,h) - -\tdx{gfp_subset} gfp(D,h) <= D - -\tdx{gfp_least} [| bnd_mono(D,h); - !!X. [| X <= h(X); X<=D |] ==> X<=A - |] ==> gfp(D,h) <= A - -\tdx{gfp_Tarski} bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h)) - -\tdx{coinduct} [| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D - |] ==> a : gfp(D,h) - -\tdx{gfp_mono} [| bnd_mono(D,h); D <= E; - !!X. X<=D ==> h(X) <= i(X) - |] ==> gfp(D,h) <= gfp(E,i) -\end{ttbox} -\caption{Least and greatest fixedpoints} \label{zf-fixedpt} -\end{figure} - -The Knaster-Tarski Theorem states that every monotone function over a -complete lattice has a fixedpoint. Theory \thydx{Fixedpt} proves the -Theorem only for a particular lattice, namely the lattice of subsets of a -set (Fig.\ts\ref{zf-fixedpt}). The theory defines least and greatest -fixedpoint operators with corresponding induction and coinduction rules. -These are essential to many definitions that follow, including the natural -numbers and the transitive closure operator. The (co)inductive definition -package also uses the fixedpoint operators~\cite{paulson-CADE}. See -Davey and Priestley~\cite{davey&priestley} for more on the Knaster-Tarski -Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle -proofs. - -Monotonicity properties are proved for most of the set-forming operations: -union, intersection, Cartesian product, image, domain, range, etc. These -are useful for applying the Knaster-Tarski Fixedpoint Theorem. The proofs -themselves are trivial applications of Isabelle's classical reasoner. See -file \texttt{ZF/mono.ML}. - - -\begin{figure} -\begin{constants} - \it symbol & \it meta-type & \it priority & \it description \\ - \sdx{O} & $[i,i]\To i$ & Right 60 & composition ($\circ$) \\ - \cdx{id} & $i\To i$ & & identity function \\ - \cdx{inj} & $[i,i]\To i$ & & injective function space\\ - \cdx{surj} & $[i,i]\To i$ & & surjective function space\\ - \cdx{bij} & $[i,i]\To i$ & & bijective function space -\end{constants} - -\begin{ttbox} -\tdx{comp_def} r O s == {\ttlbrace}xz : domain(s)*range(r) . - EX x y z. xz= & :s & :r{\ttrbrace} -\tdx{id_def} id(A) == (lam x:A. x) -\tdx{inj_def} inj(A,B) == {\ttlbrace} f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x {\ttrbrace} -\tdx{surj_def} surj(A,B) == {\ttlbrace} f: A->B . ALL y:B. EX x:A. f`x=y {\ttrbrace} -\tdx{bij_def} bij(A,B) == inj(A,B) Int surj(A,B) - - -\tdx{left_inverse} [| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a -\tdx{right_inverse} [| f: inj(A,B); b: range(f) |] ==> - f`(converse(f)`b) = b - -\tdx{inj_converse_inj} f: inj(A,B) ==> converse(f): inj(range(f), A) -\tdx{bij_converse_bij} f: bij(A,B) ==> converse(f): bij(B,A) - -\tdx{comp_type} [| s<=A*B; r<=B*C |] ==> (r O s) <= A*C -\tdx{comp_assoc} (r O s) O t = r O (s O t) - -\tdx{left_comp_id} r<=A*B ==> id(B) O r = r -\tdx{right_comp_id} r<=A*B ==> r O id(A) = r - -\tdx{comp_func} [| g:A->B; f:B->C |] ==> (f O g):A->C -\tdx{comp_func_apply} [| g:A->B; f:B->C; a:A |] ==> (f O g)`a = f`(g`a) - -\tdx{comp_inj} [| g:inj(A,B); f:inj(B,C) |] ==> (f O g):inj(A,C) -\tdx{comp_surj} [| g:surj(A,B); f:surj(B,C) |] ==> (f O g):surj(A,C) -\tdx{comp_bij} [| g:bij(A,B); f:bij(B,C) |] ==> (f O g):bij(A,C) - -\tdx{left_comp_inverse} f: inj(A,B) ==> converse(f) O f = id(A) -\tdx{right_comp_inverse} f: surj(A,B) ==> f O converse(f) = id(B) - -\tdx{bij_disjoint_Un} - [| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |] ==> - (f Un g) : bij(A Un C, B Un D) - -\tdx{restrict_bij} [| f:inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C) -\end{ttbox} -\caption{Permutations} \label{zf-perm} -\end{figure} - -The theory \thydx{Perm} is concerned with permutations (bijections) and -related concepts. These include composition of relations, the identity -relation, and three specialized function spaces: injective, surjective and -bijective. Figure~\ref{zf-perm} displays many of their properties that -have been proved. These results are fundamental to a treatment of -equipollence and cardinality. - -\begin{figure}\small -\index{#*@{\tt\#*} symbol} -\index{*div symbol} -\index{*mod symbol} -\index{#+@{\tt\#+} symbol} -\index{#-@{\tt\#-} symbol} -\begin{constants} - \it symbol & \it meta-type & \it priority & \it description \\ - \cdx{nat} & $i$ & & set of natural numbers \\ - \cdx{nat_case}& $[i,i\To i,i]\To i$ & & conditional for $nat$\\ - \cdx{rec} & $[i,i,[i,i]\To i]\To i$ & & recursor for $nat$\\ - \tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\ - \tt div & $[i,i]\To i$ & Left 70 & division\\ - \tt mod & $[i,i]\To i$ & Left 70 & modulus\\ - \tt \#+ & $[i,i]\To i$ & Left 65 & addition\\ - \tt \#- & $[i,i]\To i$ & Left 65 & subtraction -\end{constants} - -\begin{ttbox} -\tdx{nat_def} nat == lfp(lam r: Pow(Inf). {\ttlbrace}0{\ttrbrace} Un {\ttlbrace}succ(x). x:r{\ttrbrace} - -\tdx{nat_case_def} nat_case(a,b,k) == - THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x)) - -\tdx{rec_def} rec(k,a,b) == - transrec(k, \%n f. nat_case(a, \%m. b(m, f`m), n)) - -\tdx{add_def} m#+n == rec(m, n, \%u v. succ(v)) -\tdx{diff_def} m#-n == rec(n, m, \%u v. rec(v, 0, \%x y. x)) -\tdx{mult_def} m#*n == rec(m, 0, \%u v. n #+ v) -\tdx{mod_def} m mod n == transrec(m, \%j f. if(j:n, j, f`(j#-n))) -\tdx{div_def} m div n == transrec(m, \%j f. if(j:n, 0, succ(f`(j#-n)))) - - -\tdx{nat_0I} 0 : nat -\tdx{nat_succI} n : nat ==> succ(n) : nat - -\tdx{nat_induct} - [| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) - |] ==> P(n) - -\tdx{nat_case_0} nat_case(a,b,0) = a -\tdx{nat_case_succ} nat_case(a,b,succ(m)) = b(m) - -\tdx{rec_0} rec(0,a,b) = a -\tdx{rec_succ} rec(succ(m),a,b) = b(m, rec(m,a,b)) - -\tdx{mult_type} [| m:nat; n:nat |] ==> m #* n : nat -\tdx{mult_0} 0 #* n = 0 -\tdx{mult_succ} succ(m) #* n = n #+ (m #* n) -\tdx{mult_commute} [| m:nat; n:nat |] ==> m #* n = n #* m -\tdx{add_mult_dist} [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k){\thinspace}#+{\thinspace}(n #* k) -\tdx{mult_assoc} - [| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k) -\tdx{mod_quo_equality} - [| 0:n; m:nat; n:nat |] ==> (m div n)#*n #+ m mod n = m -\end{ttbox} -\caption{The natural numbers} \label{zf-nat} -\end{figure} - -Theory \thydx{Nat} defines the natural numbers and mathematical -induction, along with a case analysis operator. The set of natural -numbers, here called \texttt{nat}, is known in set theory as the ordinal~$\omega$. - -Theory \thydx{Arith} defines primitive recursion and goes on to develop -arithmetic on the natural numbers (Fig.\ts\ref{zf-nat}). It defines -addition, multiplication, subtraction, division, and remainder. Many of -their properties are proved: commutative, associative and distributive -laws, identity and cancellation laws, etc. The most interesting result is -perhaps the theorem $a \bmod b + (a/b)\times b = a$. Division and -remainder are defined by repeated subtraction, which requires well-founded -rather than primitive recursion; the termination argument relies on the -divisor's being non-zero. - -Theory \thydx{Univ} defines a `universe' $\texttt{univ}(A)$, for -constructing datatypes such as trees. This set contains $A$ and the -natural numbers. Vitally, it is closed under finite products: ${\tt - univ}(A)\times{\tt univ}(A)\subseteq{\tt univ}(A)$. This theory also -defines the cumulative hierarchy of axiomatic set theory, which -traditionally is written $V@\alpha$ for an ordinal~$\alpha$. The -`universe' is a simple generalization of~$V@\omega$. - -Theory \thydx{QUniv} defines a `universe' ${\tt quniv}(A)$, for -constructing codatatypes such as streams. It is analogous to ${\tt - univ}(A)$ (and is defined in terms of it) but is closed under the -non-standard product and sum. - -Theory \texttt{Finite} (Figure~\ref{zf-fin}) defines the finite set operator; -${\tt Fin}(A)$ is the set of all finite sets over~$A$. The theory employs -Isabelle's inductive definition package, which proves various rules -automatically. The induction rule shown is stronger than the one proved by -the package. The theory also defines the set of all finite functions -between two given sets. - -\begin{figure} -\begin{ttbox} -\tdx{Fin.emptyI} 0 : Fin(A) -\tdx{Fin.consI} [| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A) - -\tdx{Fin_induct} - [| b: Fin(A); - P(0); - !!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y)) - |] ==> P(b) - -\tdx{Fin_mono} A<=B ==> Fin(A) <= Fin(B) -\tdx{Fin_UnI} [| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A) -\tdx{Fin_UnionI} C : Fin(Fin(A)) ==> Union(C) : Fin(A) -\tdx{Fin_subset} [| c<=b; b: Fin(A) |] ==> c: Fin(A) -\end{ttbox} -\caption{The finite set operator} \label{zf-fin} -\end{figure} - -\begin{figure} -\begin{constants} - \cdx{list} & $i\To i$ && lists over some set\\ - \cdx{list_case} & $[i, [i,i]\To i, i] \To i$ && conditional for $list(A)$ \\ - \cdx{list_rec} & $[i, i, [i,i,i]\To i] \To i$ && recursor for $list(A)$ \\ - \cdx{map} & $[i\To i, i] \To i$ & & mapping functional\\ - \cdx{length} & $i\To i$ & & length of a list\\ - \cdx{rev} & $i\To i$ & & reverse of a list\\ - \tt \at & $[i,i]\To i$ & Right 60 & append for lists\\ - \cdx{flat} & $i\To i$ & & append of list of lists -\end{constants} - -\underscoreon %%because @ is used here -\begin{ttbox} -\tdx{list_rec_def} list_rec(l,c,h) == - Vrec(l, \%l g. list_case(c, \%x xs. h(x, xs, g`xs), l)) - -\tdx{map_def} map(f,l) == list_rec(l, 0, \%x xs r. ) -\tdx{length_def} length(l) == list_rec(l, 0, \%x xs r. succ(r)) -\tdx{app_def} xs@ys == list_rec(xs, ys, \%x xs r. ) -\tdx{rev_def} rev(l) == list_rec(l, 0, \%x xs r. r @ ) -\tdx{flat_def} flat(ls) == list_rec(ls, 0, \%l ls r. l @ r) - - -\tdx{NilI} Nil : list(A) -\tdx{ConsI} [| a: A; l: list(A) |] ==> Cons(a,l) : list(A) - -\tdx{List.induct} - [| l: list(A); - P(Nil); - !!x y. [| x: A; y: list(A); P(y) |] ==> P(Cons(x,y)) - |] ==> P(l) - -\tdx{Cons_iff} Cons(a,l)=Cons(a',l') <-> a=a' & l=l' -\tdx{Nil_Cons_iff} ~ Nil=Cons(a,l) - -\tdx{list_mono} A<=B ==> list(A) <= list(B) - -\tdx{list_rec_Nil} list_rec(Nil,c,h) = c -\tdx{list_rec_Cons} list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h)) - -\tdx{map_ident} l: list(A) ==> map(\%u. u, l) = l -\tdx{map_compose} l: list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l) -\tdx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys) -\tdx{map_type} - [| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B) -\tdx{map_flat} - ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls)) -\end{ttbox} -\caption{Lists} \label{zf-list} -\end{figure} - - -Figure~\ref{zf-list} presents the set of lists over~$A$, ${\tt list}(A)$. -The definition employs Isabelle's datatype package, which defines the -introduction and induction rules automatically, as well as the constructors -and case operator (\verb|list_case|). See file \texttt{ZF/List.ML}. -The file \texttt{ZF/ListFn.thy} proceeds to define structural -recursion and the usual list functions. - -The constructions of the natural numbers and lists make use of a suite of -operators for handling recursive function definitions. I have described -the developments in detail elsewhere~\cite{paulson-set-II}. Here is a brief -summary: -\begin{itemize} - \item Theory \texttt{Trancl} defines the transitive closure of a relation - (as a least fixedpoint). - - \item Theory \texttt{WF} proves the Well-Founded Recursion Theorem, using an - elegant approach of Tobias Nipkow. This theorem permits general - recursive definitions within set theory. - - \item Theory \texttt{Ord} defines the notions of transitive set and ordinal - number. It derives transfinite induction. A key definition is {\bf - less than}: $i Pow(A) <= Pow(B) -\end{ttbox} -We enter the goal and make the first step, which breaks the equation into -two inclusions by extensionality:\index{*equalityI theorem} -\begin{ttbox} -Goal "Pow(A Int B) = Pow(A) Int Pow(B)"; -{\out Level 0} -{\out Pow(A Int B) = Pow(A) Int Pow(B)} -{\out 1. Pow(A Int B) = Pow(A) Int Pow(B)} -\ttbreak -by (resolve_tac [equalityI] 1); -{\out Level 1} -{\out Pow(A Int B) = Pow(A) Int Pow(B)} -{\out 1. Pow(A Int B) <= Pow(A) Int Pow(B)} -{\out 2. Pow(A) Int Pow(B) <= Pow(A Int B)} -\end{ttbox} -Both inclusions could be tackled straightforwardly using \texttt{subsetI}. -A shorter proof results from noting that intersection forms the greatest -lower bound:\index{*Int_greatest theorem} -\begin{ttbox} -by (resolve_tac [Int_greatest] 1); -{\out Level 2} -{\out Pow(A Int B) = Pow(A) Int Pow(B)} -{\out 1. Pow(A Int B) <= Pow(A)} -{\out 2. Pow(A Int B) <= Pow(B)} -{\out 3. Pow(A) Int Pow(B) <= Pow(A Int B)} -\end{ttbox} -Subgoal~1 follows by applying the monotonicity of \texttt{Pow} to $A\int -B\subseteq A$; subgoal~2 follows similarly: -\index{*Int_lower1 theorem}\index{*Int_lower2 theorem} -\begin{ttbox} -by (resolve_tac [Int_lower1 RS Pow_mono] 1); -{\out Level 3} -{\out Pow(A Int B) = Pow(A) Int Pow(B)} -{\out 1. Pow(A Int B) <= Pow(B)} -{\out 2. Pow(A) Int Pow(B) <= Pow(A Int B)} -\ttbreak -by (resolve_tac [Int_lower2 RS Pow_mono] 1); -{\out Level 4} -{\out Pow(A Int B) = Pow(A) Int Pow(B)} -{\out 1. Pow(A) Int Pow(B) <= Pow(A Int B)} -\end{ttbox} -We are left with the opposite inclusion, which we tackle in the -straightforward way:\index{*subsetI theorem} -\begin{ttbox} -by (resolve_tac [subsetI] 1); -{\out Level 5} -{\out Pow(A Int B) = Pow(A) Int Pow(B)} -{\out 1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)} -\end{ttbox} -The subgoal is to show $x\in {\tt Pow}(A\cap B)$ assuming $x\in{\tt -Pow}(A)\cap {\tt Pow}(B)$; eliminating this assumption produces two -subgoals. The rule \tdx{IntE} treats the intersection like a conjunction -instead of unfolding its definition. -\begin{ttbox} -by (eresolve_tac [IntE] 1); -{\out Level 6} -{\out Pow(A Int B) = Pow(A) Int Pow(B)} -{\out 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)} -\end{ttbox} -The next step replaces the \texttt{Pow} by the subset -relation~($\subseteq$).\index{*PowI theorem} -\begin{ttbox} -by (resolve_tac [PowI] 1); -{\out Level 7} -{\out Pow(A Int B) = Pow(A) Int Pow(B)} -{\out 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B} -\end{ttbox} -We perform the same replacement in the assumptions. This is a good -demonstration of the tactic \ttindex{dresolve_tac}:\index{*PowD theorem} -\begin{ttbox} -by (REPEAT (dresolve_tac [PowD] 1)); -{\out Level 8} -{\out Pow(A Int B) = Pow(A) Int Pow(B)} -{\out 1. !!x. [| x <= A; x <= B |] ==> x <= A Int B} -\end{ttbox} -The assumptions are that $x$ is a lower bound of both $A$ and~$B$, but -$A\int B$ is the greatest lower bound:\index{*Int_greatest theorem} -\begin{ttbox} -by (resolve_tac [Int_greatest] 1); -{\out Level 9} -{\out Pow(A Int B) = Pow(A) Int Pow(B)} -{\out 1. !!x. [| x <= A; x <= B |] ==> x <= A} -{\out 2. !!x. [| x <= A; x <= B |] ==> x <= B} -\end{ttbox} -To conclude the proof, we clear up the trivial subgoals: -\begin{ttbox} -by (REPEAT (assume_tac 1)); -{\out Level 10} -{\out Pow(A Int B) = Pow(A) Int Pow(B)} -{\out No subgoals!} -\end{ttbox} -\medskip -We could have performed this proof in one step by applying -\ttindex{Blast_tac}. Let us -go back to the start: -\begin{ttbox} -choplev 0; -{\out Level 0} -{\out Pow(A Int B) = Pow(A) Int Pow(B)} -{\out 1. Pow(A Int B) = Pow(A) Int Pow(B)} -by (Blast_tac 1); -{\out Depth = 0} -{\out Depth = 1} -{\out Depth = 2} -{\out Depth = 3} -{\out Level 1} -{\out Pow(A Int B) = Pow(A) Int Pow(B)} -{\out No subgoals!} -\end{ttbox} -Past researchers regarded this as a difficult proof, as indeed it is if all -the symbols are replaced by their definitions. -\goodbreak - -\section{Monotonicity of the union operator} -For another example, we prove that general union is monotonic: -${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$. To begin, we -tackle the inclusion using \tdx{subsetI}: -\begin{ttbox} -Goal "C<=D ==> Union(C) <= Union(D)"; -{\out Level 0} -{\out C <= D ==> Union(C) <= Union(D)} -{\out 1. C <= D ==> Union(C) <= Union(D)} -\ttbreak -by (resolve_tac [subsetI] 1); -{\out Level 1} -{\out C <= D ==> Union(C) <= Union(D)} -{\out 1. !!x. [| C <= D; x : Union(C) |] ==> x : Union(D)} -\end{ttbox} -Big union is like an existential quantifier --- the occurrence in the -assumptions must be eliminated early, since it creates parameters. -\index{*UnionE theorem} -\begin{ttbox} -by (eresolve_tac [UnionE] 1); -{\out Level 2} -{\out C <= D ==> Union(C) <= Union(D)} -{\out 1. !!x B. [| C <= D; x : B; B : C |] ==> x : Union(D)} -\end{ttbox} -Now we may apply \tdx{UnionI}, which creates an unknown involving the -parameters. To show $x\in \bigcup(D)$ it suffices to show that $x$ belongs -to some element, say~$\Var{B2}(x,B)$, of~$D$. -\begin{ttbox} -by (resolve_tac [UnionI] 1); -{\out Level 3} -{\out C <= D ==> Union(C) <= Union(D)} -{\out 1. !!x B. [| C <= D; x : B; B : C |] ==> ?B2(x,B) : D} -{\out 2. !!x B. [| C <= D; x : B; B : C |] ==> x : ?B2(x,B)} -\end{ttbox} -Combining \tdx{subsetD} with the assumption $C\subseteq D$ yields -$\Var{a}\in C \Imp \Var{a}\in D$, which reduces subgoal~1. Note that -\texttt{eresolve_tac} has removed that assumption. -\begin{ttbox} -by (eresolve_tac [subsetD] 1); -{\out Level 4} -{\out C <= D ==> Union(C) <= Union(D)} -{\out 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C} -{\out 2. !!x B. [| C <= D; x : B; B : C |] ==> x : ?B2(x,B)} -\end{ttbox} -The rest is routine. Observe how~$\Var{B2}(x,B)$ is instantiated. -\begin{ttbox} -by (assume_tac 1); -{\out Level 5} -{\out C <= D ==> Union(C) <= Union(D)} -{\out 1. !!x B. [| C <= D; x : B; B : C |] ==> x : B} -by (assume_tac 1); -{\out Level 6} -{\out C <= D ==> Union(C) <= Union(D)} -{\out No subgoals!} -\end{ttbox} -Again, \ttindex{Blast_tac} can prove the theorem in one step. -\begin{ttbox} -by (Blast_tac 1); -{\out Depth = 0} -{\out Depth = 1} -{\out Depth = 2} -{\out Level 1} -{\out C <= D ==> Union(C) <= Union(D)} -{\out No subgoals!} -\end{ttbox} - -The file \texttt{ZF/equalities.ML} has many similar proofs. Reasoning about -general intersection can be difficult because of its anomalous behaviour on -the empty set. However, \ttindex{Blast_tac} copes well with these. Here is -a typical example, borrowed from Devlin~\cite[page 12]{devlin79}: -\begin{ttbox} -a:C ==> (INT x:C. A(x) Int B(x)) = (INT x:C. A(x)) Int (INT x:C. B(x)) -\end{ttbox} -In traditional notation this is -\[ a\in C \,\Imp\, \inter@{x\in C} \Bigl(A(x) \int B(x)\Bigr) = - \Bigl(\inter@{x\in C} A(x)\Bigr) \int - \Bigl(\inter@{x\in C} B(x)\Bigr) \] - -\section{Low-level reasoning about functions} -The derived rules \texttt{lamI}, \texttt{lamE}, \texttt{lam_type}, \texttt{beta} -and \texttt{eta} support reasoning about functions in a -$\lambda$-calculus style. This is generally easier than regarding -functions as sets of ordered pairs. But sometimes we must look at the -underlying representation, as in the following proof -of~\tdx{fun_disjoint_apply1}. This states that if $f$ and~$g$ are -functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then -$(f\un g)`a = f`a$: -\begin{ttbox} -Goal "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ttback -\ttback (f Un g)`a = f`a"; -{\out Level 0} -{\out [| a : A; f : A -> B; g : C -> D; A Int C = 0 |]} -{\out ==> (f Un g) ` a = f ` a} -{\out 1. [| a : A; f : A -> B; g : C -> D; A Int C = 0 |]} -{\out ==> (f Un g) ` a = f ` a} -\end{ttbox} -Using \tdx{apply_equality}, we reduce the equality to reasoning about -ordered pairs. The second subgoal is to verify that $f\un g$ is a function. -To save space, the assumptions will be abbreviated below. -\begin{ttbox} -by (resolve_tac [apply_equality] 1); -{\out Level 1} -{\out [| \ldots |] ==> (f Un g) ` a = f ` a} -{\out 1. [| \ldots |] ==> : f Un g} -{\out 2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} -\end{ttbox} -We must show that the pair belongs to~$f$ or~$g$; by~\tdx{UnI1} we -choose~$f$: -\begin{ttbox} -by (resolve_tac [UnI1] 1); -{\out Level 2} -{\out [| \ldots |] ==> (f Un g) ` a = f ` a} -{\out 1. [| \ldots |] ==> : f} -{\out 2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} -\end{ttbox} -To show $\pair{a,f`a}\in f$ we use \tdx{apply_Pair}, which is -essentially the converse of \tdx{apply_equality}: -\begin{ttbox} -by (resolve_tac [apply_Pair] 1); -{\out Level 3} -{\out [| \ldots |] ==> (f Un g) ` a = f ` a} -{\out 1. [| \ldots |] ==> f : (PROD x:?A2. ?B2(x))} -{\out 2. [| \ldots |] ==> a : ?A2} -{\out 3. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} -\end{ttbox} -Using the assumptions $f\in A\to B$ and $a\in A$, we solve the two subgoals -from \tdx{apply_Pair}. Recall that a $\Pi$-set is merely a generalized -function space, and observe that~{\tt?A2} is instantiated to~\texttt{A}. -\begin{ttbox} -by (assume_tac 1); -{\out Level 4} -{\out [| \ldots |] ==> (f Un g) ` a = f ` a} -{\out 1. [| \ldots |] ==> a : A} -{\out 2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} -by (assume_tac 1); -{\out Level 5} -{\out [| \ldots |] ==> (f Un g) ` a = f ` a} -{\out 1. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} -\end{ttbox} -To construct functions of the form $f\un g$, we apply -\tdx{fun_disjoint_Un}: -\begin{ttbox} -by (resolve_tac [fun_disjoint_Un] 1); -{\out Level 6} -{\out [| \ldots |] ==> (f Un g) ` a = f ` a} -{\out 1. [| \ldots |] ==> f : ?A3 -> ?B3} -{\out 2. [| \ldots |] ==> g : ?C3 -> ?D3} -{\out 3. [| \ldots |] ==> ?A3 Int ?C3 = 0} -\end{ttbox} -The remaining subgoals are instances of the assumptions. Again, observe how -unknowns are instantiated: -\begin{ttbox} -by (assume_tac 1); -{\out Level 7} -{\out [| \ldots |] ==> (f Un g) ` a = f ` a} -{\out 1. [| \ldots |] ==> g : ?C3 -> ?D3} -{\out 2. [| \ldots |] ==> A Int ?C3 = 0} -by (assume_tac 1); -{\out Level 8} -{\out [| \ldots |] ==> (f Un g) ` a = f ` a} -{\out 1. [| \ldots |] ==> A Int C = 0} -by (assume_tac 1); -{\out Level 9} -{\out [| \ldots |] ==> (f Un g) ` a = f ` a} -{\out No subgoals!} -\end{ttbox} -See the files \texttt{ZF/func.ML} and \texttt{ZF/WF.ML} for more -examples of reasoning about functions. - -\index{set theory|)} diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/intro.tex --- a/doc-src/Logics/intro.tex Fri Jan 08 13:20:59 1999 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,150 +0,0 @@ -%% $Id$ -\chapter{Basic Concepts} -Several logics come with Isabelle. Many of them are sufficiently developed -to serve as comfortable reasoning environments. They are also good -starting points for defining new logics. Each logic is distributed with -sample proofs, some of which are described in this document. - -\begin{ttdescription} -\item[\thydx{FOL}] is many-sorted first-order logic with natural -deduction. It comes in both constructive and classical versions. - -\item[\thydx{ZF}] is axiomatic set theory, using the Zermelo-Fraenkel -axioms~\cite{suppes72}. It is built upon classical~\FOL{}. - -\item[\thydx{CCL}] is Martin Coen's Classical Computational Logic, - which is the basis of a preliminary method for deriving programs from - proofs~\cite{coen92}. It is built upon classical~\FOL{}. - -\item[\thydx{LCF}] is a version of Scott's Logic for Computable - Functions, which is also implemented by the~{\sc lcf} - system~\cite{paulson87}. It is built upon classical~\FOL{}. - -\item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40}, -which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}. -This object-logic should not be confused with Isabelle's meta-logic, which is -also a form of higher-order logic. - -\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an - extension of {\tt HOL}\@. - -\item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type -Theory~\cite{nordstrom90}, with extensional equality. Universes are not -included. - -\item[\thydx{LK}] is another version of first-order logic, a classical -sequent calculus. Sequents have the form $A@1,\ldots,A@m\turn -B@1,\ldots,B@n$; rules are applied using associative matching. - -\item[\thydx{Modal}] implements the modal logics $T$, $S4$, - and~$S43$. It is built upon~\LK{}. - -\item[\thydx{Cube}] is Barendregt's $\lambda$-cube. -\end{ttdescription} -The logics {\tt CCL}, {\tt LCF}, {\tt HOLCF}, {\tt Modal} and {\tt - Cube} are currently undocumented. All object-logics' sources are -distributed with Isabelle (see the directory \texttt{src}). They are -also available for browsing on the WWW at: -\begin{ttbox} -http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/ -\end{ttbox} -Note that this is not necessarily consistent with your local sources! - -\medskip You should not read this manual before reading {\em - Introduction to Isabelle\/} and performing some Isabelle proofs. -Consult the {\em Reference Manual} for more information on tactics, -packages, etc. - - -\section{Syntax definitions} -The syntax of each logic is presented using a context-free grammar. -These grammars obey the following conventions: -\begin{itemize} -\item identifiers denote nonterminal symbols -\item {\tt typewriter} font denotes terminal symbols -\item parentheses $(\ldots)$ express grouping -\item constructs followed by a Kleene star, such as $id^*$ and $(\ldots)^*$ -can be repeated~0 or more times -\item alternatives are separated by a vertical bar,~$|$ -\item the symbol for alphanumeric identifiers is~{\it id\/} -\item the symbol for scheme variables is~{\it var} -\end{itemize} -To reduce the number of nonterminals and grammar rules required, Isabelle's -syntax module employs {\bf priorities},\index{priorities} or precedences. -Each grammar rule is given by a mixfix declaration, which has a priority, -and each argument place has a priority. This general approach handles -infix operators that associate either to the left or to the right, as well -as prefix and binding operators. - -In a syntactically valid expression, an operator's arguments never involve -an operator of lower priority unless brackets are used. Consider -first-order logic, where $\exists$ has lower priority than $\disj$, -which has lower priority than $\conj$. There, $P\conj Q \disj R$ -abbreviates $(P\conj Q) \disj R$ rather than $P\conj (Q\disj R)$. Also, -$\exists x.P\disj Q$ abbreviates $\exists x.(P\disj Q)$ rather than -$(\exists x.P)\disj Q$. Note especially that $P\disj(\exists x.Q)$ -becomes syntactically invalid if the brackets are removed. - -A {\bf binder} is a symbol associated with a constant of type -$(\sigma\To\tau)\To\tau'$. For instance, we may declare~$\forall$ as -a binder for the constant~$All$, which has type $(\alpha\To o)\To o$. -This defines the syntax $\forall x.t$ to mean $All(\lambda x.t)$. We -can also write $\forall x@1\ldots x@m.t$ to abbreviate $\forall x@1. -\ldots \forall x@m.t$; this is possible for any constant provided that -$\tau$ and $\tau'$ are the same type. \HOL's description operator -$\varepsilon x.P\,x$ has type $(\alpha\To bool)\To\alpha$ and can bind -only one variable, except when $\alpha$ is $bool$. \ZF's bounded -quantifier $\forall x\in A.P(x)$ cannot be declared as a binder -because it has type $[i, i\To o]\To o$. The syntax for binders allows -type constraints on bound variables, as in -\[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \] - -To avoid excess detail, the logic descriptions adopt a semi-formal style. -Infix operators and binding operators are listed in separate tables, which -include their priorities. Grammar descriptions do not include numeric -priorities; instead, the rules appear in order of decreasing priority. -This should suffice for most purposes; for full details, please consult the -actual syntax definitions in the {\tt.thy} files. - -Each nonterminal symbol is associated with some Isabelle type. For -example, the formulae of first-order logic have type~$o$. Every -Isabelle expression of type~$o$ is therefore a formula. These include -atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more -generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have -suitable types. Therefore, `expression of type~$o$' is listed as a -separate possibility in the grammar for formulae. - - -\section{Proof procedures}\label{sec:safe} -Most object-logics come with simple proof procedures. These are reasonably -powerful for interactive use, though often simplistic and incomplete. You -can do single-step proofs using \verb|resolve_tac| and -\verb|assume_tac|, referring to the inference rules of the logic by {\sc -ml} identifiers. - -For theorem proving, rules can be classified as {\bf safe} or {\bf unsafe}. -A rule is safe if applying it to a provable goal always yields provable -subgoals. If a rule is safe then it can be applied automatically to a goal -without destroying our chances of finding a proof. For instance, all the -rules of the classical sequent calculus {\sc lk} are safe. Universal -elimination is unsafe if the formula $\all{x}P(x)$ is deleted after use. -Other unsafe rules include the following: -\[ \infer[({\disj}I1)]{P\disj Q}{P} \qquad - \infer[({\imp}E)]{Q}{P\imp Q & P} \qquad - \infer[({\exists}I)]{\exists x.P}{P[t/x]} -\] - -Proof procedures use safe rules whenever possible, delaying the application -of unsafe rules. Those safe rules are preferred that generate the fewest -subgoals. Safe rules are (by definition) deterministic, while the unsafe -rules require search. The design of a suitable set of rules can be as -important as the strategy for applying them. - -Many of the proof procedures use backtracking. Typically they attempt to -solve subgoal~$i$ by repeatedly applying a certain tactic to it. This -tactic, which is known as a {\bf step tactic}, resolves a selection of -rules with subgoal~$i$. This may replace one subgoal by many; the -search persists until there are fewer subgoals in total than at the start. -Backtracking happens when the search reaches a dead end: when the step -tactic fails. Alternative outcomes are then searched by a depth-first or -best-first strategy. diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/logics.bbl --- a/doc-src/Logics/logics.bbl Fri Jan 08 13:20:59 1999 +0100 +++ b/doc-src/Logics/logics.bbl Fri Jan 08 14:02:04 1999 +0100 @@ -1,36 +1,11 @@ \begin{thebibliography}{10} -\bibitem{abrial93} -J.~R. Abrial and G.~Laffitte. -\newblock Towards the mechanization of the proofs of some classical theorems of - set theory. -\newblock preprint, February 1993. - \bibitem{andrews86} Peter~B. Andrews. \newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof}. \newblock Academic Press, 1986. -\bibitem{basin91} -David Basin and Matt Kaufmann. -\newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison. -\newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical - Frameworks}, pages 89--119. Cambridge University Press, 1991. - -\bibitem{boyer86} -Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and - Lawrence Wos. -\newblock Set theory in first-order logic: Clauses for {G\"{o}del's} axioms. -\newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986. - -\bibitem{camilleri92} -J.~Camilleri and T.~F. Melham. -\newblock Reasoning with inductively defined relations in the {HOL} theorem - prover. -\newblock Technical Report 265, Computer Laboratory, University of Cambridge, - August 1992. - \bibitem{church40} Alonzo Church. \newblock A formulation of the simple theory of types. @@ -48,26 +23,6 @@ System}. \newblock Prentice-Hall, 1986. -\bibitem{davey&priestley} -B.~A. Davey and H.~A. Priestley. -\newblock {\em Introduction to Lattices and Order}. -\newblock Cambridge University Press, 1990. - -\bibitem{devlin79} -Keith~J. Devlin. -\newblock {\em Fundamentals of Contemporary Set Theory}. -\newblock Springer, 1979. - -\bibitem{dummett} -Michael Dummett. -\newblock {\em Elements of Intuitionism}. -\newblock Oxford University Press, 1977. - -\bibitem{dyckhoff} -Roy Dyckhoff. -\newblock Contraction-free sequent calculi for intuitionistic logic. -\newblock {\em Journal of Symbolic Logic}, 57(3):795--807, 1992. - \bibitem{felty91a} Amy Felty. \newblock A logic program for transforming sequent proofs to natural deduction @@ -93,22 +48,12 @@ Order Logic}. \newblock Cambridge University Press, 1993. -\bibitem{halmos60} -Paul~R. Halmos. -\newblock {\em Naive Set Theory}. -\newblock Van Nostrand, 1960. - \bibitem{huet78} G.~P. Huet and B.~Lang. \newblock Proving and applying program transformations expressed with second-order patterns. \newblock {\em Acta Informatica}, 11:31--55, 1978. -\bibitem{kunen80} -Kenneth Kunen. -\newblock {\em Set Theory: An Introduction to Independence Proofs}. -\newblock North-Holland, 1980. - \bibitem{alf} Lena Magnusson and Bengt {Nordstr\"{o}m}. \newblock The {ALF} proof editor and its proof engine. @@ -140,8 +85,8 @@ Wolfgang Naraschewski and Markus Wenzel. \newblock Object-oriented verification based on record subtyping in higher-order logic. -\newblock In J.~Grundy and M.~Newey, editors, {\em Theorem Proving in Higher - Order Logics: {TPHOLs} '98}, LNCS 1479, pages 349--366, 1998. +\newblock In Jim Grundy and Malcolm Newey, editors, {\em Theorem Proving in + Higher Order Logics: {TPHOLs} '98}, LNCS 1479, pages 349--366, 1998. \bibitem{nazareth-nipkow} Dieter Nazareth and Tobias Nipkow. @@ -162,22 +107,11 @@ Technology and Theoretical Computer Science}, volume 1180 of {\em LNCS}, pages 180--192. Springer, 1996. -\bibitem{noel} -Philippe No{\"e}l. -\newblock Experimenting with {Isabelle} in {ZF} set theory. -\newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993. - \bibitem{nordstrom90} Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith. \newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}. \newblock Oxford University Press, 1990. -\bibitem{paulin92} -Christine Paulin-Mohring. -\newblock Inductive definitions in the system {Coq}: Rules and properties. -\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, - December 1992. - \bibitem{paulson85} Lawrence~C. Paulson. \newblock Verifying the unification algorithm in {LCF}. @@ -188,24 +122,12 @@ \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}. \newblock Cambridge University Press, 1987. -\bibitem{paulson-set-I} -Lawrence~C. Paulson. -\newblock Set theory for verification: {I}. {From} foundations to functions. -\newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993. - \bibitem{paulson-CADE} Lawrence~C. Paulson. \newblock A fixedpoint approach to implementing (co)inductive definitions. \newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12 International Conference}, LNAI 814, pages 148--161. Springer, 1994. -\bibitem{paulson-final} -Lawrence~C. Paulson. -\newblock A concrete final coalgebra theorem for {ZF} set theory. -\newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em - Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996, - pages 120--139. Springer, 1995. - \bibitem{paulson-set-II} Lawrence~C. Paulson. \newblock Set theory for verification: {II}. {Induction} and recursion. @@ -229,6 +151,11 @@ \newblock In {\em 10th Computer Security Foundations Workshop}, pages 70--83. IEEE Computer Society Press, 1997. +\bibitem{isabelle-ZF} +Lawrence~C. Paulson. +\newblock {Isabelle}'s logics: {FOL} and {ZF}. +\newblock Technical report, Computer Laboratory, University of Cambridge, 1999. + \bibitem{paulson-COLOG} Lawrence~C. Paulson. \newblock A formulation of the simple theory of types (for {Isabelle}). @@ -247,21 +174,11 @@ \newblock A sequent-style model elimination strategy and a positive refinement. \newblock {\em Journal of Automated Reasoning}, 6(4):389--402, 1990. -\bibitem{quaife92} -Art Quaife. -\newblock Automated deduction in {von Neumann-Bernays-G\"{o}del} set theory. -\newblock {\em Journal of Automated Reasoning}, 8(1):91--147, 1992. - \bibitem{slind-tfl} Konrad Slind. \newblock Function definition in higher-order logic. \newblock In von Wright et~al. \cite{tphols96}. -\bibitem{suppes72} -Patrick Suppes. -\newblock {\em Axiomatic Set Theory}. -\newblock Dover, 1972. - \bibitem{takeuti87} G.~Takeuti. \newblock {\em Proof Theory}. @@ -277,12 +194,6 @@ \newblock {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96}, LNCS 1125, 1996. -\bibitem{principia} -A.~N. Whitehead and B.~Russell. -\newblock {\em Principia Mathematica}. -\newblock Cambridge University Press, 1962. -\newblock Paperback edition to *56, abridged from the 2nd edition (1927). - \bibitem{winskel93} Glynn Winskel. \newblock {\em The Formal Semantics of Programming Languages}. diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/logics.ind --- a/doc-src/Logics/logics.ind Fri Jan 08 13:20:59 1999 +0100 +++ b/doc-src/Logics/logics.ind Fri Jan 08 14:02:04 1999 +0100 @@ -1,960 +1,659 @@ \begin{theindex} - \item {\tt !} symbol, 60, 62, 69, 70, 82 - \item {\tt[]} symbol, 82 - \item {\tt\#} symbol, 82 - \item {\tt\#*} symbol, 48, 137 - \item {\tt\#+} symbol, 48, 137 - \item {\tt\#-} symbol, 48 - \item {\tt\&} symbol, 7, 60, 114 - \item {\tt *} symbol, 27, 61, 79, 128 - \item {\tt *} type, 77 - \item {\tt +} symbol, 44, 61, 79, 128 - \item {\tt +} type, 77 - \item {\tt -} symbol, 26, 61, 79, 137 - \item {\tt -->} symbol, 7, 60, 114, 128 - \item {\tt ->} symbol, 27 - \item {\tt -``} symbol, 26 - \item {\tt :} symbol, 26, 68 - \item {\tt <} constant, 80 - \item {\tt <} symbol, 79 - \item {\tt <->} symbol, 7, 114 - \item {\tt <=} constant, 80 - \item {\tt <=} symbol, 26, 68 - \item {\tt =} symbol, 7, 60, 114, 128 - \item {\tt ?} symbol, 60, 62, 69, 70 - \item {\tt ?!} symbol, 60 - \item {\tt\at} symbol, 60, 82 - \item {\tt `} symbol, 26, 128 - \item {\tt ``} symbol, 26, 68 - \item \verb'{}' symbol, 68 - \item {\tt |} symbol, 7, 60, 114 - \item {\tt |-|} symbol, 137 - - \indexspace - - \item {\tt 0} constant, 26, 79, 126 + \item {\tt !} symbol, 6, 8, 15, 16, 28 + \item {\tt[]} symbol, 28 + \item {\tt\#} symbol, 28 + \item {\tt\#*} symbol, 84 + \item {\tt\#+} symbol, 84 + \item {\tt\&} symbol, 6, 60 + \item {\tt *} symbol, 7, 25, 75 + \item {\tt *} type, 23 + \item {\tt +} symbol, 7, 25, 75 + \item {\tt +} type, 23 + \item {\tt -} symbol, 7, 25, 84 + \item {\tt -->} symbol, 6, 60, 75 + \item {\tt :} symbol, 14 + \item {\tt <} constant, 26 + \item {\tt <} symbol, 25 + \item {\tt <->} symbol, 60 + \item {\tt <=} constant, 26 + \item {\tt <=} symbol, 14 + \item {\tt =} symbol, 6, 60, 75 + \item {\tt ?} symbol, 6, 8, 15, 16 + \item {\tt ?!} symbol, 6 + \item {\tt\at} symbol, 6, 28 + \item {\tt `} symbol, 75 + \item {\tt ``} symbol, 14 + \item \verb'{}' symbol, 14 + \item {\tt |} symbol, 6, 60 + \item {\tt |-|} symbol, 84 \indexspace - \item {\tt absdiff_def} theorem, 137 - \item {\tt add_assoc} theorem, 137 - \item {\tt add_commute} theorem, 137 - \item {\tt add_def} theorem, 48, 137 - \item {\tt add_inverse_diff} theorem, 137 - \item {\tt add_mp_tac}, \bold{135} - \item {\tt add_mult_dist} theorem, 48, 137 - \item {\tt add_safes}, \bold{120} - \item {\tt add_typing} theorem, 137 - \item {\tt add_unsafes}, \bold{120} - \item {\tt addC0} theorem, 137 - \item {\tt addC_succ} theorem, 137 - \item {\tt Addsplits}, \bold{76} - \item {\tt addsplits}, \bold{76}, 81, 93 - \item {\tt ALL} symbol, 7, 27, 60, 62, 69, 70, 114 - \item {\tt All} constant, 7, 60, 114 - \item {\tt All_def} theorem, 64 - \item {\tt all_dupE} theorem, 5, 9, 66 - \item {\tt all_impE} theorem, 9 - \item {\tt allE} theorem, 5, 9, 66 - \item {\tt allI} theorem, 8, 66 - \item {\tt allL} theorem, 116, 120 - \item {\tt allL_thin} theorem, 117 - \item {\tt allR} theorem, 116 - \item {\tt and_def} theorem, 43, 64 - \item {\tt app_def} theorem, 50 - \item {\tt apply_def} theorem, 32 - \item {\tt apply_equality} theorem, 40, 41, 57, 58 - \item {\tt apply_equality2} theorem, 40 - \item {\tt apply_iff} theorem, 40 - \item {\tt apply_Pair} theorem, 40, 58 - \item {\tt apply_type} theorem, 40 - \item {\tt arg_cong} theorem, 65 - \item {\tt Arith} theory, 47, 80, 136 - \item assumptions - \subitem contradictory, 16 - \subitem in {\CTT}, 125, 135 + \item {\tt 0} constant, 25, 73 \indexspace - \item {\tt Ball} constant, 26, 30, 68, 70 - \item {\tt ball_cong} theorem, 33, 34 - \item {\tt Ball_def} theorem, 31, 71 - \item {\tt ballE} theorem, 33, 34, 72 - \item {\tt ballI} theorem, 34, 72 - \item {\tt basic} theorem, 116 - \item {\tt basic_defs}, \bold{133} - \item {\tt best_tac}, \bold{121} - \item {\tt beta} theorem, 40, 41 - \item {\tt Bex} constant, 26, 30, 68, 70 - \item {\tt bex_cong} theorem, 33, 34 - \item {\tt Bex_def} theorem, 31, 71 - \item {\tt bexCI} theorem, 34, 70, 72 - \item {\tt bexE} theorem, 34, 72 - \item {\tt bexI} theorem, 34, 70, 72 - \item {\tt bij} constant, 46 - \item {\tt bij_converse_bij} theorem, 46 - \item {\tt bij_def} theorem, 46 - \item {\tt bij_disjoint_Un} theorem, 46 - \item {\tt Blast_tac}, 17, 55, 56 - \item {\tt blast_tac}, 18, 19, 21 - \item {\tt bnd_mono_def} theorem, 45 - \item {\tt Bool} theory, 41 - \item {\textit {bool}} type, 61 - \item {\tt bool_0I} theorem, 43 - \item {\tt bool_1I} theorem, 43 - \item {\tt bool_def} theorem, 43 - \item {\tt boolE} theorem, 43 - \item {\tt box_equals} theorem, 65, 67 - \item {\tt bspec} theorem, 34, 72 - \item {\tt butlast} constant, 82 + \item {\tt absdiff_def} theorem, 84 + \item {\tt add_assoc} theorem, 84 + \item {\tt add_commute} theorem, 84 + \item {\tt add_def} theorem, 84 + \item {\tt add_inverse_diff} theorem, 84 + \item {\tt add_mp_tac}, \bold{82} + \item {\tt add_mult_dist} theorem, 84 + \item {\tt add_safes}, \bold{66} + \item {\tt add_typing} theorem, 84 + \item {\tt add_unsafes}, \bold{66} + \item {\tt addC0} theorem, 84 + \item {\tt addC_succ} theorem, 84 + \item {\tt Addsplits}, \bold{22} + \item {\tt addsplits}, \bold{22}, 27, 39 + \item {\tt ALL} symbol, 6, 8, 15, 16, 60 + \item {\tt All} constant, 6, 60 + \item {\tt All_def} theorem, 10 + \item {\tt all_dupE} theorem, 12 + \item {\tt allE} theorem, 12 + \item {\tt allI} theorem, 12 + \item {\tt allL} theorem, 62, 66 + \item {\tt allL_thin} theorem, 63 + \item {\tt allR} theorem, 62 + \item {\tt and_def} theorem, 10 + \item {\tt arg_cong} theorem, 11 + \item {\tt Arith} theory, 26, 83 + \item assumptions + \subitem in {\CTT}, 72, 82 \indexspace - \item {\tt case} constant, 44 - \item {\tt case} symbol, 63, 80, 81, 93 - \item {\tt case_def} theorem, 44 - \item {\tt case_Inl} theorem, 44 - \item {\tt case_Inr} theorem, 44 - \item {\tt case_tac}, \bold{67} - \item {\tt CCL} theory, 1 - \item {\tt ccontr} theorem, 66 - \item {\tt classical} theorem, 66 - \item {\tt coinduct} theorem, 45 - \item {\tt coinductive}, 105--108 - \item {\tt Collect} constant, 26, 27, 30, 68, 70 - \item {\tt Collect_def} theorem, 31 - \item {\tt Collect_mem_eq} theorem, 70, 71 - \item {\tt Collect_subset} theorem, 37 - \item {\tt CollectD} theorem, 72, 111 - \item {\tt CollectD1} theorem, 33, 35 - \item {\tt CollectD2} theorem, 33, 35 - \item {\tt CollectE} theorem, 33, 35, 72 - \item {\tt CollectI} theorem, 35, 72, 111 - \item {\tt comp_assoc} theorem, 46 - \item {\tt comp_bij} theorem, 46 - \item {\tt comp_def} theorem, 46 - \item {\tt comp_func} theorem, 46 - \item {\tt comp_func_apply} theorem, 46 - \item {\tt comp_inj} theorem, 46 - \item {\tt comp_rls}, \bold{133} - \item {\tt comp_surj} theorem, 46 - \item {\tt comp_type} theorem, 46 - \item {\tt Compl} constant, 68 - \item {\tt Compl_def} theorem, 71 - \item {\tt Compl_disjoint} theorem, 74 - \item {\tt Compl_Int} theorem, 74 - \item {\tt Compl_partition} theorem, 74 - \item {\tt Compl_Un} theorem, 74 - \item {\tt ComplD} theorem, 73 - \item {\tt ComplI} theorem, 73 - \item {\tt concat} constant, 82 - \item {\tt cond_0} theorem, 43 - \item {\tt cond_1} theorem, 43 - \item {\tt cond_def} theorem, 43 - \item {\tt cong} theorem, 65 - \item congruence rules, 33 - \item {\tt conj_cong}, 6, 75 - \item {\tt conj_impE} theorem, 9, 10 - \item {\tt conjE} theorem, 9, 65 - \item {\tt conjI} theorem, 8, 65 - \item {\tt conjL} theorem, 116 - \item {\tt conjR} theorem, 116 - \item {\tt conjunct1} theorem, 8, 65 - \item {\tt conjunct2} theorem, 8, 65 - \item {\tt conL} theorem, 117 - \item {\tt conR} theorem, 117 - \item {\tt cons} constant, 26, 27 - \item {\tt cons_def} theorem, 32 - \item {\tt Cons_iff} theorem, 50 - \item {\tt consCI} theorem, 36 - \item {\tt consE} theorem, 36 - \item {\tt ConsI} theorem, 50 - \item {\tt consI1} theorem, 36 - \item {\tt consI2} theorem, 36 - \item Constructive Type Theory, 125--147 - \item {\tt contr} constant, 126 - \item {\tt converse} constant, 26, 40 - \item {\tt converse_def} theorem, 32 - \item {\tt could_res}, \bold{119} - \item {\tt could_resolve_seq}, \bold{119} - \item {\tt CTT} theory, 1, 125 - \item {\tt Cube} theory, 1 - \item {\tt cut} theorem, 116 - \item {\tt cut_facts_tac}, 19 - \item {\tt cutL_tac}, \bold{118} - \item {\tt cutR_tac}, \bold{118} + \item {\tt Ball} constant, 14, 16 + \item {\tt Ball_def} theorem, 17 + \item {\tt ballE} theorem, 18 + \item {\tt ballI} theorem, 18 + \item {\tt basic} theorem, 62 + \item {\tt basic_defs}, \bold{80} + \item {\tt best_tac}, \bold{67} + \item {\tt Bex} constant, 14, 16 + \item {\tt Bex_def} theorem, 17 + \item {\tt bexCI} theorem, 16, 18 + \item {\tt bexE} theorem, 18 + \item {\tt bexI} theorem, 16, 18 + \item {\textit {bool}} type, 7 + \item {\tt box_equals} theorem, 11, 13 + \item {\tt bspec} theorem, 18 + \item {\tt butlast} constant, 28 \indexspace - \item {\tt datatype}, 90--98 - \item {\tt Delsplits}, \bold{76} - \item {\tt delsplits}, \bold{76} - \item {\tt diff_0_eq_0} theorem, 137 - \item {\tt Diff_cancel} theorem, 42 - \item {\tt Diff_contains} theorem, 37 - \item {\tt Diff_def} theorem, 31 - \item {\tt diff_def} theorem, 48, 137 - \item {\tt Diff_disjoint} theorem, 42 - \item {\tt Diff_Int} theorem, 42 - \item {\tt Diff_partition} theorem, 42 - \item {\tt diff_self_eq_0} theorem, 137 - \item {\tt Diff_subset} theorem, 37 - \item {\tt diff_succ_succ} theorem, 137 - \item {\tt diff_typing} theorem, 137 - \item {\tt Diff_Un} theorem, 42 - \item {\tt diffC0} theorem, 137 - \item {\tt DiffD1} theorem, 36 - \item {\tt DiffD2} theorem, 36 - \item {\tt DiffE} theorem, 36 - \item {\tt DiffI} theorem, 36 - \item {\tt disj_impE} theorem, 9, 10, 14 - \item {\tt disjCI} theorem, 11, 66 - \item {\tt disjE} theorem, 8, 65 - \item {\tt disjI1} theorem, 8, 65 - \item {\tt disjI2} theorem, 8, 65 - \item {\tt disjL} theorem, 116 - \item {\tt disjR} theorem, 116 - \item {\tt div} symbol, 48, 79, 137 - \item {\tt div_def} theorem, 48, 137 - \item {\tt div_geq} theorem, 80 - \item {\tt div_less} theorem, 80 - \item {\tt Divides} theory, 80 - \item {\tt domain} constant, 26, 40 - \item {\tt domain_def} theorem, 32 - \item {\tt domain_of_fun} theorem, 40 - \item {\tt domain_subset} theorem, 39 - \item {\tt domain_type} theorem, 40 - \item {\tt domainE} theorem, 39, 40 - \item {\tt domainI} theorem, 39, 40 - \item {\tt double_complement} theorem, 42, 74 - \item {\tt dresolve_tac}, 54 - \item {\tt drop} constant, 82 - \item {\tt dropWhile} constant, 82 + \item {\tt case} symbol, 9, 26, 27, 39 + \item {\tt case_tac}, \bold{13} + \item {\tt CCL} theory, 1 + \item {\tt ccontr} theorem, 12 + \item {\tt classical} theorem, 12 + \item {\tt coinductive}, 51--54 + \item {\tt Collect} constant, 14, 16 + \item {\tt Collect_mem_eq} theorem, 16, 17 + \item {\tt CollectD} theorem, 18, 57 + \item {\tt CollectE} theorem, 18 + \item {\tt CollectI} theorem, 18, 57 + \item {\tt comp_rls}, \bold{80} + \item {\tt Compl} constant, 14 + \item {\tt Compl_def} theorem, 17 + \item {\tt Compl_disjoint} theorem, 20 + \item {\tt Compl_Int} theorem, 20 + \item {\tt Compl_partition} theorem, 20 + \item {\tt Compl_Un} theorem, 20 + \item {\tt ComplD} theorem, 19 + \item {\tt ComplI} theorem, 19 + \item {\tt concat} constant, 28 + \item {\tt cong} theorem, 11 + \item {\tt conj_cong}, 21 + \item {\tt conjE} theorem, 11 + \item {\tt conjI} theorem, 11 + \item {\tt conjL} theorem, 62 + \item {\tt conjR} theorem, 62 + \item {\tt conjunct1} theorem, 11 + \item {\tt conjunct2} theorem, 11 + \item {\tt conL} theorem, 63 + \item {\tt conR} theorem, 63 + \item Constructive Type Theory, 72--94 + \item {\tt contr} constant, 73 + \item {\tt could_res}, \bold{65} + \item {\tt could_resolve_seq}, \bold{65} + \item {\tt CTT} theory, 1, 72 + \item {\tt Cube} theory, 1 + \item {\tt cut} theorem, 62 + \item {\tt cutL_tac}, \bold{64} + \item {\tt cutR_tac}, \bold{64} + + \indexspace + + \item {\tt datatype}, 36--44 + \item {\tt Delsplits}, \bold{22} + \item {\tt delsplits}, \bold{22} + \item {\tt diff_0_eq_0} theorem, 84 + \item {\tt diff_def} theorem, 84 + \item {\tt diff_self_eq_0} theorem, 84 + \item {\tt diff_succ_succ} theorem, 84 + \item {\tt diff_typing} theorem, 84 + \item {\tt diffC0} theorem, 84 + \item {\tt disjCI} theorem, 12 + \item {\tt disjE} theorem, 11 + \item {\tt disjI1} theorem, 11 + \item {\tt disjI2} theorem, 11 + \item {\tt disjL} theorem, 62 + \item {\tt disjR} theorem, 62 + \item {\tt div} symbol, 25, 84 + \item {\tt div_def} theorem, 84 + \item {\tt div_geq} theorem, 26 + \item {\tt div_less} theorem, 26 + \item {\tt Divides} theory, 26 + \item {\tt double_complement} theorem, 20 + \item {\tt drop} constant, 28 + \item {\tt dropWhile} constant, 28 \indexspace - \item {\tt Elem} constant, 126 - \item {\tt elim_rls}, \bold{133} - \item {\tt elimL_rls}, \bold{133} - \item {\tt empty_def} theorem, 71 - \item {\tt empty_pack}, \bold{119} - \item {\tt empty_subsetI} theorem, 34 - \item {\tt emptyE} theorem, 34, 73 - \item {\tt Eps} constant, 60, 62 - \item {\tt Eq} constant, 126 - \item {\tt eq} constant, 126, 131 - \item {\tt eq_mp_tac}, \bold{10} - \item {\tt EqC} theorem, 132 - \item {\tt EqE} theorem, 132 - \item {\tt Eqelem} constant, 126 - \item {\tt EqF} theorem, 132 - \item {\tt EqFL} theorem, 132 - \item {\tt EqI} theorem, 132 - \item {\tt Eqtype} constant, 126 - \item {\tt equal_tac}, \bold{134} - \item {\tt equal_types} theorem, 129 - \item {\tt equal_typesL} theorem, 129 - \item {\tt equalityCE} theorem, 70, 72, 111, 112 - \item {\tt equalityD1} theorem, 34, 72 - \item {\tt equalityD2} theorem, 34, 72 - \item {\tt equalityE} theorem, 34, 72 - \item {\tt equalityI} theorem, 34, 53, 72 - \item {\tt equals0D} theorem, 34 - \item {\tt equals0I} theorem, 34 - \item {\tt eresolve_tac}, 16 - \item {\tt eta} theorem, 40, 41 - \item {\tt EX} symbol, 7, 27, 60, 62, 69, 70, 114 - \item {\tt Ex} constant, 7, 60, 114 - \item {\tt EX!} symbol, 7, 60 - \item {\tt Ex1} constant, 7, 60 - \item {\tt Ex1_def} theorem, 64 - \item {\tt ex1_def} theorem, 8 - \item {\tt ex1E} theorem, 9, 66 - \item {\tt ex1I} theorem, 9, 66 - \item {\tt Ex_def} theorem, 64 - \item {\tt ex_impE} theorem, 9 - \item {\tt exCI} theorem, 11, 15, 66 - \item {\tt excluded_middle} theorem, 11, 66 - \item {\tt exE} theorem, 8, 66 - \item {\tt exhaust_tac}, \bold{94} - \item {\tt exI} theorem, 8, 66 - \item {\tt exL} theorem, 116 - \item {\tt Exp} theory, 109 - \item {\tt exR} theorem, 116, 120, 121 - \item {\tt exR_thin} theorem, 117, 121, 122 - \item {\tt ext} theorem, 63, 64 - \item {\tt extension} theorem, 31 + \item {\tt Elem} constant, 73 + \item {\tt elim_rls}, \bold{80} + \item {\tt elimL_rls}, \bold{80} + \item {\tt empty_def} theorem, 17 + \item {\tt empty_pack}, \bold{66} + \item {\tt emptyE} theorem, 19 + \item {\tt Eps} constant, 6, 8 + \item {\tt Eq} constant, 73 + \item {\tt eq} constant, 73, 78 + \item {\tt EqC} theorem, 79 + \item {\tt EqE} theorem, 79 + \item {\tt Eqelem} constant, 73 + \item {\tt EqF} theorem, 79 + \item {\tt EqFL} theorem, 79 + \item {\tt EqI} theorem, 79 + \item {\tt Eqtype} constant, 73 + \item {\tt equal_tac}, \bold{81} + \item {\tt equal_types} theorem, 76 + \item {\tt equal_typesL} theorem, 76 + \item {\tt equalityCE} theorem, 16, 18, 57, 58 + \item {\tt equalityD1} theorem, 18 + \item {\tt equalityD2} theorem, 18 + \item {\tt equalityE} theorem, 18 + \item {\tt equalityI} theorem, 18 + \item {\tt EX} symbol, 6, 8, 15, 16, 60 + \item {\tt Ex} constant, 6, 60 + \item {\tt EX!} symbol, 6 + \item {\tt Ex1} constant, 6 + \item {\tt Ex1_def} theorem, 10 + \item {\tt ex1E} theorem, 12 + \item {\tt ex1I} theorem, 12 + \item {\tt Ex_def} theorem, 10 + \item {\tt exCI} theorem, 12 + \item {\tt excluded_middle} theorem, 12 + \item {\tt exE} theorem, 12 + \item {\tt exhaust_tac}, \bold{40} + \item {\tt exI} theorem, 12 + \item {\tt exL} theorem, 62 + \item {\tt Exp} theory, 55 + \item {\tt exR} theorem, 62, 66, 68 + \item {\tt exR_thin} theorem, 63, 68, 69 + \item {\tt ext} theorem, 9, 10 \indexspace - \item {\tt F} constant, 126 - \item {\tt False} constant, 7, 60, 114 - \item {\tt False_def} theorem, 64 - \item {\tt FalseE} theorem, 8, 65 - \item {\tt FalseL} theorem, 116 - \item {\tt fast_tac}, \bold{121} - \item {\tt FE} theorem, 132, 136 - \item {\tt FEL} theorem, 132 - \item {\tt FF} theorem, 132 - \item {\tt field} constant, 26 - \item {\tt field_def} theorem, 32 - \item {\tt field_subset} theorem, 39 - \item {\tt fieldCI} theorem, 39 - \item {\tt fieldE} theorem, 39 - \item {\tt fieldI1} theorem, 39 - \item {\tt fieldI2} theorem, 39 - \item {\tt filseq_resolve_tac}, \bold{119} - \item {\tt filt_resolve_tac}, 119, 134 - \item {\tt filter} constant, 82 - \item {\tt Fin.consI} theorem, 49 - \item {\tt Fin.emptyI} theorem, 49 - \item {\tt Fin_induct} theorem, 49 - \item {\tt Fin_mono} theorem, 49 - \item {\tt Fin_subset} theorem, 49 - \item {\tt Fin_UnI} theorem, 49 - \item {\tt Fin_UnionI} theorem, 49 - \item first-order logic, 5--23 - \item {\tt Fixedpt} theory, 43 - \item {\tt flat} constant, 50 - \item {\tt flat_def} theorem, 50 - \item flex-flex constraints, 115 - \item {\tt FOL} theory, 1, 5, 11, 135 - \item {\tt FOL_cs}, \bold{11} - \item {\tt FOL_ss}, \bold{6} - \item {\tt foldl} constant, 82 - \item {\tt form_rls}, \bold{133} - \item {\tt formL_rls}, \bold{133} - \item {\tt forms_of_seq}, \bold{118} - \item {\tt foundation} theorem, 31 - \item {\tt fst} constant, 26, 33, 77, 126, 131 - \item {\tt fst_conv} theorem, 38, 77 - \item {\tt fst_def} theorem, 32, 131 - \item {\tt Fun} theory, 75 - \item {\textit {fun}} type, 61 - \item {\tt fun_cong} theorem, 65 - \item {\tt fun_disjoint_apply1} theorem, 41, 57 - \item {\tt fun_disjoint_apply2} theorem, 41 - \item {\tt fun_disjoint_Un} theorem, 41, 58 - \item {\tt fun_empty} theorem, 41 - \item {\tt fun_extension} theorem, 40, 41 - \item {\tt fun_is_rel} theorem, 40 - \item {\tt fun_single} theorem, 41 + \item {\tt F} constant, 73 + \item {\tt False} constant, 6, 60 + \item {\tt False_def} theorem, 10 + \item {\tt FalseE} theorem, 11 + \item {\tt FalseL} theorem, 62 + \item {\tt fast_tac}, \bold{67} + \item {\tt FE} theorem, 79, 83 + \item {\tt FEL} theorem, 79 + \item {\tt FF} theorem, 79 + \item {\tt filseq_resolve_tac}, \bold{65} + \item {\tt filt_resolve_tac}, 65, 81 + \item {\tt filter} constant, 28 + \item flex-flex constraints, 61 + \item {\tt FOL} theory, 82 + \item {\tt foldl} constant, 28 + \item {\tt form_rls}, \bold{80} + \item {\tt formL_rls}, \bold{80} + \item {\tt forms_of_seq}, \bold{64} + \item {\tt fst} constant, 23, 73, 78 + \item {\tt fst_conv} theorem, 23 + \item {\tt fst_def} theorem, 78 + \item {\tt Fun} theory, 21 + \item {\textit {fun}} type, 7 + \item {\tt fun_cong} theorem, 11 \item function applications - \subitem in \CTT, 128 - \subitem in \ZF, 26 + \subitem in \CTT, 75 \indexspace - \item {\tt gfp_def} theorem, 45 - \item {\tt gfp_least} theorem, 45 - \item {\tt gfp_mono} theorem, 45 - \item {\tt gfp_subset} theorem, 45 - \item {\tt gfp_Tarski} theorem, 45 - \item {\tt gfp_upperbound} theorem, 45 - \item {\tt Goalw}, 18, 19 - - \indexspace - - \item {\tt hd} constant, 82 - \item higher-order logic, 59--112 - \item {\tt HOL} theory, 1, 59 - \item {\sc hol} system, 59, 62 - \item {\tt HOL_basic_ss}, \bold{75} - \item {\tt HOL_cs}, \bold{76} - \item {\tt HOL_quantifiers}, \bold{62}, 70 - \item {\tt HOL_ss}, \bold{75} + \item {\tt hd} constant, 28 + \item higher-order logic, 5--58 + \item {\tt HOL} theory, 1, 5 + \item {\sc hol} system, 5, 8 + \item {\tt HOL_basic_ss}, \bold{21} + \item {\tt HOL_cs}, \bold{22} + \item {\tt HOL_quantifiers}, \bold{8}, 16 + \item {\tt HOL_ss}, \bold{21} \item {\tt HOLCF} theory, 1 - \item {\tt hyp_rew_tac}, \bold{135} - \item {\tt hyp_subst_tac}, 6, 75 + \item {\tt hyp_rew_tac}, \bold{82} + \item {\tt hyp_subst_tac}, 21 \indexspace - \item {\textit {i}} type, 25, 125 - \item {\tt id} constant, 46 - \item {\tt id_def} theorem, 46 - \item {\tt If} constant, 60 - \item {\tt if} constant, 26 - \item {\tt if_def} theorem, 18, 31, 64 - \item {\tt if_not_P} theorem, 36, 66 - \item {\tt if_P} theorem, 36, 66 - \item {\tt ifE} theorem, 19 - \item {\tt iff} theorem, 63, 64 - \item {\tt iff_def} theorem, 8, 116 - \item {\tt iff_impE} theorem, 9 - \item {\tt iffCE} theorem, 11, 66, 70 - \item {\tt iffD1} theorem, 9, 65 - \item {\tt iffD2} theorem, 9, 65 - \item {\tt iffE} theorem, 9, 65 - \item {\tt iffI} theorem, 9, 19, 65 - \item {\tt iffL} theorem, 117, 123 - \item {\tt iffR} theorem, 117 - \item {\tt ifI} theorem, 19 - \item {\tt IFOL} theory, 5 - \item {\tt IFOL_ss}, \bold{6} - \item {\tt image_def} theorem, 32, 71 - \item {\tt imageE} theorem, 39, 73 - \item {\tt imageI} theorem, 39, 73 - \item {\tt imp_impE} theorem, 9, 14 - \item {\tt impCE} theorem, 11, 66 - \item {\tt impE} theorem, 9, 10, 65 - \item {\tt impI} theorem, 8, 63 - \item {\tt impL} theorem, 116 - \item {\tt impR} theorem, 116 - \item {\tt in} symbol, 28, 61 - \item {\textit {ind}} type, 78 - \item {\tt induct} theorem, 45 - \item {\tt induct_tac}, 80, \bold{94} - \item {\tt inductive}, 105--108 - \item {\tt Inf} constant, 26, 30 - \item {\tt infinity} theorem, 32 - \item {\tt inj} constant, 46, 75 - \item {\tt inj_converse_inj} theorem, 46 - \item {\tt inj_def} theorem, 46, 75 - \item {\tt inj_Inl} theorem, 79 - \item {\tt inj_Inr} theorem, 79 - \item {\tt inj_on} constant, 75 - \item {\tt inj_on_def} theorem, 75 - \item {\tt inj_Suc} theorem, 79 - \item {\tt Inl} constant, 44, 79 - \item {\tt inl} constant, 126, 131, 141 - \item {\tt Inl_def} theorem, 44 - \item {\tt Inl_inject} theorem, 44 - \item {\tt Inl_neq_Inr} theorem, 44 - \item {\tt Inl_not_Inr} theorem, 79 - \item {\tt Inr} constant, 44, 79 - \item {\tt inr} constant, 126, 131 - \item {\tt Inr_def} theorem, 44 - \item {\tt Inr_inject} theorem, 44 - \item {\tt insert} constant, 68 - \item {\tt insert_def} theorem, 71 - \item {\tt insertE} theorem, 73 - \item {\tt insertI1} theorem, 73 - \item {\tt insertI2} theorem, 73 - \item {\tt INT} symbol, 27, 29, 68--70 - \item {\tt Int} symbol, 26, 68 - \item {\tt Int_absorb} theorem, 42, 74 - \item {\tt Int_assoc} theorem, 42, 74 - \item {\tt Int_commute} theorem, 42, 74 - \item {\tt INT_D} theorem, 73 - \item {\tt Int_def} theorem, 31, 71 - \item {\tt INT_E} theorem, 35, 73 - \item {\tt Int_greatest} theorem, 37, 53, 55, 74 - \item {\tt INT_I} theorem, 35, 73 - \item {\tt Int_Inter_image} theorem, 74 - \item {\tt Int_lower1} theorem, 37, 54, 74 - \item {\tt Int_lower2} theorem, 37, 54, 74 - \item {\tt Int_Un_distrib} theorem, 42, 74 - \item {\tt Int_Union} theorem, 74 - \item {\tt Int_Union_RepFun} theorem, 42 - \item {\tt IntD1} theorem, 36, 73 - \item {\tt IntD2} theorem, 36, 73 - \item {\tt IntE} theorem, 36, 54, 73 - \item {\tt INTER} constant, 68 - \item {\tt Inter} constant, 26, 68 - \item {\tt INTER1} constant, 68 - \item {\tt INTER1_def} theorem, 71 - \item {\tt INTER_def} theorem, 71 - \item {\tt Inter_def} theorem, 31, 71 - \item {\tt Inter_greatest} theorem, 37, 74 - \item {\tt Inter_lower} theorem, 37, 74 - \item {\tt Inter_Un_distrib} theorem, 42, 74 - \item {\tt InterD} theorem, 35, 73 - \item {\tt InterE} theorem, 35, 73 - \item {\tt InterI} theorem, 33, 35, 73 - \item {\tt IntI} theorem, 36, 73 - \item {\tt IntPr.best_tac}, \bold{11} - \item {\tt IntPr.fast_tac}, \bold{10}, 13 - \item {\tt IntPr.inst_step_tac}, \bold{10} - \item {\tt IntPr.safe_step_tac}, \bold{10} - \item {\tt IntPr.safe_tac}, \bold{10} - \item {\tt IntPr.step_tac}, \bold{10} - \item {\tt intr_rls}, \bold{133} - \item {\tt intr_tac}, \bold{134}, 143, 144 - \item {\tt intrL_rls}, \bold{133} - \item {\tt inv} constant, 75 - \item {\tt inv_def} theorem, 75 + \item {\textit {i}} type, 72 + \item {\tt If} constant, 6 + \item {\tt if_def} theorem, 10 + \item {\tt if_not_P} theorem, 12 + \item {\tt if_P} theorem, 12 + \item {\tt iff} theorem, 9, 10 + \item {\tt iff_def} theorem, 62 + \item {\tt iffCE} theorem, 12, 16 + \item {\tt iffD1} theorem, 11 + \item {\tt iffD2} theorem, 11 + \item {\tt iffE} theorem, 11 + \item {\tt iffI} theorem, 11 + \item {\tt iffL} theorem, 63, 70 + \item {\tt iffR} theorem, 63 + \item {\tt ILL} theory, 1 + \item {\tt image_def} theorem, 17 + \item {\tt imageE} theorem, 19 + \item {\tt imageI} theorem, 19 + \item {\tt impCE} theorem, 12 + \item {\tt impE} theorem, 11 + \item {\tt impI} theorem, 9 + \item {\tt impL} theorem, 62 + \item {\tt impR} theorem, 62 + \item {\tt in} symbol, 7 + \item {\textit {ind}} type, 24 + \item {\tt induct_tac}, 26, \bold{40} + \item {\tt inductive}, 51--54 + \item {\tt inj} constant, 21 + \item {\tt inj_def} theorem, 21 + \item {\tt inj_Inl} theorem, 25 + \item {\tt inj_Inr} theorem, 25 + \item {\tt inj_on} constant, 21 + \item {\tt inj_on_def} theorem, 21 + \item {\tt inj_Suc} theorem, 25 + \item {\tt Inl} constant, 25 + \item {\tt inl} constant, 73, 78, 88 + \item {\tt Inl_not_Inr} theorem, 25 + \item {\tt Inr} constant, 25 + \item {\tt inr} constant, 73, 78 + \item {\tt insert} constant, 14 + \item {\tt insert_def} theorem, 17 + \item {\tt insertE} theorem, 19 + \item {\tt insertI1} theorem, 19 + \item {\tt insertI2} theorem, 19 + \item {\tt INT} symbol, 14--16 + \item {\tt Int} symbol, 14 + \item {\tt Int_absorb} theorem, 20 + \item {\tt Int_assoc} theorem, 20 + \item {\tt Int_commute} theorem, 20 + \item {\tt INT_D} theorem, 19 + \item {\tt Int_def} theorem, 17 + \item {\tt INT_E} theorem, 19 + \item {\tt Int_greatest} theorem, 20 + \item {\tt INT_I} theorem, 19 + \item {\tt Int_Inter_image} theorem, 20 + \item {\tt Int_lower1} theorem, 20 + \item {\tt Int_lower2} theorem, 20 + \item {\tt Int_Un_distrib} theorem, 20 + \item {\tt Int_Union} theorem, 20 + \item {\tt IntD1} theorem, 19 + \item {\tt IntD2} theorem, 19 + \item {\tt IntE} theorem, 19 + \item {\tt INTER} constant, 14 + \item {\tt Inter} constant, 14 + \item {\tt INTER1} constant, 14 + \item {\tt INTER1_def} theorem, 17 + \item {\tt INTER_def} theorem, 17 + \item {\tt Inter_def} theorem, 17 + \item {\tt Inter_greatest} theorem, 20 + \item {\tt Inter_lower} theorem, 20 + \item {\tt Inter_Un_distrib} theorem, 20 + \item {\tt InterD} theorem, 19 + \item {\tt InterE} theorem, 19 + \item {\tt InterI} theorem, 19 + \item {\tt IntI} theorem, 19 + \item {\tt intr_rls}, \bold{80} + \item {\tt intr_tac}, \bold{81}, 90, 91 + \item {\tt intrL_rls}, \bold{80} + \item {\tt inv} constant, 21 + \item {\tt inv_def} theorem, 21 \indexspace - \item {\tt lam} symbol, 27, 29, 128 - \item {\tt lam_def} theorem, 32 - \item {\tt lam_type} theorem, 40 - \item {\tt Lambda} constant, 26, 30 - \item {\tt lambda} constant, 126, 128 + \item {\tt lam} symbol, 75 + \item {\tt lambda} constant, 73, 75 \item $\lambda$-abstractions - \subitem in \CTT, 128 - \subitem in \ZF, 27 - \item {\tt lamE} theorem, 40, 41 - \item {\tt lamI} theorem, 40, 41 - \item {\tt last} constant, 82 + \subitem in \CTT, 75 + \item {\tt last} constant, 28 \item {\tt LCF} theory, 1 - \item {\tt le_cs}, \bold{24} - \item {\tt LEAST} constant, 61, 62, 80 - \item {\tt Least} constant, 60 - \item {\tt Least_def} theorem, 64 - \item {\tt left_comp_id} theorem, 46 - \item {\tt left_comp_inverse} theorem, 46 - \item {\tt left_inverse} theorem, 46 - \item {\tt length} constant, 50, 82 - \item {\tt length_def} theorem, 50 - \item {\tt less_induct} theorem, 81 - \item {\tt Let} constant, 25, 26, 60, 63 - \item {\tt let} symbol, 28, 61, 63 - \item {\tt Let_def} theorem, 25, 31, 63, 64 - \item {\tt LFilter} theory, 109 - \item {\tt lfp_def} theorem, 45 - \item {\tt lfp_greatest} theorem, 45 - \item {\tt lfp_lowerbound} theorem, 45 - \item {\tt lfp_mono} theorem, 45 - \item {\tt lfp_subset} theorem, 45 - \item {\tt lfp_Tarski} theorem, 45 - \item {\tt List} theory, 81, 82 - \item {\textit{list}} type, 81 - \item {\tt list} constant, 50 - \item {\tt List.induct} theorem, 50 - \item {\tt list_case} constant, 50 - \item {\tt list_mono} theorem, 50 - \item {\tt list_rec} constant, 50 - \item {\tt list_rec_Cons} theorem, 50 - \item {\tt list_rec_def} theorem, 50 - \item {\tt list_rec_Nil} theorem, 50 - \item {\tt LK} theory, 1, 113, 117 - \item {\tt LK_dup_pack}, \bold{120}, 121 - \item {\tt LK_pack}, \bold{120} - \item {\tt LList} theory, 109 - \item {\tt logic} class, 5 + \item {\tt LEAST} constant, 7, 8, 26 + \item {\tt Least} constant, 6 + \item {\tt Least_def} theorem, 10 + \item {\tt length} constant, 28 + \item {\tt less_induct} theorem, 27 + \item {\tt Let} constant, 6, 9 + \item {\tt let} symbol, 7, 9 + \item {\tt Let_def} theorem, 9, 10 + \item {\tt LFilter} theory, 55 + \item {\tt List} theory, 27, 28 + \item {\textit{list}} type, 27 + \item {\tt LK} theory, 1, 59, 63 + \item {\tt LK_dup_pack}, \bold{66}, 67 + \item {\tt LK_pack}, \bold{66} + \item {\tt LList} theory, 55 \indexspace - \item {\tt map} constant, 50, 82 - \item {\tt map_app_distrib} theorem, 50 - \item {\tt map_compose} theorem, 50 - \item {\tt map_def} theorem, 50 - \item {\tt map_flat} theorem, 50 - \item {\tt map_ident} theorem, 50 - \item {\tt map_type} theorem, 50 - \item {\tt max} constant, 61, 80 - \item {\tt mem} symbol, 82 - \item {\tt mem_asym} theorem, 36, 37 - \item {\tt mem_Collect_eq} theorem, 70, 71 - \item {\tt mem_irrefl} theorem, 36 - \item {\tt min} constant, 61, 80 - \item {\tt minus} class, 61 - \item {\tt mod} symbol, 48, 79, 137 - \item {\tt mod_def} theorem, 48, 137 - \item {\tt mod_geq} theorem, 80 - \item {\tt mod_less} theorem, 80 - \item {\tt mod_quo_equality} theorem, 48 + \item {\tt map} constant, 28 + \item {\tt max} constant, 7, 26 + \item {\tt mem} symbol, 28 + \item {\tt mem_Collect_eq} theorem, 16, 17 + \item {\tt min} constant, 7, 26 + \item {\tt minus} class, 7 + \item {\tt mod} symbol, 25, 84 + \item {\tt mod_def} theorem, 84 + \item {\tt mod_geq} theorem, 26 + \item {\tt mod_less} theorem, 26 \item {\tt Modal} theory, 1 - \item {\tt mono} constant, 61 - \item {\tt mp} theorem, 8, 63 - \item {\tt mp_tac}, \bold{10}, \bold{135} - \item {\tt mult_0} theorem, 48 - \item {\tt mult_assoc} theorem, 48, 137 - \item {\tt mult_commute} theorem, 48, 137 - \item {\tt mult_def} theorem, 48, 137 - \item {\tt mult_succ} theorem, 48 - \item {\tt mult_type} theorem, 48 - \item {\tt mult_typing} theorem, 137 - \item {\tt multC0} theorem, 137 - \item {\tt multC_succ} theorem, 137 - \item {\tt mutual_induct_tac}, \bold{94} + \item {\tt mono} constant, 7 + \item {\tt mp} theorem, 9 + \item {\tt mp_tac}, \bold{82} + \item {\tt mult_assoc} theorem, 84 + \item {\tt mult_commute} theorem, 84 + \item {\tt mult_def} theorem, 84 + \item {\tt mult_typing} theorem, 84 + \item {\tt multC0} theorem, 84 + \item {\tt multC_succ} theorem, 84 + \item {\tt mutual_induct_tac}, \bold{40} + + \indexspace + + \item {\tt N} constant, 73 + \item {\tt n_not_Suc_n} theorem, 25 + \item {\tt Nat} theory, 26 + \item {\textit {nat}} type, 25, 26 + \item {\textit{nat}} type, 24--27 + \item {\tt nat_induct} theorem, 25 + \item {\tt nat_rec} constant, 26 + \item {\tt NatDef} theory, 24 + \item {\tt NC0} theorem, 77 + \item {\tt NC_succ} theorem, 77 + \item {\tt NE} theorem, 76, 77, 85 + \item {\tt NEL} theorem, 77 + \item {\tt NF} theorem, 77, 86 + \item {\tt NI0} theorem, 77 + \item {\tt NI_succ} theorem, 77 + \item {\tt NI_succL} theorem, 77 + \item {\tt NIO} theorem, 85 + \item {\tt Not} constant, 6, 60 + \item {\tt not_def} theorem, 10 + \item {\tt not_sym} theorem, 11 + \item {\tt notE} theorem, 11 + \item {\tt notI} theorem, 11 + \item {\tt notL} theorem, 62 + \item {\tt notnotD} theorem, 12 + \item {\tt notR} theorem, 62 + \item {\tt null} constant, 28 \indexspace - \item {\tt N} constant, 126 - \item {\tt n_not_Suc_n} theorem, 79 - \item {\tt Nat} theory, 47, 80 - \item {\textit {nat}} type, 79, 80 - \item {\textit{nat}} type, 78--81 - \item {\tt nat} constant, 48 - \item {\tt nat_0I} theorem, 48 - \item {\tt nat_case} constant, 48 - \item {\tt nat_case_0} theorem, 48 - \item {\tt nat_case_def} theorem, 48 - \item {\tt nat_case_succ} theorem, 48 - \item {\tt nat_def} theorem, 48 - \item {\tt nat_induct} theorem, 48, 79 - \item {\tt nat_rec} constant, 80 - \item {\tt nat_succI} theorem, 48 - \item {\tt NatDef} theory, 78 - \item {\tt NC0} theorem, 130 - \item {\tt NC_succ} theorem, 130 - \item {\tt NE} theorem, 129, 130, 138 - \item {\tt NEL} theorem, 130 - \item {\tt NF} theorem, 130, 139 - \item {\tt NI0} theorem, 130 - \item {\tt NI_succ} theorem, 130 - \item {\tt NI_succL} theorem, 130 - \item {\tt Nil_Cons_iff} theorem, 50 - \item {\tt NilI} theorem, 50 - \item {\tt NIO} theorem, 138 - \item {\tt Not} constant, 7, 60, 114 - \item {\tt not_def} theorem, 8, 43, 64 - \item {\tt not_impE} theorem, 9 - \item {\tt not_sym} theorem, 65 - \item {\tt notE} theorem, 9, 10, 65 - \item {\tt notI} theorem, 9, 65 - \item {\tt notL} theorem, 116 - \item {\tt notnotD} theorem, 11, 66 - \item {\tt notR} theorem, 116 - \item {\tt null} constant, 82 - - \indexspace - - \item {\tt O} symbol, 46 - \item {\textit {o}} type, 5, 113 - \item {\tt o} symbol, 60, 71 - \item {\tt o_def} theorem, 64 - \item {\tt of} symbol, 63 - \item {\tt or_def} theorem, 43, 64 - \item {\tt Ord} theory, 61 - \item {\tt ord} class, 61, 62, 80 - \item {\tt order} class, 61, 80 + \item {\textit {o}} type, 59 + \item {\tt o} symbol, 6, 17 + \item {\tt o_def} theorem, 10 + \item {\tt of} symbol, 9 + \item {\tt or_def} theorem, 10 + \item {\tt Ord} theory, 7 + \item {\tt ord} class, 7, 8, 26 + \item {\tt order} class, 7, 26 \indexspace - \item {\tt pack} ML type, 119 - \item {\tt Pair} constant, 26, 27, 77 - \item {\tt pair} constant, 126 - \item {\tt Pair_def} theorem, 32 - \item {\tt Pair_eq} theorem, 77 - \item {\tt Pair_inject} theorem, 38, 77 - \item {\tt Pair_inject1} theorem, 38 - \item {\tt Pair_inject2} theorem, 38 - \item {\tt Pair_neq_0} theorem, 38 - \item {\tt PairE} theorem, 77 - \item {\tt pairing} theorem, 35 - \item {\tt pc_tac}, \bold{121}, \bold{136}, 142, 143 - \item {\tt Perm} theory, 43 - \item {\tt Pi} constant, 26, 29, 41 - \item {\tt Pi_def} theorem, 32 - \item {\tt Pi_type} theorem, 40, 41 - \item {\tt plus} class, 61 - \item {\tt PlusC_inl} theorem, 132 - \item {\tt PlusC_inr} theorem, 132 - \item {\tt PlusE} theorem, 132, 136, 140 - \item {\tt PlusEL} theorem, 132 - \item {\tt PlusF} theorem, 132 - \item {\tt PlusFL} theorem, 132 - \item {\tt PlusI_inl} theorem, 132, 141 - \item {\tt PlusI_inlL} theorem, 132 - \item {\tt PlusI_inr} theorem, 132 - \item {\tt PlusI_inrL} theorem, 132 - \item {\tt Pow} constant, 26, 68 - \item {\tt Pow_def} theorem, 71 - \item {\tt Pow_iff} theorem, 31 - \item {\tt Pow_mono} theorem, 53 - \item {\tt PowD} theorem, 34, 54, 73 - \item {\tt PowI} theorem, 34, 54, 73 - \item {\tt primrec}, 99--102 - \item {\tt primrec} symbol, 80 - \item {\tt PrimReplace} constant, 26, 30 - \item priorities, 2 - \item {\tt PROD} symbol, 27, 29, 127, 128 - \item {\tt Prod} constant, 126 - \item {\tt Prod} theory, 77 - \item {\tt ProdC} theorem, 130, 146 - \item {\tt ProdC2} theorem, 130 - \item {\tt ProdE} theorem, 130, 143, 145, 147 - \item {\tt ProdEL} theorem, 130 - \item {\tt ProdF} theorem, 130 - \item {\tt ProdFL} theorem, 130 - \item {\tt ProdI} theorem, 130, 136, 138 - \item {\tt ProdIL} theorem, 130 - \item {\tt prop_cs}, \bold{11}, \bold{76} - \item {\tt prop_pack}, \bold{119} + \item {\tt pack} ML type, 65 + \item {\tt Pair} constant, 23 + \item {\tt pair} constant, 73 + \item {\tt Pair_eq} theorem, 23 + \item {\tt Pair_inject} theorem, 23 + \item {\tt PairE} theorem, 23 + \item {\tt pc_tac}, \bold{67}, \bold{83}, 89, 90 + \item {\tt plus} class, 7 + \item {\tt PlusC_inl} theorem, 79 + \item {\tt PlusC_inr} theorem, 79 + \item {\tt PlusE} theorem, 79, 83, 87 + \item {\tt PlusEL} theorem, 79 + \item {\tt PlusF} theorem, 79 + \item {\tt PlusFL} theorem, 79 + \item {\tt PlusI_inl} theorem, 79, 88 + \item {\tt PlusI_inlL} theorem, 79 + \item {\tt PlusI_inr} theorem, 79 + \item {\tt PlusI_inrL} theorem, 79 + \item {\tt Pow} constant, 14 + \item {\tt Pow_def} theorem, 17 + \item {\tt PowD} theorem, 19 + \item {\tt PowI} theorem, 19 + \item {\tt primrec}, 45--48 + \item {\tt primrec} symbol, 26 + \item priorities, 3 + \item {\tt PROD} symbol, 74, 75 + \item {\tt Prod} constant, 73 + \item {\tt Prod} theory, 23 + \item {\tt ProdC} theorem, 77, 93 + \item {\tt ProdC2} theorem, 77 + \item {\tt ProdE} theorem, 77, 90, 92, 94 + \item {\tt ProdEL} theorem, 77 + \item {\tt ProdF} theorem, 77 + \item {\tt ProdFL} theorem, 77 + \item {\tt ProdI} theorem, 77, 83, 85 + \item {\tt ProdIL} theorem, 77 + \item {\tt prop_cs}, \bold{22} + \item {\tt prop_pack}, \bold{66} \indexspace - \item {\tt qcase_def} theorem, 44 - \item {\tt qconverse} constant, 43 - \item {\tt qconverse_def} theorem, 44 - \item {\tt qed_spec_mp}, 97 - \item {\tt qfsplit_def} theorem, 44 - \item {\tt QInl_def} theorem, 44 - \item {\tt QInr_def} theorem, 44 - \item {\tt QPair} theory, 43 - \item {\tt QPair_def} theorem, 44 - \item {\tt QSigma} constant, 43 - \item {\tt QSigma_def} theorem, 44 - \item {\tt qsplit} constant, 43 - \item {\tt qsplit_def} theorem, 44 - \item {\tt qsum_def} theorem, 44 - \item {\tt QUniv} theory, 47 + \item {\tt qed_spec_mp}, 43 + + \indexspace + + \item {\tt range} constant, 14, 56 + \item {\tt range_def} theorem, 17 + \item {\tt rangeE} theorem, 19, 57 + \item {\tt rangeI} theorem, 19 + \item {\tt rec} constant, 73, 76 + \item {\tt recdef}, 48--51 + \item {\tt record}, 33 + \item {\tt record_split_tac}, 35, 36 + \item recursion + \subitem general, 48--51 + \subitem primitive, 45--48 + \item recursive functions, \see{recursion}{44} + \item {\tt red_if_equal} theorem, 76 + \item {\tt Reduce} constant, 73, 76, 82 + \item {\tt refl} theorem, 9, 62 + \item {\tt refl_elem} theorem, 76, 80 + \item {\tt refl_red} theorem, 76 + \item {\tt refl_type} theorem, 76, 80 + \item {\tt REPEAT_FIRST}, 81 + \item {\tt repeat_goal_tac}, \bold{67} + \item {\tt replace_type} theorem, 80, 92 + \item {\tt reresolve_tac}, \bold{67} + \item {\tt res_inst_tac}, 8 + \item {\tt rev} constant, 28 + \item {\tt rew_tac}, \bold{82} + \item {\tt RL}, 87 + \item {\tt RS}, 92, 94 \indexspace - \item {\tt range} constant, 26, 68, 110 - \item {\tt range_def} theorem, 32, 71 - \item {\tt range_of_fun} theorem, 40, 41 - \item {\tt range_subset} theorem, 39 - \item {\tt range_type} theorem, 40 - \item {\tt rangeE} theorem, 39, 73, 111 - \item {\tt rangeI} theorem, 39, 73 - \item {\tt rank} constant, 49 - \item {\tt rank_ss}, \bold{24} - \item {\tt rec} constant, 48, 126, 129 - \item {\tt rec_0} theorem, 48 - \item {\tt rec_def} theorem, 48 - \item {\tt rec_succ} theorem, 48 - \item {\tt recdef}, 102--105 - \item {\tt record}, 87 - \item {\tt record_split_tac}, 89, 90 - \item recursion - \subitem general, 102--105 - \subitem primitive, 99--102 - \item recursive functions, \see{recursion}{98} - \item {\tt red_if_equal} theorem, 129 - \item {\tt Reduce} constant, 126, 129, 135 - \item {\tt refl} theorem, 8, 63, 116 - \item {\tt refl_elem} theorem, 129, 133 - \item {\tt refl_red} theorem, 129 - \item {\tt refl_type} theorem, 129, 133 - \item {\tt REPEAT_FIRST}, 134 - \item {\tt repeat_goal_tac}, \bold{121} - \item {\tt RepFun} constant, 26, 29, 30, 33 - \item {\tt RepFun_def} theorem, 31 - \item {\tt RepFunE} theorem, 35 - \item {\tt RepFunI} theorem, 35 - \item {\tt Replace} constant, 26, 29, 30, 33 - \item {\tt Replace_def} theorem, 31 - \item {\tt replace_type} theorem, 133, 145 - \item {\tt ReplaceE} theorem, 35 - \item {\tt ReplaceI} theorem, 35 - \item {\tt replacement} theorem, 31 - \item {\tt reresolve_tac}, \bold{121} - \item {\tt res_inst_tac}, 62 - \item {\tt restrict} constant, 26, 33 - \item {\tt restrict} theorem, 40 - \item {\tt restrict_bij} theorem, 46 - \item {\tt restrict_def} theorem, 32 - \item {\tt restrict_type} theorem, 40 - \item {\tt rev} constant, 50, 82 - \item {\tt rev_def} theorem, 50 - \item {\tt rew_tac}, 19, \bold{135} - \item {\tt rewrite_rule}, 19 - \item {\tt right_comp_id} theorem, 46 - \item {\tt right_comp_inverse} theorem, 46 - \item {\tt right_inverse} theorem, 46 - \item {\tt RL}, 140 - \item {\tt RS}, 145, 147 + \item {\tt safe_goal_tac}, \bold{67} + \item {\tt safe_tac}, \bold{83} + \item {\tt safestep_tac}, \bold{83} + \item search + \subitem best-first, 58 + \item {\tt select_equality} theorem, 10, 12 + \item {\tt selectI} theorem, 9, 10 + \item {\tt Seqof} constant, 60 + \item sequent calculus, 59--71 + \item {\tt Set} theory, 13, 16 + \item {\tt set} constant, 28 + \item {\tt set} type, 13 + \item {\tt set_current_thy}, 58 + \item {\tt set_diff_def} theorem, 17 + \item {\tt show_sorts}, 8 + \item {\tt show_types}, 8 + \item {\tt Sigma} constant, 23 + \item {\tt Sigma_def} theorem, 23 + \item {\tt SigmaE} theorem, 23 + \item {\tt SigmaI} theorem, 23 + \item simplification + \subitem of conjunctions, 21 + \item {\tt size} constant, 39 + \item {\tt snd} constant, 23, 73, 78 + \item {\tt snd_conv} theorem, 23 + \item {\tt snd_def} theorem, 78 + \item {\tt sobj} type, 63 + \item {\tt spec} theorem, 12 + \item {\tt split} constant, 23, 73, 87 + \item {\tt split} theorem, 23 + \item {\tt split_all_tac}, \bold{24} + \item {\tt split_if} theorem, 12, 22 + \item {\tt split_list_case} theorem, 27 + \item {\tt split_split} theorem, 23 + \item {\tt split_sum_case} theorem, 25 + \item {\tt ssubst} theorem, 11, 13 + \item {\tt stac}, \bold{21} + \item {\tt step_tac}, \bold{67}, \bold{83} + \item {\tt strip_tac}, \bold{13} + \item {\tt subset_def} theorem, 17 + \item {\tt subset_refl} theorem, 18 + \item {\tt subset_trans} theorem, 18 + \item {\tt subsetCE} theorem, 16, 18 + \item {\tt subsetD} theorem, 16, 18 + \item {\tt subsetI} theorem, 18 + \item {\tt subst} theorem, 9 + \item {\tt subst_elem} theorem, 76 + \item {\tt subst_elemL} theorem, 76 + \item {\tt subst_eqtyparg} theorem, 80, 92 + \item {\tt subst_prodE} theorem, 78, 80 + \item {\tt subst_type} theorem, 76 + \item {\tt subst_typeL} theorem, 76 + \item {\tt Suc} constant, 25 + \item {\tt Suc_not_Zero} theorem, 25 + \item {\tt succ} constant, 73 + \item {\tt SUM} symbol, 74, 75 + \item {\tt Sum} constant, 73 + \item {\tt Sum} theory, 24 + \item {\tt sum_case} constant, 25 + \item {\tt sum_case_Inl} theorem, 25 + \item {\tt sum_case_Inr} theorem, 25 + \item {\tt SumC} theorem, 78 + \item {\tt SumE} theorem, 78, 83, 87 + \item {\tt sumE} theorem, 25 + \item {\tt SumE_fst} theorem, 78, 80, 92, 93 + \item {\tt SumE_snd} theorem, 78, 80, 94 + \item {\tt SumEL} theorem, 78 + \item {\tt SumF} theorem, 78 + \item {\tt SumFL} theorem, 78 + \item {\tt SumI} theorem, 78, 88 + \item {\tt SumIL} theorem, 78 + \item {\tt SumIL2} theorem, 80 + \item {\tt surj} constant, 17, 21 + \item {\tt surj_def} theorem, 21 + \item {\tt surjective_pairing} theorem, 23 + \item {\tt surjective_sum} theorem, 25 + \item {\tt swap} theorem, 12 + \item {\tt swap_res_tac}, 57 + \item {\tt sym} theorem, 11, 62 + \item {\tt sym_elem} theorem, 76 + \item {\tt sym_type} theorem, 76 + \item {\tt symL} theorem, 63 \indexspace - \item {\tt safe_goal_tac}, \bold{121} - \item {\tt safe_tac}, \bold{136} - \item {\tt safestep_tac}, \bold{136} - \item search - \subitem best-first, 112 - \item {\tt select_equality} theorem, 64, 66 - \item {\tt selectI} theorem, 63, 64 - \item {\tt separation} theorem, 35 - \item {\tt Seqof} constant, 114 - \item sequent calculus, 113--124 - \item {\tt Set} theory, 67, 70 - \item {\tt set} constant, 82 - \item {\tt set} type, 67 - \item set theory, 24--58 - \item {\tt set_current_thy}, 112 - \item {\tt set_diff_def} theorem, 71 - \item {\tt show_sorts}, 62 - \item {\tt show_types}, 62 - \item {\tt Sigma} constant, 26, 29, 30, 38, 77 - \item {\tt Sigma_def} theorem, 32, 77 - \item {\tt SigmaE} theorem, 38, 77 - \item {\tt SigmaE2} theorem, 38 - \item {\tt SigmaI} theorem, 38, 77 - \item simplification - \subitem of conjunctions, 6, 75 - \item {\tt singletonE} theorem, 36 - \item {\tt singletonI} theorem, 36 - \item {\tt size} constant, 93 - \item {\tt snd} constant, 26, 33, 77, 126, 131 - \item {\tt snd_conv} theorem, 38, 77 - \item {\tt snd_def} theorem, 32, 131 - \item {\tt sobj} type, 117 - \item {\tt spec} theorem, 8, 66 - \item {\tt split} constant, 26, 33, 77, 126, 140 - \item {\tt split} theorem, 38, 77 - \item {\tt split_all_tac}, \bold{78} - \item {\tt split_def} theorem, 32 - \item {\tt split_if} theorem, 66, 76 - \item {\tt split_list_case} theorem, 81 - \item {\tt split_split} theorem, 77 - \item {\tt split_sum_case} theorem, 79 - \item {\tt ssubst} theorem, 9, 65, 67 - \item {\tt stac}, \bold{75} - \item {\tt Step_tac}, 22 - \item {\tt step_tac}, 23, \bold{121}, \bold{136} - \item {\tt strip_tac}, \bold{67} - \item {\tt subset_def} theorem, 31, 71 - \item {\tt subset_refl} theorem, 34, 72 - \item {\tt subset_trans} theorem, 34, 72 - \item {\tt subsetCE} theorem, 34, 70, 72 - \item {\tt subsetD} theorem, 34, 56, 70, 72 - \item {\tt subsetI} theorem, 34, 54, 55, 72 - \item {\tt subst} theorem, 8, 63 - \item {\tt subst_elem} theorem, 129 - \item {\tt subst_elemL} theorem, 129 - \item {\tt subst_eqtyparg} theorem, 133, 145 - \item {\tt subst_prodE} theorem, 131, 133 - \item {\tt subst_type} theorem, 129 - \item {\tt subst_typeL} theorem, 129 - \item {\tt Suc} constant, 79 - \item {\tt Suc_not_Zero} theorem, 79 - \item {\tt succ} constant, 26, 30, 126 - \item {\tt succ_def} theorem, 32 - \item {\tt succ_inject} theorem, 36 - \item {\tt succ_neq_0} theorem, 36 - \item {\tt succCI} theorem, 36 - \item {\tt succE} theorem, 36 - \item {\tt succI1} theorem, 36 - \item {\tt succI2} theorem, 36 - \item {\tt SUM} symbol, 27, 29, 127, 128 - \item {\tt Sum} constant, 126 - \item {\tt Sum} theory, 43, 78 - \item {\tt sum_case} constant, 79 - \item {\tt sum_case_Inl} theorem, 79 - \item {\tt sum_case_Inr} theorem, 79 - \item {\tt sum_def} theorem, 44 - \item {\tt sum_InlI} theorem, 44 - \item {\tt sum_InrI} theorem, 44 - \item {\tt SUM_Int_distrib1} theorem, 42 - \item {\tt SUM_Int_distrib2} theorem, 42 - \item {\tt SUM_Un_distrib1} theorem, 42 - \item {\tt SUM_Un_distrib2} theorem, 42 - \item {\tt SumC} theorem, 131 - \item {\tt SumE} theorem, 131, 136, 140 - \item {\tt sumE} theorem, 79 - \item {\tt sumE2} theorem, 44 - \item {\tt SumE_fst} theorem, 131, 133, 145, 146 - \item {\tt SumE_snd} theorem, 131, 133, 147 - \item {\tt SumEL} theorem, 131 - \item {\tt SumF} theorem, 131 - \item {\tt SumFL} theorem, 131 - \item {\tt SumI} theorem, 131, 141 - \item {\tt SumIL} theorem, 131 - \item {\tt SumIL2} theorem, 133 - \item {\tt surj} constant, 46, 71, 75 - \item {\tt surj_def} theorem, 46, 75 - \item {\tt surjective_pairing} theorem, 77 - \item {\tt surjective_sum} theorem, 79 - \item {\tt swap} theorem, 11, 66 - \item {\tt swap_res_tac}, 16, 111 - \item {\tt sym} theorem, 9, 65, 116 - \item {\tt sym_elem} theorem, 129 - \item {\tt sym_type} theorem, 129 - \item {\tt symL} theorem, 117 + \item {\tt T} constant, 73 + \item {\textit {t}} type, 72 + \item {\tt take} constant, 28 + \item {\tt takeWhile} constant, 28 + \item {\tt TC} theorem, 79 + \item {\tt TE} theorem, 79 + \item {\tt TEL} theorem, 79 + \item {\tt term} class, 7, 59 + \item {\tt test_assume_tac}, \bold{81} + \item {\tt TF} theorem, 79 + \item {\tt THE} symbol, 60 + \item {\tt The} constant, 60 + \item {\tt The} theorem, 62 + \item {\tt thinL} theorem, 62 + \item {\tt thinR} theorem, 62 + \item {\tt TI} theorem, 79 + \item {\tt times} class, 7 + \item {\tt tl} constant, 28 + \item tracing + \subitem of unification, 8 + \item {\tt trans} theorem, 11, 62 + \item {\tt trans_elem} theorem, 76 + \item {\tt trans_red} theorem, 76 + \item {\tt trans_tac}, 27 + \item {\tt trans_type} theorem, 76 + \item {\tt True} constant, 6, 60 + \item {\tt True_def} theorem, 10, 62 + \item {\tt True_or_False} theorem, 9, 10 + \item {\tt TrueI} theorem, 11 + \item {\tt Trueprop} constant, 6, 60 + \item {\tt TrueR} theorem, 63 + \item {\tt tt} constant, 73 + \item {\tt Type} constant, 73 + \item type definition, \bold{30} + \item {\tt typechk_tac}, \bold{81}, 86, 89, 93, 94 + \item {\tt typedef}, 27 \indexspace - \item {\tt T} constant, 126 - \item {\textit {t}} type, 125 - \item {\tt take} constant, 82 - \item {\tt takeWhile} constant, 82 - \item {\tt TC} theorem, 132 - \item {\tt TE} theorem, 132 - \item {\tt TEL} theorem, 132 - \item {\tt term} class, 5, 61, 113 - \item {\tt test_assume_tac}, \bold{134} - \item {\tt TF} theorem, 132 - \item {\tt THE} symbol, 27, 29, 37, 114 - \item {\tt The} constant, 26, 29, 30, 114 - \item {\tt The} theorem, 116 - \item {\tt the_def} theorem, 31 - \item {\tt the_equality} theorem, 36, 37 - \item {\tt theI} theorem, 36, 37 - \item {\tt thinL} theorem, 116 - \item {\tt thinR} theorem, 116 - \item {\tt TI} theorem, 132 - \item {\tt times} class, 61 - \item {\tt tl} constant, 82 - \item tracing - \subitem of unification, 62 - \item {\tt trans} theorem, 9, 65, 116 - \item {\tt trans_elem} theorem, 129 - \item {\tt trans_red} theorem, 129 - \item {\tt trans_tac}, 81 - \item {\tt trans_type} theorem, 129 - \item {\tt True} constant, 7, 60, 114 - \item {\tt True_def} theorem, 8, 64, 116 - \item {\tt True_or_False} theorem, 63, 64 - \item {\tt TrueI} theorem, 9, 65 - \item {\tt Trueprop} constant, 7, 60, 114 - \item {\tt TrueR} theorem, 117 - \item {\tt tt} constant, 126 - \item {\tt Type} constant, 126 - \item type definition, \bold{84} - \item {\tt typechk_tac}, \bold{134}, 139, 142, 146, 147 - \item {\tt typedef}, 81 + \item {\tt UN} symbol, 14--16 + \item {\tt Un} symbol, 14 + \item {\tt Un1} theorem, 16 + \item {\tt Un2} theorem, 16 + \item {\tt Un_absorb} theorem, 20 + \item {\tt Un_assoc} theorem, 20 + \item {\tt Un_commute} theorem, 20 + \item {\tt Un_def} theorem, 17 + \item {\tt UN_E} theorem, 19 + \item {\tt UN_I} theorem, 19 + \item {\tt Un_Int_distrib} theorem, 20 + \item {\tt Un_Inter} theorem, 20 + \item {\tt Un_least} theorem, 20 + \item {\tt Un_Union_image} theorem, 20 + \item {\tt Un_upper1} theorem, 20 + \item {\tt Un_upper2} theorem, 20 + \item {\tt UnCI} theorem, 16, 19 + \item {\tt UnE} theorem, 19 + \item {\tt UnI1} theorem, 19 + \item {\tt UnI2} theorem, 19 + \item unification + \subitem incompleteness of, 8 + \item {\tt Unify.trace_types}, 8 + \item {\tt UNION} constant, 14 + \item {\tt Union} constant, 14 + \item {\tt UNION1} constant, 14 + \item {\tt UNION1_def} theorem, 17 + \item {\tt UNION_def} theorem, 17 + \item {\tt Union_def} theorem, 17 + \item {\tt Union_least} theorem, 20 + \item {\tt Union_Un_distrib} theorem, 20 + \item {\tt Union_upper} theorem, 20 + \item {\tt UnionE} theorem, 19 + \item {\tt UnionI} theorem, 19 + \item {\tt unit_eq} theorem, 24 \indexspace - \item {\tt UN} symbol, 27, 29, 68--70 - \item {\tt Un} symbol, 26, 68 - \item {\tt Un1} theorem, 70 - \item {\tt Un2} theorem, 70 - \item {\tt Un_absorb} theorem, 42, 74 - \item {\tt Un_assoc} theorem, 42, 74 - \item {\tt Un_commute} theorem, 42, 74 - \item {\tt Un_def} theorem, 31, 71 - \item {\tt UN_E} theorem, 35, 73 - \item {\tt UN_I} theorem, 35, 73 - \item {\tt Un_Int_distrib} theorem, 42, 74 - \item {\tt Un_Inter} theorem, 74 - \item {\tt Un_Inter_RepFun} theorem, 42 - \item {\tt Un_least} theorem, 37, 74 - \item {\tt Un_Union_image} theorem, 74 - \item {\tt Un_upper1} theorem, 37, 74 - \item {\tt Un_upper2} theorem, 37, 74 - \item {\tt UnCI} theorem, 36, 37, 70, 73 - \item {\tt UnE} theorem, 36, 73 - \item {\tt UnI1} theorem, 36, 37, 57, 73 - \item {\tt UnI2} theorem, 36, 37, 73 - \item unification - \subitem incompleteness of, 62 - \item {\tt Unify.trace_types}, 62 - \item {\tt UNION} constant, 68 - \item {\tt Union} constant, 26, 68 - \item {\tt UNION1} constant, 68 - \item {\tt UNION1_def} theorem, 71 - \item {\tt UNION_def} theorem, 71 - \item {\tt Union_def} theorem, 71 - \item {\tt Union_iff} theorem, 31 - \item {\tt Union_least} theorem, 37, 74 - \item {\tt Union_Un_distrib} theorem, 42, 74 - \item {\tt Union_upper} theorem, 37, 74 - \item {\tt UnionE} theorem, 35, 56, 73 - \item {\tt UnionI} theorem, 35, 56, 73 - \item {\tt unit_eq} theorem, 78 - \item {\tt Univ} theory, 47 - \item {\tt Upair} constant, 25, 26, 30 - \item {\tt Upair_def} theorem, 31 - \item {\tt UpairE} theorem, 35 - \item {\tt UpairI1} theorem, 35 - \item {\tt UpairI2} theorem, 35 + \item {\tt when} constant, 73, 78, 87 \indexspace - \item {\tt vimage_def} theorem, 32 - \item {\tt vimageE} theorem, 39 - \item {\tt vimageI} theorem, 39 - - \indexspace - - \item {\tt when} constant, 126, 131, 140 - - \indexspace - - \item {\tt xor_def} theorem, 43 - - \indexspace - - \item {\tt zero_ne_succ} theorem, 129, 130 - \item {\tt ZF} theory, 1, 24, 59 - \item {\tt ZF_cs}, \bold{24} - \item {\tt ZF_ss}, \bold{24} + \item {\tt zero_ne_succ} theorem, 76, 77 + \item {\tt ZF} theory, 5 \end{theindex} diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/logics.tex --- a/doc-src/Logics/logics.tex Fri Jan 08 13:20:59 1999 +0100 +++ b/doc-src/Logics/logics.tex Fri Jan 08 14:02:04 1999 +0100 @@ -1,3 +1,4 @@ +%% $Id$ \documentclass[12pt]{report} \usepackage{graphicx,a4,latexsym,../pdfsetup} @@ -8,15 +9,13 @@ \input{../extra.sty} \makeatother -%% $Id$ %%%STILL NEEDS MODAL, LCF -%%%\includeonly{ZF} %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} %% run ../sedindex logics to prepare index file -\title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] Isabelle's Object-Logics} +\title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] Isabelle's Logics} \author{{\em Lawrence C. Paulson}\\ Computer Laboratory \\ University of Cambridge \\ @@ -25,9 +24,8 @@ \thanks{Tobias Nipkow revised and extended the chapter on \HOL. Markus Wenzel made numerous improvements. Philippe de Groote wrote the - first version of the logic~\LK{} and contributed to~\ZF{}. Tobias - Nipkow developed~\HOL{}, \LCF{} and~\Cube{}. Philippe No\"el and - Martin Coen made many contributions to~\ZF{}. Martin Coen + first version of the logic~\LK{}. Tobias + Nipkow developed~\HOL{}, \LCF{} and~\Cube{}. Martin Coen developed~\Modal{} with assistance from Rajeev Gor\'e. The research has been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT project 6453: Types.} @@ -39,9 +37,6 @@ \makeindex -%%\newenvironment{example}{\begin{Example}\rm}{\end{Example}} -%%\newtheorem{Example}{Example}[chapter] - \underscoreoff \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? @@ -53,9 +48,8 @@ \begin{document} \maketitle \pagenumbering{roman} \tableofcontents \clearfirst -\include{intro} -\include{FOL} -\include{ZF} +\include{preface} +\include{syntax} \include{HOL} \include{LK} %%\include{Modal}