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.