equal
deleted
inserted
replaced
273 apply(induct xs) |
273 apply(induct xs) |
274 apply(simp add: permute_bool_def) |
274 apply(simp add: permute_bool_def) |
275 apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt) |
275 apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt) |
276 done |
276 done |
277 |
277 |
|
278 lemma length_eqvt[eqvt]: |
|
279 shows "p \<bullet> (length xs) = length (p \<bullet> xs)" |
|
280 by (induct xs) (simp_all add: permute_pure) |
|
281 |
278 |
282 |
279 subsection {* Equivariance Finite-Set Operations *} |
283 subsection {* Equivariance Finite-Set Operations *} |
280 |
284 |
281 lemma in_fset_eqvt[eqvt]: |
285 lemma in_fset_eqvt[eqvt]: |
282 shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))" |
286 shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))" |