equal
deleted
inserted
replaced
481 apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x") |
481 apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x") |
482 apply(auto simp add: fresh_star_def fresh_def supp_perm)[1] |
482 apply(auto simp add: fresh_star_def fresh_def supp_perm)[1] |
483 apply(auto simp add: fresh_star_def fresh_def) |
483 apply(auto simp add: fresh_star_def fresh_def) |
484 done |
484 done |
485 |
485 |
|
486 lemma at_set_avoiding2_atom: |
|
487 assumes "finite (supp c)" "finite (supp x)" |
|
488 and b: "xa \<sharp> x" |
|
489 shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p" |
|
490 proof - |
|
491 have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b) |
|
492 obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p" |
|
493 using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast |
|
494 have c: "(p \<bullet> xa) \<sharp> c" using p1 |
|
495 unfolding fresh_star_def Ball_def |
|
496 by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts) |
|
497 hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast |
|
498 then show ?thesis by blast |
|
499 qed |
|
500 |
486 end |
501 end |