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
|
\contentsline {chapter}{\numberline {1}The finite{\unhbox \voidb@x \kern 0.15ex \vbox {\hrule height0.1ex width0.3em}\kern 0.2ex}sets Library}{1}
\contentsline {section}{\numberline {1.1}The type definition}{1}
\contentsline {section}{\numberline {1.2}Abstract characterization of the type {\ptt (*)set}}{2}
\contentsline {section}{\numberline {1.3}The set induction tactic}{3}
\contentsline {subsection}{\numberline {1.3.1}Parser and pretty-printer support}{4}
\contentsline {section}{\numberline {1.4}Set inclusion}{5}
\contentsline {section}{\numberline {1.5}Union, intersection, and set difference}{6}
\contentsline {section}{\numberline {1.6}Disjoint sets}{6}
\contentsline {section}{\numberline {1.7}Insertion and deletion of an element}{7}
\contentsline {subsection}{\numberline {1.7.1}Conversions for enumerated finite sets}{7}
\contentsline {subsubsection}{\numberline {1.7.1.1}Membership}{7}
\contentsline {subsubsection}{\numberline {1.7.1.2}Union}{9}
\contentsline {subsubsection}{\numberline {1.7.1.3}Insertion}{10}
\contentsline {subsubsection}{\numberline {1.7.1.4}Deletion}{11}
\contentsline {section}{\numberline {1.8}Singleton sets}{11}
\contentsline {section}{\numberline {1.9}The {\ptt CHOICE} and {\ptt REST} functions}{12}
\contentsline {section}{\numberline {1.10}Image of a function on a set}{12}
\contentsline {subsection}{\numberline {1.10.1}Theorem-proving support}{13}
\contentsline {section}{\numberline {1.11}Mappings between sets}{14}
\contentsline {section}{\numberline {1.12}Finite and infinite sets}{14}
\contentsline {subsection}{\numberline {1.12.1}Theorem-proving support}{15}
\contentsline {section}{\numberline {1.13}Cardinality of finite sets}{16}
\contentsline {section}{\numberline {1.14}Using the library}{16}
\contentsline {subsection}{\numberline {1.14.1}Example session}{17}
\contentsline {subsection}{\numberline {1.14.2}The {\ptt load\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}finite\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}sets} function}{18}
\contentsline {chapter}{\numberline {2}ML Functions in the Library}{19}
\contentsline {chapter}{\numberline {3}Pre-proved Theorems}{29}
\contentsline {section}{\numberline {3.1}The type definition}{29}
\contentsline {section}{\numberline {3.2}Basic properties of {\ptt EMPTY}, {\ptt INSERT}, and {\ptt IN}}{29}
\contentsline {section}{\numberline {3.3}Set inclusion}{31}
\contentsline {section}{\numberline {3.4}Intersection and union}{32}
\contentsline {section}{\numberline {3.5}Set difference}{33}
\contentsline {section}{\numberline {3.6}Deletion of an element}{33}
\contentsline {section}{\numberline {3.7}Disjoint sets}{34}
\contentsline {section}{\numberline {3.8}The {\ptt CHOICE} and {\ptt REST} functions}{35}
\contentsline {section}{\numberline {3.9}Image of a function on a set}{36}
\contentsline {section}{\numberline {3.10}Mappings between sets}{37}
\contentsline {section}{\numberline {3.11}Singleton sets}{38}
\contentsline {section}{\numberline {3.12}Cardinality of sets}{38}
\contentsline {chapter}{References}{41}
\contentsline {chapter}{Index}{42}
|
