# Re: [isabelle] HOLCF equality

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

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