56 |
56 |
57 lemma fresh_star_prod_elim: |
57 lemma fresh_star_prod_elim: |
58 shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)" |
58 shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)" |
59 by (rule, simp_all add: fresh_star_prod) |
59 by (rule, simp_all add: fresh_star_prod) |
60 |
60 |
|
61 lemma fresh_star_zero: |
|
62 shows "as \<sharp>* (0::perm)" |
|
63 unfolding fresh_star_def |
|
64 by (simp add: fresh_zero_perm) |
|
65 |
61 lemma fresh_star_plus: |
66 lemma fresh_star_plus: |
62 fixes p q::perm |
67 fixes p q::perm |
63 shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
68 shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
64 unfolding fresh_star_def |
69 unfolding fresh_star_def |
65 by (simp add: fresh_plus_perm) |
70 by (simp add: fresh_plus_perm) |
|
71 |
66 |
72 |
67 lemma fresh_star_permute_iff: |
73 lemma fresh_star_permute_iff: |
68 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
74 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
69 unfolding fresh_star_def |
75 unfolding fresh_star_def |
70 by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff) |
76 by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff) |