1 (*  Title:      Nominal2_Supp

     2     Authors:    Brian Huffman, Christian Urban

     3 

     4     Supplementary Lemmas and Definitions for 

     5     Nominal Isabelle. 

     6 *)

     7 theory Nominal2_Supp

     8 imports Nominal2_Base Nominal2_Eqvt Nominal2_Atoms

     9 begin

    10 

    11 

    12 section {* Fresh-Star *}

    13 

    14 text {* The fresh-star generalisation of fresh is used in strong

    15   induction principles. *}

    16 

    17 definition 

    18   fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80)

    19 where 

    20   "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"

    21 

    22 lemma fresh_star_prod:

    23   fixes as::"atom set"

    24   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)"

    25   by (auto simp add: fresh_star_def fresh_Pair)

    26 

    27 lemma fresh_star_union:

    28   shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"

    29   by (auto simp add: fresh_star_def)

    30 

    31 lemma fresh_star_insert:

    32   shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)"

    33   by (auto simp add: fresh_star_def)

    34 

    35 lemma fresh_star_Un_elim:

    36   "((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)"

    37   unfolding fresh_star_def

    38   apply(rule)

    39   apply(erule meta_mp)

    40   apply(auto)

    41   done

    42 

    43 lemma fresh_star_insert_elim:

    44   "(insert a as \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> as \<sharp>* x \<Longrightarrow> PROP C)"

    45   unfolding fresh_star_def

    46   by rule (simp_all add: fresh_star_def)

    47 

    48 lemma fresh_star_empty_elim:

    49   "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C"

    50   by (simp add: fresh_star_def)

    51 

    52 lemma fresh_star_unit_elim: 

    53   shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"

    54   by (simp add: fresh_star_def fresh_unit) 

    55 

    56 lemma fresh_star_prod_elim: 

    57   shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"

    58   by (rule, simp_all add: fresh_star_prod)

    59 

    60 lemma fresh_star_plus:

    61   fixes p q::perm

    62   shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"

    63   unfolding fresh_star_def

    64   by (simp add: fresh_plus_perm)

    65 

    66 lemma fresh_star_permute_iff:

    67   shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"

    68   unfolding fresh_star_def

    69   by (metis mem_permute_iff permute_minus_cancel fresh_permute_iff)

    70 

    71 lemma fresh_star_eqvt:

    72   shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"

    73 unfolding fresh_star_def

    74 unfolding Ball_def

    75 apply(simp add: all_eqvt)

    76 apply(subst permute_fun_def)

    77 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)

    78 done

    79 

    80 section {* Avoiding of atom sets *}

    81 

    82 text {* 

    83   For every set of atoms, there is another set of atoms

    84   avoiding a finitely supported c and there is a permutation

    85   which 'translates' between both sets.

    86 *}

    87 

    88 lemma at_set_avoiding_aux:

    89   fixes Xs::"atom set"

    90   and   As::"atom set"

    91   assumes b: "Xs \<subseteq> As"

    92   and     c: "finite As"

    93   shows "\<exists>p. (p \<bullet> Xs) \<inter> As = {} \<and> (supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"

    94 proof -

    95   from b c have "finite Xs" by (rule finite_subset)

    96   then show ?thesis using b

    97   proof (induct rule: finite_subset_induct)

    98     case empty

    99     have "0 \<bullet> {} \<inter> As = {}" by simp

   100     moreover

   101     have "supp (0::perm) \<subseteq> {} \<union> 0 \<bullet> {}" by (simp add: supp_zero_perm)

   102     ultimately show ?case by blast

   103   next

   104     case (insert x Xs)

   105     then obtain p where

   106       p1: "(p \<bullet> Xs) \<inter> As = {}" and 

   107       p2: "supp p \<subseteq> (Xs \<union> (p \<bullet> Xs))" by blast

   108     from `x \<in> As` p1 have "x \<notin> p \<bullet> Xs" by fast

   109     with `x \<notin> Xs` p2 have "x \<notin> supp p" by fast

   110     hence px: "p \<bullet> x = x" unfolding supp_perm by simp

   111     have "finite (As \<union> p \<bullet> Xs)"

   112       using `finite As` `finite Xs`

   113       by (simp add: permute_set_eq_image)

   114     then obtain y where "y \<notin> (As \<union> p \<bullet> Xs)" "sort_of y = sort_of x"

   115       by (rule obtain_atom)

   116     hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "sort_of y = sort_of x"

   117       by simp_all

   118     let ?q = "(x \<rightleftharpoons> y) + p"

   119     have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)"

   120       unfolding insert_eqvt

   121       using `p \<bullet> x = x` `sort_of y = sort_of x`

   122       using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs`

   123       by (simp add: swap_atom swap_set_not_in)

   124     have "?q \<bullet> insert x Xs \<inter> As = {}"

   125       using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}`

   126       unfolding q by simp

   127     moreover

   128     have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs"

   129       using p2 unfolding q

   130       apply (intro subset_trans [OF supp_plus_perm])

   131       apply (auto simp add: supp_swap)

   132       done

   133     ultimately show ?case by blast

   134   qed

   135 qed

   136 

   137 lemma at_set_avoiding:

   138   assumes a: "finite Xs"

   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))"

   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

   143 

   144 

   145 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 

   158 lemma freshness_lemma:

   159   fixes h :: "'a::at \<Rightarrow> 'b::pt"

   160   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"

   161   shows  "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"

   162 proof -

   163   from a obtain b where a1: "atom b \<sharp> h" and a2: "atom b \<sharp> h b"

   164     by (auto simp add: fresh_Pair)

   165   show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"

   166   proof (intro exI allI impI)

   167     fix a :: 'a

   168     assume a3: "atom a \<sharp> h"

   169     show "h a = h b"

   170     proof (cases "a = b")

   171       assume "a = b"

   172       thus "h a = h b" by simp

   173     next

   174       assume "a \<noteq> b"

   175       hence "atom a \<sharp> b" by (simp add: fresh_at_base)

   176       with a3 have "atom a \<sharp> h b" by (rule fresh_apply)

   177       with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"

   178         by (rule swap_fresh_fresh)

   179       from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"

   180         by (rule swap_fresh_fresh)

   181       from d1 have "h b = (atom b \<rightleftharpoons> atom a) \<bullet> (h b)" by simp

   182       also have "\<dots> = ((atom b \<rightleftharpoons> atom a) \<bullet> h) ((atom b \<rightleftharpoons> atom a) \<bullet> b)"

   183         by (rule permute_fun_app_eq)

   184       also have "\<dots> = h a"

   185         using d2 by simp

   186       finally show "h a = h b"  by simp

   187     qed

   188   qed

   189 qed

   190 

   191 lemma freshness_lemma_unique:

   192   fixes h :: "'a::at \<Rightarrow> 'b::pt"

   193   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"

   194   shows "\<exists>!x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"

   195 proof (rule ex_ex1I)

   196   from a show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"

   197     by (rule freshness_lemma)

   198 next

   199   fix x y

   200   assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"

   201   assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y"

   202   from a x y show "x = y"

   203     by (auto simp add: fresh_Pair)

   204 qed

   205 

   206 text {* packaging the freshness lemma into a function *}

   207 

   208 definition

   209   fresh_fun :: "('a::at \<Rightarrow> 'b::pt) \<Rightarrow> 'b"

   210 where

   211   "fresh_fun h = (THE x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x)"

   212 

   213 lemma fresh_fun_app:

   214   fixes h :: "'a::at \<Rightarrow> 'b::pt"

   215   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"

   216   assumes b: "atom a \<sharp> h"

   217   shows "fresh_fun h = h a"

   218 unfolding fresh_fun_def

   219 proof (rule the_equality)

   220   show "\<forall>a'. atom a' \<sharp> h \<longrightarrow> h a' = h a"

   221   proof (intro strip)

   222     fix a':: 'a

   223     assume c: "atom a' \<sharp> h"

   224     from a have "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" by (rule freshness_lemma)

   225     with b c show "h a' = h a" by auto

   226   qed

   227 next

   228   fix fr :: 'b

   229   assume "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = fr"

   230   with b show "fr = h a" by auto

   231 qed

   232 

   233 lemma fresh_fun_app':

   234   fixes h :: "'a::at \<Rightarrow> 'b::pt"

   235   assumes a: "atom a \<sharp> h" "atom a \<sharp> h a"

   236   shows "fresh_fun h = h a"

   237   apply (rule fresh_fun_app)

   238   apply (auto simp add: fresh_Pair intro: a)

   239   done

   240 

   241 lemma fresh_fun_eqvt:

   242   fixes h :: "'a::at \<Rightarrow> 'b::pt"

   243   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"

   244   shows "p \<bullet> (fresh_fun h) = fresh_fun (p \<bullet> h)"

   245   using a

   246   apply (clarsimp simp add: fresh_Pair)

   247   apply (subst fresh_fun_app', assumption+)

   248   apply (drule fresh_permute_iff [where p=p, THEN iffD2])

   249   apply (drule fresh_permute_iff [where p=p, THEN iffD2])

   250   apply (simp add: atom_eqvt permute_fun_app_eq [where f=h])

   251   apply (erule (1) fresh_fun_app' [symmetric])

   252   done

   253 

   254 lemma fresh_fun_supports:

   255   fixes h :: "'a::at \<Rightarrow> 'b::pt"

   256   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"

   257   shows "(supp h) supports (fresh_fun h)"

   258   apply (simp add: supports_def fresh_def [symmetric])

   259   apply (simp add: fresh_fun_eqvt [OF a] swap_fresh_fresh)

   260   done

   261 

   262 notation fresh_fun (binder "FRESH " 10)

   263 

   264 lemma FRESH_f_iff:

   265   fixes P :: "'a::at \<Rightarrow> 'b::pure"

   266   fixes f :: "'b \<Rightarrow> 'c::pure"

   267   assumes P: "finite (supp P)"

   268   shows "(FRESH x. f (P x)) = f (FRESH x. P x)"

   269 proof -

   270   obtain a::'a where "atom a \<notin> supp P"

   271     using P by (rule obtain_at_base)

   272   hence "atom a \<sharp> P"

   273     by (simp add: fresh_def)

   274   show "(FRESH x. f (P x)) = f (FRESH x. P x)"

   275     apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])

   276     apply (cut_tac `atom a \<sharp> P`)

   277     apply (simp add: fresh_conv_MOST)

   278     apply (elim MOST_rev_mp, rule MOST_I, clarify)

   279     apply (simp add: permute_fun_def permute_pure expand_fun_eq)

   280     apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])

   281     apply (rule refl)

   282     done

   283 qed

   284 

   285 lemma FRESH_binop_iff:

   286   fixes P :: "'a::at \<Rightarrow> 'b::pure"

   287   fixes Q :: "'a::at \<Rightarrow> 'c::pure"

   288   fixes binop :: "'b \<Rightarrow> 'c \<Rightarrow> 'd::pure"

   289   assumes P: "finite (supp P)" 

   290   and     Q: "finite (supp Q)"

   291   shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)"

   292 proof -

   293   from assms have "finite (supp P \<union> supp Q)" by simp

   294   then obtain a::'a where "atom a \<notin> (supp P \<union> supp Q)"

   295     by (rule obtain_at_base)

   296   hence "atom a \<sharp> P" and "atom a \<sharp> Q"

   297     by (simp_all add: fresh_def)

   298   show ?thesis

   299     apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])

   300     apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)

   301     apply (simp add: fresh_conv_MOST)

   302     apply (elim MOST_rev_mp, rule MOST_I, clarify)

   303     apply (simp add: permute_fun_def permute_pure expand_fun_eq)

   304     apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])

   305     apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> Q` pure_fresh])

   306     apply (rule refl)

   307     done

   308 qed

   309 

   310 lemma FRESH_conj_iff:

   311   fixes P Q :: "'a::at \<Rightarrow> bool"

   312   assumes P: "finite (supp P)" and Q: "finite (supp Q)"

   313   shows "(FRESH x. P x \<and> Q x) \<longleftrightarrow> (FRESH x. P x) \<and> (FRESH x. Q x)"

   314 using P Q by (rule FRESH_binop_iff)

   315 

   316 lemma FRESH_disj_iff:

   317   fixes P Q :: "'a::at \<Rightarrow> bool"

   318   assumes P: "finite (supp P)" and Q: "finite (supp Q)"

   319   shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)"

   320 using P Q by (rule FRESH_binop_iff)

   321 

   322 

   323 section {* An example of a function without finite support *}

   324 

   325 primrec

   326   nat_of :: "atom \<Rightarrow> nat"

   327 where

   328   "nat_of (Atom s n) = n"

   329 

   330 lemma atom_eq_iff:

   331   fixes a b :: atom

   332   shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b"

   333   by (induct a, induct b, simp)

   334 

   335 lemma not_fresh_nat_of:

   336   shows "\<not> a \<sharp> nat_of"

   337 unfolding fresh_def supp_def

   338 proof (clarsimp)

   339   assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"

   340   hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})"

   341     by simp

   342   then obtain b where

   343     b1: "b \<noteq> a" and

   344     b2: "sort_of b = sort_of a" and

   345     b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of"

   346     by (rule obtain_atom) auto

   347   have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def)

   348   also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq)

   349   also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp

   350   also have "\<dots> = nat_of b" using b2 by simp

   351   finally have "nat_of a = nat_of b" by simp

   352   with b2 have "a = b" by (simp add: atom_eq_iff)

   353   with b1 show "False" by simp

   354 qed

   355 

   356 lemma supp_nat_of:

   357   shows "supp nat_of = UNIV"

   358   using not_fresh_nat_of [unfolded fresh_def] by auto

   359 

   360 

   361 section {* Support for sets of atoms *}

   362 

   363 lemma supp_finite_atom_set:

   364   fixes S::"atom set"

   365   assumes "finite S"

   366   shows "supp S = S"

   367   apply(rule finite_supp_unique)

   368   apply(simp add: supports_def)

   369   apply(simp add: swap_set_not_in)

   370   apply(rule assms)

   371   apply(simp add: swap_set_in)

   372 done

   373 

   374 

   375 section {* transpositions of permutations *}

   376 

   377 fun

   378   add_perm 

   379 where

   380   "add_perm [] = 0"

   381 | "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"

   382 

   383 lemma add_perm_append:

   384   shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"

   385 by (induct xs arbitrary: ys)

   386    (auto simp add: add_assoc)

   387 

   388 lemma perm_list_exists:

   389   fixes p::perm

   390   shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"

   391 apply(induct p taking: "\<lambda>p::perm. card (supp p)" rule: measure_induct)

   392 apply(rename_tac p)

   393 apply(case_tac "supp p = {}")

   394 apply(simp)

   395 apply(simp add: supp_perm)

   396 apply(rule_tac x="[]" in exI)

   397 apply(simp add: supp_Nil)

   398 apply(simp add: expand_perm_eq)

   399 apply(subgoal_tac "\<exists>x. x \<in> supp p")

   400 defer

   401 apply(auto)[1]

   402 apply(erule exE)

   403 apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec)

   404 apply(drule mp)

   405 defer

   406 apply(erule exE)

   407 apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI)

   408 apply(simp add: add_perm_append)

   409 apply(erule conjE)

   410 apply(drule sym)

   411 apply(simp)

   412 apply(simp add: expand_perm_eq)

   413 apply(simp add: supp_append)

   414 apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom)

   415 apply(rule conjI)

   416 prefer 2

   417 apply(auto)[1]

   418 apply (metis permute_atom_def_raw permute_minus_cancel(2))

   419 defer

   420 apply(rule psubset_card_mono)

   421 apply(simp add: finite_supp)

   422 apply(rule psubsetI)

   423 defer

   424 apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))")

   425 apply(blast)

   426 apply(simp add: supp_perm)

   427 defer

   428 apply(auto simp add: supp_perm)[1]

   429 apply(case_tac "x = xa")

   430 apply(simp)

   431 apply(case_tac "((- p) \<bullet> x) = xa")

   432 apply(simp)

   433 apply(case_tac "sort_of xa = sort_of x")

   434 apply(simp)

   435 apply(auto)[1]

   436 apply(simp)

   437 apply(simp)

   438 apply(subgoal_tac "{a. p \<bullet> (- p \<bullet> x \<rightleftharpoons> x) \<bullet> a \<noteq> a} \<subseteq> {a. p \<bullet> a \<noteq> a}")

   439 apply(blast)

   440 apply(auto simp add: supp_perm)[1]

   441 apply(case_tac "x = xa")

   442 apply(simp)

   443 apply(case_tac "((- p) \<bullet> x) = xa")

   444 apply(simp)

   445 apply(case_tac "sort_of xa = sort_of x")

   446 apply(simp)

   447 apply(auto)[1]

   448 apply(simp)

   449 apply(simp)

   450 done

   451 

   452 section {* Lemma about support and permutations *}

   453 

   454 lemma supp_perm_eq:

   455   assumes a: "(supp x) \<sharp>* p"

   456   shows "p \<bullet> x = x"

   457 proof -

   458   obtain xs where eq: "p = add_perm xs" and sub: "supp xs \<subseteq> supp p"

   459     using perm_list_exists by blast

   460   from a have "\<forall>a \<in> supp p. a \<sharp> x"

   461     by (auto simp add: fresh_star_def fresh_def supp_perm)

   462   with eq sub have "\<forall>a \<in> supp xs. a \<sharp> x" by auto

   463   then have "add_perm xs \<bullet> x = x" 

   464     by (induct xs rule: add_perm.induct)

   465        (simp_all add: supp_Cons supp_Pair supp_atom swap_fresh_fresh)

   466   then show "p \<bullet> x = x" using eq by simp

   467 qed

   468 

   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

   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 

   501 end