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

   221   and fcb1: "(as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c"

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

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

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

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

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

   226   shows "f (as \<inter> supp x) x c = f (bs \<inter> supp y) y c"

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

   228   have "supp (as, x, c) supports (f (as \<inter> supp x) x c)"

   230     unfolding  supports_def fresh_def[symmetric]

   229     unfolding  supports_def fresh_def[symmetric]

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

   230     by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh inter_eqvt supp_eqvt)

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

   231   then have fin1: "finite (supp (f (as \<inter> supp x) x c))"

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

   233   have "supp (bs, y, c) supports (f (bs \<inter> supp y) y c)"

   235     unfolding  supports_def fresh_def[symmetric]

   234     unfolding  supports_def fresh_def[symmetric]

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

   235     by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh inter_eqvt supp_eqvt)

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

   236   then have fin2: "finite (supp (f (bs \<inter> supp y) y c))"

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

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

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

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

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

   241     inc: "supp q \<subseteq> (as \<inter> supp x) \<union> (q \<bullet> (as \<inter> supp x))"

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

   242     using at_set_avoiding3[where xs="as \<inter> supp x" and c="(x, c, f (as \<inter> supp x) x c, f (bs \<inter> supp y) y c)" 

   243       and x="[as \<inter> supp x]set. x"]  

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

   245     apply (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv)

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

   246     done

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

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

   248   also have "\<dots> = [as \<inter> supp x]set. x"

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

   250   finally have "[q \<bullet> (as \<inter> supp x)]set. (q \<bullet> x) = [bs \<inter> supp y]set. y" using eq 

   251     by(simp add: Abs_eq_res_set)

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

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

   260     apply(simp add: set_eqvt)

   261     apply(simp add: set_eqvt inter_eqvt supp_eqvt)

   261     done

   262     done

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

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

   267     sorry (* perm? *)

   268     apply(subst (asm) perm1)

   268   then have "r \<bullet> (bs \<inter> supp y) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq2 

   269     using inc fresh1 fr1

   269     apply (simp add: inter_eqvt)

   270     apply(auto simp add: fresh_star_def fresh_Pair)

   270     sorry

   271     done

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

   272   then have "(r \<bullet> (bs \<inter> supp y)) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq1 qq2 

   272   show ?thesis sorry

   273     apply(perm_simp)

   274     apply simp

   275     done

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

   277     apply(simp add: fresh_star_eqvt set_eqvt)

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

   279     using qq3 fresh2 fr1

   280     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)

   281     done

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

   283   have "f (as \<inter> supp x) x c = q \<bullet> (f (as \<inter> supp x) x c)"

   284     apply(rule perm_supp_eq[symmetric])

   285     using inc fcb1 fr1 

   286     apply (auto simp add: fresh_star_def)

   287     done

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

   289     apply(rule perm1)

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

   291   also have "\<dots> = f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq1 qq2 

   292     apply(perm_simp)

   293     apply simp

   294     done

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

   296     apply(rule perm2[symmetric])

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

   298   also have "... = f (bs \<inter> supp y) y c"

   299     apply(rule perm_supp_eq)

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

   301   finally show ?thesis by simp

   274 *}

   303 

   275 

   304 typedef ('a::fs, 'b::fs) ffun = "{f::'a => 'b. finite (supp f)}"

   305 apply(subgoal_tac "\<exists>x::'b::fs. x \<in> (UNIV::('b::fs) set)")

   306 apply(erule exE)

   307 apply(rule_tac x="\<lambda>_. x" in exI)

   308 apply(auto)

   309 apply(rule_tac S="supp x" in supports_finite)

   310 apply(simp add: supports_def)

   311 apply(perm_simp)

   312 apply(simp add: fresh_def[symmetric])

   313 apply(simp add: swap_fresh_fresh)

   314 apply(simp add: finite_supp)

   315 done