# HG changeset patch # User noschinl # Date 1311839548 7200 # Node ID 5de4bde3ad41577870c3cb29f3277802ade238da # Parent b141d7a3d4e323bf9c9bb129a20745f14435be85 document coercions diff -r b141d7a3d4e3 -r 5de4bde3ad41 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Jul 27 20:28:00 2011 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Jul 28 05:52:28 2011 -0200 @@ -1283,6 +1283,63 @@ *} +section {* Coercive subtyping *} + +text {* + \begin{matharray}{rcl} + @{attribute_def (HOL) coercion} & : & @{text attribute} \\ + @{attribute_def (HOL) coercion_enabled} & : & @{text attribute} \\ + @{attribute_def (HOL) coercion_map} & : & @{text attribute} \\ + \end{matharray} + + @{rail " + @@{attribute (HOL) coercion} (@{syntax term})? + ; + "} + @{rail " + @@{attribute (HOL) coercion_map} (@{syntax term})? + ; + "} + + Coercive subtyping allows the user to omit explicit type conversions, + also called \emph{coercions}. Type inference will add them as + necessary when parsing a term. See + \cite{traytel-berghofer-nipkow-2011} for details. + + \begin{description} + + \item @{attribute (HOL) "coercion"}~@{text "f"} registers a new + coercion function @{text "f :: \\<^isub>1 \ + \\<^isub>2"} where @{text "\\<^isub>1"} and @{text + "\\<^isub>2"} are nullary type constructors. Coercions are + composed by the inference algorithm if needed. Note that the type + inference algorithm is complete only if the registered coercions form + a lattice. + + + \item @{attribute (HOL) "coercion_map"}~@{text "map"} registers a new + map function to lift coercions through type constructors. The function + @{text "map"} must conform to the following type pattern + + \begin{matharray}{lll} + @{text "map"} & @{text "::"} & + @{text "f\<^isub>1 \ \ \ f\<^isub>n \ (\\<^isub>1, \, \\<^isub>n) t \ (\\<^isub>1, \, \\<^isub>n) t"} \\ + \end{matharray} + + where @{text "t"} is a type constructor and @{text "f\<^isub>i"} is of + type @{text "\\<^isub>i \ \\<^isub>i"} or + @{text "\\<^isub>i \ \\<^isub>i"}. + Registering a map function overwrites any existing map function for + this particular type constructor. + + + \item @{attribute (HOL) "coercion_enabled"} enables the coercion + inference algorithm. + + \end{description} + +*} + section {* Arithmetic proof support *} text {* diff -r b141d7a3d4e3 -r 5de4bde3ad41 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Jul 27 20:28:00 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Jul 28 05:52:28 2011 -0200 @@ -1849,6 +1849,75 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsection{Coercive subtyping% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{HOL}{attribute}{coercion}\hypertarget{attribute.HOL.coercion}{\hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}} & : & \isa{attribute} \\ + \indexdef{HOL}{attribute}{coercion\_enabled}\hypertarget{attribute.HOL.coercion-enabled}{\hyperlink{attribute.HOL.coercion-enabled}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}enabled}}}} & : & \isa{attribute} \\ + \indexdef{HOL}{attribute}{coercion\_map}\hypertarget{attribute.HOL.coercion-map}{\hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}} & : & \isa{attribute} \\ + \end{matharray} + + \begin{railoutput} +\rail@begin{2}{} +\rail@term{\hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}}[] +\rail@bar +\rail@nextbar{1} +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] +\rail@endbar +\rail@end +\end{railoutput} + + \begin{railoutput} +\rail@begin{2}{} +\rail@term{\hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}}[] +\rail@bar +\rail@nextbar{1} +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] +\rail@endbar +\rail@end +\end{railoutput} + + + Coercive subtyping allows the user to omit explicit type conversions, + also called \emph{coercions}. Type inference will add them as + necessary when parsing a term. See + \cite{traytel-berghofer-nipkow-2011} for details. + + \begin{description} + + \item \hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}~\isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} registers a new + coercion function \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} where \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} are nullary type constructors. Coercions are + composed by the inference algorithm if needed. Note that the type + inference algorithm is complete only if the registered coercions form + a lattice. + + + \item \hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}~\isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} registers a new + map function to lift coercions through type constructors. The function + \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} must conform to the following type pattern + + \begin{matharray}{lll} + \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & + \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ f\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} \\ + \end{matharray} + + where \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} is a type constructor and \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} is of + type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} or + \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}}. + Registering a map function overwrites any existing map function for + this particular type constructor. + + + \item \hyperlink{attribute.HOL.coercion-enabled}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}enabled}}} enables the coercion + inference algorithm. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsection{Arithmetic proof support% } \isamarkuptrue% diff -r b141d7a3d4e3 -r 5de4bde3ad41 doc-src/manual.bib --- a/doc-src/manual.bib Wed Jul 27 20:28:00 2011 +0200 +++ b/doc-src/manual.bib Thu Jul 28 05:52:28 2011 -0200 @@ -1570,6 +1570,15 @@ year = 2007, publisher = Springer} +@unpublished{traytel-berghofer-nipkow-2011, + author = {D. Traytel and S. Berghofer and T. Nipkow}, + title = {Extending Hindley-Milner Type Inference with Coercive + Subtyping (long version)}, + year = 2011, + note = {Submitted, + \url{http://isabelle.in.tum.de/doc/implementation.pdf}}}, +} + @Unpublished{Trybulec:1993:MizarFeatures, author = {A. Trybulec}, title = {Some Features of the {Mizar} Language},