Re: [isabelle] Opposite of the `transfer` method
Am Donnerstag, den 04.07.2019, 17:26 +0100 schrieb Peter Lammich:
> > 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?
Well, I’d want something like that for Isabelle. 😉
I have a considerable amount of Isabelle code, which I wouldn’t like to
translate to Coq, for three reasons:
* The translation would take a lot of time.
* The translation would perhaps not be straightforward because of
* Coq doesn’t have a proper proof language along the lines of Isar.
> 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 😉).
Please implement it! 🙏
All the best,
This archive was generated by a fusion of
Pipermail (Mailman edition) and