# Re: [isabelle] Transfer rule for transfer_forall

```On 03/11/2013 01:54 PM, Ondřej Kunčar wrote:
```
```On 03/11/2013 12:22 PM, Andreas Lochbihler wrote:
```
```Dear all,

I am trying to replace the quotient package (by Cezary and Urban) with
lifting and transfer for the theory TLList in AFP-Coinductive. When I
invoke transfer on the new coinduction rule for tllist_all2 (see below),
the second subgoal is

"Transfer.Rel
(((cr_tllist ===> cr_tllist ===> op =) ===> op =) ===> op =) ?a76
transfer_forall"

and the first one is cluttered with transfer_forall and
what ?a76 should be? I hope that there's a canonical solution. I can
also try to produce a smaller example but have failed so far.

lemma tllist_all2_coinduct:
assumes "X xs ys"
and "!!xs ys. X xs ys ==>
(is_TNil xs = is_TNil ys) &
(is_TNil xs --> is_TNil ys --> R (terminal xs) (terminal ys)) &
(~ is_TNil xs --> ~ is_TNil ys
--> P (thd xs) (thd ys) &
(X (ttl xs) (ttl ys) | tllist_all2 P R (ttl xs) (ttl ys)))"
shows "tllist_all2 P R xs ys"
using assms
apply transfer

Some more data on the setup:

definition cr_tllist :: "('a llist * 'b) => ('a, 'b) tllist => bool"
where "cr_tllist = (%(xs, b) ys. tllist_of_llist b xs = ys)"

lemma Quotient_tllist:
"Quotient (%(xs, a) (ys, b). xs = ys & (lfinite ys --> a = b))
(%(xs, a). tllist_of_llist a xs)
(%ys. (llist_of_tllist ys, terminal ys))
cr_tllist"

lemma reflp_tllist:
"reflp (%(xs, a) (ys, b). xs = ys & (lfinite ys --> a = b))"

setup_lifting (no_code) Quotient_tllist reflp_tllist

Thanks in advance for any pointers,
Andreas
```
```

I'll take a look at it. Could please send me a self-contained file? Thanks.

Ondrej
```
```
```
OK. The rule you are looking for already exists. It's called Domainp_forall_transfer:
```  assumes "right_total A"
shows "((A ===> op =) ===> op =)
(transfer_bforall (Domainp A)) transfer_forall"

```
But the transfer method has to be able to prove that A is right_total, which didn't happen in your case. The reason is that you didn't prove these properties about your relator llist_all2:
```lemma[transfer_rule]: "right_total A ==> right_total (llist_all2 A)" sorry
lemma[transfer_rule]: "right_unique A ==> right_unique (llist_all2 A)" sorry

You were already warned in the setup_lifting:
```
Non-trivial assumptions in right_unique transfer rule found: right_unique (llist_all2 ?T5). Non-trivial assumptions in right_total transfer rule found: right_total (llist_all2 ?T5).
```
```
This error message comes from a big patch of Lifitng, which I pushed on Friday, so there is not any documentation to it yet (explaining what to do in this situation). That's an disadvantage of the development version.
```
```
In general, you might want to take a look to HOL/Library/Quotient_List.thy and get an inspiration what should be proved about your "list" type.
```
Hope this helps.
Ondrej

```

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