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.