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 {*