doc-src/TutorialI/Sets/sets.tex

added Permutation;

% $Id$
\chapter{Sets, Functions and Relations}

\REMARK{The old version used lots of bold. I've cut down,
changing some \texttt{textbf} to \texttt{relax}. This can be undone.
See the source.}
Mathematics relies heavily on set theory: not just unions and intersections
but images, 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.  Our sets are  typed. In a given set,
all elements have the same type, say~$\tau$,  and the set itself has type
\isa{$\tau$~set}. 

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.  They are not sets in
Isabelle/HOL, but many of their properties concern sets.  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 \relax{intersection}, \relax{union} and
\relax{complement}. In addition to the
\relax{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.
Note that it is denoted by a minus sign.
\begin{isabelle}
(c\ \isasymin\ -\ A)\ =\ (c\ \isasymnotin\ A)
\rulename{Compl_iff}\isanewline
-\ (A\ \isasymunion\ B)\ =\ -\ A\ \isasyminter\ -\ B
\rulename{Compl_Un}
\end{isabelle}

Set \relax{difference} is the intersection of a set 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\ -\ A)\ =\ \isacharbraceleft\isacharbraceright
\rulename{Diff_disjoint}\isanewline
A\ \isasymunion\ -\ A\ =\ UNIV%
\rulename{Compl_partition}
\end{isabelle}

The \relax{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{by}\ blast
\end{isabelle}
%
This is the same example using \textsc{ascii} syntax, illustrating a pitfall: 
\begin{isabelle}
\isacommand{lemma}\ "(A\ <=\ -B)\ =\ (B\ <=\ -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)\ <=\ -B)\ =\ (B\ <=\
-A)"
\end{isabelle}
Section~\ref{sec:axclass} below describes overloading.  Incidentally,
\isa{A~\isasymsubseteq~-B} asserts that the sets \isa{A} and \isa{B} are
disjoint.

\medskip
Two sets are \relax{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
a form of 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 facts about finite sets 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{by}\ blast
\end{isabelle}


Not everything that we would like to prove is valid. 
Consider this attempt: 
\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{by}\ blast
\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}

The set comprehension \isa{\isacharbraceleft x.\
P\isacharbraceright} expresses the set of all elements that satisfy the
predicate~\isa{P}.  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}

\smallskip
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\ =\
-\isacharbraceleft x.\ P\ x\isacharbraceright\
\isasymunion\ \isacharbraceleft x.\ Q\ x\isacharbraceright"
\end{isabelle}

\smallskip
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.  The syntax provides a neat
way of expressing any set given by an expression built up from variables
under specific constraints.  The drawback is that it hides the true form of
the expression, with its existential quantifiers. 

\smallskip
\emph{Remark}.  We do not need sets at all.  They are essentially equivalent
to predicate variables, which are allowed in  higher-order logic.  The main
benefit of 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}. 


\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
\mbox{\isa{\isasymUnion x\isasymin A.\ B}} or \isa{UN
x\isasymin 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)\ {\isasymrightleftharpoons}\
({\isasymUnion}x{\isasymin}UNIV.\ B\ x)
\end{isabelle}
Abbreviations work as you might expect.  The term on the left-hand side of
the
\indexboldpos{\isasymrightleftharpoons}{$IsaEqq} 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 $\binom{n}{k}$.

\begin{warn}
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.  There is no constant
\isa{Finite}.
\end{warn}
 

\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}. 

\subsection{Function Basics}

Two functions are \relax{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 \relax{identity} function and function \relax{composition} are defined:
\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}

\subsection{Injections, Surjections, Bijections}

A function may be \relax{injective}, \relax{surjective} or \relax{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 \relax{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 equality 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)\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}
\ 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. 


\subsection{Function Image}

