[isabelle-dev] HOLCF lists

[Christian Sternagel]

On 07/17/2012 07:53 PM, Brian Huffman wrote:
>> 2) I think at some point something like "set :: 'a list => 'a set" for HOLCF
>> lists would be useful...
>
> What for? Is it meant to be an abstraction of some kind of executable
> function, or is it only useful for writing logical specifications?
Only for specification. Thus, I'll use an inductive definition.

>> 4) How to nicely integrate natural numbers? I don't really want to mix =>
>> and ->, e.g., the "list"-function "take" should have type "nat lift -> 'a
>> list -> 'a list" (or something similar), rather than "nat => 'a list -> 'a
>> list" I guess.
>
> HOLCF/Library/{Nat,Int}_Discrete.thy define cpo instances for types
> nat and int, so you can write types like "nat -> 'a list" or
> "nat\<^sub>\<bottom> -> 'a list". Decisions about which types to use
> should probably follow Haskell: "Integer" should be modeled as
> "int\<^sub>\<bottom>" or "int lift", and for unboxed Haskell types
> (e.g. Int#) you can use "int".
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 ;).

class eq =
   fixes eq :: "'a::pcpo → 'a → tr"
   assumes equals_strict [simp]:
     "eq⋅x⋅⊥ = ⊥" "eq⋅⊥⋅y = ⊥"
     and eq_simps [dest]:
     "eq⋅x⋅y = TT ⟹ x = y"
     "eq⋅x⋅y = FF ⟹ x ≠ y"

Btw: any more thoughts on actually putting code into some publicly 
available destination (bitbucket, sourceforge, ...)?

cheers

chris