[isabelle-dev] typedef

[Andreas Schropp]

On 08/26/2011 11:08 PM, Makarius wrote:
> 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.

The thing is: in traditional HOL we always have non-empty type 
constructor interpretations,
and the whole meta-theory is based on that fact: the type universe 
contains only non-empty sets.
So this is not some minor change as you suggest.

>
> This does not mean there is no other way.

What do you mean?
If we can have type constructors which are semantically the empty set
under assumption False, how can we get around using False
to forge the traditional meta-theory results?

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

Stuck somewhere in a porting effort I guess. ;>
If you are interested I will bring it up to date in the near future.

>
>     Makarius