218 apply rule |
228 apply rule |
219 apply rule |
229 apply rule |
220 apply(rule quotient_compose_list_pre) |
230 apply(rule quotient_compose_list_pre) |
221 done |
231 done |
222 |
232 |
|
233 lemma quotient_compose_list_gen_pre: |
|
234 assumes a: "equivp r2" |
|
235 and b: "Quotient r2 abs2 rep2" |
|
236 shows "(list_rel r2 OO op \<approx>1 OO list_rel r2) r s = |
|
237 ((list_rel r2 OO op \<approx>1 OO list_rel r2) r r \<and> |
|
238 (list_rel r2 OO op \<approx>1 OO list_rel r2) s s \<and> |
|
239 abs_fset (map abs2 r) = abs_fset (map abs2 s))" |
|
240 apply rule |
|
241 apply rule |
|
242 apply rule |
|
243 apply (rule list_rel_refl) |
|
244 apply (metis equivp_def a) |
|
245 apply rule |
|
246 apply (rule equivp_reflp[OF fset_equivp]) |
|
247 apply (rule list_rel_refl) |
|
248 apply (metis equivp_def a) |
|
249 apply(rule) |
|
250 apply rule |
|
251 apply (rule list_rel_refl) |
|
252 apply (metis equivp_def a) |
|
253 apply rule |
|
254 apply (rule equivp_reflp[OF fset_equivp]) |
|
255 apply (rule list_rel_refl) |
|
256 apply (metis equivp_def a) |
|
257 apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s") |
|
258 apply (metis Quotient_rel[OF Quotient_fset]) |
|
259 apply (auto)[1] |
|
260 apply (subgoal_tac "map abs2 r = map abs2 b") |
|
261 prefer 2 |
|
262 apply (metis Quotient_rel[OF list_quotient[OF b]]) |
|
263 apply (subgoal_tac "map abs2 s = map abs2 ba") |
|
264 prefer 2 |
|
265 apply (metis Quotient_rel[OF list_quotient[OF b]]) |
|
266 apply (simp add: map_abs_ok_gen) |
|
267 apply rule |
|
268 apply (rule rep_abs_rsp[of "list_rel r2" "map abs2"]) |
|
269 apply (rule list_quotient) |
|
270 apply (rule b) |
|
271 apply (rule list_rel_refl) |
|
272 apply (metis equivp_def a) |
|
273 apply rule |
|
274 prefer 2 |
|
275 apply (rule rep_abs_rsp_left[of "list_rel r2" "map abs2"]) |
|
276 apply (rule list_quotient) |
|
277 apply (rule b) |
|
278 apply (rule list_rel_refl) |
|
279 apply (metis equivp_def a) |
|
280 apply (erule conjE)+ |
|
281 apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s") |
|
282 apply (rule map_rep_ok_gen) |
|
283 apply (assumption) |
|
284 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp a b) |
|
285 done |
|
286 |
223 lemma quotient_compose_list_gen: |
287 lemma quotient_compose_list_gen: |
224 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
288 assumes a: "Quotient r2 abs2 rep2" |
225 and a2: "Quotient r2 abs2 rep2" "equivp r2" |
289 and b: "equivp r2" (* reflp should be enough... *) |
226 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) |
290 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) |
227 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
291 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
228 unfolding Quotient_def comp_def |
292 unfolding Quotient_def comp_def |
229 apply (rule)+ |
293 apply (rule)+ |
230 apply (simp add: abs_o_rep[OF a2(1)] id_simps Quotient_abs_rep[OF Quotient_fset]) |
294 apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset]) |
231 apply (rule) |
295 apply (rule) |
232 apply (rule) |
296 apply (rule) |
233 apply (rule) |
297 apply (rule) |
234 apply (rule list_rel_refl) |
298 apply (rule list_rel_refl) |
235 apply (metis a2(2) equivp_def) |
299 apply (metis b equivp_def) |
236 apply (rule) |
300 apply (rule) |
237 apply (rule equivp_reflp[OF fset_equivp]) |
301 apply (rule equivp_reflp[OF fset_equivp]) |
238 apply (rule list_rel_refl) |
302 apply (rule list_rel_refl) |
239 apply (metis a2(2) equivp_def) |
303 apply (metis b equivp_def) |
240 apply rule |
304 apply rule |
241 apply rule |
305 apply rule |
242 apply(rule quotient_compose_list_gen_pre) |
306 apply(rule quotient_compose_list_gen_pre[OF b a]) |
243 done |
307 done |
244 |
308 |
245 (* This is the general statement but the types are wrong as in following exanples *) |
309 (* This is the general statement but the types of abs2 and rep2 |
|
310 are wrong as can be seen in following exanples *) |
|
311 |
246 lemma quotient_compose_general: |
312 lemma quotient_compose_general: |
247 assumes a2: "Quotient r1 abs1 rep_fset" |
313 assumes a2: "Quotient r1 abs1 rep1" |
248 and "Quotient r2 abs2 rep2" |
314 and "Quotient r2 abs2 rep2" |
249 shows "Quotient ((list_rel r2) OO r1 OO (list_rel r2)) |
315 shows "Quotient ((list_rel r2) OO r1 OO (list_rel r2)) |
250 (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
316 (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)" |
251 sorry |
317 sorry |
252 |
318 |
253 thm quotient_compose_ok [OF Quotient_fset] |
319 thm quotient_compose_ok [OF Quotient_fset] |
254 thm quotient_compose_general[OF Quotient_fset] |
320 thm quotient_compose_general[OF Quotient_fset] |
255 |
321 |