equal
deleted
inserted
replaced
66 lemma fresh_star_permute_iff: |
66 lemma fresh_star_permute_iff: |
67 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
67 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
68 unfolding fresh_star_def |
68 unfolding fresh_star_def |
69 by (metis mem_permute_iff permute_minus_cancel fresh_permute_iff) |
69 by (metis mem_permute_iff permute_minus_cancel fresh_permute_iff) |
70 |
70 |
71 lemma fresh_star_eqvt: |
71 lemma fresh_star_eqvt[eqvt]: |
72 shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)" |
72 shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)" |
73 unfolding fresh_star_def |
73 unfolding fresh_star_def |
74 unfolding Ball_def |
74 unfolding Ball_def |
75 apply(simp add: all_eqvt) |
75 apply(simp add: all_eqvt) |
76 apply(subst permute_fun_def) |
76 apply(subst permute_fun_def) |