857 |
857 |
858 lemma supp_zero_perm: |
858 lemma supp_zero_perm: |
859 shows "supp (0::perm) = {}" |
859 shows "supp (0::perm) = {}" |
860 unfolding supp_perm by simp |
860 unfolding supp_perm by simp |
861 |
861 |
|
862 lemma fresh_plus_perm: |
|
863 fixes p q::perm |
|
864 assumes "a \<sharp> p" "a \<sharp> q" |
|
865 shows "a \<sharp> (p + q)" |
|
866 using assms |
|
867 unfolding fresh_def |
|
868 by (auto simp add: supp_perm) |
|
869 |
862 lemma supp_plus_perm: |
870 lemma supp_plus_perm: |
863 fixes p q::perm |
871 fixes p q::perm |
864 shows "supp (p + q) \<subseteq> supp p \<union> supp q" |
872 shows "supp (p + q) \<subseteq> supp p \<union> supp q" |
865 by (auto simp add: supp_perm) |
873 by (auto simp add: supp_perm) |
866 |
874 |
|
875 lemma fresh_minus_perm: |
|
876 fixes p::perm |
|
877 shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p" |
|
878 unfolding fresh_def |
|
879 apply(auto simp add: supp_perm) |
|
880 apply(metis permute_minus_cancel)+ |
|
881 done |
|
882 |
867 lemma supp_minus_perm: |
883 lemma supp_minus_perm: |
868 fixes p::perm |
884 fixes p::perm |
869 shows "supp (- p) = supp p" |
885 shows "supp (- p) = supp p" |
870 apply(auto simp add: supp_perm) |
886 unfolding supp_conv_fresh |
871 apply(metis permute_minus_cancel)+ |
887 by (simp add: fresh_minus_perm) |
872 done |
|
873 |
888 |
874 instance perm :: fs |
889 instance perm :: fs |
875 by default (simp add: supp_perm finite_perm_lemma) |
890 by default (simp add: supp_perm finite_perm_lemma) |
876 |
891 |
877 |
892 |