equal
deleted
inserted
replaced
27 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
27 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
28 apply(simp add: fresh_star_def) |
28 apply(simp add: fresh_star_def) |
29 apply(auto) |
29 apply(auto) |
30 apply(drule_tac x="p \<bullet> xa" in bspec) |
30 apply(drule_tac x="p \<bullet> xa" in bspec) |
31 apply(unfold mem_def permute_fun_def)[1] |
31 apply(unfold mem_def permute_fun_def)[1] |
32 apply(simp add: eqvts) |
32 apply(simp add: eqvts del: permute_eqvt) |
33 apply(simp add: fresh_permute_iff) |
33 apply(simp add: fresh_permute_iff) |
34 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1]) |
34 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1]) |
35 apply(simp) |
35 apply(simp) |
36 apply(drule_tac x="- p \<bullet> xa" in bspec) |
36 apply(drule_tac x="- p \<bullet> xa" in bspec) |
37 apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1]) |
37 apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1]) |