equal
deleted
inserted
replaced
1244 |
1244 |
1245 definition |
1245 definition |
1246 fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80) |
1246 fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80) |
1247 where |
1247 where |
1248 "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x" |
1248 "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x" |
|
1249 |
|
1250 lemma fresh_star_supp_conv: |
|
1251 shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x" |
|
1252 by (auto simp add: fresh_star_def fresh_def) |
1249 |
1253 |
1250 lemma fresh_star_prod: |
1254 lemma fresh_star_prod: |
1251 fixes as::"atom set" |
1255 fixes as::"atom set" |
1252 shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" |
1256 shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" |
1253 by (auto simp add: fresh_star_def fresh_Pair) |
1257 by (auto simp add: fresh_star_def fresh_Pair) |
1480 using assms |
1484 using assms |
1481 apply(erule_tac c="(c, x)" in at_set_avoiding) |
1485 apply(erule_tac c="(c, x)" in at_set_avoiding) |
1482 apply(simp add: supp_Pair) |
1486 apply(simp add: supp_Pair) |
1483 apply(rule_tac x="p" in exI) |
1487 apply(rule_tac x="p" in exI) |
1484 apply(simp add: fresh_star_prod) |
1488 apply(simp add: fresh_star_prod) |
1485 apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x") |
1489 apply(rule fresh_star_supp_conv) |
1486 apply(auto simp add: fresh_star_def fresh_def supp_perm)[1] |
1490 apply(auto simp add: fresh_star_def) |
1487 apply(auto simp add: fresh_star_def fresh_def) |
|
1488 done |
1491 done |
1489 |
1492 |
1490 lemma at_set_avoiding2_atom: |
1493 lemma at_set_avoiding2_atom: |
1491 assumes "finite (supp c)" "finite (supp x)" |
1494 assumes "finite (supp c)" "finite (supp x)" |
1492 and b: "a \<sharp> x" |
1495 and b: "a \<sharp> x" |