48 

    49 lemma Abs_set_fcb2:

    50   fixes as bs :: "atom set"

    51     and x y :: "'b :: fs"

    52     and c::"'c::fs"

    53   assumes eq: "[as]set. x = [bs]set. y"

    54   and fin: "finite as" "finite bs"

    55   and fcb1: "as \<sharp>* f as x c"

    56   and fresh1: "as \<sharp>* c"

    57   and fresh2: "bs \<sharp>* c"

    58   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"

    59   and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"

    60   shows "f as x c = f bs y c"

    61 proof -

    62   have "supp (as, x, c) supports (f as x c)"

    63     unfolding  supports_def fresh_def[symmetric]

    64     by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh)

    65   then have fin1: "finite (supp (f as x c))"

    66     using fin by (auto intro: supports_finite simp add: finite_supp supp_of_finite_sets supp_Pair)

    67   have "supp (bs, y, c) supports (f bs y c)"

    68     unfolding  supports_def fresh_def[symmetric]

    69     by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh)

    70   then have fin2: "finite (supp (f bs y c))"

    71     using fin by (auto intro: supports_finite simp add: finite_supp supp_of_finite_sets supp_Pair)

    72   obtain q::"perm" where 

    73     fr1: "(q \<bullet> as) \<sharp>* (x, c, f as x c, f bs y c)" and 

    74     fr2: "supp q \<sharp>* ([as]set. x)" and 

    75     inc: "supp q \<subseteq> as \<union> (q \<bullet> as)"

    76     using at_set_avoiding3[where xs="as" and c="(x, c, f as x c, f bs y c)" and x="[as]set. x"]  

    77       fin1 fin2 fin

    78     by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv)

    79   have "[q \<bullet> as]set. (q \<bullet> x) = q \<bullet> ([as]set. x)" by simp

    80   also have "\<dots> = [as]set. x"

    81     by (simp only: fr2 perm_supp_eq)

    82   finally have "[q \<bullet> as]set. (q \<bullet> x) = [bs]set. y" using eq by simp

    83   then obtain r::perm where 

    84     qq1: "q \<bullet> x = r \<bullet> y" and 

    85     qq2: "q \<bullet> as = r \<bullet> bs" and 

    86     qq3: "supp r \<subseteq> (q \<bullet> as) \<union> bs"

    87     apply(drule_tac sym)

    88     apply(simp only: Abs_eq_iff2 alphas)

    89     apply(erule exE)

    90     apply(erule conjE)+

    91     apply(drule_tac x="p" in meta_spec)

    92     apply(simp add: set_eqvt)

    93     apply(blast)

    94     done

    95   have "as \<sharp>* f as x c" by (rule fcb1)

    96   then have "q \<bullet> (as \<sharp>* f as x c)"

    97     by (simp add: permute_bool_def)

    98   then have "(q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"

    99     apply(simp add: fresh_star_eqvt set_eqvt)

   100     apply(subst (asm) perm1)

   101     using inc fresh1 fr1

   102     apply(auto simp add: fresh_star_def fresh_Pair)

   103     done

   104   then have "(r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp

   105   then have "r \<bullet> (bs \<sharp>* f bs y c)"

   106     apply(simp add: fresh_star_eqvt set_eqvt)

   107     apply(subst (asm) perm2[symmetric])

   108     using qq3 fresh2 fr1

   109     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)

   110     done

   111   then have fcb2: "bs \<sharp>* f bs y c" by (simp add: permute_bool_def)

   112   have "f as x c = q \<bullet> (f as x c)"

   113     apply(rule perm_supp_eq[symmetric])

   114     using inc fcb1 fr1 by (auto simp add: fresh_star_def)

   115   also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" 

   116     apply(rule perm1)

   117     using inc fresh1 fr1 by (auto simp add: fresh_star_def)

   118   also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp

   119   also have "\<dots> = r \<bullet> (f bs y c)"

   120     apply(rule perm2[symmetric])

   121     using qq3 fresh2 fr1 by (auto simp add: fresh_star_def)

   122   also have "... = f bs y c"

   123     apply(rule perm_supp_eq)

   124     using qq3 fr1 fcb2 by (auto simp add: fresh_star_def)

   125   finally show ?thesis by simp

   126 qed

   127