*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Opposite of the `transfer` method*From*: Wolfgang Jeltsch <wolfgang-it at jeltsch.info>*Date*: Thu, 04 Jul 2019 19:12:25 +0300*In-reply-to*: <418274F9-C70D-4208-948C-00B27F15070B@uibk.ac.at>*References*: <7a02be06e80cee6cb48222288464a47f4662f189.camel@jeltsch.info> <418274F9-C70D-4208-948C-00B27F15070B@uibk.ac.at>

Am Donnerstag, den 04.07.2019, 06:28 +0000 schrieb Thiemann, René: > Hi Wolfgang, > > I’m unsure whether there is a proof method, however there is the > “untransferred” attribute that works in the opposite direction. So > also transfer is to a certain extend bidirectional. > > > lemma "equivalence (a + b) (c + d)" > proof - > have "abstract_plus a b = abstract_plus c d" for a b c d sorry > from this[untransferred] show ?thesis . > qed > > Perhaps this solves your goal. Hi, René! Thanks a lot for your response. Technically, your solution would work. However, it would mean that the user would have to add a considerable amount of boilerplate, because stating the equations on the quotient types is necessary. Maybe I should explain a bit more the background of my question. I’m working with a process calculus. I have an algebraic data type `process` of processes (or rather process terms) and several bisimilarity relations, which describe different notions of behavioral equivalence. Most of the proofs I’m conducting are proofs of bisimilarities, proving goals of the form `p ∼ q` where `p` and `q` are processes and `(∼)` is one of the bisimilarity relations. In many of these proofs, I’m using calculational reasoning, exploiting the fact that `(∼)` is transitive. There are certain core facts about the bisimilarity relations that state things like transitivity and commutativity of certain process operators modulo bisimilarity, things like `(p ∥ q) ∥ r ∼ p ∥ (q ∥ r)` and `p ∥ q ∼ q ∥ p`. Having to apply these facts manually in the proofs is really painful. My goal is to have a proof method that applies such technical facts as rewrite rules, analogously to what the simplifier does with equations. For example, in a proof I might have something like the following: from "p ∼ q ∥ r" have "p ∥ q ∼ r ∥ (q ∥ q)" sorry I’d like to replace the `sorry` with something as simple as `by simp`. While your approach would work, it would mean I had to add a quotient type version of every single proof step. Of course, it would be an option to translate the overall bisimilarity goal of each proof into a goal about quotient type equations and then reason in the quotient type throughout the proof. However, this would feel quite unnatural to me. The main reason is that there’s not a single best bisimilarity but there are multiple ones; so I would have to work with several quotient types and convert back and forth between them. I was considering using quotient types only internally as a means to make the simplifier reason with arbitrary equivalences. The basic idea is to translate both the goal and the rewrite rules (like `p ∥ q ∼ q ∥ p`) into statements that use equality on quotient types and then employ the simplifier to solve the new goals entirely. 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? All the best, Wolfgang

**Follow-Ups**:**Re: [isabelle] Opposite of the `transfer` method***From:*Peter Lammich

**References**:**[isabelle] Opposite of the `transfer` method***From:*Wolfgang Jeltsch

**Re: [isabelle] Opposite of the `transfer` method***From:*Thiemann, René

- Previous by Date: Re: [isabelle] Opposite of the `transfer` method
- Next by Date: Re: [isabelle] Opposite of the `transfer` method
- Previous by Thread: Re: [isabelle] Opposite of the `transfer` method
- Next by Thread: Re: [isabelle] Opposite of the `transfer` method
- Cl-isabelle-users July 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list