144 |
144 |
145 %%% Cezary: I like the diagram, maybe 'new type' could be outside, but otherwise |
145 %%% Cezary: I like the diagram, maybe 'new type' could be outside, but otherwise |
146 %%% I wouldn't change it. |
146 %%% I wouldn't change it. |
147 |
147 |
148 \begin{center} |
148 \begin{center} |
149 \mbox{}\hspace{20mm}\begin{tikzpicture}[scale=0.9] |
149 \mbox{}\hspace{20mm}\begin{tikzpicture}[scale=1.1] |
150 %%\draw[step=2mm] (-4,-1) grid (4,1); |
150 %%\draw[step=2mm] (-4,-1) grid (4,1); |
151 |
151 |
152 \draw[very thick] (0.7,0.3) circle (4.85mm); |
152 \draw[very thick] (0.7,0.3) circle (4.85mm); |
153 \draw[rounded corners=1mm, very thick] ( 0.0,-0.9) rectangle ( 1.8, 0.9); |
153 \draw[rounded corners=1mm, very thick] ( 0.0,-0.9) rectangle ( 1.8, 0.9); |
154 \draw[rounded corners=1mm, very thick] (-1.95,0.8) rectangle (-2.9,-0.195); |
154 \draw[rounded corners=1mm, very thick] (-1.95,0.8) rectangle (-2.9,-0.195); |
220 \emph{compositions} of quotients. Such compositions are needed for example |
220 \emph{compositions} of quotients. Such compositions are needed for example |
221 in case of quotienting lists to yield finite sets and the operator that |
221 in case of quotienting lists to yield finite sets and the operator that |
222 flattens lists of lists, defined as follows |
222 flattens lists of lists, defined as follows |
223 |
223 |
224 \begin{isabelle}\ \ \ \ \ %%% |
224 \begin{isabelle}\ \ \ \ \ %%% |
225 @{thm concat.simps(1)[THEN eq_reflection]}\hspace{10mm} |
225 \begin{tabular}{@ {}l} |
226 @{thm concat.simps(2)[THEN eq_reflection]} |
226 @{thm concat.simps(1)[THEN eq_reflection]}\\ |
|
227 @{thm concat.simps(2)[THEN eq_reflection, where x1="x" and xs1="xs"]} |
|
228 \end{tabular} |
227 \end{isabelle} |
229 \end{isabelle} |
228 |
230 |
229 \noindent |
231 \noindent |
230 where @{text "@"} is the usual |
232 where @{text "@"} is the usual |
231 list append. We expect that the corresponding |
233 list append. We expect that the corresponding |
232 operator on finite sets, written @{term "fconcat"}, |
234 operator on finite sets, written @{term "fconcat"}, |
233 builds finite unions of finite sets: |
235 builds finite unions of finite sets: |
234 |
236 |
235 \begin{isabelle}\ \ \ \ \ %%% |
237 \begin{isabelle}\ \ \ \ \ %%% |
236 @{thm concat_empty_fset[THEN eq_reflection]}\hspace{10mm} |
238 \begin{tabular}{@ {}l} |
237 @{thm concat_insert_fset[THEN eq_reflection]} |
239 @{thm concat_empty_fset[THEN eq_reflection]}\\ |
|
240 @{thm concat_insert_fset[THEN eq_reflection, where x1="x" and S1="S"]} |
|
241 \end{tabular} |
238 \end{isabelle} |
242 \end{isabelle} |
239 |
243 |
240 \noindent |
244 \noindent |
241 The quotient package should automatically provide us with a definition for @{text "\<Union>"} in |
245 The quotient package should automatically provide us with a definition for @{text "\<Union>"} in |
242 terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is |
246 terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is |