equal
deleted
inserted
replaced
91 (map_pair Rep1 Rep2) (prod_rel T1 T2)" |
91 (map_pair Rep1 Rep2) (prod_rel T1 T2)" |
92 using assms unfolding Quotient_alt_def by auto |
92 using assms unfolding Quotient_alt_def by auto |
93 |
93 |
94 declare [[map prod = (prod_rel, Quotient_prod)]] |
94 declare [[map prod = (prod_rel, Quotient_prod)]] |
95 |
95 |
|
96 definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
|
97 where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)" |
|
98 |
|
99 lemma prod_invariant_commute [invariant_commute]: |
|
100 "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)" |
|
101 apply (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) |
|
102 apply blast |
|
103 done |
|
104 |
96 subsection {* Rules for quotient package *} |
105 subsection {* Rules for quotient package *} |
97 |
106 |
98 lemma prod_quotient [quot_thm]: |
107 lemma prod_quotient [quot_thm]: |
99 assumes "Quotient3 R1 Abs1 Rep1" |
108 assumes "Quotient3 R1 Abs1 Rep1" |
100 assumes "Quotient3 R2 Abs2 Rep2" |
109 assumes "Quotient3 R2 Abs2 Rep2" |