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