src/Doc/Corec/Corec.thy
author wenzelm
Sat, 22 Apr 2017 22:01:35 +0200
changeset 65552 f533820e7248
parent 64384 f8c1c12d6af5
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     1
(*  Title:      Doc/Corec/Corec.thy
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     3
    Author:     Aymeric Bouzy, Ecole polytechnique
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     4
    Author:     Andreas Lochbihler, ETH Zuerich
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     5
    Author:     Andrei Popescu, Middlesex University
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     6
    Author:     Dmitriy Traytel, ETH Zuerich
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     7
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     8
Tutorial for nonprimitively corecursive definitions.
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
     9
*)
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
    10
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
    11
theory Corec
65552
f533820e7248 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents: 64384
diff changeset
    12
imports Main "../Datatypes/Setup" "~~/src/HOL/Library/BNF_Corec"
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
    13
  "~~/src/HOL/Library/FSet"
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
    14
begin
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
    15
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
    16
section \<open>Introduction
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
    17
  \label{sec:introduction}\<close>
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
    18
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
    19
text \<open>
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    20
Isabelle's (co)datatype package @{cite "isabelle-datatypes"} offers a convenient
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    21
syntax for introducing codatatypes. For example, the type of (infinite) streams
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
    22
can be defined as follows (cf. \<^file>\<open>~~/src/HOL/Library/Stream.thy\<close>):
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    23
\<close>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    24
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    25
    codatatype 'a stream =
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    26
      SCons (shd: 'a) (stl: "'a stream")
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    27
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    28
text \<open>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    29
\noindent
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    30
The (co)datatype package also provides two commands, \keyw{primcorec} and
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    31
\keyw{prim\-corec\-ur\-sive}, for defining primitively corecursive functions.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    32
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    33
This tutorial presents a definitional package for functions beyond
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    34
primitive corecursion. It describes @{command corec} and related commands:\
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    35
@{command corecursive}, @{command friend_of_corec}, and @{command coinduction_upto}.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    36
It also covers the @{method corec_unique} proof method.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    37
The package is not part of @{theory Main}; it is located in
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
    38
\<^file>\<open>~~/src/HOL/Library/BNF_Corec.thy\<close>.
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
    39
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    40
The @{command corec} command generalizes \keyw{primcorec} in three main
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    41
respects. First, it allows multiple constructors around corecursive calls, where
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    42
\keyw{primcorec} expects exactly one. For example:
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    43
\<close>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    44
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    45
    corec oneTwos :: "nat stream" where
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    46
      "oneTwos = SCons 1 (SCons 2 oneTwos)"
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    47
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    48
text \<open>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    49
Second, @{command corec} allows other functions than constructors to appear in
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    50
the corecursive call context (i.e., around any self-calls on the right-hand side
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    51
of the equation). The requirement on these functions is that they must be
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    52
\emph{friendly}. Intuitively, a function is friendly if it needs to destruct
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    53
at most one constructor of input to produce one constructor of output.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    54
We can register functions as friendly using the @{command friend_of_corec}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    55
command, or by passing the @{text friend} option to @{command corec}. The
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    56
friendliness check relies on an internal syntactic check in combination with
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    57
a parametricity subgoal, which must be discharged manually (typically using
64380
4b22e1268779 document transfer_prover_eq and friend_of_corec_simps
Andreas Lochbihler
parents: 63680
diff changeset
    58
@{method transfer_prover} or @{method transfer_prover_eq}).
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    59
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    60
Third, @{command corec} allows self-calls that are not guarded by a constructor,
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    61
as long as these calls occur in a friendly context (a context consisting
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    62
exclusively of friendly functions) and can be shown to be terminating
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    63
(well founded). The mixture of recursive and corecursive calls in a single
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    64
function can be quite useful in practice.
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
    65
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    66
Internally, the package synthesizes corecursors that take into account the
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    67
possible call contexts. The corecursor is accompanined by a corresponding,
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    68
equally general coinduction principle. The corecursor and the coinduction
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    69
principle grow in expressiveness as we interact with it. In process algebra
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    70
terminology, corecursion and coinduction take place \emph{up to} friendly
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    71
contexts.
62745
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
    72
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    73
The package fully adheres to the LCF philosophy @{cite mgordon79}: The
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    74
characteristic theorems associated with the specified corecursive functions are
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
    75
derived rather than introduced axiomatically.
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
    76
(Exceptionally, most of the internal proof obligations are omitted if the
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
    77
@{text quick_and_dirty} option is enabled.)
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    78
The package is described in a pair of scientific papers
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
    79
@{cite "blanchette-et-al-2015-fouco" and "blanchette-et-al-201x-amico"}. Some
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    80
of the text and examples below originate from there.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    81
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    82
This tutorial is organized as follows:
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    83
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    84
\begin{itemize}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    85
\setlength{\itemsep}{0pt}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    86
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    87
\item Section \ref{sec:introductory-examples}, ``Introductory Examples,''
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    88
describes how to specify corecursive functions and to reason about them.
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
    89
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    90
\item Section \ref{sec:command-syntax}, ``Command Syntax,'' describes the syntax
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    91
of the commands offered by the package.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    92
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    93
\item Section \ref{sec:generated-theorems}, ``Generated Theorems,'' lists the
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    94
theorems produced by the package's commands.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
    95
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
    96
\item Section \ref{sec:proof-methods}, ``Proof Methods,'' briefly describes the
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
    97
@{method corec_unique} and @{method transfer_prover_eq} proof methods.
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
    98
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
    99
\item Section \ref{sec:attribute}, ``Attribute,'' briefly describes the
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   100
@{attribute friend_of_corec_simps} attribute, which can be used to strengthen
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   101
the tactics underlying the @{command friend_of_corec} and @{command corec}
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   102
@{text "(friend)"} commands.
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   103
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   104
\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   105
Limitations,'' concludes with known open issues.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   106
\end{itemize}
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   107
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   108
Although it is more powerful than \keyw{primcorec} in many respects,
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   109
@{command corec} suffers from a number of limitations. Most notably, it does
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   110
not support mutually corecursive codatatypes, and it is less efficient than
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   111
\keyw{primcorec} because it needs to dynamically synthesize corecursors and
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   112
corresponding coinduction principles to accommodate the friends.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   113
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   114
\newbox\boxA
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   115
\setbox\boxA=\hbox{\texttt{NOSPAM}}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   116
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   117
\newcommand\authoremaili{\texttt{jasmin.blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   118
gmail.\allowbreak com}}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   119
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   120
Comments and bug reports concerning either the package or this tutorial should
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   121
be directed to the first author at \authoremaili{} or to the
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   122
\texttt{cl-isabelle-users} mailing list.
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   123
\<close>
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   124
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   125
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   126
section \<open>Introductory Examples
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   127
  \label{sec:introductory-examples}\<close>
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   128
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   129
text \<open>
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   130
The package is illustrated through concrete examples featuring different flavors
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   131
of corecursion. More examples can be found in the directory
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   132
\<^dir>\<open>~~/src/HOL/Corec_Examples\<close>.
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   133
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   134
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   135
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   136
subsection \<open>Simple Corecursion
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   137
  \label{ssec:simple-corecursion}\<close>
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   138
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   139
text \<open>
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   140
The case studies by Rutten~@{cite rutten05} and Hinze~@{cite hinze10} on stream
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   141
calculi serve as our starting point. The following definition of pointwise sum
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   142
can be performed with either \keyw{primcorec} or @{command corec}:
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   143
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   144
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   145
    primcorec ssum :: "('a :: plus) stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   146
      "ssum xs ys = SCons (shd xs + shd ys) (ssum (stl xs) (stl ys))"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   147
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   148
text \<open>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   149
\noindent
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   150
Pointwise sum meets the friendliness criterion. We register it as a friend using
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   151
the @{command friend_of_corec} command. The command requires us to give a
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   152
specification of @{const ssum} where a constructor (@{const SCons}) occurs at
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   153
the outermost position on the right-hand side. Here, we can simply reuse the
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   154
\keyw{primcorec} specification above:
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   155
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   156
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   157
    friend_of_corec ssum :: "('a :: plus) stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   158
      "ssum xs ys = SCons (shd xs + shd ys) (ssum (stl xs) (stl ys))"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   159
       apply (rule ssum.code)
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   160
      by transfer_prover
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   161
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   162
text \<open>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   163
\noindent
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   164
The command emits two subgoals. The first subgoal corresponds to the equation we
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   165
specified and is trivial to discharge. The second subgoal is a parametricity
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   166
property that captures the the requirement that the function may destruct at
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   167
most one constructor of input to produce one constructor of output. This subgoal
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   168
can usually be discharged using the @{text transfer_prover} or
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   169
@{method transfer_prover_eq} proof method (Section~\ref{ssec:transfer-prover-eq}).
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   170
The latter replaces equality relations by their relator terms according to the
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   171
@{thm [source] relator_eq} theorem collection before it invokes
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   172
@{method transfer_prover}.
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   173
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   174
After registering @{const ssum} as a friend, we can use it in the corecursive
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   175
call context, either inside or outside the constructor guard:
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   176
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   177
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   178
    corec fibA :: "nat stream" where
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   179
      "fibA = SCons 0 (ssum (SCons 1 fibA) fibA)"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   180
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   181
text \<open>\blankline\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   182
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   183
    corec fibB :: "nat stream" where
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   184
      "fibB = ssum (SCons 0 (SCons 1 fibB)) (SCons 0 fibB)"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   185
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   186
text \<open>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   187
Using the @{text "friend"} option, we can simultaneously define a function and
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   188
register it as a friend:
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   189
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   190
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   191
    corec (friend)
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   192
      sprod :: "('a :: {plus,times}) stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   193
    where
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   194
      "sprod xs ys =
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   195
       SCons (shd xs * shd ys) (ssum (sprod xs (stl ys)) (sprod (stl xs) ys))"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   196
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   197
text \<open>\blankline\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   198
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   199
    corec (friend) sexp :: "nat stream \<Rightarrow> nat stream" where
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   200
      "sexp xs = SCons (2 ^^ shd xs) (sprod (stl xs) (sexp xs))"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   201
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   202
text \<open>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   203
\noindent
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   204
The parametricity subgoal is given to @{text transfer_prover_eq}
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   205
(Section~\ref{ssec:transfer-prover-eq}).
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   206
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   207
The @{const sprod} and @{const sexp} functions provide shuffle product and
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   208
exponentiation on streams. We can use them to define the stream of factorial
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   209
numbers in two different ways:
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   210
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   211
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   212
    corec factA :: "nat stream" where
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   213
      "factA = (let zs = SCons 1 factA in sprod zs zs)"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   214
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   215
text \<open>\blankline\<close>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   216
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   217
    corec factB :: "nat stream" where
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   218
      "factB = sexp (SCons 0 factB)"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   219
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   220
text \<open>
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   221
The arguments of friendly functions can be of complex types involving the
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   222
target codatatype. The following example defines the supremum of a finite set of
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   223
streams by primitive corecursion and registers it as friendly:
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   224
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   225
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   226
    corec (friend) sfsup :: "nat stream fset \<Rightarrow> nat stream" where
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   227
      "sfsup X = SCons (Sup (fset (fimage shd X))) (sfsup (fimage stl X))"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   228
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   229
text \<open>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   230
\noindent
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   231
In general, the arguments may be any bounded natural functor (BNF)
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   232
@{cite "isabelle-datatypes"}, with the restriction that the target codatatype
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   233
(@{typ "nat stream"}) may occur only in a \emph{live} position of the BNF. For
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   234
this reason, the following function, on unbounded sets, cannot be registered as
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   235
a friend:
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   236
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   237
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   238
    primcorec ssup :: "nat stream set \<Rightarrow> nat stream" where
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   239
      "ssup X = SCons (Sup (image shd X)) (ssup (image stl X))"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   240
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   241
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   242
subsection \<open>Nested Corecursion
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   243
  \label{ssec:nested-corecursion}\<close>
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   244
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   245
text \<open>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   246
The package generally supports arbitrary codatatypes with multiple constructors
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   247
and nesting through other type constructors (BNFs). Consider the following type
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   248
of finitely branching Rose trees of potentially infinite depth:
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   249
\<close>
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   250
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   251
    codatatype 'a tree =
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   252
      Node (lab: 'a) (sub: "'a tree list")
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   253
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   254
text \<open>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   255
We first define the pointwise sum of two trees analogously to @{const ssum}:
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   256
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   257
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   258
    corec (friend) tsum :: "('a :: plus) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   259
      "tsum t u =
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   260
       Node (lab t + lab u) (map (\<lambda>(t', u'). tsum t' u') (zip (sub t) (sub u)))"
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   261
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   262
text \<open>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   263
\noindent
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   264
Here, @{const map} is the standard map function on lists, and @{const zip}
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   265
converts two parallel lists into a list of pairs. The @{const tsum} function is
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   266
primitively corecursive. Instead of @{command corec} @{text "(friend)"}, we could
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   267
also have used \keyw{primcorec} and @{command friend_of_corec}, as we did for
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   268
@{const ssum}.
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   269
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   270
Once @{const tsum} is registered as friendly, we can use it in the corecursive
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   271
call context of another function:
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   272
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   273
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   274
    corec (friend) ttimes :: "('a :: {plus,times}) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   275
      "ttimes t u = Node (lab t * lab u)
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   276
         (map (\<lambda>(t', u'). tsum (ttimes t u') (ttimes t' u)) (zip (sub t) (sub u)))"
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   277
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   278
text \<open>
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   279
All the syntactic convenience provided by \keyw{primcorec} is also supported by
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   280
@{command corec}, @{command corecursive}, and @{command friend_of_corec}. In
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   281
particular, nesting through the function type can be expressed using
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   282
@{text \<lambda>}-abstractions and function applications rather than through composition
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   283
(@{term "op \<circ>"}, the map function for @{text \<Rightarrow>}). For example:
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   284
\<close>
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   285
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   286
    codatatype 'a language =
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   287
      Lang (\<oo>: bool) (\<dd>: "'a \<Rightarrow> 'a language")
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   288
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   289
text \<open>\blankline\<close>
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   290
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   291
    corec (friend) Plus :: "'a language \<Rightarrow> 'a language \<Rightarrow> 'a language" where
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   292
      "Plus r s = Lang (\<oo> r \<or> \<oo> s) (\<lambda>a. Plus (\<dd> r a) (\<dd> s a))"
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   293
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   294
text \<open>\blankline\<close>
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   295
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   296
    corec (friend) Times :: "'a language \<Rightarrow> 'a language \<Rightarrow> 'a language" where
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   297
      "Times r s = Lang (\<oo> r \<and> \<oo> s)
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   298
         (\<lambda>a. if \<oo> r then Plus (Times (\<dd> r a) s) (\<dd> s a) else Times (\<dd> r a) s)"
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   299
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   300
text \<open>\blankline\<close>
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   301
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   302
    corec (friend) Star :: "'a language \<Rightarrow> 'a language" where
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   303
      "Star r = Lang True (\<lambda>a. Times (\<dd> r a) (Star r))"
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   304
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   305
text \<open>\blankline\<close>
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   306
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   307
    corec (friend) Inter :: "'a language \<Rightarrow> 'a language \<Rightarrow> 'a language" where
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   308
      "Inter r s = Lang (\<oo> r \<and> \<oo> s) (\<lambda>a. Inter (\<dd> r a) (\<dd> s a))"
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   309
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   310
text \<open>\blankline\<close>
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   311
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   312
    corec (friend) PLUS :: "'a language list \<Rightarrow> 'a language" where
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   313
      "PLUS xs = Lang (\<exists>x \<in> set xs. \<oo> x) (\<lambda>a. PLUS (map (\<lambda>r. \<dd> r a) xs))"
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   314
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   315
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   316
subsection \<open>Mixed Recursion--Corecursion
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   317
  \label{ssec:mixed-recursion-corecursion}\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   318
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   319
text \<open>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   320
It is often convenient to let a corecursive function perform some finite
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   321
computation before producing a constructor. With mixed recursion--corecursion, a
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   322
finite number of unguarded recursive calls perform this calculation before
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   323
reaching a guarded corecursive call. Intuitively, the unguarded recursive call
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   324
can be unfolded to arbitrary finite depth, ultimately yielding a purely
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   325
corecursive definition. An example is the @{term primes} function from Di
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   326
Gianantonio and Miculan @{cite "di-gianantonio-miculan-2003"}:
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   327
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   328
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   329
    corecursive primes :: "nat \<Rightarrow> nat \<Rightarrow> nat stream" where
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   330
      "primes m n =
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   331
       (if (m = 0 \<and> n > 1) \<or> coprime m n then
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   332
          SCons n (primes (m * n) (n + 1))
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   333
        else
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   334
          primes m (n + 1))"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   335
      apply (relation "measure (\<lambda>(m, n).
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   336
        if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   337
       apply (auto simp: mod_Suc intro: Suc_lessI)
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   338
       apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   339
      by (metis diff_less_mono2 lessI mod_less_divisor)
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   340
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   341
text \<open>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   342
\noindent
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   343
The @{command corecursive} command is a variant of @{command corec} that allows
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   344
us to specify a termination argument for any unguarded self-call.
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   345
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   346
When called with @{text "m = 1"} and @{text "n = 2"}, the @{const primes}
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   347
function computes the stream of prime numbers. The unguarded call in the
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   348
@{text else} branch increments @{term n} until it is coprime to the first
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   349
argument @{term m} (i.e., the greatest common divisor of @{term m} and
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   350
@{term n} is @{text 1}).
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   351
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   352
For any positive integers @{term m} and @{term n}, the numbers @{term m} and
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   353
@{text "m * n + 1"} are coprime, yielding an upper bound on the number of times
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   354
@{term n} is increased. Hence, the function will take the @{text else} branch at
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   355
most finitely often before taking the then branch and producing one constructor.
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   356
There is a slight complication when @{text "m = 0 \<and> n > 1"}: Without the first
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   357
disjunct in the @{text "if"} condition, the function could stall. (This corner
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   358
case was overlooked in the original example
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   359
@{cite "di-gianantonio-miculan-2003"}.)
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   360
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   361
In the following examples, termination is discharged automatically by
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   362
@{command corec} by invoking @{method lexicographic_order}:
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   363
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   364
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   365
    corec catalan :: "nat \<Rightarrow> nat stream" where
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   366
      "catalan n =
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   367
       (if n > 0 then ssum (catalan (n - 1)) (SCons 0 (catalan (n + 1)))
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   368
        else SCons 1 (catalan 1))"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   369
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   370
text \<open>\blankline\<close>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   371
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   372
    corec collatz :: "nat \<Rightarrow> nat stream" where
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   373
      "collatz n = (if even n \<and> n > 0 then collatz (n div 2)
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   374
         else SCons n (collatz (3 * n + 1)))"
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   375
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   376
text \<open>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   377
A more elaborate case study, revolving around the filter function on lazy lists,
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   378
is presented in \<^file>\<open>~~/src/HOL/Corec_Examples/LFilter.thy\<close>.
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   379
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   380
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   381
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   382
subsection \<open>Self-Friendship
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   383
  \label{ssec:self-friendship}\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   384
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   385
text \<open>
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   386
The package allows us to simultaneously define a function and use it as its own
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   387
friend, as in the following definition of a ``skewed product'':
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   388
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   389
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   390
    corec (friend)
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   391
      sskew :: "('a :: {plus,times}) stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   392
    where
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   393
      "sskew xs ys =
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   394
       SCons (shd xs * shd ys) (sskew (sskew xs (stl ys)) (sskew (stl xs) ys))"
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   395
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   396
text \<open>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   397
\noindent
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   398
Such definitions, with nested self-calls on the right-hand side, cannot be
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   399
separated into a @{command corec} part and a @{command friend_of_corec} part.
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   400
\<close>
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   401
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   402
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   403
subsection \<open>Coinduction
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   404
  \label{ssec:coinduction}\<close>
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   405
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   406
text \<open>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   407
Once a corecursive specification has been accepted, we normally want to reason
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   408
about it. The @{text codatatype} command generates a structural coinduction
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   409
principle that matches primitively corecursive functions. For nonprimitive
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   410
specifications, our package provides the more advanced proof principle of
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   411
\emph{coinduction up to congruence}---or simply \emph{coinduction up-to}.
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   412
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   413
The structural coinduction principle for @{typ "'a stream"}, called
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   414
@{thm [source] stream.coinduct}, is as follows:
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   415
%
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   416
\begin{indentblock}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   417
@{thm stream.coinduct[no_vars]}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   418
\end{indentblock}
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   419
%
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   420
Coinduction allows us to prove an equality @{text "l = r"} on streams by
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   421
providing a relation @{text R} that relates @{text l} and @{text r} (first
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   422
premise) and that constitutes a bisimulation (second premise). Streams that are
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   423
related by a bisimulation cannot be distinguished by taking observations (via
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   424
the selectors @{const shd} and @{const stl}); hence they must be equal.
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   425
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   426
The coinduction up-to principle after registering @{const sskew} as friendly is
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   427
available as @{thm [source] sskew.coinduct} and as one of the components of
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   428
the theorem collection @{thm [source] stream.coinduct_upto}:
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   429
%
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   430
\begin{indentblock}
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   431
@{thm sskew.coinduct[no_vars]}
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   432
\end{indentblock}
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   433
%
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   434
This rule is almost identical to structural coinduction, except that the
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   435
corecursive application of @{term R} is generalized to
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   436
@{term "stream.v5.congclp R"}.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   437
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   438
The @{const stream.v5.congclp} predicate is equipped with the following
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   439
introduction rules:
62745
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   440
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   441
\begin{indentblock}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   442
\begin{description}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   443
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   444
\item[@{thm [source] sskew.cong_base}\rm:] ~ \\
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   445
@{thm sskew.cong_base[no_vars]}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   446
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   447
\item[@{thm [source] sskew.cong_refl}\rm:] ~ \\
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   448
@{thm sskew.cong_refl[no_vars]}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   449
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   450
\item[@{thm [source] sskew.cong_sym}\rm:] ~ \\
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   451
@{thm sskew.cong_sym[no_vars]}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   452
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   453
\item[@{thm [source] sskew.cong_trans}\rm:] ~ \\
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   454
@{thm sskew.cong_trans[no_vars]}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   455
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   456
\item[@{thm [source] sskew.cong_SCons}\rm:] ~ \\
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   457
@{thm sskew.cong_SCons[no_vars]}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   458
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   459
\item[@{thm [source] sskew.cong_ssum}\rm:] ~ \\
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   460
@{thm sskew.cong_ssum[no_vars]}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   461
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   462
\item[@{thm [source] sskew.cong_sprod}\rm:] ~ \\
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   463
@{thm sskew.cong_sprod[no_vars]}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   464
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   465
\item[@{thm [source] sskew.cong_sskew}\rm:] ~ \\
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   466
@{thm sskew.cong_sskew[no_vars]}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   467
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   468
\end{description}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   469
\end{indentblock}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   470
%
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   471
The introduction rules are also available as
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   472
@{thm [source] sskew.cong_intros}.
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   473
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   474
Notice that there is no introduction rule corresponding to @{const sexp},
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   475
because @{const sexp} has a more restrictive result type than @{const sskew}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   476
(@{typ "nat stream"} vs. @{typ "('a :: {plus,times}) stream"}.
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   477
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   478
The version numbers, here @{text v5}, distinguish the different congruence
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   479
closures generated for a given codatatype as more friends are registered. As
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   480
much as possible, it is recommended to avoid referring to them in proof
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   481
documents.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   482
62745
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   483
Since the package maintains a set of incomparable corecursors, there is also a
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   484
set of associated coinduction principles and a set of sets of introduction
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   485
rules. A technically subtle point is to make Isabelle choose the right rules in
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   486
most situations. For this purpose, the package maintains the collection
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   487
@{thm [source] stream.coinduct_upto} of coinduction principles ordered by
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   488
increasing generality, which works well with Isabelle's philosophy of applying
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   489
the first rule that matches. For example, after registering @{const ssum} as a
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   490
friend, proving the equality @{term "l = r"} on @{typ "nat stream"} might
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   491
require coinduction principle for @{term "nat stream"}, which is up to
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   492
@{const ssum}.
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   493
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   494
The collection @{thm [source] stream.coinduct_upto} is guaranteed to be complete
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   495
and up to date with respect to the type instances of definitions considered so
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   496
far, but occasionally it may be necessary to take the union of two incomparable
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   497
coinduction principles. This can be done using the @{command coinduction_upto}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   498
command. Consider the following definitions:
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   499
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   500
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   501
    codatatype ('a, 'b) tllist =
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   502
      TNil (terminal: 'b)
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   503
    | TCons (thd: 'a) (ttl: "('a, 'b) tllist")
62745
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   504
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   505
text \<open>\blankline\<close>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   506
62745
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   507
    corec (friend) square_elems :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   508
      "square_elems xs =
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   509
       (case xs of
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   510
         TNil z \<Rightarrow> TNil z
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   511
       | TCons y ys \<Rightarrow> TCons (y ^^ 2) (square_elems ys))"
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   512
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   513
text \<open>\blankline\<close>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   514
62745
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   515
    corec (friend) square_terminal :: "('a, int) tllist \<Rightarrow> ('a, int) tllist" where
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   516
      "square_terminal xs =
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   517
       (case xs of
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   518
         TNil z \<Rightarrow> TNil (z ^^ 2)
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   519
       | TCons y ys \<Rightarrow> TCons y (square_terminal ys))"
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   520
62745
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   521
text \<open>
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   522
At this point, @{thm [source] tllist.coinduct_upto} contains three variants of the
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   523
coinduction principles:
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   524
%
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   525
\begin{itemize}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   526
\item @{typ "('a, int) tllist"} up to @{const TNil}, @{const TCons}, and
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   527
  @{const square_terminal};
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   528
\item @{typ "(nat, 'b) tllist"} up to @{const TNil}, @{const TCons}, and
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   529
  @{const square_elems};
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   530
\item @{typ "('a, 'b) tllist"} up to @{const TNil} and @{const TCons}.
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   531
\end{itemize}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   532
%
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   533
The following variant is missing:
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   534
%
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   535
\begin{itemize}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   536
\item @{typ "(nat, int) tllist"} up to @{const TNil}, @{const TCons},
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   537
  @{const square_elems}, and @{const square_terminal}.
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   538
\end{itemize}
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   539
%
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   540
To generate it without having to define a new function with @{command corec},
62745
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   541
we can use the following command:
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   542
\<close>
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   543
62745
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   544
    coinduction_upto nat_int_tllist: "(nat, int) tllist"
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   545
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   546
text \<open>
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   547
\noindent
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   548
This produces the theorems
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   549
%
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   550
\begin{indentblock}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   551
@{thm [source] nat_int_tllist.coinduct_upto} \\
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   552
@{thm [source] nat_int_tllist.cong_intros}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   553
\end{indentblock}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   554
%
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   555
(as well as the individually named introduction rules) and extends
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   556
the dynamic collections @{thm [source] tllist.coinduct_upto} and
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   557
@{thm [source] tllist.cong_intros}.
62745
257a022f7e7b more 'corec' docs
blanchet
parents: 62742
diff changeset
   558
\<close>
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   559
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   560
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   561
subsection \<open>Uniqueness Reasoning
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   562
  \label{ssec:uniqueness-reasoning}\<close>
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   563
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   564
text \<open>
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   565
It is sometimes possible to achieve better automation by using a more
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   566
specialized proof method than coinduction. Uniqueness principles maintain a good
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   567
balance between expressiveness and automation. They exploit the property that a
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   568
corecursive definition is the unique solution to a fixpoint equation.
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   569
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   570
The @{command corec}, @{command corecursive}, and @{command friend_of_corec}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   571
commands generate a property @{text f.unique} about the function of interest
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   572
@{term f} that can be used to prove that any function that satisfies
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   573
@{term f}'s corecursive specification must be equal to~@{term f}. For example:
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   574
\[@{thm ssum.unique[no_vars]}\]
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   575
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   576
The uniqueness principles are not restricted to functions defined using
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   577
@{command corec} or @{command corecursive} or registered with
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   578
@{command friend_of_corec}. Suppose @{term "t x"} is an arbitrary term
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   579
depending on @{term x}. The @{method corec_unique} proof method, provided by our
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   580
tool, transforms subgoals of the form
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   581
\[@{term "(\<forall>x. f x = H x f) \<Longrightarrow> f x = t x"}\]
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   582
into
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   583
\[@{term "\<forall>x. t x = H x t"}\]
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   584
The higher-order functional @{term H} must be such that @{term "f x = H x f"}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   585
would be a valid @{command corec} specification, but without nested self-calls
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   586
or unguarded (recursive) calls. Thus, @{method corec_unique} proves uniqueness
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   587
of @{term t} with respect to the given corecursive equation regardless of how
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   588
@{term t} was defined. For example:
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   589
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   590
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   591
    lemma
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   592
      fixes f :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream"
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   593
      assumes "\<forall>xs ys. f xs ys =
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   594
        SCons (shd ys * shd xs) (ssum (f xs (stl ys)) (f (stl xs) ys))"
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   595
      shows "f = sprod"
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   596
        using assms
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   597
      proof corec_unique
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   598
        show "sprod = (\<lambda>xs ys :: nat stream.
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   599
            SCons (shd ys * shd xs) (ssum (sprod xs (stl ys)) (sprod (stl xs) ys)))"
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   600
          apply (rule ext)+
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   601
          apply (subst sprod.code)
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   602
          by simp
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   603
      qed
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   604
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   605
text \<open>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   606
The proof method relies on some theorems generated by the package. If no function
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   607
over a given codatatype has been defined using @{command corec} or
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   608
@{command corecursive} or registered as friendly using @{command friend_of_corec},
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   609
the theorems will not be available yet. In such cases, the theorems can be
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   610
explicitly generated using the command
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   611
\<close>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   612
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   613
    coinduction_upto stream: "'a stream"
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   614
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   615
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   616
section \<open>Command Syntax
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   617
  \label{sec:command-syntax}\<close>
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   618
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   619
subsection \<open>\keyw{corec} and \keyw{corecursive}
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   620
  \label{ssec:corec-and-corecursive-syntax}\<close>
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   621
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   622
text \<open>
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   623
\begin{matharray}{rcl}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   624
  @{command_def "corec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   625
  @{command_def "corecursive"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   626
\end{matharray}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   627
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   628
@{rail \<open>
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   629
  (@@{command corec} | @@{command corecursive}) target? \<newline>
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   630
    @{syntax cr_options}? fix @'where' prop
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   631
  ;
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   632
  @{syntax_def cr_options}: '(' ((@{syntax plugins} | 'friend' | 'transfer') + ',') ')'
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   633
\<close>}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   634
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   635
\medskip
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   636
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   637
\noindent
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   638
The @{command corec} and @{command corecursive} commands introduce a corecursive
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   639
function over a codatatype.
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   640
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   641
The syntactic entity \synt{target} can be used to specify a local context,
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   642
\synt{fix} denotes name with an optional type signature, and \synt{prop} denotes
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   643
a HOL proposition @{cite "isabelle-isar-ref"}.
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   644
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   645
The optional target is optionally followed by a combination of the following
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   646
options:
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   647
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   648
\begin{itemize}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   649
\setlength{\itemsep}{0pt}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   650
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   651
\item
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   652
The @{text plugins} option indicates which plugins should be enabled
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   653
(@{text only}) or disabled (@{text del}). By default, all plugins are enabled.
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   654
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   655
\item
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   656
The @{text friend} option indicates that the defined function should be
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   657
registered as a friend. This gives rise to additional proof obligations.
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   658
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   659
\item
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   660
The @{text transfer} option indicates that an unconditional transfer rule
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   661
should be generated and proved @{text "by transfer_prover"}. The
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   662
@{text "[transfer_rule]"} attribute is set on the generated theorem.
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   663
\end{itemize}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   664
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   665
The @{command corec} command is an abbreviation for @{command corecursive}
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   666
with appropriate applications of @{method transfer_prover_eq}
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   667
(Section~\ref{ssec:transfer-prover-eq}) and @{method lexicographic_order} to
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   668
discharge any emerging proof obligations.
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   669
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   670
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   671
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   672
subsection \<open>\keyw{friend_of_corec}
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   673
  \label{ssec:friend-of-corec-syntax}\<close>
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   674
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   675
text \<open>
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   676
\begin{matharray}{rcl}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   677
  @{command_def "friend_of_corec"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   678
\end{matharray}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   679
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   680
@{rail \<open>
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   681
  @@{command friend_of_corec} target? \<newline>
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   682
    @{syntax foc_options}? fix @'where' prop
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   683
  ;
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   684
  @{syntax_def foc_options}: '(' ((@{syntax plugins} | 'transfer') + ',') ')'
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   685
\<close>}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   686
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   687
\medskip
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   688
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   689
\noindent
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   690
The @{command friend_of_corec} command registers a corecursive function as
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   691
friendly.
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   692
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   693
The syntactic entity \synt{target} can be used to specify a local context,
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   694
\synt{fix} denotes name with an optional type signature, and \synt{prop} denotes
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   695
a HOL proposition @{cite "isabelle-isar-ref"}.
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   696
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   697
The optional target is optionally followed by a combination of the following
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   698
options:
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   699
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   700
\begin{itemize}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   701
\setlength{\itemsep}{0pt}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   702
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   703
\item
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   704
The @{text plugins} option indicates which plugins should be enabled
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   705
(@{text only}) or disabled (@{text del}). By default, all plugins are enabled.
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   706
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   707
\item
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   708
The @{text transfer} option indicates that an unconditional transfer rule
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   709
should be generated and proved @{text "by transfer_prover"}. The
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   710
@{text "[transfer_rule]"} attribute is set on the generated theorem.
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   711
\end{itemize}
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   712
\<close>
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   713
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   714
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   715
subsection \<open>\keyw{coinduction_upto}
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   716
  \label{ssec:coinduction-upto-syntax}\<close>
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   717
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   718
text \<open>
62747
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   719
\begin{matharray}{rcl}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   720
  @{command_def "coinduction_upto"} & : & @{text "local_theory \<rightarrow> local_theory"}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   721
\end{matharray}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   722
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   723
@{rail \<open>
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   724
  @@{command coinduction_upto} target? name ':' type
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   725
\<close>}
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   726
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   727
\medskip
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   728
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   729
\noindent
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   730
The @{command coinduction_upto} generates a coinduction up-to rule for a given
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   731
instance of a (possibly polymorphic) codatatype and notes the result with the
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   732
specified prefix.
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   733
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   734
The syntactic entity \synt{name} denotes an identifier and \synt{type} denotes a
f65ef4723aca more 'corec' docs
blanchet
parents: 62745
diff changeset
   735
type @{cite "isabelle-isar-ref"}.
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   736
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   737
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   738
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   739
section \<open>Generated Theorems
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   740
  \label{sec:generated-theorems}\<close>
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   741
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   742
text \<open>
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   743
The full list of named theorems generated by the package can be obtained by
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   744
issuing the command \keyw{print_theorems} immediately after the datatype definition.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   745
This list excludes low-level theorems that reveal internal constructions. To
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   746
make these accessible, add the line
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   747
\<close>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   748
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   749
    declare [[bnf_internals]]
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   750
(*<*)
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   751
    declare [[bnf_internals = false]]
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   752
(*>*)
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   753
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   754
text \<open>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   755
In addition to the theorem listed below for each command provided by the
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   756
package, all commands update the dynamic theorem collections
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   757
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   758
\begin{indentblock}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   759
\begin{description}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   760
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   761
\item[@{text "t."}\hthm{coinduct_upto}]
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   762
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   763
\item[@{text "t."}\hthm{cong_intros}]
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   764
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   765
\end{description}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   766
\end{indentblock}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   767
%
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   768
for the corresponding codatatype @{text t} so that they always contain the most
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   769
powerful coinduction up-to principles derived so far.
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   770
\<close>
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   771
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   772
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   773
subsection \<open>\keyw{corec} and \keyw{corecursive}
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   774
  \label{ssec:corec-and-corecursive-theorems}\<close>
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   775
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   776
text \<open>
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   777
For a function @{term f} over codatatype @{text t}, the @{command corec} and
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   778
@{command corecursive} commands generate the following properties (listed for
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   779
@{const sexp}, cf. Section~\ref{ssec:simple-corecursion}):
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   780
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   781
\begin{indentblock}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   782
\begin{description}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   783
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   784
\item[@{text "f."}\hthm{code} @{text "[code]"}\rm:] ~ \\
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   785
@{thm sexp.code[no_vars]} \\
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   786
The @{text "[code]"} attribute is set by the @{text code} plugin
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   787
@{cite "isabelle-datatypes"}.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   788
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   789
\item[@{text "f."}\hthm{coinduct} @{text "[consumes 1, case_names t, case_conclusion D\<^sub>1 \<dots>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   790
  D\<^sub>n]"}\rm:] ~ \\
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   791
@{thm sexp.coinduct[no_vars]}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   792
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   793
\item[@{text "f."}\hthm{cong_intros}\rm:] ~ \\
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   794
@{thm sexp.cong_intros[no_vars]}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   795
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   796
\item[@{text "f."}\hthm{unique}\rm:] ~ \\
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   797
@{thm sexp.unique[no_vars]} \\
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   798
This property is not generated for mixed recursive--corecursive definitions.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   799
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   800
\item[@{text "f."}\hthm{inner_induct}\rm:] ~ \\
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   801
This property is only generated for mixed recursive--corecursive definitions.
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   802
For @{const primes} (Section~\ref{ssec:mixed-recursion-corecursion}, it reads as
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   803
follows: \\[\jot]
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   804
@{thm primes.inner_induct[no_vars]}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   805
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   806
\end{description}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   807
\end{indentblock}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   808
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   809
\noindent
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   810
The individual rules making up @{text "f.cong_intros"} are available as
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   811
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   812
\begin{indentblock}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   813
\begin{description}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   814
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   815
\item[@{text "f."}\hthm{cong_base}]
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   816
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   817
\item[@{text "f."}\hthm{cong_refl}]
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   818
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   819
\item[@{text "f."}\hthm{cong_sym}]
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   820
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   821
\item[@{text "f."}\hthm{cong_trans}]
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   822
62816
19387866eace tuned LaTeX
blanchet
parents: 62756
diff changeset
   823
\item[@{text "f."}\hthm{cong_C}@{text "\<^sub>1"}, \ldots, @{text "f."}\hthm{cong_C}@{text "\<^sub>n"}] ~ \\
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   824
where @{text "C\<^sub>1"}, @{text "\<dots>"}, @{text "C\<^sub>n"} are @{text t}'s
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   825
constructors
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   826
62816
19387866eace tuned LaTeX
blanchet
parents: 62756
diff changeset
   827
\item[@{text "f."}\hthm{cong_f}@{text "\<^sub>1"}, \ldots, @{text "f."}\hthm{cong_f}@{text "\<^sub>m"}] ~ \\
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   828
where @{text "f\<^sub>1"}, @{text "\<dots>"}, @{text "f\<^sub>m"} are the available
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   829
friends for @{text t}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   830
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   831
\end{description}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   832
\end{indentblock}
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   833
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   834
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   835
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   836
subsection \<open>\keyw{friend_of_corec}
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   837
  \label{ssec:friend-of-corec-theorems}\<close>
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   838
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   839
text \<open>
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   840
The @{command friend_of_corec} command generates the same theorems as
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   841
@{command corec} and @{command corecursive}, except that it adds an optional
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   842
@{text "friend."} component to the names to prevent potential clashes (e.g.,
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   843
@{text "f.friend.code"}).
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   844
\<close>
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   845
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   846
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   847
subsection \<open>\keyw{coinduction_upto}
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   848
  \label{ssec:coinduction-upto-theorems}\<close>
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   849
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   850
text \<open>
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   851
The @{command coinduction_upto} command generates the following properties
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   852
(listed for @{text nat_int_tllist}):
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   853
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   854
\begin{indentblock}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   855
\begin{description}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   856
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   857
\item[\begin{tabular}{@ {}l@ {}}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   858
  @{text "t."}\hthm{coinduct_upto} @{text "[consumes 1, case_names t,"} \\
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   859
  \phantom{@{text "t."}\hthm{coinduct_upto} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   860
  D\<^sub>n]"}\rm:
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   861
\end{tabular}] ~ \\
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   862
@{thm nat_int_tllist.coinduct_upto[no_vars]}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   863
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   864
\item[@{text "t."}\hthm{cong_intros}\rm:] ~ \\
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   865
@{thm nat_int_tllist.cong_intros[no_vars]}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   866
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   867
\end{description}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   868
\end{indentblock}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   869
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   870
\noindent
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   871
The individual rules making up @{text "t.cong_intros"} are available
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   872
separately as @{text "t.cong_base"}, @{text "t.cong_refl"}, etc.\
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   873
(Section~\ref{ssec:corec-and-corecursive-theorems}).
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   874
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   875
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   876
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   877
section \<open>Proof Methods
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   878
  \label{sec:proof-methods}\<close>
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   879
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   880
subsection \<open>\textit{corec_unique}
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   881
  \label{ssec:corec-unique}\<close>
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   882
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   883
text \<open>
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   884
The @{method corec_unique} proof method can be used to prove the uniqueness of
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   885
a corecursive specification. See Section~\ref{ssec:uniqueness-reasoning} for
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   886
details.
62742
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   887
\<close>
bfb5a70e4319 more 'corec' documentation
blanchet
parents: 62739
diff changeset
   888
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   889
64380
4b22e1268779 document transfer_prover_eq and friend_of_corec_simps
Andreas Lochbihler
parents: 63680
diff changeset
   890
subsection \<open>\textit{transfer_prover_eq}
4b22e1268779 document transfer_prover_eq and friend_of_corec_simps
Andreas Lochbihler
parents: 63680
diff changeset
   891
  \label{ssec:transfer-prover-eq}\<close>
4b22e1268779 document transfer_prover_eq and friend_of_corec_simps
Andreas Lochbihler
parents: 63680
diff changeset
   892
4b22e1268779 document transfer_prover_eq and friend_of_corec_simps
Andreas Lochbihler
parents: 63680
diff changeset
   893
text \<open>
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   894
The @{method transfer_prover_eq} proof method replaces the equality relation
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   895
@{term "op ="} with compound relator expressions according to
64380
4b22e1268779 document transfer_prover_eq and friend_of_corec_simps
Andreas Lochbihler
parents: 63680
diff changeset
   896
@{thm [source] relator_eq} before calling @{method transfer_prover} on the
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   897
current subgoal. It tends to work better than plain @{method transfer_prover} on
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   898
the parametricity proof obligations of @{command corecursive} and
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   899
@{command friend_of_corec}, because they often contain equality relations on
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   900
complex types, which @{method transfer_prover} cannot reason about.
64380
4b22e1268779 document transfer_prover_eq and friend_of_corec_simps
Andreas Lochbihler
parents: 63680
diff changeset
   901
\<close>
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   902
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   903
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   904
section \<open>Attribute
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   905
  \label{sec:attribute}\<close>
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   906
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   907
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   908
subsection \<open>\textit{friend_of_corec_simps}
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   909
  \label{ssec:friend-of-corec-simps}\<close>
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   910
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   911
text \<open>
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   912
The @{attribute friend_of_corec_simps} attribute declares naturality theorems
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   913
to be used by @{command friend_of_corec} and @{command corec} @{text "(friend)"} in
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   914
deriving the user specification from reduction to primitive corecursion.
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   915
Internally, these commands derive naturality theorems from the parametricity proof
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   916
obligations dischared by the user or the @{method transfer_prover_eq} method, but
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   917
this derivation fails if in the arguments of a higher-order constant a type variable
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   918
occurs on both sides of the function type constructor. The required naturality
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   919
theorem can then be declared with @{attribute friend_of_corec_simps}. See
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   920
@{file "~~/src/HOL/Corec_Examples/Tests/Iterate_GPV.thy"} for an example.
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   921
\<close>
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   922
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   923
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   924
section \<open>Known Bugs and Limitations
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   925
  \label{sec:known-bugs-and-limitations}\<close>
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   926
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   927
text \<open>
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   928
This section lists the known bugs and limitations of the corecursion package at
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   929
the time of this writing.
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   930
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   931
\begin{enumerate}
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   932
\setlength{\itemsep}{0pt}
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   933
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   934
\item
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   935
\emph{Mutually corecursive codatatypes are not supported.}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   936
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   937
\item
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   938
\emph{The signature of friend functions may not depend on type variables beyond
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   939
those that appear in the codatatype.}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   940
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   941
\item
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   942
\emph{The internal tactics may fail on legal inputs.}
64384
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   943
In some cases, this limitation can be circumvented using the
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   944
@{attribute friend_of_corec_simps} attribute
f8c1c12d6af5 tuned documentation
blanchet
parents: 64383
diff changeset
   945
(Section~\ref{ssec:friend-of-corec-simps}).
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   946
62756
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   947
\item
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   948
\emph{The @{text transfer} option is not implemented yet.}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   949
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   950
\item
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   951
\emph{The constructor and destructor views offered by {\upshape\keyw{primcorec}}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   952
are not supported by @{command corec} and @{command corecursive}.}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   953
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   954
\item
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   955
\emph{There is no mechanism for registering custom plugins.}
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   956
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   957
\item
d4b7d128ec5a more 'corec' docs
blanchet
parents: 62747
diff changeset
   958
\emph{The package does not interact well with locales.}
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   959
64383
b9d4efb43fd9 document limitations
blanchet
parents: 64380
diff changeset
   960
\item
b9d4efb43fd9 document limitations
blanchet
parents: 64380
diff changeset
   961
\emph{The undocumented @{text corecUU_transfer} theorem is not as polymorphic as
b9d4efb43fd9 document limitations
blanchet
parents: 64380
diff changeset
   962
it could be.}
b9d4efb43fd9 document limitations
blanchet
parents: 64380
diff changeset
   963
b9d4efb43fd9 document limitations
blanchet
parents: 64380
diff changeset
   964
\item
b9d4efb43fd9 document limitations
blanchet
parents: 64380
diff changeset
   965
\emph{All type variables occurring in the arguments of a friendly function must occur
b9d4efb43fd9 document limitations
blanchet
parents: 64380
diff changeset
   966
as direct arguments of the type constructor of the resulting type.}
b9d4efb43fd9 document limitations
blanchet
parents: 64380
diff changeset
   967
62739
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   968
\end{enumerate}
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   969
\<close>
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   970
628c97d39627 added sketchy 'corec' documentation
blanchet
parents:
diff changeset
   971
end