paulson@6121: %% $Id$ paulson@6121: \chapter{Zermelo-Fraenkel Set Theory} paulson@6121: \index{set theory|(} paulson@6121: paulson@6121: The theory~\thydx{ZF} implements Zermelo-Fraenkel set paulson@6121: theory~\cite{halmos60,suppes72} as an extension of~\texttt{FOL}, classical paulson@6121: first-order logic. The theory includes a collection of derived natural paulson@14154: deduction rules, for use with Isabelle's classical reasoner. Some paulson@6121: of it is based on the work of No\"el~\cite{noel}. paulson@6121: paulson@6121: A tremendous amount of set theory has been formally developed, including the paulson@6121: basic properties of relations, functions, ordinals and cardinals. Significant paulson@6121: results have been proved, such as the Schr\"oder-Bernstein Theorem, the paulson@6121: Wellordering Theorem and a version of Ramsey's Theorem. \texttt{ZF} provides paulson@6121: both the integers and the natural numbers. General methods have been paulson@6121: developed for solving recursion equations over monotonic functors; these have paulson@6121: been applied to yield constructions of lists, trees, infinite lists, etc. paulson@6121: paulson@6121: \texttt{ZF} has a flexible package for handling inductive definitions, paulson@6121: such as inference systems, and datatype definitions, such as lists and paulson@6121: trees. Moreover it handles coinductive definitions, such as paulson@6121: bisimulation relations, and codatatype definitions, such as streams. It paulson@6121: provides a streamlined syntax for defining primitive recursive functions over paulson@6121: datatypes. paulson@6121: paulson@6121: Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF} paulson@6121: less formally than this chapter. Isabelle employs a novel treatment of paulson@6121: non-well-founded data structures within the standard {\sc zf} axioms including paulson@6592: the Axiom of Foundation~\cite{paulson-mscs}. paulson@6121: paulson@6121: paulson@6121: \section{Which version of axiomatic set theory?} paulson@6121: The two main axiom systems for set theory are Bernays-G\"odel~({\sc bg}) paulson@6121: and Zermelo-Fraenkel~({\sc zf}). Resolution theorem provers can use {\sc paulson@6121: bg} because it is finite~\cite{boyer86,quaife92}. {\sc zf} does not paulson@6121: have a finite axiom system because of its Axiom Scheme of Replacement. paulson@6121: This makes it awkward to use with many theorem provers, since instances paulson@6121: of the axiom scheme have to be invoked explicitly. Since Isabelle has no paulson@6121: difficulty with axiom schemes, we may adopt either axiom system. paulson@6121: paulson@6121: These two theories differ in their treatment of {\bf classes}, which are paulson@6121: collections that are `too big' to be sets. The class of all sets,~$V$, paulson@6121: cannot be a set without admitting Russell's Paradox. In {\sc bg}, both paulson@6121: classes and sets are individuals; $x\in V$ expresses that $x$ is a set. In paulson@6121: {\sc zf}, all variables denote sets; classes are identified with unary paulson@6121: predicates. The two systems define essentially the same sets and classes, paulson@6121: with similar properties. In particular, a class cannot belong to another paulson@6121: class (let alone a set). paulson@6121: paulson@6121: Modern set theorists tend to prefer {\sc zf} because they are mainly concerned paulson@6121: with sets, rather than classes. {\sc bg} requires tiresome proofs that various paulson@6121: collections are sets; for instance, showing $x\in\{x\}$ requires showing that paulson@6121: $x$ is a set. paulson@6121: paulson@6121: paulson@6121: \begin{figure} \small paulson@6121: \begin{center} paulson@6121: \begin{tabular}{rrr} paulson@6121: \it name &\it meta-type & \it description \\ paulson@6121: \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder\\ paulson@6121: \cdx{0} & $i$ & empty set\\ paulson@6121: \cdx{cons} & $[i,i]\To i$ & finite set constructor\\ paulson@6121: \cdx{Upair} & $[i,i]\To i$ & unordered pairing\\ paulson@6121: \cdx{Pair} & $[i,i]\To i$ & ordered pairing\\ paulson@6121: \cdx{Inf} & $i$ & infinite set\\ paulson@6121: \cdx{Pow} & $i\To i$ & powerset\\ paulson@6121: \cdx{Union} \cdx{Inter} & $i\To i$ & set union/intersection \\ paulson@6121: \cdx{split} & $[[i,i]\To i, i] \To i$ & generalized projection\\ paulson@6121: \cdx{fst} \cdx{snd} & $i\To i$ & projections\\ paulson@6121: \cdx{converse}& $i\To i$ & converse of a relation\\ paulson@6121: \cdx{succ} & $i\To i$ & successor\\ paulson@6121: \cdx{Collect} & $[i,i\To o]\To i$ & separation\\ paulson@6121: \cdx{Replace} & $[i, [i,i]\To o] \To i$ & replacement\\ paulson@6121: \cdx{PrimReplace} & $[i, [i,i]\To o] \To i$ & primitive replacement\\ paulson@6121: \cdx{RepFun} & $[i, i\To i] \To i$ & functional replacement\\ paulson@6121: \cdx{Pi} \cdx{Sigma} & $[i,i\To i]\To i$ & general product/sum\\ paulson@6121: \cdx{domain} & $i\To i$ & domain of a relation\\ paulson@6121: \cdx{range} & $i\To i$ & range of a relation\\ paulson@6121: \cdx{field} & $i\To i$ & field of a relation\\ paulson@6121: \cdx{Lambda} & $[i, i\To i]\To i$ & $\lambda$-abstraction\\ paulson@6121: \cdx{restrict}& $[i, i] \To i$ & restriction of a function\\ paulson@6121: \cdx{The} & $[i\To o]\To i$ & definite description\\ paulson@6121: \cdx{if} & $[o,i,i]\To i$ & conditional\\ paulson@6121: \cdx{Ball} \cdx{Bex} & $[i, i\To o]\To o$ & bounded quantifiers paulson@6121: \end{tabular} paulson@6121: \end{center} paulson@6121: \subcaption{Constants} paulson@6121: paulson@6121: \begin{center} paulson@6121: \index{*"`"` symbol} paulson@6121: \index{*"-"`"` symbol} paulson@9836: \index{*"` symbol}\index{function applications} paulson@6121: \index{*"- symbol} paulson@6121: \index{*": symbol} paulson@6121: \index{*"<"= symbol} paulson@6121: \begin{tabular}{rrrr} paulson@6121: \it symbol & \it meta-type & \it priority & \it description \\ paulson@6121: \tt `` & $[i,i]\To i$ & Left 90 & image \\ paulson@6121: \tt -`` & $[i,i]\To i$ & Left 90 & inverse image \\ paulson@6121: \tt ` & $[i,i]\To i$ & Left 90 & application \\ paulson@6121: \sdx{Int} & $[i,i]\To i$ & Left 70 & intersection ($\int$) \\ paulson@6121: \sdx{Un} & $[i,i]\To i$ & Left 65 & union ($\un$) \\ paulson@6121: \tt - & $[i,i]\To i$ & Left 65 & set difference ($-$) \\[1ex] paulson@6121: \tt: & $[i,i]\To o$ & Left 50 & membership ($\in$) \\ paulson@6121: \tt <= & $[i,i]\To o$ & Left 50 & subset ($\subseteq$) paulson@6121: \end{tabular} paulson@6121: \end{center} paulson@6121: \subcaption{Infixes} wenzelm@9695: \caption{Constants of ZF} \label{zf-constants} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \section{The syntax of set theory} paulson@6121: The language of set theory, as studied by logicians, has no constants. The paulson@6121: traditional axioms merely assert the existence of empty sets, unions, paulson@6121: powersets, etc.; this would be intolerable for practical reasoning. The paulson@6121: Isabelle theory declares constants for primitive sets. It also extends paulson@6121: \texttt{FOL} with additional syntax for finite sets, ordered pairs, paulson@6121: comprehension, general union/intersection, general sums/products, and paulson@6121: bounded quantifiers. In most other respects, Isabelle implements precisely paulson@6121: Zermelo-Fraenkel set theory. paulson@6121: wenzelm@9695: Figure~\ref{zf-constants} lists the constants and infixes of~ZF, while paulson@6121: Figure~\ref{zf-trans} presents the syntax translations. Finally, wenzelm@9695: Figure~\ref{zf-syntax} presents the full grammar for set theory, including the wenzelm@9695: constructs of FOL. paulson@6121: paulson@14154: Local abbreviations can be introduced by a \isa{let} construct whose paulson@6121: syntax appears in Fig.\ts\ref{zf-syntax}. Internally it is translated into paulson@6121: the constant~\cdx{Let}. It can be expanded by rewriting with its paulson@6121: definition, \tdx{Let_def}. paulson@6121: paulson@14154: Apart from \isa{let}, set theory does not use polymorphism. All terms in paulson@14154: ZF have type~\tydx{i}, which is the type of individuals and has paulson@14154: class~\cldx{term}. The type of first-order formulae, remember, paulson@14154: is~\tydx{o}. paulson@6121: paulson@6121: Infix operators include binary union and intersection ($A\un B$ and paulson@6121: $A\int B$), set difference ($A-B$), and the subset and membership paulson@14154: relations. Note that $a$\verb|~:|$b$ is translated to $\lnot(a\in b)$, paulson@14154: which is equivalent to $a\notin b$. The paulson@6121: union and intersection operators ($\bigcup A$ and $\bigcap A$) form the paulson@6121: union or intersection of a set of sets; $\bigcup A$ means the same as paulson@6121: $\bigcup@{x\in A}x$. Of these operators, only $\bigcup A$ is primitive. paulson@6121: paulson@14154: The constant \cdx{Upair} constructs unordered pairs; thus \isa{Upair($A$,$B$)} denotes the set~$\{A,B\}$ and paulson@14154: \isa{Upair($A$,$A$)} denotes the singleton~$\{A\}$. General union is paulson@14154: used to define binary union. The Isabelle version goes on to define paulson@14154: the constant paulson@6121: \cdx{cons}: paulson@6121: \begin{eqnarray*} paulson@14154: A\cup B & \equiv & \bigcup(\isa{Upair}(A,B)) \\ paulson@14154: \isa{cons}(a,B) & \equiv & \isa{Upair}(a,a) \un B paulson@6121: \end{eqnarray*} paulson@6121: The $\{a@1, \ldots\}$ notation abbreviates finite sets constructed in the paulson@14154: obvious manner using~\isa{cons} and~$\emptyset$ (the empty set) \isasymin \begin{eqnarray*} paulson@14154: \{a,b,c\} & \equiv & \isa{cons}(a,\isa{cons}(b,\isa{cons}(c,\emptyset))) paulson@6121: \end{eqnarray*} paulson@6121: paulson@14154: The constant \cdx{Pair} constructs ordered pairs, as in \isa{Pair($a$,$b$)}. Ordered pairs may also be written within angle brackets, paulson@6121: as {\tt<$a$,$b$>}. The $n$-tuple {\tt<$a@1$,\ldots,$a@{n-1}$,$a@n$>} paulson@6121: abbreviates the nest of pairs\par\nobreak paulson@14154: \centerline{\isa{Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).}} paulson@6121: wenzelm@9695: In ZF, a function is a set of pairs. A ZF function~$f$ is simply an wenzelm@9695: individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say wenzelm@9695: $i\To i$. The infix operator~{\tt`} denotes the application of a function set wenzelm@9695: to its argument; we must write~$f{\tt`}x$, not~$f(x)$. The syntax for image wenzelm@9695: is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$. paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@9836: \index{lambda abs@$\lambda$-abstractions} paulson@6121: \index{*"-"> symbol} paulson@6121: \index{*"* symbol} paulson@6121: \begin{center} \footnotesize\tt\frenchspacing paulson@6121: \begin{tabular}{rrr} paulson@6121: \it external & \it internal & \it description \\ paulson@6121: $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\ paulson@6121: \ttlbrace$a@1$, $\ldots$, $a@n$\ttrbrace & cons($a@1$,$\ldots$,cons($a@n$,0)) & paulson@6121: \rm finite set \\ paulson@6121: <$a@1$, $\ldots$, $a@{n-1}$, $a@n$> & paulson@6121: Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) & paulson@6121: \rm ordered $n$-tuple \\ paulson@6121: \ttlbrace$x$:$A . P[x]$\ttrbrace & Collect($A$,$\lambda x. P[x]$) & paulson@6121: \rm separation \\ paulson@6121: \ttlbrace$y . x$:$A$, $Q[x,y]$\ttrbrace & Replace($A$,$\lambda x\,y. Q[x,y]$) & paulson@6121: \rm replacement \\ paulson@6121: \ttlbrace$b[x] . x$:$A$\ttrbrace & RepFun($A$,$\lambda x. b[x]$) & paulson@6121: \rm functional replacement \\ paulson@6121: \sdx{INT} $x$:$A . B[x]$ & Inter(\ttlbrace$B[x] . x$:$A$\ttrbrace) & paulson@6121: \rm general intersection \\ paulson@6121: \sdx{UN} $x$:$A . B[x]$ & Union(\ttlbrace$B[x] . x$:$A$\ttrbrace) & paulson@6121: \rm general union \\ paulson@6121: \sdx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x. B[x]$) & paulson@6121: \rm general product \\ paulson@6121: \sdx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x. B[x]$) & paulson@6121: \rm general sum \\ paulson@6121: $A$ -> $B$ & Pi($A$,$\lambda x. B$) & paulson@6121: \rm function space \\ paulson@6121: $A$ * $B$ & Sigma($A$,$\lambda x. B$) & paulson@6121: \rm binary product \\ paulson@6121: \sdx{THE} $x . P[x]$ & The($\lambda x. P[x]$) & paulson@6121: \rm definite description \\ paulson@6121: \sdx{lam} $x$:$A . b[x]$ & Lambda($A$,$\lambda x. b[x]$) & paulson@6121: \rm $\lambda$-abstraction\\[1ex] paulson@6121: \sdx{ALL} $x$:$A . P[x]$ & Ball($A$,$\lambda x. P[x]$) & paulson@6121: \rm bounded $\forall$ \\ paulson@6121: \sdx{EX} $x$:$A . P[x]$ & Bex($A$,$\lambda x. P[x]$) & paulson@6121: \rm bounded $\exists$ paulson@6121: \end{tabular} paulson@6121: \end{center} wenzelm@9695: \caption{Translations for ZF} \label{zf-trans} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@6121: \index{*let symbol} paulson@6121: \index{*in symbol} paulson@6121: \dquotes paulson@6121: \[\begin{array}{rcl} paulson@6121: term & = & \hbox{expression of type~$i$} \\ paulson@6121: & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\ paulson@6121: & | & "if"~term~"then"~term~"else"~term \\ paulson@6121: & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\ paulson@6121: & | & "< " term\; ("," term)^* " >" \\ paulson@6121: & | & "{\ttlbrace} " id ":" term " . " formula " {\ttrbrace}" \\ paulson@6121: & | & "{\ttlbrace} " id " . " id ":" term ", " formula " {\ttrbrace}" \\ paulson@6121: & | & "{\ttlbrace} " term " . " id ":" term " {\ttrbrace}" \\ paulson@6121: & | & term " `` " term \\ paulson@6121: & | & term " -`` " term \\ paulson@6121: & | & term " ` " term \\ paulson@6121: & | & term " * " term \\ paulson@14158: & | & term " \isasyminter " term \\ paulson@14154: & | & term " \isasymunion " term \\ paulson@6121: & | & term " - " term \\ paulson@6121: & | & term " -> " term \\ paulson@6121: & | & "THE~~" id " . " formula\\ paulson@6121: & | & "lam~~" id ":" term " . " term \\ paulson@6121: & | & "INT~~" id ":" term " . " term \\ paulson@6121: & | & "UN~~~" id ":" term " . " term \\ paulson@6121: & | & "PROD~" id ":" term " . " term \\ paulson@6121: & | & "SUM~~" id ":" term " . " term \\[2ex] paulson@6121: formula & = & \hbox{expression of type~$o$} \\ paulson@6121: & | & term " : " term \\ paulson@6121: & | & term " \ttilde: " term \\ paulson@6121: & | & term " <= " term \\ paulson@6121: & | & term " = " term \\ paulson@6121: & | & term " \ttilde= " term \\ paulson@6121: & | & "\ttilde\ " formula \\ paulson@6121: & | & formula " \& " formula \\ paulson@6121: & | & formula " | " formula \\ paulson@6121: & | & formula " --> " formula \\ paulson@6121: & | & formula " <-> " formula \\ paulson@6121: & | & "ALL " id ":" term " . " formula \\ paulson@6121: & | & "EX~~" id ":" term " . " formula \\ paulson@6121: & | & "ALL~" id~id^* " . " formula \\ paulson@6121: & | & "EX~~" id~id^* " . " formula \\ paulson@6121: & | & "EX!~" id~id^* " . " formula paulson@6121: \end{array} paulson@6121: \] wenzelm@9695: \caption{Full grammar for ZF} \label{zf-syntax} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \section{Binding operators} paulson@6121: The constant \cdx{Collect} constructs sets by the principle of {\bf paulson@6121: separation}. The syntax for separation is paulson@6121: \hbox{\tt\ttlbrace$x$:$A$.\ $P[x]$\ttrbrace}, where $P[x]$ is a formula paulson@14154: that may contain free occurrences of~$x$. It abbreviates the set \isa{Collect($A$,$\lambda x. P[x]$)}, which consists of all $x\in A$ that paulson@14154: satisfy~$P[x]$. Note that \isa{Collect} is an unfortunate choice of paulson@6121: name: some set theories adopt a set-formation principle, related to paulson@6121: replacement, called collection. paulson@6121: paulson@6121: The constant \cdx{Replace} constructs sets by the principle of {\bf paulson@6121: replacement}. The syntax paulson@14154: \hbox{\tt\ttlbrace$y$.\ $x$:$A$,$Q[x,y]$\ttrbrace} denotes the set paulson@14154: \isa{Replace($A$,$\lambda x\,y. Q[x,y]$)}, which consists of all~$y$ such paulson@6121: that there exists $x\in A$ satisfying~$Q[x,y]$. The Replacement Axiom paulson@6121: has the condition that $Q$ must be single-valued over~$A$: for paulson@6121: all~$x\in A$ there exists at most one $y$ satisfying~$Q[x,y]$. A paulson@6121: single-valued binary predicate is also called a {\bf class function}. paulson@6121: paulson@6121: The constant \cdx{RepFun} expresses a special case of replacement, paulson@6121: where $Q[x,y]$ has the form $y=b[x]$. Such a $Q$ is trivially paulson@6121: single-valued, since it is just the graph of the meta-level paulson@6121: function~$\lambda x. b[x]$. The resulting set consists of all $b[x]$ paulson@14154: for~$x\in A$. This is analogous to the \ML{} functional \isa{map}, paulson@6121: since it applies a function to every element of a set. The syntax is paulson@14154: \isa{\ttlbrace$b[x]$.\ $x$:$A$\ttrbrace}, which expands to paulson@14154: \isa{RepFun($A$,$\lambda x. b[x]$)}. paulson@6121: paulson@6121: \index{*INT symbol}\index{*UN symbol} paulson@6121: General unions and intersections of indexed paulson@6121: families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$, paulson@14154: are written \isa{UN $x$:$A$.\ $B[x]$} and \isa{INT $x$:$A$.\ $B[x]$}. paulson@14154: Their meaning is expressed using \isa{RepFun} as paulson@6121: \[ paulson@6121: \bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad paulson@6121: \bigcap(\{B[x]. x\in A\}). paulson@6121: \] paulson@6121: General sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$ can be paulson@6121: constructed in set theory, where $B[x]$ is a family of sets over~$A$. They paulson@6121: have as special cases $A\times B$ and $A\to B$, where $B$ is simply a set. paulson@6121: This is similar to the situation in Constructive Type Theory (set theory paulson@6121: has `dependent sets') and calls for similar syntactic conventions. The paulson@6121: constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and paulson@14154: products. Instead of \isa{Sigma($A$,$B$)} and \isa{Pi($A$,$B$)} we may paulson@6121: write paulson@14154: \isa{SUM $x$:$A$.\ $B[x]$} and \isa{PROD $x$:$A$.\ $B[x]$}. paulson@6121: \index{*SUM symbol}\index{*PROD symbol}% paulson@6121: The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$->$B$} abbreviate paulson@6121: general sums and products over a constant family.\footnote{Unlike normal paulson@6121: infix operators, {\tt*} and {\tt->} merely define abbreviations; there are paulson@14154: no constants~\isa{op~*} and~\isa{op~->}.} Isabelle accepts these paulson@6121: abbreviations in parsing and uses them whenever possible for printing. paulson@6121: wenzelm@9695: \index{*THE symbol} As mentioned above, whenever the axioms assert the wenzelm@9695: existence and uniqueness of a set, Isabelle's set theory declares a constant wenzelm@9695: for that set. These constants can express the {\bf definite description} wenzelm@9695: operator~$\iota x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, wenzelm@9695: if such exists. Since all terms in ZF denote something, a description is wenzelm@9695: always meaningful, but we do not know its value unless $P[x]$ defines it paulson@14154: uniquely. Using the constant~\cdx{The}, we may write descriptions as paulson@14154: \isa{The($\lambda x. P[x]$)} or use the syntax \isa{THE $x$.\ $P[x]$}. paulson@6121: paulson@6121: \index{*lam symbol} paulson@6121: Function sets may be written in $\lambda$-notation; $\lambda x\in A. b[x]$ paulson@6121: stands for the set of all pairs $\pair{x,b[x]}$ for $x\in A$. In order for paulson@6121: this to be a set, the function's domain~$A$ must be given. Using the paulson@14154: constant~\cdx{Lambda}, we may express function sets as \isa{Lambda($A$,$\lambda x. b[x]$)} or use the syntax \isa{lam $x$:$A$.\ $b[x]$}. paulson@6121: paulson@6121: Isabelle's set theory defines two {\bf bounded quantifiers}: paulson@6121: \begin{eqnarray*} paulson@6121: \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ paulson@6121: \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] paulson@6121: \end{eqnarray*} paulson@6121: The constants~\cdx{Ball} and~\cdx{Bex} are defined paulson@14154: accordingly. Instead of \isa{Ball($A$,$P$)} and \isa{Bex($A$,$P$)} we may paulson@6121: write paulson@14154: \isa{ALL $x$:$A$.\ $P[x]$} and \isa{EX $x$:$A$.\ $P[x]$}. paulson@6121: paulson@6121: paulson@6121: %%%% ZF.thy paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{Let_def}: Let(s, f) == f(s) paulson@14154: paulson@14154: \tdx{Ball_def}: Ball(A,P) == {\isasymforall}x. x \isasymin A --> P(x) paulson@14154: \tdx{Bex_def}: Bex(A,P) == {\isasymexists}x. x \isasymin A & P(x) paulson@14154: paulson@14154: \tdx{subset_def}: A \isasymsubseteq B == {\isasymforall}x \isasymin A. x \isasymin B paulson@14154: \tdx{extension}: A = B <-> A \isasymsubseteq B & B \isasymsubseteq A paulson@14154: paulson@14154: \tdx{Union_iff}: A \isasymin Union(C) <-> ({\isasymexists}B \isasymin C. A \isasymin B) paulson@14154: \tdx{Pow_iff}: A \isasymin Pow(B) <-> A \isasymsubseteq B paulson@14154: \tdx{foundation}: A=0 | ({\isasymexists}x \isasymin A. {\isasymforall}y \isasymin x. y \isasymnotin A) paulson@14154: paulson@14154: \tdx{replacement}: ({\isasymforall}x \isasymin A. {\isasymforall}y z. P(x,y) & P(x,z) --> y=z) ==> paulson@14154: b \isasymin PrimReplace(A,P) <-> ({\isasymexists}x{\isasymin}A. P(x,b)) paulson@6121: \subcaption{The Zermelo-Fraenkel Axioms} paulson@6121: paulson@14154: \tdx{Replace_def}: Replace(A,P) == paulson@14154: PrimReplace(A, \%x y. (\isasymexists!z. P(x,z)) & P(x,y)) paulson@14154: \tdx{RepFun_def}: RepFun(A,f) == {\ttlbrace}y . x \isasymin A, y=f(x)\ttrbrace paulson@14154: \tdx{the_def}: The(P) == Union({\ttlbrace}y . x \isasymin {\ttlbrace}0{\ttrbrace}, P(y){\ttrbrace}) paulson@14154: \tdx{if_def}: if(P,a,b) == THE z. P & z=a | ~P & z=b paulson@14154: \tdx{Collect_def}: Collect(A,P) == {\ttlbrace}y . x \isasymin A, x=y & P(x){\ttrbrace} paulson@14154: \tdx{Upair_def}: Upair(a,b) == paulson@14154: {\ttlbrace}y. x\isasymin{}Pow(Pow(0)), x=0 & y=a | x=Pow(0) & y=b{\ttrbrace} paulson@6121: \subcaption{Consequences of replacement} paulson@6121: paulson@14154: \tdx{Inter_def}: Inter(A) == {\ttlbrace}x \isasymin Union(A) . {\isasymforall}y \isasymin A. x \isasymin y{\ttrbrace} paulson@14154: \tdx{Un_def}: A \isasymunion B == Union(Upair(A,B)) paulson@14158: \tdx{Int_def}: A \isasyminter B == Inter(Upair(A,B)) paulson@14154: \tdx{Diff_def}: A - B == {\ttlbrace}x \isasymin A . x \isasymnotin B{\ttrbrace} paulson@6121: \subcaption{Union, intersection, difference} paulson@14154: \end{alltt*} wenzelm@9695: \caption{Rules and axioms of ZF} \label{zf-rules} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{cons_def}: cons(a,A) == Upair(a,a) \isasymunion A paulson@14154: \tdx{succ_def}: succ(i) == cons(i,i) paulson@14154: \tdx{infinity}: 0 \isasymin Inf & ({\isasymforall}y \isasymin Inf. succ(y) \isasymin Inf) paulson@6121: \subcaption{Finite and infinite sets} paulson@6121: paulson@14154: \tdx{Pair_def}: == {\ttlbrace}{\ttlbrace}a,a{\ttrbrace}, {\ttlbrace}a,b{\ttrbrace}{\ttrbrace} paulson@14154: \tdx{split_def}: split(c,p) == THE y. {\isasymexists}a b. p= & y=c(a,b) paulson@14154: \tdx{fst_def}: fst(A) == split(\%x y. x, p) paulson@14154: \tdx{snd_def}: snd(A) == split(\%x y. y, p) paulson@14154: \tdx{Sigma_def}: Sigma(A,B) == {\isasymUnion}x \isasymin A. {\isasymUnion}y \isasymin B(x). {\ttlbrace}{\ttrbrace} paulson@6121: \subcaption{Ordered pairs and Cartesian products} paulson@6121: paulson@14154: \tdx{converse_def}: converse(r) == {\ttlbrace}z. w\isasymin{}r, {\isasymexists}x y. w= & z={\ttrbrace} paulson@14154: \tdx{domain_def}: domain(r) == {\ttlbrace}x. w \isasymin r, {\isasymexists}y. w={\ttrbrace} paulson@14154: \tdx{range_def}: range(r) == domain(converse(r)) paulson@14154: \tdx{field_def}: field(r) == domain(r) \isasymunion range(r) paulson@14154: \tdx{image_def}: r `` A == {\ttlbrace}y\isasymin{}range(r) . {\isasymexists}x \isasymin A. \isasymin r{\ttrbrace} paulson@14154: \tdx{vimage_def}: r -`` A == converse(r)``A paulson@6121: \subcaption{Operations on relations} paulson@6121: paulson@14154: \tdx{lam_def}: Lambda(A,b) == {\ttlbrace} . x \isasymin A{\ttrbrace} paulson@14154: \tdx{apply_def}: f`a == THE y. \isasymin f paulson@14154: \tdx{Pi_def}: Pi(A,B) == {\ttlbrace}f\isasymin{}Pow(Sigma(A,B)). {\isasymforall}x\isasymin{}A. \isasymexists!y. \isasymin{}f{\ttrbrace} paulson@14154: \tdx{restrict_def}: restrict(f,A) == lam x \isasymin A. f`x paulson@6121: \subcaption{Functions and general product} paulson@14154: \end{alltt*} wenzelm@9695: \caption{Further definitions of ZF} \label{zf-defs} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: paulson@6121: \section{The Zermelo-Fraenkel axioms} paulson@6121: The axioms appear in Fig.\ts \ref{zf-rules}. They resemble those paulson@6121: presented by Suppes~\cite{suppes72}. Most of the theory consists of paulson@6121: definitions. In particular, bounded quantifiers and the subset relation paulson@6121: appear in other axioms. Object-level quantifiers and implications have paulson@6121: been replaced by meta-level ones wherever possible, to simplify use of the paulson@14154: axioms. paulson@6121: paulson@6121: The traditional replacement axiom asserts paulson@14154: \[ y \in \isa{PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \] paulson@6121: subject to the condition that $P(x,y)$ is single-valued for all~$x\in A$. paulson@6121: The Isabelle theory defines \cdx{Replace} to apply paulson@6121: \cdx{PrimReplace} to the single-valued part of~$P$, namely paulson@6121: \[ (\exists!z. P(x,z)) \conj P(x,y). \] paulson@14154: Thus $y\in \isa{Replace}(A,P)$ if and only if there is some~$x$ such that paulson@6121: $P(x,-)$ holds uniquely for~$y$. Because the equivalence is unconditional, paulson@14154: \isa{Replace} is much easier to use than \isa{PrimReplace}; it defines the paulson@6121: same set, if $P(x,y)$ is single-valued. The nice syntax for replacement paulson@14154: expands to \isa{Replace}. paulson@6121: paulson@14158: Other consequences of replacement include replacement for paulson@14158: meta-level functions paulson@6121: (\cdx{RepFun}) and definite descriptions (\cdx{The}). paulson@6121: Axioms for separation (\cdx{Collect}) and unordered pairs paulson@6121: (\cdx{Upair}) are traditionally assumed, but they actually follow paulson@6121: from replacement~\cite[pages 237--8]{suppes72}. paulson@6121: paulson@6121: The definitions of general intersection, etc., are straightforward. Note paulson@14154: the definition of \isa{cons}, which underlies the finite set notation. paulson@6121: The axiom of infinity gives us a set that contains~0 and is closed under paulson@6121: successor (\cdx{succ}). Although this set is not uniquely defined, paulson@6121: the theory names it (\cdx{Inf}) in order to simplify the paulson@6121: construction of the natural numbers. paulson@6121: paulson@6121: Further definitions appear in Fig.\ts\ref{zf-defs}. Ordered pairs are paulson@6121: defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$. Recall paulson@6121: that \cdx{Sigma}$(A,B)$ generalizes the Cartesian product of two paulson@6121: sets. It is defined to be the union of all singleton sets paulson@6121: $\{\pair{x,y}\}$, for $x\in A$ and $y\in B(x)$. This is a typical usage of paulson@6121: general union. paulson@6121: paulson@6121: The projections \cdx{fst} and~\cdx{snd} are defined in terms of the paulson@6121: generalized projection \cdx{split}. The latter has been borrowed from paulson@6121: Martin-L\"of's Type Theory, and is often easier to use than \cdx{fst} paulson@6121: and~\cdx{snd}. paulson@6121: paulson@6121: Operations on relations include converse, domain, range, and image. The paulson@14154: set $\isa{Pi}(A,B)$ generalizes the space of functions between two sets. paulson@6121: Note the simple definitions of $\lambda$-abstraction (using paulson@6121: \cdx{RepFun}) and application (using a definite description). The paulson@6121: function \cdx{restrict}$(f,A)$ has the same values as~$f$, but only paulson@6121: over the domain~$A$. paulson@6121: paulson@6121: paulson@14154: %%%% zf.thy paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{ballI}: [| !!x. x\isasymin{}A ==> P(x) |] ==> {\isasymforall}x\isasymin{}A. P(x) paulson@14154: \tdx{bspec}: [| {\isasymforall}x\isasymin{}A. P(x); x\isasymin{}A |] ==> P(x) paulson@14154: \tdx{ballE}: [| {\isasymforall}x\isasymin{}A. P(x); P(x) ==> Q; x \isasymnotin A ==> Q |] ==> Q paulson@14154: paulson@14154: \tdx{ball_cong}: [| A=A'; !!x. x\isasymin{}A' ==> P(x) <-> P'(x) |] ==> paulson@14154: ({\isasymforall}x\isasymin{}A. P(x)) <-> ({\isasymforall}x\isasymin{}A'. P'(x)) paulson@14154: paulson@14154: \tdx{bexI}: [| P(x); x\isasymin{}A |] ==> {\isasymexists}x\isasymin{}A. P(x) paulson@14154: \tdx{bexCI}: [| {\isasymforall}x\isasymin{}A. ~P(x) ==> P(a); a\isasymin{}A |] ==> {\isasymexists}x\isasymin{}A. P(x) paulson@14154: \tdx{bexE}: [| {\isasymexists}x\isasymin{}A. P(x); !!x. [| x\isasymin{}A; P(x) |] ==> Q |] ==> Q paulson@14154: paulson@14154: \tdx{bex_cong}: [| A=A'; !!x. x\isasymin{}A' ==> P(x) <-> P'(x) |] ==> paulson@14154: ({\isasymexists}x\isasymin{}A. P(x)) <-> ({\isasymexists}x\isasymin{}A'. P'(x)) paulson@6121: \subcaption{Bounded quantifiers} paulson@6121: paulson@14154: \tdx{subsetI}: (!!x. x \isasymin A ==> x \isasymin B) ==> A \isasymsubseteq B paulson@14154: \tdx{subsetD}: [| A \isasymsubseteq B; c \isasymin A |] ==> c \isasymin B paulson@14154: \tdx{subsetCE}: [| A \isasymsubseteq B; c \isasymnotin A ==> P; c \isasymin B ==> P |] ==> P paulson@14154: \tdx{subset_refl}: A \isasymsubseteq A paulson@14154: \tdx{subset_trans}: [| A \isasymsubseteq B; B \isasymsubseteq C |] ==> A \isasymsubseteq C paulson@14154: paulson@14154: \tdx{equalityI}: [| A \isasymsubseteq B; B \isasymsubseteq A |] ==> A = B paulson@14154: \tdx{equalityD1}: A = B ==> A \isasymsubseteq B paulson@14154: \tdx{equalityD2}: A = B ==> B \isasymsubseteq A paulson@14154: \tdx{equalityE}: [| A = B; [| A \isasymsubseteq B; B \isasymsubseteq A |] ==> P |] ==> P paulson@6121: \subcaption{Subsets and extensionality} paulson@6121: paulson@14154: \tdx{emptyE}: a \isasymin 0 ==> P paulson@14154: \tdx{empty_subsetI}: 0 \isasymsubseteq A paulson@14154: \tdx{equals0I}: [| !!y. y \isasymin A ==> False |] ==> A=0 paulson@14154: \tdx{equals0D}: [| A=0; a \isasymin A |] ==> P paulson@14154: paulson@14154: \tdx{PowI}: A \isasymsubseteq B ==> A \isasymin Pow(B) paulson@14154: \tdx{PowD}: A \isasymin Pow(B) ==> A \isasymsubseteq B paulson@6121: \subcaption{The empty set; power sets} paulson@14154: \end{alltt*} wenzelm@9695: \caption{Basic derived rules for ZF} \label{zf-lemmas1} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \section{From basic lemmas to function spaces} paulson@6121: Faced with so many definitions, it is essential to prove lemmas. Even paulson@6121: trivial theorems like $A \int B = B \int A$ would be difficult to paulson@6121: prove from the definitions alone. Isabelle's set theory derives many paulson@6121: rules using a natural deduction style. Ideally, a natural deduction paulson@6121: rule should introduce or eliminate just one operator, but this is not paulson@6121: always practical. For most operators, we may forget its definition paulson@6121: and use its derived rules instead. paulson@6121: paulson@6121: \subsection{Fundamental lemmas} paulson@6121: Figure~\ref{zf-lemmas1} presents the derived rules for the most basic paulson@6121: operators. The rules for the bounded quantifiers resemble those for the paulson@6121: ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption paulson@6121: in the style of Isabelle's classical reasoner. The \rmindex{congruence paulson@6121: rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's paulson@6121: simplifier, but have few other uses. Congruence rules must be specially paulson@6121: derived for all binding operators, and henceforth will not be shown. paulson@6121: paulson@6121: Figure~\ref{zf-lemmas1} also shows rules for the subset and equality paulson@6121: relations (proof by extensionality), and rules about the empty set and the paulson@6121: power set operator. paulson@6121: paulson@6121: Figure~\ref{zf-lemmas2} presents rules for replacement and separation. paulson@6121: The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than paulson@14154: comparable rules for \isa{PrimReplace} would be. The principle of paulson@6121: separation is proved explicitly, although most proofs should use the paulson@14154: natural deduction rules for \isa{Collect}. The elimination rule paulson@6121: \tdx{CollectE} is equivalent to the two destruction rules paulson@6121: \tdx{CollectD1} and \tdx{CollectD2}, but each rule is suited to paulson@6121: particular circumstances. Although too many rules can be confusing, there paulson@14154: is no reason to aim for a minimal set of rules. paulson@6121: paulson@6121: Figure~\ref{zf-lemmas3} presents rules for general union and intersection. paulson@6121: The empty intersection should be undefined. We cannot have paulson@6121: $\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set. All wenzelm@9695: expressions denote something in ZF set theory; the definition of paulson@6121: intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is paulson@6121: arbitrary. The rule \tdx{InterI} must have a premise to exclude paulson@6121: the empty intersection. Some of the laws governing intersections require paulson@6121: similar premises. paulson@6121: paulson@6121: paulson@6121: %the [p] gives better page breaking for the book paulson@6121: \begin{figure}[p] paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{ReplaceI}: [| x\isasymin{}A; P(x,b); !!y. P(x,y) ==> y=b |] ==> paulson@14154: b\isasymin{}{\ttlbrace}y. x\isasymin{}A, P(x,y){\ttrbrace} paulson@14154: paulson@14154: \tdx{ReplaceE}: [| b\isasymin{}{\ttlbrace}y. x\isasymin{}A, P(x,y){\ttrbrace}; paulson@14154: !!x. [| x\isasymin{}A; P(x,b); {\isasymforall}y. P(x,y)-->y=b |] ==> R paulson@14154: |] ==> R paulson@14154: paulson@14154: \tdx{RepFunI}: [| a\isasymin{}A |] ==> f(a)\isasymin{}{\ttlbrace}f(x). x\isasymin{}A{\ttrbrace} paulson@14154: \tdx{RepFunE}: [| b\isasymin{}{\ttlbrace}f(x). x\isasymin{}A{\ttrbrace}; paulson@14154: !!x.[| x\isasymin{}A; b=f(x) |] ==> P |] ==> P paulson@14154: paulson@14154: \tdx{separation}: a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} <-> a\isasymin{}A & P(a) paulson@14154: \tdx{CollectI}: [| a\isasymin{}A; P(a) |] ==> a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} paulson@14154: \tdx{CollectE}: [| a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace}; [| a\isasymin{}A; P(a) |] ==> R |] ==> R paulson@14154: \tdx{CollectD1}: a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} ==> a\isasymin{}A paulson@14154: \tdx{CollectD2}: a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} ==> P(a) paulson@14154: \end{alltt*} paulson@6121: \caption{Replacement and separation} \label{zf-lemmas2} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{UnionI}: [| B\isasymin{}C; A\isasymin{}B |] ==> A\isasymin{}Union(C) paulson@14154: \tdx{UnionE}: [| A\isasymin{}Union(C); !!B.[| A\isasymin{}B; B\isasymin{}C |] ==> R |] ==> R paulson@14154: paulson@14154: \tdx{InterI}: [| !!x. x\isasymin{}C ==> A\isasymin{}x; c\isasymin{}C |] ==> A\isasymin{}Inter(C) paulson@14154: \tdx{InterD}: [| A\isasymin{}Inter(C); B\isasymin{}C |] ==> A\isasymin{}B paulson@14154: \tdx{InterE}: [| A\isasymin{}Inter(C); A\isasymin{}B ==> R; B \isasymnotin C ==> R |] ==> R paulson@14154: paulson@14154: \tdx{UN_I}: [| a\isasymin{}A; b\isasymin{}B(a) |] ==> b\isasymin{}({\isasymUnion}x\isasymin{}A. B(x)) paulson@14154: \tdx{UN_E}: [| b\isasymin{}({\isasymUnion}x\isasymin{}A. B(x)); !!x.[| x\isasymin{}A; b\isasymin{}B(x) |] ==> R paulson@14154: |] ==> R paulson@14154: paulson@14154: \tdx{INT_I}: [| !!x. x\isasymin{}A ==> b\isasymin{}B(x); a\isasymin{}A |] ==> b\isasymin{}({\isasymInter}x\isasymin{}A. B(x)) paulson@14154: \tdx{INT_E}: [| b\isasymin{}({\isasymInter}x\isasymin{}A. B(x)); a\isasymin{}A |] ==> b\isasymin{}B(a) paulson@14154: \end{alltt*} paulson@6121: \caption{General union and intersection} \label{zf-lemmas3} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@14154: %%% upair.thy paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{pairing}: a\isasymin{}Upair(b,c) <-> (a=b | a=c) paulson@14154: \tdx{UpairI1}: a\isasymin{}Upair(a,b) paulson@14154: \tdx{UpairI2}: b\isasymin{}Upair(a,b) paulson@14154: \tdx{UpairE}: [| a\isasymin{}Upair(b,c); a=b ==> P; a=c ==> P |] ==> P paulson@14154: \end{alltt*} paulson@6121: \caption{Unordered pairs} \label{zf-upair1} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{UnI1}: c\isasymin{}A ==> c\isasymin{}A \isasymunion B paulson@14154: \tdx{UnI2}: c\isasymin{}B ==> c\isasymin{}A \isasymunion B paulson@14154: \tdx{UnCI}: (c \isasymnotin B ==> c\isasymin{}A) ==> c\isasymin{}A \isasymunion B paulson@14154: \tdx{UnE}: [| c\isasymin{}A \isasymunion B; c\isasymin{}A ==> P; c\isasymin{}B ==> P |] ==> P paulson@14154: paulson@14158: \tdx{IntI}: [| c\isasymin{}A; c\isasymin{}B |] ==> c\isasymin{}A \isasyminter B paulson@14158: \tdx{IntD1}: c\isasymin{}A \isasyminter B ==> c\isasymin{}A paulson@14158: \tdx{IntD2}: c\isasymin{}A \isasyminter B ==> c\isasymin{}B paulson@14158: \tdx{IntE}: [| c\isasymin{}A \isasyminter B; [| c\isasymin{}A; c\isasymin{}B |] ==> P |] ==> P paulson@14154: paulson@14154: \tdx{DiffI}: [| c\isasymin{}A; c \isasymnotin B |] ==> c\isasymin{}A - B paulson@14154: \tdx{DiffD1}: c\isasymin{}A - B ==> c\isasymin{}A paulson@14154: \tdx{DiffD2}: c\isasymin{}A - B ==> c \isasymnotin B paulson@14154: \tdx{DiffE}: [| c\isasymin{}A - B; [| c\isasymin{}A; c \isasymnotin B |] ==> P |] ==> P paulson@14154: \end{alltt*} paulson@6121: \caption{Union, intersection, difference} \label{zf-Un} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{consI1}: a\isasymin{}cons(a,B) paulson@14154: \tdx{consI2}: a\isasymin{}B ==> a\isasymin{}cons(b,B) paulson@14154: \tdx{consCI}: (a \isasymnotin B ==> a=b) ==> a\isasymin{}cons(b,B) paulson@14154: \tdx{consE}: [| a\isasymin{}cons(b,A); a=b ==> P; a\isasymin{}A ==> P |] ==> P paulson@14154: paulson@14154: \tdx{singletonI}: a\isasymin{}{\ttlbrace}a{\ttrbrace} paulson@14154: \tdx{singletonE}: [| a\isasymin{}{\ttlbrace}b{\ttrbrace}; a=b ==> P |] ==> P paulson@14154: \end{alltt*} paulson@6121: \caption{Finite and singleton sets} \label{zf-upair2} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{succI1}: i\isasymin{}succ(i) paulson@14154: \tdx{succI2}: i\isasymin{}j ==> i\isasymin{}succ(j) paulson@14154: \tdx{succCI}: (i \isasymnotin j ==> i=j) ==> i\isasymin{}succ(j) paulson@14154: \tdx{succE}: [| i\isasymin{}succ(j); i=j ==> P; i\isasymin{}j ==> P |] ==> P paulson@14154: \tdx{succ_neq_0}: [| succ(n)=0 |] ==> P paulson@14154: \tdx{succ_inject}: succ(m) = succ(n) ==> m=n paulson@14154: \end{alltt*} paulson@6121: \caption{The successor function} \label{zf-succ} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{the_equality}: [| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x))=a paulson@14154: \tdx{theI}: \isasymexists! x. P(x) ==> P(THE x. P(x)) paulson@14154: paulson@14154: \tdx{if_P}: P ==> (if P then a else b) = a paulson@14154: \tdx{if_not_P}: ~P ==> (if P then a else b) = b paulson@14154: paulson@14154: \tdx{mem_asym}: [| a\isasymin{}b; b\isasymin{}a |] ==> P paulson@14154: \tdx{mem_irrefl}: a\isasymin{}a ==> P paulson@14154: \end{alltt*} paulson@6121: \caption{Descriptions; non-circularity} \label{zf-the} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \subsection{Unordered pairs and finite sets} paulson@6121: Figure~\ref{zf-upair1} presents the principle of unordered pairing, along paulson@6121: with its derived rules. Binary union and intersection are defined in terms paulson@6121: of ordered pairs (Fig.\ts\ref{zf-Un}). Set difference is also included. The paulson@6121: rule \tdx{UnCI} is useful for classical reasoning about unions, paulson@14154: like \isa{disjCI}\@; it supersedes \tdx{UnI1} and paulson@6121: \tdx{UnI2}, but these rules are often easier to work with. For paulson@6121: intersection and difference we have both elimination and destruction rules. paulson@6121: Again, there is no reason to provide a minimal rule set. paulson@6121: paulson@6121: Figure~\ref{zf-upair2} is concerned with finite sets: it presents rules paulson@14154: for~\isa{cons}, the finite set constructor, and rules for singleton paulson@6121: sets. Figure~\ref{zf-succ} presents derived rules for the successor paulson@14154: function, which is defined in terms of~\isa{cons}. The proof that paulson@14154: \isa{succ} is injective appears to require the Axiom of Foundation. paulson@6121: paulson@6121: Definite descriptions (\sdx{THE}) are defined in terms of the singleton paulson@6121: set~$\{0\}$, but their derived rules fortunately hide this paulson@6121: (Fig.\ts\ref{zf-the}). The rule~\tdx{theI} is difficult to apply paulson@6121: because of the two occurrences of~$\Var{P}$. However, paulson@6121: \tdx{the_equality} does not have this problem and the files contain paulson@6121: many examples of its use. paulson@6121: paulson@6121: Finally, the impossibility of having both $a\in b$ and $b\in a$ paulson@6121: (\tdx{mem_asym}) is proved by applying the Axiom of Foundation to paulson@6121: the set $\{a,b\}$. The impossibility of $a\in a$ is a trivial consequence. paulson@6121: paulson@14154: paulson@14154: %%% subset.thy? paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{Union_upper}: B\isasymin{}A ==> B \isasymsubseteq Union(A) paulson@14154: \tdx{Union_least}: [| !!x. x\isasymin{}A ==> x \isasymsubseteq C |] ==> Union(A) \isasymsubseteq C paulson@14154: paulson@14154: \tdx{Inter_lower}: B\isasymin{}A ==> Inter(A) \isasymsubseteq B paulson@14154: \tdx{Inter_greatest}: [| a\isasymin{}A; !!x. x\isasymin{}A ==> C \isasymsubseteq x |] ==> C\isasymsubseteq{}Inter(A) paulson@14154: paulson@14154: \tdx{Un_upper1}: A \isasymsubseteq A \isasymunion B paulson@14154: \tdx{Un_upper2}: B \isasymsubseteq A \isasymunion B paulson@14154: \tdx{Un_least}: [| A \isasymsubseteq C; B \isasymsubseteq C |] ==> A \isasymunion B \isasymsubseteq C paulson@14154: paulson@14158: \tdx{Int_lower1}: A \isasyminter B \isasymsubseteq A paulson@14158: \tdx{Int_lower2}: A \isasyminter B \isasymsubseteq B paulson@14158: \tdx{Int_greatest}: [| C \isasymsubseteq A; C \isasymsubseteq B |] ==> C \isasymsubseteq A \isasyminter B paulson@14154: paulson@14154: \tdx{Diff_subset}: A-B \isasymsubseteq A paulson@14158: \tdx{Diff_contains}: [| C \isasymsubseteq A; C \isasyminter B = 0 |] ==> C \isasymsubseteq A-B paulson@14154: paulson@14154: \tdx{Collect_subset}: Collect(A,P) \isasymsubseteq A paulson@14154: \end{alltt*} paulson@6121: \caption{Subset and lattice properties} \label{zf-subset} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \subsection{Subset and lattice properties} paulson@6121: The subset relation is a complete lattice. Unions form least upper bounds; paulson@6121: non-empty intersections form greatest lower bounds. Figure~\ref{zf-subset} paulson@6121: shows the corresponding rules. A few other laws involving subsets are paulson@14154: included. paulson@6121: Reasoning directly about subsets often yields clearer proofs than paulson@6121: reasoning about the membership relation. Section~\ref{sec:ZF-pow-example} paulson@14154: below presents an example of this, proving the equation paulson@14154: ${\isa{Pow}(A)\cap \isa{Pow}(B)}= \isa{Pow}(A\cap B)$. paulson@14154: paulson@14154: %%% pair.thy paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{Pair_inject1}: = ==> a=c paulson@14154: \tdx{Pair_inject2}: = ==> b=d paulson@14154: \tdx{Pair_inject}: [| = ; [| a=c; b=d |] ==> P |] ==> P paulson@14154: \tdx{Pair_neq_0}: =0 ==> P paulson@14154: paulson@14154: \tdx{fst_conv}: fst() = a paulson@14154: \tdx{snd_conv}: snd() = b paulson@14154: \tdx{split}: split(\%x y. c(x,y), ) = c(a,b) paulson@14154: paulson@14154: \tdx{SigmaI}: [| a\isasymin{}A; b\isasymin{}B(a) |] ==> \isasymin{}Sigma(A,B) paulson@14154: paulson@14154: \tdx{SigmaE}: [| c\isasymin{}Sigma(A,B); paulson@14154: !!x y.[| x\isasymin{}A; y\isasymin{}B(x); c= |] ==> P |] ==> P paulson@14154: paulson@14154: \tdx{SigmaE2}: [| \isasymin{}Sigma(A,B); paulson@14154: [| a\isasymin{}A; b\isasymin{}B(a) |] ==> P |] ==> P paulson@14154: \end{alltt*} paulson@6121: \caption{Ordered pairs; projections; general sums} \label{zf-pair} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \subsection{Ordered pairs} \label{sec:pairs} paulson@6121: paulson@6121: Figure~\ref{zf-pair} presents the rules governing ordered pairs, paulson@14154: projections and general sums --- in particular, that paulson@14154: $\{\{a\},\{a,b\}\}$ functions as an ordered pair. This property is paulson@14154: expressed as two destruction rules, paulson@6121: \tdx{Pair_inject1} and \tdx{Pair_inject2}, and equivalently paulson@6121: as the elimination rule \tdx{Pair_inject}. paulson@6121: paulson@6121: The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$. This paulson@6121: is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other paulson@6121: encodings of ordered pairs. The non-standard ordered pairs mentioned below paulson@6121: satisfy $\pair{\emptyset;\emptyset}=\emptyset$. paulson@6121: paulson@6121: The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE} paulson@6121: assert that \cdx{Sigma}$(A,B)$ consists of all pairs of the form paulson@6121: $\pair{x,y}$, for $x\in A$ and $y\in B(x)$. The rule \tdx{SigmaE2} paulson@14154: merely states that $\pair{a,b}\in \isa{Sigma}(A,B)$ implies $a\in A$ and paulson@6121: $b\in B(a)$. paulson@6121: paulson@6121: In addition, it is possible to use tuples as patterns in abstractions: paulson@6121: \begin{center} paulson@14154: {\tt\%<$x$,$y$>. $t$} \quad stands for\quad \isa{split(\%$x$ $y$.\ $t$)} paulson@6121: \end{center} paulson@6121: Nested patterns are translated recursively: paulson@6121: {\tt\%<$x$,$y$,$z$>. $t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>. $t$} $\leadsto$ paulson@14154: \isa{split(\%$x$.\%<$y$,$z$>. $t$)} $\leadsto$ \isa{split(\%$x$. split(\%$y$ paulson@6121: $z$.\ $t$))}. The reverse translation is performed upon printing. paulson@6121: \begin{warn} paulson@14154: The translation between patterns and \isa{split} is performed automatically paulson@6121: by the parser and printer. Thus the internal and external form of a term paulson@14154: may differ, which affects proofs. For example the term \isa{(\%.)} requires the theorem \isa{split} to rewrite to paulson@6121: {\tt}. paulson@6121: \end{warn} paulson@6121: In addition to explicit $\lambda$-abstractions, patterns can be used in any paulson@6121: variable binding construct which is internally described by a paulson@6121: $\lambda$-abstraction. Here are some important examples: paulson@6121: \begin{description} paulson@14154: \item[Let:] \isa{let {\it pattern} = $t$ in $u$} paulson@14154: \item[Choice:] \isa{THE~{\it pattern}~.~$P$} paulson@14154: \item[Set operations:] \isa{\isasymUnion~{\it pattern}:$A$.~$B$} paulson@14154: \item[Comprehension:] \isa{{\ttlbrace}~{\it pattern}:$A$~.~$P$~{\ttrbrace}} paulson@6121: \end{description} paulson@6121: paulson@6121: paulson@14154: %%% domrange.thy? paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{domainI}: \isasymin{}r ==> a\isasymin{}domain(r) paulson@14154: \tdx{domainE}: [| a\isasymin{}domain(r); !!y. \isasymin{}r ==> P |] ==> P paulson@14154: \tdx{domain_subset}: domain(Sigma(A,B)) \isasymsubseteq A paulson@14154: paulson@14154: \tdx{rangeI}: \isasymin{}r ==> b\isasymin{}range(r) paulson@14154: \tdx{rangeE}: [| b\isasymin{}range(r); !!x. \isasymin{}r ==> P |] ==> P paulson@14154: \tdx{range_subset}: range(A*B) \isasymsubseteq B paulson@14154: paulson@14154: \tdx{fieldI1}: \isasymin{}r ==> a\isasymin{}field(r) paulson@14154: \tdx{fieldI2}: \isasymin{}r ==> b\isasymin{}field(r) paulson@14154: \tdx{fieldCI}: ( \isasymnotin r ==> \isasymin{}r) ==> a\isasymin{}field(r) paulson@14154: paulson@14154: \tdx{fieldE}: [| a\isasymin{}field(r); paulson@14158: !!x. \isasymin{}r ==> P; paulson@14158: !!x. \isasymin{}r ==> P paulson@14158: |] ==> P paulson@6121: paulson@14154: \tdx{field_subset}: field(A*A) \isasymsubseteq A paulson@14154: \end{alltt*} paulson@6121: \caption{Domain, range and field of a relation} \label{zf-domrange} paulson@6121: \end{figure} paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{imageI}: [| \isasymin{}r; a\isasymin{}A |] ==> b\isasymin{}r``A paulson@14154: \tdx{imageE}: [| b\isasymin{}r``A; !!x.[| \isasymin{}r; x\isasymin{}A |] ==> P |] ==> P paulson@14154: paulson@14154: \tdx{vimageI}: [| \isasymin{}r; b\isasymin{}B |] ==> a\isasymin{}r-``B paulson@14154: \tdx{vimageE}: [| a\isasymin{}r-``B; !!x.[| \isasymin{}r; x\isasymin{}B |] ==> P |] ==> P paulson@14154: \end{alltt*} paulson@6121: \caption{Image and inverse image} \label{zf-domrange2} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \subsection{Relations} paulson@6121: Figure~\ref{zf-domrange} presents rules involving relations, which are sets paulson@6121: of ordered pairs. The converse of a relation~$r$ is the set of all pairs paulson@6121: $\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then paulson@6121: {\cdx{converse}$(r)$} is its inverse. The rules for the domain paulson@6121: operation, namely \tdx{domainI} and~\tdx{domainE}, assert that paulson@6121: \cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains paulson@6121: some pair of the form~$\pair{x,y}$. The range operation is similar, and paulson@6121: the field of a relation is merely the union of its domain and range. paulson@6121: paulson@6121: Figure~\ref{zf-domrange2} presents rules for images and inverse images. paulson@6121: Note that these operations are generalisations of range and domain, paulson@14154: respectively. paulson@14154: paulson@14154: paulson@14154: %%% func.thy paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{fun_is_rel}: f\isasymin{}Pi(A,B) ==> f \isasymsubseteq Sigma(A,B) paulson@14154: paulson@14158: \tdx{apply_equality}: [| \isasymin{}f; f\isasymin{}Pi(A,B) |] ==> f`a = b paulson@14154: \tdx{apply_equality2}: [| \isasymin{}f; \isasymin{}f; f\isasymin{}Pi(A,B) |] ==> b=c paulson@14154: paulson@14154: \tdx{apply_type}: [| f\isasymin{}Pi(A,B); a\isasymin{}A |] ==> f`a\isasymin{}B(a) paulson@14154: \tdx{apply_Pair}: [| f\isasymin{}Pi(A,B); a\isasymin{}A |] ==> \isasymin{}f paulson@14154: \tdx{apply_iff}: f\isasymin{}Pi(A,B) ==> \isasymin{}f <-> a\isasymin{}A & f`a = b paulson@14154: paulson@14154: \tdx{fun_extension}: [| f\isasymin{}Pi(A,B); g\isasymin{}Pi(A,D); paulson@14154: !!x. x\isasymin{}A ==> f`x = g`x |] ==> f=g paulson@14154: paulson@14154: \tdx{domain_type}: [| \isasymin{}f; f\isasymin{}Pi(A,B) |] ==> a\isasymin{}A paulson@14154: \tdx{range_type}: [| \isasymin{}f; f\isasymin{}Pi(A,B) |] ==> b\isasymin{}B(a) paulson@14154: paulson@14154: \tdx{Pi_type}: [| f\isasymin{}A->C; !!x. x\isasymin{}A ==> f`x\isasymin{}B(x) |] ==> f\isasymin{}Pi(A,B) paulson@14154: \tdx{domain_of_fun}: f\isasymin{}Pi(A,B) ==> domain(f)=A paulson@14154: \tdx{range_of_fun}: f\isasymin{}Pi(A,B) ==> f\isasymin{}A->range(f) paulson@14154: paulson@14154: \tdx{restrict}: a\isasymin{}A ==> restrict(f,A) ` a = f`a paulson@14154: \tdx{restrict_type}: [| !!x. x\isasymin{}A ==> f`x\isasymin{}B(x) |] ==> paulson@14154: restrict(f,A)\isasymin{}Pi(A,B) paulson@14154: \end{alltt*} paulson@6121: \caption{Functions} \label{zf-func1} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{lamI}: a\isasymin{}A ==> \isasymin{}(lam x\isasymin{}A. b(x)) paulson@14154: \tdx{lamE}: [| p\isasymin{}(lam x\isasymin{}A. b(x)); !!x.[| x\isasymin{}A; p= |] ==> P paulson@8249: |] ==> P paulson@8249: paulson@14154: \tdx{lam_type}: [| !!x. x\isasymin{}A ==> b(x)\isasymin{}B(x) |] ==> (lam x\isasymin{}A. b(x))\isasymin{}Pi(A,B) paulson@14154: paulson@14154: \tdx{beta}: a\isasymin{}A ==> (lam x\isasymin{}A. b(x)) ` a = b(a) paulson@14154: \tdx{eta}: f\isasymin{}Pi(A,B) ==> (lam x\isasymin{}A. f`x) = f paulson@14154: \end{alltt*} paulson@6121: \caption{$\lambda$-abstraction} \label{zf-lam} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{fun_empty}: 0\isasymin{}0->0 paulson@14154: \tdx{fun_single}: {\ttlbrace}{\ttrbrace}\isasymin{}{\ttlbrace}a{\ttrbrace} -> {\ttlbrace}b{\ttrbrace} paulson@14154: paulson@14158: \tdx{fun_disjoint_Un}: [| f\isasymin{}A->B; g\isasymin{}C->D; A \isasyminter C = 0 |] ==> paulson@14154: (f \isasymunion g)\isasymin{}(A \isasymunion C) -> (B \isasymunion D) paulson@14154: paulson@14154: \tdx{fun_disjoint_apply1}: [| a\isasymin{}A; f\isasymin{}A->B; g\isasymin{}C->D; A\isasyminter{}C = 0 |] ==> paulson@14154: (f \isasymunion g)`a = f`a paulson@14154: paulson@14154: \tdx{fun_disjoint_apply2}: [| c\isasymin{}C; f\isasymin{}A->B; g\isasymin{}C->D; A\isasyminter{}C = 0 |] ==> paulson@14154: (f \isasymunion g)`c = g`c paulson@14154: \end{alltt*} paulson@6121: \caption{Constructing functions from smaller sets} \label{zf-func2} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \subsection{Functions} paulson@6121: Functions, represented by graphs, are notoriously difficult to reason paulson@14154: about. The ZF theory provides many derived rules, which overlap more paulson@6121: than they ought. This section presents the more important rules. paulson@6121: paulson@6121: Figure~\ref{zf-func1} presents the basic properties of \cdx{Pi}$(A,B)$, paulson@6121: the generalized function space. For example, if $f$ is a function and paulson@6121: $\pair{a,b}\in f$, then $f`a=b$ (\tdx{apply_equality}). Two functions paulson@6121: are equal provided they have equal domains and deliver equals results paulson@6121: (\tdx{fun_extension}). paulson@6121: paulson@6121: By \tdx{Pi_type}, a function typing of the form $f\in A\to C$ can be paulson@6121: refined to the dependent typing $f\in\prod@{x\in A}B(x)$, given a suitable paulson@6121: family of sets $\{B(x)\}@{x\in A}$. Conversely, by \tdx{range_of_fun}, paulson@6121: any dependent typing can be flattened to yield a function type of the form paulson@14154: $A\to C$; here, $C=\isa{range}(f)$. paulson@6121: paulson@6121: Among the laws for $\lambda$-abstraction, \tdx{lamI} and \tdx{lamE} paulson@6121: describe the graph of the generated function, while \tdx{beta} and paulson@6121: \tdx{eta} are the standard conversions. We essentially have a paulson@6121: dependently-typed $\lambda$-calculus (Fig.\ts\ref{zf-lam}). paulson@6121: paulson@6121: Figure~\ref{zf-func2} presents some rules that can be used to construct paulson@6121: functions explicitly. We start with functions consisting of at most one paulson@6121: pair, and may form the union of two functions provided their domains are paulson@6121: disjoint. paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14158: \tdx{Int_absorb}: A \isasyminter A = A paulson@14158: \tdx{Int_commute}: A \isasyminter B = B \isasyminter A paulson@14158: \tdx{Int_assoc}: (A \isasyminter B) \isasyminter C = A \isasyminter (B \isasyminter C) paulson@14158: \tdx{Int_Un_distrib}: (A \isasymunion B) \isasyminter C = (A \isasyminter C) \isasymunion (B \isasyminter C) paulson@14154: paulson@14154: \tdx{Un_absorb}: A \isasymunion A = A paulson@14154: \tdx{Un_commute}: A \isasymunion B = B \isasymunion A paulson@14154: \tdx{Un_assoc}: (A \isasymunion B) \isasymunion C = A \isasymunion (B \isasymunion C) paulson@14158: \tdx{Un_Int_distrib}: (A \isasyminter B) \isasymunion C = (A \isasymunion C) \isasyminter (B \isasymunion C) paulson@14154: paulson@14154: \tdx{Diff_cancel}: A-A = 0 paulson@14158: \tdx{Diff_disjoint}: A \isasyminter (B-A) = 0 paulson@14154: \tdx{Diff_partition}: A \isasymsubseteq B ==> A \isasymunion (B-A) = B paulson@14154: \tdx{double_complement}: [| A \isasymsubseteq B; B \isasymsubseteq C |] ==> (B - (C-A)) = A paulson@14158: \tdx{Diff_Un}: A - (B \isasymunion C) = (A-B) \isasyminter (A-C) paulson@14158: \tdx{Diff_Int}: A - (B \isasyminter C) = (A-B) \isasymunion (A-C) paulson@14154: paulson@14154: \tdx{Union_Un_distrib}: Union(A \isasymunion B) = Union(A) \isasymunion Union(B) paulson@14154: \tdx{Inter_Un_distrib}: [| a \isasymin A; b \isasymin B |] ==> paulson@14158: Inter(A \isasymunion B) = Inter(A) \isasyminter Inter(B) paulson@14158: paulson@14158: \tdx{Int_Union_RepFun}: A \isasyminter Union(B) = ({\isasymUnion}C \isasymin B. A \isasyminter C) paulson@14154: paulson@14154: \tdx{Un_Inter_RepFun}: b \isasymin B ==> paulson@14154: A \isasymunion Inter(B) = ({\isasymInter}C \isasymin B. A \isasymunion C) paulson@14154: paulson@14154: \tdx{SUM_Un_distrib1}: (SUM x \isasymin A \isasymunion B. C(x)) = paulson@14154: (SUM x \isasymin A. C(x)) \isasymunion (SUM x \isasymin B. C(x)) paulson@14154: paulson@14154: \tdx{SUM_Un_distrib2}: (SUM x \isasymin C. A(x) \isasymunion B(x)) = paulson@14154: (SUM x \isasymin C. A(x)) \isasymunion (SUM x \isasymin C. B(x)) paulson@14154: paulson@14158: \tdx{SUM_Int_distrib1}: (SUM x \isasymin A \isasyminter B. C(x)) = paulson@14158: (SUM x \isasymin A. C(x)) \isasyminter (SUM x \isasymin B. C(x)) paulson@14158: paulson@14158: \tdx{SUM_Int_distrib2}: (SUM x \isasymin C. A(x) \isasyminter B(x)) = paulson@14158: (SUM x \isasymin C. A(x)) \isasyminter (SUM x \isasymin C. B(x)) paulson@14154: \end{alltt*} paulson@6121: \caption{Equalities} \label{zf-equalities} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@6121: %\begin{constants} paulson@6121: % \cdx{1} & $i$ & & $\{\emptyset\}$ \\ paulson@6121: % \cdx{bool} & $i$ & & the set $\{\emptyset,1\}$ \\ paulson@14154: % \cdx{cond} & $[i,i,i]\To i$ & & conditional for \isa{bool} \\ paulson@14154: % \cdx{not} & $i\To i$ & & negation for \isa{bool} \\ paulson@14154: % \sdx{and} & $[i,i]\To i$ & Left 70 & conjunction for \isa{bool} \\ paulson@14154: % \sdx{or} & $[i,i]\To i$ & Left 65 & disjunction for \isa{bool} \\ paulson@14154: % \sdx{xor} & $[i,i]\To i$ & Left 65 & exclusive-or for \isa{bool} paulson@6121: %\end{constants} paulson@6121: % paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{bool_def}: bool == {\ttlbrace}0,1{\ttrbrace} paulson@14154: \tdx{cond_def}: cond(b,c,d) == if b=1 then c else d paulson@14154: \tdx{not_def}: not(b) == cond(b,0,1) paulson@14154: \tdx{and_def}: a and b == cond(a,b,0) paulson@14154: \tdx{or_def}: a or b == cond(a,1,b) paulson@14154: \tdx{xor_def}: a xor b == cond(a,not(b),b) paulson@14154: paulson@14154: \tdx{bool_1I}: 1 \isasymin bool paulson@14154: \tdx{bool_0I}: 0 \isasymin bool paulson@14154: \tdx{boolE}: [| c \isasymin bool; c=1 ==> P; c=0 ==> P |] ==> P paulson@14154: \tdx{cond_1}: cond(1,c,d) = c paulson@14154: \tdx{cond_0}: cond(0,c,d) = d paulson@14154: \end{alltt*} paulson@6121: \caption{The booleans} \label{zf-bool} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \section{Further developments} paulson@6121: The next group of developments is complex and extensive, and only paulson@14154: highlights can be covered here. It involves many theories and proofs. paulson@6121: paulson@6121: Figure~\ref{zf-equalities} presents commutative, associative, distributive, paulson@6121: and idempotency laws of union and intersection, along with other equations. paulson@6121: paulson@6121: Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual wenzelm@9695: operators including a conditional (Fig.\ts\ref{zf-bool}). Although ZF is a paulson@6121: first-order theory, you can obtain the effect of higher-order logic using paulson@14154: \isa{bool}-valued functions, for example. The constant~\isa{1} is paulson@14154: translated to \isa{succ(0)}. paulson@6121: paulson@6121: \begin{figure} paulson@6121: \index{*"+ symbol} paulson@6121: \begin{constants} paulson@6121: \it symbol & \it meta-type & \it priority & \it description \\ paulson@6121: \tt + & $[i,i]\To i$ & Right 65 & disjoint union operator\\ paulson@6121: \cdx{Inl}~~\cdx{Inr} & $i\To i$ & & injections\\ paulson@6121: \cdx{case} & $[i\To i,i\To i, i]\To i$ & & conditional for $A+B$ paulson@6121: \end{constants} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{sum_def}: A+B == {\ttlbrace}0{\ttrbrace}*A \isasymunion {\ttlbrace}1{\ttrbrace}*B paulson@14154: \tdx{Inl_def}: Inl(a) == <0,a> paulson@14154: \tdx{Inr_def}: Inr(b) == <1,b> paulson@14154: \tdx{case_def}: case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u) paulson@14154: paulson@14154: \tdx{InlI}: a \isasymin A ==> Inl(a) \isasymin A+B paulson@14154: \tdx{InrI}: b \isasymin B ==> Inr(b) \isasymin A+B paulson@14154: paulson@14154: \tdx{Inl_inject}: Inl(a)=Inl(b) ==> a=b paulson@14154: \tdx{Inr_inject}: Inr(a)=Inr(b) ==> a=b paulson@14154: \tdx{Inl_neq_Inr}: Inl(a)=Inr(b) ==> P paulson@14154: paulson@14154: \tdx{sum_iff}: u \isasymin A+B <-> ({\isasymexists}x\isasymin{}A. u=Inl(x)) | ({\isasymexists}y\isasymin{}B. u=Inr(y)) paulson@14154: paulson@14154: \tdx{case_Inl}: case(c,d,Inl(a)) = c(a) paulson@14154: \tdx{case_Inr}: case(c,d,Inr(b)) = d(b) paulson@14154: \end{alltt*} paulson@6121: \caption{Disjoint unions} \label{zf-sum} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@9584: \subsection{Disjoint unions} paulson@9584: paulson@6121: Theory \thydx{Sum} defines the disjoint union of two sets, with paulson@6121: injections and a case analysis operator (Fig.\ts\ref{zf-sum}). Disjoint paulson@6121: unions play a role in datatype definitions, particularly when there is paulson@6121: mutual recursion~\cite{paulson-set-II}. paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{QPair_def}: == a+b paulson@14154: \tdx{qsplit_def}: qsplit(c,p) == THE y. {\isasymexists}a b. p= & y=c(a,b) paulson@14154: \tdx{qfsplit_def}: qfsplit(R,z) == {\isasymexists}x y. z= & R(x,y) paulson@14154: \tdx{qconverse_def}: qconverse(r) == {\ttlbrace}z. w \isasymin r, {\isasymexists}x y. w= & z={\ttrbrace} paulson@14154: \tdx{QSigma_def}: QSigma(A,B) == {\isasymUnion}x \isasymin A. {\isasymUnion}y \isasymin B(x). {\ttlbrace}{\ttrbrace} paulson@14154: paulson@14154: \tdx{qsum_def}: A <+> B == ({\ttlbrace}0{\ttrbrace} <*> A) \isasymunion ({\ttlbrace}1{\ttrbrace} <*> B) paulson@14154: \tdx{QInl_def}: QInl(a) == <0;a> paulson@14154: \tdx{QInr_def}: QInr(b) == <1;b> paulson@14154: \tdx{qcase_def}: qcase(c,d) == qsplit(\%y z. cond(y, d(z), c(z))) paulson@14154: \end{alltt*} paulson@6121: \caption{Non-standard pairs, products and sums} \label{zf-qpair} paulson@6121: \end{figure} paulson@6121: paulson@9584: paulson@9584: \subsection{Non-standard ordered pairs} paulson@9584: paulson@6121: Theory \thydx{QPair} defines a notion of ordered pair that admits paulson@6121: non-well-founded tupling (Fig.\ts\ref{zf-qpair}). Such pairs are written paulson@6121: {\tt<$a$;$b$>}. It also defines the eliminator \cdx{qsplit}, the paulson@6121: converse operator \cdx{qconverse}, and the summation operator paulson@6121: \cdx{QSigma}. These are completely analogous to the corresponding paulson@6121: versions for standard ordered pairs. The theory goes on to define a paulson@6121: non-standard notion of disjoint sum using non-standard pairs. All of these paulson@6121: concepts satisfy the same properties as their standard counterparts; in paulson@6121: addition, {\tt<$a$;$b$>} is continuous. The theory supports coinductive paulson@6592: definitions, for example of infinite lists~\cite{paulson-mscs}. paulson@6121: paulson@6121: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{bnd_mono_def}: bnd_mono(D,h) == paulson@14158: h(D)\isasymsubseteq{}D & ({\isasymforall}W X. W\isasymsubseteq{}X --> X\isasymsubseteq{}D --> h(W)\isasymsubseteq{}h(X)) paulson@14154: paulson@14154: \tdx{lfp_def}: lfp(D,h) == Inter({\ttlbrace}X \isasymin Pow(D). h(X) \isasymsubseteq X{\ttrbrace}) paulson@14154: \tdx{gfp_def}: gfp(D,h) == Union({\ttlbrace}X \isasymin Pow(D). X \isasymsubseteq h(X){\ttrbrace}) paulson@14154: paulson@14154: paulson@14158: \tdx{lfp_lowerbound}: [| h(A) \isasymsubseteq A; A \isasymsubseteq D |] ==> lfp(D,h) \isasymsubseteq A paulson@14154: paulson@14154: \tdx{lfp_subset}: lfp(D,h) \isasymsubseteq D paulson@14154: paulson@14154: \tdx{lfp_greatest}: [| bnd_mono(D,h); paulson@14154: !!X. [| h(X) \isasymsubseteq X; X \isasymsubseteq D |] ==> A \isasymsubseteq X paulson@14154: |] ==> A \isasymsubseteq lfp(D,h) paulson@14154: paulson@14154: \tdx{lfp_Tarski}: bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h)) paulson@14154: paulson@14154: \tdx{induct}: [| a \isasymin lfp(D,h); bnd_mono(D,h); paulson@14154: !!x. x \isasymin h(Collect(lfp(D,h),P)) ==> P(x) paulson@6121: |] ==> P(a) paulson@6121: paulson@14154: \tdx{lfp_mono}: [| bnd_mono(D,h); bnd_mono(E,i); paulson@14154: !!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X) paulson@14154: |] ==> lfp(D,h) \isasymsubseteq lfp(E,i) paulson@14154: paulson@14158: \tdx{gfp_upperbound}: [| A \isasymsubseteq h(A); A \isasymsubseteq D |] ==> A \isasymsubseteq gfp(D,h) paulson@14154: paulson@14154: \tdx{gfp_subset}: gfp(D,h) \isasymsubseteq D paulson@14154: paulson@14154: \tdx{gfp_least}: [| bnd_mono(D,h); paulson@14154: !!X. [| X \isasymsubseteq h(X); X \isasymsubseteq D |] ==> X \isasymsubseteq A paulson@14154: |] ==> gfp(D,h) \isasymsubseteq A paulson@14154: paulson@14154: \tdx{gfp_Tarski}: bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h)) paulson@14154: paulson@14154: \tdx{coinduct}: [| bnd_mono(D,h); a \isasymin X; X \isasymsubseteq h(X \isasymunion gfp(D,h)); X \isasymsubseteq D paulson@14154: |] ==> a \isasymin gfp(D,h) paulson@14154: paulson@14154: \tdx{gfp_mono}: [| bnd_mono(D,h); D \isasymsubseteq E; paulson@14154: !!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X) paulson@14154: |] ==> gfp(D,h) \isasymsubseteq gfp(E,i) paulson@14154: \end{alltt*} paulson@6121: \caption{Least and greatest fixedpoints} \label{zf-fixedpt} paulson@6121: \end{figure} paulson@6121: paulson@9584: paulson@9584: \subsection{Least and greatest fixedpoints} paulson@9584: paulson@6121: The Knaster-Tarski Theorem states that every monotone function over a paulson@6121: complete lattice has a fixedpoint. Theory \thydx{Fixedpt} proves the paulson@6121: Theorem only for a particular lattice, namely the lattice of subsets of a paulson@6121: set (Fig.\ts\ref{zf-fixedpt}). The theory defines least and greatest paulson@6121: fixedpoint operators with corresponding induction and coinduction rules. paulson@6121: These are essential to many definitions that follow, including the natural paulson@6121: numbers and the transitive closure operator. The (co)inductive definition paulson@6121: package also uses the fixedpoint operators~\cite{paulson-CADE}. See wenzelm@6745: Davey and Priestley~\cite{davey-priestley} for more on the Knaster-Tarski paulson@6121: Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle paulson@6121: proofs. paulson@6121: paulson@6121: Monotonicity properties are proved for most of the set-forming operations: paulson@6121: union, intersection, Cartesian product, image, domain, range, etc. These paulson@6121: are useful for applying the Knaster-Tarski Fixedpoint Theorem. The proofs paulson@14154: themselves are trivial applications of Isabelle's classical reasoner. paulson@6121: paulson@6121: paulson@9584: \subsection{Finite sets and lists} paulson@9584: paulson@9584: Theory \texttt{Finite} (Figure~\ref{zf-fin}) defines the finite set operator; paulson@14154: $\isa{Fin}(A)$ is the set of all finite sets over~$A$. The theory employs paulson@9584: Isabelle's inductive definition package, which proves various rules paulson@9584: automatically. The induction rule shown is stronger than the one proved by paulson@9584: the package. The theory also defines the set of all finite functions paulson@9584: between two given sets. paulson@9584: paulson@9584: \begin{figure} paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{Fin.emptyI} 0 \isasymin Fin(A) paulson@14154: \tdx{Fin.consI} [| a \isasymin A; b \isasymin Fin(A) |] ==> cons(a,b) \isasymin Fin(A) paulson@9584: paulson@9584: \tdx{Fin_induct} paulson@14154: [| b \isasymin Fin(A); paulson@9584: P(0); paulson@14158: !!x y. [| x\isasymin{}A; y\isasymin{}Fin(A); x\isasymnotin{}y; P(y) |] ==> P(cons(x,y)) paulson@9584: |] ==> P(b) paulson@9584: paulson@14154: \tdx{Fin_mono}: A \isasymsubseteq B ==> Fin(A) \isasymsubseteq Fin(B) paulson@14154: \tdx{Fin_UnI}: [| b \isasymin Fin(A); c \isasymin Fin(A) |] ==> b \isasymunion c \isasymin Fin(A) paulson@14154: \tdx{Fin_UnionI}: C \isasymin Fin(Fin(A)) ==> Union(C) \isasymin Fin(A) paulson@14154: \tdx{Fin_subset}: [| c \isasymsubseteq b; b \isasymin Fin(A) |] ==> c \isasymin Fin(A) paulson@14154: \end{alltt*} paulson@9584: \caption{The finite set operator} \label{zf-fin} paulson@9584: \end{figure} paulson@9584: paulson@9584: \begin{figure} paulson@9584: \begin{constants} paulson@9584: \it symbol & \it meta-type & \it priority & \it description \\ paulson@9584: \cdx{list} & $i\To i$ && lists over some set\\ paulson@9584: \cdx{list_case} & $[i, [i,i]\To i, i] \To i$ && conditional for $list(A)$ \\ paulson@9584: \cdx{map} & $[i\To i, i] \To i$ & & mapping functional\\ paulson@9584: \cdx{length} & $i\To i$ & & length of a list\\ paulson@9584: \cdx{rev} & $i\To i$ & & reverse of a list\\ paulson@9584: \tt \at & $[i,i]\To i$ & Right 60 & append for lists\\ paulson@9584: \cdx{flat} & $i\To i$ & & append of list of lists paulson@9584: \end{constants} paulson@9584: paulson@9584: \underscoreon %%because @ is used here paulson@14154: \begin{alltt*}\isastyleminor paulson@14158: \tdx{NilI}: Nil \isasymin list(A) paulson@14158: \tdx{ConsI}: [| a \isasymin A; l \isasymin list(A) |] ==> Cons(a,l) \isasymin list(A) paulson@9584: paulson@9584: \tdx{List.induct} paulson@14154: [| l \isasymin list(A); paulson@9584: P(Nil); paulson@14154: !!x y. [| x \isasymin A; y \isasymin list(A); P(y) |] ==> P(Cons(x,y)) paulson@9584: |] ==> P(l) paulson@9584: paulson@14154: \tdx{Cons_iff}: Cons(a,l)=Cons(a',l') <-> a=a' & l=l' paulson@14154: \tdx{Nil_Cons_iff}: Nil \isasymnoteq Cons(a,l) paulson@14154: paulson@14154: \tdx{list_mono}: A \isasymsubseteq B ==> list(A) \isasymsubseteq list(B) paulson@14154: paulson@14158: \tdx{map_ident}: l\isasymin{}list(A) ==> map(\%u. u, l) = l paulson@14158: \tdx{map_compose}: l\isasymin{}list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l) paulson@14158: \tdx{map_app_distrib}: xs\isasymin{}list(A) ==> map(h, xs@ys) = map(h,xs)@map(h,ys) paulson@9584: \tdx{map_type} paulson@14158: [| l\isasymin{}list(A); !!x. x\isasymin{}A ==> h(x)\isasymin{}B |] ==> map(h,l)\isasymin{}list(B) paulson@9584: \tdx{map_flat} paulson@9584: ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls)) paulson@14154: \end{alltt*} paulson@9584: \caption{Lists} \label{zf-list} paulson@9584: \end{figure} paulson@9584: paulson@9584: paulson@14154: Figure~\ref{zf-list} presents the set of lists over~$A$, $\isa{list}(A)$. The paulson@9584: definition employs Isabelle's datatype package, which defines the introduction paulson@9584: and induction rules automatically, as well as the constructors, case operator paulson@14154: (\isa{list\_case}) and recursion operator. The theory then defines the usual paulson@9584: list functions by primitive recursion. See theory \texttt{List}. paulson@9584: paulson@9584: paulson@9584: \subsection{Miscellaneous} paulson@9584: paulson@6121: \begin{figure} paulson@6121: \begin{constants} paulson@6121: \it symbol & \it meta-type & \it priority & \it description \\ paulson@6121: \sdx{O} & $[i,i]\To i$ & Right 60 & composition ($\circ$) \\ paulson@6121: \cdx{id} & $i\To i$ & & identity function \\ paulson@6121: \cdx{inj} & $[i,i]\To i$ & & injective function space\\ paulson@6121: \cdx{surj} & $[i,i]\To i$ & & surjective function space\\ paulson@6121: \cdx{bij} & $[i,i]\To i$ & & bijective function space paulson@6121: \end{constants} paulson@6121: paulson@14154: \begin{alltt*}\isastyleminor paulson@14154: \tdx{comp_def}: r O s == {\ttlbrace}xz \isasymin domain(s)*range(r) . paulson@14154: {\isasymexists}x y z. xz= & \isasymin s & \isasymin r{\ttrbrace} paulson@14154: \tdx{id_def}: id(A) == (lam x \isasymin A. x) paulson@14158: \tdx{inj_def}: inj(A,B) == {\ttlbrace} f\isasymin{}A->B. {\isasymforall}w\isasymin{}A. {\isasymforall}x\isasymin{}A. f`w=f`x --> w=x {\ttrbrace} paulson@14158: \tdx{surj_def}: surj(A,B) == {\ttlbrace} f\isasymin{}A->B . {\isasymforall}y\isasymin{}B. {\isasymexists}x\isasymin{}A. f`x=y {\ttrbrace} paulson@14158: \tdx{bij_def}: bij(A,B) == inj(A,B) \isasyminter surj(A,B) paulson@14158: paulson@14158: paulson@14158: \tdx{left_inverse}: [| f\isasymin{}inj(A,B); a\isasymin{}A |] ==> converse(f)`(f`a) = a paulson@14158: \tdx{right_inverse}: [| f\isasymin{}inj(A,B); b\isasymin{}range(f) |] ==> paulson@6121: f`(converse(f)`b) = b paulson@6121: paulson@14158: \tdx{inj_converse_inj}: f\isasymin{}inj(A,B) ==> converse(f) \isasymin inj(range(f),A) paulson@14158: \tdx{bij_converse_bij}: f\isasymin{}bij(A,B) ==> converse(f) \isasymin bij(B,A) paulson@14158: paulson@14158: \tdx{comp_type}: [| s \isasymsubseteq A*B; r \isasymsubseteq B*C |] ==> (r O s) \isasymsubseteq A*C paulson@14158: \tdx{comp_assoc}: (r O s) O t = r O (s O t) paulson@14158: paulson@14158: \tdx{left_comp_id}: r \isasymsubseteq A*B ==> id(B) O r = r paulson@14158: \tdx{right_comp_id}: r \isasymsubseteq A*B ==> r O id(A) = r paulson@14158: paulson@14158: \tdx{comp_func}: [| g\isasymin{}A->B; f\isasymin{}B->C |] ==> (f O g) \isasymin A->C paulson@14158: \tdx{comp_func_apply}: [| g\isasymin{}A->B; f\isasymin{}B->C; a\isasymin{}A |] ==> (f O g)`a = f`(g`a) paulson@14158: paulson@14158: \tdx{comp_inj}: [| g\isasymin{}inj(A,B); f\isasymin{}inj(B,C) |] ==> (f O g)\isasymin{}inj(A,C) paulson@14158: \tdx{comp_surj}: [| g\isasymin{}surj(A,B); f\isasymin{}surj(B,C) |] ==> (f O g)\isasymin{}surj(A,C) paulson@14158: \tdx{comp_bij}: [| g\isasymin{}bij(A,B); f\isasymin{}bij(B,C) |] ==> (f O g)\isasymin{}bij(A,C) paulson@14158: paulson@14158: \tdx{left_comp_inverse}: f\isasymin{}inj(A,B) ==> converse(f) O f = id(A) paulson@14158: \tdx{right_comp_inverse}: f\isasymin{}surj(A,B) ==> f O converse(f) = id(B) paulson@14154: paulson@14154: \tdx{bij_disjoint_Un}: paulson@14158: [| f\isasymin{}bij(A,B); g\isasymin{}bij(C,D); A \isasyminter C = 0; B \isasyminter D = 0 |] ==> paulson@14158: (f \isasymunion g)\isasymin{}bij(A \isasymunion C, B \isasymunion D) paulson@14158: paulson@14158: \tdx{restrict_bij}: [| f\isasymin{}inj(A,B); C\isasymsubseteq{}A |] ==> restrict(f,C)\isasymin{}bij(C, f``C) paulson@14154: \end{alltt*} paulson@6121: \caption{Permutations} \label{zf-perm} paulson@6121: \end{figure} paulson@6121: paulson@6121: The theory \thydx{Perm} is concerned with permutations (bijections) and paulson@6121: related concepts. These include composition of relations, the identity paulson@6121: relation, and three specialized function spaces: injective, surjective and paulson@6121: bijective. Figure~\ref{zf-perm} displays many of their properties that paulson@6121: have been proved. These results are fundamental to a treatment of paulson@6121: equipollence and cardinality. paulson@6121: paulson@14154: Theory \thydx{Univ} defines a `universe' $\isa{univ}(A)$, which is used by paulson@9584: the datatype package. This set contains $A$ and the paulson@14154: natural numbers. Vitally, it is closed under finite products: paulson@14154: $\isa{univ}(A)\times\isa{univ}(A)\subseteq\isa{univ}(A)$. This theory also paulson@9584: defines the cumulative hierarchy of axiomatic set theory, which paulson@9584: traditionally is written $V@\alpha$ for an ordinal~$\alpha$. The paulson@9584: `universe' is a simple generalization of~$V@\omega$. paulson@9584: paulson@14154: Theory \thydx{QUniv} defines a `universe' $\isa{quniv}(A)$, which is used by paulson@9584: the datatype package to construct codatatypes such as streams. It is paulson@14154: analogous to $\isa{univ}(A)$ (and is defined in terms of it) but is closed paulson@9584: under the non-standard product and sum. paulson@9584: paulson@9584: paulson@9584: \section{Automatic Tools} paulson@9584: wenzelm@9695: ZF provides the simplifier and the classical reasoner. Moreover it supplies a wenzelm@9695: specialized tool to infer `types' of terms. paulson@9584: paulson@14154: \subsection{Simplification and Classical Reasoning} paulson@9584: wenzelm@9695: ZF inherits simplification from FOL but adopts it for set theory. The wenzelm@9695: extraction of rewrite rules takes the ZF primitives into account. It can paulson@9584: strip bounded universal quantifiers from a formula; for example, ${\forall paulson@9584: x\in A. f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp paulson@9584: f(x)=g(x)$. Given $a\in\{x\in A. P(x)\}$ it extracts rewrite rules from $a\in paulson@9584: A$ and~$P(a)$. It can also break down $a\in A\int B$ and $a\in A-B$. paulson@9584: paulson@14154: The default simpset used by \isa{simp} contains congruence rules for all of ZF's paulson@14154: binding operators. It contains all the conversion rules, such as paulson@14154: \isa{fst} and paulson@14154: \isa{snd}, as well as the rewrites shown in Fig.\ts\ref{zf-simpdata}. paulson@14154: paulson@14154: Classical reasoner methods such as \isa{blast} and \isa{auto} refer to paulson@14154: a rich collection of built-in axioms for all the set-theoretic paulson@14154: primitives. paulson@9584: paulson@9584: paulson@9584: \begin{figure} paulson@9584: \begin{eqnarray*} paulson@9584: a\in \emptyset & \bimp & \bot\\ paulson@9584: a \in A \un B & \bimp & a\in A \disj a\in B\\ paulson@9584: a \in A \int B & \bimp & a\in A \conj a\in B\\ paulson@14154: a \in A-B & \bimp & a\in A \conj \lnot (a\in B)\\ paulson@14154: \pair{a,b}\in \isa{Sigma}(A,B) paulson@9584: & \bimp & a\in A \conj b\in B(a)\\ paulson@14154: a \in \isa{Collect}(A,P) & \bimp & a\in A \conj P(a)\\ paulson@9584: (\forall x \in \emptyset. P(x)) & \bimp & \top\\ paulson@9584: (\forall x \in A. \top) & \bimp & \top paulson@9584: \end{eqnarray*} paulson@9584: \caption{Some rewrite rules for set theory} \label{zf-simpdata} paulson@9584: \end{figure} paulson@9584: paulson@9584: paulson@9584: \subsection{Type-Checking Tactics} paulson@9584: \index{type-checking tactics} paulson@9584: wenzelm@9695: Isabelle/ZF provides simple tactics to help automate those proofs that are paulson@9584: essentially type-checking. Such proofs are built by applying rules such as paulson@9584: these: paulson@14154: \begin{ttbox}\isastyleminor paulson@14158: [| ?P ==> ?a \isasymin ?A; ~?P ==> ?b \isasymin ?A |] paulson@14158: ==> (if ?P then ?a else ?b) \isasymin ?A paulson@14154: paulson@14154: [| ?m \isasymin nat; ?n \isasymin nat |] ==> ?m #+ ?n \isasymin nat paulson@14154: paulson@14154: ?a \isasymin ?A ==> Inl(?a) \isasymin ?A + ?B paulson@9584: \end{ttbox} paulson@9584: In typical applications, the goal has the form $t\in\Var{A}$: in other words, paulson@9584: we have a specific term~$t$ and need to infer its `type' by instantiating the paulson@9584: set variable~$\Var{A}$. Neither the simplifier nor the classical reasoner paulson@9584: does this job well. The if-then-else rule, and many similar ones, can make paulson@9584: the classical reasoner loop. The simplifier refuses (on principle) to paulson@14154: instantiate variables during rewriting, so goals such as \isa{i\#+j \isasymin \ ?A} paulson@9584: are left unsolved. paulson@9584: paulson@9584: The simplifier calls the type-checker to solve rewritten subgoals: this stage paulson@9584: can indeed instantiate variables. If you have defined new constants and paulson@14154: proved type-checking rules for them, then declare the rules using paulson@14154: the attribute \isa{TC} and the rest should be automatic. In paulson@14154: particular, the simplifier will use type-checking to help satisfy paulson@14154: conditional rewrite rules. Call the method \ttindex{typecheck} to paulson@14154: break down all subgoals using type-checking rules. You can add new paulson@14154: type-checking rules temporarily like this: paulson@14154: \begin{isabelle} paulson@14158: \isacommand{apply}\ (typecheck add:\ inj_is_fun) paulson@14154: \end{isabelle} paulson@14154: paulson@14154: paulson@14154: %Though the easiest way to invoke the type-checker is via the simplifier, paulson@14154: %specialized applications may require more detailed knowledge of paulson@14154: %the type-checking primitives. They are modelled on the simplifier's: paulson@14154: %\begin{ttdescription} paulson@14154: %\item[\ttindexbold{tcset}] is the type of tcsets: sets of type-checking rules. paulson@14154: % paulson@14154: %\item[\ttindexbold{addTCs}] is an infix operator to add type-checking rules to paulson@14154: % a tcset. paulson@14154: % paulson@14154: %\item[\ttindexbold{delTCs}] is an infix operator to remove type-checking rules paulson@14154: % from a tcset. paulson@14154: % paulson@14154: %\item[\ttindexbold{typecheck_tac}] is a tactic for attempting to prove all paulson@14154: % subgoals using the rules given in its argument, a tcset. paulson@14154: %\end{ttdescription} paulson@14154: % paulson@14154: %Tcsets, like simpsets, are associated with theories and are merged when paulson@14154: %theories are merged. There are further primitives that use the default tcset. paulson@14154: %\begin{ttdescription} paulson@14154: %\item[\ttindexbold{tcset}] is a function to return the default tcset; use the paulson@14154: % expression \isa{tcset()}. paulson@14154: % paulson@14154: %\item[\ttindexbold{AddTCs}] adds type-checking rules to the default tcset. paulson@14154: % paulson@14154: %\item[\ttindexbold{DelTCs}] removes type-checking rules from the default paulson@14154: % tcset. paulson@14154: % paulson@14154: %\item[\ttindexbold{Typecheck_tac}] calls \isa{typecheck_tac} using the paulson@14154: % default tcset. paulson@14154: %\end{ttdescription} paulson@14154: % paulson@14154: %To supply some type-checking rules temporarily, using \isa{Addrules} and paulson@14154: %later \isa{Delrules} is the simplest way. There is also a high-tech paulson@14154: %approach. Call the simplifier with a new solver expressed using paulson@14154: %\ttindexbold{type_solver_tac} and your temporary type-checking rules. paulson@14154: %\begin{ttbox}\isastyleminor paulson@14154: %by (asm_simp_tac paulson@14154: % (simpset() setSolver type_solver_tac (tcset() addTCs prems)) 2); paulson@14154: %\end{ttbox} paulson@9584: paulson@9584: paulson@9584: \section{Natural number and integer arithmetic} paulson@9584: paulson@9584: \index{arithmetic|(} paulson@9584: paulson@6121: \begin{figure}\small paulson@6121: \index{#*@{\tt\#*} symbol} paulson@6121: \index{*div symbol} paulson@6121: \index{*mod symbol} paulson@6121: \index{#+@{\tt\#+} symbol} paulson@6121: \index{#-@{\tt\#-} symbol} paulson@6121: \begin{constants} paulson@6121: \it symbol & \it meta-type & \it priority & \it description \\ paulson@6121: \cdx{nat} & $i$ & & set of natural numbers \\ paulson@6121: \cdx{nat_case}& $[i,i\To i,i]\To i$ & & conditional for $nat$\\ paulson@6121: \tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\ paulson@6121: \tt div & $[i,i]\To i$ & Left 70 & division\\ paulson@6121: \tt mod & $[i,i]\To i$ & Left 70 & modulus\\ paulson@6121: \tt \#+ & $[i,i]\To i$ & Left 65 & addition\\ paulson@6121: \tt \#- & $[i,i]\To i$ & Left 65 & subtraction paulson@6121: \end{constants} paulson@6121: paulson@14158: \begin{alltt*}\isastyleminor paulson@14154: \tdx{nat_def}: nat == lfp(lam r \isasymin Pow(Inf). {\ttlbrace}0{\ttrbrace} \isasymunion {\ttlbrace}succ(x). x \isasymin r{\ttrbrace} paulson@14154: paulson@14158: \tdx{nat_case_def}: nat_case(a,b,k) == paulson@14154: THE y. k=0 & y=a | ({\isasymexists}x. k=succ(x) & y=b(x)) paulson@14154: paulson@14158: \tdx{nat_0I}: 0 \isasymin nat paulson@14158: \tdx{nat_succI}: n \isasymin nat ==> succ(n) \isasymin nat paulson@14158: paulson@14158: \tdx{nat_induct}: paulson@14154: [| n \isasymin nat; P(0); !!x. [| x \isasymin nat; P(x) |] ==> P(succ(x)) paulson@6121: |] ==> P(n) paulson@6121: paulson@14158: \tdx{nat_case_0}: nat_case(a,b,0) = a paulson@14158: \tdx{nat_case_succ}: nat_case(a,b,succ(m)) = b(m) paulson@14158: paulson@14158: \tdx{add_0_natify}: 0 #+ n = natify(n) paulson@14158: \tdx{add_succ}: succ(m) #+ n = succ(m #+ n) paulson@14158: paulson@14158: \tdx{mult_type}: m #* n \isasymin nat paulson@14158: \tdx{mult_0}: 0 #* n = 0 paulson@14158: \tdx{mult_succ}: succ(m) #* n = n #+ (m #* n) paulson@14158: \tdx{mult_commute}: m #* n = n #* m paulson@14158: \tdx{add_mult_dist}: (m #+ n) #* k = (m #* k) #+ (n #* k) paulson@14158: \tdx{mult_assoc}: (m #* n) #* k = m #* (n #* k) paulson@14158: \tdx{mod_div_equality}: m \isasymin nat ==> (m div n)#*n #+ m mod n = m paulson@14158: \end{alltt*} paulson@6121: \caption{The natural numbers} \label{zf-nat} paulson@6121: \end{figure} paulson@6121: paulson@9584: \index{natural numbers} paulson@9584: paulson@6121: Theory \thydx{Nat} defines the natural numbers and mathematical paulson@6121: induction, along with a case analysis operator. The set of natural paulson@14154: numbers, here called \isa{nat}, is known in set theory as the ordinal~$\omega$. paulson@6121: paulson@6121: Theory \thydx{Arith} develops arithmetic on the natural numbers paulson@6121: (Fig.\ts\ref{zf-nat}). Addition, multiplication and subtraction are defined paulson@6121: by primitive recursion. Division and remainder are defined by repeated paulson@6121: subtraction, which requires well-founded recursion; the termination argument paulson@6121: relies on the divisor's being non-zero. Many properties are proved: paulson@6121: commutative, associative and distributive laws, identity and cancellation paulson@6121: laws, etc. The most interesting result is perhaps the theorem $a \bmod b + paulson@6121: (a/b)\times b = a$. paulson@6121: paulson@14154: To minimize the need for tedious proofs of $t\in\isa{nat}$, the arithmetic paulson@9584: operators coerce their arguments to be natural numbers. The function paulson@14154: \cdx{natify} is defined such that $\isa{natify}(n) = n$ if $n$ is a natural paulson@14154: number, $\isa{natify}(\isa{succ}(x)) = paulson@14154: \isa{succ}(\isa{natify}(x))$ for all $x$, and finally paulson@14154: $\isa{natify}(x)=0$ in all other cases. The benefit is that the addition, paulson@9584: subtraction, multiplication, division and remainder operators always return paulson@9584: natural numbers, regardless of their arguments. Algebraic laws (commutative, paulson@14154: associative, distributive) are unconditional. Occurrences of \isa{natify} paulson@9584: as operands of those operators are simplified away. Any remaining occurrences paulson@9584: can either be tolerated or else eliminated by proving that the argument is a paulson@9584: natural number. paulson@9584: paulson@9584: The simplifier automatically cancels common terms on the opposite sides of paulson@9584: subtraction and of relations ($=$, $<$ and $\le$). Here is an example: paulson@14154: \begin{isabelle} paulson@14154: 1. i \#+ j \#+ k \#- j < k \#+ l\isanewline paulson@14154: \isacommand{apply}\ simp\isanewline paulson@9584: 1. natify(i) < natify(l) paulson@14154: \end{isabelle} paulson@14154: Given the assumptions \isa{i \isasymin nat} and \isa{l \isasymin nat}, both occurrences of paulson@9584: \cdx{natify} would be simplified away. paulson@9584: paulson@9584: paulson@9584: \begin{figure}\small paulson@9584: \index{$*@{\tt\$*} symbol} paulson@9584: \index{$+@{\tt\$+} symbol} paulson@9584: \index{$-@{\tt\$-} symbol} paulson@6121: \begin{constants} paulson@6121: \it symbol & \it meta-type & \it priority & \it description \\ paulson@9584: \cdx{int} & $i$ & & set of integers \\ paulson@9584: \tt \$* & $[i,i]\To i$ & Left 70 & multiplication \\ paulson@9584: \tt \$+ & $[i,i]\To i$ & Left 65 & addition\\ paulson@9584: \tt \$- & $[i,i]\To i$ & Left 65 & subtraction\\ paulson@9584: \tt \$< & $[i,i]\To o$ & Left 50 & $<$ on integers\\ paulson@9584: \tt \$<= & $[i,i]\To o$ & Left 50 & $\le$ on integers paulson@6121: \end{constants} paulson@6121: paulson@14158: \begin{alltt*}\isastyleminor paulson@14154: \tdx{zadd_0_intify}: 0 $+ n = intify(n) paulson@14154: paulson@14154: \tdx{zmult_type}: m $* n \isasymin int paulson@14154: \tdx{zmult_0}: 0 $* n = 0 paulson@14154: \tdx{zmult_commute}: m $* n = n $* m paulson@14154: \tdx{zadd_zmult_dist}: (m $+ n) $* k = (m $* k) $+ (n $* k) paulson@14154: \tdx{zmult_assoc}: (m $* n) $* k = m $* (n $* k) paulson@14158: \end{alltt*} paulson@9584: \caption{The integers} \label{zf-int} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@9584: \index{integers} paulson@9584: paulson@9584: Theory \thydx{Int} defines the integers, as equivalence classes of natural paulson@9584: numbers. Figure~\ref{zf-int} presents a tidy collection of laws. In paulson@9584: fact, a large library of facts is proved, including monotonicity laws for paulson@9584: addition and multiplication, covering both positive and negative operands. paulson@9584: paulson@9584: As with the natural numbers, the need for typing proofs is minimized. All the paulson@9584: operators defined in Fig.\ts\ref{zf-int} coerce their operands to integers by paulson@9584: applying the function \cdx{intify}. This function is the identity on integers paulson@9584: and maps other operands to zero. paulson@9584: paulson@9584: Decimal notation is provided for the integers. Numbers, written as paulson@14154: \isa{\#$nnn$} or \isa{\#-$nnn$}, are represented internally in paulson@9584: two's-complement binary. Expressions involving addition, subtraction and paulson@9584: multiplication of numeral constants are evaluated (with acceptable efficiency) paulson@9584: by simplification. The simplifier also collects similar terms, multiplying paulson@9584: them by a numerical coefficient. It also cancels occurrences of the same paulson@9584: terms on the other side of the relational operators. Example: paulson@14154: \begin{isabelle} paulson@14154: 1. y \$+ z \$+ \#-3 \$* x \$+ y \$<= x \$* \#2 \$+ paulson@14154: z\isanewline paulson@14154: \isacommand{apply}\ simp\isanewline paulson@14154: 1. \#2 \$* y \$<= \#5 \$* x paulson@14154: \end{isabelle} paulson@9584: For more information on the integers, please see the theories on directory paulson@9584: \texttt{ZF/Integ}. paulson@9584: paulson@9584: \index{arithmetic|)} paulson@6173: paulson@6173: paulson@6121: \section{Datatype definitions} paulson@6121: \label{sec:ZF:datatype} paulson@6121: \index{*datatype|(} paulson@6121: wenzelm@9695: The \ttindex{datatype} definition package of ZF constructs inductive datatypes paulson@14154: similar to \ML's. It can also construct coinductive datatypes wenzelm@9695: (codatatypes), which are non-well-founded structures such as streams. It wenzelm@9695: defines the set using a fixed-point construction and proves induction rules, wenzelm@9695: as well as theorems for recursion and case combinators. It supplies wenzelm@9695: mechanisms for reasoning about freeness. The datatype package can handle both wenzelm@9695: mutual and indirect recursion. paulson@6121: paulson@6121: paulson@6121: \subsection{Basics} paulson@6121: \label{subsec:datatype:basics} paulson@6121: paulson@14154: A \isa{datatype} definition has the following form: paulson@6121: \[ paulson@6121: \begin{array}{llcl} paulson@6121: \mathtt{datatype} & t@1(A@1,\ldots,A@h) & = & paulson@6121: constructor^1@1 ~\mid~ \ldots ~\mid~ constructor^1@{k@1} \\ paulson@6121: & & \vdots \\ paulson@6121: \mathtt{and} & t@n(A@1,\ldots,A@h) & = & paulson@6121: constructor^n@1~ ~\mid~ \ldots ~\mid~ constructor^n@{k@n} paulson@6121: \end{array} paulson@6121: \] paulson@6121: Here $t@1$, \ldots,~$t@n$ are identifiers and $A@1$, \ldots,~$A@h$ are paulson@6121: variables: the datatype's parameters. Each constructor specification has the paulson@6121: form \dquotesoff paulson@6121: \[ C \hbox{\tt~( } \hbox{\tt"} x@1 \hbox{\tt:} T@1 \hbox{\tt"},\; paulson@6121: \ldots,\; paulson@6121: \hbox{\tt"} x@m \hbox{\tt:} T@m \hbox{\tt"} paulson@6121: \hbox{\tt~)} paulson@6121: \] paulson@6121: Here $C$ is the constructor name, and variables $x@1$, \ldots,~$x@m$ are the paulson@6121: constructor arguments, belonging to the sets $T@1$, \ldots, $T@m$, paulson@6121: respectively. Typically each $T@j$ is either a constant set, a datatype paulson@6121: parameter (one of $A@1$, \ldots, $A@h$) or a recursive occurrence of one of paulson@6121: the datatypes, say $t@i(A@1,\ldots,A@h)$. More complex possibilities exist, paulson@6121: but they are much harder to realize. Often, additional information must be paulson@6121: supplied in the form of theorems. paulson@6121: paulson@6121: A datatype can occur recursively as the argument of some function~$F$. This paulson@6121: is called a {\em nested} (or \emph{indirect}) occurrence. It is only allowed paulson@6121: if the datatype package is given a theorem asserting that $F$ is monotonic. paulson@6121: If the datatype has indirect occurrences, then Isabelle/ZF does not support paulson@6121: recursive function definitions. paulson@6121: paulson@14154: A simple example of a datatype is \isa{list}, which is built-in, and is paulson@6121: defined by paulson@14158: \begin{alltt*}\isastyleminor paulson@14154: consts list :: "i=>i" paulson@14154: datatype "list(A)" = Nil | Cons ("a \isasymin A", "l \isasymin list(A)") paulson@14158: \end{alltt*} paulson@6121: Note that the datatype operator must be declared as a constant first. paulson@14154: However, the package declares the constructors. Here, \isa{Nil} gets type paulson@14154: $i$ and \isa{Cons} gets type $[i,i]\To i$. paulson@6121: paulson@6121: Trees and forests can be modelled by the mutually recursive datatype paulson@6121: definition paulson@14158: \begin{alltt*}\isastyleminor paulson@14154: consts paulson@14154: tree :: "i=>i" paulson@14154: forest :: "i=>i" paulson@14154: tree_forest :: "i=>i" paulson@14154: datatype "tree(A)" = Tcons ("a{\isasymin}A", "f{\isasymin}forest(A)") paulson@14154: and "forest(A)" = Fnil | Fcons ("t{\isasymin}tree(A)", "f{\isasymin}forest(A)") paulson@14158: \end{alltt*} paulson@14154: Here $\isa{tree}(A)$ is the set of trees over $A$, $\isa{forest}(A)$ is paulson@14154: the set of forests over $A$, and $\isa{tree_forest}(A)$ is the union of paulson@6121: the previous two sets. All three operators must be declared first. paulson@6121: paulson@14154: The datatype \isa{term}, which is defined by paulson@14158: \begin{alltt*}\isastyleminor paulson@14154: consts term :: "i=>i" paulson@14154: datatype "term(A)" = Apply ("a \isasymin A", "l \isasymin list(term(A))") paulson@14154: monos list_mono paulson@28871: type_elims list_univ [THEN subsetD, elim_format] paulson@14158: \end{alltt*} paulson@14154: is an example of nested recursion. (The theorem \isa{list_mono} is proved paulson@14154: in theory \isa{List}, and the \isa{term} example is developed in paulson@14154: theory paulson@14154: \thydx{Induct/Term}.) paulson@6121: paulson@6121: \subsubsection{Freeness of the constructors} paulson@6121: paulson@6121: Constructors satisfy {\em freeness} properties. Constructions are distinct, paulson@14154: for example $\isa{Nil}\not=\isa{Cons}(a,l)$, and they are injective, for paulson@14154: example $\isa{Cons}(a,l)=\isa{Cons}(a',l') \bimp a=a' \conj l=l'$. paulson@6121: Because the number of freeness is quadratic in the number of constructors, the paulson@6143: datatype package does not prove them. Instead, it ensures that simplification paulson@6143: will prove them dynamically: when the simplifier encounters a formula paulson@6143: asserting the equality of two datatype constructors, it performs freeness paulson@6143: reasoning. paulson@6143: paulson@6143: Freeness reasoning can also be done using the classical reasoner, but it is paulson@6143: more complicated. You have to add some safe elimination rules rules to the paulson@14154: claset. For the \isa{list} datatype, they are called paulson@14154: \isa{list.free_elims}. Occasionally this exposes the underlying paulson@6143: representation of some constructor, which can be rectified using the command paulson@14154: \isa{unfold list.con_defs [symmetric]}. paulson@6143: paulson@6121: paulson@6121: \subsubsection{Structural induction} paulson@6121: paulson@6121: The datatype package also provides structural induction rules. For datatypes paulson@6121: without mutual or nested recursion, the rule has the form exemplified by paulson@14154: \isa{list.induct} in Fig.\ts\ref{zf-list}. For mutually recursive paulson@6121: datatypes, the induction rule is supplied in two forms. Consider datatype paulson@14154: \isa{TF}. The rule \isa{tree_forest.induct} performs induction over a paulson@14154: single predicate~\isa{P}, which is presumed to be defined for both trees paulson@6121: and forests: paulson@14158: \begin{alltt*}\isastyleminor paulson@14154: [| x \isasymin tree_forest(A); paulson@14154: !!a f. [| a \isasymin A; f \isasymin forest(A); P(f) |] ==> P(Tcons(a, f)); paulson@8249: P(Fnil); paulson@14154: !!f t. [| t \isasymin tree(A); P(t); f \isasymin forest(A); P(f) |] paulson@6121: ==> P(Fcons(t, f)) paulson@6121: |] ==> P(x) paulson@14158: \end{alltt*} paulson@14154: The rule \isa{tree_forest.mutual_induct} performs induction over two paulson@14154: distinct predicates, \isa{P_tree} and \isa{P_forest}. paulson@14158: \begin{alltt*}\isastyleminor paulson@6121: [| !!a f. paulson@14154: [| a{\isasymin}A; f{\isasymin}forest(A); P_forest(f) |] ==> P_tree(Tcons(a,f)); paulson@6121: P_forest(Fnil); paulson@14154: !!f t. [| t{\isasymin}tree(A); P_tree(t); f{\isasymin}forest(A); P_forest(f) |] paulson@6121: ==> P_forest(Fcons(t, f)) paulson@14154: |] ==> ({\isasymforall}za. za \isasymin tree(A) --> P_tree(za)) & paulson@14154: ({\isasymforall}za. za \isasymin forest(A) --> P_forest(za)) paulson@14158: \end{alltt*} paulson@6121: paulson@14154: For datatypes with nested recursion, such as the \isa{term} example from paulson@14154: above, things are a bit more complicated. The rule \isa{term.induct} paulson@14154: refers to the monotonic operator, \isa{list}: paulson@14158: \begin{alltt*}\isastyleminor paulson@14154: [| x \isasymin term(A); paulson@14158: !!a l. [| a\isasymin{}A; l\isasymin{}list(Collect(term(A), P)) |] ==> P(Apply(a,l)) paulson@6121: |] ==> P(x) paulson@14158: \end{alltt*} paulson@14154: The theory \isa{Induct/Term.thy} derives two higher-level induction rules, paulson@14154: one of which is particularly useful for proving equations: paulson@14158: \begin{alltt*}\isastyleminor paulson@14154: [| t \isasymin term(A); paulson@14154: !!x zs. [| x \isasymin A; zs \isasymin list(term(A)); map(f, zs) = map(g, zs) |] paulson@6121: ==> f(Apply(x, zs)) = g(Apply(x, zs)) paulson@6121: |] ==> f(t) = g(t) paulson@14158: \end{alltt*} paulson@6121: How this can be generalized to other nested datatypes is a matter for future paulson@6121: research. paulson@6121: paulson@6121: paulson@14154: \subsubsection{The \isa{case} operator} paulson@6121: paulson@6121: The package defines an operator for performing case analysis over the paulson@14154: datatype. For \isa{list}, it is called \isa{list_case} and satisfies paulson@6121: the equations paulson@14154: \begin{ttbox}\isastyleminor paulson@6121: list_case(f_Nil, f_Cons, []) = f_Nil paulson@6121: list_case(f_Nil, f_Cons, Cons(a, l)) = f_Cons(a, l) paulson@6121: \end{ttbox} paulson@14154: Here \isa{f_Nil} is the value to return if the argument is \isa{Nil} and paulson@14154: \isa{f_Cons} is a function that computes the value to return if the paulson@14154: argument has the form $\isa{Cons}(a,l)$. The function can be expressed as paulson@6121: an abstraction, over patterns if desired (\S\ref{sec:pairs}). paulson@6121: paulson@14154: For mutually recursive datatypes, there is a single \isa{case} operator. paulson@14154: In the tree/forest example, the constant \isa{tree_forest_case} handles all paulson@6121: of the constructors of the two datatypes. paulson@6121: paulson@6121: paulson@6121: \subsection{Defining datatypes} paulson@6121: paulson@6121: The theory syntax for datatype definitions is shown in paulson@6121: Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype paulson@6121: definition has to obey the rules stated in the previous section. As a result paulson@6121: the theory is extended with the new types, the constructors, and the theorems paulson@6121: listed in the previous section. The quotation marks are necessary because paulson@6121: they enclose general Isabelle formul\ae. paulson@6121: paulson@6121: \begin{figure} paulson@6121: \begin{rail} paulson@6121: datatype : ( 'datatype' | 'codatatype' ) datadecls; paulson@6121: paulson@6121: datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and' paulson@6121: ; paulson@6121: constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) ) paulson@6121: ; paulson@14154: consargs : '(' ('"' var ' : ' term '"' + ',') ')' paulson@6121: ; paulson@6121: \end{rail} paulson@6121: \caption{Syntax of datatype declarations} paulson@6121: \label{datatype-grammar} paulson@6121: \end{figure} paulson@6121: paulson@6121: Codatatypes are declared like datatypes and are identical to them in every paulson@6121: respect except that they have a coinduction rule instead of an induction rule. paulson@6121: Note that while an induction rule has the effect of limiting the values paulson@6121: contained in the set, a coinduction rule gives a way of constructing new paulson@6121: values of the set. paulson@6121: paulson@6121: Most of the theorems about datatypes become part of the default simpset. You paulson@6121: never need to see them again because the simplifier applies them paulson@14154: automatically. paulson@14154: paulson@14154: \subsubsection{Specialized methods for datatypes} paulson@14154: paulson@14154: Induction and case-analysis can be invoked using these special-purpose paulson@14154: methods: paulson@6121: \begin{ttdescription} paulson@14154: \item[\methdx{induct_tac} $x$] applies structural paulson@14154: induction on variable $x$ to subgoal~1, provided the type of $x$ is a paulson@6121: datatype. The induction variable should not occur among other assumptions paulson@6121: of the subgoal. paulson@6121: \end{ttdescription} paulson@14154: % paulson@14154: % we also have the ind_cases method, but what does it do? paulson@14154: In some situations, induction is overkill and a case distinction over all paulson@6121: constructors of the datatype suffices. paulson@6121: \begin{ttdescription} paulson@14202: \item[\methdx{case_tac} $x$] paulson@14154: performs a case analysis for the variable~$x$. paulson@6121: \end{ttdescription} paulson@6121: paulson@6121: Both tactics can only be applied to a variable, whose typing must be given in paulson@14154: some assumption, for example the assumption \isa{x \isasymin \ list(A)}. The tactics paulson@14154: also work for the natural numbers (\isa{nat}) and disjoint sums, although paulson@6121: these sets were not defined using the datatype package. (Disjoint sums are paulson@14154: not recursive, so only \isa{case_tac} is available.) paulson@14154: paulson@14154: Structured Isar methods are also available. Below, $t$ paulson@14154: stands for the name of the datatype. paulson@14154: \begin{ttdescription} paulson@14154: \item[\methdx{induct} \isa{set:}\ $t$] is the Isar induction tactic. paulson@14154: \item[\methdx{cases} \isa{set:}\ $t$] is the Isar case-analysis tactic. paulson@14154: \end{ttdescription} paulson@14154: paulson@14154: paulson@14154: \subsubsection{The theorems proved by a datatype declaration} paulson@14154: paulson@6121: Here are some more details for the technically minded. Processing the paulson@14154: datatype declaration of a set~$t$ produces a name space~$t$ containing paulson@14154: the following theorems: paulson@14154: \begin{ttbox}\isastyleminor paulson@14154: intros \textrm{the introduction rules} paulson@14154: cases \textrm{the case analysis rule} paulson@14154: induct \textrm{the standard induction rule} paulson@14154: mutual_induct \textrm{the mutual induction rule, if needed} paulson@14154: case_eqns \textrm{equations for the case operator} paulson@14154: recursor_eqns \textrm{equations for the recursor} paulson@14154: simps \textrm{the union of} case_eqns \textrm{and} recursor_eqns paulson@14154: con_defs \textrm{definitions of the case operator and constructors} paulson@14154: free_iffs \textrm{logical equivalences for proving freeness} paulson@14154: free_elims \textrm{elimination rules for proving freeness} paulson@14154: defs \textrm{datatype definition(s)} paulson@6121: \end{ttbox} paulson@14154: Furthermore there is the theorem $C$ for every constructor~$C$; for paulson@14154: example, the \isa{list} datatype's introduction rules are bound to the paulson@14154: identifiers \isa{Nil} and \isa{Cons}. paulson@14154: paulson@14154: For a codatatype, the component \isa{coinduct} is the coinduction rule, paulson@14154: replacing the \isa{induct} component. paulson@14154: paulson@14154: See the theories \isa{Induct/Ntree} and \isa{Induct/Brouwer} for examples of paulson@14154: infinitely branching datatypes. See theory \isa{Induct/LList} for an example paulson@6121: of a codatatype. Some of these theories illustrate the use of additional, paulson@6121: undocumented features of the datatype package. Datatype definitions are paulson@6121: reduced to inductive definitions, and the advanced features should be paulson@6121: understood in that light. paulson@6121: paulson@6121: paulson@6121: \subsection{Examples} paulson@6121: paulson@6121: \subsubsection{The datatype of binary trees} paulson@6121: paulson@14154: Let us define the set $\isa{bt}(A)$ of binary trees over~$A$. The theory paulson@6121: must contain these lines: paulson@14158: \begin{alltt*}\isastyleminor paulson@14154: consts bt :: "i=>i" paulson@14154: datatype "bt(A)" = Lf | Br ("a\isasymin{}A", "t1\isasymin{}bt(A)", "t2\isasymin{}bt(A)") paulson@14158: \end{alltt*} paulson@14154: After loading the theory, we can prove some theorem. paulson@14154: We begin by declaring the constructor's typechecking rules paulson@14154: as simplification rules: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{declare}\ bt.intros\ [simp]% paulson@14154: \end{isabelle} paulson@14154: paulson@14154: Our first example is the theorem that no tree equals its paulson@14154: left branch. To make the inductive hypothesis strong enough, paulson@14154: the proof requires a quantified induction formula, but paulson@14154: the \isa{rule\_format} attribute will remove the quantifiers paulson@14154: before the theorem is stored. paulson@14154: \begin{isabelle} paulson@14158: \isacommand{lemma}\ Br\_neq\_left\ [rule\_format]:\ "l\isasymin bt(A)\ ==>\ \isasymforall x\ r.\ Br(x,l,r)\isasymnoteq{}l"\isanewline paulson@14154: \ 1.\ l\ \isasymin \ bt(A)\ \isasymLongrightarrow \ \isasymforall x\ r.\ Br(x,\ l,\ r)\ \isasymnoteq \ l% paulson@14154: \end{isabelle} paulson@6121: This can be proved by the structural induction tactic: paulson@14154: \begin{isabelle} paulson@14154: \ \ \isacommand{apply}\ (induct\_tac\ l)\isanewline paulson@14154: \ 1.\ \isasymforall x\ r.\ Br(x,\ Lf,\ r)\ \isasymnoteq \ Lf\isanewline paulson@14154: \ 2.\ \isasymAnd a\ t1\ t2.\isanewline paulson@14154: \isaindent{\ 2.\ \ \ \ }\isasymlbrakk a\ \isasymin \ A;\ t1\ \isasymin \ bt(A);\ \isasymforall x\ r.\ Br(x,\ t1,\ r)\ \isasymnoteq \ t1;\ t2\ \isasymin \ bt(A);\isanewline paulson@14154: \isaindent{\ 2.\ \ \ \ \ \ \ }\isasymforall x\ r.\ Br(x,\ t2,\ r)\ \isasymnoteq \ t2\isasymrbrakk \isanewline paulson@14154: \isaindent{\ 2.\ \ \ \ }\isasymLongrightarrow \ \isasymforall x\ r.\ Br(x,\ Br(a,\ t1,\ t2),\ r)\ \isasymnoteq \ Br(a,\ t1,\ t2) paulson@14154: \end{isabelle} paulson@14154: Both subgoals are proved using \isa{auto}, which performs the necessary paulson@6143: freeness reasoning. paulson@14154: \begin{isabelle} paulson@14154: \ \ \isacommand{apply}\ auto\isanewline paulson@14154: No\ subgoals!\isanewline paulson@14154: \isacommand{done} paulson@14154: \end{isabelle} paulson@14154: paulson@14154: An alternative proof uses Isar's fancy \isa{induct} method, which paulson@14154: automatically quantifies over all free variables: paulson@14154: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ Br\_neq\_left':\ "l\ \isasymin \ bt(A)\ ==>\ (!!x\ r.\ Br(x,\ l,\ r)\ \isasymnoteq \ l)"\isanewline paulson@14154: \ \ \isacommand{apply}\ (induct\ set:\ bt)\isanewline paulson@14154: \ 1.\ \isasymAnd x\ r.\ Br(x,\ Lf,\ r)\ \isasymnoteq \ Lf\isanewline paulson@14154: \ 2.\ \isasymAnd a\ t1\ t2\ x\ r.\isanewline paulson@14154: \isaindent{\ 2.\ \ \ \ }\isasymlbrakk a\ \isasymin \ A;\ t1\ \isasymin \ bt(A);\ \isasymAnd x\ r.\ Br(x,\ t1,\ r)\ \isasymnoteq \ t1;\ t2\ \isasymin \ bt(A);\isanewline paulson@14154: \isaindent{\ 2.\ \ \ \ \ \ \ }\isasymAnd x\ r.\ Br(x,\ t2,\ r)\ \isasymnoteq \ t2\isasymrbrakk \isanewline paulson@14154: \isaindent{\ 2.\ \ \ \ }\isasymLongrightarrow \ Br(x,\ Br(a,\ t1,\ t2),\ r)\ \isasymnoteq \ Br(a,\ t1,\ t2) paulson@14154: \end{isabelle} paulson@14154: Compare the form of the induction hypotheses with the corresponding ones in paulson@14154: the previous proof. As before, to conclude requires only \isa{auto}. paulson@6121: paulson@6121: When there are only a few constructors, we might prefer to prove the freenness paulson@14154: theorems for each constructor. This is simple: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ Br\_iff:\ "Br(a,l,r)\ =\ Br(a',l',r')\ <->\ a=a'\ \&\ l=l'\ \&\ r=r'"\isanewline paulson@14154: \ \ \isacommand{by}\ (blast\ elim!:\ bt.free\_elims) paulson@14154: \end{isabelle} paulson@14154: Here we see a demonstration of freeness reasoning using paulson@14154: \isa{bt.free\_elims}, but simpler still is just to apply \isa{auto}. paulson@14154: paulson@14154: An \ttindex{inductive\_cases} declaration generates instances of the paulson@14154: case analysis rule that have been simplified using freeness paulson@14154: reasoning. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{inductive\_cases}\ Br\_in\_bt:\ "Br(a,\ l,\ r)\ \isasymin \ bt(A)" paulson@14154: \end{isabelle} paulson@14154: The theorem just created is paulson@14154: \begin{isabelle} paulson@14154: \isasymlbrakk Br(a,\ l,\ r)\ \isasymin \ bt(A);\ \isasymlbrakk a\ \isasymin \ A;\ l\ \isasymin \ bt(A);\ r\ \isasymin \ bt(A)\isasymrbrakk \ \isasymLongrightarrow \ Q\isasymrbrakk \ \isasymLongrightarrow \ Q. paulson@14154: \end{isabelle} paulson@14154: It is an elimination rule that from $\isa{Br}(a,l,r)\in\isa{bt}(A)$ paulson@14154: lets us infer $a\in A$, $l\in\isa{bt}(A)$ and paulson@14154: $r\in\isa{bt}(A)$. paulson@6121: paulson@6121: paulson@6121: \subsubsection{Mixfix syntax in datatypes} paulson@6121: paulson@14154: Mixfix syntax is sometimes convenient. The theory \isa{Induct/PropLog} makes a paulson@6121: deep embedding of propositional logic: paulson@14158: \begin{alltt*}\isastyleminor paulson@6121: consts prop :: i paulson@6121: datatype "prop" = Fls paulson@14154: | Var ("n \isasymin nat") ("#_" [100] 100) paulson@14154: | "=>" ("p \isasymin prop", "q \isasymin prop") (infixr 90) paulson@14158: \end{alltt*} paulson@6121: The second constructor has a special $\#n$ syntax, while the third constructor paulson@6121: is an infixed arrow. paulson@6121: paulson@6121: paulson@6121: \subsubsection{A giant enumeration type} paulson@6121: paulson@6121: This example shows a datatype that consists of 60 constructors: paulson@14158: \begin{alltt*}\isastyleminor paulson@6121: consts enum :: i paulson@6121: datatype paulson@6121: "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09 paulson@6121: | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19 paulson@6121: | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29 paulson@6121: | C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39 paulson@6121: | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49 paulson@6121: | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59 paulson@6121: end paulson@14158: \end{alltt*} paulson@6121: The datatype package scales well. Even though all properties are proved paulson@14154: rather than assumed, full processing of this definition takes around two seconds paulson@14154: (on a 1.8GHz machine). The constructors have a balanced representation, paulson@14154: related to binary notation, so freeness properties can be proved fast. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "C00 \isasymnoteq\ C01"\isanewline paulson@14154: \ \ \isacommand{by}\ simp paulson@14154: \end{isabelle} paulson@14154: You need not derive such inequalities explicitly. The simplifier will paulson@14154: dispose of them automatically. paulson@6121: paulson@6121: \index{*datatype|)} paulson@6121: paulson@6121: paulson@6121: \subsection{Recursive function definitions}\label{sec:ZF:recursive} paulson@6121: \index{recursive functions|see{recursion}} paulson@6121: \index{*primrec|(} paulson@6173: \index{recursion!primitive|(} paulson@6121: paulson@6121: Datatypes come with a uniform way of defining functions, {\bf primitive paulson@6121: recursion}. Such definitions rely on the recursion operator defined by the paulson@6121: datatype package. Isabelle proves the desired recursion equations as paulson@6121: theorems. paulson@6121: paulson@6121: In principle, one could introduce primitive recursive functions by asserting paulson@14154: their reduction rules as axioms. Here is a dangerous way of defining a paulson@14154: recursive function over binary trees: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{consts}\ \ n\_nodes\ ::\ "i\ =>\ i"\isanewline paulson@14154: \isacommand{axioms}\isanewline paulson@14154: \ \ n\_nodes\_Lf:\ "n\_nodes(Lf)\ =\ 0"\isanewline paulson@14154: \ \ n\_nodes\_Br:\ "n\_nodes(Br(a,l,r))\ =\ succ(n\_nodes(l)\ \#+\ n\_nodes(r))" paulson@14154: \end{isabelle} paulson@14154: Asserting axioms brings the danger of accidentally introducing paulson@14154: contradictions. It should be avoided whenever possible. paulson@6121: paulson@6121: The \ttindex{primrec} declaration is a safe means of defining primitive paulson@6121: recursive functions on datatypes: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{consts}\ \ n\_nodes\ ::\ "i\ =>\ i"\isanewline paulson@14154: \isacommand{primrec}\isanewline paulson@14154: \ \ "n\_nodes(Lf)\ =\ 0"\isanewline paulson@14154: \ \ "n\_nodes(Br(a,\ l,\ r))\ =\ succ(n\_nodes(l)\ \#+\ n\_nodes(r))" paulson@14154: \end{isabelle} paulson@14154: Isabelle will now derive the two equations from a low-level definition paulson@14154: based upon well-founded recursion. If they do not define a legitimate paulson@14154: recursion, then Isabelle will reject the declaration. paulson@6121: paulson@6121: paulson@6121: \subsubsection{Syntax of recursive definitions} paulson@6121: paulson@6121: The general form of a primitive recursive definition is paulson@14154: \begin{ttbox}\isastyleminor paulson@6121: primrec paulson@6121: {\it reduction rules} paulson@6121: \end{ttbox} paulson@6121: where \textit{reduction rules} specify one or more equations of the form paulson@6121: \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \, paulson@6121: \dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$ paulson@6121: contains only the free variables on the left-hand side, and all recursive paulson@6121: calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. paulson@6121: There must be at most one reduction rule for each constructor. The order is paulson@6121: immaterial. For missing constructors, the function is defined to return zero. paulson@6121: paulson@6121: All reduction rules are added to the default simpset. paulson@6121: If you would like to refer to some rule by name, then you must prefix paulson@6121: the rule with an identifier. These identifiers, like those in the paulson@14154: \isa{rules} section of a theory, will be visible in proof scripts. paulson@14154: paulson@14154: The reduction rules become part of the default simpset, which paulson@6121: leads to short proof scripts: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ n\_nodes\_type\ [simp]:\ "t\ \isasymin \ bt(A)\ ==>\ n\_nodes(t)\ \isasymin \ nat"\isanewline paulson@14154: \ \ \isacommand{by}\ (induct\_tac\ t,\ auto) paulson@14154: \end{isabelle} paulson@14154: paulson@14154: You can even use the \isa{primrec} form with non-recursive datatypes and paulson@6121: with codatatypes. Recursion is not allowed, but it provides a convenient paulson@6121: syntax for defining functions by cases. paulson@6121: paulson@6121: paulson@6121: \subsubsection{Example: varying arguments} paulson@6121: paulson@6121: All arguments, other than the recursive one, must be the same in each equation paulson@6121: and in each recursive call. To get around this restriction, use explict paulson@14154: $\lambda$-abstraction and function application. For example, let us paulson@14154: define the tail-recursive version of \isa{n\_nodes}, using an paulson@14154: accumulating argument for the counter. The second argument, $k$, varies in paulson@6121: recursive calls. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{consts}\ \ n\_nodes\_aux\ ::\ "i\ =>\ i"\isanewline paulson@14154: \isacommand{primrec}\isanewline paulson@14154: \ \ "n\_nodes\_aux(Lf)\ =\ (\isasymlambda k\ \isasymin \ nat.\ k)"\isanewline paulson@14154: \ \ "n\_nodes\_aux(Br(a,l,r))\ =\ \isanewline paulson@14154: \ \ \ \ \ \ (\isasymlambda k\ \isasymin \ nat.\ n\_nodes\_aux(r)\ `\ \ (n\_nodes\_aux(l)\ `\ succ(k)))" paulson@14154: \end{isabelle} paulson@14154: Now \isa{n\_nodes\_aux(t)\ `\ k} is our function in two arguments. We paulson@14154: can prove a theorem relating it to \isa{n\_nodes}. Note the quantification paulson@14154: over \isa{k\ \isasymin \ nat}: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ n\_nodes\_aux\_eq\ [rule\_format]:\isanewline paulson@14154: \ \ \ \ \ "t\ \isasymin \ bt(A)\ ==>\ \isasymforall k\ \isasymin \ nat.\ n\_nodes\_aux(t)`k\ =\ n\_nodes(t)\ \#+\ k"\isanewline paulson@14154: \ \ \isacommand{by}\ (induct\_tac\ t,\ simp\_all) paulson@14154: \end{isabelle} paulson@14154: paulson@14154: Now, we can use \isa{n\_nodes\_aux} to define a tail-recursive version paulson@14154: of \isa{n\_nodes}: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{constdefs}\isanewline paulson@14154: \ \ n\_nodes\_tail\ ::\ "i\ =>\ i"\isanewline paulson@14154: \ \ \ "n\_nodes\_tail(t)\ ==\ n\_nodes\_aux(t)\ `\ 0" paulson@14154: \end{isabelle} paulson@14154: It is easy to paulson@14154: prove that \isa{n\_nodes\_tail} is equivalent to \isa{n\_nodes}: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "t\ \isasymin \ bt(A)\ ==>\ n\_nodes\_tail(t)\ =\ n\_nodes(t)"\isanewline paulson@14154: \ \isacommand{by}\ (simp\ add:\ n\_nodes\_tail\_def\ n\_nodes\_aux\_eq) paulson@14154: \end{isabelle} paulson@14154: paulson@14154: paulson@14154: paulson@6121: paulson@6121: \index{recursion!primitive|)} paulson@6121: \index{*primrec|)} paulson@6121: paulson@6121: paulson@6121: \section{Inductive and coinductive definitions} paulson@6121: \index{*inductive|(} paulson@6121: \index{*coinductive|(} paulson@6121: paulson@6121: An {\bf inductive definition} specifies the least set~$R$ closed under given paulson@6121: rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For paulson@6121: example, a structural operational semantics is an inductive definition of an paulson@6121: evaluation relation. Dually, a {\bf coinductive definition} specifies the paulson@6121: greatest set~$R$ consistent with given rules. (Every element of~$R$ can be paulson@6121: seen as arising by applying a rule to elements of~$R$.) An important example paulson@6121: is using bisimulation relations to formalise equivalence of processes and paulson@6121: infinite data structures. paulson@6121: paulson@6121: A theory file may contain any number of inductive and coinductive paulson@6121: definitions. They may be intermixed with other declarations; in paulson@6121: particular, the (co)inductive sets {\bf must} be declared separately as paulson@6121: constants, and may have mixfix syntax or be subject to syntax translations. paulson@6121: paulson@6121: Each (co)inductive definition adds definitions to the theory and also paulson@14154: proves some theorems. It behaves identially to the analogous paulson@14154: inductive definition except that instead of an induction rule there is paulson@14154: a coinduction rule. Its treatment of coinduction is described in paulson@14154: detail in a separate paper,% paulson@6121: \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is paulson@6121: distributed with Isabelle as \emph{A Fixedpoint Approach to paulson@6121: (Co)Inductive and (Co)Datatype Definitions}.} % paulson@6121: which you might refer to for background information. paulson@6121: paulson@6121: paulson@6121: \subsection{The syntax of a (co)inductive definition} paulson@6121: An inductive definition has the form paulson@14154: \begin{ttbox}\isastyleminor paulson@6121: inductive paulson@14154: domains {\it domain declarations} paulson@14154: intros {\it introduction rules} paulson@14154: monos {\it monotonicity theorems} paulson@14154: con_defs {\it constructor definitions} paulson@14154: type_intros {\it introduction rules for type-checking} paulson@14154: type_elims {\it elimination rules for type-checking} paulson@6121: \end{ttbox} paulson@6121: A coinductive definition is identical, but starts with the keyword paulson@14154: \isa{co\-inductive}. paulson@14154: paulson@14154: The \isa{monos}, \isa{con\_defs}, \isa{type\_intros} and \isa{type\_elims} paulson@14154: sections are optional. If present, each is specified as a list of paulson@14154: theorems, which may contain Isar attributes as usual. paulson@6121: paulson@6121: \begin{description} paulson@8249: \item[\it domain declarations] are items of the form paulson@14154: {\it string\/}~\isa{\isasymsubseteq }~{\it string}, associating each recursive set with paulson@6121: its domain. (The domain is some existing set that is large enough to paulson@6121: hold the new set being defined.) paulson@6121: paulson@6121: \item[\it introduction rules] specify one or more introduction rules in paulson@6121: the form {\it ident\/}~{\it string}, where the identifier gives the name of paulson@6121: the rule in the result structure. paulson@6121: paulson@6121: \item[\it monotonicity theorems] are required for each operator applied to paulson@6121: a recursive set in the introduction rules. There \textbf{must} be a theorem paulson@6121: of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each premise $t\in M(R_i)$ paulson@6121: in an introduction rule! paulson@6121: paulson@6121: \item[\it constructor definitions] contain definitions of constants paulson@6121: appearing in the introduction rules. The (co)datatype package supplies paulson@6121: the constructors' definitions here. Most (co)inductive definitions omit paulson@6121: this section; one exception is the primitive recursive functions example; paulson@14154: see theory \isa{Induct/Primrec}. paulson@6121: paulson@14154: \item[\it type\_intros] consists of introduction rules for type-checking the paulson@6121: definition: for demonstrating that the new set is included in its domain. paulson@6121: (The proof uses depth-first search.) paulson@6121: paulson@6121: \item[\it type\_elims] consists of elimination rules for type-checking the paulson@6121: definition. They are presumed to be safe and are applied as often as paulson@14154: possible prior to the \isa{type\_intros} search. paulson@6121: \end{description} paulson@6121: paulson@6121: The package has a few restrictions: paulson@6121: \begin{itemize} paulson@6121: \item The theory must separately declare the recursive sets as paulson@6121: constants. paulson@6121: paulson@6121: \item The names of the recursive sets must be identifiers, not infix paulson@6121: operators. paulson@6121: paulson@6121: \item Side-conditions must not be conjunctions. However, an introduction rule paulson@6121: may contain any number of side-conditions. paulson@6121: paulson@6121: \item Side-conditions of the form $x=t$, where the variable~$x$ does not paulson@14154: occur in~$t$, will be substituted through the rule \isa{mutual\_induct}. paulson@6121: \end{itemize} paulson@6121: paulson@6121: paulson@6121: \subsection{Example of an inductive definition} paulson@6121: paulson@14154: Below, we shall see how Isabelle/ZF defines the finite powerset paulson@14154: operator. The first step is to declare the constant~\isa{Fin}. Then we paulson@14154: must declare it inductively, with two introduction rules: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{consts}\ \ Fin\ ::\ "i=>i"\isanewline paulson@14154: \isacommand{inductive}\isanewline paulson@14154: \ \ \isakeyword{domains}\ \ \ "Fin(A)"\ \isasymsubseteq\ "Pow(A)"\isanewline paulson@14154: \ \ \isakeyword{intros}\isanewline paulson@14154: \ \ \ \ emptyI:\ \ "0\ \isasymin\ Fin(A)"\isanewline paulson@14154: \ \ \ \ consI:\ \ \ "[|\ a\ \isasymin\ A;\ \ b\ \isasymin\ Fin(A)\ |]\ ==>\ cons(a,b)\ \isasymin\ Fin(A)"\isanewline paulson@14154: \ \ \isakeyword{type\_intros}\ \ empty\_subsetI\ cons\_subsetI\ PowI\isanewline paulson@14154: \ \ \isakeyword{type\_elims}\ \ \ PowD\ [THEN\ revcut\_rl]\end{isabelle} paulson@14154: The resulting theory contains a name space, called~\isa{Fin}. paulson@14154: The \isa{Fin}$~A$ introduction rules can be referred to collectively as paulson@14154: \isa{Fin.intros}, and also individually as \isa{Fin.emptyI} and paulson@14154: \isa{Fin.consI}. The induction rule is \isa{Fin.induct}. paulson@6121: paulson@6121: The chief problem with making (co)inductive definitions involves type-checking paulson@6121: the rules. Sometimes, additional theorems need to be supplied under paulson@14154: \isa{type_intros} or \isa{type_elims}. If the package fails when trying paulson@6121: to prove your introduction rules, then set the flag \ttindexbold{trace_induct} paulson@14154: to \isa{true} and try again. (See the manual \emph{A Fixedpoint Approach paulson@6121: \ldots} for more discussion of type-checking.) paulson@6121: paulson@14154: In the example above, $\isa{Pow}(A)$ is given as the domain of paulson@14154: $\isa{Fin}(A)$, for obviously every finite subset of~$A$ is a subset paulson@6121: of~$A$. However, the inductive definition package can only prove that given a paulson@6121: few hints. paulson@6121: Here is the output that results (with the flag set) when the paulson@14154: \isa{type_intros} and \isa{type_elims} are omitted from the inductive paulson@6121: definition above: paulson@14158: \begin{alltt*}\isastyleminor paulson@6121: Inductive definition Finite.Fin paulson@6121: Fin(A) == paulson@6121: lfp(Pow(A), paulson@14158: \%X. {z\isasymin{}Pow(A) . z = 0 | ({\isasymexists}a b. z = cons(a,b) & a\isasymin{}A & b\isasymin{}X)}) paulson@6121: Proving monotonicity... paulson@6121: \ttbreak paulson@6121: Proving the introduction rules... paulson@6173: The type-checking subgoal: paulson@14154: 0 \isasymin Fin(A) paulson@14154: 1. 0 \isasymin Pow(A) paulson@6121: \ttbreak paulson@6121: The subgoal after monos, type_elims: paulson@14154: 0 \isasymin Fin(A) paulson@14154: 1. 0 \isasymin Pow(A) paulson@6121: *** prove_goal: tactic failed paulson@14158: \end{alltt*} paulson@6121: We see the need to supply theorems to let the package prove paulson@14154: $\emptyset\in\isa{Pow}(A)$. Restoring the \isa{type_intros} but not the paulson@14154: \isa{type_elims}, we again get an error message: paulson@14158: \begin{alltt*}\isastyleminor paulson@6173: The type-checking subgoal: paulson@14154: 0 \isasymin Fin(A) paulson@14154: 1. 0 \isasymin Pow(A) paulson@6121: \ttbreak paulson@6121: The subgoal after monos, type_elims: paulson@14154: 0 \isasymin Fin(A) paulson@14154: 1. 0 \isasymin Pow(A) paulson@6121: \ttbreak paulson@6173: The type-checking subgoal: paulson@14154: cons(a, b) \isasymin Fin(A) paulson@14154: 1. [| a \isasymin A; b \isasymin Fin(A) |] ==> cons(a, b) \isasymin Pow(A) paulson@6121: \ttbreak paulson@6121: The subgoal after monos, type_elims: paulson@14154: cons(a, b) \isasymin Fin(A) paulson@14154: 1. [| a \isasymin A; b \isasymin Pow(A) |] ==> cons(a, b) \isasymin Pow(A) paulson@6121: *** prove_goal: tactic failed paulson@14158: \end{alltt*} paulson@6121: The first rule has been type-checked, but the second one has failed. The paulson@6121: simplest solution to such problems is to prove the failed subgoal separately paulson@14154: and to supply it under \isa{type_intros}. The solution actually used is paulson@14154: to supply, under \isa{type_elims}, a rule that changes paulson@14154: $b\in\isa{Pow}(A)$ to $b\subseteq A$; together with \isa{cons_subsetI} paulson@14154: and \isa{PowI}, it is enough to complete the type-checking. paulson@6121: paulson@6121: paulson@6121: paulson@6121: \subsection{Further examples} paulson@6121: paulson@6121: An inductive definition may involve arbitrary monotonic operators. Here is a paulson@6121: standard example: the accessible part of a relation. Note the use paulson@14154: of~\isa{Pow} in the introduction rule and the corresponding mention of the paulson@14154: rule \isa{Pow\_mono} in the \isa{monos} list. If the desired rule has a paulson@6121: universally quantified premise, usually the effect can be obtained using paulson@14154: \isa{Pow}. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{consts}\ \ acc\ ::\ "i\ =>\ i"\isanewline paulson@14154: \isacommand{inductive}\isanewline paulson@14154: \ \ \isakeyword{domains}\ "acc(r)"\ \isasymsubseteq \ "field(r)"\isanewline paulson@14154: \ \ \isakeyword{intros}\isanewline paulson@14154: \ \ \ \ vimage:\ \ "[|\ r-``\isacharbraceleft a\isacharbraceright\ \isasymin\ Pow(acc(r));\ a\ \isasymin \ field(r)\ |] paulson@14154: \isanewline paulson@14154: \ \ \ \ \ \ \ \ \ \ \ \ \ \ ==>\ a\ \isasymin \ acc(r)"\isanewline paulson@14154: \ \ \isakeyword{monos}\ \ Pow\_mono paulson@14154: \end{isabelle} paulson@14154: paulson@14154: Finally, here are some coinductive definitions. We begin by defining paulson@14154: lazy (potentially infinite) lists as a codatatype: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{consts}\ \ llist\ \ ::\ "i=>i"\isanewline paulson@14154: \isacommand{codatatype}\isanewline paulson@14154: \ \ "llist(A)"\ =\ LNil\ |\ LCons\ ("a\ \isasymin \ A",\ "l\ \isasymin \ llist(A)")\isanewline paulson@14154: \end{isabelle} paulson@14154: paulson@14154: The notion of equality on such lists is modelled as a bisimulation: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{consts}\ \ lleq\ ::\ "i=>i"\isanewline paulson@14154: \isacommand{coinductive}\isanewline paulson@14154: \ \ \isakeyword{domains}\ "lleq(A)"\ <=\ "llist(A)\ *\ llist(A)"\isanewline paulson@14154: \ \ \isakeyword{intros}\isanewline paulson@14154: \ \ \ \ LNil:\ \ "\ \isasymin \ lleq(A)"\isanewline paulson@14154: \ \ \ \ LCons:\ "[|\ a\ \isasymin \ A;\ \ \isasymin \ lleq(A)\ |]\ \isanewline paulson@14154: \ \ \ \ \ \ \ \ \ \ \ \ ==>\ \ \isasymin \ lleq(A)"\isanewline paulson@14154: \ \ \isakeyword{type\_intros}\ \ llist.intros paulson@14154: \end{isabelle} paulson@14154: This use of \isa{type_intros} is typical: the relation concerns the paulson@14154: codatatype \isa{llist}, so naturally the introduction rules for that paulson@14154: codatatype will be required for type-checking the rules. paulson@14154: paulson@14154: The Isabelle distribution contains many other inductive definitions. Simple paulson@14154: examples are collected on subdirectory \isa{ZF/Induct}. The directory paulson@14154: \isa{Coind} and the theory \isa{ZF/Induct/LList} contain coinductive paulson@14154: definitions. Larger examples may be found on other subdirectories of paulson@14154: \isa{ZF}, such as \isa{IMP}, and \isa{Resid}. paulson@14154: paulson@14154: paulson@14154: \subsection{Theorems generated} paulson@14154: paulson@14154: Each (co)inductive set defined in a theory file generates a name space paulson@14154: containing the following elements: paulson@14154: \begin{ttbox}\isastyleminor paulson@14154: intros \textrm{the introduction rules} paulson@14154: elim \textrm{the elimination (case analysis) rule} paulson@14154: induct \textrm{the standard induction rule} paulson@14154: mutual_induct \textrm{the mutual induction rule, if needed} paulson@14154: defs \textrm{definitions of inductive sets} paulson@14154: bnd_mono \textrm{monotonicity property} paulson@14154: dom_subset \textrm{inclusion in `bounding set'} paulson@6121: \end{ttbox} paulson@14154: Furthermore, each introduction rule is available under its declared paulson@14154: name. For a codatatype, the component \isa{coinduct} is the coinduction rule, paulson@14154: replacing the \isa{induct} component. paulson@14154: paulson@14154: Recall that the \ttindex{inductive\_cases} declaration generates paulson@14154: simplified instances of the case analysis rule. It is as useful for paulson@14154: inductive definitions as it is for datatypes. There are many examples paulson@14154: in the theory paulson@14154: \isa{Induct/Comb}, which is discussed at length paulson@14154: elsewhere~\cite{paulson-generic}. The theory first defines the paulson@14154: datatype paulson@14154: \isa{comb} of combinators: paulson@14158: \begin{alltt*}\isastyleminor paulson@6121: consts comb :: i paulson@6121: datatype "comb" = K paulson@6121: | S paulson@14154: | "#" ("p \isasymin comb", "q \isasymin comb") (infixl 90) paulson@14158: \end{alltt*} paulson@6121: The theory goes on to define contraction and parallel contraction paulson@14154: inductively. Then the theory \isa{Induct/Comb.thy} defines special paulson@14154: cases of contraction, such as this one: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{inductive\_cases}\ K\_contractE [elim!]:\ "K -1-> r" paulson@14154: \end{isabelle} paulson@14154: The theorem just created is \isa{K -1-> r \ \isasymLongrightarrow \ Q}, paulson@14154: which expresses that the combinator \isa{K} cannot reduce to paulson@14154: anything. (From the assumption \isa{K-1->r}, we can conclude any desired paulson@14154: formula \isa{Q}\@.) Similar elimination rules for \isa{S} and application are also paulson@14154: generated. The attribute \isa{elim!}\ shown above supplies the generated paulson@14154: theorem to the classical reasoner. This mode of working allows paulson@14154: effective reasoniung about operational semantics. paulson@6121: paulson@6121: \index{*coinductive|)} \index{*inductive|)} paulson@6121: paulson@6121: paulson@6121: paulson@6121: \section{The outer reaches of set theory} paulson@6121: paulson@6121: The constructions of the natural numbers and lists use a suite of paulson@6121: operators for handling recursive function definitions. I have described paulson@6121: the developments in detail elsewhere~\cite{paulson-set-II}. Here is a brief paulson@6121: summary: paulson@6121: \begin{itemize} paulson@14154: \item Theory \isa{Trancl} defines the transitive closure of a relation paulson@6121: (as a least fixedpoint). paulson@6121: paulson@14154: \item Theory \isa{WF} proves the well-founded recursion theorem, using an paulson@6121: elegant approach of Tobias Nipkow. This theorem permits general paulson@6121: recursive definitions within set theory. paulson@6121: paulson@14154: \item Theory \isa{Ord} defines the notions of transitive set and ordinal paulson@6121: number. It derives transfinite induction. A key definition is {\bf paulson@6121: less than}: $i Pow(A) \isasymsubseteq Pow(B) paulson@14154: \end{isabelle} paulson@6121: We enter the goal and make the first step, which breaks the equation into paulson@6121: two inclusions by extensionality:\index{*equalityI theorem} paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "Pow(A\ Int\ B)\ =\ Pow(A)\ Int\ Pow(B)"\isanewline paulson@14154: \ 1.\ Pow(A\ \isasyminter \ B)\ =\ Pow(A)\ \isasyminter \ Pow(B)\isanewline paulson@14154: \isacommand{apply}\ (rule\ equalityI)\isanewline paulson@14154: \ 1.\ Pow(A\ \isasyminter \ B)\ \isasymsubseteq \ Pow(A)\ \isasyminter \ Pow(B)\isanewline paulson@14154: \ 2.\ Pow(A)\ \isasyminter \ Pow(B)\ \isasymsubseteq \ Pow(A\ \isasyminter \ B) paulson@14154: \end{isabelle} paulson@14154: Both inclusions could be tackled straightforwardly using \isa{subsetI}. paulson@6121: A shorter proof results from noting that intersection forms the greatest paulson@6121: lower bound:\index{*Int_greatest theorem} paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ Int\_greatest)\isanewline paulson@14154: \ 1.\ Pow(A\ \isasyminter \ B)\ \isasymsubseteq \ Pow(A)\isanewline paulson@14154: \ 2.\ Pow(A\ \isasyminter \ B)\ \isasymsubseteq \ Pow(B)\isanewline paulson@14154: \ 3.\ Pow(A)\ \isasyminter \ Pow(B)\ \isasymsubseteq \ Pow(A\ \isasyminter \ B) paulson@14154: \end{isabelle} paulson@14154: Subgoal~1 follows by applying the monotonicity of \isa{Pow} to $A\int paulson@6121: B\subseteq A$; subgoal~2 follows similarly: paulson@6121: \index{*Int_lower1 theorem}\index{*Int_lower2 theorem} paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ Int\_lower1\ [THEN\ Pow\_mono])\isanewline paulson@14154: \ 1.\ Pow(A\ \isasyminter \ B)\ \isasymsubseteq \ Pow(B)\isanewline paulson@14154: \ 2.\ Pow(A)\ \isasyminter \ Pow(B)\ \isasymsubseteq \ Pow(A\ \isasyminter \ B) paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ (rule\ Int\_lower2\ [THEN\ Pow\_mono])\isanewline paulson@14154: \ 1.\ Pow(A)\ \isasyminter \ Pow(B)\ \isasymsubseteq \ Pow(A\ \isasyminter \ B) paulson@14154: \end{isabelle} paulson@6121: We are left with the opposite inclusion, which we tackle in the paulson@6121: straightforward way:\index{*subsetI theorem} paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ subsetI)\isanewline paulson@14154: \ 1.\ \isasymAnd x.\ x\ \isasymin \ Pow(A)\ \isasyminter \ Pow(B)\ \isasymLongrightarrow \ x\ \isasymin \ Pow(A\ \isasyminter \ B) paulson@14154: \end{isabelle} paulson@14154: The subgoal is to show $x\in \isa{Pow}(A\cap B)$ assuming $x\in\isa{Pow}(A)\cap \isa{Pow}(B)$; eliminating this assumption produces two paulson@6121: subgoals. The rule \tdx{IntE} treats the intersection like a conjunction paulson@6121: instead of unfolding its definition. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (erule\ IntE)\isanewline paulson@14154: \ 1.\ \isasymAnd x.\ \isasymlbrakk x\ \isasymin \ Pow(A);\ x\ \isasymin \ Pow(B)\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymin \ Pow(A\ \isasyminter \ B) paulson@14154: \end{isabelle} paulson@14154: The next step replaces the \isa{Pow} by the subset paulson@6121: relation~($\subseteq$).\index{*PowI theorem} paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ PowI)\isanewline paulson@14154: \ 1.\ \isasymAnd x.\ \isasymlbrakk x\ \isasymin \ Pow(A);\ x\ \isasymin \ Pow(B)\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymsubseteq \ A\ \isasyminter \ B% paulson@14154: \end{isabelle} paulson@6121: We perform the same replacement in the assumptions. This is a good paulson@14154: demonstration of the tactic \ttindex{drule}:\index{*PowD theorem} paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (drule\ PowD)+\isanewline paulson@14154: \ 1.\ \isasymAnd x.\ \isasymlbrakk x\ \isasymsubseteq \ A;\ x\ \isasymsubseteq \ B\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymsubseteq \ A\ \isasyminter \ B% paulson@14154: \end{isabelle} paulson@6121: The assumptions are that $x$ is a lower bound of both $A$ and~$B$, but paulson@6121: $A\int B$ is the greatest lower bound:\index{*Int_greatest theorem} paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ Int\_greatest)\isanewline paulson@14154: \ 1.\ \isasymAnd x.\ \isasymlbrakk x\ \isasymsubseteq \ A;\ x\ \isasymsubseteq \ B\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymsubseteq \ A\isanewline paulson@14154: \ 2.\ \isasymAnd x.\ \isasymlbrakk x\ \isasymsubseteq \ A;\ x\ \isasymsubseteq \ B\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymsubseteq \ B% paulson@14154: \end{isabelle} paulson@6121: To conclude the proof, we clear up the trivial subgoals: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (assumption+)\isanewline paulson@14154: \isacommand{done}% paulson@14154: \end{isabelle} paulson@14154: paulson@14154: We could have performed this proof instantly by calling paulson@14154: \ttindex{blast}: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "Pow(A\ Int\ B)\ =\ Pow(A)\ Int\ Pow(B)"\isanewline paulson@14154: \isacommand{by} paulson@14154: \end{isabelle} paulson@6121: Past researchers regarded this as a difficult proof, as indeed it is if all paulson@6121: the symbols are replaced by their definitions. paulson@6121: \goodbreak paulson@6121: paulson@6121: \section{Monotonicity of the union operator} paulson@6121: For another example, we prove that general union is monotonic: paulson@6121: ${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$. To begin, we paulson@6121: tackle the inclusion using \tdx{subsetI}: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "C\isasymsubseteq D\ ==>\ Union(C)\ paulson@14154: \isasymsubseteq \ Union(D)"\isanewline paulson@14154: \isacommand{apply}\ (rule\ subsetI)\isanewline paulson@14154: \ 1.\ \isasymAnd x.\ \isasymlbrakk C\ \isasymsubseteq \ D;\ x\ \isasymin \ \isasymUnion C\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymin \ \isasymUnion D% paulson@14154: \end{isabelle} paulson@6121: Big union is like an existential quantifier --- the occurrence in the paulson@6121: assumptions must be eliminated early, since it creates parameters. paulson@6121: \index{*UnionE theorem} paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (erule\ UnionE)\isanewline paulson@14154: \ 1.\ \isasymAnd x\ B.\ \isasymlbrakk C\ \isasymsubseteq \ D;\ x\ \isasymin \ B;\ B\ \isasymin \ C\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymin \ \isasymUnion D% paulson@14154: \end{isabelle} paulson@6121: Now we may apply \tdx{UnionI}, which creates an unknown involving the paulson@14154: parameters. To show \isa{x\ \isasymin \ \isasymUnion D} it suffices to show that~\isa{x} belongs paulson@14154: to some element, say~\isa{?B2(x,B)}, of~\isa{D}\@. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ UnionI)\isanewline paulson@14154: \ 1.\ \isasymAnd x\ B.\ \isasymlbrakk C\ \isasymsubseteq \ D;\ x\ \isasymin \ B;\ B\ \isasymin \ C\isasymrbrakk \ \isasymLongrightarrow \ ?B2(x,\ B)\ \isasymin \ D\isanewline paulson@14154: \ 2.\ \isasymAnd x\ B.\ \isasymlbrakk C\ \isasymsubseteq \ D;\ x\ \isasymin \ B;\ B\ \isasymin \ C\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymin \ ?B2(x,\ B) paulson@14154: \end{isabelle} paulson@14154: Combining the rule \tdx{subsetD} with the assumption \isa{C\ \isasymsubseteq \ D} yields paulson@6121: $\Var{a}\in C \Imp \Var{a}\in D$, which reduces subgoal~1. Note that paulson@14154: \isa{erule} removes the subset assumption. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (erule\ subsetD)\isanewline paulson@14154: \ 1.\ \isasymAnd x\ B.\ \isasymlbrakk x\ \isasymin \ B;\ B\ \isasymin \ C\isasymrbrakk \ \isasymLongrightarrow \ ?B2(x,\ B)\ \isasymin \ C\isanewline paulson@14154: \ 2.\ \isasymAnd x\ B.\ \isasymlbrakk C\ \isasymsubseteq \ D;\ x\ \isasymin \ B;\ B\ \isasymin \ C\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymin \ ?B2(x,\ B) paulson@14154: \end{isabelle} paulson@14154: The rest is routine. Observe how the first call to \isa{assumption} paulson@14154: instantiates \isa{?B2(x,B)} to~\isa{B}\@. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ assumption\ \isanewline paulson@14154: \ 1.\ \isasymAnd x\ B.\ \isasymlbrakk C\ \isasymsubseteq \ D;\ x\ \isasymin \ B;\ B\ \isasymin \ C\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymin \ B% paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ assumption\ \isanewline paulson@14154: No\ subgoals!\isanewline paulson@14154: \isacommand{done}% paulson@14154: \end{isabelle} paulson@14154: Again, \isa{blast} can prove this theorem in one step. paulson@14154: paulson@14154: The theory \isa{ZF/equalities.thy} has many similar proofs. Reasoning about paulson@6121: general intersection can be difficult because of its anomalous behaviour on paulson@14154: the empty set. However, \isa{blast} copes well with these. Here is paulson@6121: a typical example, borrowed from Devlin~\cite[page 12]{devlin79}: paulson@6121: \[ a\in C \,\Imp\, \inter@{x\in C} \Bigl(A(x) \int B(x)\Bigr) = paulson@6121: \Bigl(\inter@{x\in C} A(x)\Bigr) \int paulson@6121: \Bigl(\inter@{x\in C} B(x)\Bigr) \] paulson@6121: paulson@6121: \section{Low-level reasoning about functions} paulson@14154: The derived rules \isa{lamI}, \isa{lamE}, \isa{lam_type}, \isa{beta} paulson@14154: and \isa{eta} support reasoning about functions in a paulson@6121: $\lambda$-calculus style. This is generally easier than regarding paulson@6121: functions as sets of ordered pairs. But sometimes we must look at the paulson@6121: underlying representation, as in the following proof paulson@6121: of~\tdx{fun_disjoint_apply1}. This states that if $f$ and~$g$ are paulson@6121: functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then paulson@6121: $(f\un g)`a = f`a$: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "[|\ a\ \isasymin \ A;\ \ f\ \isasymin \ A->B;\ \ g\ \isasymin \ C->D;\ \ A\ \isasyminter \ C\ =\ 0\ |] paulson@14154: \isanewline paulson@14154: \ \ \ \ \ \ \ \ ==>\ (f\ \isasymunion \ g)`a\ =\ f`a" paulson@14154: \end{isabelle} paulson@6121: Using \tdx{apply_equality}, we reduce the equality to reasoning about paulson@14154: ordered pairs. The second subgoal is to verify that \isa{f\ \isasymunion \ g} is a function, since paulson@14154: \isa{Pi(?A,?B)} denotes a dependent function space. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ apply\_equality)\isanewline paulson@14154: \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \isanewline paulson@14154: \isaindent{\ 1.\ }\isasymLongrightarrow \ \isasymlangle a,\ f\ `\ a\isasymrangle \ \isasymin \ f\ \isasymunion \ g\isanewline paulson@14154: \ 2.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \isanewline paulson@14154: \isaindent{\ 2.\ }\isasymLongrightarrow \ f\ \isasymunion \ g\ \isasymin \ Pi(?A,\ ?B) paulson@14154: \end{isabelle} paulson@6121: We must show that the pair belongs to~$f$ or~$g$; by~\tdx{UnI1} we paulson@6121: choose~$f$: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ UnI1)\isanewline paulson@14154: \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ \isasymlangle a,\ f\ `\ a\isasymrangle \ \isasymin \ f\isanewline paulson@14154: \ 2.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \isanewline paulson@14154: \isaindent{\ 2.\ }\isasymLongrightarrow \ f\ \isasymunion \ g\ \isasymin \ Pi(?A,\ ?B) paulson@14154: \end{isabelle} paulson@6121: To show $\pair{a,f`a}\in f$ we use \tdx{apply_Pair}, which is paulson@6121: essentially the converse of \tdx{apply_equality}: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ apply\_Pair)\isanewline paulson@14154: \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ f\ \isasymin \ Pi(?A2,?B2)\isanewline paulson@14154: \ 2.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ a\ \isasymin \ ?A2\isanewline paulson@14154: \ 3.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \isanewline paulson@14154: \isaindent{\ 3.\ }\isasymLongrightarrow \ f\ \isasymunion \ g\ \isasymin \ Pi(?A,\ ?B) paulson@14154: \end{isabelle} paulson@6121: Using the assumptions $f\in A\to B$ and $a\in A$, we solve the two subgoals paulson@6121: from \tdx{apply_Pair}. Recall that a $\Pi$-set is merely a generalized paulson@14154: function space, and observe that~{\tt?A2} gets instantiated to~\isa{A}. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ assumption\ \isanewline paulson@14154: \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ a\ \isasymin \ A\isanewline paulson@14154: \ 2.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \isanewline paulson@14154: \isaindent{\ 2.\ }\isasymLongrightarrow \ f\ \isasymunion \ g\ \isasymin \ Pi(?A,\ ?B) paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ assumption\ \isanewline paulson@14154: \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \isanewline paulson@14154: \isaindent{\ 1.\ }\isasymLongrightarrow \ f\ \isasymunion \ g\ \isasymin \ Pi(?A,\ ?B) paulson@14154: \end{isabelle} paulson@6121: To construct functions of the form $f\un g$, we apply paulson@6121: \tdx{fun_disjoint_Un}: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ fun\_disjoint\_Un)\isanewline paulson@14154: \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ f\ \isasymin \ ?A3\ \isasymrightarrow \ ?B3\isanewline paulson@14154: \ 2.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ g\ \isasymin \ ?C3\ \isasymrightarrow \ ?D3\isanewline paulson@14154: \ 3.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ ?A3\ \isasyminter \ ?C3\ =\ 0 paulson@14154: \end{isabelle} paulson@6121: The remaining subgoals are instances of the assumptions. Again, observe how paulson@14154: unknowns become instantiated: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ assumption\ \isanewline paulson@14154: \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ g\ \isasymin \ ?C3\ \isasymrightarrow \ ?D3\isanewline paulson@14154: \ 2.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ A\ \isasyminter \ ?C3\ =\ 0 paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ assumption\ \isanewline paulson@14154: \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ A\ \isasyminter \ C\ =\ 0 paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ assumption\ \isanewline paulson@14154: No\ subgoals!\isanewline paulson@14154: \isacommand{done} paulson@14154: \end{isabelle} paulson@14154: See the theories \isa{ZF/func.thy} and \isa{ZF/WF.thy} for more paulson@6121: examples of reasoning about functions. paulson@6121: paulson@6121: \index{set theory|)}