equal
deleted
inserted
replaced
143 done |
143 done |
144 |
144 |
145 lemma quotient_compose_list_gen_pre: |
145 lemma quotient_compose_list_gen_pre: |
146 assumes a: "equivp r2" |
146 assumes a: "equivp r2" |
147 and b: "Quotient r2 abs2 rep2" |
147 and b: "Quotient r2 abs2 rep2" |
148 shows "(list_rel r2 OO op \<approx>1 OO list_rel r2) r s = |
148 shows "(list_rel r2 OOO op \<approx>1) r s = |
149 ((list_rel r2 OO op \<approx>1 OO list_rel r2) r r \<and> |
149 ((list_rel r2 OOO op \<approx>1) r r \<and> (list_rel r2 OOO op \<approx>1) s s \<and> |
150 (list_rel r2 OO op \<approx>1 OO list_rel r2) s s \<and> |
|
151 abs_fset (map abs2 r) = abs_fset (map abs2 s))" |
150 abs_fset (map abs2 r) = abs_fset (map abs2 s))" |
152 apply rule |
151 apply rule |
153 apply rule |
152 apply rule |
154 apply rule |
153 apply rule |
155 apply (rule list_rel_refl) |
154 apply (rule list_rel_refl) |
197 done |
196 done |
198 |
197 |
199 lemma quotient_compose_list_gen: |
198 lemma quotient_compose_list_gen: |
200 assumes a: "Quotient r2 abs2 rep2" |
199 assumes a: "Quotient r2 abs2 rep2" |
201 and b: "equivp r2" (* reflp is not enough *) |
200 and b: "equivp r2" (* reflp is not enough *) |
202 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) |
201 shows "Quotient ((list_rel r2) OOO (op \<approx>1)) |
203 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
202 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
204 unfolding Quotient_def comp_def |
203 unfolding Quotient_def comp_def |
205 apply (rule)+ |
204 apply (rule)+ |
206 apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset]) |
205 apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset]) |
207 apply (rule) |
206 apply (rule) |
221 (* This is the general statement but the types of abs2 and rep2 |
220 (* This is the general statement but the types of abs2 and rep2 |
222 are wrong as can be seen in following exanples *) |
221 are wrong as can be seen in following exanples *) |
223 lemma quotient_compose_general: |
222 lemma quotient_compose_general: |
224 assumes a2: "Quotient r1 abs1 rep1" |
223 assumes a2: "Quotient r1 abs1 rep1" |
225 and "Quotient r2 abs2 rep2" |
224 and "Quotient r2 abs2 rep2" |
226 shows "Quotient ((list_rel r2) OO r1 OO (list_rel r2)) |
225 shows "Quotient ((list_rel r2) OOO r1) |
227 (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)" |
226 (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)" |
228 sorry |
227 sorry |
229 |
228 |
230 thm quotient_compose_list_gen[OF Quotient_fset fset_equivp] |
229 thm quotient_compose_list_gen[OF Quotient_fset fset_equivp] |
231 thm quotient_compose_general[OF Quotient_fset] |
230 thm quotient_compose_general[OF Quotient_fset] |