330 |
330 |
331 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ |
331 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ |
332 @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\\ |
332 @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\\ |
333 @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\ |
333 @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\ |
334 \multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\ |
334 \multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\ |
335 @{text "ABS (\<sigma>\<^isub>1 \<rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\ |
335 @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\ |
336 @{text "REP (\<sigma>\<^isub>1 \<rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\ |
336 @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\ |
337 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ |
337 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ |
338 @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\ |
338 @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\ |
339 @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\ |
339 @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\ |
340 \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\ |
340 \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\ |
341 @{text "ABS (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>2 \<circ> (MAP(\<rho>s \<kappa>\<^isub>1) (ABS (\<sigma>s', \<tau>s')))"}\\ |
341 @{text "ABS (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>2 \<circ> (MAP(\<rho>s \<kappa>\<^isub>1) (ABS (\<sigma>s', \<tau>s')))"}\\ |
354 The function @{text "MAP"} calculates an \emph{aggregate map-function} for a type |
354 The function @{text "MAP"} calculates an \emph{aggregate map-function} for a type |
355 as follows: |
355 as follows: |
356 |
356 |
357 \begin{center} |
357 \begin{center} |
358 \begin{tabular}{rcl} |
358 \begin{tabular}{rcl} |
359 @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "\<alpha>"}\\ |
359 @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a"}\\ |
|
360 @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id"}\\ |
360 @{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\ |
361 @{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\ |
361 @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>\<alpha>s. MAP'(\<sigma>)"} |
362 @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"} |
362 \end{tabular} |
363 \end{tabular} |
363 \end{center} |
364 \end{center} |
364 |
365 |
365 \noindent |
366 \noindent |
366 In this definition we abuse the fact that we can interpret type-variables as |
367 In this definition we abuse the fact that we can interpret type-variables @{text \<alpha>} as |
367 term variables, and in the last clause build the abstraction over all |
368 term variables @{text a}, and in the last clause build an abstraction over all |
368 term-variables inside the aggregate map-function generated by @{text "MAP'"}. |
369 term-variables inside the aggregate map-function generated by @{text "MAP'"}. |
369 |
370 This aggregate map-function is necessary if we build quotients, say @{text "(\<alpha>, \<beta>) foo"}, |
|
371 out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}. In this case @{text MAP} |
|
372 generates the aggregate map-function: |
|
373 |
|
374 @{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"} |
|
375 |
|
376 \noindent |
|
377 Returning to our example about @{term "concat"} and @{term "fconcat"} which have the |
|
378 types @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. Feeding this |
|
379 into @{text ABS} gives us the abstraction function: |
|
380 |
|
381 @{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"} |
|
382 |
|
383 \noindent |
|
384 where we already performed some @{text "\<beta>"}-simplifications. In our implementation |
|
385 we further simplified this by noticing the usual laws about @{text "map"}s and @{text "id"}, |
|
386 namely @{term "map id = id"} and |
|
387 @{text "f \<circ> id = id \<circ> f = f"}. This gives us the simplified abstarction function |
|
388 |
|
389 @{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"} |
|
390 |
|
391 \noindent |
|
392 which we can use for defining @{term "fconcat"} as follows |
|
393 |
|
394 @{text [display, indent=10] "\<Union> \<equiv> ((map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"} |
370 |
395 |
371 Apart from the last 2 points the definition is same as the one implemented in |
396 Apart from the last 2 points the definition is same as the one implemented in |
372 in Homeier's HOL package. Adding composition in last two cases is necessary |
397 in Homeier's HOL package. Adding composition in last two cases is necessary |
373 for compositional quotients. We illustrate the different behaviour of the |
398 for compositional quotients. We illustrate the different behaviour of the |
374 definition by showing the derived definition of @{term fconcat}: |
399 definition by showing the derived definition of @{term fconcat}: |
392 If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"} |
417 If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"} |
393 and @{text "REP (\<sigma>, \<tau>)"} some representation function @{text "Rep"}, |
418 and @{text "REP (\<sigma>, \<tau>)"} some representation function @{text "Rep"}, |
394 then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type |
419 then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type |
395 @{text "\<tau> \<Rightarrow> \<sigma>"}. |
420 @{text "\<tau> \<Rightarrow> \<sigma>"}. |
396 \end{lemma} |
421 \end{lemma} |
|
422 |
|
423 This lemma fails in the over-simplified abstraction and representation function used |
|
424 in Homeier's quotient package. |
397 *} |
425 *} |
398 |
426 |
399 subsection {* Respectfulness *} |
427 subsection {* Respectfulness *} |
400 |
428 |
401 text {* |
429 text {* |