[isabelle-dev] typedef

[Florian Haftmann]

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

IMHO {default} is even the more suitable choice, although it makes no
substantial difference.

Btw. there is often the situation that, given an Abs :: b => a for a
"new" type "a", the user defines a constructor C which then is "total",
e.g. for rats:

  Rat k l := (if l = 0 then Abs_rat 0 1 else Abs_rat k l)

or for dlists:

  Dlist xs := Abs_dlist (remdups xs)

This saves some case distinctions in trivial cases.  I have called this
"totalisation".

> You surely know this HOL joke in some form or the other:
> 
>   "if default = undefined then SOME x. True else SOME x. False"

The original formulation also involved "arbitrary", which we have
managed to get rid of finally, but you can still permute the values in
the term above in an arbitrary order.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110830/7d180939/attachment.sig>