[isabelle-dev] HOLCF lists
Christian Sternagel
c-sterna at jaist.ac.jp
Wed Jul 18 08:52:58 CEST 2012
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
More information about the isabelle-dev
mailing list