Re: [isabelle] HOLCF equality
On 07/09/2012 10:04 PM, Brian Huffman wrote:
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").
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.
That sounds reasonable.
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).
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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and