[isabelle-dev] typedef

[Brian Huffman]

On Fri, Aug 26, 2011 at 2:02 PM, Andreas Schropp <schropp at 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