Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id IAA03302 for qed-out; Mon, 22 May 1995 08:30:04 -0500
Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id IAA03297 for ; Mon, 22 May 1995 08:29:56 -0500
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk
with SMTP (PP-6.5) to cl; Mon, 22 May 1995 14:27:46 +0100
To: qed@mcs.anl.gov
In-reply-to: Your message of "Mon, 22 May 1995 13:41:00 -0400." <9505221347.AA09578@cksr.ac.bialystok.pl>
Date: Mon, 22 May 1995 14:27:18 +0100
From: John Harrison
Message-ID: <"swan.cl.cam.:171830:950522132813"@cl.cam.ac.uk>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.020
Andrzej Trybulec writes:
| If I correctly recall
| permissiveness is used in Excheck for the abstraction operator, one
| can use
| { x : P[x] }
| without any restriction, but to infer
| y \in { x : P[x] } implies P[y]
| one have to prove earlier that there exists a set A such that
| P[x] implies x \in A
Yes, I meant to remark on this kind of problem with approaches [1] and [2]. In
the HOL real analysis theories we have various higher order operators for
"limit", "derivative", "integral" and so on. These are usually applied to
lambda terms giving a uniform treatment of variable binding constructs (see QED
passim.) Thus:
|- lim x_n = l
n->oo
is really a gloss for something like:
|- LIM_INFINITY (\n. x_n) = l
Because of the approach I've taken to undefinedness, theorems like this are
weaker than they look. LIM_INFINITY returns a value on any sequence, whether
convergent or not, and we can't a priori rule out the possibility that it could
give "l" on a nonconvergent sequence. Thus the above does *not* imply that
"x_n" is convergent. In practice then, I tend to use the stronger property "x_n
tends to l" instead of "the limit of x_n is l". For example, the theorem about
the limit of a sum is (verbatim; "!" means "for all", "/\" means "and", "==>"
means "implies" and "\" means "lambda"):
|- !x x0 y y0. x --> x0 /\ y --> y0 ==> (\n. x(n) + y(n)) --> (x0 + y0)
On the whole this works well, but has quite poor compositionality properties;
for example dealing with nontrivial differential equations in these terms is a
bit tiresome!
John.