# 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.