[isabelle-dev] typedef

[Makarius]

On Fri, 26 Aug 2011, Brian Huffman wrote:

> 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.

How about {undefined}, or similar?

You surely know this HOL joke in some form or the other:

   "if default = undefined then SOME x. True else SOME x. False"

(Attributed to F. Haftmann?)


 	Makarius