# HG changeset patch
# User Andreas Lochbihler
# Date 1477326330 -7200
# Node ID 4b22e1268779d4ebbd25d9ecf84da75567f46084
# Parent  71f42dcaa1df2f3732d339a81d3c94d746c21ca3
document transfer_prover_eq and friend_of_corec_simps

diff -r 71f42dcaa1df -r 4b22e1268779 src/Doc/Corec/Corec.thy
--- a/src/Doc/Corec/Corec.thy	Mon Oct 24 16:53:32 2016 +0200
+++ b/src/Doc/Corec/Corec.thy	Mon Oct 24 18:25:30 2016 +0200
@@ -58,7 +58,7 @@
 command, or by passing the @{text friend} option to @{command corec}. The
 friendliness check relies on an internal syntactic check in combination with
 a parametricity subgoal, which must be discharged manually (typically using
-@{method transfer_prover}).
+@{method transfer_prover} or @{method transfer_prover_eq}).
 
 Third, @{command corec} allows self-calls that are not guarded by a constructor,
 as long as these calls occur in a friendly context (a context consisting
@@ -163,7 +163,10 @@
 specified and is trivial to discharge. The second subgoal is a parametricity
 property that captures the the requirement that the function may destruct at
 most one constructor of input to produce one constructor of output. This subgoal
-can usually be discharged using the @{text transfer_prover} proof method.
+can usually be discharged using the @{text transfer_prover} or 
+@{method transfer_prover_eq} proof method. The latter replaces equality relations
+by their relator terms according to the theorem collection @{thm [source] relator_eq}
+before it calles @{method transfer_prover}.
 
 After registering @{const ssum} as a friend, we can use it in the corecursive
 call context, either inside or outside the constructor guard:
@@ -195,7 +198,7 @@
 
 text \<open>
 \noindent
-The parametricity subgoal is given to @{text transfer_prover}.
+The parametricity subgoal is given to @{text transfer_prover_eq}.
 
 The @{const sprod} and @{const sexp} functions provide shuffle product and
 exponentiation on streams. We can use them to define the stream of factorial
@@ -656,7 +659,7 @@
 \end{itemize}
 
 The @{command corec} command is an abbreviation for @{command corecursive}
-with appropriate applications of @{method transfer_prover} and
+with appropriate applications of @{method transfer_prover_eq} and
 @{method lexicographic_order} to discharge any emerging proof obligations.
 \<close>
 
@@ -667,6 +670,8 @@
 text \<open>
 \begin{matharray}{rcl}
   @{command_def "friend_of_corec"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
+  \\
+  @{attribute_def "friend_of_corec_simps"} & : & @{text "attribute"}
 \end{matharray}
 
 @{rail \<open>
@@ -700,10 +705,20 @@
 The @{text transfer} option indicates that an unconditional transfer rule
 should be generated and proved @{text "by transfer_prover"}. The
 @{text "[transfer_rule]"} attribute is set on the generated theorem.
+
+\item
+The attribute @{attribute friend_of_corec_simps} declares naturality theorems
+to be used by @{command friend_of_corec} and @{text "corec (friend)"} in deriving
+the user specification from reduction to primitive corecursion.
+Internally, they derive naturality theorems from the parametricity proof obligations
+dischared by the user or the method @{method transfer_prover_eq}, but this derivation
+fails if in the arguments of a higher-order constant a type variable occurs on both
+sides of the function type constructor. In that case, the required naturality
+theorem can be declared with @{attribute friend_of_corec_simps}. See 
+@{file "~~/src/HOL/Corec_Examples/Tests/Iterate_GPV.thy"} for an example.
 \end{itemize}
 \<close>
 
-
 subsection \<open>\keyw{coinduction_upto}
   \label{ssec:coinduction-upto-syntax}\<close>
 
@@ -878,6 +893,18 @@
 details.
 \<close>
 
+subsection \<open>\textit{transfer_prover_eq}
+  \label{ssec:transfer-prover-eq}\<close>
+
+text \<open>
+The proof method @{method transfer_prover_eq} replaces the equality relation
+@{term "op ="} with compound relator expressions according to 
+@{thm [source] relator_eq} before calling @{method transfer_prover} on the
+current subgoal. It works better than plain @{method transfer_prover} on 
+the parametricity proof obligations of @{command corecursive} and 
+@{command friend_of_corec}, as they often contain equality relations on complex
+types, which @{method transfer_prover} does not like.
+\<close>
 
 section \<open>Known Bugs and Limitations
   \label{sec:known-bugs-and-limitations}\<close>