equal
deleted
inserted
replaced
747 "distinct_perms [] = True" |
747 "distinct_perms [] = True" |
748 | "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)" |
748 | "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)" |
749 |
749 |
750 (* support of concrete atom sets *) |
750 (* support of concrete atom sets *) |
751 |
751 |
752 lemma atom_eqvt_raw: |
|
753 fixes p::"perm" |
|
754 shows "(p \<bullet> atom) = atom" |
|
755 by (simp add: expand_fun_eq permute_fun_def atom_eqvt) |
|
756 |
|
757 lemma atom_image_cong: |
|
758 shows "(atom ` X = atom ` Y) = (X = Y)" |
|
759 apply(rule inj_image_eq_iff) |
|
760 apply(simp add: inj_on_def) |
|
761 done |
|
762 |
|
763 lemma supp_atom_image: |
752 lemma supp_atom_image: |
764 fixes as::"'a::at_base set" |
753 fixes as::"'a::at_base set" |
765 shows "supp (atom ` as) = supp as" |
754 shows "supp (atom ` as) = supp as" |
766 apply(simp add: supp_def) |
755 apply(simp add: supp_def) |
767 apply(simp add: image_eqvt) |
756 apply(simp add: image_eqvt) |