I have ran into `uprod`

- quotient type, something I have no practical experience with. If I understand correctly, the lifting and transfer tools are important facilities for working with quotients, so I'd like to learn something about them. However, I can't seem to find any introductory documentation on them. Looking through the documentation page, I've only been able to find a dry description in isar-ref, with no examples. Is there any more introductory material?

There is `src/HOL/ex/Transfer_Int_Nat.thy`

Hmm, I guess that helps somewhat. Though, I still don't see how I could prove something simple like

```
lift_definition pair_content :: "'a uprod ⇒ 'a multiset" is
"λ(a, b). {# a, b #}" by auto
lemma "pair_content (Upair a b) = {# a, b #}"
```

I've managed to prove this with `by (simp add: Upair.abs_eq pair_content.abs_eq)`

, is that the canonical approach, or am I going about this in a round-about way?

No, it the idiomatic way would be something like `by transfer auto`

, but it doesn't. I don't really understand why it doesn't work, but I never had a very good understanding of the `transfer`

package.

The transfer method leaves some schematic variables in the goals in this case. Is that normal, or could that be the problem?

No, this normally happens when there's a missing transfer rule.

And the first goal tells you what constant the rule is missing for.

But sometimes I don't understand why it happens, and this is one of these cases.

Sometimes `transfer'`

does the trick in those cases, bot not here. I'm not even sure what `transfer'`

does. Ondřej Kunčar told me it's bad and that I shouldn't use it.

Hmm, I think it's trying to transfer through both uprod and multiset?

That might be the problem, yes. I never really understood how to get around that.

Maybe ask on the mailing list. I think the probability that someone knowledgeable on lifting and transfer will reply is higher there.

If you haven't seen it already, there is also a file `HOL/ex/Transfer_Debug.thy`

that goes through same cases where `transfer`

fails and how to debug. (I have to add that I didn't find the file too illuminating)

Yes, I've just noticed. I managed to craft the following proof with that method:

```
declare Upair_parametric[transfer_rule del]
lemma [simp]: "pair_content (Upair a b) = {# a, b #}"
apply transfer_start
apply (rule Rel_eq_refl)
apply transfer_step+
apply transfer_end
by simp
```

oh, actually, this works:

```
declare Upair_parametric[transfer_rule del] zero_multiset.transfer[transfer_rule del]
lemma [simp]: "pair_content (Upair a b) = {# a, b #}"
by transfer simp
```

What theories did you import? For me, it works without the `declare`

.

(On the development version of Isabelle and Isabelle2020)

Oh, so apparently `apply transfer by simp`

doesn't work and `by transfer simp`

does...

Yes, `by transfer simp`

does backtracking.

The other one does not.

Beware though: `transfer`

can cause excessive backtracking sometimes.

Last updated: Sep 25 2022 at 23:25 UTC