equal
deleted
inserted
replaced
32 text {* Basic projection function. *} |
32 text {* Basic projection function. *} |
33 |
33 |
34 primrec |
34 primrec |
35 sort_of :: "atom \<Rightarrow> atom_sort" |
35 sort_of :: "atom \<Rightarrow> atom_sort" |
36 where |
36 where |
37 "sort_of (Atom s i) = s" |
37 "sort_of (Atom s n) = s" |
38 |
38 |
39 primrec |
39 primrec |
40 nat_of :: "atom \<Rightarrow> nat" |
40 nat_of :: "atom \<Rightarrow> nat" |
41 where |
41 where |
42 "nat_of (Atom s n) = n" |
42 "nat_of (Atom s n) = n" |
1119 by (simp add: fresh_permute_iff) |
1119 by (simp add: fresh_permute_iff) |
1120 |
1120 |
1121 lemma supp_eqvt [eqvt]: |
1121 lemma supp_eqvt [eqvt]: |
1122 shows "p \<bullet> (supp x) = supp (p \<bullet> x)" |
1122 shows "p \<bullet> (supp x) = supp (p \<bullet> x)" |
1123 unfolding supp_conv_fresh |
1123 unfolding supp_conv_fresh |
1124 unfolding Collect_def |
1124 by (perm_simp) (rule refl) |
1125 unfolding permute_fun_def |
|
1126 by (simp add: Not_eqvt fresh_eqvt) |
|
1127 |
1125 |
1128 lemma fresh_permute_left: |
1126 lemma fresh_permute_left: |
1129 shows "a \<sharp> p \<bullet> x \<longleftrightarrow> - p \<bullet> a \<sharp> x" |
1127 shows "a \<sharp> p \<bullet> x \<longleftrightarrow> - p \<bullet> a \<sharp> x" |
1130 proof |
1128 proof |
1131 assume "a \<sharp> p \<bullet> x" |
1129 assume "a \<sharp> p \<bullet> x" |
1715 shows "supp S = S" |
1713 shows "supp S = S" |
1716 apply(rule finite_supp_unique) |
1714 apply(rule finite_supp_unique) |
1717 apply(simp add: supports_def) |
1715 apply(simp add: supports_def) |
1718 apply(simp add: swap_set_not_in) |
1716 apply(simp add: swap_set_not_in) |
1719 apply(rule assms) |
1717 apply(rule assms) |
|
1718 apply(simp add: swap_set_in) |
|
1719 done |
|
1720 |
|
1721 lemma supp_cofinite_atom_set: |
|
1722 fixes S::"atom set" |
|
1723 assumes "finite (UNIV - S)" |
|
1724 shows "supp S = (UNIV - S)" |
|
1725 apply(rule finite_supp_unique) |
|
1726 apply(simp add: supports_def) |
|
1727 apply(simp add: swap_set_both_in) |
|
1728 apply(rule assms) |
|
1729 apply(subst swap_commute) |
1720 apply(simp add: swap_set_in) |
1730 apply(simp add: swap_set_in) |
1721 done |
1731 done |
1722 |
1732 |
1723 lemma fresh_finite_atom_set: |
1733 lemma fresh_finite_atom_set: |
1724 fixes S::"atom set" |
1734 fixes S::"atom set" |