Tutorial/document/sets.tex

1 \chapter{Sets, Functions and Relations}
5 inductive definition yields a set, and the abstract theories of relations
7 constants such as union and intersection, as well as the main operations on relations, such as converse, composition and
10 function is a set, and the inverse image of a function maps sets to sets.
14 as grammars, logical calculi and state transition systems.  Isabelle can
20 out some key properties of the various constants and to introduce you to
32 all elements have the same type, say~$\tau$,  and the set itself has type
35 We begin with \textbf{intersection}, \textbf{union} and
64 for the  empty set and for the universal set.
116 \isa{A~\isasymsubseteq~-B} asserts that the sets \isa{A} and \isa{B} are
189 remark: this proof uses two methods, namely {\isa{simp}}  and
192 cannot break down. The combined methods (namely {\isa{force}}  and
202 comprehension and the membership relation:
235 The left and right hand sides
247 and
250 \isa{A(x)} and
258 Universal and existential quantifications may range over sets,
343 x:\ A.\ B} and \isa{Inter\ C} in \textsc{ascii}.  Among others, these
361 Unions, intersections and so forth are not simply replaced by their
372 \isa{{\isasymforall}x.\ P\ x} and
375 \isa{{\isasymforall}x\isasymin A.\ P\ x} and
377 \isa{\isasymexists x\isasymin A.\ P\ x}.  For indexed unions and
379 \cdx{UNION} and  \cdx{INTER}\@.
386 \subsection{Finiteness and Cardinality}
390 includes many familiar theorems about finiteness and cardinality
392 cardinalities of unions, intersections and the
431 we cannot simply state lemmas and expect them to be proved using
448 the obvious definition and many useful facts are proved about
467 The \bfindex{identity function} and function
479 Many familiar theorems concerning the identity and composition
523 %is a surjection and vice versa; the inverse of a bijection is
564 The first step of the proof invokes extensionality and the definitions
565 of injectiveness and composition. It leaves one subgoal:
601 are two examples, illustrating connections with indexed union and with the
695 Here is a typical law proved about converse and composition:
713 The \textbf{domain} and \textbf{range} of a relation are defined in the
734 \subsection{The Reflexive and Transitive Closure}
736 \index{reflexive and transitive closure|(}%
737 The \textbf{reflexive and transitive closure} of the
739 postfix syntax.  In ASCII we write \isa{r\isacharcircum*} and in
820 \isasymin\ r}, and then
843 \isa{equalityI} and \isa{subsetI} have been applied:
854 The \isa{simp} and \isa{blast} methods can do nothing, so let us try
862 \isa{auto}, \isa{fast} and \isa{best}.  Section~\ref{sec:products} will discuss proof
865 \index{relations|)}\index{reflexive and transitive closure|)}
868 \section{Well-Founded Relations and Induction}
902 relation  behaves as expected and that it is well-founded:
912 a relation. Given a relation~\isa{r} and a function~\isa{f}, we express  a
915 on~\isa{r}.  Isabelle/HOL defines this concept and proves a
926 size} justifies primitive recursion and structural induction over a
939 rb}, where \isa{ra} and \isa{rb} are the two operands.  The
940 lexicographic product satisfies the usual  definition and it preserves
960 Baader and Nipkow \cite[{\S}2.5]{Baader-Nipkow} discuss it.
966 lists and induction on size.  All are instances of the following rule,
1021 definition, monotonicity has the obvious introduction and destruction
1033 it is a fixed point and that it enjoys an induction rule: