Quelle  Corec.thy

(*  Title:      Doc/Corec/Corec.thy
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
    Author:     Aymeric Bouzy, Ecole polytechnique
    Author:     Andreas Lochbihler, ETH Zuerich
    Author:     Andrei Popescu, Middlesex University
    Author:     Dmitriy Traytel, ETH Zuerich

Tutorial for nonprimitively corecursive definitions.
*)

theory Corec
imports Main Datatypes.Setup "HOL-Library.BNF_Corec"
  "HOL-Library.FSet"
begin

section ‹Introduction
 \label{sec:introduction}›

text ‹
 's (co)datatype package cite‹"isabelle-datatypes"› offers a convenient
  for introducing codatatypes. For example, the type of (infinite) streams
  be defined as follows (cf. 🍋‹~~/src/HOL/Library/Stream.thy›):
 ›

    codatatype 'a stream =
      SCons (shd: 'a) (stl: "'a stream")

text ‹
 noindent
  (co)datatype package also provides two commands, \keyw{primcorec} and
 keyw{prim\-corec\-ur\-sive}, for defining primitively corecursive functions.

  tutorial presents a definitional package for functions beyond
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 {command corecursive}, @{command friend_of_corec}, and @{command coinduction_upto}.
  also covers the @{method corec_unique} proof method.
  package is not part of 🍋‹Main›; it is located in
 🍋‹~~/src/HOL/Library/BNF_Corec.thy›.

  @{command corec} command generalizes \keyw{primcorec} in three main
 . First, it allows multiple constructors around corecursive calls, where
 keyw{primcorec} expects exactly one. For example:
 ›

    corec oneTwos :: "nat stream" where
      "oneTwos = SCons 1 (SCons 2 oneTwos)"

text ‹
 , @{command corec} allows other functions than constructors to appear in
  corecursive call context (i.e., around any self-calls on the right-hand side
  the equation). The requirement on these functions is that they must be
 emph{friendly}. Intuitively, a function is friendly if it needs to destruct
  most one constructor of input to produce one constructor of output.
  can register functions as friendly using the @{command friend_of_corec}
 , or by passing the ‹friend› option to @{command corec}. The
  check relies on an internal syntactic check in combination with
  parametricity subgoal, which must be discharged manually (typically using
 {method transfer_prover} or @{method transfer_prover_eq}).

 , @{command corec} allows self-calls that are not guarded by a constructor,
  long as these calls occur in a friendly context (a context consisting
  of friendly functions) and can be shown to be terminating
 well founded). The mixture of recursive and corecursive calls in a single
  can be quite useful in practice.

 , the package synthesizes corecursors that take into account the
  call contexts. The corecursor is accompanined by a corresponding,
  general coinduction principle. The corecursor and the coinduction
  grow in expressiveness as we interact with it. In process algebra
 , corecursion and coinduction take place \emph{up to} friendly
 .

  package fully adheres to the LCF philosophy cite‹mgordon79›: The
  theorems associated with the specified corecursive functions are
  rather than introduced axiomatically.
 Exceptionally, most of the internal proof obligations are omitted if the
 ‹quick_and_dirty› option is enabled.)
  package is described in a pair of scientific papers
 cite‹"blanchette-et-al-2015-fouco" and "blanchette-et-al-201x-amico"›. Some
  the text and examples below originate from there.

  tutorial is organized as follows:

 begin{itemize}
 setlength{\itemsep}{0pt}

 item Section \ref{sec:introductory-examples}, ``Introductory Examples,''
  how to specify corecursive functions and to reason about them.

 item Section \ref{sec:command-syntax}, ``Command Syntax,'' describes the syntax
  the commands offered by the package.

 item Section \ref{sec:generated-theorems}, ``Generated Theorems,'' lists the
  produced by the package's commands.

 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
  tactics underlying the @{command friend_of_corec} and @{command corec}
 ‹(friend)› commands.

 item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
 ,'' concludes with known open issues.
 end{itemize}

  it is more powerful than \keyw{primcorec} in many respects,
 {command corec} suffers from a number of limitations. Most notably, it does
  support mutually corecursive codatatypes, and it is less efficient than
 keyw{primcorec} because it needs to dynamically synthesize corecursors and
  coinduction principles to accommodate the friends.

 newbox\boxA
 setbox\boxA=\hbox{\texttt{NOSPAM}}

 newcommand\authoremaili{\texttt{jasmin.blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
 .\allowbreak com}}

  and bug reports concerning either the package or this tutorial should
  directed to the first author at \authoremaili{} or to the
 texttt{cl-isabelle-users} mailing list.
 ›


section ‹Introductory Examples
 \label{sec:introductory-examples}›

text ‹
  package is illustrated through concrete examples featuring different flavors
  corecursion. More examples can be found in the directory
 🍋‹~~/src/HOL/Corec_Examples›.
 ›


subsection ‹Simple Corecursion
 \label{ssec:simple-corecursion}›

text ‹
  case studies by Rutten~cite‹rutten05› and Hinze~cite‹hinze10› on stream
  serve as our starting point. The following definition of pointwise sum
  be performed with either \keyw{primcorec} or @{command corec}:
 ›

    primcorec ssum :: "('a :: plus) stream ==> 'a stream ==> 'a stream" where
      "ssum xs ys = SCons (shd xs + shd ys) (ssum (stl xs) (stl ys))"

text ‹
 noindent
  sum meets the friendliness criterion. We register it as a friend using
  @{command friend_of_corec} command. The command requires us to give a
  of const‹ssum› where a constructor (const‹SCons›) occurs at
  outermost position on the right-hand side. Here, we can simply reuse the
 keyw{primcorec} specification above:
 ›

    friend_of_corec ssum :: "('a :: plus) stream ==> 'a stream ==> 'a stream" where
      "ssum xs ys = SCons (shd xs + shd ys) (ssum (stl xs) (stl ys))"
       apply (rule ssum.code)
      by transfer_prover

text ‹
 noindent
  command emits two subgoals. The first subgoal corresponds to the equation we
  and is trivial to discharge. The second subgoal is a parametricity
  that captures the the requirement that the function may destruct at
  one constructor of input to produce one constructor of output. This subgoal
  usually be discharged using the ‹transfer_prover› or
 {method transfer_prover_eq} proof method (Section~\ref{ssec:transfer-prover-eq}).
  latter replaces equality relations by their relator terms according to the
 {thm [source] relator_eq} theorem collection before it invokes
 {method transfer_prover}.

  registering const‹ssum› as a friend, we can use it in the corecursive
  context, either inside or outside the constructor guard:
 ›

    corec fibA :: "nat stream" where
      "fibA = SCons 0 (ssum (SCons 1 fibA) fibA)"

text ‹\blankline›

    corec fibB :: "nat stream" where
      "fibB = ssum (SCons 0 (SCons 1 fibB)) (SCons 0 fibB)"

text ‹
  the ‹friend› option, we can simultaneously define a function and
  it as a friend:
 ›

    corec (friend)
      sprod :: "('a :: {plus,times}) stream ==> 'a stream ==> 'a stream"
    where
      "sprod xs ys =
       SCons (shd xs * shd ys) (ssum (sprod xs (stl ys)) (sprod (stl xs) ys))"

text ‹\blankline›

    corec (friend) sexp :: "nat stream ==> nat stream" where
      "sexp xs = SCons (2 ^^ shd xs) (sprod (stl xs) (sexp xs))"

text ‹
 noindent
  parametricity subgoal is given to ‹transfer_prover_eq›
 Section~\ref{ssec:transfer-prover-eq}).

  const‹sprod› and const‹sexp› functions provide shuffle product and
  on streams. We can use them to define the stream of factorial
  in two different ways:
 ›

    corec factA :: "nat stream" where
      "factA = (let zs = SCons 1 factA in sprod zs zs)"

text ‹\blankline›

    corec factB :: "nat stream" where
      "factB = sexp (SCons 0 factB)"

text ‹
  arguments of friendly functions can be of complex types involving the
  codatatype. The following example defines the supremum of a finite set of
  by primitive corecursion and registers it as friendly:
 ›

    corec (friend) sfsup :: "nat stream fset ==> nat stream" where
      "sfsup X = SCons (Sup (fset (fimage shd X))) (sfsup (fimage stl X))"

text ‹
 noindent
  general, the arguments may be any bounded natural functor (BNF)
 cite‹"isabelle-datatypes"›, with the restriction that the target codatatype
 🍋‹nat stream›) may occur only in a \emph{live} position of the BNF. For
  reason, the following function, on unbounded sets, cannot be registered as
  friend:
 ›

    primcorec ssup :: "nat stream set ==> nat stream" where
      "ssup X = SCons (Sup (image shd X)) (ssup (image stl X))"


subsection ‹Nested Corecursion
 \label{ssec:nested-corecursion}›

text ‹
  package generally supports arbitrary codatatypes with multiple constructors
  nesting through other type constructors (BNFs). Consider the following type
  finitely branching Rose trees of potentially infinite depth:
 ›

    codatatype 'a tree =
      Node (lab: 'a) (sub: "'a tree list")

text ‹
  first define the pointwise sum of two trees analogously to const‹ssum›:
 ›

    corec (friend) tsum :: "('a :: plus) tree ==> 'a tree ==> 'a tree" where
      "tsum t u =
       Node (lab t + lab u) (map (λ(t', u'). tsum t' u') (zip (sub t) (sub u)))"

text ‹
 noindent
 , const‹map› is the standard map function on lists, and const‹zip›
  two parallel lists into a list of pairs. The const‹tsum› function is
  corecursive. Instead of @{command corec} ‹(friend)›, we could
  have used \keyw{primcorec} and @{command friend_of_corec}, as we did for
 const‹ssum›.

  const‹tsum› is registered as friendly, we can use it in the corecursive
  context of another function:
 ›

    corec (friend) ttimes :: "('a :: {plus,times}) tree ==> 'a tree ==> 'a tree" where
      "ttimes t u = Node (lab t * lab u)
         (map (λ(t', u'). tsum (ttimes t u') (ttimes t' u)) (zip (sub t) (sub u)))"

text ‹
  the syntactic convenience provided by \keyw{primcorec} is also supported by
 {command corec}, @{command corecursive}, and @{command friend_of_corec}. In
 , nesting through the function type can be expressed using
 ‹λ›-abstractions and function applications rather than through composition
 term‹(∘)›, the map function for ‹==>›). For example:
 ›

    codatatype 'a language =
      Lang (o: bool) (d: "'a ==> 'a language")

text ‹\blankline›

    corec (friend) Plus :: "'a language ==> 'a language ==> 'a language" where
      "Plus r s = Lang (o r ∨ o s) (λa. Plus (d r a) (d s a))"

text ‹\blankline›

    corec (friend) Times :: "'a language ==> 'a language ==> 'a language" where
      "Times r s = Lang (o r ∧ o s)
         (λa. if o r then Plus (Times (d r a) s) (d s a) else Times (d r a) s)"

text ‹\blankline›

    corec (friend) Star :: "'a language ==> 'a language" where
      "Star r = Lang True (λa. Times (d r a) (Star r))"

text ‹\blankline›

    corec (friend) Inter :: "'a language ==> 'a language ==> 'a language" where
      "Inter r s = Lang (o r ∧ o s) (λa. Inter (d r a) (d s a))"

text ‹\blankline›

    corec (friend) PLUS :: "'a language list ==> 'a language" where
      "PLUS xs = Lang (∃x ∈ set xs. o x) (λa. PLUS (map (λr. d r a) xs))"


subsection ‹Mixed Recursion--Corecursion
 \label{ssec:mixed-recursion-corecursion}›

