[isabelle-dev] typedef

[Makarius]

On Fri, 26 Aug 2011, Andreas Schropp wrote:

>>> This is not really a problem, but complicates my conservativity argument. 
>>> Before local typedefs the proof of (EX x. x : A) was global. Actually 
>>> Makarius' attitude on this was that those non-emptiness proofs "should be 
>>> global most of the time", but he didn't want to introduce a check.
>> 
>> I don't understand this.  Local typedefs are just a conjuring trick around 
>> plain old global ones (in the above presentation) -- no changes of the 
>> logical foundations here.
>
> Formerly the non-emptiness proof was global, now its local!
>
> locale bla =
>  assume "False"
>  typedef empty = {}

Yes, I now remember our state of discussion quite some time ago.  It is 
part of the conjuring to make it a bit unconstructive, but it still 
follows the original spirit of Gordon/Pitts HOL typedefs as I've 
understood them many years ago.

This does not mean there is no other way.  Back then we just did not get 
to the point where I had your translation running concretely, so it was 
not continued.  Where is your translation tool suite now?  What is its 
state concerning current Isabelle versions?


 	Makarius