Re: [isabelle] HOLCF equality



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

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".)
Thanks for pointing this out. As I said, I did not think much about the details yet (and my only instance of "eq" was "lift").

Alternatively, a subclass "eq_flat" with the strong eq_iff rules might
be useful alongside a weakened "eq" class.
That sounds reasonable.

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.)
I would suggest to start with a sourceforge project (or anything equivalent) until there actually is something constituting a "standard library" which can then be submitted to the AFP (or the distribution).

- chris





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