1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Jul 27 20:28:00 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Jul 28 05:52:28 2011 -0200
     1.3 @@ -1849,6 +1849,75 @@
     1.4  \end{isamarkuptext}%
     1.5  \isamarkuptrue%
     1.6  %
     1.7 +\isamarkupsection{Coercive subtyping%
     1.8 +}
     1.9 +\isamarkuptrue%
    1.10 +%
    1.11 +\begin{isamarkuptext}%
    1.12 +\begin{matharray}{rcl}
    1.13 +    \indexdef{HOL}{attribute}{coercion}\hypertarget{attribute.HOL.coercion}{\hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}} & : & \isa{attribute} \\
    1.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} \\
    1.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} \\
    1.16 +  \end{matharray}
    1.17 +
    1.18 +  \begin{railoutput}
    1.19 +\rail@begin{2}{}
    1.20 +\rail@term{\hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}}[]
    1.21 +\rail@bar
    1.22 +\rail@nextbar{1}
    1.23 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    1.24 +\rail@endbar
    1.25 +\rail@end
    1.26 +\end{railoutput}
    1.27 +
    1.28 +  \begin{railoutput}
    1.29 +\rail@begin{2}{}
    1.30 +\rail@term{\hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}}[]
    1.31 +\rail@bar
    1.32 +\rail@nextbar{1}
    1.33 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    1.34 +\rail@endbar
    1.35 +\rail@end
    1.36 +\end{railoutput}
    1.37 +
    1.38 +
    1.39 +  Coercive subtyping allows the user to omit explicit type conversions,
    1.40 +  also called \emph{coercions}.  Type inference will add them as
    1.41 +  necessary when parsing a term. See
    1.42 +  \cite{traytel-berghofer-nipkow-2011} for details.
    1.43 +
    1.44 +  \begin{description}
    1.45 +
    1.46 +  \item \hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}~\isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} registers a new
    1.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
    1.48 +  composed by the inference algorithm if needed. Note that the type
    1.49 +  inference algorithm is complete only if the registered coercions form
    1.50 +  a lattice.
    1.51 +
    1.52 +
    1.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
    1.54 +  map function to lift coercions through type constructors. The function
    1.55 +  \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} must conform to the following type pattern
    1.56 +
    1.57 +  \begin{matharray}{lll}
    1.58 +    \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} &
    1.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}}} \\
    1.60 +  \end{matharray}
    1.61 +
    1.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
    1.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
    1.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}}}.
    1.65 +  Registering a map function overwrites any existing map function for
    1.66 +  this particular type constructor.
    1.67 +
    1.68 +
    1.69 +  \item \hyperlink{attribute.HOL.coercion-enabled}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}enabled}}} enables the coercion
    1.70 +  inference algorithm.
    1.71 +
    1.72 +  \end{description}%
    1.73 +\end{isamarkuptext}%
    1.74 +\isamarkuptrue%
    1.75 +%
    1.76  \isamarkupsection{Arithmetic proof support%
    1.77  }
    1.78  \isamarkuptrue%