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

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

Best,
René

> Am 03.07.2019 um 22:03 schrieb Wolfgang Jeltsch <wolfgang-it at jeltsch.info>:
>
> Hi!
>
> I’m looking for a proof method that is like `transfer` but transforms
> into the opposite direction.
>
> Consider, for example, the following code:
>
>    axiomatization equivalence :: "[nat, nat] ⇒ bool" where
>      is_equi
> valence:
>        "equivp equivalence"
>    and
>      is_compatible_with_plus
> :
>        "⟦equivalence n n'; equivalence m m'⟧ ⟹
>        equivalence (n +
> m) (n' + m')"
>
>    quotient_type abstract = nat / equivalence
>      using is_equivalence .
>
>    lift_definition abstract_plus :: "[abstract, abstract] ⇒ abstract"
>      is "(+)"
>      using is_compatible_with_plus .
>
> The `transfer` method can replace equalities of `abstract` values by
> equivalences of `nat` values:
>
>    lemma "abstract_plus a b = abstract_plus c d"
>    proof transfer
>      ― ‹yields \<^term>‹⋀a b c d. equivalence (a + b) (c + d)››
>      oops
>
> However, it does not perform the opposite conversion:
>
>    lemma "equivalence (a + b) (c + d)"
>    proof transfer
>      ― ‹also yields \<^term>‹⋀a b c d. equivalence (a + b) (c + d)››
>      oops
>
> Is there a proof method that replaces equivalences by equalities on a
> corresponding quotient type? I know that there’s the `transferred`
> attribute, but this works only for facts, not for goals.
>
> The background of my question is that I’d like to employ the simplifier
> for reasoning with arbitrary equivalences. The idea is to reduce a goal
> that states an equivalence to a goal that states a corresponding
> equality on a quotient type and then let the simplifier do equational
> reasoning in that quotient type.
>
> All the best,
> Wolfgang
>
>

```

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