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

      (((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? Thanks.


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.

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