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



Dear Andreas,

thanks a lot for your response.

> Collecting the rewrite rules will not get you very far in general,
> because you need a relational approach to deal with that; think of
> something like
>
>    list_all2 equivalence (map ((+) x) xs) (map ((+) y) ys)
> 
> That’s why the transfer package uses a relation approach that is
> beyond the simplifier’s reach.

Well, in my use cases, premises and conclusions are always applications
of equivalence relations. I guess invoking those rewrite rules will work
for turning these applications of equivalence relations into equalities
on the quotient type. However, I’d still like to avoid this approach,
since it means too much manual work for my taste.

> Finally, the old quotient package by Cezary and Urban supports
> transferring in both directions (Section 11.9.4 in `isar-ref`:
> `quotient_definition` instead of `lift_definition`, methods `lifting`
> and `descending`).

I tried with the old quotient package, but it didn’t work for me.
Consider my example code adapted to the old package:

    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 .

    quotient_definition "abstract_plus :: [abstract, abstract] ⇒ abstract"
      is "(+) :: [nat, nat] ⇒ nat"
      using is_compatible_with_plus .

Now assume I have a goal `equivalence (a + b) (c + d)` and I want it to
be turned into the goal `abstract_plus x y = abstract_plus z u`. Neither
applying `lifting` nor applying `descending` does that: `lifting` leaves
the goal in place; `descending` just adds explicit universal
quantification of the variables via `⋀`. What am I doing wrong here?

All the best,
Wolfgang





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