Re: [isabelle] Opposite of the `transfer` method

> I’m wondering how others reason with equivalence relations. Somehow I
> can’t imagine that a situation like mine is so rare; so I’d be
> surprised
> if there isn’t an approach to performing “equivalence reasoning”
> conveniently. Any hints?

Coq has a setoid rewrite engine, which might be what you want here?.
The idea is to rewrite wrt arbitrary preorders.

Up to my knowledge, such a thing has not yet been implemented in
Isabelle (though I'm collecting possible applications, as I might
implement such a thing sooner or later ;) )


> All the best,
> Wolfgang

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