[isabelle] Transfer rule for transfer_forall



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 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))
     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




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