equal
deleted
inserted
replaced
252 lemma concat2: |
252 lemma concat2: |
253 shows "concat (x # xs) \<approx> x @ concat xs" |
253 shows "concat (x # xs) \<approx> x @ concat xs" |
254 by (simp add: id_simps) |
254 by (simp add: id_simps) |
255 |
255 |
256 lemma concat_rsp[quot_respect]: |
256 lemma concat_rsp[quot_respect]: |
257 shows "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> op \<approx>) concat concat" |
257 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
258 sorry |
258 sorry |
259 |
259 |
260 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) [] []" |
260 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []" |
261 apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros) |
261 apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros) |
262 done |
262 done |
263 |
263 |
264 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B" |
264 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B" |
265 apply (rule eq_reflection) |
265 apply (rule eq_reflection) |
270 unfolding list_eq.simps |
270 unfolding list_eq.simps |
271 apply(simp only: set_map set_in_eq) |
271 apply(simp only: set_map set_in_eq) |
272 done |
272 done |
273 |
273 |
274 lemma quotient_compose_list_pre: |
274 lemma quotient_compose_list_pre: |
275 "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r s = |
275 "(list_rel op \<approx> OOO op \<approx>) r s = |
276 ((list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r r \<and> |
276 ((list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s \<and> |
277 (list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) s s \<and> |
|
278 abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
277 abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
279 apply rule |
278 apply rule |
280 apply rule |
279 apply rule |
281 apply rule |
280 apply rule |
282 apply (rule list_rel_refl) |
281 apply (rule list_rel_refl) |
321 apply (rule map_rel_cong) |
320 apply (rule map_rel_cong) |
322 apply (assumption) |
321 apply (assumption) |
323 done |
322 done |
324 |
323 |
325 lemma quotient_compose_list[quot_thm]: |
324 lemma quotient_compose_list[quot_thm]: |
326 shows "Quotient ((list_rel op \<approx>) OO (op \<approx>) OO (list_rel op \<approx>)) |
325 shows "Quotient ((list_rel op \<approx>) OOO (op \<approx>)) |
327 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
326 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
328 unfolding Quotient_def comp_def |
327 unfolding Quotient_def comp_def |
329 apply (rule)+ |
328 apply (rule)+ |
330 apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset]) |
329 apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset]) |
331 apply (rule) |
330 apply (rule) |
332 apply (rule) |
331 apply (rule) |
352 done |
351 done |
353 |
352 |
354 (* Should be true *) |
353 (* Should be true *) |
355 |
354 |
356 lemma insert_rsp2[quot_respect]: |
355 lemma insert_rsp2[quot_respect]: |
357 "(op \<approx> ===> list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) op # op #" |
356 "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #" |
358 apply auto |
357 apply auto |
359 apply (simp add: set_in_eq) |
358 apply (simp add: set_in_eq) |
360 sorry |
359 sorry |
361 |
360 |
362 lemma append_rsp[quot_respect]: |
361 lemma append_rsp[quot_respect]: |