159 @{text "Abs::nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep::int \<Rightarrow> nat \<times> nat"} |
159 @{text "Abs::nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep::int \<Rightarrow> nat \<times> nat"} |
160 \end{isabelle} |
160 \end{isabelle} |
161 |
161 |
162 \noindent |
162 \noindent |
163 However we often leave this typing information implicit for better |
163 However we often leave this typing information implicit for better |
164 readability. Every abstraction and representation function stands for an |
164 readability, but sometimes write @{text Abs_int} and @{text Rep_int} if the |
165 isomorphism between the non-empty subset and elements in the new type. They |
165 typing information is important. Every abstraction and representation |
166 are necessary for making definitions involving the new type. For example |
166 function stands for an isomorphism between the non-empty subset and elements |
167 @{text "0"} and @{text "1"} of type @{typ int} can be defined as |
167 in the new type. They are necessary for making definitions involving the new |
168 |
168 type. For example @{text "0"} and @{text "1"} of type @{typ int} can be |
|
169 defined as |
169 |
170 |
170 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
171 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
171 @{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"} |
172 @{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"} |
172 \end{isabelle} |
173 \end{isabelle} |
173 |
174 |
332 @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\ |
333 @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\ |
333 \multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\ |
334 \multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\ |
334 @{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)"}\\ |
335 @{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\\ |
336 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ |
337 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ |
337 @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "\<kappa>_map (ABS (\<sigma>s, \<tau>s))"}\\ |
338 @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\ |
338 @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "\<kappa>_map (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\\ |
339 \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\ |
340 \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\ |
340 @{text "ABS (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "\<kappa>\<^isub>2_Abs \<circ> \<kappa>\<^isub>1_map (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')))"}\\ |
341 @{text "REP (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "\<kappa>\<^isub>1_map (REP (\<sigma>s', \<tau>s')) \<circ> \<kappa>\<^isub>2_Rep"}\\ |
342 @{text "REP (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>\<^isub>1) (REP (\<sigma>s', \<tau>s'))) \<circ> Rep_\<kappa>\<^isub>2"}\\ |
342 \end{tabular} |
343 \end{tabular} |
343 \end{center} |
344 \end{center} |
344 |
345 |
|
346 \noindent |
|
347 where in the last two clauses we have that the quotient type @{text "\<alpha>s \<kappa>\<^isub>2"} is a quotient of |
|
348 the raw type @{text "\<rho>s \<kappa>\<^isub>1"} (for example @{text "\<alpha> fset"} and @{text "\<alpha> list"}). |
|
349 The quotient construction ensures that the type variables in @{text "\<rho>s"} |
|
350 must be amongst the @{text "\<alpha>s"}. Now the @{text "\<sigma>s'"} are given by the matchers |
|
351 for the @{text "\<alpha>s"} |
|
352 when matching @{text "\<sigma>s \<kappa>\<^isub>2"} against @{text "\<alpha>s \<kappa>\<^isub>2"}; similarly the @{text "\<tau>s'"} are given by the |
|
353 same type-variables when matching @{text "\<tau>s \<kappa>\<^isub>1"} against @{text "\<rho>s \<kappa>\<^isub>1"}. |
|
354 The function @{text "MAP"} calculates an \emph{aggregate map-function} for a type |
|
355 as follows: |
|
356 |
345 \begin{center} |
357 \begin{center} |
346 \begin{tabular}{rcl} |
358 \begin{tabular}{rcl} |
347 @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n) \<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m) \<kappa>\<^isub>2)"} = @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"}\\ |
359 @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "\<alpha>"}\\ |
348 @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n) \<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m) \<kappa>\<^isub>2)"} = @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"}\\ |
360 @{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\ |
349 provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"} |
361 @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>\<alpha>s. MAP'(\<sigma>)"} |
350 \end{tabular} |
362 \end{tabular} |
351 \end{center} |
363 \end{center} |
|
364 |
|
365 \noindent |
|
366 In this definition we abuse the fact that we can interpret type-variables as |
|
367 term variables, and in the last clause build the abstraction over all |
|
368 term-variables inside the aggregate map-function generated by @{text "MAP'"}. |
|
369 |
352 |
370 |
353 Apart from the last 2 points the definition is same as the one implemented in |
371 Apart from the last 2 points the definition is same as the one implemented in |
354 in Homeier's HOL package. Adding composition in last two cases is necessary |
372 in Homeier's HOL package. Adding composition in last two cases is necessary |
355 for compositional quotients. We illustrate the different behaviour of the |
373 for compositional quotients. We illustrate the different behaviour of the |
356 definition by showing the derived definition of @{term fconcat}: |
374 definition by showing the derived definition of @{term fconcat}: |