Re: [isabelle] Transfer rule for transfer_forall
On 03/12/2013 11:53 AM, Andreas Lochbihler wrote:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and