equal
deleted
inserted
replaced
352 |
352 |
353 lemma fconcat_insert: |
353 lemma fconcat_insert: |
354 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
354 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
355 apply(lifting concat2) |
355 apply(lifting concat2) |
356 apply(injection) |
356 apply(injection) |
|
357 (* The Relation is wrong to apply rep_abs_rsp *) |
|
358 thm rep_abs_rsp[of "(op \<approx> ===> op =)"] |
357 defer |
359 defer |
|
360 apply (simp only: finsert_def[simplified id_simps]) |
|
361 apply (simp only: fconcat_def[simplified id_simps]) |
358 apply(cleaning) |
362 apply(cleaning) |
|
363 (* finsert_def doesn't get folded, since rep-abs types are incorrect *) |
359 apply(simp add: comp_def) |
364 apply(simp add: comp_def) |
360 apply(cleaning) |
365 apply (simp add: fconcat_def[simplified id_simps]) |
|
366 apply cleaning |
|
367 (* The Relation is wrong again. *) |
361 sorry |
368 sorry |
362 |
369 |
363 text {* raw section *} |
370 text {* raw section *} |
364 |
371 |
365 lemma map_rsp_aux: |
372 lemma map_rsp_aux: |