|
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: |