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

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

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

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,

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