text ‹
  is often convenient to let a corecursive function perform some finite
  before producing a constructor. With mixed recursion--corecursion, a
  number of unguarded recursive calls perform this calculation before
  a guarded corecursive call. Intuitively, the unguarded recursive call
  be unfolded to arbitrary finite depth, ultimately yielding a purely
  definition. An example is the term‹primes› function from Di
  and Miculan cite‹"di-gianantonio-miculan-2003"›:
 ›

    corecursive primes :: "nat ==> nat ==> nat stream" where
      "primes m n =
       (if (m = 0 ∧ n > 1) ∨ coprime m n then
          SCons n (primes (m * n) (n + 1))
        else
          primes m (n + 1))"
      apply (relation "measure (λ(m, n).
        if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
       apply (auto simp: mod_Suc diff_less_mono2 intro: Suc_lessI elim!: not_coprimeE)
      apply (metis dvd_1_iff_1 dvd_eq_mod_eq_0 mod_0 mod_Suc mod_Suc_eq mod_mod_cancel)
      done

text ‹
 noindent
  @{command corecursive} command is a variant of @{command corec} that allows
  to specify a termination argument for any unguarded self-call.

  called with ‹m = 1› and ‹n = 2›, the const‹primes›
  computes the stream of prime numbers. The unguarded call in the
 ‹else› branch increments term‹n› until it is coprime to the first
  term‹m› (i.e., the greatest common divisor of term‹m› and
 term‹n› is ‹1›).

  any positive integers term‹m› and term‹n›, the numbers term‹m› and
 ‹m * n + 1› are coprime, yielding an upper bound on the number of times
 term‹n› is increased. Hence, the function will take the ‹else› branch at
  finitely often before taking the then branch and producing one constructor.
  is a slight complication when ‹m = 0 ∧ n > 1›: Without the first
  in the ‹if› condition, the function could stall. (This corner
  was overlooked in the original example
 cite‹"di-gianantonio-miculan-2003"›.)

  the following examples, termination is discharged automatically by
 {command corec} by invoking @{method lexicographic_order}:
 ›

    corec catalan :: "nat ==> nat stream" where
      "catalan n =
       (if n > 0 then ssum (catalan (n - 1)) (SCons 0 (catalan (n + 1)))
        else SCons 1 (catalan 1))"

text ‹\blankline›

    corec collatz :: "nat ==> nat stream" where
      "collatz n = (if even n ∧ n > 0 then collatz (n div 2)
         else SCons n (collatz (3 * n + 1)))"

text ‹
  more elaborate case study, revolving around the filter function on lazy lists,
  presented in 🍋‹~~/src/HOL/Corec_Examples/LFilter.thy›.
 ›


subsection ‹Self-Friendship
 \label{ssec:self-friendship}›

text ‹
  package allows us to simultaneously define a function and use it as its own
 , as in the following definition of a ``skewed product'':
 ›

    corec (friend)
      sskew :: "('a :: {plus,times}) stream ==> 'a stream ==> 'a stream"
    where
      "sskew xs ys =
       SCons (shd xs * shd ys) (sskew (sskew xs (stl ys)) (sskew (stl xs) ys))"

text ‹
 noindent
  definitions, with nested self-calls on the right-hand side, cannot be
  into a @{command corec} part and a @{command friend_of_corec} part.
 ›


subsection ‹Coinduction
 \label{ssec:coinduction}›

