128 lemma Abs_res_fcb2:

   129   fixes as bs :: "atom set"

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

   131     and c::"'c::fs"

   132   assumes eq: "[as]res. x = [bs]res. y"

   133   and fin: "finite as" "finite bs"

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

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

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

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

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

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

   140 proof -

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

   142     unfolding  supports_def fresh_def[symmetric]

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

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

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

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

   147     unfolding  supports_def fresh_def[symmetric]

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

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

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

   151   obtain q::"perm" where 

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

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

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

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

   156       fin1 fin2 fin

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

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

   159   also have "\<dots> = [as]res. x"

   160     by (simp only: fr2 perm_supp_eq)

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

   162   then obtain r::perm where 

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

   164     qq2: "(q \<bullet> as \<inter> supp (q \<bullet> x)) = r \<bullet> (bs \<inter> supp y)" and 

   165     qq3: "supp r \<subseteq> bs \<inter> supp y \<union> q \<bullet> as \<inter> supp (q \<bullet> x)"

   166     apply(drule_tac sym)

   167     apply(subst(asm) Abs_eq_res_set)

   168     apply(simp only: Abs_eq_iff2 alphas)

   169     apply(erule exE)

   170     apply(erule conjE)+

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

   172     apply(simp add: set_eqvt)

   173     done

   174   have "(as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c" sorry (* FCB? *)

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

   176     by (simp add: permute_bool_def)

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

   178     apply(simp add: fresh_star_eqvt set_eqvt)

   179     sorry (* perm? *)

   180   then have "r \<bullet> (bs \<inter> supp y) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq2 apply (simp add: inter_eqvt)

   181   (* rest similar reversing it other way around... *)

   182   show ?thesis sorry

   183 qed

   184 

   185 

   290 lemma permute_length_eq:

   291   shows "p \<bullet> xs = ys \<Longrightarrow> length xs = length ys"

   292   by (auto simp add: length_eqvt[symmetric] permute_pure)

   293 

   303 

   304 lemma in_permute_list:

   305   shows "py \<bullet> p \<bullet> xs = px \<bullet> xs \<Longrightarrow>  x \<in> set xs \<Longrightarrow> py \<bullet> p \<bullet> x = px \<bullet> x"

   306   by (induct xs) auto

   307 

   308 

   309