| 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.