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