more 'corec' docs
Tue, 29 Mar 2016 19:11:03 +0200
changeset 62745 257a022f7e7b
parent 62744 b4f139bf02e3
child 62746 4384baae8753
more 'corec' docs
--- 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
 link to papers
@@ -61,6 +63,8 @@
     corec oneTwos :: "nat stream" where
       "oneTwos = SCons 1 (SCons 2 oneTwos)"
+thm oneTwos.cong_intros
 text \<open>
 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:
+\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]}
+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:
-  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 \<Rightarrow> (nat, 'b) tllist" where
+      "square_elems xs =
+       (case xs of
+         TNil z \<Rightarrow> TNil z
+       | TCons y ys \<Rightarrow> TCons (y ^^ 2) (square_elems ys))"
+    corec (friend) square_terminal :: "('a, int) tllist \<Rightarrow> ('a, int) tllist" where
+      "square_terminal xs =
+       (case xs of
+         TNil z \<Rightarrow> TNil (z ^^ 2)
+       | TCons y ys \<Rightarrow> TCons y (square_terminal ys))"
-thm stream.coinduct_upto(2)
-  sskew.coinduct
+text \<open>
+At this point, @{thm [source] tllist.coinduct_upto} contains three variants of the
+coinduction principles:
+\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}.
+The following variant is missing:
+\item @{typ "(nat, int) tllist"} up to @{const TNil}, @{const TCons},
+  @{const square_elems}, and @{const square_terminal}.
+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 \<open>
+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 \<open>Uniqueness Reasoning
 text \<open>
+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.