1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Jul 27 20:28:00 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Jul 28 05:52:28 2011 -0200
1.3 @@ -1283,6 +1283,63 @@
1.4
1.5 *}
1.6
1.7 +section {* Coercive subtyping *}
1.8 +
1.9 +text {*
1.10 + \begin{matharray}{rcl}
1.11 + @{attribute_def (HOL) coercion} & : & @{text attribute} \\
1.12 + @{attribute_def (HOL) coercion_enabled} & : & @{text attribute} \\
1.13 + @{attribute_def (HOL) coercion_map} & : & @{text attribute} \\
1.14 + \end{matharray}
1.15 +
1.16 + @{rail "
1.17 + @@{attribute (HOL) coercion} (@{syntax term})?
1.18 + ;
1.19 + "}
1.20 + @{rail "
1.21 + @@{attribute (HOL) coercion_map} (@{syntax term})?
1.22 + ;
1.23 + "}
1.24 +
1.25 + Coercive subtyping allows the user to omit explicit type conversions,
1.26 + also called \emph{coercions}. Type inference will add them as
1.27 + necessary when parsing a term. See
1.28 + \cite{traytel-berghofer-nipkow-2011} for details.
1.29 +
1.30 + \begin{description}
1.31 +
1.32 + \item @{attribute (HOL) "coercion"}~@{text "f"} registers a new
1.33 + coercion function @{text "f :: \<sigma>\<^isub>1 \<Rightarrow>
1.34 + \<sigma>\<^isub>2"} where @{text "\<sigma>\<^isub>1"} and @{text
1.35 + "\<sigma>\<^isub>2"} are nullary type constructors. Coercions are
1.36 + composed by the inference algorithm if needed. Note that the type
1.37 + inference algorithm is complete only if the registered coercions form
1.38 + a lattice.
1.39 +
1.40 +
1.41 + \item @{attribute (HOL) "coercion_map"}~@{text "map"} registers a new
1.42 + map function to lift coercions through type constructors. The function
1.43 + @{text "map"} must conform to the following type pattern
1.44 +
1.45 + \begin{matharray}{lll}
1.46 + @{text "map"} & @{text "::"} &
1.47 + @{text "f\<^isub>1 \<Rightarrow> \<dots> \<Rightarrow> f\<^isub>n \<Rightarrow> (\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n) t \<Rightarrow> (\<beta>\<^isub>1, \<dots>, \<beta>\<^isub>n) t"} \\
1.48 + \end{matharray}
1.49 +
1.50 + where @{text "t"} is a type constructor and @{text "f\<^isub>i"} is of
1.51 + type @{text "\<alpha>\<^isub>i \<Rightarrow> \<beta>\<^isub>i"} or
1.52 + @{text "\<beta>\<^isub>i \<Rightarrow> \<alpha>\<^isub>i"}.
1.53 + Registering a map function overwrites any existing map function for
1.54 + this particular type constructor.
1.55 +
1.56 +
1.57 + \item @{attribute (HOL) "coercion_enabled"} enables the coercion
1.58 + inference algorithm.
1.59 +
1.60 + \end{description}
1.61 +
1.62 +*}
1.63 +
1.64 section {* Arithmetic proof support *}
1.65
1.66 text {*
2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Jul 27 20:28:00 2011 +0200
2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Jul 28 05:52:28 2011 -0200
2.3 @@ -1849,6 +1849,75 @@
2.4 \end{isamarkuptext}%
2.5 \isamarkuptrue%
2.6 %
2.7 +\isamarkupsection{Coercive subtyping%
2.8 +}
2.9 +\isamarkuptrue%
2.10 +%
2.11 +\begin{isamarkuptext}%
2.12 +\begin{matharray}{rcl}
2.13 + \indexdef{HOL}{attribute}{coercion}\hypertarget{attribute.HOL.coercion}{\hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}} & : & \isa{attribute} \\
2.14 + \indexdef{HOL}{attribute}{coercion\_enabled}\hypertarget{attribute.HOL.coercion-enabled}{\hyperlink{attribute.HOL.coercion-enabled}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}enabled}}}} & : & \isa{attribute} \\
2.15 + \indexdef{HOL}{attribute}{coercion\_map}\hypertarget{attribute.HOL.coercion-map}{\hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}} & : & \isa{attribute} \\
2.16 + \end{matharray}
2.17 +
2.18 + \begin{railoutput}
2.19 +\rail@begin{2}{}
2.20 +\rail@term{\hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}}[]
2.21 +\rail@bar
2.22 +\rail@nextbar{1}
2.23 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
2.24 +\rail@endbar
2.25 +\rail@end
2.26 +\end{railoutput}
2.27 +
2.28 + \begin{railoutput}
2.29 +\rail@begin{2}{}
2.30 +\rail@term{\hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}}[]
2.31 +\rail@bar
2.32 +\rail@nextbar{1}
2.33 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
2.34 +\rail@endbar
2.35 +\rail@end
2.36 +\end{railoutput}
2.37 +
2.38 +
2.39 + Coercive subtyping allows the user to omit explicit type conversions,
2.40 + also called \emph{coercions}. Type inference will add them as
2.41 + necessary when parsing a term. See
2.42 + \cite{traytel-berghofer-nipkow-2011} for details.
2.43 +
2.44 + \begin{description}
2.45 +
2.46 + \item \hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}~\isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} registers a new
2.47 + 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
2.48 + composed by the inference algorithm if needed. Note that the type
2.49 + inference algorithm is complete only if the registered coercions form
2.50 + a lattice.
2.51 +
2.52 +
2.53 + \item \hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}~\isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} registers a new
2.54 + map function to lift coercions through type constructors. The function
2.55 + \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} must conform to the following type pattern
2.56 +
2.57 + \begin{matharray}{lll}
2.58 + \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} &
2.59 + \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}}} \\
2.60 + \end{matharray}
2.61 +
2.62 + 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
2.63 + 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
2.64 + \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}}.
2.65 + Registering a map function overwrites any existing map function for
2.66 + this particular type constructor.
2.67 +
2.68 +
2.69 + \item \hyperlink{attribute.HOL.coercion-enabled}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}enabled}}} enables the coercion
2.70 + inference algorithm.
2.71 +
2.72 + \end{description}%
2.73 +\end{isamarkuptext}%
2.74 +\isamarkuptrue%
2.75 +%
2.76 \isamarkupsection{Arithmetic proof support%
2.77 }
2.78 \isamarkuptrue%
3.1 --- a/doc-src/manual.bib Wed Jul 27 20:28:00 2011 +0200
3.2 +++ b/doc-src/manual.bib Thu Jul 28 05:52:28 2011 -0200
3.3 @@ -1570,6 +1570,15 @@
3.4 year = 2007,
3.5 publisher = Springer}
3.6
3.7 +@unpublished{traytel-berghofer-nipkow-2011,
3.8 + author = {D. Traytel and S. Berghofer and T. Nipkow},
3.9 + title = {Extending Hindley-Milner Type Inference with Coercive
3.10 + Subtyping (long version)},
3.11 + year = 2011,
3.12 + note = {Submitted,
3.13 + \url{http://isabelle.in.tum.de/doc/implementation.pdf}}},
3.14 +}
3.15 +
3.16 @Unpublished{Trybulec:1993:MizarFeatures,
3.17 author = {A. Trybulec},
3.18 title = {Some Features of the {Mizar} Language},