equal
deleted
inserted
replaced
276 |
276 |
277 lemma memb_delete_raw: |
277 lemma memb_delete_raw: |
278 "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)" |
278 "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)" |
279 by (induct xs arbitrary: x y) (auto simp add: memb_def) |
279 by (induct xs arbitrary: x y) (auto simp add: memb_def) |
280 |
280 |
|
281 lemma delete_raw_rsp: |
|
282 "l \<approx> r \<Longrightarrow> delete_raw l x \<approx> delete_raw r x" |
|
283 by (simp add: memb_def[symmetric] memb_delete_raw) |
|
284 |
281 lemma [quot_respect]: |
285 lemma [quot_respect]: |
282 "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw" |
286 "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw" |
283 by (simp add: memb_def[symmetric] memb_delete_raw) |
287 by (simp add: memb_def[symmetric] memb_delete_raw) |
284 |
288 |
285 lemma memb_delete_raw_ident: |
289 lemma memb_delete_raw_ident: |