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



Am Mittwoch, den 03.07.2019, 23:03 +0300 schrieb Wolfgang Jeltsch:
> 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_equivalence:
>         "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

One step in the right direction might be to invoke the simplifier using
equations auto-generated by `quotient_type` and `lift_definition`, like
so:

    lemma "equivalence (a + b) (c + d)"
    proof (simp only: abstract.abs_eq_iff [THEN sym] abstract_plus.abs_eq [THEN sym])
      ― ‹yields \<^term>‹abstract_plus (abs_abstract a) (abs_abstract b) = abstract_plus (abs_abstract c) (abs_abstract d)››
      oops

However, I wouldn’t like to specify the rewrite rules manually like in
this code snippet. Is there a way to automatically gather all
`abs_eq_iff` and `abs_eq` rules or perhaps only those that are related
to the equivalence relation used in the goal?

All the best,
Wolfgang





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