The \relax{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)\ =\ -\ 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\
{\isasymrightleftharpoons}\ 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
\relax{Inverse image} is also  useful. It is defined as follows: 
\begin{isabelle}
f\ -`\ 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\ -`\ (-\ A)\ =\ -\ f\ -`\ A%
\rulename{vimage_Compl}
\end{isabelle}


\section{Relations}
\label{sec:Relations}

A \relax{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. 

\subsection{Relation Basics}

The \relax{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}

\relax{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 \relax{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}-1\ =\ s\isacharcircum-1\ O\ r\isacharcircum-1
\rulename{converse_comp}
\end{isabelle}

The \relax{image} of a set under a relation is defined analogously 
to image under a function: 
\begin{isabelle}
(b\ \isasymin\ r\ ``\ 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\ ``\ 
%({\isasymUnion}x\isasyminA.\
%B\
%x)\ =\ 
%({\isasymUnion}x\isasyminA.\
%r\ ``\ B\
%x)
%\rulename{Image_UN}
%\end{isabelle}


The \relax{domain} and \relax{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}

\subsection{The Reflexive Transitive Closure}

The \relax{reflexive transitive closure} of the
relation~\isa{r} is written with the
postfix syntax \isa{r\isacharcircum{*}} and appears in X-symbol notation
as~\isa{r\isactrlsup *}.  It is the least solution of the equation
\begin{isabelle}
r\isactrlsup *\ =\ Id\ \isasymunion \ (r\ O\ r\isactrlsup *)
\rulename{rtrancl_unfold}
\end{isabelle}
%
Among its basic properties are three that serve as introduction 
rules:
\begin{isabelle}
(a,\ a)\ \isasymin \ r\isactrlsup *
\rulename{rtrancl_refl}\isanewline
p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup *
\rulename{r_into_rtrancl}\isanewline
\isasymlbrakk (a,b)\ \isasymin \ r\isactrlsup *;\ 
(b,c)\ \isasymin \ r\isactrlsup *\isasymrbrakk \ \isasymLongrightarrow \
(a,c)\ \isasymin \ r\isactrlsup *
\rulename{rtrancl_trans}
\end{isabelle}
%
Induction over the reflexive transitive closure is available: 
\begin{isabelle}
\isasymlbrakk (a,\ b)\ \isasymin \ r\isactrlsup *;\ P\ a;\ \isasymAnd y\ z.\ \isasymlbrakk (a,\ y)\ \isasymin \ r\isactrlsup *;\ (y,\ z)\ \isasymin \ r;\ P\ y\isasymrbrakk \ \isasymLongrightarrow \ P\ z\isasymrbrakk \isanewline
\isasymLongrightarrow \ P\ b%
\rulename{rtrancl_induct}
\end{isabelle}
%
Idempotence is one of the laws proved about the reflexive transitive 
closure: 
\begin{isabelle}
(r\isactrlsup *)\isactrlsup *\ =\ r\isactrlsup *
\rulename{rtrancl_idemp}
\end{isabelle}

\smallskip
The transitive closure is similar. It has two 
introduction rules: 
\begin{isabelle}
p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup +
\rulename{r_into_trancl}\isanewline
\isasymlbrakk (a,\ b)\ \isasymin \ r\isactrlsup +;\ (b,\ c)\ \isasymin \ r\isactrlsup +\isasymrbrakk \ \isasymLongrightarrow \ (a,\ c)\ \isasymin \ r\isactrlsup +
\rulename{trancl_trans}
\end{isabelle}
%
The induction rule resembles the one shown above. 
A typical lemma states that transitive closure commutes with the converse
operator: 
\begin{isabelle}
(r\isasyminverse )\isactrlsup +\ =\ (r\isactrlsup +)\isasyminverse 
\rulename{trancl_converse}
\end{isabelle}

\subsection{A Sample Proof}

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 \ (y,x)\ \isasymin \ r\isacharcircum *"\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\isactrlsup *\isanewline
\ 2.\ \isasymAnd y\ z.\ \isasymlbrakk (x,y)\ \isasymin \ (r\isasyminverse )\isactrlsup *;\ (y,z)\ \isasymin \ r\isasyminverse ;\ (y,x)\ \isasymin \ r\isactrlsup *\isasymrbrakk \isanewline
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (z,x)\ \isasymin \ r\isactrlsup *
\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:\ "(y,x)\ \isasymin \ r\isacharcircum *\ \isasymLongrightarrow \ (x,y)\ \isasymin \ (r\isacharcircum -1)\isacharcircum *"\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}-1"\isanewline
\isacommand{by}\ (auto\ intro:\ rtrancl_converseI\ dest:\
rtrancl_converseD)
\end{isabelle}

\begin{warn}
Note that \isa{blast} cannot prove this theorem.  Here is a subgoal that
arises internally after  the rules \isa{equalityI} and \isa{subsetI} have
been applied:
\begin{isabelle}
\ 1.\ \isasymAnd x.\ x\ \isasymin \ (r\isasyminverse )\isactrlsup *\ \isasymLongrightarrow \ x\ \isasymin \ (r\isactrlsup
*)\isasyminverse
%ignore subgoal 2
%\ 2.\ \isasymAnd x.\ x\ \isasymin \ (r\isactrlsup *)\isasyminverse \
%\isasymLongrightarrow \ x\ \isasymin \ (r\isasyminverse )\isactrlsup *
\end{isabelle}
\par\noindent
We cannot use \isa{rtrancl_converseD}\@.  It refers to
ordered pairs, while \isa{x} is a variable of product type.
The \isa{simp} and \isa{blast} methods can do nothing, so let us try
\isa{clarify}:
\begin{isabelle}
\ 1.\ \isasymAnd a\ b.\ (a,b)\ \isasymin \ (r\isasyminverse )\isactrlsup *\ \isasymLongrightarrow \ (b,a)\ \isasymin \ r\isactrlsup
*
\end{isabelle}
Now that \isa{x} has been replaced by the pair \isa{(a,b)}, we can
proceed.  Other methods that split variables in this way are \isa{force}
and \isa{auto}.  Section~\ref{sec:products} will discuss proof techniques
for ordered pairs in more detail.
\end{warn}



\section{Well-Founded Relations and Induction}
\label{sec:Well-founded}

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.

\smallskip
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 the 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 
formulations are all complicated.  However,  often a relation
is well-founded by construction.  HOL provides
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.

Isabelle/HOL 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
a 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}.  Isabelle/HOL 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 a list (\isa{measure length}). 
Isabelle/HOL 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.

The \textbf{multiset ordering}, useful for hard termination proofs, is available
in the Library.  Baader and Nipkow \cite[\S2.5]{Baader-Nipkow} discuss it. 


\section{Fixed Point Operators}

Fixed point operators define sets recursively.  They are invoked
implicitly when making an inductive definition, as discussed in
Chap.\ts\ref{chap:inductive} below.  However, they can be used directly, too.
The
\relax{least}  or \relax{strongest} fixed point yields an inductive
definition;  the \relax{greatest} or \relax{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 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 \relax{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 \relax{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.