Re: [isabelle] Transfer rule for transfer_forall



On 03/12/2013 11:53 AM, Andreas Lochbihler wrote:
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?

Yes, it is meant that way. We don't have any proper left_total relations thus this rule is not registered as a transfer rule: all correspondence relations for quotients (or subtypes) are at least right_total and right_unique. It might happen that somebody in future will try to use transfer with proper left_total and left_unique relations but nobody has come up with an example so far.

But this rule is used to prove that assumptions of abstraction function equations (f.abs_eq generated by lift_definition) holds (i.e., R x x holds). It's namely used when you have to prove that a composition of quotients yields a reflexive relation; then you have to prove that the outer relation is left_total. See the theorem reflp_Quotient_composition.

Ondrej





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