doc-src/Main/Main_Doc.tex
 changeset 30442 1bc0638d554d
equal inserted replaced
30441:193cf2fa692a 30442:1bc0638d554d

     1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{Main{\isacharunderscore}Doc}%

     4 %

     5 \isadelimtheory

     6 %

     7 \endisadelimtheory

     8 %

     9 \isatagtheory

    10 %

    11 \endisatagtheory

    12 {\isafoldtheory}%

    13 %

    14 \isadelimtheory

    15 %

    16 \endisadelimtheory

    17 %

    18 \isadelimML

    19 %

    20 \endisadelimML

    21 %

    22 \isatagML

    23 %

    24 \endisatagML

    25 {\isafoldML}%

    26 %

    27 \isadelimML

    28 %

    29 \endisadelimML

    30 %

    31 \begin{isamarkuptext}%

    32 \begin{abstract}

    33 This document lists the main types, functions and syntax provided by theory \isa{Main}. It is meant as a quick overview of what is available. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/dist/library/HOL/}.

    34 \end{abstract}

    35

    36 \section{HOL}

    37

    38 The basic logic: \isa{x\ {\isacharequal}\ y}, \isa{True}, \isa{False}, \isa{{\isasymnot}\ P}, \isa{P\ {\isasymand}\ Q}, \isa{P\ {\isasymor}\ Q}, \isa{P\ {\isasymlongrightarrow}\ Q}, \isa{{\isasymforall}x{\isachardot}\ P}, \isa{{\isasymexists}x{\isachardot}\ P}, \isa{{\isasymexists}{\isacharbang}x{\isachardot}\ P}, \isa{THE\ x{\isachardot}\ P}.

    39 \smallskip

    40

    41 \begin{tabular}{@ {} l @ {~::~} l @ {}}

    42 \isa{undefined} & \isa{{\isacharprime}a}\\

    43 \isa{default} & \isa{{\isacharprime}a}\\

    44 \end{tabular}

    45

    46 \subsubsection*{Syntax}

    47

    48 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}

    49 \isa{x\ {\isasymnoteq}\ y} & \isa{{\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}} & (\verb$~=$)\\

    50 \isa{{\isachardoublequote}P\ {\isasymlongleftrightarrow}\ Q{\isachardoublequote}} & \isa{P\ {\isacharequal}\ Q} \\

    51 \isa{if\ x\ then\ y\ else\ z} & \isa{{\isachardoublequote}If\ x\ y\ z{\isachardoublequote}}\\

    52 \isa{let\ x\ {\isacharequal}\ e\isactrlisub {\isadigit{1}}\ in\ e\isactrlisub {\isadigit{2}}} & \isa{{\isachardoublequote}Let\ e\isactrlisub {\isadigit{1}}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequote}}\\

    53 \end{supertabular}

    54

    55

    56 \section{Orderings}

    57

    58 A collection of classes defining basic orderings:

    59 preorder, partial order, linear order, dense linear order and wellorder.

    60 \smallskip

    61

    62 \begin{supertabular}{@ {} l @ {~::~} l l @ {}}

    63 \isa{op\ {\isasymle}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (\verb$<=$)\\

    64 \isa{op\ {\isacharless}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool}\\

    65 \isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\

    66 \isa{min} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

    67 \isa{max} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

    68 \isa{top} & \isa{{\isacharprime}a}\\

    69 \isa{bot} & \isa{{\isacharprime}a}\\

    70 \isa{mono} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\

    71 \isa{strict{\isacharunderscore}mono} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\

    72 \end{supertabular}

    73

    74 \subsubsection*{Syntax}

    75

    76 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}

    77 \isa{{\isachardoublequote}x\ {\isasymge}\ y{\isachardoublequote}} & \isa{y\ {\isasymle}\ x} & (\verb$>=$)\\

    78 \isa{{\isachardoublequote}x\ {\isachargreater}\ y{\isachardoublequote}} & \isa{y\ {\isacharless}\ x}\\

    79 \isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P{\isachardoublequote}}\\

    80 \isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P{\isachardoublequote}}\\

    81 \multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\

    82 \isa{LEAST\ x{\isachardot}\ P} & \isa{{\isachardoublequote}Least\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\

    83 \end{supertabular}

    84

    85

    86 \section{Lattices}

    87

    88 Classes semilattice, lattice, distributive lattice and complete lattice (the

    89 latter in theory \isa{Set}).

    90

    91 \begin{tabular}{@ {} l @ {~::~} l @ {}}

    92 \isa{inf} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

    93 \isa{sup} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

    94 \isa{Inf} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a}\\

    95 \isa{Sup} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a}\\

    96 \end{tabular}

    97

    98 \subsubsection*{Syntax}

    99

   100 Available by loading theory \isa{Lattice{\isacharunderscore}Syntax} in directory \isa{Library}.

   101

   102 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}

   103 \isa{{\isachardoublequote}x\ {\isasymsqsubseteq}\ y{\isachardoublequote}} & \isa{x\ {\isasymle}\ y}\\

   104 \isa{{\isachardoublequote}x\ {\isasymsqsubset}\ y{\isachardoublequote}} & \isa{x\ {\isacharless}\ y}\\

   105 \isa{{\isachardoublequote}x\ {\isasymsqinter}\ y{\isachardoublequote}} & \isa{inf\ x\ y}\\

   106 \isa{{\isachardoublequote}x\ {\isasymsqunion}\ y{\isachardoublequote}} & \isa{sup\ x\ y}\\

   107 \isa{{\isachardoublequote}{\isasymSqinter}\ A{\isachardoublequote}} & \isa{Sup\ A}\\

   108 \isa{{\isachardoublequote}{\isasymSqunion}\ A{\isachardoublequote}} & \isa{Inf\ A}\\

   109 \isa{{\isachardoublequote}{\isasymtop}{\isachardoublequote}} & \isa{top}\\

   110 \isa{{\isachardoublequote}{\isasymbottom}{\isachardoublequote}} & \isa{bot}\\

   111 \end{supertabular}

   112

   113

   114 \section{Set}

   115

   116 Sets are predicates: \isa{{\isachardoublequote}{\isacharprime}a\ set\ \ {\isacharequal}\ \ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}}

   117 \bigskip

   118

   119 \begin{supertabular}{@ {} l @ {~::~} l l @ {}}

   120 \isa{{\isacharbraceleft}{\isacharbraceright}} & \isa{{\isacharprime}a\ set}\\

   121 \isa{insert} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   122 \isa{Collect} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   123 \isa{op\ {\isasymin}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool} & (\texttt{:})\\

   124 \isa{op\ {\isasymunion}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set} & (\texttt{Un})\\

   125 \isa{op\ {\isasyminter}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set} & (\texttt{Int})\\

   126 \isa{UNION} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\

   127 \isa{INTER} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\

   128 \isa{Union} & \isa{{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   129 \isa{Inter} & \isa{{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   130 \isa{Pow} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set}\\

   131 \isa{UNIV} & \isa{{\isacharprime}a\ set}\\

   132 \isa{op\ {\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\

   133 \isa{Ball} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool}\\

   134 \isa{Bex} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool}\\

   135 \end{supertabular}

   136

   137 \subsubsection*{Syntax}

   138

   139 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}

   140 \isa{{\isacharbraceleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isacharbraceright}} & \isa{insert\ x\isactrlisub {\isadigit{1}}\ {\isacharparenleft}{\isasymdots}\ {\isacharparenleft}insert\ x\isactrlisub n\ {\isacharbraceleft}{\isacharbraceright}{\isacharparenright}{\isasymdots}{\isacharparenright}}\\

   141 \isa{x\ {\isasymnotin}\ A} & \isa{{\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isasymin}\ A{\isacharparenright}{\isachardoublequote}}\\

   142 \isa{A\ {\isasymsubseteq}\ B} & \isa{{\isachardoublequote}A\ {\isasymle}\ B{\isachardoublequote}}\\

   143 \isa{A\ {\isasymsubset}\ B} & \isa{{\isachardoublequote}A\ {\isacharless}\ B{\isachardoublequote}}\\

   144 \isa{{\isachardoublequote}A\ {\isasymsupseteq}\ B{\isachardoublequote}} & \isa{{\isachardoublequote}B\ {\isasymle}\ A{\isachardoublequote}}\\

   145 \isa{{\isachardoublequote}A\ {\isasymsupset}\ B{\isachardoublequote}} & \isa{{\isachardoublequote}B\ {\isacharless}\ A{\isachardoublequote}}\\

   146 \isa{{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}} & \isa{{\isachardoublequote}Collect\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\

   147 \isa{{\isasymUnion}x{\isasymin}I{\isachardot}\ A} & \isa{{\isachardoublequote}UNION\ I\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}} & (\texttt{UN})\\

   148 \isa{{\isasymUnion}x{\isachardot}\ A} & \isa{{\isachardoublequote}UNION\ UNIV\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}}\\

   149 \isa{{\isasymInter}x{\isasymin}I{\isachardot}\ A} & \isa{{\isachardoublequote}INTER\ I\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}} & (\texttt{INT})\\

   150 \isa{{\isasymInter}x{\isachardot}\ A} & \isa{{\isachardoublequote}INTER\ UNIV\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}}\\

   151 \isa{{\isasymforall}x{\isasymin}A{\isachardot}\ P} & \isa{{\isachardoublequote}Ball\ A\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\

   152 \isa{{\isasymexists}x{\isasymin}A{\isachardot}\ P} & \isa{{\isachardoublequote}Bex\ A\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\

   153 \isa{range\ f} & \isa{{\isachardoublequote}f\ {\isacharbackquote}\ UNIV{\isachardoublequote}}\\

   154 \end{supertabular}

   155

   156

   157 \section{Fun}

   158

   159 \begin{supertabular}{@ {} l @ {~::~} l @ {}}

   160 \isa{id} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

   161 \isa{op\ {\isasymcirc}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}c\ {\isasymRightarrow}\ {\isacharprime}b}\\

   162 \isa{inj{\isacharunderscore}on} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool}\\

   163 \isa{inj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\

   164 \isa{surj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\

   165 \isa{bij} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\

   166 \isa{bij{\isacharunderscore}betw} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set\ {\isasymRightarrow}\ bool}\\

   167 \isa{fun{\isacharunderscore}upd} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b}\\

   168 \end{supertabular}

   169

   170 \subsubsection*{Syntax}

   171

   172 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}

   173 \isa{f{\isacharparenleft}x\ {\isacharcolon}{\isacharequal}\ y{\isacharparenright}} & \isa{{\isachardoublequote}fun{\isacharunderscore}upd\ f\ x\ y{\isachardoublequote}}\\

   174 \isa{f{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isacharcolon}{\isacharequal}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isacharcolon}{\isacharequal}y\isactrlisub n{\isacharparenright}} & \isa{f{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isacharcolon}{\isacharequal}y\isactrlisub {\isadigit{1}}{\isacharparenright}{\isasymdots}{\isacharparenleft}x\isactrlisub n{\isacharcolon}{\isacharequal}y\isactrlisub n{\isacharparenright}}\\

   175 \end{tabular}

   176

   177

   178 \section{Fixed Points}

   179

   180 Theory: \isa{Inductive}.

   181

   182 Least and greatest fixed points in a complete lattice \isa{{\isacharprime}a}:

   183

   184 \begin{tabular}{@ {} l @ {~::~} l @ {}}

   185 \isa{lfp} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\

   186 \isa{gfp} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\

   187 \end{tabular}

   188

   189 Note that in particular sets (\isa{{\isacharprime}a\ {\isasymRightarrow}\ bool}) are complete lattices.

   190

   191 \section{Sum\_Type}

   192

   193 Type constructor \isa{{\isacharplus}}.

   194

   195 \begin{tabular}{@ {} l @ {~::~} l @ {}}

   196 \isa{Inl} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isacharplus}\ {\isacharprime}b}\\

   197 \isa{Inr} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isacharplus}\ {\isacharprime}a}\\

   198 \isa{op\ {\isacharless}{\isacharplus}{\isachargreater}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharplus}\ {\isacharprime}b{\isacharparenright}\ set}

   199 \end{tabular}

   200

   201

   202 \section{Product\_Type}

   203

   204 Types \isa{unit} and \isa{{\isasymtimes}}.

   205

   206 \begin{supertabular}{@ {} l @ {~::~} l @ {}}

   207 \isa{{\isacharparenleft}{\isacharparenright}} & \isa{unit}\\

   208 \isa{Pair} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}\\

   209 \isa{fst} & \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a}\\

   210 \isa{snd} & \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}\\

   211 \isa{split} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c}\\

   212 \isa{curry} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c}\\

   213 \isa{Sigma} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\

   214 \end{supertabular}

   215

   216 \subsubsection*{Syntax}

   217

   218 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}

   219 \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}} & \isa{{\isachardoublequote}Pair\ a\ b{\isachardoublequote}}\\

   220 \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} & \isa{{\isachardoublequote}split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}{\isachardoublequote}}\\

   221 \isa{A\ {\isasymtimes}\ B} &  \isa{Sigma\ A\ {\isacharparenleft}{\isasymlambda}\_{\isachardot}\ B{\isacharparenright}} & (\verb$<*>$)

   222 \end{tabular}

   223

   224 Pairs may be nested. Nesting to the right is printed as a tuple,

   225 e.g.\ \mbox{\isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharcomma}\ c{\isacharparenright}}} is really \mbox{\isa{{\isacharparenleft}a{\isacharcomma}\ {\isacharparenleft}b{\isacharcomma}\ c{\isacharparenright}{\isacharparenright}}.}

   226 Pattern matching with pairs and tuples extends to all binders,

   227 e.g.\ \mbox{\isa{{\isasymforall}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A{\isachardot}\ P},} \isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ P{\isacharbraceright}}, etc.

   228

   229

   230 \section{Relation}

   231

   232 \begin{supertabular}{@ {} l @ {~::~} l @ {}}

   233 \isa{converse} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\

   234 \isa{op\ O} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\

   235 \isa{op\ {\isacharbackquote}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\

   236 \isa{inv{\isacharunderscore}image} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\

   237 \isa{Id{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\

   238 \isa{Id} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\

   239 \isa{Domain} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   240 \isa{Range} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\

   241 \isa{Field} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   242 \isa{refl{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\

   243 \isa{refl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\

   244 \isa{sym} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\

   245 \isa{antisym} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\

   246 \isa{trans} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\

   247 \isa{irrefl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\

   248 \isa{total{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\

   249 \isa{total} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\

   250 \end{supertabular}

   251

   252 \subsubsection*{Syntax}

   253

   254 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}

   255 \isa{r{\isasyminverse}} & \isa{{\isachardoublequote}converse\ r{\isachardoublequote}} & (\verb$^-1$)

   256 \end{tabular}

   257

   258 \section{Equiv\_Relations}

   259

   260 \begin{supertabular}{@ {} l @ {~::~} l @ {}}

   261 \isa{equiv} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\

   262 \isa{op\ {\isacharslash}{\isacharslash}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set}\\

   263 \isa{congruent} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\

   264 \isa{congruent{\isadigit{2}}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ bool}\\

   265 %@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\

   266 \end{supertabular}

   267

   268 \subsubsection*{Syntax}

   269

   270 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}

   271 \isa{f\ respects\ r} & \isa{{\isachardoublequote}congruent\ r\ f{\isachardoublequote}}\\

   272 \isa{f\ respects{\isadigit{2}}\ r} & \isa{{\isachardoublequote}congruent{\isadigit{2}}\ r\ r\ f{\isachardoublequote}}\\

   273 \end{tabular}

   274

   275

   276 \section{Transitive\_Closure}

   277

   278 \begin{tabular}{@ {} l @ {~::~} l @ {}}

   279 \isa{rtrancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\

   280 \isa{trancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\

   281 \isa{reflcl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\

   282 \end{tabular}

   283

   284 \subsubsection*{Syntax}

   285

   286 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}

   287 \isa{r\isactrlsup {\isacharasterisk}} & \isa{{\isachardoublequote}rtrancl\ r{\isachardoublequote}} & (\verb$^*$)\\

   288 \isa{r\isactrlsup {\isacharplus}} & \isa{{\isachardoublequote}trancl\ r{\isachardoublequote}} & (\verb$^+$)\\

   289 \isa{r\isactrlsup {\isacharequal}} & \isa{{\isachardoublequote}reflcl\ r{\isachardoublequote}} & (\verb$^=$)

   290 \end{tabular}

   291

   292

   293 \section{Algebra}

   294

   295 Theories \isa{OrderedGroup}, \isa{Ring{\isacharunderscore}and{\isacharunderscore}Field} and \isa{Divides} define a large collection of classes describing common algebraic

   296 structures from semigroups up to fields. Everything is done in terms of

   297 overloaded operators:

   298

   299 \begin{supertabular}{@ {} l @ {~::~} l l @ {}}

   300 \isa{{\isadigit{0}}} & \isa{{\isacharprime}a}\\

   301 \isa{{\isadigit{1}}} & \isa{{\isacharprime}a}\\

   302 \isa{op\ {\isacharplus}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

   303 \isa{op\ {\isacharminus}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

   304 \isa{uminus} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (\verb$-$)\\

   305 \isa{op\ {\isacharasterisk}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

   306 \isa{inverse} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

   307 \isa{op\ {\isacharslash}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

   308 \isa{abs} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

   309 \isa{sgn} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

   310 \isa{op\ dvd} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool}\\

   311 \isa{op\ div} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

   312 \isa{op\ mod} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\

   313 \end{supertabular}

   314

   315 \subsubsection*{Syntax}

   316

   317 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}

   318 \isa{{\isasymbar}x{\isasymbar}} & \isa{{\isachardoublequote}abs\ x{\isachardoublequote}}

   319 \end{tabular}

   320

   321

   322 \section{Nat}

   323

   324 \isa{\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat}

   325 \bigskip

   326

   327 \begin{tabular}{@ {} lllllll @ {}}

   328 \isa{op\ {\isacharplus}} &

   329 \isa{op\ {\isacharminus}} &

   330 \isa{op\ {\isacharasterisk}} &

   331 \isa{op\ {\isacharcircum}} &

   332 \isa{op\ div}&

   333 \isa{op\ mod}&

   334 \isa{op\ dvd}\\

   335 \isa{op\ {\isasymle}} &

   336 \isa{op\ {\isacharless}} &

   337 \isa{min} &

   338 \isa{max} &

   339 \isa{Min} &

   340 \isa{Max}\\

   341 \end{tabular}

   342

   343 \begin{tabular}{@ {} l @ {~::~} l @ {}}

   344 \isa{of{\isacharunderscore}nat} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a}

   345 \end{tabular}

   346

   347 \section{Int}

   348

   349 Type \isa{int}

   350 \bigskip

   351

   352 \begin{tabular}{@ {} llllllll @ {}}

   353 \isa{op\ {\isacharplus}} &

   354 \isa{op\ {\isacharminus}} &

   355 \isa{uminus} &

   356 \isa{op\ {\isacharasterisk}} &

   357 \isa{op\ {\isacharcircum}} &

   358 \isa{op\ div}&

   359 \isa{op\ mod}&

   360 \isa{op\ dvd}\\

   361 \isa{op\ {\isasymle}} &

   362 \isa{op\ {\isacharless}} &

   363 \isa{min} &

   364 \isa{max} &

   365 \isa{Min} &

   366 \isa{Max}\\

   367 \isa{abs} &

   368 \isa{sgn}\\

   369 \end{tabular}

   370

   371 \begin{tabular}{@ {} l @ {~::~} l l @ {}}

   372 \isa{nat} & \isa{int\ {\isasymRightarrow}\ nat}\\

   373 \isa{of{\isacharunderscore}int} & \isa{int\ {\isasymRightarrow}\ {\isacharprime}a}\\

   374 \isa{{\isasymint}} & \isa{{\isacharprime}a\ set} & (\verb$Ints$)

   375 \end{tabular}

   376

   377 \subsubsection*{Syntax}

   378

   379 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}

   380 \isa{int} & \isa{{\isachardoublequote}of{\isacharunderscore}nat{\isachardoublequote}}\\

   381 \end{tabular}

   382

   383

   384 \section{Finite\_Set}

   385

   386

   387 \begin{supertabular}{@ {} l @ {~::~} l @ {}}

   388 \isa{finite} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ bool}\\

   389 \isa{card} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ nat}\\

   390 \isa{fold} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\

   391 \isa{fold{\isacharunderscore}image} & \isa{{\isacharparenleft}{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\

   392 \isa{setsum} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\

   393 \isa{setprod} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\

   394 \end{supertabular}

   395

   396

   397 \subsubsection*{Syntax}

   398

   399 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}

   400 \isa{{\isasymSum}A} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x{\isacharparenright}\ A{\isachardoublequote}} & (\verb$SUM$)\\

   401 \isa{{\isasymSum}x{\isasymin}A{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ A{\isachardoublequote}}\\

   402 \isa{{\isachardoublequote}{\isasymSum}x{\isacharbar}P{\isachardot}\ t{\isachardoublequote}} & \isa{{\isasymSum}x{\isasymin}{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}{\isachardot}\ t}\\

   403 \multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymProd}} instead of \isa{{\isasymSum}}} & (\verb$PROD$)\\

   404 \end{supertabular}

   405

   406

   407 \section{Wellfounded}

   408

   409 \begin{supertabular}{@ {} l @ {~::~} l @ {}}

   410 \isa{wf} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\

   411 \isa{acyclic} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\

   412 \isa{acc} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   413 \isa{measure} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\

   414 \isa{op\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\

   415 \isa{op\ {\isacharless}{\isacharasterisk}mlex{\isacharasterisk}{\isachargreater}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\

   416 \isa{less{\isacharunderscore}than} & \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set}\\

   417 \isa{pred{\isacharunderscore}nat} & \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set}\\

   418 \end{supertabular}

   419

   420

   421 \section{SetInterval}

   422

   423 \begin{supertabular}{@ {} l @ {~::~} l @ {}}

   424 \isa{lessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   425 \isa{atMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   426 \isa{greaterThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   427 \isa{atLeast} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   428 \isa{greaterThanLessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   429 \isa{atLeastLessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   430 \isa{greaterThanAtMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   431 \isa{atLeastAtMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   432 \end{supertabular}

   433

   434 \subsubsection*{Syntax}

   435

   436 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}

   437 \isa{{\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}lessThan\ y{\isachardoublequote}}\\

   438 \isa{{\isacharbraceleft}{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}atMost\ y{\isachardoublequote}}\\

   439 \isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThan\ x{\isachardoublequote}}\\

   440 \isa{{\isacharbraceleft}x{\isachardot}{\isachardot}{\isacharbraceright}} & \isa{{\isachardoublequote}atLeast\ x{\isachardoublequote}}\\

   441 \isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThanLessThan\ x\ y{\isachardoublequote}}\\

   442 \isa{{\isacharbraceleft}x{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}atLeastLessThan\ x\ y{\isachardoublequote}}\\

   443 \isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThanAtMost\ x\ y{\isachardoublequote}}\\

   444 \isa{{\isacharbraceleft}x{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}atLeastAtMost\ x\ y{\isachardoublequote}}\\

   445 \isa{{\isasymUnion}\ i{\isasymle}n{\isachardot}\ A} & \isa{{\isachardoublequote}{\isasymUnion}\ i\ {\isasymin}\ {\isacharbraceleft}{\isachardot}{\isachardot}n{\isacharbraceright}{\isachardot}\ A{\isachardoublequote}}\\

   446 \isa{{\isasymUnion}\ i{\isacharless}n{\isachardot}\ A} & \isa{{\isachardoublequote}{\isasymUnion}\ i\ {\isasymin}\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardot}\ A{\isachardoublequote}}\\

   447 \multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymInter}} instead of \isa{{\isasymUnion}}}\\

   448 \isa{{\isasymSum}x\ {\isacharequal}\ a{\isachardot}{\isachardot}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}a{\isachardot}{\isachardot}b{\isacharbraceright}{\isachardoublequote}}\\

   449 \isa{{\isasymSum}x\ {\isacharequal}\ a{\isachardot}{\isachardot}{\isacharless}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}a{\isachardot}{\isachardot}{\isacharless}b{\isacharbraceright}{\isachardoublequote}}\\

   450 \isa{{\isasymSum}x{\isasymle}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}{\isachardot}{\isachardot}b{\isacharbraceright}{\isachardoublequote}}\\

   451 \isa{{\isasymSum}x{\isacharless}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}b{\isacharbraceright}{\isachardoublequote}}\\

   452 \multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymProd}} instead of \isa{{\isasymSum}}}\\

   453 \end{supertabular}

   454

   455

   456 \section{Power}

   457

   458 \begin{tabular}{@ {} l @ {~::~} l @ {}}

   459 \isa{op\ {\isacharcircum}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a}

   460 \end{tabular}

   461

   462

   463 \section{Iterated Functions and Relations}

   464

   465 Theory: \isa{Relation{\isacharunderscore}Power}

   466

   467 Iterated functions \ \isa{{\isachardoublequote}{\isacharparenleft}f{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isasymRightarrow}{\isacharprime}a{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}} \

   468 and relations \ \isa{{\isachardoublequote}{\isacharparenleft}r{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}a{\isacharparenright}set{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}}.

   469

   470

   471 \section{Option}

   472

   473 \isa{\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a}

   474 \bigskip

   475

   476 \begin{tabular}{@ {} l @ {~::~} l @ {}}

   477 \isa{the} & \isa{{\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}a}\\

   478 \isa{Option{\isachardot}map} & \isa{{\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}b\ option{\isachardoublequote}}\\

   479 \isa{Option{\isachardot}set} & \isa{{\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}a\ set}

   480 \end{tabular}

   481

   482 \section{List}

   483

   484 \isa{\isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ op\ {\isacharhash}\ {\isacharprime}a\ {\isacharparenleft}{\isacharprime}a\ list{\isacharparenright}}

   485 \bigskip

   486

   487 \begin{supertabular}{@ {} l @ {~::~} l @ {}}

   488 \isa{op\ {\isacharat}} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   489 \isa{butlast} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   490 \isa{concat} & \isa{{\isacharprime}a\ list\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   491 \isa{distinct} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ bool}\\

   492 \isa{drop} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   493 \isa{dropWhile} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   494 \isa{filter} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   495 \isa{foldl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\

   496 \isa{foldr} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}\\

   497 \isa{hd} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\

   498 \isa{last} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\

   499 \isa{length} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat}\\

   500 \isa{lenlex} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\

   501 \isa{lex} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\

   502 \isa{lexn} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\

   503 \isa{lexord} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\

   504 \isa{listrel} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\

   505 \isa{lists} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ list\ set}\\

   506 \isa{listset} & \isa{{\isacharprime}a\ set\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ set}\\

   507 \isa{listsum} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\

   508 \isa{list{\isacharunderscore}all{\isadigit{2}}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ bool}\\

   509 \isa{list{\isacharunderscore}update} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   510 \isa{map} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list}\\

   511 \isa{measures} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\

   512 \isa{remdups} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   513 \isa{removeAll} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   514 \isa{remove{\isadigit{1}}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   515 \isa{replicate} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   516 \isa{rev} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   517 \isa{rotate} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   518 \isa{rotate{\isadigit{1}}} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   519 \isa{set} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   520 \isa{sort} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   521 \isa{sorted} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ bool}\\

   522 \isa{splice} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   523 \isa{sublist} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   524 \isa{take} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   525 \isa{takeWhile} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   526 \isa{tl} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   527 \isa{upt} & \isa{nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\ list}\\

   528 \isa{upto} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\

   529 \isa{zip} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list}\\

   530 \end{supertabular}

   531

   532 \subsubsection*{Syntax}

   533

   534 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}

   535 \isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isacharbrackright}} & \isa{x\isactrlisub {\isadigit{1}}\ {\isacharhash}\ {\isasymdots}\ {\isacharhash}\ x\isactrlisub n\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}\\

   536 \isa{{\isacharbrackleft}m{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}} & \isa{{\isachardoublequote}upt\ m\ n{\isachardoublequote}}\\

   537 \isa{{\isacharbrackleft}i{\isachardot}{\isachardot}j{\isacharbrackright}} & \isa{{\isachardoublequote}upto\ i\ j{\isachardoublequote}}\\

   538 \isa{{\isacharbrackleft}e{\isachardot}\ x\ {\isasymleftarrow}\ xs{\isacharbrackright}} & \isa{map\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e{\isacharparenright}\ xs}\\

   539 \isa{{\isacharbrackleft}x{\isasymleftarrow}xs\ {\isachardot}\ b{\isacharbrackright}} & \isa{{\isachardoublequote}filter\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharparenright}\ xs{\isachardoublequote}} \\

   540 \isa{xs{\isacharbrackleft}n\ {\isacharcolon}{\isacharequal}\ x{\isacharbrackright}} & \isa{{\isachardoublequote}list{\isacharunderscore}update\ xs\ n\ x{\isachardoublequote}}\\

   541 \isa{{\isasymSum}x{\isasymleftarrow}xs{\isachardot}\ e} & \isa{{\isachardoublequote}listsum\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}}\\

   542 \end{supertabular}

   543 \medskip

   544

   545 List comprehension: \isa{{\isacharbrackleft}e{\isachardot}\ q\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ q\isactrlisub n{\isacharbrackright}} where each

   546 qualifier \isa{q\isactrlisub i} is either a generator \mbox{\isa{pat\ {\isasymleftarrow}\ e}} or a

   547 guard, i.e.\ boolean expression.

   548

   549 \section{Map}

   550

   551 Maps model partial functions and are often used as finite tables. However,

   552 the domain of a map may be infinite.

   553

   554 \isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b\ \ {\isacharequal}\ \ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option}

   555 \bigskip

   556

   557 \begin{supertabular}{@ {} l @ {~::~} l @ {}}

   558 \isa{Map{\isachardot}empty} & \isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\

   559 \isa{op\ {\isacharplus}{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\

   560 \isa{op\ {\isasymcirc}\isactrlsub m} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymrightharpoonup}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}c\ {\isasymrightharpoonup}\ {\isacharprime}b}\\

   561 \isa{op\ {\isacharbar}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\

   562 \isa{dom} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\

   563 \isa{ran} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\

   564 \isa{op\ {\isasymsubseteq}\isactrlsub m} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\

   565 \isa{map{\isacharunderscore}of} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\

   566 \isa{map{\isacharunderscore}upds} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\

   567 \end{supertabular}

   568

   569 \subsubsection*{Syntax}

   570

   571 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}

   572 \isa{Map{\isachardot}empty} & \isa{{\isasymlambda}x{\isachardot}\ None}\\

   573 \isa{m{\isacharparenleft}x\ {\isasymmapsto}\ y{\isacharparenright}} & \isa{{\isachardoublequote}m{\isacharparenleft}x{\isacharcolon}{\isacharequal}Some\ y{\isacharparenright}{\isachardoublequote}}\\

   574 \isa{m{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharparenright}} & \isa{{\isachardoublequote}m{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharparenright}{\isasymdots}{\isacharparenleft}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharparenright}{\isachardoublequote}}\\

   575 \isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharbrackright}} & \isa{{\isachardoublequote}Map{\isachardot}empty{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharparenright}{\isachardoublequote}}\\

   576 \isa{m{\isacharparenleft}xs\ {\isacharbrackleft}{\isasymmapsto}{\isacharbrackright}\ ys{\isacharparenright}} & \isa{{\isachardoublequote}map{\isacharunderscore}upds\ m\ xs\ ys{\isachardoublequote}}\\

   577 \end{tabular}%

   578 \end{isamarkuptext}%

   579 \isamarkuptrue%

   580 %

   581 \isadelimtheory

   582 %

   583 \endisadelimtheory

   584 %

   585 \isatagtheory

   586 %

   587 \endisatagtheory

   588 {\isafoldtheory}%

   589 %

   590 \isadelimtheory

   591 %

   592 \endisadelimtheory

   593 \end{isabellebody}%

   594 %%% Local Variables:

   595 %%% mode: latex

   596 %%% TeX-master: "root"

   597 %%% End: