On 08/30/2011 08:12 PM, Brian Huffman wrote:
On Fri, Aug 26, 2011 at 1:34 PM, Andreas Schropp<schr...@in.tum.de> wrote:
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.
Andreas,
How would your HOL->ZF translation handle the following typedef?
Its been a while, I don't remember the exact details,
but type classes are a global concept, so this is quite
different from the complications via local typedefs.
Think: type constructor well-formedness arguments
via type classes can stay global.
Non-Emptiness-Proofs are still global in this case
because instances are global.
If I am not mistaken I don't have to do anything
to treat typedefs with type class constraints:
due to our efforts back then, type class reasoning
is eliminated directly in the kernel.
class infinite = assumes infinite_UNIV: "~ finite UNIV"
typedef 'a infset = "{A::('a::infinite) set. ~ finite A}"
using infinite_UNIV [where 'a='a] by fast
This example does not rely on locales at all. It doesn't rely on any
overloaded constants either, not even indirectly.
However, the nonemptiness proof does rely on type class assumptions:
Indeed, "{A. ~ finite A}" is actually empty for any finite type 'a.
So it seems to me that this problem you describe where "the semantic
interpretation of [a type] is the empty set" predates the localization
of typedef.
The question is not so much about typedef semantics IMO (but it can be
resolved
this way), but more about the status of globality/localness of
non-emptiness proofs
demanded by the typedef principle.
Of course the empty set could always be written down there, but whether this
"justified" globally or locally is more interesting ...
- Brian
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
