On 08/26/2011 11:08 PM, Brian Huffman wrote:
On Fri, Aug 26, 2011 at 1:34 PM, Andreas Schropp<schr...@in.tum.de> wrote:
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.
As I understand it, the typedef in the above example will cause a
conditional axiom to be generated, something like this:
axiom type_definition_empty:
"False ==> type_definition Rep_empty Abs_empty {}"
As far as I can tell, this axiom doesn't force you to use the empty
set to denote type "empty" in your set-theoretic model. In fact, you
can use any set you want to denote type "empty", because the axiom
type_definition_empty doesn't assert anything about it at all!
So you suggest using e.g.
if EX x. x : A then A
else {0}
instead of A as the semantic interpretation?
Interesting!
- Brian
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
