[isabelle-dev] typedef

[Makarius]

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

Whatever is done in Isabelle with sort constraints and the above 
conditional typedefs should be an instance of the loose type 
specifications according to A. Pitts in the HOL book from 1993.


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


 	Makarius