summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Tue, 29 Mar 2016 17:42:43 +0200 | |

changeset 62742 | bfb5a70e4319 |

parent 62741 | 1ddfe28117e9 |

child 62743 | f9a65b48f5e2 |

more 'corec' documentation

--- a/src/Doc/Corec/Corec.thy Tue Mar 29 10:57:02 2016 +0200 +++ b/src/Doc/Corec/Corec.thy Tue Mar 29 17:42:43 2016 +0200 @@ -10,8 +10,10 @@ theory Corec imports + GCD "../Datatypes/Setup" "~~/src/HOL/Library/BNF_Corec" + "~~/src/HOL/Library/FSet" begin section \<open>Introduction @@ -20,72 +22,393 @@ text \<open> ... \cite{isabelle-datatypes} + +* friend +* up to + +BNF + +link to papers \<close> section \<open>Introductory Examples \label{sec:introductory-examples}\<close> +text \<open> +\<close> + subsection \<open>Simple Corecursion \label{ssec:simple-corecursion}\<close> +text \<open> +The case studies by Rutten~\cite{rutten05} and Hinze~\cite{hinze10} on stream +calculi serve as our starting point. Streams can be defined as follows +(cf. @{file "~~/src/HOL/Library/Stream.thy"}): +\<close> + + codatatype (sset: 'a) stream = + SCons (shd: 'a) (stl: "'a stream") + for + map: smap + +text \<open> +The @{command corec} command makes it possible to define functions where the +corecursive call occurs under two or more constructors: +\<close> + + corec oneTwos :: "nat stream" where + "oneTwos = SCons 1 (SCons 2 oneTwos)" + +text \<open> +\noindent +This is already beyond the syntactic fragment supported by \keyw{primcorec}. + +The following definition of pointwise sum can be performed with either +\keyw{primcorec} or @{command corec}: +\<close> + + primcorec ssum :: "('a :: plus) stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where + "ssum xs ys = SCons (shd xs + shd ys) (ssum (stl xs) (stl ys))" + +text \<open> +\noindent +Pointwise sum meets the friendliness criterion. We register it as a friend using +the @{command friend_of_corec} command. The command requires us to give a +specification of @{const ssum} where a constructor (@{const SCons}) occurs at +the outermost position on the right-hand side. Here, we can simply reuse the +\keyw{primcorec} specification above: +\<close> + + friend_of_corec ssum :: "('a :: plus) stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where + "ssum xs ys = SCons (shd xs + shd ys) (ssum (stl xs) (stl ys))" + apply (rule ssum.code) + by transfer_prover + +text \<open> +\noindent +The command emits two proof goals. The first one corresponds to the equation we +specified and is trivial to discharge. The second one is a parametricity goal +and can usually be discharged using the @{text transfer_prover} proof method. + +After registering @{const ssum} as a friend, we can use it in the corecursive +call context, either inside or outside the constructor guard: +\<close> + + corec fibA :: "nat stream" where + "fibA = SCons 0 (ssum (SCons 1 fibA) fibA)" + +text \<open>\blankline\<close> + + corec fibB :: "nat stream" where + "fibB = ssum (SCons 0 (SCons 1 fibB)) (SCons 0 fibB)" + +text \<open> +Using the @{text "friend"} option, we can simultaneously define a function and +register it as a friend: +\<close> + + corec (friend) + sprod :: "('a :: {plus,times}) stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" + where + "sprod xs ys = + SCons (shd xs * shd ys) (ssum (sprod xs (stl ys)) (sprod (stl xs) ys))" + +text \<open>\blankline\<close> + + corec (friend) sexp :: "nat stream \<Rightarrow> nat stream" where + "sexp xs = SCons (2 ^^ shd xs) (sprod (stl xs) (sexp xs))" + +text \<open> +\noindent +The parametricity proof goal is given to @{text transfer_prover}. + +The @{const sprod} and @{const sexp} functions provide shuffle product and +exponentiation on streams. We can use them to define the stream of factorial +numbers in two different ways: +\<close> + + corec factA :: "nat stream" where + "factA = (let zs = SCons 1 factA in sprod zs zs)" + + corec factB :: "nat stream" where + "factB = sexp (SCons 0 factB)" + +text \<open> +The arguments of friendly operations can be of complex types involving the +target codatatype. The following example defines the supremum of a finite set of +streams by primitive corecursion and registers it as friendly: +\<close> + + corec (friend) sfsup :: "nat stream fset \<Rightarrow> nat stream" where + "sfsup X = SCons (Sup (fset (fimage shd X))) (sfsup (fimage stl X))" + +text \<open> +\noindent +In general, the arguments may be any BNF, with the restriction that the target +codatatype (@{typ "nat stream"}) may occur only in a live position of the BNF. +For this reason, the following operation, on unbounded sets, cannot be +registered as a friend: +\<close> + + corec ssup :: "nat stream set \<Rightarrow> nat stream" where + "ssup X = SCons (Sup (image shd X)) (ssup (image stl X))" + subsection \<open>Nested Corecursion \label{ssec:nested-corecursion}\<close> +text \<open> +The package generally supports arbitrary codatatypes with multiple constructors +and nesting through other type constructors (BNFs). Consider the following type +of finitely branching Rose trees of potentially infinite depth: +\<close> -subsection \<open>Polymorphism - \label{ssec:polymorphism}\<close> + codatatype 'a tree = + Node (lab: 'a) (sub: "'a tree list") + +text \<open> +We first define the pointwise sum of two trees analogously to @{const ssum}: +\<close> + + corec (friend) tplus :: "('a :: plus) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where + "tplus t u = + Node (lab t + lab u) (map (\<lambda>(t', u'). tplus t' u') (zip (sub t) (sub u)))" + +text \<open> +\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 tplus} 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 +@{const ssum}. + +Once @{const tplus} is registered as friendly, we can use it in the corecursive +call context: +\<close> + + corec (friend) ttimes :: "('a :: {plus,times}) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where + "ttimes t u = Node (lab t * lab u) + (map (\<lambda>(t', u'). tplus (ttimes t u') (ttimes t' u)) (zip (sub t) (sub u)))" + + +subsection \<open>Mixed Recursion--Corecursion + \label{ssec:mixed-recursion-corecursion}\<close> + +text \<open> +It is often convenient to let a corecursive function perform some finite +computation before producing a constructor. With mixed recursion--corecursion, a +finite number of unguarded recursive calls perform this calculation before +reaching a guarded corecursive call. + +Intuitively, the unguarded recursive call can be unfolded to arbitrary finite +depth, ultimately yielding a purely corecursive definition. An example is the +@{term primes} function from Di Gianantonio and Miculan +\cite{di-gianantonio-miculan-2003}: +\<close> + + corecursive primes :: "nat \<Rightarrow> nat \<Rightarrow> nat stream" where + "primes m n = + (if (m = 0 \<and> n > 1) \<or> coprime m n then + SCons n (primes (m * n) (n + 1)) + else + primes m (n + 1))" + apply (relation "measure (\<lambda>(m, n). + if n = 0 then 1 else if coprime m n then 0 else m - n mod m)") + apply (auto simp: mod_Suc intro: Suc_lessI) + apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat) + by (metis diff_less_mono2 lessI mod_less_divisor) + +text \<open> +\noindent +The @{command corecursive} command is a variant of @{command corec} that allows +us to specify a termination argument for any unguarded self-call. + +When called with @{term "m = 1"} and @{term "n = 2"}, the @{const primes} +function computes the stream of prime numbers. The unguarded call in the +@{text else} branch increments @{term n} until it is coprime to the first +argument @{term m} (i.e., the greatest common divisor of @{term m} and +@{term n} is @{term 1}). + +For any positive integers @{term m} and @{term n}, the numbers @{term m} and +@{term "m * n + 1"} are coprime, yielding an upper bound on the number of times +@{term n} is increased. Hence, the function will take the @{text else} branch at +most finitely often before taking the then branch and producing one constructor. +There is a slight complication when @{term "m = 0 \<and> n > 1"}: Without the first +disjunct in the @{text "if"} condition, the function could stall. (This corner +case was overlooked in the original example \cite{di-gianantonio-miculan-2003}.) + +In the following example, which defines the stream of Catalan numbers, +termination is discharged automatically using @{text lexicographic_order}: +\<close> + + corec catalan :: "nat \<Rightarrow> nat stream" where + "catalan n = + (if n > 0 then ssum (catalan (n - 1)) (SCons 0 (catalan (n + 1))) + else SCons 1 (catalan 1))" + +text \<open> +A more elaborate case study, revolving around the filter function on lazy lists, +is presented in @{file "~~/src/HOL/Corec_Examples/LFilter.thy"}. +\<close> + + +subsection \<open>Self-Friendship + \label{ssec:self-friendship}\<close> + +text \<open> +Paradoxically, the package allows us to simultaneously define a function and use +it as its own friend, as in the following definition of a ``skewed product'': +\<close> + + corec (friend) + sskew :: "('a :: {plus,times}) stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" + where + "sskew xs ys = + SCons (shd xs * shd ys) (sskew (sskew xs (stl ys)) (sskew (stl xs) ys))" + +text \<open> +\noindent +Such definitions, with nested self-calls on the right-hand side, cannot be +separated into a @{command corec} part and a @{command friend_of_corec} part. +\<close> subsection \<open>Coinduction \label{ssec:coinduction}\<close> +text \<open> +Once a corecursive specification has been accepted, we normally want to reason +about it. The @{text codatatype} command generates a structural coinduction +principle that matches primitively corecursive functions. For nonprimitive +specifications, our package provides the more advanced proof principle of +\emph{coinduction up to congruence}---or simply \emph{coinduction up-to}. + +The structural coinduction principle for @{typ "'a stream"}, called +@{thm [source] stream.coinduct}, is as follows: +% +\[@{thm stream.coinduct[no_vars]}\] +% +Coinduction allows us to prove an equality @{text "l = r"} on streams by +providing a relation @{text R} that relates @{text l} and @{text r} (first +premise) and that constitutes a bisimulation (second premise). Streams that are +related by a bisimulation cannot be distinguished by taking observations (via +the selectors @{const shd} and @{const stl}); hence they must be equal. + +The coinduction up-to principle after registering @{const sskew} as friendly is +available as @{thm [source] sskew.coinduct} or +@{thm [source] stream.coinduct_upto(2)}: +% +\[@{thm sfsup.coinduct[no_vars]}\] +% +This rule is almost identical to structural coinduction, except that the +corecursive application of @{term R} is replaced by +@{term "stream.v5.congclp R"}. The @{const stream.v5.congclp} predicate is +equipped with the following introduction rules: +\<close> + +(* FIXME: +thm + sskew.cong_base + sskew.cong_refl + sskew.cong_intros + +thm stream.coinduct_upto(2) + sskew.coinduct + +thm stream.cong_intros +thm sfsup.cong_intros +*) + subsection \<open>Uniqueness Reasoning \label{ssec:uniqueness-reasoning}\<close> +text \<open> +... +\<close> + section \<open>Command Syntax \label{sec:command-syntax}\<close> +text \<open> +... +\<close> -subsection \<open>corec and corecursive + +subsection \<open>\keyw{corec} and \keyw{corecursive} \label{ssec:corec-and-corecursive}\<close> +text \<open> +... +\<close> + -subsection \<open>friend_of_corec +subsection \<open>\keyw{friend_of_corec} \label{ssec:friend-of-corec}\<close> +text \<open> +... +\<close> -subsection \<open>coinduction_upto + +subsection \<open>\keyw{coinduction_upto} \label{ssec:coinduction-upto}\<close> +text \<open> +... +\<close> + section \<open>Generated Theorems \label{sec:generated-theorems}\<close> +text \<open> +... +\<close> -subsection \<open>corec and corecursive + +subsection \<open>\keyw{corec} and \keyw{corecursive} \label{ssec:corec-and-corecursive}\<close> +text \<open> +... +\<close> + -subsection \<open>friend_of_corec +subsection \<open>\keyw{friend_of_corec} \label{ssec:friend-of-corec}\<close> +text \<open> +... +\<close> -subsection \<open>coinduction_upto + +subsection \<open>\keyw{coinduction_upto} \label{ssec:coinduction-upto}\<close> +text \<open> +... +\<close> + section \<open>Proof Method \label{sec:proof-method}\<close> +text \<open> +... +\<close> -subsection \<open>corec_unique + +subsection \<open>\textit{corec_unique} \label{ssec:corec-unique}\<close> +text \<open> +... +\<close> + section \<open>Known Bugs and Limitations \label{sec:known-bugs-and-limitations}\<close> @@ -104,6 +427,7 @@ * limitation on type of friend * unfinished tactics * polymorphism of corecUU_transfer + * alternative views \end{enumerate} \<close>

--- a/src/Doc/Corec/document/root.tex Tue Mar 29 10:57:02 2016 +0200 +++ b/src/Doc/Corec/document/root.tex Tue Mar 29 17:42:43 2016 +0200 @@ -75,8 +75,8 @@ \noindent This tutorial describes the definitional package for nonprimitively corecursive functions in Isabelle/HOL. The following commands are provided: -\keyw{corec}, \keyw{corecursive}, \keyw{friend\_of\_corec}, and \keyw{coinduction\_upto}. -They complement \keyw{codatatype}, \keyw{primcorec}, and \keyw{primcorecursive}, which +\keyw{corec}, \keyw{corecursive}, \keyw{friend\_of\_corec}, and \keyw{coinduction\_\allowbreak upto}. +They supplement \keyw{codatatype}, \keyw{primcorec}, and \keyw{primcorecursive}, which define codatatypes and primitively corecursive functions. \end{abstract} \end{sloppy}

--- a/src/Doc/manual.bib Tue Mar 29 10:57:02 2016 +0200 +++ b/src/Doc/manual.bib Tue Mar 29 17:42:43 2016 +0200 @@ -575,6 +575,20 @@ publisher = {Springer}, year = 1979} +@inproceedings{di-gianantonio-miculan-2003, + author = {Di Gianantonio, Pietro and + Marino Miculan}, + title = {A Unifying Approach to Recursive and Co-recursive Definitions}, + booktitle = {TYPES 2002}, + year = {2003}, + pages = {148--161}, + editor = {Herman Geuvers and + Freek Wiedijk}, + publisher = {Springer}, + series = {LNCS}, + volume = {2646} +} + @book{dummett, author = {Michael Dummett}, title = {Elements of Intuitionism}, @@ -834,6 +848,28 @@ pages = {265--270}, year = 1997} +@article{hinze10, + author = {Hinze, Ralf}, + title = {Concrete stream calculus---{A}n extended study}, + journal = {J. Funct. Program.}, + volume = {20}, + issue = {Special Issue 5-6}, + year = {2010}, + issn = {1469-7653}, + pages = {463--535} +} + +@inproceedings{sine, + author = "Kry\v{s}tof Hoder and Andrei Voronkov", + title = "Sine Qua Non for Large Theory Reasoning", + booktitle = {Automated Deduction --- CADE-23}, + publisher = Springer, + series = LNCS, + volume = 6803, + pages = "299--314", + editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans", + year = 2011} + @book{HopcroftUllman,author={John E. Hopcroft and Jeffrey D. Ullman}, title={Introduction to Automata Theory, Languages, and Computation.}, publisher={Addison-Wesley},year=1979} @@ -858,17 +894,6 @@ number = 5, month = May} -@inproceedings{sine, - author = "Kry\v{s}tof Hoder and Andrei Voronkov", - title = "Sine Qua Non for Large Theory Reasoning", - booktitle = {Automated Deduction --- CADE-23}, - publisher = Springer, - series = LNCS, - volume = 6803, - pages = "299--314", - editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans", - year = 2011} - @book{Hudak-Haskell,author={Paul Hudak}, title={The Haskell School of Expression},publisher=CUP,year=2000} @@ -1725,6 +1750,16 @@ publisher = {Bastad} } +@article{rutten05, + author = {Jan J. M. M. Rutten}, + title = {A coinductive calculus of streams}, + journal = {Math. Struct. Comp. Sci.}, + volume = 15, + number = 1, + year = 2005, + pages = {93--147}, +} + %S @inproceedings{saaltink-fme,