723   "distinct_perms [] = True"

   723   "distinct_perms [] = True"

   724 | "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"

   724 | "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"

   725 

   725 

   726 (* support of concrete atom sets *)

   726 (* support of concrete atom sets *)

   727 

   727 

   730 lemma atom_eqvt_raw:

   728 lemma atom_eqvt_raw:

   731   fixes p::"perm"

   729   fixes p::"perm"

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

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

   733 by (simp add: expand_fun_eq permute_fun_def atom_eqvt)

   731 by (simp add: expand_fun_eq permute_fun_def atom_eqvt)

   734 

   732 

   737 apply(rule inj_image_eq_iff)

   735 apply(rule inj_image_eq_iff)

   738 apply(simp add: inj_on_def)

   736 apply(simp add: inj_on_def)

   739 done

   737 done

   740 

   738 

   741 lemma

   739 lemma

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

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

   744 apply(simp add: supp_def)

   742 apply(simp add: supp_def)

   745 apply(simp add: image_eqvt)

   743 apply(simp add: image_eqvt)

   746 apply(simp add: atom_eqvt_raw)

   744 apply(simp add: atom_eqvt_raw)

   747 apply(simp add: atom_image_cong)

   745 apply(simp add: atom_image_cong)