# HG changeset patch # User blanchet # Date 1459271463 -7200 # Node ID 257a022f7e7b074db4f2a09c80864790a67cdb5d # Parent b4f139bf02e38da5e51b735ea17fdf5be545c86e more 'corec' docs diff -r b4f139bf02e3 -r 257a022f7e7b src/Doc/Corec/Corec.thy --- a/src/Doc/Corec/Corec.thy Tue Mar 29 18:32:08 2016 +0200 +++ b/src/Doc/Corec/Corec.thy Tue Mar 29 19:11:03 2016 +0200 @@ -26,6 +26,8 @@ * friend * up to +* versioning + BNF link to papers @@ -61,6 +63,8 @@ corec oneTwos :: "nat stream" where "oneTwos = SCons 1 (SCons 2 oneTwos)" +thm oneTwos.cong_intros + text \ \noindent This is already beyond the syntactic fragment supported by \keyw{primcorec}. @@ -306,27 +310,121 @@ 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: + +\begin{indentblock} +\begin{description} + +\item[@{thm [source] sskew.cong_base}\rm:] ~ \\ +@{thm sskew.cong_base[no_vars]} + +\item[@{thm [source] sskew.cong_refl}\rm:] ~ \\ +@{thm sskew.cong_refl[no_vars]} + +\item[@{thm [source] sskew.cong_sym}\rm:] ~ \\ +@{thm sskew.cong_sym[no_vars]} + +\item[@{thm [source] sskew.cong_trans}\rm:] ~ \\ +@{thm sskew.cong_trans[no_vars]} + +\item[@{thm [source] sskew.cong_SCons}\rm:] ~ \\ +@{thm sskew.cong_SCons[no_vars]} + +\item[@{thm [source] sskew.cong_ssum}\rm:] ~ \\ +@{thm sskew.cong_ssum[no_vars]} + +\item[@{thm [source] sskew.cong_sprod}\rm:] ~ \\ +@{thm sskew.cong_sprod[no_vars]} + +\item[@{thm [source] sskew.cong_sskew}\rm:] ~ \\ +@{thm sskew.cong_sskew[no_vars]} + +\end{description} +\end{indentblock} +% +The introduction rules are also available as +@{thm [source] sskew.cong_intros}. + +Notice that there is no introduction rule corresponding to @{const sexp}, +because @{const sexp} has a more restrictive result type than @{const sskew} +(@{typ "nat stream"} vs. @{typ "('a :: {plus,times}) stream"}. + +Since the package maintains a set of incomparable corecursors, there is also a +set of associated coinduction principles and a set of sets of introduction +rules. A technically subtle point is to make Isabelle choose the right rules in +most situations. For this purpose, the package maintains the collection +@{thm [source] stream.coinduct_upto} of coinduction principles ordered by +increasing generality, which works well with Isabelle's philosophy of applying +the first rule that matches. For example, after registering @{const ssum} as a +friend, proving the equality @{term "l = r"} on @{typ "nat stream"} might +require coinduction principle for @{term "nat stream"}, which is up to +@{const ssum}. + +The collection @{thm [source] stream.coinduct_upto} is guaranteed to be complete +and up to date with respect to the type instances of definitions considered so +far, but occasionally it may be necessary to take the union of two incomparable +coinduction principles. This can be done using the @{command coinduction_upto} +command. Consider the following definitions: \ -(* FIXME: -thm - sskew.cong_base - sskew.cong_refl - sskew.cong_intros + codatatype (tset: 'a, 'b) tllist = + TNil (terminal : 'b) + | TCons (thd : 'a) (ttl : "('a, 'b) tllist") + for + map: tmap + rel: tllist_all2 + + corec (friend) square_elems :: "(nat, 'b) tllist \ (nat, 'b) tllist" where + "square_elems xs = + (case xs of + TNil z \ TNil z + | TCons y ys \ TCons (y ^^ 2) (square_elems ys))" + + corec (friend) square_terminal :: "('a, int) tllist \ ('a, int) tllist" where + "square_terminal xs = + (case xs of + TNil z \ TNil (z ^^ 2) + | TCons y ys \ TCons y (square_terminal ys))" -thm stream.coinduct_upto(2) - sskew.coinduct +text \ +At this point, @{thm [source] tllist.coinduct_upto} contains three variants of the +coinduction principles: +% +\begin{itemize} +\item @{typ "('a, int) tllist"} up to @{const TNil}, @{const TCons}, and + @{const square_terminal}; +\item @{typ "(nat, 'b) tllist"} up to @{const TNil}, @{const TCons}, and + @{const square_elems}; +\item @{typ "('a, 'b) tllist"} up to @{const TNil} and @{const TCons}. +\end{itemize} +% +The following variant is missing: +% +\begin{itemize} +\item @{typ "(nat, int) tllist"} up to @{const TNil}, @{const TCons}, + @{const square_elems}, and @{const square_terminal}. +\end{itemize} +% +To generate it, without having to define a new function with @{command corec}, +we can use the following command: +\ -thm stream.cong_intros -thm sfsup.cong_intros -*) + coinduction_upto nat_int_tllist: "(nat, int) tllist" + +text \ +This produces the theorems @{thm [source] nat_int_tllist.coinduct_upto} and +@{thm [source] nat_int_tllist.cong_intros} (as well as the individually named +introduction rules), and extends @{thm [source] tllist.coinduct_upto}. +\ subsection \Uniqueness Reasoning \label{ssec:uniqueness-reasoning}\ text \ -... +t is sometimes possible to achieve better automation by using a more specialized +proof method than coinduction. Uniqueness principles maintain a good balance +between expressiveness and automation. They exploit the property that a +corecursive specification is the unique solution to a fixpoint equation. \