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