55 |
55 |
56 lemma fresh_star_prod_elim: |
56 lemma fresh_star_prod_elim: |
57 shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)" |
57 shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)" |
58 by (rule, simp_all add: fresh_star_prod) |
58 by (rule, simp_all add: fresh_star_prod) |
59 |
59 |
|
60 lemma fresh_star_plus: |
|
61 fixes p q::perm |
|
62 shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
|
63 unfolding fresh_star_def |
|
64 by (simp add: fresh_plus_perm) |
|
65 |
|
66 lemma fresh_star_permute_iff: |
|
67 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
|
68 unfolding fresh_star_def |
|
69 by (metis mem_permute_iff permute_minus_cancel fresh_permute_iff) |
|
70 |
|
71 lemma fresh_star_eqvt: |
|
72 shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)" |
|
73 unfolding fresh_star_def |
|
74 unfolding Ball_def |
|
75 apply(simp add: all_eqvt) |
|
76 apply(subst permute_fun_def) |
|
77 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt) |
|
78 done |
60 |
79 |
61 section {* Avoiding of atom sets *} |
80 section {* Avoiding of atom sets *} |
62 |
81 |
63 text {* |
82 text {* |
64 For every set of atoms, there is another set of atoms |
83 For every set of atoms, there is another set of atoms |