makarius at sketis.net
Fri Aug 26 22:51:16 CEST 2011
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
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
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.
More information about the isabelle-dev