equal
deleted
inserted
replaced
154 |
154 |
155 lemma Collect_eqvt2: |
155 lemma Collect_eqvt2: |
156 shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}" |
156 shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}" |
157 by (perm_simp add: permute_minus_cancel) (rule refl) |
157 by (perm_simp add: permute_minus_cancel) (rule refl) |
158 |
158 |
|
159 lemma Bex_eqvt[eqvt]: |
|
160 shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)" |
|
161 unfolding Bex_def |
|
162 by (perm_simp) (rule refl) |
|
163 |
|
164 lemma Ball_eqvt[eqvt]: |
|
165 shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)" |
|
166 unfolding Ball_def |
|
167 by (perm_simp) (rule refl) |
|
168 |
159 lemma empty_eqvt[eqvt]: |
169 lemma empty_eqvt[eqvt]: |
160 shows "p \<bullet> {} = {}" |
170 shows "p \<bullet> {} = {}" |
161 unfolding empty_def |
171 unfolding empty_def |
162 by (perm_simp) (rule refl) |
172 by (perm_simp) (rule refl) |
163 |
173 |
202 unfolding permute_set_eq_image image_insert .. |
212 unfolding permute_set_eq_image image_insert .. |
203 |
213 |
204 lemma vimage_eqvt[eqvt]: |
214 lemma vimage_eqvt[eqvt]: |
205 shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)" |
215 shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)" |
206 unfolding vimage_def |
216 unfolding vimage_def |
|
217 by (perm_simp) (rule refl) |
|
218 |
|
219 lemma Union_eqvt[eqvt]: |
|
220 shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)" |
|
221 unfolding Union_eq |
207 by (perm_simp) (rule refl) |
222 by (perm_simp) (rule refl) |
208 |
223 |
209 lemma finite_permute_iff: |
224 lemma finite_permute_iff: |
210 shows "finite (p \<bullet> A) \<longleftrightarrow> finite A" |
225 shows "finite (p \<bullet> A) \<longleftrightarrow> finite A" |
211 unfolding permute_set_eq_vimage |
226 unfolding permute_set_eq_vimage |