equal
deleted
inserted
replaced
270 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp a b) |
270 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp a b) |
271 done |
271 done |
272 |
272 |
273 lemma quotient_compose_list_gen: |
273 lemma quotient_compose_list_gen: |
274 assumes a: "Quotient r2 abs2 rep2" |
274 assumes a: "Quotient r2 abs2 rep2" |
275 and b: "equivp r2" (* reflp should be enough... *) |
275 and b: "equivp r2" (* reflp is not enough *) |
276 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) |
276 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) |
277 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
277 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
278 unfolding Quotient_def comp_def |
278 unfolding Quotient_def comp_def |
279 apply (rule)+ |
279 apply (rule)+ |
280 apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset]) |
280 apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset]) |