726 (* support of concrete atom sets *)

   727 

   728 atom_decl name

   729 

   730 lemma atom_eqvt_raw:

   731   fixes p::"perm"

   732   shows "(p \<bullet> atom) = atom"

   733 by (simp add: expand_fun_eq permute_fun_def atom_eqvt)

   734 

   735 lemma atom_image_cong:

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

   737 apply(rule inj_image_eq_iff)

   738 apply(simp add: inj_on_def)

   739 done

   740 

   741 lemma

   742   fixes as::"name set"

   743   shows "supp (atom ` as) = supp as"

   744 apply(simp add: supp_def)

   745 apply(simp add: image_eqvt)

   746 apply(simp add: atom_eqvt_raw)

   747 apply(simp add: atom_image_cong)

   748 done

   749