78 done

    79 

    80 lemma Abs_lst_fcb2:

    81   fixes as bs :: "atom list"

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

    83     and c::"'c::fs"

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

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

    86   and fresh1: "set as \<sharp>* c"

    87   and fresh2: "set bs \<sharp>* c"

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

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

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

    91 proof -

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

    93     unfolding  supports_def fresh_def[symmetric]

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

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

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

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

    98     unfolding  supports_def fresh_def[symmetric]

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

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

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

   102   obtain q::"perm" where 

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

   104     fr2: "supp q \<sharp>* Abs_lst as x" and 

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

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

   107       fin1 fin2

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

   109   have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp

   110   also have "\<dots> = Abs_lst as x"

   111     by (simp only: fr2 perm_supp_eq)

   112   finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp

   113   then obtain r::perm where 

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

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

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

   117     apply(drule_tac sym)

   118     apply(simp only: Abs_eq_iff2 alphas)

   119     apply(erule exE)

   120     apply(erule conjE)+

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

   122     apply(simp add: set_eqvt)

   123     apply(blast)

   124     done

   125   have "(set as) \<sharp>* f as x c" 

   126     apply(rule fcb1)

   127     apply(rule fresh1)

   128     done

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

   130     by (simp add: permute_bool_def)

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

   132     apply(simp add: fresh_star_eqvt set_eqvt)

   133     apply(subst (asm) perm1)

   134     using inc fresh1 fr1

   135     apply(auto simp add: fresh_star_def fresh_Pair)

   136     done

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

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

   139     apply(simp add: fresh_star_eqvt set_eqvt)

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

   141     using qq3 fresh2 fr1

   142     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)

   143     done

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

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

   146     apply(rule perm_supp_eq[symmetric])

   147     using inc fcb1[OF fresh1] fr1 by (auto simp add: fresh_star_def)

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

   149     apply(rule perm1)

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

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

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

   153     apply(rule perm2[symmetric])

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

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

   156     apply(rule perm_supp_eq)

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

   158   finally show ?thesis by simp

   159 qed

   160 

   161 lemma Abs_lst1_fcb2:

   162   fixes a b :: "atom"

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

   164     and c::"'c :: fs"

   165   assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)"

   166   and fcb1: "a \<sharp> c \<Longrightarrow> a \<sharp> f a x c"

   167   and fresh: "{a, b} \<sharp>* c"

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

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

   170   shows "f a x c = f b y c"

   171 using e

   172 apply(drule_tac Abs_lst_fcb2[where c="c" and f="\<lambda>(as::atom list) . f (hd as)"])

   173 apply(simp_all)

   174 using fcb1 fresh perm1 perm2

   175 apply(simp_all add: fresh_star_def)