text ‹
  a corecursive specification has been accepted, we normally want to reason
  it. The ‹codatatype› command generates a structural coinduction
  that matches primitively corecursive functions. For nonprimitive
 , our package provides the more advanced proof principle of
 emph{coinduction up to congruence}---or simply \emph{coinduction up-to}.

  structural coinduction principle for 🍋‹'a stream›, called
 {thm [source] stream.coinduct}, is as follows:
 
 begin{indentblock}
 {thm stream.coinduct[no_vars]}
 end{indentblock}
 
  allows us to prove an equality ‹l = r› on streams by
  a relation ‹R› that relates ‹l› and ‹r› (first
 ) and that constitutes a bisimulation (second premise). Streams that are
  by a bisimulation cannot be distinguished by taking observations (via
  selectors const‹shd› and const‹stl›); hence they must be equal.

  coinduction up-to principle after registering const‹sskew› as friendly is
  as @{thm [source] sskew.coinduct} and as one of the components of
  theorem collection @{thm [source] stream.coinduct_upto}:
 
 begin{indentblock}
 {thm sskew.coinduct[no_vars]}
 end{indentblock}
 
  rule is almost identical to structural coinduction, except that the
  application of term‹R› is generalized to
 term‹stream.v5.congclp R›.

  const‹stream.v5.congclp› predicate is equipped with the following
  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}
 
  introduction rules are also available as
 {thm [source] sskew.cong_intros}.

  that there is no introduction rule corresponding to const‹sexp›,
  const‹sexp› has a more restrictive result type than const‹sskew›
 🍋‹nat stream› vs. 🍋‹('a :: {plus,times}) stream›.

  version numbers, here ‹v5›, distinguish the different congruence
  generated for a given codatatype as more friends are registered. As
  as possible, it is recommended to avoid referring to them in proof
 .

  the package maintains a set of incomparable corecursors, there is also a
  of associated coinduction principles and a set of sets of introduction
 . A technically subtle point is to make Isabelle choose the right rules in
  situations. For this purpose, the package maintains the collection
 {thm [source] stream.coinduct_upto} of coinduction principles ordered by
  generality, which works well with Isabelle's philosophy of applying
  first rule that matches. For example, after registering const‹ssum› as a
 , proving the equality term‹l = r› on 🍋‹nat stream› might
  coinduction principle for term‹nat stream›, which is up to
 const‹ssum›.

  collection @{thm [source] stream.coinduct_upto} is guaranteed to be complete
  up to date with respect to the type instances of definitions considered so
 , but occasionally it may be necessary to take the union of two incomparable
  principles. This can be done using the @{command coinduction_upto}
 . Consider the following definitions:
 ›

    codatatype ('a, 'b) tllist =
      TNil (terminal: 'b)
    | TCons (thd: 'a) (ttl: "('a, 'b) tllist")

text ‹\blankline›

    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))"

text ‹\blankline›

    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))"

text ‹
  this point, @{thm [source] tllist.coinduct_upto} contains three variants of the
  principles:
 
 begin{itemize}
 item 🍋‹('a, int) tllist› up to const‹TNil›, const‹TCons›, and
 const‹square_terminal›;
 item 🍋‹(nat, 'b) tllist› up to const‹TNil›, const‹TCons›, and
 const‹square_elems›;
 item 🍋‹('a, 'b) tllist› up to const‹TNil› and const‹TCons›.
 end{itemize}
 
  following variant is missing:
 
 begin{itemize}
 item 🍋‹(nat, int) tllist› up to const‹TNil›, const‹TCons›,
 const‹square_elems›, and const‹square_terminal›.
 end{itemize}
 
  generate it without having to define a new function with @{command corec},
  can use the following command:
 ›

    coinduction_upto nat_int_tllist: "(nat, int) tllist"

text ‹
 noindent
  produces the theorems
 
 begin{indentblock}
 {thm [source] nat_int_tllist.coinduct_upto} \\
 {thm [source] nat_int_tllist.cong_intros}
 end{indentblock}
 
 as well as the individually named introduction rules) and extends
  dynamic collections @{thm [source] tllist.coinduct_upto} and
 {thm [source] tllist.cong_intros}.
 ›


subsection ‹Uniqueness Reasoning
 \label{ssec:uniqueness-reasoning}›

text ‹
  is sometimes possible to achieve better automation by using a more
  proof method than coinduction. Uniqueness principles maintain a good
  between expressiveness and automation. They exploit the property that a
  definition is the unique solution to a fixpoint equation.

  @{command corec}, @{command corecursive}, and @{command friend_of_corec}
  generate a property ‹f.unique› about the function of interest
 term‹f› that can be used to prove that any function that satisfies
 term‹f›'s corecursive specification must be equal to~term‹f›. For example:
 [@{thm ssum.unique[no_vars]}\]

  uniqueness principles are not restricted to functions defined using
 {command corec} or @{command corecursive} or registered with
 {command friend_of_corec}. Suppose term‹t x› is an arbitrary term
  on term‹x›. The @{method corec_unique} proof method, provided by our
 , transforms subgoals of the form
 [term‹(∀x. f x = H x f) ==> f x = t x›\]
 
 [term‹∀x. t x = H x t›\]
  higher-order functional term‹H› must be such that term‹f x = H x f›
  be a valid @{command corec} specification, but without nested self-calls
  unguarded (recursive) calls. Thus, @{method corec_unique} proves uniqueness
  term‹t› with respect to the given corecursive equation regardless of how
 term‹t› was defined. For example:
 ›

    lemma
      fixes f :: "nat stream ==> nat stream ==> nat stream"
      assumes "∀xs ys. f xs ys =
        SCons (shd ys * shd xs) (ssum (f xs (stl ys)) (f (stl xs) ys))"
      shows "f = sprod"
        using assms
      proof corec_unique
        show "sprod = (λxs ys :: nat stream.
            SCons (shd ys * shd xs) (ssum (sprod xs (stl ys)) (sprod (stl xs) ys)))"
          apply (rule ext)+
          apply (subst sprod.code)
          by simp
      qed

