summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/TutorialI/Sets/sets.tex

changeset 10303 | 0bea1c33abef |

child 10341 | 6eb91805a012 |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Sets/sets.tex Mon Oct 23 18:54:47 2000 +0200 @@ -0,0 +1,1040 @@ +\chapter{Sets, Functions and Relations} + +Mathematics relies heavily on set theory: not just unions and intersections +but least fixed points and other concepts. In computer science, sets are +used to formalize grammars, state transition systems, etc. The set theory +of Isabelle/HOL should not be confused with traditional, untyped set +theory, in which everything is a set. There the slogan is `set theory is +the foundation of mathematics.' Our sets are typed. In a given set, all +elements have the same type, say +\isa{T}, and the set itself has type \isa{T set}. Sets are typed in the +same way as lists. + +Relations are simply sets of pairs. This chapter describes +the main operations on relations, such as converse, composition and +transitive closure. Functions are also covered below. They are not sets in +Isabelle/HOL, but (for example) the range of a function is a set, +and the inverse image of a function maps sets to sets. + +This chapter ends with a case study concerning model checking for the +temporal logic CTL\@. Most of the other examples are simple. The +chapter presents a small selection of built-in theorems in order to point +out some key properties of the various constants and to introduce you to +the notation. + +Natural deduction rules are provided for the set theory constants, but they +are seldom used directly, so only a few are presented here. Many formulas +involving sets can be proved automatically or simplified to a great extent. +Expressing your concepts in terms of sets will probably make your proofs +easier. + + +\section{Sets} + +We begin with \textbf{intersection}, \textbf{union} and \textbf{complement} (denoted +by a minus sign). In addition to the \textbf{membership} relation, there +is a symbol for its negation. These points can be seen below. + +Here are the natural deduction rules for intersection. Note the +resemblance to those for conjunction. +\begin{isabelle} +\isasymlbrakk c\ \isasymin\ +A;\ c\ \isasymin\ +B\isasymrbrakk\ \isasymLongrightarrow\ c\ +\isasymin\ A\ \isasyminter\ B% +\rulename{IntI}\isanewline +c\ \isasymin\ A\ \isasyminter\ +B\ \isasymLongrightarrow\ c\ \isasymin\ +A% +\rulename{IntD1}\isanewline +c\ \isasymin\ A\ \isasyminter\ +B\ \isasymLongrightarrow\ c\ \isasymin\ +B% +\rulename{IntD2}% +\end{isabelle} + +Here are two of the many installed theorems concerning set complement: +\begin{isabelle} +(c\ \isasymin\ \isacharminus\ A)\ =\ (c\ \isasymnotin\ A) +\rulename{Compl_iff}\isanewline +\isacharminus\ (A\ \isasymunion\ +B)\ =\ \isacharminus\ +A\ \isasyminter\ \isacharminus\ B +\rulename{Compl_Un} +\end{isabelle} + +Set \textbf{difference} means the same thing as intersection with the +complement of another set. Here we also see the syntax for the +empty set and for the universal set. +\begin{isabelle} +A\ \isasyminter\ (B\ +\isacharminus\ A)\ =\ +\isacharbraceleft{\isacharbraceright} +\rulename{Diff_disjoint}% +\isanewline +A\ \isasymunion\ \isacharminus\ A\ +=\ UNIV% +\rulename{Compl_partition} +\end{isabelle} + +The \textbf{subset} relation holds between two sets just if every element +of one is also an element of the other. This relation is reflexive. These +are its natural deduction rules: +\begin{isabelle} +({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ x\ \isasymin\ B)\ \isasymLongrightarrow\ A\ \isasymsubseteq\ B% +\rulename{subsetI}% +\par\smallskip% \isanewline didn't leave enough space +\isasymlbrakk A\ \isasymsubseteq\ B;\ c\ \isasymin\ +A\isasymrbrakk\ \isasymLongrightarrow\ c\ +\isasymin\ B% +\rulename{subsetD} +\end{isabelle} +In harder proofs, you may need to apply \isa{subsetD} giving a specific term +for~\isa{c}. However, \isa{blast} can instantly prove facts such as this +one: +\begin{isabelle} +(A\ \isasymunion\ B\ +\isasymsubseteq\ C)\ =\ +(A\ \isasymsubseteq\ C\ +\isasymand\ B\ \isasymsubseteq\ +C) +\rulename{Un_subset_iff} +\end{isabelle} +Here is another example, also proved automatically: +\begin{isabelle} +\isacommand{lemma}\ "(A\ +\isasymsubseteq\ -B)\ =\ +(B\ \isasymsubseteq\ +-A)"\isanewline +\isacommand{apply}\ (blast)\isanewline +\isacommand{done} +\end{isabelle} +% +This is the same example using ASCII syntax, illustrating a pitfall: +\begin{isabelle} +\isacommand{lemma}\ "(A\ \isacharless=\ -B)\ =\ (B\ \isacharless=\ +-A)" +\end{isabelle} +% +The proof fails. It is not a statement about sets, due to overloading; +the relation symbol~\isa{<=} can be any relation, not just +subset. +In this general form, the statement is not valid. Putting +in a type constraint forces the variables to denote sets, allowing the +proof to succeed: + +\begin{isabelle} +\isacommand{lemma}\ "((A::\ {\isacharprime}a\ set)\ \isacharless=\ -B)\ =\ (B\ \isacharless=\ +-A)" +\end{isabelle} +Incidentally, \isa{A\ \isasymsubseteq\ -B} asserts that +the sets \isa{A} and \isa{B} are disjoint. + +\medskip +Two sets are \textbf{equal} if they contain the same elements. +This is +the principle of \textbf{extensionality} for sets. +\begin{isabelle} +({\isasymAnd}x.\ (x\ {\isasymin}\ A)\ =\ (x\ {\isasymin}\ B))\ +{\isasymLongrightarrow}\ A\ =\ B +\rulename{set_ext} +\end{isabelle} +Extensionality is often expressed as +$A=B\iff A\subseteq B\conj B\subseteq A$. +The following rules express both +directions of this equivalence. Proving a set equation using +\isa{equalityI} allows the two inclusions to be proved independently. +\begin{isabelle} +\isasymlbrakk A\ \isasymsubseteq\ B;\ B\ \isasymsubseteq\ +A\isasymrbrakk\ \isasymLongrightarrow\ A\ =\ B% +\rulename{equalityI} +\par\smallskip% \isanewline didn't leave enough space +\isasymlbrakk A\ =\ B;\ \isasymlbrakk A\ \isasymsubseteq\ B;\ B\ +\isasymsubseteq\ A\isasymrbrakk\ \isasymLongrightarrow\ P\isasymrbrakk\ +\isasymLongrightarrow\ P% +\rulename{equalityE} +\end{isabelle} + + +\subsection{Finite set notation} + +Finite sets are expressed using the constant {\isa{insert}}, which is +closely related to union: +\begin{isabelle} +insert\ a\ A\ =\ +\isacharbraceleft a\isacharbraceright\ \isasymunion\ +A% +\rulename{insert_is_Un} +\end{isabelle} +% +The finite set expression \isa{\isacharbraceleft +a,b\isacharbraceright} abbreviates +\isa{insert\ a\ (insert\ b\ \isacharbraceleft\isacharbraceright)}. +Many simple facts can be proved automatically: +\begin{isabelle} +\isacommand{lemma}\ +"{\isacharbraceleft}a,b\isacharbraceright\ +\isasymunion\ {\isacharbraceleft}c,d\isacharbraceright\ +=\ +{\isacharbraceleft}a,b,c,d\isacharbraceright"\isanewline +\isacommand{apply}\ +(blast)\isanewline +\isacommand{done} +\end{isabelle} + + +Not everything that we would like to prove is valid. +Consider this try: +\begin{isabelle} +\isacommand{lemma}\ "{\isacharbraceleft}a,b\isacharbraceright\ \isasyminter\ {\isacharbraceleft}b,c\isacharbraceright\ =\ +{\isacharbraceleft}b\isacharbraceright"\isanewline +\isacommand{apply}\ +(auto) +\end{isabelle} +% +The proof fails, leaving the subgoal \isa{b=c}. To see why it +fails, consider a correct version: +\begin{isabelle} +\isacommand{lemma}\ "{\isacharbraceleft}a,b\isacharbraceright\ \isasyminter\ {\isacharbraceleft}b,c\isacharbraceright\ =\ (if\ a=c\ then\ {\isacharbraceleft}a,b\isacharbraceright\ else\ {\isacharbraceleft}b\isacharbraceright)"\isanewline +\isacommand{apply}\ (simp)\isanewline +\isacommand{apply}\ (blast)\isanewline +\isacommand{done}% +\end{isabelle} + +Our mistake was to suppose that the various items were distinct. Another +remark: this proof uses two methods, namely {\isa{simp}} and +{\isa{blast}}. Calling {\isa{simp}} eliminates the +\isa{if}-\isa{then}-\isa{else} expression, which {\isa{blast}} +cannot break down. The combined methods (namely {\isa{force}} and +{\isa{auto}}) can prove this fact in one step. + + +\subsection{Set comprehension} + +A set comprehension expresses the set of all elements that satisfy +a given predicate. Formally, we do not need sets at all. We are +working in higher-order logic, where variables can range over +predicates. The main benefit of using sets is their notation; +we can write \isa{x{\isasymin}A} and \isa{{\isacharbraceleft}z.\ +P\isacharbraceright} where predicates would require writing +\isa{A(x)} and +\isa{{\isasymlambda}z.\ P}. + +These two laws describe the relationship between set +comprehension and the membership relation. +\begin{isabelle} +(a\ \isasymin\ +{\isacharbraceleft}x.\ P\ +x\isacharbraceright)\ =\ +P\ a% +\rulename{mem_Collect_eq}% +\isanewline +{\isacharbraceleft}x.\ x\ \isasymin\ +A\isacharbraceright\ =\ A% +\rulename{Collect_mem_eq} +\end{isabelle} + +Facts such as these have trivial proofs: +\begin{isabelle} +\isacommand{lemma}\ +"{\isacharbraceleft}x.\ P\ x\ \isasymor\ +x\ \isasymin\ A\isacharbraceright\ =\ +{\isacharbraceleft}x.\ P\ x\isacharbraceright\ +\isasymunion\ A" +\par\smallskip +\isacommand{lemma}\ +"{\isacharbraceleft}x.\ P\ x\ +\isasymlongrightarrow\ Q\ x\isacharbraceright\ =\ +\isacharminus{\isacharbraceleft}x.\ P\ x\isacharbraceright\ +\isasymunion\ {\isacharbraceleft}x.\ Q\ +x\isacharbraceright" +\end{isabelle} + +Isabelle has a general syntax for comprehension, which is best +described through an example: +\begin{isabelle} +\isacommand{lemma}\ "{\isacharbraceleft}p*q\ \isacharbar\ p\ q.\ +p{\isasymin}prime\ \isasymand\ q{\isasymin}prime\isacharbraceright\ =\ +\isanewline +\ \ \ \ \ \ \ \ {\isacharbraceleft}z.\ {\isasymexists}p\ q.\ z\ =\ p*q\ +\isasymand\ p{\isasymin}prime\ \isasymand\ +q{\isasymin}prime\isacharbraceright" +\end{isabelle} +The proof is trivial because the left and right hand side +of the expression are synonymous. The syntax appearing on the +left-hand side abbreviates the right-hand side: in this case, all numbers +that are the product of two primes. In general, the syntax provides a neat +way of expressing any set given by an expression built up from variables +under specific constraints. + + + +\subsection{Binding operators} + +Universal and existential quantifications may range over sets, +with the obvious meaning. Here are the natural deduction rules for the +bounded universal quantifier. Occasionally you will need to apply +\isa{bspec} with an explicit instantiation of the variable~\isa{x}: +% +\begin{isabelle} +({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ P\ x)\ \isasymLongrightarrow\ {\isasymforall}x\isasymin +A.\ P\ x% +\rulename{ballI}% +\isanewline +\isasymlbrakk{\isasymforall}x\isasymin A.\ +P\ x;\ x\ \isasymin\ +A\isasymrbrakk\ \isasymLongrightarrow\ P\ +x% +\rulename{bspec} +\end{isabelle} +% +Dually, here are the natural deduction rules for the +bounded existential quantifier. You may need to apply +\isa{bexI} with an explicit instantiation: +\begin{isabelle} +\isasymlbrakk P\ x;\ +x\ \isasymin\ A\isasymrbrakk\ +\isasymLongrightarrow\ +{\isasymexists}x\isasymin A.\ P\ +x% +\rulename{bexI}% +\isanewline +\isasymlbrakk{\isasymexists}x\isasymin A.\ +P\ x;\ {\isasymAnd}x.\ +{\isasymlbrakk}x\ \isasymin\ A;\ +P\ x\isasymrbrakk\ \isasymLongrightarrow\ +Q\isasymrbrakk\ \isasymLongrightarrow\ Q% +\rulename{bexE} +\end{isabelle} + +Unions can be formed over the values of a given set. The syntax is +\isa{\isasymUnion x\isasymin A.\ B} or \isa{UN +x:\ A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law: +\begin{isabelle} +(b\ \isasymin\ +(\isasymUnion x\isasymin A.\ B\ x))\ =\ ({\isasymexists}x\isasymin A.\ +b\ \isasymin\ B\ x) +\rulename{UN_iff} +\end{isabelle} +It has two natural deduction rules similar to those for the existential +quantifier. Sometimes \isa{UN_I} must be applied explicitly: +\begin{isabelle} +\isasymlbrakk a\ \isasymin\ +A;\ b\ \isasymin\ +B\ a\isasymrbrakk\ \isasymLongrightarrow\ +b\ \isasymin\ +({\isasymUnion}x\isasymin A.\ +B\ x) +\rulename{UN_I}% +\isanewline +\isasymlbrakk b\ \isasymin\ +({\isasymUnion}x\isasymin A.\ +B\ x);\ +{\isasymAnd}x.\ {\isasymlbrakk}x\ \isasymin\ +A;\ b\ \isasymin\ +B\ x\isasymrbrakk\ \isasymLongrightarrow\ +R\isasymrbrakk\ \isasymLongrightarrow\ R% +\rulename{UN_E} +\end{isabelle} +% +The following built-in abbreviation lets us express the union +over a \emph{type}: +\begin{isabelle} +\ \ \ \ \ +({\isasymUnion}x.\ B\ x)\ {==}\ +({\isasymUnion}x{\isasymin}UNIV.\ B\ x) +\end{isabelle} +Abbreviations work as you might expect. The term on the left-hand side of +the +\isa{==} symbol is automatically translated to the right-hand side when the +term is parsed, the reverse translation being done when the term is +displayed. + +We may also express the union of a set of sets, written \isa{Union\ C} in +\textsc{ascii}: +\begin{isabelle} +(A\ \isasymin\ \isasymUnion C)\ =\ ({\isasymexists}X\isasymin C.\ A\ +\isasymin\ X) +\rulename{Union_iff} +\end{isabelle} + +Intersections are treated dually, although they seem to be used less often +than unions. The syntax below would be \isa{INT +x:\ A.\ B} and \isa{Inter\ C} in \textsc{ascii}. Among others, these +theorems are available: +\begin{isabelle} +(b\ \isasymin\ +({\isasymInter}x\isasymin A.\ +B\ x))\ +=\ +({\isasymforall}x\isasymin A.\ +b\ \isasymin\ B\ x) +\rulename{INT_iff}% +\isanewline +(A\ \isasymin\ +\isasymInter C)\ =\ +({\isasymforall}X\isasymin C.\ +A\ \isasymin\ X) +\rulename{Inter_iff} +\end{isabelle} + +Isabelle uses logical equivalences such as those above in automatic proof. +Unions, intersections and so forth are not simply replaced by their +definitions. Instead, membership tests are simplified. For example, $x\in +A\cup B$ is replaced by $x\in A\vee x\in B$. + +The internal form of a comprehension involves the constant +\isa{Collect}, which occasionally appears when a goal or theorem +is displayed. For example, \isa{Collect\ P} is the same term as +\isa{{\isacharbraceleft}z.\ P\ x\isacharbraceright}. The same thing can +happen with quantifiers: for example, \isa{Ball\ A\ P} is +\isa{{\isasymforall}z\isasymin A.\ P\ x} and \isa{Bex\ A\ P} is +\isa{{\isasymexists}z\isasymin A.\ P\ x}. For indexed unions and +intersections, you may see the constants \isa{UNION} and \isa{INTER}\@. + +We have only scratched the surface of Isabelle/HOL's set theory. +One primitive not mentioned here is the powerset operator +{\isa{Pow}}. Hundreds of theorems are proved in theory \isa{Set} and its +descendants. + + +\subsection{Finiteness and cardinality} + +The predicate \isa{finite} holds of all finite sets. Isabelle/HOL includes +many familiar theorems about finiteness and cardinality +(\isa{card}). For example, we have theorems concerning the cardinalities +of unions, intersections and the powerset: +% +\begin{isabelle} +{\isasymlbrakk}finite\ A;\ finite\ B\isasymrbrakk\isanewline +\isasymLongrightarrow\ card\ A\ \isacharplus\ card\ B\ =\ card\ (A\ \isasymunion\ B)\ \isacharplus\ card\ (A\ \isasyminter\ B) +\rulename{card_Un_Int}% +\isanewline +\isanewline +finite\ A\ \isasymLongrightarrow\ card\ +(Pow\ A)\ =\ 2\ \isacharcircum\ card\ A% +\rulename{card_Pow}% +\isanewline +\isanewline +finite\ A\ \isasymLongrightarrow\isanewline +card\ {\isacharbraceleft}B.\ B\ \isasymsubseteq\ +A\ \isasymand\ card\ B\ =\ +k\isacharbraceright\ =\ card\ A\ choose\ k% +\rulename{n_subsets} +\end{isabelle} +Writing $|A|$ as $n$, the last of these theorems says that the number of +$k$-element subsets of~$A$ is $n \choose k$. + +\emph{Note}: the term \isa{Finite\ A} is an abbreviation for +\isa{A\ \isasymin\ Finites}, where the constant \isa{Finites} denotes the +set of all finite sets of a given type. So there is no constant +\isa{Finite}. + + +\section{Functions} + +This section describes a few concepts that involve functions. +Some of the more important theorems are given along with the +names. A few sample proofs appear. Unlike with set theory, however, +we cannot simply state lemmas and expect them to be proved using {\isa{blast}}. + +Two functions are \textbf{equal} if they yield equal results given equal arguments. +This is the principle of \textbf{extensionality} for functions: +\begin{isabelle} +({\isasymAnd}x.\ f\ x\ =\ g\ x)\ {\isasymLongrightarrow}\ f\ =\ g +\rulename{ext} +\end{isabelle} + + +Function \textbf{update} is useful for modelling machine states. It has +the obvious definition and many useful facts are proved about +it. In particular, the following equation is installed as a simplification +rule: +\begin{isabelle} +(f(x:=y))\ z\ =\ (if\ z\ =\ x\ then\ y\ else\ f\ z) +\rulename{fun_upd_apply} +\end{isabelle} +Two syntactic points must be noted. In +\isa{(f(x:=y))\ z} we are applying an updated function to an +argument; the outer parentheses are essential. A series of two or more +updates can be abbreviated as shown on the left-hand side of this theorem: +\begin{isabelle} +f(x:=y,\ x:=z)\ =\ f(x:=z) +\rulename{fun_upd_upd} +\end{isabelle} +Note also that we can write \isa{f(x:=z)} with only one pair of parentheses +when it is not being applied to an argument. + +\medskip +The \textbf{identity} function and function \textbf{composition} are defined as +follows: +\begin{isabelle}% +id\ \isasymequiv\ {\isasymlambda}x.\ x% +\rulename{id_def}\isanewline +f\ \isasymcirc\ g\ \isasymequiv\ +{\isasymlambda}x.\ f\ +(g\ x)% +\rulename{o_def} +\end{isabelle} +% +Many familiar theorems concerning the identity and composition +are proved. For example, we have the associativity of composition: +\begin{isabelle} +f\ \isasymcirc\ (g\ \isasymcirc\ h)\ =\ f\ \isasymcirc\ g\ \isasymcirc\ h +\rulename{o_assoc} +\end{isabelle} + +\medskip + +A function may be \textbf{injective}, \textbf{surjective} or \textbf{bijective}: +\begin{isabelle} +inj_on\ f\ A\ \isasymequiv\ {\isasymforall}x\isasymin A.\ +{\isasymforall}y\isasymin A.\ f\ x\ =\ f\ y\ \isasymlongrightarrow\ x\ +=\ y% +\rulename{inj_on_def}\isanewline +surj\ f\ \isasymequiv\ {\isasymforall}y.\ +{\isasymexists}x.\ y\ =\ f\ x% +\rulename{surj_def}\isanewline +bij\ f\ \isasymequiv\ inj\ f\ \isasymand\ surj\ f +\rulename{bij_def} +\end{isabelle} +The second argument +of \isa{inj_on} lets us express that a function is injective over a +given set. This refinement is useful in higher-order logic, where +functions are total; in some cases, a function's natural domain is a subset +of its domain type. Writing \isa{inj\ f} abbreviates \isa{inj_on\ f\ +UNIV}, for when \isa{f} is injective everywhere. + +The operator {\isa{inv}} expresses the \textbf{inverse} of a function. In +general the inverse may not be well behaved. We have the usual laws, +such as these: +\begin{isabelle} +inj\ f\ \ \isasymLongrightarrow\ inv\ f\ (f\ x)\ =\ x% +\rulename{inv_f_f}\isanewline +surj\ f\ \isasymLongrightarrow\ f\ (inv\ f\ y)\ =\ y +\rulename{surj_f_inv_f}\isanewline +bij\ f\ \ \isasymLongrightarrow\ inv\ (inv\ f)\ =\ f +\rulename{inv_inv_eq} +\end{isabelle} +% +%Other useful facts are that the inverse of an injection +%is a surjection and vice versa; the inverse of a bijection is +%a bijection. +%\begin{isabelle} +%inj\ f\ \isasymLongrightarrow\ surj\ +%(inv\ f) +%\rulename{inj_imp_surj_inv}\isanewline +%surj\ f\ \isasymLongrightarrow\ inj\ (inv\ f) +%\rulename{surj_imp_inj_inv}\isanewline +%bij\ f\ \isasymLongrightarrow\ bij\ (inv\ f) +%\rulename{bij_imp_bij_inv} +%\end{isabelle} +% +%The converses of these results fail. Unless a function is +%well behaved, little can be said about its inverse. Here is another +%law: +%\begin{isabelle} +%{\isasymlbrakk}bij\ f;\ bij\ g\isasymrbrakk\ \isasymLongrightarrow\ inv\ (f\ \isasymcirc\ g)\ =\ inv\ g\ \isasymcirc\ inv\ f% +%\rulename{o_inv_distrib} +%\end{isabelle} + +Theorems involving these concepts can be hard to prove. The following +example is easy, but it cannot be proved automatically. To begin +with, we need a law that relates the quality of functions to +equality over all arguments: +\begin{isabelle} +(f\ =\ g)\ =\ ({\isasymforall}x.\ f\ x\ =\ g\ x) +\rulename{expand_fun_eq} +\end{isabelle} + +This is just a restatement of extensionality. Our lemma states +that an injection can be cancelled from the left +side of function composition: +\begin{isabelle} +\isacommand{lemma}\ "inj\ f\ \isasymLongrightarrow\ (f\ o\ g\ =\ f\ o\ h)\ =\ (g\ =\ h)"\isanewline +\isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def\ o_def)\isanewline +\isacommand{apply}\ (auto)\isanewline +\isacommand{done} +\end{isabelle} + +The first step of the proof invokes extensionality and the definitions +of injectiveness and composition. It leaves one subgoal: +\begin{isabelle} +%inj\ f\ \isasymLongrightarrow\ (f\ \isasymcirc\ g\ =\ f\ \isasymcirc\ h)\ +%=\ (g\ =\ h)\isanewline +\ 1.\ {\isasymforall}x\ y.\ f\ x\ =\ f\ y\ \isasymlongrightarrow\ x\ =\ y\ \isasymLongrightarrow\isanewline +\ \ \ \ ({\isasymforall}x.\ f\ (g\ x)\ =\ f\ (h\ x))\ =\ ({\isasymforall}x.\ g\ x\ =\ h\ x) +\end{isabelle} +This can be proved using the {\isa{auto}} method. + +\medskip + +The \textbf{image} of a set under a function is a most useful notion. It +has the obvious definition: +\begin{isabelle} +f\ ``\ A\ \isasymequiv\ {\isacharbraceleft}y.\ {\isasymexists}x\isasymin +A.\ y\ =\ f\ x\isacharbraceright +\rulename{image_def} +\end{isabelle} +% +Here are some of the many facts proved about image: +\begin{isabelle} +(f\ \isasymcirc\ g)\ ``\ r\ =\ f\ ``\ g\ ``\ r +\rulename{image_compose}\isanewline +f``(A\ \isasymunion\ B)\ =\ f``A\ \isasymunion\ f``B +\rulename{image_Un}\isanewline +inj\ f\ \isasymLongrightarrow\ f``(A\ \isasyminter\ +B)\ =\ f``A\ \isasyminter\ f``B +\rulename{image_Int} +%\isanewline +%bij\ f\ \isasymLongrightarrow\ f\ ``\ (-\ A)\ =\ \isacharminus\ f\ ``\ A% +%\rulename{bij_image_Compl_eq} +\end{isabelle} + + +Laws involving image can often be proved automatically. Here +are two examples, illustrating connections with indexed union and with the +general syntax for comprehension: +\begin{isabelle} +\isacommand{lemma}\ "f``A\ \isasymunion\ g``A\ =\ ({\isasymUnion}x{\isasymin}A.\ {\isacharbraceleft}f\ x,\ g\ +x\isacharbraceright) +\par\smallskip +\isacommand{lemma}\ "f\ ``\ \isacharbraceleft(x,y){.}\ P\ x\ y\isacharbraceright\ =\ {\isacharbraceleft}f(x,y)\ \isacharbar\ x\ y.\ P\ x\ +y\isacharbraceright" +\end{isabelle} + +\medskip + A function's \textbf{range} is the set of values that the function can +take on. It is, in fact, the image of the universal set under +that function. There is no constant {\isa{range}}. Instead, {\isa{range}} +abbreviates an application of image to {\isa{UNIV}}: +\begin{isabelle} +\ \ \ \ \ range\ f\ +{==}\ f``UNIV +\end{isabelle} +% +Few theorems are proved specifically +for {\isa{range}}; in most cases, you should look for a more general +theorem concerning images. + +\medskip +\textbf{Inverse image} is also useful. It is defined as follows: +\begin{isabelle} +f\ \isacharminus``\ B\ \isasymequiv\ {\isacharbraceleft}x.\ f\ x\ \isasymin\ B\isacharbraceright +\rulename{vimage_def} +\end{isabelle} +% +This is one of the facts proved about it: +\begin{isabelle} +f\ \isacharminus``\ (-\ A)\ =\ \isacharminus\ f\ \isacharminus``\ A% +\rulename{vimage_Compl} +\end{isabelle} + + +\section{Relations} + +A \textbf{relation} is a set of pairs. As such, the set operations apply +to them. For instance, we may form the union of two relations. Other +primitives are defined specifically for relations. + +The \textbf{identity} relation, also known as equality, has the obvious +definition: +\begin{isabelle} +Id\ \isasymequiv\ {\isacharbraceleft}p.\ {\isasymexists}x.\ p\ =\ (x,x){\isacharbraceright}% +\rulename{Id_def} +\end{isabelle} + +\textbf{Composition} of relations (the infix \isa{O}) is also available: +\begin{isabelle} +r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z){.}\ {\isasymexists}y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright +\rulename{comp_def} +\end{isabelle} + +This is one of the many lemmas proved about these concepts: +\begin{isabelle} +R\ O\ Id\ =\ R +\rulename{R_O_Id} +\end{isabelle} +% +Composition is monotonic, as are most of the primitives appearing +in this chapter. We have many theorems similar to the following +one: +\begin{isabelle} +\isasymlbrakk r\isacharprime\ \isasymsubseteq\ r;\ s\isacharprime\ +\isasymsubseteq\ s\isasymrbrakk\ \isasymLongrightarrow\ r\isacharprime\ O\ +s\isacharprime\ \isasymsubseteq\ r\ O\ s% +\rulename{comp_mono} +\end{isabelle} + +The \textbf{converse} or inverse of a relation exchanges the roles +of the two operands. Note that \isa{\isacharcircum-1} is a postfix +operator. +\begin{isabelle} +((a,b)\ \isasymin\ r\isacharcircum-1)\ =\ +((b,a)\ \isasymin\ r) +\rulename{converse_iff} +\end{isabelle} +% +Here is a typical law proved about converse and composition: +\begin{isabelle} +(r\ O\ s){\isacharcircum}\isacharminus1\ =\ s\isacharcircum-1\ O\ r\isacharcircum-1 +\rulename{converse_comp} +\end{isabelle} + + +The \textbf{image} of a set under a relation is defined analogously +to image under a function: +\begin{isabelle} +(b\ \isasymin\ r\ \isacharcircum{\isacharcircum}\ A)\ =\ ({\isasymexists}x\isasymin +A.\ (x,b)\ \isasymin\ r) +\rulename{Image_iff} +\end{isabelle} +It satisfies many similar laws. + +%Image under relations, like image under functions, distributes over unions: +%\begin{isabelle} +%r\ \isacharcircum{\isacharcircum}\ +%({\isasymUnion}x\isasyminA.\ +%B\ +%x)\ =\ +%({\isasymUnion}x\isasyminA.\ +%r\ \isacharcircum{\isacharcircum}\ B\ +%x) +%\rulename{Image_UN} +%\end{isabelle} + + +The \textbf{domain} and \textbf{range} of a relation are defined in the +standard way: +\begin{isabelle} +(a\ \isasymin\ Domain\ r)\ =\ ({\isasymexists}y.\ (a,y)\ \isasymin\ +r) +\rulename{Domain_iff}% +\isanewline +(a\ \isasymin\ Range\ r)\ +\ =\ ({\isasymexists}y.\ +(y,a)\ +\isasymin\ r) +\rulename{Range_iff} +\end{isabelle} + +Iterated composition of a relation is available. The notation overloads +that of exponentiation: +\begin{isabelle} +R\ \isacharcircum\ \isadigit{0}\ =\ Id\isanewline +R\ \isacharcircum\ Suc\ n\ =\ R\ O\ R\isacharcircum n +\rulename{RelPow.relpow.simps} +\end{isabelle} + +The \textbf{reflexive transitive closure} of a relation is particularly +important. It has the postfix syntax \isa{r\isacharcircum{*}}. The +construction is defined to be the least fixedpoint satisfying the +following equation: +\begin{isabelle} +r\isacharcircum{*}\ =\ Id\ \isasymunion\ (r\ O\ r\isacharcircum{*}) +\rulename{rtrancl_unfold} +\end{isabelle} +% +Among its basic properties are three that serve as introduction +rules: +\begin{isabelle} +(a,a)\ \isasymin\ +r\isacharcircum{*} +\rulename{rtrancl_refl}% +\isanewline +p\ \isasymin\ r\ \isasymLongrightarrow\ +p\ \isasymin\ +r\isacharcircum{*} +\rulename{r_into_rtrancl}% +\isanewline +\isasymlbrakk(a,b)\ \isasymin\ +r\isacharcircum{*};\ +(b,c)\ \isasymin\ r\isacharcircum{*}\isasymrbrakk\ +\isasymLongrightarrow\ +(a,c)\ \isasymin\ r\isacharcircum{*} +\rulename{rtrancl_trans} +\end{isabelle} +% +Induction over the reflexive transitive closure is available: +\begin{isabelle} +\isasymlbrakk(a,b)\ \isasymin\ r\isacharcircum{*};\ P\ a;\isanewline +\ \ {\isasymAnd}y\ z.\ +\isasymlbrakk(a,y)\ \isasymin\ r\isacharcircum{*};\ +(y,z)\ \isasymin\ r;\ P\ y\isasymrbrakk\ +\isasymLongrightarrow\ P\ z\isasymrbrakk\isanewline +\isasymLongrightarrow\ P\ b% +\rulename{rtrancl_induct} +\end{isabelle} +% +Here is one of the many laws proved about the reflexive transitive +closure: +\begin{isabelle} +(r\isacharcircum{*}){\isacharcircum}*\ =\ r\isacharcircum{*} +\rulename{rtrancl_idemp} +\end{isabelle} + +The transitive closure is similar. It has two +introduction rules: +\begin{isabelle} +p\ \isasymin\ r\ \isasymLongrightarrow\ p\ \isasymin\ r\isacharcircum{\isacharplus} +\rulename{r_into_trancl}\isanewline +\isasymlbrakk(a,b)\ \isasymin\ +r\isacharcircum{\isacharplus};\ (b,c)\ +\isasymin\ r\isacharcircum{\isacharplus}\isasymrbrakk\ +\isasymLongrightarrow\ (a,c)\ \isasymin\ +r\isacharcircum{\isacharplus} +\rulename{trancl_trans} +\end{isabelle} +% +The induction rule is similar to the one shown above. +A typical lemma states that transitive closure commutes with the converse +operator: +\begin{isabelle} +(r\isacharcircum-1){\isacharcircum}\isacharplus\ =\ (r\isacharcircum{\isacharplus}){\isacharcircum}\isacharminus1 +\rulename{trancl_converse} +\end{isabelle} + + +The reflexive transitive closure also commutes with the converse. +Let us examine the proof. Each direction of the equivalence is +proved separately. The two proofs are almost identical. Here +is the first one: +\begin{isabelle} +\isacommand{lemma}\ rtrancl_converseD:\ "(x,y)\ \isasymin\ (r\isacharcircum-1){\isacharcircum}*\ \isasymLongrightarrow\ (x,y)\ \isasymin\ (r\isacharcircum{*}){\isacharcircum}\isacharminus1"\isanewline +\isacommand{apply}\ (erule\ +rtrancl_induct)\isanewline +\ \isacommand{apply}\ (rule\ rtrancl_refl)\isanewline +\isacommand{apply}\ (blast\ intro:\ r_into_rtrancl\ rtrancl_trans)\isanewline +\isacommand{done} +\end{isabelle} + +The first step of the proof applies induction, leaving these subgoals: +\begin{isabelle} +\ 1.\ (x,x)\ \isasymin\ r\isacharcircum{*}\isanewline +\ 2.\ {\isasymAnd}y\ z.\ \isasymlbrakk(x,y)\ \isasymin\ (r\isacharcircum-1){\isacharcircum}*;\ (y,z)\ \isasymin\ r\isacharcircum-1;\ (y,x)\ \isasymin\ r\isacharcircum{*}\isasymrbrakk\isanewline +\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ (z,x)\ \isasymin\ r\isacharcircum{*} +\end{isabelle} + +The first subgoal is trivial by reflexivity. The second follows +by first eliminating the converse operator, yielding the +assumption \isa{(z,y)\ +\isasymin\ r}, and then +applying the introduction rules shown above. The same proof script handles +the other direction: +\begin{isabelle} +\isacommand{lemma}\ rtrancl_converseI:\ "(x,y)\ \isasymin\ (r\isacharcircum{*}){\isacharcircum}\isacharminus1\ \isasymLongrightarrow\ (x,y)\ \isasymin\ (r\isacharcircum-1){\isacharcircum}*"\isanewline +\isacommand{apply}\ (drule\ converseD)\isanewline +\isacommand{apply}\ (erule\ rtrancl_induct)\isanewline +\ \isacommand{apply}\ (rule\ rtrancl_refl)\isanewline +\isacommand{apply}\ (blast\ intro:\ r_into_rtrancl\ rtrancl_trans)\isanewline +\isacommand{done} +\end{isabelle} + + +Finally, we combine the two lemmas to prove the desired equation: +\begin{isabelle} +\isacommand{lemma}\ rtrancl_converse:\ "(r\isacharcircum-1){\isacharcircum}*\ =\ (r\isacharcircum{*}){\isacharcircum}\isacharminus1"\isanewline +\isacommand{apply}\ (auto\ intro:\ +rtrancl_converseI\ dest:\ +rtrancl_converseD)\isanewline +\isacommand{done} +\end{isabelle} + +Note one detail. The {\isa{auto}} method can prove this but +{\isa{blast}} cannot. \remark{move to a later section?} +This is because the +lemmas we have proved only apply to ordered pairs. {\isa{Auto}} can +convert a bound variable of a product type into a pair of bound variables, +allowing the lemmas to be applied. A toy example demonstrates this +point: +\begin{isabelle} +\isacommand{lemma}\ "A\ \isasymsubseteq\ Id"\isanewline +\isacommand{apply}\ (rule\ subsetI)\isanewline +\isacommand{apply}\ (auto) +\end{isabelle} +Applying the introduction rule \isa{subsetI} leaves the goal of showing +that an arbitrary element of~\isa{A} belongs to~\isa{Id}. +\begin{isabelle} +A\ \isasymsubseteq\ Id\isanewline +\ 1.\ {\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ x\ \isasymin\ Id +\end{isabelle} +The \isa{simp} and \isa{blast} methods can do nothing here. However, +\isa{x} is of product type and therefore denotes an ordered pair. The +\isa{auto} method (and some others, including \isa{clarify}) +can replace +\isa{x} by a pair, which then allows the further simplification from +\isa{(a,b)\ \isasymin\ A} to \isa{a\ =\ b}. +\begin{isabelle} +A\ \isasymsubseteq\ Id\isanewline +\ 1.\ {\isasymAnd}a\ b.\ (a,b)\ \isasymin\ A\ \isasymLongrightarrow\ a\ =\ b +\end{isabelle} + + + +\section{Well-founded relations and induction} + +Induction comes in many forms, including traditional mathematical +induction, structural induction on lists and induction on size. +More general than these is induction over a well-founded relation. +Such A relation expresses the notion of a terminating process. +Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no +infinite descending chains +\[ \cdots \prec a@2 \prec a@1 \prec a@0. \] +If $\prec$ is well-founded then it can be used with the well-founded +induction rule: +\[ \infer{P(a)}{\infer*{P(x)}{[\forall y.\, y\prec x \imp P(y)]}} \] +To show $P(a)$ for a particular term~$a$, it suffices to show $P(x)$ for +arbitrary~$x$ under the assumption that $P(y)$ holds for $y\prec x$. +Intuitively, the well-foundedness of $\prec$ ensures that the chains of +reasoning are finite. + +In Isabelle, the induction rule is expressed like this: +\begin{isabelle} +{\isasymlbrakk}wf\ r;\ + {\isasymAnd}x.\ {\isasymforall}y.\ (y,x)\ \isasymin\ r\ +\isasymlongrightarrow\ P\ y\ \isasymLongrightarrow\ P\ x\isasymrbrakk\ +\isasymLongrightarrow\ P\ a +\rulename{wf_induct} +\end{isabelle} +Here \isa{wf\ r} expresses that relation~\isa{r} is well-founded. + +Many familiar induction principles are instances of this rule. +For example, the predecessor relation on the natural numbers +is well-founded; induction over it is mathematical induction. +The `tail of' relation on lists is well-founded; induction over +it is structural induction. + +Well-foundedness can be difficult to show. The various equivalent +formulations are all hard to use formally. However, often a relation +is obviously well-founded by construction. The HOL library provides +several theorems concerning ways of constructing a well-founded relation. +For example, a relation can be defined by means of a measure function +involving an existing relation, or two relations can be +combined lexicographically. + +The library declares \isa{less_than} as a relation object, +that is, a set of pairs of natural numbers. Two theorems tell us that this +relation behaves as expected and that it is well-founded: +\begin{isabelle} +((x,y)\ \isasymin\ less_than)\ =\ (x\ <\ y) +\rulename{less_than_iff}\isanewline +wf\ less_than +\rulename{wf_less_than} +\end{isabelle} + +The notion of measure generalizes to the \textbf{inverse image} of +relation. Given a relation~\isa{r} and a function~\isa{f}, we express a new +relation using \isa{f} as a measure. An infinite descending chain on this +new relation would give rise to an infinite descending chain on~\isa{r}. +The library holds the definition of this concept and a theorem stating +that it preserves well-foundedness: +\begin{isabelle} +inv_image\ r\ f\ \isasymequiv\ \isacharbraceleft(x,y).\ (f\ x,\ f\ y)\ +\isasymin\ r\isacharbraceright +\rulename{inv_image_def}\isanewline +wf\ r\ \isasymLongrightarrow\ wf\ (inv_image\ r\ f) +\rulename{wf_inv_image} +\end{isabelle} + +The most familiar notion of measure involves the natural numbers. This yields, +for example, induction on the length of the list or the size +of a tree. The library defines \isa{measure} specifically: +\begin{isabelle} +measure\ \isasymequiv\ inv_image\ less_than% +\rulename{measure_def}\isanewline +wf\ (measure\ f) +\rulename{wf_measure} +\end{isabelle} + +Of the other constructions, the most important is the \textbf{lexicographic +product} of two relations. It expresses the standard dictionary +ordering over pairs. We write \isa{ra\ <*lex*>\ rb}, where \isa{ra} +and \isa{rb} are the two operands. The lexicographic product satisfies the +usual definition and it preserves well-foundedness: +\begin{isabelle} +ra\ <*lex*>\ rb\ \isasymequiv \isanewline +\ \ \isacharbraceleft ((a,b),(a',b')).\ (a,a')\ \isasymin \ ra\ +\isasymor\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \,a=a'\ \isasymand \ (b,b')\ +\isasymin \ rb\isacharbraceright +\rulename{lex_prod_def}% +\par\smallskip +\isasymlbrakk wf\ ra;\ wf\ rb\isasymrbrakk \ \isasymLongrightarrow \ wf\ (ra\ <*lex*>\ rb) +\rulename{wf_lex_prod} +\end{isabelle} + +These constructions can be used in a +\textbf{recdef} declaration (\S\ref{sec:recdef-simplification}) to define +the well-founded relation used to prove termination. + + + + + +\section{Fixed point operators} + +Fixed point operators define sets recursively. Most users invoke +them through Isabelle's inductive definition facility, which +is discussed later. However, they can be invoked directly. The \textbf{least} +or \textbf{strongest} fixed point yields an inductive definition; +the \textbf{greatest} or \textbf{weakest} fixed point yields a coinductive +definition. Mathematicians may wish to note that the existence +of these fixed points is guaranteed by the Knaster-Tarski theorem. + + +The theory works applies only to monotonic functions. Isabelle's +definition of monotone is overloaded over all orderings: +\begin{isabelle} +mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B% +\rulename{mono_def} +\end{isabelle} +% +For fixed point operators, the ordering will be the subset relation: if +$A\subseteq B$ then we expect $f(A)\subseteq f(B)$. In addition to its +definition, monotonicity has the obvious introduction and destruction +rules: +\begin{isabelle} +({\isasymAnd}A\ B.\ A\ \isasymle\ B\ \isasymLongrightarrow\ f\ A\ \isasymle\ f\ B)\ \isasymLongrightarrow\ mono\ f% +\rulename{monoI}% +\par\smallskip% \isanewline didn't leave enough space +{\isasymlbrakk}mono\ f;\ A\ \isasymle\ B\isasymrbrakk\ +\isasymLongrightarrow\ f\ A\ \isasymle\ f\ B% +\rulename{monoD} +\end{isabelle} + +The most important properties of the least fixed point are that +it is a fixed point and that it enjoys an induction rule: +\begin{isabelle} +mono\ f\ \isasymLongrightarrow\ lfp\ f\ =\ f\ (lfp\ f) +\rulename{lfp_unfold}% +\par\smallskip% \isanewline didn't leave enough space +{\isasymlbrakk}a\ \isasymin\ lfp\ f;\ mono\ f;\isanewline + \ {\isasymAnd}x.\ x\ +\isasymin\ f\ (lfp\ f\ \isasyminter\ {\isacharbraceleft}x.\ P\ +x\isacharbraceright)\ \isasymLongrightarrow\ P\ x\isasymrbrakk\ +\isasymLongrightarrow\ P\ a% +\rulename{lfp_induct} +\end{isabelle} +% +The induction rule shown above is more convenient than the basic +one derived from the minimality of {\isa{lfp}}. Observe that both theorems +demand \isa{mono\ f} as a premise. + +The greatest fixed point is similar, but it has a \textbf{coinduction} rule: +\begin{isabelle} +mono\ f\ \isasymLongrightarrow\ gfp\ f\ =\ f\ (gfp\ f) +\rulename{gfp_unfold}% +\isanewline +{\isasymlbrakk}mono\ f;\ a\ \isasymin\ X;\ X\ \isasymsubseteq\ f\ (X\ +\isasymunion\ gfp\ f)\isasymrbrakk\ \isasymLongrightarrow\ a\ \isasymin\ +gfp\ f% +\rulename{coinduct} +\end{isabelle} +A \textbf{bisimulation} is perhaps the best-known concept defined as a +greatest fixed point. Exhibiting a bisimulation to prove the equality of +two agents in a process algebra is an example of coinduction. +The coinduction rule can be strengthened in various ways; see +theory {\isa{Gfp}} for details. +An example using the fixed point operators appears later in this +chapter, in the section on computation tree logic +(\S\ref{sec:ctl-case-study}).