equal
deleted
inserted
replaced
464 by (induct xs rule: add_perm.induct) |
464 by (induct xs rule: add_perm.induct) |
465 (simp_all add: supp_Cons supp_Pair supp_atom swap_fresh_fresh) |
465 (simp_all add: supp_Cons supp_Pair supp_atom swap_fresh_fresh) |
466 then show "p \<bullet> x = x" using eq by simp |
466 then show "p \<bullet> x = x" using eq by simp |
467 qed |
467 qed |
468 |
468 |
469 |
469 section {* at_set_avoiding2 *} |
|
470 |
|
471 lemma at_set_avoiding2 |
|
472 assumes "finite xs" |
|
473 and "finite (supp c)" "finite (supp x)" |
|
474 and "xs \<sharp>* x" |
|
475 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p" |
|
476 using assms |
|
477 apply(erule_tac c="(c, x)" in at_set_avoiding) |
|
478 apply(simp add: supp_Pair) |
|
479 apply(rule_tac x="p" in exI) |
|
480 apply(simp add: fresh_star_prod) |
|
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] |
|
483 apply(auto simp add: fresh_star_def fresh_def) |
|
484 done |
470 |
485 |
471 end |
486 end |