[isabelle-dev] Non-standard transfer vs. generic transfer

[Lawrence Paulson]

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

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",  
> both
> 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.
>
> Cheers
> 	Florian
>
> -- 
>
> Home:
> http://www.in.tum.de/~haftmann
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev