--- 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,