98 

    99 lemma Abs_lst_fcb2:

   100   fixes as bs :: "'a :: fs"

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

   102     and c::"'c::fs"

   103   assumes eq: "[ba as]lst. x = [ba bs]lst. y"

   104   and fcb1: "(set (ba as)) \<sharp>* f as x c"

   105   and fresh1: "set (ba as) \<sharp>* c"

   106   and fresh2: "set (ba bs) \<sharp>* c"

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

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

   109   and props: "eqvt ba" "inj ba"

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

   111 proof -

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

   113     unfolding  supports_def fresh_def[symmetric]

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

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

   116     by (auto intro: supports_finite simp add: finite_supp)

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

   118     unfolding  supports_def fresh_def[symmetric]

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

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

   121     by (auto intro: supports_finite simp add: finite_supp)

   122   obtain q::"perm" where 

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

   124     fr2: "supp q \<sharp>* ([ba as]lst. x)" and 

   125     inc: "supp q \<subseteq> (set (ba as)) \<union> q \<bullet> (set (ba as))"

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

   127       fin1 fin2

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

   129   have "[q \<bullet> (ba as)]lst. (q \<bullet> x) = q \<bullet> ([ba as]lst. x)" by simp

   130   also have "\<dots> = [ba as]lst. x"

   131     by (simp only: fr2 perm_supp_eq)

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

   133   then obtain r::perm where 

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

   135     qq2: "q \<bullet> (ba as) = r \<bullet> (ba bs)" and 

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

   137     apply(drule_tac sym)

   138     apply(simp only: Abs_eq_iff2 alphas)

   139     apply(erule exE)

   140     apply(erule conjE)+

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

   142     apply(simp add: set_eqvt)

   143     apply(blast)

   144     done

   145   have qq4: "q \<bullet> as = r \<bullet> bs" using qq2 props unfolding eqvt_def inj_on_def

   146     apply(perm_simp)

   147     apply(simp)

   148     done

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

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

   151     by (simp add: permute_bool_def)

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

   153     apply(simp add: fresh_star_eqvt set_eqvt)

   154     apply(subst (asm) perm1)

   155     using inc fresh1 fr1

   156     apply(auto simp add: fresh_star_def fresh_Pair)

   157     done

   158   then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 qq4

   159     by simp

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

   161     apply(simp add: fresh_star_eqvt set_eqvt)

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

   163     using qq3 fresh2 fr1

   164     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)

   165     done

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

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

   168     apply(rule perm_supp_eq[symmetric])

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

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

   171     apply(rule perm1)

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

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

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

   175     apply(rule perm2[symmetric])

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

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

   178     apply(rule perm_supp_eq)

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

   180   finally show ?thesis by simp

   181 qed