equal
deleted
inserted
replaced
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 |
165 by auto |
166 |
166 |
167 lemma [quot_respect]: |
167 lemma [quot_respect]: |
168 shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
168 shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
348 have "ya \<in> set y'" using b h by simp |
348 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) |
349 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 |
350 then show ?thesis using f i by auto |
351 qed |
351 qed |
352 |
352 |
353 lemma [quot_respect]: |
353 lemma concat_rsp[quot_respect]: |
354 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
354 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
355 proof (rule fun_relI, elim pred_compE) |
355 proof (rule fun_relI, elim pred_compE) |
356 fix a b ba bb |
356 fix a b ba bb |
357 assume a: "list_rel op \<approx> a ba" |
357 assume a: "list_rel op \<approx> a ba" |
358 assume b: "ba \<approx> bb" |
358 assume b: "ba \<approx> bb" |