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