equal
deleted
inserted
replaced
258 fixes x::"atom" |
258 fixes x::"atom" |
259 shows "supp (removeAll x xs) = supp xs - {x}" |
259 shows "supp (removeAll x xs) = supp xs - {x}" |
260 by (induct xs) |
260 by (induct xs) |
261 (auto simp add: supp_Nil supp_Cons supp_atom) |
261 (auto simp add: supp_Nil supp_Cons supp_atom) |
262 |
262 |
|
263 lemma filter_eqvt[eqvt]: |
|
264 shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)" |
|
265 apply(induct xs) |
|
266 apply(simp) |
|
267 apply(simp only: filter.simps permute_list.simps if_eqvt) |
|
268 apply(simp only: permute_fun_app_eq) |
|
269 done |
|
270 |
|
271 lemma distinct_eqvt[eqvt]: |
|
272 shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)" |
|
273 apply(induct xs) |
|
274 apply(simp add: permute_bool_def) |
|
275 apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt) |
|
276 done |
|
277 |
263 |
278 |
264 subsection {* Equivariance Finite-Set Operations *} |
279 subsection {* Equivariance Finite-Set Operations *} |
265 |
280 |
266 lemma in_fset_eqvt[eqvt]: |
281 lemma in_fset_eqvt[eqvt]: |
267 shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))" |
282 shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))" |