document coercions
authornoschinl
Thu, 28 Jul 2011 05:52:28 -0200
changeset 448655de4bde3ad41
parent 44864 b141d7a3d4e3
child 44866 c479836d9048
document coercions
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
doc-src/manual.bib
     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},