[isabelle-dev] HOLCF lists

[Christian Sternagel]

On 07/18/2012 05:45 PM, Brian Huffman wrote:
>> Sorry for asking stupid questions (since I am to lazy to look it up myself):
>> what's the difference between "'a lift" and "'a u" exactly? Is either of
>> them preferable to model "Haskell-Integers"? I tried to instantiate "'a u"
>> for my eq-class, but failed due to sort problems, since I'm not that
>> familiar with the type class hierarchy of HOLCF, maybe you could save me
>> some time ;).
>
> Type "'a u" or "'a\<^sub>\<bottom>" requires its argument to have
> class "cpo". The ordering on "'a u" is the same as 'a, but with a new
> bottom element.
>
> Type 'a lift only requires its argument to have class "type"; the
> ordering is always a flat pcpo. It is intended for use with HOL types
> without cpo instances.
>
> If 'a is a cpo with a discrete ordering, then 'a u and 'a lift are
> isomorphic. However, I consider it a bad practice to use "lift" with
> any type that actually has a cpo instance.
>
> For modeling Haskell integers, I would suggest using "nat lift", "int
> lift", etc. if you are not using the {Nat,Int}_Discrete libraries, but
> if you are, I would prefer using "nat u" or "int u".
Thanks for the explanation. So "int u" it is.
>
>> Btw: any more thoughts on actually putting code into some publicly available
>> destination (bitbucket, sourceforge, ...)?
>
> If you want to set up a bitbucket or sourceforge repo for this
> purpose, that would be great. I'd be happy to contribute to something
> like that.
I created a repository at

http://sourceforge.net/p/holcf-prelude/

I chose sourceforge since I could reuse my AFP related account (which 
should be true for many others). Please let me know when I should add 
you as Admin/Developer.

cheers

chris

PS: in the repo, "elem" is still based on the eq-class variant which I 
could not instantiate for "'a u"... It would be great if somebody could 
change "class eq" such that "'a u" becomes an instance.

PPS: As I mentioned in an earlier mail. I would like to add a constant 
"set :: 'a Data_List.list => 'a set" for specification purposes. I don't 
see how this is possible as inductive_set. Any hints?

The reason why I think I need this function is that I want to prove

   filter$P$(filter$Q$xs) = filter$Q$(filter$P$xs)

which is not true unconditionally due to strictness issues. I thought 
that using "set" I could formulate appropriate assumptions, such that 
the above equation holds, e.g., "ALL x : set xs. P x andalso Q x = Q x 
andalso P x".