equal
deleted
inserted
replaced
734 shows "(atom ` X = atom ` Y) = (X = Y)" |
734 shows "(atom ` X = atom ` Y) = (X = Y)" |
735 apply(rule inj_image_eq_iff) |
735 apply(rule inj_image_eq_iff) |
736 apply(simp add: inj_on_def) |
736 apply(simp add: inj_on_def) |
737 done |
737 done |
738 |
738 |
739 lemma |
739 lemma supp_atom_image: |
740 fixes as::"'a::at_base set" |
740 fixes as::"'a::at_base set" |
741 shows "supp (atom ` as) = supp as" |
741 shows "supp (atom ` as) = supp as" |
742 apply(simp add: supp_def) |
742 apply(simp add: supp_def) |
743 apply(simp add: image_eqvt) |
743 apply(simp add: image_eqvt) |
744 apply(simp add: atom_eqvt_raw) |
744 apply(simp add: atom_eqvt_raw) |
745 apply(simp add: atom_image_cong) |
745 apply(simp add: atom_image_cong) |
746 done |
746 done |
747 |
747 |
|
748 lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn" |
|
749 apply (simp add: fresh_def) |
|
750 apply (simp add: supp_atom_image) |
|
751 apply (fold fresh_def) |
|
752 apply (simp add: swap_fresh_fresh) |
|
753 done |
748 |
754 |
749 |
755 |
750 end |
756 end |
751 |
757 |