158 qed |
158 qed |
159 qed |
159 qed |
160 |
160 |
161 text {* Respectfullness *} |
161 text {* Respectfullness *} |
162 |
162 |
163 lemma [quot_respect]: |
163 lemma append_rsp[quot_respect]: |
164 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
164 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
|
165 by auto |
|
166 |
|
167 lemma append_rsp_unfolded: |
|
168 "\<lbrakk>x \<approx> y; v \<approx> w\<rbrakk> \<Longrightarrow> x @ v \<approx> y @ w" |
165 by auto |
169 by auto |
166 |
170 |
167 lemma [quot_respect]: |
171 lemma [quot_respect]: |
168 shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
172 shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
169 by (auto simp add: sub_list_def) |
173 by (auto simp add: sub_list_def) |
348 have "ya \<in> set y'" using b h by simp |
352 have "ya \<in> set y'" using b h by simp |
349 then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_rel_find_element) |
353 then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_rel_find_element) |
350 then show ?thesis using f i by auto |
354 then show ?thesis using f i by auto |
351 qed |
355 qed |
352 |
356 |
353 lemma [quot_respect]: |
357 lemma concat_rsp[quot_respect]: |
354 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
358 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
355 proof (rule fun_relI, elim pred_compE) |
359 proof (rule fun_relI, elim pred_compE) |
|
360 fix a b ba bb |
|
361 assume a: "list_rel op \<approx> a ba" |
|
362 assume b: "ba \<approx> bb" |
|
363 assume c: "list_rel op \<approx> bb b" |
|
364 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
|
365 fix x |
|
366 show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
|
367 assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
|
368 show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
|
369 next |
|
370 assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
|
371 have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a]) |
|
372 have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) |
|
373 have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c]) |
|
374 show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
|
375 qed |
|
376 qed |
|
377 then show "concat a \<approx> concat b" by simp |
|
378 qed |
|
379 |
|
380 |
|
381 |
|
382 lemma concat_rsp_unfolded: |
|
383 "\<lbrakk>list_rel op \<approx> a ba; ba \<approx> bb; list_rel op \<approx> bb b\<rbrakk> \<Longrightarrow> concat a \<approx> concat b" |
|
384 proof - |
356 fix a b ba bb |
385 fix a b ba bb |
357 assume a: "list_rel op \<approx> a ba" |
386 assume a: "list_rel op \<approx> a ba" |
358 assume b: "ba \<approx> bb" |
387 assume b: "ba \<approx> bb" |
359 assume c: "list_rel op \<approx> bb b" |
388 assume c: "list_rel op \<approx> bb b" |
360 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
389 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
594 apply (rule_tac b="x # b" in pred_compI) |
623 apply (rule_tac b="x # b" in pred_compI) |
595 apply auto |
624 apply auto |
596 apply (rule_tac b="x # ba" in pred_compI) |
625 apply (rule_tac b="x # ba" in pred_compI) |
597 apply auto |
626 apply auto |
598 done |
627 done |
|
628 |
|
629 lemma insert_preserve2: |
|
630 shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) = |
|
631 (id ---> rep_fset ---> abs_fset) op #" |
|
632 by (simp add: expand_fun_eq abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset]) |
599 |
633 |
600 lemma [quot_preserve]: |
634 lemma [quot_preserve]: |
601 "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert" |
635 "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert" |
602 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
636 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
603 abs_o_rep[OF Quotient_fset] map_id finsert_def) |
637 abs_o_rep[OF Quotient_fset] map_id finsert_def) |