Re: [isabelle] HOLCF equality



On 07/09/2012 05:45 PM, Brian Huffman wrote:
On Sat, Jul 7, 2012 at 6:04 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
Dear all,

is there already something like Haskell's "Eq" typeclass for HOLCF (which
seems to be neccessariy/convenient to formalize typical Haskell functions).
If not, are there any other reasons than lack of time?

A library with class "Eq" and other classes from Haskell would
certainly be useful, and I don't think it would take much time to
implement.

I think the main reason I never implemented it is I could never decide
on the details: what to name the functions, what syntax to provide,
what axioms to use, which classes to provide, etc.

- Brian

I am currently using

class eq =
  fixes eq :: "'a::pcpo → 'a → tr"
  assumes equals_strict [simp]:
    "eq⋅x⋅⊥ = ⊥" "eq⋅⊥⋅y = ⊥"
    and eq_iff [iff]:
    "eq⋅x⋅y = TT ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x = y"
    "eq⋅x⋅y = FF ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x ≠ y"
    "eq⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"

but did not think much about the details ;).

Maybe something like a theory for standard Haskell functions could be placed where everybody can browse and contribute? (I am currently mainly defining very basic list functions and proving basic properties about them.)

cheers

chris






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.