equal
deleted
inserted
replaced
162 |
162 |
163 lemma append_rsp[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 append_rsp_unfolded: |
|
168 "\<lbrakk>x \<approx> y; v \<approx> w\<rbrakk> \<Longrightarrow> x @ v \<approx> y @ w" |
|
169 by auto |
|
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) |
170 |
174 |
171 lemma memb_rsp[quot_respect]: |
175 lemma memb_rsp[quot_respect]: |
371 qed |
375 qed |
372 qed |
376 qed |
373 then show "concat a \<approx> concat b" by simp |
377 then show "concat a \<approx> concat b" by simp |
374 qed |
378 qed |
375 |
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 - |
|
385 fix a b ba bb |
|
386 assume a: "list_rel op \<approx> a ba" |
|
387 assume b: "ba \<approx> bb" |
|
388 assume c: "list_rel op \<approx> bb b" |
|
389 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
|
390 fix x |
|
391 show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
|
392 assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
|
393 show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
|
394 next |
|
395 assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
|
396 have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a]) |
|
397 have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) |
|
398 have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c]) |
|
399 show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
|
400 qed |
|
401 qed |
|
402 then show "concat a \<approx> concat b" by simp |
|
403 qed |
|
404 |
376 lemma [quot_respect]: |
405 lemma [quot_respect]: |
377 "((op =) ===> op \<approx> ===> op \<approx>) filter filter" |
406 "((op =) ===> op \<approx> ===> op \<approx>) filter filter" |
378 by auto |
407 by auto |
379 |
408 |
380 text {* Distributive lattice with bot *} |
409 text {* Distributive lattice with bot *} |