text ‹
  proof method relies on some theorems generated by the package. If no function
  a given codatatype has been defined using @{command corec} or
 {command corecursive} or registered as friendly using @{command friend_of_corec},
  theorems will not be available yet. In such cases, the theorems can be
  generated using the command
 ›

    coinduction_upto stream: "'a stream"


section ‹Command Syntax
 \label{sec:command-syntax}›

subsection ‹\keyw{corec} and \keyw{corecursive}
 \label{ssec:corec-and-corecursive-syntax}›

text ‹
 begin{matharray}{rcl}
 @{command_def "corec"} & : & ‹local_theory → local_theory› \\
 @{command_def "corecursive"} & : & ‹local_theory → proof(prove)›
 end{matharray}

 🪙‹
 (@@{command corec} | @@{command corecursive}) target? 🍋
 @{syntax cr_options}? fix @'where' prop
 ;
 @{syntax_def cr_options}: '(' ((@{syntax plugins} | 'friend' | 'transfer') + ',') ')'
 ›

 medskip

 noindent
  @{command corec} and @{command corecursive} commands introduce a corecursive
  over a codatatype.

  syntactic entity \synt{target} can be used to specify a local context,
 synt{fix} denotes name with an optional type signature, and \synt{prop} denotes
  HOL proposition cite‹"isabelle-isar-ref"›.

  optional target is optionally followed by a combination of the following
 :

 begin{itemize}
 setlength{\itemsep}{0pt}

 item
  ‹plugins› option indicates which plugins should be enabled
 ‹only›) or disabled (‹del›). By default, all plugins are enabled.

 item
  ‹friend› option indicates that the defined function should be
  as a friend. This gives rise to additional proof obligations.

 item
  ‹transfer› option indicates that an unconditional transfer rule
  be generated and proved ‹by transfer_prover›. The
 ‹[transfer_rule]› attribute is set on the generated theorem.
 end{itemize}

  @{command corec} command is an abbreviation for @{command corecursive}
  appropriate applications of @{method transfer_prover_eq}
 Section~\ref{ssec:transfer-prover-eq}) and @{method lexicographic_order} to
  any emerging proof obligations.
 ›


subsection ‹\keyw{friend_of_corec}
 \label{ssec:friend-of-corec-syntax}›

text ‹
 begin{matharray}{rcl}
 @{command_def "friend_of_corec"} & : & ‹local_theory → proof(prove)›
 end{matharray}

 🪙‹
 @@{command friend_of_corec} target? 🍋
 @{syntax foc_options}? fix @'where' prop
 ;
 @{syntax_def foc_options}: '(' ((@{syntax plugins} | 'transfer') + ',') ')'
 ›

 medskip

 noindent
  @{command friend_of_corec} command registers a corecursive function as
 .

  syntactic entity \synt{target} can be used to specify a local context,
 synt{fix} denotes name with an optional type signature, and \synt{prop} denotes
  HOL proposition cite‹"isabelle-isar-ref"›.

  optional target is optionally followed by a combination of the following
 :

 begin{itemize}
 setlength{\itemsep}{0pt}

 item
  ‹plugins› option indicates which plugins should be enabled
 ‹only›) or disabled (‹del›). By default, all plugins are enabled.

 item
  ‹transfer› option indicates that an unconditional transfer rule
  be generated and proved ‹by transfer_prover›. The
 ‹[transfer_rule]› attribute is set on the generated theorem.
 end{itemize}
 ›


