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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
