# HG changeset patch
# User traytel
# Date 1438683581 -7200
# Node ID c362049f3f842841a9af605771bdf66c6f22372d
# Parent  c5db501da8e4675fde05e708e604967237f02393
more documentation of coercions

diff -r c5db501da8e4 -r c362049f3f84 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Jul 30 21:56:19 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Tue Aug 04 12:19:41 2015 +0200
@@ -2078,8 +2078,10 @@
 text \<open>
   \begin{matharray}{rcl}
     @{attribute_def (HOL) coercion} & : & @{text attribute} \\
+    @{attribute_def (HOL) coercion_delete} & : & @{text attribute} \\
     @{attribute_def (HOL) coercion_enabled} & : & @{text attribute} \\
     @{attribute_def (HOL) coercion_map} & : & @{text attribute} \\
+    @{attribute_def (HOL) coercion_args} & : & @{text attribute} \\
   \end{matharray}
 
   Coercive subtyping allows the user to omit explicit type
@@ -2088,9 +2090,13 @@
   @{cite "traytel-berghofer-nipkow-2011"} for details.
 
   @{rail \<open>
-    @@{attribute (HOL) coercion} (@{syntax term})?
+    @@{attribute (HOL) coercion} (@{syntax term})
+    ;
+    @@{attribute (HOL) coercion_delete} (@{syntax term})
     ;
-    @@{attribute (HOL) coercion_map} (@{syntax term})?
+    @@{attribute (HOL) coercion_map} (@{syntax term})
+    ;
+    @@{attribute (HOL) coercion_args} (@{syntax const}) (('+' | '0' | '-')+)
   \<close>}
 
   \begin{description}
@@ -2102,6 +2108,10 @@
   inference algorithm is complete only if the registered coercions
   form a lattice.
 
+  \item @{attribute (HOL) "coercion_delete"}~@{text "f"} deletes a
+  preceding declaration (using @{attribute (HOL) "coercion"}) of the
+  function @{text "f :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2"} as a coercion.
+
   \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
@@ -2116,6 +2126,21 @@
   overwrites any existing map function for this particular type
   constructor.
 
+  \item @{attribute (HOL) "coercion_args"} can be used to disallow
+  coercions to be inserted in certain positions in a term. For example,
+  given the constant @{text "c :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2 \<Rightarrow> \<sigma>\<^sub>3 \<Rightarrow> \<sigma>\<^sub>4"} and the list
+  of policies @{text "- + 0"} as arguments, coercions will not be
+  inserted in the first argument of @{text "c"} (policy @{text "-"});
+  they may be inserted in the second argument (policy @{text "+"})
+  even if the constant @{text "c"} itself is in a position where
+  coercions are disallowed; the third argument inherits the allowance
+  of coercsion insertion from the position of the constant @{text "c"}
+  (policy @{text "0"}). The standard usage of policies is the definition
+  of syntatic constructs (usually extralogical, i.e., processed and
+  stripped during type inference), that should not be destroyed by the
+  insertion of coercions (see, for example, the setup for the case syntax
+  in @{theory Ctr_Sugar}). 
+
   \item @{attribute (HOL) "coercion_enabled"} enables the coercion
   inference algorithm.
 
diff -r c5db501da8e4 -r c362049f3f84 src/Doc/Isar_Ref/document/root.tex
--- a/src/Doc/Isar_Ref/document/root.tex	Thu Jul 30 21:56:19 2015 +0200
+++ b/src/Doc/Isar_Ref/document/root.tex	Tue Aug 04 12:19:41 2015 +0200
@@ -45,8 +45,9 @@
   Lars Noschinski,
   David von Oheimb, \\
   Larry Paulson,
-  Sebastian Skalberg,
-  Christian Sternagel
+  Sebastian Skalberg, \\
+  Christian Sternagel,
+  Dmitriy Traytel
 }
 
 \makeindex