70 |
70 |
71 lemma nil_rsp[quot_respect]: |
71 lemma nil_rsp[quot_respect]: |
72 shows "[] \<approx> []" |
72 shows "[] \<approx> []" |
73 by simp |
73 by simp |
74 |
74 |
75 lemma cons_rsp[quot_respect]: |
75 lemma cons_rsp: |
|
76 "xa \<approx> ya \<Longrightarrow> y # xa \<approx> y # ya" |
|
77 by simp |
|
78 |
|
79 lemma [quot_respect]: |
76 shows "(op = ===> op \<approx> ===> op \<approx>) op # op #" |
80 shows "(op = ===> op \<approx> ===> op \<approx>) op # op #" |
77 by simp |
81 by simp |
78 |
82 |
79 |
83 |
80 section {* Augmenting a set -- @{const finsert} *} |
84 section {* Augmenting a set -- @{const finsert} *} |
81 |
85 |
82 text {* raw section *} |
86 text {* raw section *} |
255 shows "concat [] \<approx> []" |
259 shows "concat [] \<approx> []" |
256 by (simp add: id_simps) |
260 by (simp add: id_simps) |
257 |
261 |
258 lemma concat2: |
262 lemma concat2: |
259 shows "concat (x # xs) \<approx> x @ concat xs" |
263 shows "concat (x # xs) \<approx> x @ concat xs" |
260 by (simp add: id_simps) |
264 by (simp) |
261 |
265 |
262 lemma concat_rsp[quot_respect]: |
266 lemma concat_rsp[quot_respect]: |
263 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
267 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
264 sorry |
268 sorry |
265 |
269 |
266 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []" |
270 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []" |
267 apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros) |
271 apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros) |
268 done |
272 done |
269 |
273 |
342 apply (rule equivp_reflp[OF fset_equivp]) |
346 apply (rule equivp_reflp[OF fset_equivp]) |
343 apply (rule list_rel_refl) |
347 apply (rule list_rel_refl) |
344 apply (metis equivp_def fset_equivp) |
348 apply (metis equivp_def fset_equivp) |
345 apply rule |
349 apply rule |
346 apply rule |
350 apply rule |
347 apply(rule quotient_compose_list_pre) |
351 apply (rule quotient_compose_list_pre) |
348 done |
352 done |
349 |
353 |
350 lemma fconcat_empty: |
354 lemma fconcat_empty: |
351 shows "fconcat {||} = {||}" |
355 shows "fconcat {||} = {||}" |
352 apply(lifting concat1) |
356 apply(lifting concat1) |
353 apply(cleaning) |
357 apply(cleaning) |
354 apply(simp add: comp_def) |
358 apply(simp add: comp_def) |
355 apply(fold fempty_def[simplified id_simps]) |
359 apply(fold fempty_def[simplified id_simps]) |
356 apply(rule refl) |
360 apply(rule refl) |
357 done |
361 done |
358 |
362 |
359 (* Should be true *) |
363 (* Should be true *) |
360 |
364 |
361 lemma insert_rsp2[quot_respect]: |
365 lemma insert_rsp2[quot_respect]: |
362 "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #" |
366 "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #" |
363 apply auto |
367 apply auto |
364 apply (simp add: set_in_eq) |
368 apply (simp add: set_in_eq) |
365 sorry |
369 apply (rule_tac b="x # b" in pred_compI) |
|
370 apply auto |
|
371 apply (rule_tac b="x # ba" in pred_compI) |
|
372 apply (rule cons_rsp) |
|
373 apply simp |
|
374 apply (auto)[1] |
|
375 done |
366 |
376 |
367 lemma append_rsp[quot_respect]: |
377 lemma append_rsp[quot_respect]: |
368 "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
378 "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
369 by (auto) |
379 by (auto) |
370 |
380 |
371 lemma fconcat_insert: |
381 lemma fconcat_insert: |
372 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
382 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
373 apply(lifting concat2) |
383 apply(lifting concat2) |
374 apply(cleaning) |
384 apply(cleaning) |
375 apply (simp add: finsert_def fconcat_def comp_def) |
385 apply (simp add: finsert_def fconcat_def comp_def) |
376 apply cleaning |
386 apply cleaning |
377 done |
387 done |
378 |
388 |
379 text {* raw section *} |
389 text {* raw section *} |
380 |
390 |
381 lemma map_rsp_aux: |
391 lemma map_rsp_aux: |
382 assumes a: "a \<approx> b" |
392 assumes a: "a \<approx> b" |