1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
\contentsline {chapter}{\numberline {1}The pred{\unhbox \voidb@x \kern 0.15ex \vbox {\hrule height0.1ex width0.3em}\kern 0.2ex}sets Library}{1}
\contentsline {section}{\numberline {1.1}Membership and the axioms of set theory}{1}
\contentsline {section}{\numberline {1.2}Generalized set specifications}{2}
\contentsline {subsection}{\numberline {1.2.1}Parser and pretty-printer support}{3}
\contentsline {subsection}{\numberline {1.2.2}Theorem-proving support}{4}
\contentsline {section}{\numberline {1.3}The empty and universal sets}{5}
\contentsline {section}{\numberline {1.4}Set inclusion}{6}
\contentsline {section}{\numberline {1.5}Union, intersection, and set difference}{7}
\contentsline {section}{\numberline {1.6}Disjoint sets}{7}
\contentsline {section}{\numberline {1.7}Insertion and deletion of an element}{8}
\contentsline {subsection}{\numberline {1.7.1}Parser and pretty-printer support}{8}
\contentsline {subsection}{\numberline {1.7.2}Conversions for enumerated finite sets}{9}
\contentsline {subsubsection}{\numberline {1.7.2.1}Membership}{9}
\contentsline {subsubsection}{\numberline {1.7.2.2}Union}{10}
\contentsline {subsubsection}{\numberline {1.7.2.3}Insertion}{12}
\contentsline {subsubsection}{\numberline {1.7.2.4}Deletion}{13}
\contentsline {section}{\numberline {1.8}Singleton sets}{13}
\contentsline {section}{\numberline {1.9}The {\ptt CHOICE} and {\ptt REST} functions}{14}
\contentsline {section}{\numberline {1.10}Image of a function on a set}{14}
\contentsline {subsection}{\numberline {1.10.1}Theorem-proving support}{15}
\contentsline {section}{\numberline {1.11}Mappings between sets}{16}
\contentsline {section}{\numberline {1.12}Finite and infinite sets}{16}
\contentsline {subsection}{\numberline {1.12.1}Theorem-proving support}{17}
\contentsline {section}{\numberline {1.13}Cardinality of finite sets}{18}
\contentsline {section}{\numberline {1.14}Using the library}{19}
\contentsline {subsection}{\numberline {1.14.1}Example session}{19}
\contentsline {subsection}{\numberline {1.14.2}The {\ptt load\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}pred\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}sets} function}{20}
\contentsline {chapter}{\numberline {2}ML Functions in the Library}{23}
\contentsline {chapter}{\numberline {3}Pre-proved Theorems}{33}
\contentsline {section}{\numberline {3.1}Membership, equality, and set specifications}{33}
\contentsline {section}{\numberline {3.2}The empty and universal sets}{33}
\contentsline {section}{\numberline {3.3}Set inclusion}{34}
\contentsline {section}{\numberline {3.4}Intersection and union}{35}
\contentsline {section}{\numberline {3.5}Set difference}{37}
\contentsline {section}{\numberline {3.6}Disjoint sets}{37}
\contentsline {section}{\numberline {3.7}Insertion and deletion of an element}{38}
\contentsline {section}{\numberline {3.8}The {\ptt CHOICE} and {\ptt REST} functions}{40}
\contentsline {section}{\numberline {3.9}Image of a function on a set}{41}
\contentsline {section}{\numberline {3.10}Mappings between sets}{41}
\contentsline {section}{\numberline {3.11}Singleton sets}{43}
\contentsline {section}{\numberline {3.12}Finite and infinite sets}{43}
\contentsline {section}{\numberline {3.13}Cardinality of sets}{45}
\contentsline {chapter}{References}{47}
\contentsline {chapter}{Index}{48}
|
