On Fri, Aug 26, 2011 at 2:02 PM, Andreas Schropp <schr...@in.tum.de> wrote:
>
> So you suggest using e.g.
> if EX x. x : A then A
> else {0}
> instead of A as the semantic interpretation?
> Interesting!
Yes, this is exactly the kind of thing I meant. You could use any
nonempty set you want in place of {0}, of course.
Conditional type definition axioms remind me a lot of
partially-specified functions. For example, the defining axiom for
"THE" doesn't specify what "THE n::nat. False" is equal to, but we do
know that "THE n::nat. False" is equal to *something* of type nat.
Likewise, the axiom "False ==> type_definition Rep_empty Abs_empty {}"
doesn't specify what kind of set can model type "empty", but we do
know that type "empty" must be *some* nonempty set.
- Brian
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
