*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] HOLCF equality*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Mon, 09 Jul 2012 18:14:10 +0900*In-reply-to*: <CAAMXsia+HxapVm_nR9040QGcWKbDJX8SWnaRjLvpPYqnj8YdmQ@mail.gmail.com>*References*: <4FF7B559.4010204@jaist.ac.jp> <CAAMXsia+HxapVm_nR9040QGcWKbDJX8SWnaRjLvpPYqnj8YdmQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:13.0) Gecko/20120615 Thunderbird/13.0.1

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 ;).

cheers chris

**Follow-Ups**:**Re: [isabelle] HOLCF equality***From:*Brian Huffman

**References**:**[isabelle] HOLCF equality***From:*Christian Sternagel

**Re: [isabelle] HOLCF equality***From:*Brian Huffman

- Previous by Date: Re: [isabelle] HOLCF equality
- Next by Date: Re: [isabelle] HOLCF equality
- Previous by Thread: Re: [isabelle] HOLCF equality
- Next by Thread: Re: [isabelle] HOLCF equality
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list