author | wenzelm |
Sat, 10 Jun 2017 21:48:02 +0200 | |
changeset 66061 | 880db47fed30 |
parent 65552 | f533820e7248 |
child 66453 | cc19f7ca2ed6 |
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 |
|
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 | 13 |
"~~/src/HOL/Library/FSet" |
62739 | 14 |
begin |
15 |
||
16 |
section \<open>Introduction |
|
17 |
\label{sec:introduction}\<close> |
|
18 |
||
19 |
text \<open> |
|
62756 | 20 |
Isabelle's (co)datatype package @{cite "isabelle-datatypes"} offers a convenient |
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. |
|
37 |
The package is not part of @{theory Main}; 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} |
|
55 |
command, or by passing the @{text friend} option to @{command corec}. The |
|
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 |
|
62756 | 73 |
The package fully adheres to the LCF philosophy @{cite mgordon79}: The |
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 |
|
77 |
@{text quick_and_dirty} option is enabled.) |
|
62756 | 78 |
The package is described in a pair of scientific papers |
64384 | 79 |
@{cite "blanchette-et-al-2015-fouco" and "blanchette-et-al-201x-amico"}. 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} |
|
102 |
@{text "(friend)"} 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> |
62747 | 140 |
The case studies by Rutten~@{cite rutten05} and Hinze~@{cite hinze10} 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 |
|
152 |
specification of @{const ssum} where a constructor (@{const SCons}) occurs at |
|
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 |
|
64384 | 168 |
can usually be discharged using the @{text transfer_prover} or |
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 |
|
174 |
After registering @{const ssum} as a friend, we can use it in the corecursive |
|
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> |
|
187 |
Using the @{text "friend"} option, we can simultaneously define a function and |
|
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 |
|
64384 | 204 |
The parametricity subgoal is given to @{text transfer_prover_eq} |
205 |
(Section~\ref{ssec:transfer-prover-eq}). |
|
62742 | 206 |
|
207 |
The @{const sprod} and @{const sexp} functions provide shuffle product and |
|
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) |
232 |
@{cite "isabelle-datatypes"}, with the restriction that the target codatatype |
|
233 |
(@{typ "nat stream"}) may occur only in a \emph{live} position of the BNF. For |
|
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> |
|
255 |
We first define the pointwise sum of two trees analogously to @{const ssum}: |
|
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 |
|
264 |
Here, @{const map} is the standard map function on lists, and @{const zip} |
|
62756 | 265 |
converts two parallel lists into a list of pairs. The @{const tsum} function is |
64384 | 266 |
primitively corecursive. Instead of @{command corec} @{text "(friend)"}, we could |
267 |
also have used \keyw{primcorec} and @{command friend_of_corec}, as we did for |
|
62742 | 268 |
@{const ssum}. |
269 |
||
62756 | 270 |
Once @{const tsum} is registered as friendly, we can use it in the corecursive |
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 |
|
282 |
@{text \<lambda>}-abstractions and function applications rather than through composition |
|
283 |
(@{term "op \<circ>"}, the map function for @{text \<Rightarrow>}). For example: |
|
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 |
|
325 |
corecursive definition. An example is the @{term primes} function from Di |
|
326 |
Gianantonio and Miculan @{cite "di-gianantonio-miculan-2003"}: |
|
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)") |
|
337 |
apply (auto simp: mod_Suc intro: Suc_lessI) |
|
338 |
apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat) |
|
339 |
by (metis diff_less_mono2 lessI mod_less_divisor) |
|
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 |
||
62756 | 346 |
When called with @{text "m = 1"} and @{text "n = 2"}, the @{const primes} |
62742 | 347 |
function computes the stream of prime numbers. The unguarded call in the |
348 |
@{text else} branch increments @{term n} until it is coprime to the first |
|
349 |
argument @{term m} (i.e., the greatest common divisor of @{term m} and |
|
62756 | 350 |
@{term n} is @{text 1}). |
62742 | 351 |
|
352 |
For any positive integers @{term m} and @{term n}, the numbers @{term m} and |
|
62756 | 353 |
@{text "m * n + 1"} are coprime, yielding an upper bound on the number of times |
62742 | 354 |
@{term n} is increased. Hence, the function will take the @{text else} branch at |
355 |
most finitely often before taking the then branch and producing one constructor. |
|
62756 | 356 |
There is a slight complication when @{text "m = 0 \<and> n > 1"}: Without the first |
62742 | 357 |
disjunct in the @{text "if"} condition, the function could stall. (This corner |
62747 | 358 |
case was overlooked in the original example |
359 |
@{cite "di-gianantonio-miculan-2003"}.) |
|
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 |
|
408 |
about it. The @{text codatatype} command generates a structural coinduction |
|
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 |
||
413 |
The structural coinduction principle for @{typ "'a stream"}, called |
|
414 |
@{thm [source] stream.coinduct}, is as follows: |
|
415 |
% |
|
62747 | 416 |
\begin{indentblock} |
417 |
@{thm stream.coinduct[no_vars]} |
|
418 |
\end{indentblock} |
|
62742 | 419 |
% |
420 |
Coinduction allows us to prove an equality @{text "l = r"} on streams by |
|
421 |
providing a relation @{text R} that relates @{text l} and @{text r} (first |
|
422 |
premise) and that constitutes a bisimulation (second premise). Streams that are |
|
423 |
related by a bisimulation cannot be distinguished by taking observations (via |
|
424 |
the selectors @{const shd} and @{const stl}); hence they must be equal. |
|
425 |
||
426 |
The coinduction up-to principle after registering @{const sskew} 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 |
|
62756 | 435 |
corecursive application of @{term R} is generalized to |
436 |
@{term "stream.v5.congclp R"}. |
|
437 |
||
438 |
The @{const stream.v5.congclp} predicate is equipped with the following |
|
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 |
||
474 |
Notice that there is no introduction rule corresponding to @{const sexp}, |
|
475 |
because @{const sexp} has a more restrictive result type than @{const sskew} |
|
476 |
(@{typ "nat stream"} vs. @{typ "('a :: {plus,times}) stream"}. |
|
477 |
||
62756 | 478 |
The version numbers, here @{text v5}, distinguish the different congruence |
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 |
|
489 |
the first rule that matches. For example, after registering @{const ssum} as a |
|
490 |
friend, proving the equality @{term "l = r"} on @{typ "nat stream"} might |
|
491 |
require coinduction principle for @{term "nat stream"}, which is up to |
|
492 |
@{const ssum}. |
|
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} |
|
526 |
\item @{typ "('a, int) tllist"} up to @{const TNil}, @{const TCons}, and |
|
527 |
@{const square_terminal}; |
|
528 |
\item @{typ "(nat, 'b) tllist"} up to @{const TNil}, @{const TCons}, and |
|
529 |
@{const square_elems}; |
|
530 |
\item @{typ "('a, 'b) tllist"} up to @{const TNil} and @{const TCons}. |
|
531 |
\end{itemize} |
|
532 |
% |
|
533 |
The following variant is missing: |
|
534 |
% |
|
535 |
\begin{itemize} |
|
536 |
\item @{typ "(nat, int) tllist"} up to @{const TNil}, @{const TCons}, |
|
537 |
@{const square_elems}, and @{const square_terminal}. |
|
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} |
|
571 |
commands generate a property @{text f.unique} about the function of interest |
|
572 |
@{term f} that can be used to prove that any function that satisfies |
|
62756 | 573 |
@{term f}'s corecursive specification must be equal to~@{term f}. 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 |
|
578 |
@{command friend_of_corec}. Suppose @{term "t x"} is an arbitrary term |
|
579 |
depending on @{term x}. The @{method corec_unique} proof method, provided by our |
|
580 |
tool, transforms subgoals of the form |
|
581 |
\[@{term "(\<forall>x. f x = H x f) \<Longrightarrow> f x = t x"}\] |
|
582 |
into |
|
583 |
\[@{term "\<forall>x. t x = H x t"}\] |
|
62756 | 584 |
The higher-order functional @{term H} must be such that @{term "f x = H x f"} |
585 |
would be a valid @{command corec} specification, but without nested self-calls |
|
586 |
or unguarded (recursive) calls. Thus, @{method corec_unique} proves uniqueness |
|
587 |
of @{term t} with respect to the given corecursive equation regardless of how |
|
588 |
@{term t} 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} |
624 |
@{command_def "corec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
|
625 |
@{command_def "corecursive"} & : & @{text "local_theory \<rightarrow> proof(prove)"} |
|
626 |
\end{matharray} |
|
627 |
||
628 |
@{rail \<open> |
|
629 |
(@@{command corec} | @@{command corecursive}) target? \<newline> |
|
630 |
@{syntax cr_options}? fix @'where' prop |
|
631 |
; |
|
632 |
@{syntax_def cr_options}: '(' ((@{syntax plugins} | 'friend' | 'transfer') + ',') ')' |
|
633 |
\<close>} |
|
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 |
|
643 |
a HOL proposition @{cite "isabelle-isar-ref"}. |
|
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 |
|
652 |
The @{text plugins} option indicates which plugins should be enabled |
|
653 |
(@{text only}) or disabled (@{text del}). By default, all plugins are enabled. |
|
654 |
||
655 |
\item |
|
656 |
The @{text friend} option indicates that the defined function should be |
|
657 |
registered as a friend. This gives rise to additional proof obligations. |
|
658 |
||
659 |
\item |
|
660 |
The @{text transfer} option indicates that an unconditional transfer rule |
|
661 |
should be generated and proved @{text "by transfer_prover"}. The |
|
662 |
@{text "[transfer_rule]"} attribute is set on the generated theorem. |
|
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} |
677 |
@{command_def "friend_of_corec"} & : & @{text "local_theory \<rightarrow> proof(prove)"} |
|
678 |
\end{matharray} |
|
679 |
||
680 |
@{rail \<open> |
|
681 |
@@{command friend_of_corec} target? \<newline> |
|
682 |
@{syntax foc_options}? fix @'where' prop |
|
683 |
; |
|
684 |
@{syntax_def foc_options}: '(' ((@{syntax plugins} | 'transfer') + ',') ')' |
|
685 |
\<close>} |
|
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 |
|
695 |
a HOL proposition @{cite "isabelle-isar-ref"}. |
|
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 |
|
704 |
The @{text plugins} option indicates which plugins should be enabled |
|
705 |
(@{text only}) or disabled (@{text del}). By default, all plugins are enabled. |
|
706 |
||
707 |
\item |
|
708 |
The @{text transfer} option indicates that an unconditional transfer rule |
|
709 |
should be generated and proved @{text "by transfer_prover"}. The |
|
710 |
@{text "[transfer_rule]"} attribute is set on the generated theorem. |
|
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} |
720 |
@{command_def "coinduction_upto"} & : & @{text "local_theory \<rightarrow> local_theory"} |
|
721 |
\end{matharray} |
|
722 |
||
723 |
@{rail \<open> |
|
724 |
@@{command coinduction_upto} target? name ':' type |
|
725 |
\<close>} |
|
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 |
|
735 |
type @{cite "isabelle-isar-ref"}. |
|
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 |
||
761 |
\item[@{text "t."}\hthm{coinduct_upto}] |
|
762 |
||
763 |
\item[@{text "t."}\hthm{cong_intros}] |
|
764 |
||
765 |
\end{description} |
|
766 |
\end{indentblock} |
|
767 |
% |
|
768 |
for the corresponding codatatype @{text t} so that they always contain the most |
|
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> |
62756 | 777 |
For a function @{term f} over codatatype @{text t}, the @{command corec} and |
778 |
@{command corecursive} commands generate the following properties (listed for |
|
779 |
@{const sexp}, cf. Section~\ref{ssec:simple-corecursion}): |
|
780 |
||
781 |
\begin{indentblock} |
|
782 |
\begin{description} |
|
783 |
||
784 |
\item[@{text "f."}\hthm{code} @{text "[code]"}\rm:] ~ \\ |
|
785 |
@{thm sexp.code[no_vars]} \\ |
|
786 |
The @{text "[code]"} attribute is set by the @{text code} plugin |
|
787 |
@{cite "isabelle-datatypes"}. |
|
788 |
||
789 |
\item[@{text "f."}\hthm{coinduct} @{text "[consumes 1, case_names t, case_conclusion D\<^sub>1 \<dots> |
|
790 |
D\<^sub>n]"}\rm:] ~ \\ |
|
791 |
@{thm sexp.coinduct[no_vars]} |
|
792 |
||
793 |
\item[@{text "f."}\hthm{cong_intros}\rm:] ~ \\ |
|
794 |
@{thm sexp.cong_intros[no_vars]} |
|
795 |
||
796 |
\item[@{text "f."}\hthm{unique}\rm:] ~ \\ |
|
797 |
@{thm sexp.unique[no_vars]} \\ |
|
798 |
This property is not generated for mixed recursive--corecursive definitions. |
|
799 |
||
800 |
\item[@{text "f."}\hthm{inner_induct}\rm:] ~ \\ |
|
801 |
This property is only generated for mixed recursive--corecursive definitions. |
|
802 |
For @{const primes} (Section~\ref{ssec:mixed-recursion-corecursion}, it reads as |
|
803 |
follows: \\[\jot] |
|
804 |
@{thm primes.inner_induct[no_vars]} |
|
805 |
||
806 |
\end{description} |
|
807 |
\end{indentblock} |
|
808 |
||
809 |
\noindent |
|
810 |
The individual rules making up @{text "f.cong_intros"} are available as |
|
811 |
||
812 |
\begin{indentblock} |
|
813 |
\begin{description} |
|
814 |
||
815 |
\item[@{text "f."}\hthm{cong_base}] |
|
816 |
||
817 |
\item[@{text "f."}\hthm{cong_refl}] |
|
818 |
||
819 |
\item[@{text "f."}\hthm{cong_sym}] |
|
820 |
||
821 |
\item[@{text "f."}\hthm{cong_trans}] |
|
822 |
||
62816 | 823 |
\item[@{text "f."}\hthm{cong_C}@{text "\<^sub>1"}, \ldots, @{text "f."}\hthm{cong_C}@{text "\<^sub>n"}] ~ \\ |
62756 | 824 |
where @{text "C\<^sub>1"}, @{text "\<dots>"}, @{text "C\<^sub>n"} are @{text t}'s |
825 |
constructors |
|
826 |
||
62816 | 827 |
\item[@{text "f."}\hthm{cong_f}@{text "\<^sub>1"}, \ldots, @{text "f."}\hthm{cong_f}@{text "\<^sub>m"}] ~ \\ |
62756 | 828 |
where @{text "f\<^sub>1"}, @{text "\<dots>"}, @{text "f\<^sub>m"} are the available |
829 |
friends for @{text t} |
|
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 |
|
842 |
@{text "friend."} component to the names to prevent potential clashes (e.g., |
|
843 |
@{text "f.friend.code"}). |
|
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 |
852 |
(listed for @{text nat_int_tllist}): |
|
853 |
||
854 |
\begin{indentblock} |
|
855 |
\begin{description} |
|
856 |
||
857 |
\item[\begin{tabular}{@ {}l@ {}} |
|
858 |
@{text "t."}\hthm{coinduct_upto} @{text "[consumes 1, case_names t,"} \\ |
|
859 |
\phantom{@{text "t."}\hthm{coinduct_upto} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> |
|
860 |
D\<^sub>n]"}\rm: |
|
861 |
\end{tabular}] ~ \\ |
|
862 |
@{thm nat_int_tllist.coinduct_upto[no_vars]} |
|
863 |
||
864 |
\item[@{text "t."}\hthm{cong_intros}\rm:] ~ \\ |
|
865 |
@{thm nat_int_tllist.cong_intros[no_vars]} |
|
866 |
||
867 |
\end{description} |
|
868 |
\end{indentblock} |
|
869 |
||
870 |
\noindent |
|
871 |
The individual rules making up @{text "t.cong_intros"} are available |
|
872 |
separately as @{text "t.cong_base"}, @{text "t.cong_refl"}, etc.\ |
|
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 |
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 | 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 |
|
913 |
to be used by @{command friend_of_corec} and @{command corec} @{text "(friend)"} in |
|
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 |
|
920 |
@{file "~~/src/HOL/Corec_Examples/Tests/Iterate_GPV.thy"} for an example. |
|
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 |
948 |
\emph{The @{text transfer} option is not implemented yet.} |
|
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 |
961 |
\emph{The undocumented @{text corecUU_transfer} theorem is not as polymorphic as |
|
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 |