Re: [isabelle] HOLCF equality
On 07/09/2012 05:45 PM, Brian Huffman wrote:
On Sat, Jul 7, 2012 at 6:04 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
is there already something like Haskell's "Eq" typeclass for HOLCF (which
seems to be neccessariy/convenient to formalize typical Haskell functions).
If not, are there any other reasons than lack of time?
A library with class "Eq" and other classes from Haskell would
certainly be useful, and I don't think it would take much time to
I think the main reason I never implemented it is I could never decide
on the details: what to name the functions, what syntax to provide,
what axioms to use, which classes to provide, etc.
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 ;).
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 archive was generated by a fusion of
Pipermail (Mailman edition) and