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