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