equal
deleted
inserted
replaced
153 lemma Ball_eqvt[eqvt]: |
153 lemma Ball_eqvt[eqvt]: |
154 shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)" |
154 shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)" |
155 unfolding Ball_def |
155 unfolding Ball_def |
156 by (perm_simp) (rule refl) |
156 by (perm_simp) (rule refl) |
157 |
157 |
158 lemma supp_set_empty: |
|
159 shows "supp {} = {}" |
|
160 unfolding supp_def |
|
161 by (simp add: empty_eqvt) |
|
162 |
|
163 lemma fresh_set_empty: |
|
164 shows "a \<sharp> {}" |
|
165 by (simp add: fresh_def supp_set_empty) |
|
166 |
|
167 lemma UNIV_eqvt[eqvt]: |
158 lemma UNIV_eqvt[eqvt]: |
168 shows "p \<bullet> UNIV = UNIV" |
159 shows "p \<bullet> UNIV = UNIV" |
169 unfolding UNIV_def |
160 unfolding UNIV_def |
170 by (perm_simp) (rule refl) |
161 by (perm_simp) (rule refl) |
171 |
162 |
214 |
205 |
215 lemma finite_eqvt[eqvt]: |
206 lemma finite_eqvt[eqvt]: |
216 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
207 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
217 unfolding finite_permute_iff permute_bool_def .. |
208 unfolding finite_permute_iff permute_bool_def .. |
218 |
209 |
219 lemma supp_set: |
|
220 fixes xs :: "('a::fs) list" |
|
221 shows "supp (set xs) = supp xs" |
|
222 apply(induct xs) |
|
223 apply(simp add: supp_set_empty supp_Nil) |
|
224 apply(simp add: supp_Cons supp_of_finite_insert) |
|
225 done |
|
226 |
|
227 |
210 |
228 section {* List Operations *} |
211 section {* List Operations *} |
229 |
212 |
230 lemma append_eqvt[eqvt]: |
213 lemma append_eqvt[eqvt]: |
231 shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)" |
214 shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)" |
232 by (induct xs) auto |
215 by (induct xs) auto |
233 |
|
234 lemma supp_append: |
|
235 shows "supp (xs @ ys) = supp xs \<union> supp ys" |
|
236 by (induct xs) (auto simp add: supp_Nil supp_Cons) |
|
237 |
|
238 lemma fresh_append: |
|
239 shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys" |
|
240 by (induct xs) (simp_all add: fresh_Nil fresh_Cons) |
|
241 |
216 |
242 lemma rev_eqvt[eqvt]: |
217 lemma rev_eqvt[eqvt]: |
243 shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)" |
218 shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)" |
244 by (induct xs) (simp_all add: append_eqvt) |
219 by (induct xs) (simp_all add: append_eqvt) |
245 |
220 |