1165 lemma image_eqvt:

  1166   shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"

  1167   unfolding permute_set_eq_image

  1168   unfolding permute_fun_def [where f=f]

  1169   by (simp add: image_image)

  1170 

  1171 lemma atom_image_cong:

  1172   shows "(atom ` X = atom ` Y) = (X = Y)"

  1173   apply(rule inj_image_eq_iff)

  1174   apply(simp add: inj_on_def)

  1175   done

  1176 

  1177 lemma atom_image_supp:

  1178   shows "supp S = supp (atom ` S)"

  1179   apply(simp add: supp_def)

  1180   apply(simp add: image_eqvt)

  1181   apply(subst (2) permute_fun_def)

  1182   apply(simp add: atom_eqvt)

  1183   apply(simp add: atom_image_cong)

  1184   done

  1185 

  1186 lemma supp_finite_at_set:

  1187   assumes a: "finite S"

  1188   shows "supp S = atom ` S"

  1189 proof -

  1190   have fin: "finite (atom ` S)" 

  1191     using a by (simp add: finite_imageI) 

  1192   have "supp S = supp (atom ` S)" by (rule atom_image_supp)

  1193   also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set)

  1194   finally show "supp S = atom ` S" by simp

  1195 qed

  1196 

  1197 lemma supp_at_insert:

  1198   fixes a::"'a::at_base"

  1199   assumes a: "finite S"

  1200   shows "supp (insert a S) = supp a \<union> supp S"

  1201   using a by (simp add: supp_finite_at_set supp_at_base)

  1202