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 <John.Harrison@cl.cam.ac.uk>
Message-ID: <"swan.cl.cam.:171830:950522132813"@cl.cam.ac.uk>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


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.