[isabelle] Opposite of the `transfer` method
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
"⟦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"
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"
― ‹yields \<^term>‹⋀a b c d. equivalence (a + b) (c + d)››
However, it does not perform the opposite conversion:
lemma "equivalence (a + b) (c + d)"
― ‹also yields \<^term>‹⋀a b c d. equivalence (a + b) (c + d)››
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and