equal
deleted
inserted
replaced
88 assumes q1: "Quotient R1 Abs1 Rep1" |
88 assumes q1: "Quotient R1 Abs1 Rep1" |
89 assumes q2: "Quotient R2 Abs2 Rep2" |
89 assumes q2: "Quotient R2 Abs2 Rep2" |
90 shows "Abs2 (snd ((prod_fun Rep1 Rep2) p)) = snd p" |
90 shows "Abs2 (snd ((prod_fun Rep1 Rep2) p)) = snd p" |
91 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2]) |
91 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2]) |
92 |
92 |
|
93 lemma prod_fun_id[id_simps]: "prod_fun id id \<equiv> id" |
|
94 by (rule eq_reflection) (simp add: prod_fun_def) |
93 |
95 |
94 section {* general setup for products *} |
96 section {* general setup for products *} |
95 |
97 |
96 declare [[map * = (prod_fun, prod_rel)]] |
98 declare [[map * = (prod_fun, prod_rel)]] |
97 |
99 |