# HG changeset patch # User wenzelm # Date 1477336478 -7200 # Node ID 14571c9e1d5077993f4558a44b2c087c2e3e3b13 # Parent f8c1c12d6af52ee1aa4b266f9ed1402cda09cfef# Parent 2a4672722aaa1e3aa3638df09d28e0873297262b merged diff -r 2a4672722aaa -r 14571c9e1d50 src/Doc/Corec/Corec.thy --- a/src/Doc/Corec/Corec.thy Mon Oct 24 20:57:58 2016 +0200 +++ b/src/Doc/Corec/Corec.thy Mon Oct 24 21:14:38 2016 +0200 @@ -9,10 +9,7 @@ *) theory Corec -imports - GCD - "../Datatypes/Setup" - "~~/src/HOL/Library/BNF_Corec" +imports GCD "../Datatypes/Setup" "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/FSet" begin @@ -75,11 +72,11 @@ The package fully adheres to the LCF philosophy @{cite mgordon79}: The characteristic theorems associated with the specified corecursive functions are -derived rather than introduced axiomatically.% -\footnote{However, most of the internal proof obligations are omitted if the -@{text quick_and_dirty} option is enabled.} +derived rather than introduced axiomatically. +(Exceptionally, most of the internal proof obligations are omitted if the +@{text quick_and_dirty} option is enabled.) The package is described in a pair of scientific papers -@{cite "blanchette-et-al-2015-fouco" and "blanchette-et-al-2016-fouco2"}. Some +@{cite "blanchette-et-al-2015-fouco" and "blanchette-et-al-201x-amico"}. Some of the text and examples below originate from there. This tutorial is organized as follows: @@ -96,8 +93,13 @@ \item Section \ref{sec:generated-theorems}, ``Generated Theorems,'' lists the theorems produced by the package's commands. -\item Section \ref{sec:proof-method}, ``Proof Method,'' briefly describes the -@{method corec_unique} proof method. +\item Section \ref{sec:proof-methods}, ``Proof Methods,'' briefly describes the +@{method corec_unique} and @{method transfer_prover_eq} proof methods. + +\item Section \ref{sec:attribute}, ``Attribute,'' briefly describes the +@{attribute friend_of_corec_simps} attribute, which can be used to strengthen +the tactics underlying the @{command friend_of_corec} and @{command corec} +@{text "(friend)"} commands. \item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and Limitations,'' concludes with known open issues. @@ -163,10 +165,11 @@ 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} 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}. +can usually be discharged using the @{text transfer_prover} or +@{method transfer_prover_eq} proof method (Section~\ref{ssec:transfer-prover-eq}). +The latter replaces equality relations by their relator terms according to the +@{thm [source] relator_eq} theorem collection before it invokes +@{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: @@ -198,7 +201,8 @@ text \ \noindent -The parametricity subgoal is given to @{text transfer_prover_eq}. +The parametricity subgoal is given to @{text transfer_prover_eq} +(Section~\ref{ssec: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 @@ -259,8 +263,8 @@ \noindent Here, @{const map} is the standard map function on lists, and @{const zip} converts two parallel lists into a list of pairs. The @{const tsum} function is -primitively corecursive. Instead of @{text "corec (friend)"}, we could also have -used \keyw{primcorec} and @{command friend_of_corec}, as we did for +primitively corecursive. Instead of @{command corec} @{text "(friend)"}, we could +also have used \keyw{primcorec} and @{command friend_of_corec}, as we did for @{const ssum}. Once @{const tsum} is registered as friendly, we can use it in the corecursive @@ -659,8 +663,9 @@ \end{itemize} The @{command corec} command is an abbreviation for @{command corecursive} -with appropriate applications of @{method transfer_prover_eq} and -@{method lexicographic_order} to discharge any emerging proof obligations. +with appropriate applications of @{method transfer_prover_eq} +(Section~\ref{ssec:transfer-prover-eq}) and @{method lexicographic_order} to +discharge any emerging proof obligations. \ @@ -670,8 +675,6 @@ text \ \begin{matharray}{rcl} @{command_def "friend_of_corec"} & : & @{text "local_theory \ proof(prove)"} - \\ - @{attribute_def "friend_of_corec_simps"} & : & @{text "attribute"} \end{matharray} @{rail \ @@ -705,20 +708,10 @@ 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} \ + subsection \\keyw{coinduction_upto} \label{ssec:coinduction-upto-syntax}\ @@ -881,8 +874,8 @@ \ -section \Proof Method - \label{sec:proof-method}\ +section \Proof Methods + \label{sec:proof-methods}\ subsection \\textit{corec_unique} \label{ssec:corec-unique}\ @@ -893,19 +886,41 @@ details. \ + subsection \\textit{transfer_prover_eq} \label{ssec:transfer-prover-eq}\ text \ -The proof method @{method transfer_prover_eq} replaces the equality relation -@{term "op ="} with compound relator expressions according to +The @{method transfer_prover_eq} proof method 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. +current subgoal. It tends to work better than plain @{method transfer_prover} on +the parametricity proof obligations of @{command corecursive} and +@{command friend_of_corec}, because they often contain equality relations on +complex types, which @{method transfer_prover} cannot reason about. \ + +section \Attribute + \label{sec:attribute}\ + + +subsection \\textit{friend_of_corec_simps} + \label{ssec:friend-of-corec-simps}\ + +text \ +The @{attribute friend_of_corec_simps} attribute declares naturality theorems +to be used by @{command friend_of_corec} and @{command corec} @{text "(friend)"} in +deriving the user specification from reduction to primitive corecursion. +Internally, these commands derive naturality theorems from the parametricity proof +obligations dischared by the user or the @{method transfer_prover_eq} method, 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. The required naturality +theorem can then be declared with @{attribute friend_of_corec_simps}. See +@{file "~~/src/HOL/Corec_Examples/Tests/Iterate_GPV.thy"} for an example. +\ + + section \Known Bugs and Limitations \label{sec:known-bugs-and-limitations}\ @@ -925,6 +940,9 @@ \item \emph{The internal tactics may fail on legal inputs.} +In some cases, this limitation can be circumvented using the +@{attribute friend_of_corec_simps} attribute +(Section~\ref{ssec:friend-of-corec-simps}). \item \emph{The @{text transfer} option is not implemented yet.} @@ -939,6 +957,14 @@ \item \emph{The package does not interact well with locales.} +\item +\emph{The undocumented @{text corecUU_transfer} theorem is not as polymorphic as +it could be.} + +\item +\emph{All type variables occurring in the arguments of a friendly function must occur +as direct arguments of the type constructor of the resulting type.} + \end{enumerate} \ diff -r 2a4672722aaa -r 14571c9e1d50 src/Doc/manual.bib --- a/src/Doc/manual.bib Mon Oct 24 20:57:58 2016 +0200 +++ b/src/Doc/manual.bib Mon Oct 24 21:14:38 2016 +0200 @@ -372,13 +372,14 @@ publisher = {{ACM}}, } -@misc{blanchette-et-al-2016-fouco2, +@misc{blanchette-et-al-201x-amico, author = {Jasmin Christian Blanchette and + Aymeric Bouzy and Andreas Lochbihler and Andrei Popescu and Dmitriy Traytel}, - title = {Productivity for free: Friendly Corecursion for {Isabelle\slash HOL}}, - howpublished = "\url{http://www21.in.tum.de/~blanchet/fouco2.pdf}", + title = {Friends with benefits: Implementing corecursion in foundational proof assistants}, + howpublished = "\url{http://www21.in.tum.de/~blanchet/amico.pdf}", year = 2016} @inproceedings{blanchette-et-al-2014-impl, diff -r 2a4672722aaa -r 14571c9e1d50 src/HOL/Tools/BNF/bnf_gfp_grec.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Oct 24 20:57:58 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Oct 24 21:14:38 2016 +0200 @@ -3112,7 +3112,8 @@ val _ = (case filter_out (member (op =) As o TFree) k_As of [] => () | k_A :: _ => error ("Cannot have type variable " ^ quote (Syntax.string_of_typ lthy (TFree k_A)) ^ - " in the argument types when it does not occur in the result type")); + " in the argument types when it does not occur as an immediate argument of the result \ + \type constructor")); val substDT = Term.typ_subst_atomic (Ds ~~ res_Ds); diff -r 2a4672722aaa -r 14571c9e1d50 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Oct 24 20:57:58 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Oct 24 21:14:38 2016 +0200 @@ -2257,7 +2257,8 @@ |> (case raw_fun_T_opt of SOME raw_T => Proof_Context.add_const_constraint (fun_name, SOME (Syntax.read_typ lthy raw_T)) - | NONE => I); + | NONE => I) + handle TYPE (s, _, _) => error s; val fun_b = Binding.name (Long_Name.base_name fun_name); val code_goal = Syntax.read_prop fake_lthy raw_eq;