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:
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.
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"
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)"
"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))
"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
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
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