equal
deleted
inserted
replaced
158 lemma set_fminus_raw[simp]: |
158 lemma set_fminus_raw[simp]: |
159 "set (fminus_raw xs ys) = (set xs - set ys)" |
159 "set (fminus_raw xs ys) = (set xs - set ys)" |
160 by (induct ys arbitrary: xs) (auto) |
160 by (induct ys arbitrary: xs) (auto) |
161 |
161 |
162 |
162 |
163 text {* Respectfullness *} |
163 text {* Respectfulness *} |
164 |
164 |
165 lemma append_rsp[quot_respect]: |
165 lemma append_rsp[quot_respect]: |
166 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append" |
166 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append" |
167 by (simp) |
167 by (simp) |
168 |
168 |
297 qed |
297 qed |
298 then show "concat a \<approx> concat b" by auto |
298 then show "concat a \<approx> concat b" by auto |
299 qed |
299 qed |
300 |
300 |
301 lemma [quot_respect]: |
301 lemma [quot_respect]: |
302 shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter" |
302 shows "(op = ===> op \<approx> ===> op \<approx>) filter filter" |
303 by auto |
303 by auto |
304 |
304 |
305 text {* Distributive lattice with bot *} |
305 text {* Distributive lattice with bot *} |
306 |
306 |
307 lemma append_inter_distrib: |
307 lemma append_inter_distrib: |