equal
deleted
inserted
replaced
242 |
242 |
243 lemma map_eqvt[eqvt]: |
243 lemma map_eqvt[eqvt]: |
244 shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)" |
244 shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)" |
245 by (induct xs) (simp_all, simp only: permute_fun_app_eq) |
245 by (induct xs) (simp_all, simp only: permute_fun_app_eq) |
246 |
246 |
|
247 lemma removeAll_eqvt[eqvt]: |
|
248 shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)" |
|
249 by (induct xs) (auto) |
|
250 |
|
251 lemma supp_removeAll: |
|
252 fixes x::"atom" |
|
253 shows "supp (removeAll x xs) = supp xs - {x}" |
|
254 by (induct xs) |
|
255 (auto simp add: supp_Nil supp_Cons supp_atom) |
|
256 |
247 |
257 |
248 subsection {* Equivariance Finite-Set Operations *} |
258 subsection {* Equivariance Finite-Set Operations *} |
249 |
259 |
250 lemma in_fset_eqvt[eqvt]: |
260 lemma in_fset_eqvt[eqvt]: |
251 shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))" |
261 shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))" |