subsection ‹\keyw{coinduction_upto}
 \label{ssec:coinduction-upto-syntax}›

text ‹
 begin{matharray}{rcl}
 @{command_def "coinduction_upto"} & : & ‹local_theory → local_theory›
 end{matharray}

 🪙‹
 @@{command coinduction_upto} target? name ':' type
 ›

 medskip

 noindent
  @{command coinduction_upto} generates a coinduction up-to rule for a given
  of a (possibly polymorphic) codatatype and notes the result with the
  prefix.

  syntactic entity \synt{name} denotes an identifier and \synt{type} denotes a
  cite‹"isabelle-isar-ref"›.
 ›


section ‹Generated Theorems
 \label{sec:generated-theorems}›

text ‹
  full list of named theorems generated by the package can be obtained by
  the command \keyw{print_theorems} immediately after the datatype definition.
  list excludes low-level theorems that reveal internal constructions. To
  these accessible, add the line
 ›

    declare [[bnf_internals]]
(*<*)
    declare [[bnf_internals = false]]
(*>*)

text ‹
  addition to the theorem listed below for each command provided by the
 , all commands update the dynamic theorem collections

 begin{indentblock}
 begin{description}

 item[‹t.›\hthm{coinduct_upto}]

 item[‹t.›\hthm{cong_intros}]

 end{description}
 end{indentblock}
 
  the corresponding codatatype ‹t› so that they always contain the most
  coinduction up-to principles derived so far.
 ›


subsection ‹\keyw{corec} and \keyw{corecursive}
 \label{ssec:corec-and-corecursive-theorems}›

text ‹
  a function term‹f› over codatatype ‹t›, the @{command corec} and
 {command corecursive} commands generate the following properties (listed for
 const‹sexp›, cf. Section~\ref{ssec:simple-corecursion}):

 begin{indentblock}
 begin{description}

 item[‹f.›\hthm{code} ‹[code]›\rm:] ~ \\
 {thm sexp.code[no_vars]} \\
  ‹[code]› attribute is set by the ‹code› plugin
 cite‹"isabelle-datatypes"›.

 item[‹f.›\hthm{coinduct} ‹[consumes 1, case_names t, case_conclusion D₁ …
 D_n]›\rm:] ~ \\
 {thm sexp.coinduct[no_vars]}

 item[‹f.›\hthm{cong_intros}\rm:] ~ \\
 {thm sexp.cong_intros[no_vars]}

 item[‹f.›\hthm{unique}\rm:] ~ \\
 {thm sexp.unique[no_vars]} \\
  property is not generated for mixed recursive--corecursive definitions.

 item[‹f.›\hthm{inner_induct}\rm:] ~ \\
  property is only generated for mixed recursive--corecursive definitions.
  const‹primes› (Section~\ref{ssec:mixed-recursion-corecursion}, it reads as
 : \\[\jot]
 {thm primes.inner_induct[no_vars]}

 end{description}
 end{indentblock}

 noindent
  individual rules making up ‹f.cong_intros› are available as

 begin{indentblock}
 begin{description}

 item[‹f.›\hthm{cong_base}]

 item[‹f.›\hthm{cong_refl}]

 item[‹f.›\hthm{cong_sym}]

 item[‹f.›\hthm{cong_trans}]

 item[‹f.›\hthm{cong_C}‹₁›, \ldots, ‹f.›\hthm{cong_C}‹_n›] ~ \\
  ‹C₁›, ‹…›, ‹C_n› are ‹t›'s
 

 item[‹f.›\hthm{cong_f}‹₁›, \ldots, ‹f.›\hthm{cong_f}‹_m›] ~ \\
  ‹f₁›, ‹…›, ‹f_m› are the available
  for ‹t›

 end{description}
 end{indentblock}
 ›


subsection ‹\keyw{friend_of_corec}
 \label{ssec:friend-of-corec-theorems}›

text ‹
  @{command friend_of_corec} command generates the same theorems as
 {command corec} and @{command corecursive}, except that it adds an optional
 ‹friend.› component to the names to prevent potential clashes (e.g.,
 ‹f.friend.code›).
 ›


subsection ‹\keyw{coinduction_upto}
 \label{ssec:coinduction-upto-theorems}›

text ‹
  @{command coinduction_upto} command generates the following properties
 listed for ‹nat_int_tllist›):

 begin{indentblock}
 begin{description}

 item[\begin{tabular}{@ {}l@ {}}
 ‹t.›\hthm{coinduct_upto} ‹[consumes 1, case_names t,› \\
 \phantom{‹t.›\hthm{coinduct_upto} ‹[›}‹case_conclusion D₁ …
 D_n]›\rm:
 end{tabular}] ~ \\
 {thm nat_int_tllist.coinduct_upto[no_vars]}

 item[‹t.›\hthm{cong_intros}\rm:] ~ \\
 {thm nat_int_tllist.cong_intros[no_vars]}

 end{description}
 end{indentblock}

 noindent
  individual rules making up ‹t.cong_intros› are available
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 Section~\ref{ssec:corec-and-corecursive-theorems}).
 ›


