*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] HOLCF equality*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Tue, 10 Jul 2012 14:21:24 +0900*In-reply-to*: <CAAMXsiZQjMH74qEMb0Xn4sNPxr1L3Ho3U9H=t5uPfvh_rb-aeQ@mail.gmail.com>*References*: <4FF7B559.4010204@jaist.ac.jp> <CAAMXsia+HxapVm_nR9040QGcWKbDJX8SWnaRjLvpPYqnj8YdmQ@mail.gmail.com> <4FFAA0E2.3090006@jaist.ac.jp> <CAAMXsiZQjMH74qEMb0Xn4sNPxr1L3Ho3U9H=t5uPfvh_rb-aeQ@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 10:04 PM, Brian Huffman wrote:

On Mon, Jul 9, 2012 at 11:14 AM, Christian Sternagel <c-sterna at jaist.ac.jp> wrote: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 ;).

{-# RULES

"filterList" [1] forall p. foldr (filterFB (:) p) [] = filter p

#-}

-- filterFB (filterFB c p) q a b -- = if q a then filterFB c p a b else b -- = if q a then (if p a then c a b else b) else b -- = if q a && p a then c a b else b -- = filterFB c (\x -> q x && p x) a b -- I originally wrote (\x -> p x && q x), which is wrong, and actually -- gave rise to a live bug report. SLPJ.

chris

I think your eq_iff rules need to be weakened like this: "eq⋅x⋅y = TT ==> x = y" "eq⋅x⋅y = FF ==> x ≠ y" Otherwise instances for lazy lists or other lazy datatypes are not possible. (Your class "eq" is provably a subclass of "flat".) Alternatively, a subclass "eq_flat" with the strong eq_iff rules might be useful alongside a weakened "eq" class.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.)This sounds like a good idea. The question is where to put it. We could add a theory file under HOLCF in the distribution, or we could add an AFP entry for this purpose. (Maybe using the distribution is better; as an "archive", the AFP seems not to be intended so much for dynamic, growing works with open authorship.) - Brian

**Follow-Ups**:**Re: [isabelle] HOLCF equality type class***From:*Christian Sternagel

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

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

**Re: [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] I want to print axiomatization info
- Previous by Thread: Re: [isabelle] HOLCF equality
- Next by Thread: Re: [isabelle] HOLCF equality type class
- 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