[isabelle] Opposite of the `transfer` method



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.