equal
deleted
inserted
replaced
68 subsection {* Quotient theorem for the Lifting package *} |
68 subsection {* Quotient theorem for the Lifting package *} |
69 |
69 |
70 lemma Quotient_prod[quot_map]: |
70 lemma Quotient_prod[quot_map]: |
71 assumes "Quotient R1 Abs1 Rep1 T1" |
71 assumes "Quotient R1 Abs1 Rep1 T1" |
72 assumes "Quotient R2 Abs2 Rep2 T2" |
72 assumes "Quotient R2 Abs2 Rep2 T2" |
73 shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) |
73 shows "Quotient (prod_rel R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2) (prod_rel T1 T2)" |
74 (map_pair Rep1 Rep2) (prod_rel T1 T2)" |
|
75 using assms unfolding Quotient_alt_def by auto |
74 using assms unfolding Quotient_alt_def by auto |
76 |
75 |
77 subsection {* Transfer rules for the Transfer package *} |
76 subsection {* Transfer rules for the Transfer package *} |
78 |
77 |
79 context |
78 context |
95 |
94 |
96 lemma curry_transfer [transfer_rule]: |
95 lemma curry_transfer [transfer_rule]: |
97 "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry" |
96 "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry" |
98 unfolding curry_def by transfer_prover |
97 unfolding curry_def by transfer_prover |
99 |
98 |
100 lemma map_pair_transfer [transfer_rule]: |
99 lemma map_prod_transfer [transfer_rule]: |
101 "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D) |
100 "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D) |
102 map_pair map_pair" |
101 map_prod map_prod" |
103 unfolding map_pair_def [abs_def] by transfer_prover |
102 unfolding map_prod_def [abs_def] by transfer_prover |
104 |
103 |
105 lemma prod_rel_transfer [transfer_rule]: |
104 lemma prod_rel_transfer [transfer_rule]: |
106 "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> |
105 "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> |
107 prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel" |
106 prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel" |
108 unfolding fun_rel_def by auto |
107 unfolding fun_rel_def by auto |