[isabelle-dev] Non-standard transfer vs. generic transfer
lp15 at cam.ac.uk
Mon Oct 26 09:33:10 CET 2009
A brief comment: a few weeks ago, I found myself doing a difficult
epsilon/delta proof, invoking limit theorems using e/2^N and summing
them up to get e, when I suddenly remembered non-standard analysis and
how it could eliminate those horrible proofs. Only, by that time, I
had nearly finished this proof; moreover, its argument (involving a
bijection between N x N and N) might have been difficult to formalise
using non-standard analysis.
However, I hope that non-standard analysis doesn't get overlooked in
our developments; I recall once thinking that it was worth any number
of decision procedures.
On 26 Oct 2009, at 08:17, Florian Haftmann wrote:
> Hi Brian,
> I would like to come back to the matter of the non-standard transfer
> method in theory src/HOL/NSA/StarDef.thy, or more exactly its name.
> With the perspective that in future the generic transfer facilities
> (src/HOL/Tools/transfer.ML) could also provide a method "transfer",
> methods have to be distinguished somehow.
> What comes to my mind are three options:
> a) rename non-standard transfer method to hyper_transfer
> b) rename non-standard transfer method to star_transfer
> c) or join theories src/HOL/NSA/StarDef.thy and src/HOL/NSA/Star.thy,
> such that the resulting full method name is Star.transfer
> What's you opinion about this?
> Currently, the need is not urgent, but perhaps the upcoming release
> is a
> good opportunity.
> PGP available:
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev