235 subsection {* Equivariance for fsets *} 

   235 subsection {* Equivariance Finite-Set Operations *}

   236 

   237 lemma in_fset_eqvt[eqvt]:

   238   shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"

   239 unfolding in_fset

   240 by (perm_simp) (simp)

   241 

   242 lemma union_fset_eqvt[eqvt]:

   243   shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"

   244 by (induct S) (simp_all)

   245 

   246 lemma supp_union_fset:

   247   fixes S T::"'a::fs fset"

   248   shows "supp (S |\<union>| T) = supp S \<union> supp T"

   249 by (induct S) (auto)

   250 

   251 lemma fresh_union_fset:

   252   fixes S T::"'a::fs fset"

   253   shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"

   254 unfolding fresh_def

   255 by (simp add: supp_union_fset)