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".
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