section ‹Proof Methods
 \label{sec:proof-methods}›

subsection ‹\textit{corec_unique}
 \label{ssec:corec-unique}›

text ‹
  @{method corec_unique} proof method can be used to prove the uniqueness of
  corecursive specification. See Section~\ref{ssec:uniqueness-reasoning} for
 .
 ›


subsection ‹\textit{transfer_prover_eq}
 \label{ssec:transfer-prover-eq}›

text ‹
  @{method transfer_prover_eq} proof method replaces the equality relation
 term‹(=)› with compound relator expressions according to
 {thm [source] relator_eq} before calling @{method transfer_prover} on the
  subgoal. It tends to work better than plain @{method transfer_prover} on
  parametricity proof obligations of @{command corecursive} and
 {command friend_of_corec}, because they often contain equality relations on
  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 ‹
  @{attribute friend_of_corec_simps} attribute declares naturality theorems
  be used by @{command friend_of_corec} and @{command corec} ‹(friend)› in
  the user specification from reduction to primitive corecursion.
 , these commands derive naturality theorems from the parametricity proof
  dischared by the user or the @{method transfer_prover_eq} method, but
  derivation fails if in the arguments of a higher-order constant a type variable
  on both sides of the function type constructor. The required naturality
  can then be declared with @{attribute friend_of_corec_simps}. See
 🍋‹~~/src/HOL/Corec_Examples/Tests/Iterate_GPV.thy› for an example.
 ›


section ‹Known Bugs and Limitations
 \label{sec:known-bugs-and-limitations}›

text ‹
  section lists the known bugs and limitations of the corecursion package at
  time of this writing.

 begin{enumerate}
 setlength{\itemsep}{0pt}

 item
 emph{Mutually corecursive codatatypes are not supported.}

 item
 emph{The signature of friend functions may not depend on type variables beyond
  that appear in the codatatype.}

 item
 emph{The internal tactics may fail on legal inputs.}
  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 ‹transfer› option is not implemented yet.}

 item
 emph{The constructor and destructor views offered by {\upshape\keyw{primcorec}}
  not supported by @{command corec} and @{command corecursive}.}

 item
 emph{There is no mechanism for registering custom plugins.}

 item
 emph{The package does not interact well with locales.}

 item
 emph{The undocumented ‹corecUU_transfer› theorem is not as polymorphic as
  could be.}

 item
 emph{All type variables occurring in the arguments of a friendly function must occur
  direct arguments of the type constructor of the resulting type.}

 end{enumerate}
 ›

end