Re: [isabelle] Transfer rule for transfer_forall

Dear Ondřej,

Thanks a lot for looking into this. It now works fine.
But I still don't understand what all these attributes do. In Library/Quotient_List, e.g., list_left_total is declared as reflexivity_rule, but list_right_total as transfer_rule. Is that meant to be that way?


On 11/03/13 22:46, Ondřej Kunčar wrote:
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

      (((cr_tllist ===> cr_tllist ===> op =) ===> op =) ===> op =) ?a76

and the first one is cluttered with transfer_forall and
transfer_implies. Can anyone knowledgable please help me in figuring out
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))

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,

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


OK. The rule you are looking for already exists. It's called
   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)"

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.

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