139 and b: "finite (supp c)" |
139 and b: "finite (supp c)" |
140 obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))" |
140 obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))" |
141 using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"] |
141 using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"] |
142 unfolding fresh_star_def fresh_def by blast |
142 unfolding fresh_star_def fresh_def by blast |
143 |
143 |
|
144 lemma at_set_avoiding2: |
|
145 assumes "finite xs" |
|
146 and "finite (supp c)" "finite (supp x)" |
|
147 and "xs \<sharp>* x" |
|
148 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p" |
|
149 using assms |
|
150 apply(erule_tac c="(c, x)" in at_set_avoiding) |
|
151 apply(simp add: supp_Pair) |
|
152 apply(rule_tac x="p" in exI) |
|
153 apply(simp add: fresh_star_prod) |
|
154 apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x") |
|
155 apply(auto simp add: fresh_star_def fresh_def supp_perm)[1] |
|
156 apply(auto simp add: fresh_star_def fresh_def) |
|
157 done |
|
158 |
|
159 lemma at_set_avoiding2_atom: |
|
160 assumes "finite (supp c)" "finite (supp x)" |
|
161 and b: "xa \<sharp> x" |
|
162 shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p" |
|
163 proof - |
|
164 have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b) |
|
165 obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p" |
|
166 using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast |
|
167 have c: "(p \<bullet> xa) \<sharp> c" using p1 |
|
168 unfolding fresh_star_def Ball_def |
|
169 by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts) |
|
170 hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast |
|
171 then show ?thesis by blast |
|
172 qed |
144 |
173 |
145 section {* The freshness lemma according to Andrew Pitts *} |
174 section {* The freshness lemma according to Andrew Pitts *} |
146 |
|
147 lemma fresh_conv_MOST: |
|
148 shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)" |
|
149 unfolding fresh_def supp_def MOST_iff_cofinite by simp |
|
150 |
|
151 lemma fresh_apply: |
|
152 assumes "a \<sharp> f" and "a \<sharp> x" |
|
153 shows "a \<sharp> f x" |
|
154 using assms unfolding fresh_conv_MOST |
|
155 unfolding permute_fun_app_eq [where f=f] |
|
156 by (elim MOST_rev_mp, simp) |
|
157 |
175 |
158 lemma freshness_lemma: |
176 lemma freshness_lemma: |
159 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
177 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
160 assumes a: "\<exists>a. atom a \<sharp> (h, h a)" |
178 assumes a: "\<exists>a. atom a \<sharp> (h, h a)" |
161 shows "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" |
179 shows "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" |
171 assume "a = b" |
189 assume "a = b" |
172 thus "h a = h b" by simp |
190 thus "h a = h b" by simp |
173 next |
191 next |
174 assume "a \<noteq> b" |
192 assume "a \<noteq> b" |
175 hence "atom a \<sharp> b" by (simp add: fresh_at_base) |
193 hence "atom a \<sharp> b" by (simp add: fresh_at_base) |
176 with a3 have "atom a \<sharp> h b" by (rule fresh_apply) |
194 with a3 have "atom a \<sharp> h b" |
|
195 by (rule fresh_fun_app) |
177 with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)" |
196 with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)" |
178 by (rule swap_fresh_fresh) |
197 by (rule swap_fresh_fresh) |
179 from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h" |
198 from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h" |
180 by (rule swap_fresh_fresh) |
199 by (rule swap_fresh_fresh) |
181 from d1 have "h b = (atom b \<rightleftharpoons> atom a) \<bullet> (h b)" by simp |
200 from d1 have "h b = (atom b \<rightleftharpoons> atom a) \<bullet> (h b)" by simp |
445 have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+ |
464 have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+ |
446 then show "(p1 + p2) \<bullet> x = x" by simp |
465 then show "(p1 + p2) \<bullet> x = x" by simp |
447 qed |
466 qed |
448 qed |
467 qed |
449 |
468 |
450 section {* at_set_avoiding2 *} |
|
451 |
|
452 lemma at_set_avoiding2: |
|
453 assumes "finite xs" |
|
454 and "finite (supp c)" "finite (supp x)" |
|
455 and "xs \<sharp>* x" |
|
456 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p" |
|
457 using assms |
|
458 apply(erule_tac c="(c, x)" in at_set_avoiding) |
|
459 apply(simp add: supp_Pair) |
|
460 apply(rule_tac x="p" in exI) |
|
461 apply(simp add: fresh_star_prod) |
|
462 apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x") |
|
463 apply(auto simp add: fresh_star_def fresh_def supp_perm)[1] |
|
464 apply(auto simp add: fresh_star_def fresh_def) |
|
465 done |
|
466 |
|
467 lemma at_set_avoiding2_atom: |
|
468 assumes "finite (supp c)" "finite (supp x)" |
|
469 and b: "xa \<sharp> x" |
|
470 shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p" |
|
471 proof - |
|
472 have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b) |
|
473 obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p" |
|
474 using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast |
|
475 have c: "(p \<bullet> xa) \<sharp> c" using p1 |
|
476 unfolding fresh_star_def Ball_def |
|
477 by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts) |
|
478 hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast |
|
479 then show ?thesis by blast |
|
480 qed |
|
481 |
|
482 end |
469 end |