theory Classical
imports "../Nominal2"
begin

lemma supp_zero_perm_zero:
  shows "supp (p :: perm) = {} \<longleftrightarrow> p = 0"
  by (metis supp_perm_singleton supp_zero_perm)

lemma permute_atom_list_id:
  shows "p \<bullet> l = l \<longleftrightarrow> supp p \<inter> set l = {}"
  by (induct l) (auto simp add: supp_Nil supp_perm)

lemma permute_length_eq:
  shows "p \<bullet> xs = ys \<Longrightarrow> length xs = length ys"
  by (auto simp add: length_eqvt[symmetric] permute_pure)

lemma Abs_lst_binder_length:
  shows "[xs]lst. T = [ys]lst. S \<Longrightarrow> length xs = length ys"
  by (auto simp add: Abs_eq_iff alphas length_eqvt[symmetric] permute_pure)

lemma Abs_lst_binder_eq:
  shows "Abs_lst l T = Abs_lst l S \<longleftrightarrow> T = S"
  by (rule, simp_all add: Abs_eq_iff2 alphas)
     (metis fresh_star_zero inf_absorb1 permute_atom_list_id supp_perm_eq
       supp_zero_perm_zero)

lemma in_permute_list:
  shows "py \<bullet> p \<bullet> xs = px \<bullet> xs \<Longrightarrow>  x \<in> set xs \<Longrightarrow> py \<bullet> p \<bullet> x = px \<bullet> x"
  by (induct xs) auto

lemma obtain_atom_list:
  assumes eq: "p \<bullet> xs = ys"
      and fin: "finite (supp c)"
      and sorts: "map sort_of xs = map sort_of ys"
  shows "\<exists>ds px py. (set ds \<sharp>* c) \<and> (px \<bullet> xs = ds) \<and> (py \<bullet> ys = ds)
    \<and> (supp px - set xs) \<sharp>* c \<and> (supp py - set ys) \<sharp>* c"
  sorry

lemma Abs_lst_fcb2:
  fixes S T :: "'b :: fs"
    and c::"'c::fs"
  assumes e: "[xs]lst. T = [ys]lst. S"
  and sorts: "map sort_of xs = map sort_of ys"
  and fcb1: "\<And>x. x \<in> set xs \<Longrightarrow> x \<sharp> f xs T c"
  and fcb2: "\<And>x. x \<in> set ys \<Longrightarrow> x \<sharp> f ys S c"
  and fresh: "(set xs \<union> set ys) \<sharp>* c"
  and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f xs T c) = f (p \<bullet> xs) (p \<bullet> T) c"
  and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f ys S c) = f (p \<bullet> ys) (p \<bullet> S) c"
  shows "f xs T c = f ys S c"
proof -
  have fin1: "finite (supp (f xs T c))"
    apply(rule_tac S="supp (xs, T, c)" in supports_finite)
    apply(simp add: supports_def)
    apply(simp add: fresh_def[symmetric])
    apply(clarify)
    apply(subst perm1)
    apply(simp add: supp_swap fresh_star_def)
    apply(simp add: swap_fresh_fresh fresh_Pair)
    apply(simp add: finite_supp)
    done
  have fin2: "finite (supp (f ys S c))"
    apply(rule_tac S="supp (ys, S, c)" in supports_finite)
    apply(simp add: supports_def)
    apply(simp add: fresh_def[symmetric])
    apply(clarify)
    apply(subst perm2)
    apply(simp add: supp_swap fresh_star_def)
    apply(simp add: swap_fresh_fresh fresh_Pair)
    apply(simp add: finite_supp)
    done
  obtain p :: perm where xs_ys: "p \<bullet> xs = ys" using e
    by (auto simp add: Abs_eq_iff alphas)
  obtain ds::"atom list" and px and py
    where fr: "set ds \<sharp>* (xs, ys, S, T, c, f xs T c, f ys S c)"
    and pxd: "px \<bullet> xs = ds"     and pyd: "py \<bullet> ys = ds"
    and spx: "(supp px - set xs) \<sharp>* (xs, ys, S, T, c, f xs T c, f ys S c)"
    and spy: "(supp py - set ys) \<sharp>* (xs, ys, S, T, c, f xs T c, f ys S c)"
    using obtain_atom_list[OF xs_ys, of "(xs, ys, S, T, c, f xs T c, f ys S c)"]
    sorts by (auto simp add: finite_supp supp_Pair fin1 fin2)
  have "px \<bullet> (Abs_lst xs T) = py \<bullet> (Abs_lst ys S)"
    apply (subst perm_supp_eq)
    using spx apply (auto simp add: fresh_star_def Abs_fresh_iff)[1]
    apply (subst perm_supp_eq)
    using spy apply (auto simp add: fresh_star_def Abs_fresh_iff)[1]
    by(rule e)
  then have "Abs_lst ds (px \<bullet> T) = Abs_lst ds (py \<bullet> S)" by (simp add: pxd pyd)
  then have eq: "px \<bullet> T = py \<bullet> S" by (simp add: Abs_lst_binder_eq)
  have "f xs T c = px \<bullet> f xs T c"
    apply(rule perm_supp_eq[symmetric])
    using spx unfolding fresh_star_def
    apply (intro ballI)
    by (case_tac "a \<in> set xs") (simp_all add: fcb1)
  also have "... = f (px \<bullet> xs) (px \<bullet> T) c"
    apply(rule perm1)
    using spx fresh unfolding fresh_star_def
    apply (intro ballI)
    by (case_tac "a \<in> set xs") (simp_all add: fcb1)
  also have "... = f (py \<bullet> ys) (py \<bullet> S) c" using eq pxd pyd by simp
  also have "... = py \<bullet> f ys S c"
    apply(rule perm2[symmetric])
    using spy fresh unfolding fresh_star_def
    apply (intro ballI)
    by (case_tac "a \<in> set ys") (simp_all add: fcb1)
  also have "... = f ys S c"
    apply(rule perm_supp_eq)
    using spy unfolding fresh_star_def
    apply (intro ballI)
    by (case_tac "a \<in> set ys") (simp_all add: fcb2)
  finally show ?thesis by simp
qed

end