[isabelle-dev] typedef

[Andreas Schropp]

On 08/26/2011 10:51 PM, Makarius wrote:
> On Fri, 26 Aug 2011, Andreas Schropp wrote:
>
>> On 08/26/2011 07:08 PM, Brian Huffman wrote:
>>> As far as I understand, the typedef package merely issues global
>>> axioms of the form "type_definition Rep Abs S", as long as it is
>>> provided with a proof of "EX x. x : S".
>>>
>>
>> The global axiom is
>>
>>  EX x. x : A ==> type_definition Rep Abs A
>>
>> allowing local typedefs whenever non-emptiness of A is
>> derivable, even using assumptions in the context.
>
> Yes, this is the key point.  By digging further in the Mercurial 
> history, you will see when I actually introduced it -- way before the 
> "localized" typedef.  (I am not digging myself, because I am not 
> participating in this strange game of the seasion to generate workload 
> by changing long-standing things arbitrarily.)

You did not change the global axiom, but before local typedefs
the non-emptiness proofs were global.

>
>> 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 = {}

Now I have to put up with the fact the semantic interpretation of empty is
the empty set. Formerly only non-empty sets were semantic interpretations of
type constructors. The way around this is to localize derivations related to
type constructor well-formedness, using False to forge all those crazy 
things.