Re: [isabelle] Countable type: stream



Dear Roger,

> thank you Rene and Andreas for the help with the countable datatype, it works for a random type color.
> 
> Now my last problem is to show that the datatype  --- 'a stream --- is countable.
> 
> Stream is a package in the FOCUS library and is smth defined with the HOLCF  "domain" construct and resembles
> 
> the lists in Haskell. To show now:
> 
> 
> instance stream :: (countable) countable
> by.... ?
> 
> can you help me?

It definitely is not possible using the tactic mentioned by Andreas (which is based on
how "datatype"s are constructed by the datatype-package) and thus, also not by the wrapper
that makes use of this tactic in the "deriving" package.

So far I have never worked with HOLCF, but I just wondered whether you are sure that 
stream really is countable: If it can model infinite lists (Haskell lists), then most 
likely the set of all "bool stream"s already can encode the real interval [0,1] which is 
uncountable.

Best regards,
René
-- 
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.