Theory Nominal2.Nominal2_Abs

theory Nominal2_Abs
imports Nominal2_Base
        "HOL-Library.Quotient_List"
        "HOL-Library.Quotient_Product"
begin


section ‹Abstractions›

fun
  alpha_set
where
  alpha_set[simp del]:
  "alpha_set (bs, x) R f p (cs, y) 
     f x - bs = f y - cs 
     (f x - bs) ♯* p 
     R (p  x) y 
     p  bs = cs"

fun
  alpha_res
where
  alpha_res[simp del]:
  "alpha_res (bs, x) R f p (cs, y) 
     f x - bs = f y - cs 
     (f x - bs) ♯* p 
     R (p  x) y"

fun
  alpha_lst
where
  alpha_lst[simp del]:
  "alpha_lst (bs, x) R f p (cs, y) 
     f x - set bs = f y - set cs 
     (f x - set bs) ♯* p 
     R (p  x) y 
     p  bs = cs"

lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps

notation
  alpha_set ("_ ≈set _ _ _ _" [100, 100, 100, 100, 100] 100) and
  alpha_res ("_ ≈res _ _ _ _" [100, 100, 100, 100, 100] 100) and
  alpha_lst ("_ ≈lst _ _ _ _" [100, 100, 100, 100, 100] 100)

section ‹Mono›

lemma [mono]:
  shows "R1  R2  alpha_set bs R1  alpha_set bs R2"
  and   "R1  R2  alpha_res bs R1  alpha_res bs R2"
  and   "R1  R2  alpha_lst cs R1  alpha_lst cs R2"
  by (case_tac [!] bs, case_tac [!] cs)
     (auto simp: le_fun_def le_bool_def alphas)

section ‹Equivariance›

lemma alpha_eqvt[eqvt]:
  shows "(bs, x) ≈set R f q (cs, y)  (p  bs, p  x) ≈set (p  R) (p  f) (p  q) (p  cs, p  y)"
  and   "(bs, x) ≈res R f q (cs, y)  (p  bs, p  x) ≈res (p  R) (p  f) (p  q) (p  cs, p  y)"
  and   "(ds, x) ≈lst R f q (es, y)  (p  ds, p  x) ≈lst (p  R) (p  f) (p  q) (p  es, p  y)"
  unfolding alphas
  unfolding permute_eqvt[symmetric]
  unfolding set_eqvt[symmetric]
  unfolding permute_fun_app_eq[symmetric]
  unfolding Diff_eqvt[symmetric]
  unfolding eq_eqvt[symmetric]
  unfolding fresh_star_eqvt[symmetric]
  by (auto simp only: permute_bool_def)

section ‹Equivalence›

lemma alpha_refl:
  assumes a: "R x x"
  shows "(bs, x) ≈set R f 0 (bs, x)"
  and   "(bs, x) ≈res R f 0 (bs, x)"
  and   "(cs, x) ≈lst R f 0 (cs, x)"
  using a
  unfolding alphas
  unfolding fresh_star_def
  by (simp_all add: fresh_zero_perm)

lemma alpha_sym:
  assumes a: "R (p  x) y  R (- p  y) x"
  shows "(bs, x) ≈set R f p (cs, y)  (cs, y) ≈set R f (- p) (bs, x)"
  and   "(bs, x) ≈res R f p (cs, y)  (cs, y) ≈res R f (- p) (bs, x)"
  and   "(ds, x) ≈lst R f p (es, y)  (es, y) ≈lst R f (- p) (ds, x)"
  unfolding alphas fresh_star_def
  using a
  by (auto simp: fresh_minus_perm)

lemma alpha_trans:
  assumes a: "R (p  x) y; R (q  y) z  R ((q + p)  x) z"
  shows "(bs, x) ≈set R f p (cs, y); (cs, y) ≈set R f q (ds, z)  (bs, x) ≈set R f (q + p) (ds, z)"
  and   "(bs, x) ≈res R f p (cs, y); (cs, y) ≈res R f q (ds, z)  (bs, x) ≈res R f (q + p) (ds, z)"
  and   "(es, x) ≈lst R f p (gs, y); (gs, y) ≈lst R f q (hs, z)  (es, x) ≈lst R f (q + p) (hs, z)"
  using a
  unfolding alphas fresh_star_def
  by (simp_all add: fresh_plus_perm)

lemma alpha_sym_eqvt:
  assumes a: "R (p  x) y  R y (p  x)"
  and     b: "p  R = R"
  shows "(bs, x) ≈set R f p (cs, y)  (cs, y) ≈set R f (- p) (bs, x)"
  and   "(bs, x) ≈res R f p (cs, y)  (cs, y) ≈res R f (- p) (bs, x)"
  and   "(ds, x) ≈lst R f p (es, y)  (es, y) ≈lst R f (- p) (ds, x)"
apply(auto intro!: alpha_sym)
apply(drule_tac [!] a)
apply(rule_tac [!] p="p" in permute_boolE)
apply(simp_all add: b permute_self)
done

lemma alpha_set_trans_eqvt:
  assumes b: "(cs, y) ≈set R f q (ds, z)"
  and     a: "(bs, x) ≈set R f p (cs, y)"
  and     d: "q  R = R"
  and     c: "R (p  x) y; R y (- q  z)  R (p  x) (- q  z)"
  shows "(bs, x) ≈set R f (q + p) (ds, z)"
apply(rule alpha_trans(1)[OF _ a b])
apply(drule c)
apply(rule_tac p="q" in permute_boolE)
apply(simp add: d permute_self)
apply(rotate_tac -1)
apply(drule_tac p="q" in permute_boolI)
apply(simp add: d permute_self permute_eqvt[symmetric])
done

lemma alpha_res_trans_eqvt:
  assumes  b: "(cs, y) ≈res R f q (ds, z)"
  and     a: "(bs, x) ≈res R f p (cs, y)"
  and     d: "q  R = R"
  and     c: "R (p  x) y; R y (- q  z)  R (p  x) (- q  z)"
  shows "(bs, x) ≈res R f (q + p) (ds, z)"
apply(rule alpha_trans(2)[OF _ a b])
apply(drule c)
apply(rule_tac p="q" in permute_boolE)
apply(simp add: d permute_self)
apply(rotate_tac -1)
apply(drule_tac p="q" in permute_boolI)
apply(simp add: d permute_self permute_eqvt[symmetric])
done

lemma alpha_lst_trans_eqvt:
  assumes b: "(cs, y) ≈lst R f q (ds, z)"
  and     a: "(bs, x) ≈lst R f p (cs, y)"
  and     d: "q  R = R"
  and     c: "R (p  x) y; R y (- q  z)  R (p  x) (- q  z)"
  shows "(bs, x) ≈lst R f (q + p) (ds, z)"
apply(rule alpha_trans(3)[OF _ a b])
apply(drule c)
apply(rule_tac p="q" in permute_boolE)
apply(simp add: d permute_self)
apply(rotate_tac -1)
apply(drule_tac p="q" in permute_boolI)
apply(simp add: d permute_self permute_eqvt[symmetric])
done

lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt


section ‹General Abstractions›

fun
  alpha_abs_set
where
  [simp del]:
  "alpha_abs_set (bs, x) (cs, y)  (p. (bs, x) ≈set ((=)) supp p (cs, y))"

fun
  alpha_abs_lst
where
  [simp del]:
  "alpha_abs_lst (bs, x) (cs, y)  (p. (bs, x) ≈lst ((=)) supp p (cs, y))"

fun
  alpha_abs_res
where
  [simp del]:
  "alpha_abs_res (bs, x) (cs, y)  (p. (bs, x) ≈res ((=)) supp p (cs, y))"

notation
  alpha_abs_set (infix "≈abs'_set" 50) and
  alpha_abs_lst (infix "≈abs'_lst" 50) and
  alpha_abs_res (infix "≈abs'_res" 50)

lemmas alphas_abs = alpha_abs_set.simps alpha_abs_res.simps alpha_abs_lst.simps


lemma alphas_abs_refl:
  shows "(bs, x) ≈abs_set (bs, x)"
  and   "(bs, x) ≈abs_res (bs, x)"
  and   "(cs, x) ≈abs_lst (cs, x)"
  unfolding alphas_abs
  unfolding alphas
  unfolding fresh_star_def
  by (rule_tac [!] x="0" in exI)
     (simp_all add: fresh_zero_perm)

lemma alphas_abs_sym:
  shows "(bs, x) ≈abs_set (cs, y)  (cs, y) ≈abs_set (bs, x)"
  and   "(bs, x) ≈abs_res (cs, y)  (cs, y) ≈abs_res (bs, x)"
  and   "(ds, x) ≈abs_lst (es, y)  (es, y) ≈abs_lst (ds, x)"
  unfolding alphas_abs
  unfolding alphas
  unfolding fresh_star_def
  by (erule_tac [!] exE, rule_tac [!] x="-p" in exI)
     (auto simp: fresh_minus_perm)

lemma alphas_abs_trans:
  shows "(bs, x) ≈abs_set (cs, y); (cs, y) ≈abs_set (ds, z)  (bs, x) ≈abs_set (ds, z)"
  and   "(bs, x) ≈abs_res (cs, y); (cs, y) ≈abs_res (ds, z)  (bs, x) ≈abs_res (ds, z)"
  and   "(es, x) ≈abs_lst (gs, y); (gs, y) ≈abs_lst (hs, z)  (es, x) ≈abs_lst (hs, z)"
  unfolding alphas_abs
  unfolding alphas
  unfolding fresh_star_def
  apply(erule_tac [!] exE, erule_tac [!] exE)
  apply(rule_tac [!] x="pa + p" in exI)
  by (simp_all add: fresh_plus_perm)

lemma alphas_abs_eqvt:
  shows "(bs, x) ≈abs_set (cs, y)  (p  bs, p  x) ≈abs_set (p  cs, p  y)"
  and   "(bs, x) ≈abs_res (cs, y)  (p  bs, p  x) ≈abs_res (p  cs, p  y)"
  and   "(ds, x) ≈abs_lst (es, y)  (p  ds, p  x) ≈abs_lst (p  es, p  y)"
  unfolding alphas_abs
  unfolding alphas
  unfolding set_eqvt[symmetric]
  unfolding supp_eqvt[symmetric]
  unfolding Diff_eqvt[symmetric]
  apply(erule_tac [!] exE)
  apply(rule_tac [!] x="p  pa" in exI)
  by (auto simp only: fresh_star_permute_iff permute_eqvt[symmetric])


section ‹Strengthening the equivalence›

lemma disjoint_right_eq:
  assumes a: "A  B1 = A  B2"
  and     b: "A  B1 = {}" "A  B2 = {}"
  shows "B1 = B2"
using a b
by (metis Int_Un_distrib2 Int_absorb2 Int_commute Un_upper2)

lemma supp_property_res:
  assumes a: "(as, x) ≈res (=) supp p (as', x')"
  shows "p  (supp x  as) = supp x'  as'"
proof -
  from a have "(supp x - as) ♯* p" by  (auto simp only: alphas)
  then have *: "p  (supp x - as) = (supp x - as)"
    by (simp add: atom_set_perm_eq)
  have "(supp x' - as')  (supp x'  as') = supp x'" by auto
  also have " = supp (p  x)" using a by (simp add: alphas)
  also have " = p  (supp x)" by (simp add: supp_eqvt)
  also have " = p  ((supp x - as)  (supp x  as))" by auto
  also have " = (p  (supp x - as))  (p  (supp x  as))" by (simp add: union_eqvt)
  also have " = (supp x - as)  (p  (supp x  as))" using * by simp
  also have " = (supp x' - as')  (p  (supp x  as))" using a by (simp add: alphas)
  finally have "(supp x' - as')  (supp x'  as') = (supp x' - as')  (p  (supp x  as))" .
  moreover
  have "(supp x' - as')  (supp x'  as') = {}" by auto
  moreover
  have "(supp x - as)  (supp x  as) = {}" by auto
  then have "p  ((supp x - as)  (supp x  as) = {})" by (simp add: permute_bool_def)
  then have "(p  (supp x - as))  (p  (supp x  as)) = {}" by (perm_simp) (simp)
  then have "(supp x - as)  (p  (supp x  as)) = {}" using * by simp
  then have "(supp x' - as')  (p  (supp x  as)) = {}" using a by (simp add: alphas)
  ultimately show "p  (supp x  as) = supp x'  as'"
    by (auto dest: disjoint_right_eq)
qed

lemma alpha_abs_res_stronger1_aux:
  assumes asm: "(as, x) ≈res (=) supp p' (as', x')"
  shows "p. (as, x) ≈res (=) supp p (as', x')  supp p  (supp x  as)  (supp x'  as')"
proof -
  from asm have 0: "(supp x - as) ♯* p'" by  (auto simp only: alphas)
  then have #: "p'  (supp x - as) = (supp x - as)"
    by (simp add: atom_set_perm_eq)
  obtain p where *: "b  supp x. p  b = p'  b" and **: "supp p  supp x  p'  supp x"
    using set_renaming_perm2 by blast
  from * have a: "p  x = p'  x" using supp_perm_perm_eq by auto
  from 0 have 1: "(supp x - as) ♯* p" using *
    by (auto simp: fresh_star_def fresh_perm)
  then have 2: "(supp x - as)  supp p = {}"
    by (auto simp: fresh_star_def fresh_def)
  have b: "supp x = (supp x - as)  (supp x  as)" by auto
  have "supp p  supp x  p'  supp x" using ** by simp
  also have " = (supp x - as)  (supp x  as)  (p'  ((supp x - as)  (supp x  as)))"
    using b by simp
  also have " = (supp x - as)  (supp x  as)  ((p'  (supp x - as))  (p'  (supp x  as)))"
    by (simp add: union_eqvt)
  also have " = (supp x - as)  (supp x  as)  (p'  (supp x  as))"
    using # by auto
  also have " = (supp x - as)  (supp x  as)  (supp x'  as')" using asm
    by (simp add: supp_property_res)
  finally have "supp p  (supp x - as)  (supp x  as)  (supp x'  as')" .
  then
  have "supp p  (supp x  as)  (supp x'  as')" using 2 by auto
  moreover
  have "(as, x) ≈res (=) supp p (as', x')" using asm 1 a by (simp add: alphas)
  ultimately
  show "p. (as, x) ≈res (=) supp p (as', x')  supp p  (supp x  as)  (supp x'  as')" by blast
qed

lemma alpha_abs_res_minimal:
  assumes asm: "(as, x) ≈res (=) supp p (as', x')"
  shows "(as  supp x, x) ≈res (=) supp p (as'  supp x', x')"
  using asm unfolding alpha_res by (auto simp: Diff_Int)

lemma alpha_abs_res_abs_set:
  assumes asm: "(as, x) ≈res (=) supp p (as', x')"
  shows "(as  supp x, x) ≈set (=) supp p (as'  supp x', x')"
proof -
  have c: "p  x = x'"
    using alpha_abs_res_minimal[OF asm] unfolding alpha_res by clarify
  then have a: "supp x - as  supp x = supp (p  x) - as'  supp (p  x)"
    using alpha_abs_res_minimal[OF asm] by (simp add: alpha_res)
  have b: "(supp x - as  supp x) ♯* p"
    using alpha_abs_res_minimal[OF asm] unfolding alpha_res by clarify
  have "p  (as  supp x) = as'  supp (p  x)"
    by (metis Int_commute asm c supp_property_res)
  then show ?thesis using a b c unfolding alpha_set by simp
qed

lemma alpha_abs_set_abs_res:
  assumes asm: "(as  supp x, x) ≈set (=) supp p (as'  supp x', x')"
  shows "(as, x) ≈res (=) supp p (as', x')"
  using asm unfolding alphas by (auto simp: Diff_Int)

lemma alpha_abs_res_stronger1:
  assumes asm: "(as, x) ≈res (=) supp p' (as', x')"
  shows "p. (as, x) ≈res (=) supp p (as', x')  supp p  as  as'"
using alpha_abs_res_stronger1_aux[OF asm] by auto

lemma alpha_abs_set_stronger1:
  assumes asm: "(as, x) ≈set (=) supp p' (as', x')"
  shows "p. (as, x) ≈set (=) supp p (as', x')  supp p  as  as'"
proof -
  from asm have 0: "(supp x - as) ♯* p'" by  (auto simp only: alphas)
  then have #: "p'  (supp x - as) = (supp x - as)"
    by (simp add: atom_set_perm_eq)
  obtain p where *: "b  (supp x  as). p  b = p'  b"
    and **: "supp p  (supp x  as)  p'  (supp x  as)"
    using set_renaming_perm2 by blast
  from * have "b  supp x. p  b = p'  b" by blast
  then have a: "p  x = p'  x" using supp_perm_perm_eq by auto
  from * have "b  as. p  b = p'  b" by blast
  then have zb: "p  as = p'  as"
    apply(auto simp: permute_set_def)
    apply(rule_tac x="xa" in exI)
    apply(simp)
    done
  have zc: "p'  as = as'" using asm by (simp add: alphas)
  from 0 have 1: "(supp x - as) ♯* p" using *
    by (auto simp: fresh_star_def fresh_perm)
  then have 2: "(supp x - as)  supp p = {}"
    by (auto simp: fresh_star_def fresh_def)
  have b: "supp x = (supp x - as)  (supp x  as)" by auto
  have "supp p  supp x  as  p'  supp x  p'  as" using ** using union_eqvt by blast
  also have " = (supp x - as)  (supp x  as)  as  (p'  ((supp x - as)  (supp x  as)))  p'  as"
    using b by simp
  also have " = (supp x - as)  (supp x  as)  as 
    ((p'  (supp x - as))  (p'  (supp x  as)))  p'  as" by (simp add: union_eqvt)
  also have " = (supp x - as)  (supp x  as)  as  (p'  (supp x  as))  p'  as"
    using # by auto
  also have " = (supp x - as)  (supp x  as)  as  p'  ((supp x  as)  as)" using union_eqvt
    by auto
  also have " = (supp x - as)  (supp x  as)  as  p'  as"
    by (metis Int_commute Un_commute sup_inf_absorb)
  also have " = (supp x - as)  as  p'  as" by blast
  finally have "supp p  (supp x - as)  as  p'  as" .
  then have "supp p  as  p'  as" using 2 by blast
  moreover
  have "(as, x) ≈set (=) supp p (as', x')" using asm 1 a zb by (simp add: alphas)
  ultimately
  show "p. (as, x) ≈set (=) supp p (as', x')  supp p  as  as'" using zc by blast
qed

lemma alpha_abs_lst_stronger1:
  assumes asm: "(as, x) ≈lst (=) supp p' (as', x')"
  shows "p. (as, x) ≈lst (=) supp p (as', x')  supp p  set as  set as'"
proof -
  from asm have 0: "(supp x - set as) ♯* p'" by  (auto simp only: alphas)
  then have #: "p'  (supp x - set as) = (supp x - set as)"
    by (simp add: atom_set_perm_eq)
  obtain p where *: "b  (supp x  set as). p  b = p'  b"
    and **: "supp p  (supp x  set as)  p'  (supp x  set as)"
    using set_renaming_perm2 by blast
  from * have "b  supp x. p  b = p'  b" by blast
  then have a: "p  x = p'  x" using supp_perm_perm_eq by auto
  from * have "b  set as. p  b = p'  b" by blast
  then have zb: "p  as = p'  as" by (induct as) (auto)
  have zc: "p'  set as = set as'" using asm by (simp add: alphas set_eqvt)
  from 0 have 1: "(supp x - set as) ♯* p" using *
    by (auto simp: fresh_star_def fresh_perm)
  then have 2: "(supp x - set as)  supp p = {}"
    by (auto simp: fresh_star_def fresh_def)
  have b: "supp x = (supp x - set as)  (supp x  set as)" by auto
  have "supp p  supp x  set as  p'  supp x  p'  set as" using ** using union_eqvt by blast
  also have " = (supp x - set as)  (supp x  set as)  set as 
    (p'  ((supp x - set as)  (supp x  set as)))  p'  set as" using b by simp
  also have " = (supp x - set as)  (supp x  set as)  set as 
    ((p'  (supp x - set as))  (p'  (supp x  set as)))  p'  set as" by (simp add: union_eqvt)
  also have " = (supp x - set as)  (supp x  set as)  set as 
    (p'  (supp x  set as))  p'  set as" using # by auto
  also have " = (supp x - set as)  (supp x  set as)  set as  p'  ((supp x  set as)  set as)"
    using union_eqvt by auto
  also have " = (supp x - set as)  (supp x  set as)  set as  p'  set as"
    by (metis Int_commute Un_commute sup_inf_absorb)
  also have " = (supp x - set as)  set as  p'  set as" by blast
  finally have "supp p  (supp x - set as)  set as  p'  set as" .
  then have "supp p  set as  p'  set as" using 2 by blast
  moreover
  have "(as, x) ≈lst (=) supp p (as', x')" using asm 1 a zb by (simp add: alphas)
  ultimately
  show "p. (as, x) ≈lst (=) supp p (as', x')  supp p  set as  set as'" using zc by blast
qed

lemma alphas_abs_stronger:
  shows "(as, x) ≈abs_set (as', x')  (p. (as, x) ≈set (=) supp p (as', x')  supp p  as  as')"
  and   "(as, x) ≈abs_res (as', x')  (p. (as, x) ≈res (=) supp p (as', x')  supp p  as  as')"
  and   "(bs, x) ≈abs_lst (bs', x') 
   (p. (bs, x) ≈lst (=) supp p (bs', x')  supp p  set bs  set bs')"
apply(rule iffI)
apply(auto simp: alphas_abs alpha_abs_set_stronger1)[1]
apply(auto simp: alphas_abs)[1]
apply(rule iffI)
apply(auto simp: alphas_abs alpha_abs_res_stronger1)[1]
apply(auto simp: alphas_abs)[1]
apply(rule iffI)
apply(auto simp: alphas_abs alpha_abs_lst_stronger1)[1]
apply(auto simp: alphas_abs)[1]
done

lemma alpha_res_alpha_set:
  "(bs, x) ≈res (=) supp p (cs, y)  (bs  supp x, x) ≈set (=) supp p (cs  supp y, y)"
  using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast

section ‹Quotient types›

quotient_type
    'a abs_set = "(atom set × 'a::pt)" / "alpha_abs_set"
  apply(rule equivpI)
  unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
  by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)

quotient_type
    'b abs_res = "(atom set × 'b::pt)" / "alpha_abs_res"
  apply(rule equivpI)
  unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
  by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)

quotient_type
   'c abs_lst = "(atom list × 'c::pt)" / "alpha_abs_lst"
  apply(rule_tac [!] equivpI)
  unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
  by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)

quotient_definition
  Abs_set ("[_]set. _" [60, 60] 60)
where
  "Abs_set::atom set  ('a::pt)  'a abs_set"
is
  "Pair::atom set  ('a::pt)  (atom set × 'a)" .

quotient_definition
  Abs_res ("[_]res. _" [60, 60] 60)
where
  "Abs_res::atom set  ('a::pt)  'a abs_res"
is
  "Pair::atom set  ('a::pt)  (atom set × 'a)" .

quotient_definition
  Abs_lst ("[_]lst. _" [60, 60] 60)
where
  "Abs_lst::atom list  ('a::pt)  'a abs_lst"
is
  "Pair::atom list  ('a::pt)  (atom list × 'a)" .

lemma [quot_respect]:
  shows "((=) ===> (=) ===> alpha_abs_set) Pair Pair"
  and   "((=) ===> (=) ===> alpha_abs_res) Pair Pair"
  and   "((=) ===> (=) ===> alpha_abs_lst) Pair Pair"
  unfolding rel_fun_def
  by (auto intro: alphas_abs_refl)

lemma [quot_respect]:
  shows "((=) ===> alpha_abs_set ===> alpha_abs_set) permute permute"
  and   "((=) ===> alpha_abs_res ===> alpha_abs_res) permute permute"
  and   "((=) ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
  unfolding rel_fun_def
  by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)

lemma Abs_eq_iff:
  shows "[bs]set. x = [bs']set. y  (p. (bs, x) ≈set (=) supp p (bs', y))"
  and   "[bs]res. x = [bs']res. y  (p. (bs, x) ≈res (=) supp p (bs', y))"
  and   "[cs]lst. x = [cs']lst. y  (p. (cs, x) ≈lst (=) supp p (cs', y))"
  by (lifting alphas_abs)

lemma Abs_eq_iff2:
  shows "[bs]set. x = [bs']set. y  (p. (bs, x) ≈set ((=)) supp p (bs', y)  supp p  bs  bs')"
  and   "[bs]res. x = [bs']res. y  (p. (bs, x) ≈res ((=)) supp p (bs', y)  supp p  bs  bs')"
  and   "[cs]lst. x = [cs']lst. y  (p. (cs, x) ≈lst ((=)) supp p (cs', y)  supp p  set cs  set cs')"
  by (lifting alphas_abs_stronger)


lemma Abs_eq_res_set:
  shows "[bs]res. x = [cs]res. y  [bs  supp x]set. x = [cs  supp y]set. y"
  unfolding Abs_eq_iff alpha_res_alpha_set by rule

lemma Abs_eq_res_supp:
  assumes asm: "supp x  bs"
  shows "[as]res. x = [as  bs]res. x"
  unfolding Abs_eq_iff alphas
  apply (rule_tac x="0::perm" in exI)
  apply (simp add: fresh_star_zero)
  using asm by blast

lemma Abs_exhausts[cases type]:
  shows "(as (x::'a::pt). y1 = [as]set. x  P1)  P1"
  and   "(as (x::'a::pt). y2 = [as]res. x  P2)  P2"
  and   "(bs (x::'a::pt). y3 = [bs]lst. x  P3)  P3"
  by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"]
              prod.exhaust[where 'a="atom set" and 'b="'a"]
              prod.exhaust[where 'a="atom list" and 'b="'a"])

instantiation abs_set :: (pt) pt
begin

quotient_definition
  "permute_abs_set::perm  ('a::pt abs_set)  'a abs_set"
is
  "permute:: perm  (atom set × 'a::pt)  (atom set × 'a::pt)"
  by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)

lemma permute_Abs_set[simp]:
  fixes x::"'a::pt"
  shows "(p  ([as]set. x)) = [p  as]set. (p  x)"
  by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])

instance
  apply standard
  apply(case_tac [!] x)
  apply(simp_all)
  done

end

instantiation abs_res :: (pt) pt
begin

quotient_definition
  "permute_abs_res::perm  ('a::pt abs_res)  'a abs_res"
is
  "permute:: perm  (atom set × 'a::pt)  (atom set × 'a::pt)"
  by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)

lemma permute_Abs_res[simp]:
  fixes x::"'a::pt"
  shows "(p  ([as]res. x)) = [p  as]res. (p  x)"
  by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])

instance
  apply standard
  apply(case_tac [!] x)
  apply(simp_all)
  done

end

instantiation abs_lst :: (pt) pt
begin

quotient_definition
  "permute_abs_lst::perm  ('a::pt abs_lst)  'a abs_lst"
is
  "permute:: perm  (atom list × 'a::pt)  (atom list × 'a::pt)"
  by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)

lemma permute_Abs_lst[simp]:
  fixes x::"'a::pt"
  shows "(p  ([as]lst. x)) = [p  as]lst. (p  x)"
  by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"])

instance
  apply standard
  apply(case_tac [!] x)
  apply(simp_all)
  done

end

lemmas permute_Abs[eqvt] = permute_Abs_set permute_Abs_res permute_Abs_lst


lemma Abs_swap1:
  assumes a1: "a  (supp x) - bs"
  and     a2: "b  (supp x) - bs"
  shows "[bs]set. x = [(a  b)  bs]set. ((a  b)  x)"
  and   "[bs]res. x = [(a  b)  bs]res. ((a  b)  x)"
  unfolding Abs_eq_iff
  unfolding alphas
  unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
  unfolding fresh_star_def fresh_def
  unfolding swap_set_not_in[OF a1 a2]
  using a1 a2
  by (rule_tac [!] x="(a  b)" in exI)
     (auto simp: supp_perm swap_atom)

lemma Abs_swap2:
  assumes a1: "a  (supp x) - (set bs)"
  and     a2: "b  (supp x) - (set bs)"
  shows "[bs]lst. x = [(a  b)  bs]lst. ((a  b)  x)"
  unfolding Abs_eq_iff
  unfolding alphas
  unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
  unfolding fresh_star_def fresh_def
  unfolding swap_set_not_in[OF a1 a2]
  using a1 a2
  by (rule_tac [!] x="(a  b)" in exI)
     (auto simp: supp_perm swap_atom)

lemma Abs_supports:
  shows "((supp x) - as) supports ([as]set. x)"
  and   "((supp x) - as) supports ([as]res. x)"
  and   "((supp x) - set bs) supports ([bs]lst. x)"
  unfolding supports_def
  unfolding permute_Abs
  by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric])

function
  supp_set  :: "('a::pt) abs_set  atom set" and
  supp_res :: "('a::pt) abs_res  atom set" and
  supp_lst :: "('a::pt) abs_lst  atom set"
where
  "supp_set ([as]set. x) = supp x - as"
| "supp_res ([as]res. x) = supp x - as"
| "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
apply(simp_all add: Abs_eq_iff alphas_abs alphas)
apply(case_tac x)
apply(case_tac a)
apply(simp)
apply(case_tac b)
apply(case_tac a)
apply(simp)
apply(case_tac ba)
apply(simp)
done

termination
  by lexicographic_order

lemma supp_funs_eqvt[eqvt]:
  shows "(p  supp_set x) = supp_set (p  x)"
  and   "(p  supp_res y) = supp_res (p  y)"
  and   "(p  supp_lst z) = supp_lst (p  z)"
  apply(case_tac x)
  apply(simp)
  apply(case_tac y)
  apply(simp)
  apply(case_tac z)
  apply(simp)
  done

lemma Abs_fresh_aux:
  shows "a  [bs]set. x  a  supp_set ([bs]set. x)"
  and   "a  [bs]res. x  a  supp_res ([bs]res. x)"
  and   "a  [cs]lst. x  a  supp_lst ([cs]lst. x)"
  by (rule_tac [!] fresh_fun_eqvt_app)
     (auto simp only: eqvt_def eqvts_raw)

lemma Abs_supp_subset1:
  assumes a: "finite (supp x)"
  shows "(supp x) - as  supp ([as]set. x)"
  and   "(supp x) - as  supp ([as]res. x)"
  and   "(supp x) - (set bs)  supp ([bs]lst. x)"
  unfolding supp_conv_fresh
  by (auto dest!: Abs_fresh_aux)
     (simp_all add: fresh_def supp_finite_atom_set a)

lemma Abs_supp_subset2:
  assumes a: "finite (supp x)"
  shows "supp ([as]set. x)  (supp x) - as"
  and   "supp ([as]res. x)  (supp x) - as"
  and   "supp ([bs]lst. x)  (supp x) - (set bs)"
  by (rule_tac [!] supp_is_subset)
     (simp_all add: Abs_supports a)

lemma Abs_finite_supp:
  assumes a: "finite (supp x)"
  shows "supp ([as]set. x) = (supp x) - as"
  and   "supp ([as]res. x) = (supp x) - as"
  and   "supp ([bs]lst. x) = (supp x) - (set bs)"
using Abs_supp_subset1[OF a] Abs_supp_subset2[OF a]
  by blast+

lemma supp_Abs:
  fixes x::"'a::fs"
  shows "supp ([as]set. x) = (supp x) - as"
  and   "supp ([as]res. x) = (supp x) - as"
  and   "supp ([bs]lst. x) = (supp x) - (set bs)"
by (simp_all add: Abs_finite_supp finite_supp)

instance abs_set :: (fs) fs
  apply standard
  apply(case_tac x)
  apply(simp add: supp_Abs finite_supp)
  done

instance abs_res :: (fs) fs
  apply standard
  apply(case_tac x)
  apply(simp add: supp_Abs finite_supp)
  done

instance abs_lst :: (fs) fs
  apply standard
  apply(case_tac x)
  apply(simp add: supp_Abs finite_supp)
  done

lemma Abs_fresh_iff:
  fixes x::"'a::fs"
  shows "a  [bs]set. x  a  bs  (a  bs  a  x)"
  and   "a  [bs]res. x  a  bs  (a  bs  a  x)"
  and   "a  [cs]lst. x  a  (set cs)  (a  (set cs)  a  x)"
  unfolding fresh_def
  unfolding supp_Abs
  by auto

lemma Abs_fresh_star_iff:
  fixes x::"'a::fs"
  shows "as ♯* ([bs]set. x)  (as - bs) ♯* x"
  and   "as ♯* ([bs]res. x)  (as - bs) ♯* x"
  and   "as ♯* ([cs]lst. x)  (as - set cs) ♯* x"
  unfolding fresh_star_def
  by (auto simp: Abs_fresh_iff)

lemma Abs_fresh_star:
  fixes x::"'a::fs"
  shows "as  as'  as ♯* ([as']set. x)"
  and   "as  as'  as ♯* ([as']res. x)"
  and   "bs  set bs'  bs ♯* ([bs']lst. x)"
  unfolding fresh_star_def
  by(auto simp: Abs_fresh_iff)

lemma Abs_fresh_star2:
  fixes x::"'a::fs"
  shows "as  bs = {}  as ♯* ([bs]set. x)  as ♯* x"
  and   "as  bs = {}  as ♯* ([bs]res. x)  as ♯* x"
  and   "cs  set ds = {}  cs ♯* ([ds]lst. x)  cs ♯* x"
  unfolding fresh_star_def Abs_fresh_iff
  by auto


section ‹Abstractions of single atoms›


lemma Abs1_eq:
  fixes x y::"'a::fs"
  shows "[{atom a}]set. x = [{atom a}]set. y  x = y"
  and   "[{atom a}]res. x = [{atom a}]res. y  x = y"
  and   "[[atom a]]lst. x = [[atom a]]lst. y  x = y"
unfolding Abs_eq_iff2 alphas
by (auto simp: supp_perm_singleton fresh_star_def fresh_zero_perm)

lemma Abs1_eq_iff_fresh:
  fixes x y::"'a::fs"
  and a b c::"'b::at"
  assumes "atom c  (a, b, x, y)"
  shows "[{atom a}]set. x = [{atom b}]set. y  (a  c)  x = (b  c)  y"
  and   "[{atom a}]res. x = [{atom b}]res. y  (a  c)  x = (b  c)  y"
  and   "[[atom a]]lst. x = [[atom b]]lst. y  (a  c)  x = (b  c)  y"
proof -
  have "[{atom a}]set. x = (a  c)  ([{atom a}]set. x)"
    by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
  then have "[{atom a}]set. x = [{atom c}]set. ((a  c)  x)" by simp
  moreover
  have "[{atom b}]set. y = (b  c)  ([{atom b}]set. y)"
    by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
  then have "[{atom b}]set. y = [{atom c}]set. ((b  c)  y)" by simp
  ultimately
  show "[{atom a}]set. x = [{atom b}]set. y  (a  c)  x = (b  c)  y"
    by (simp add: Abs1_eq)
next
  have "[{atom a}]res. x = (a  c)  ([{atom a}]res. x)"
    by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
  then have "[{atom a}]res. x = [{atom c}]res. ((a  c)  x)" by simp
  moreover
  have "[{atom b}]res. y = (b  c)  ([{atom b}]res. y)"
    by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
  then have "[{atom b}]res. y = [{atom c}]res. ((b  c)  y)" by simp
  ultimately
  show "[{atom a}]res. x = [{atom b}]res. y  (a  c)  x = (b  c)  y"
    by (simp add: Abs1_eq)
next
  have "[[atom a]]lst. x = (a  c)  ([[atom a]]lst. x)"
    by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
  then have "[[atom a]]lst. x = [[atom c]]lst. ((a  c)  x)" by simp
  moreover
  have "[[atom b]]lst. y = (b  c)  ([[atom b]]lst. y)"
    by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
  then have "[[atom b]]lst. y = [[atom c]]lst. ((b  c)  y)" by simp
  ultimately
  show "[[atom a]]lst. x = [[atom b]]lst. y  (a  c)  x = (b  c)  y"
    by (simp add: Abs1_eq)
qed

lemma Abs1_eq_iff_all:
  fixes x y::"'a::fs"
  and z::"'c::fs"
  and a b::"'b::at"
  shows "[{atom a}]set. x = [{atom b}]set. y  (c. atom c  z  atom c  (a, b, x, y)  (a  c)  x = (b  c)  y)"
  and   "[{atom a}]res. x = [{atom b}]res. y  (c. atom c  z  atom c  (a, b, x, y)  (a  c)  x = (b  c)  y)"
  and   "[[atom a]]lst. x = [[atom b]]lst. y  (c. atom c  z  atom c  (a, b, x, y)  (a  c)  x = (b  c)  y)"
apply(auto)
apply(simp add: Abs1_eq_iff_fresh(1)[symmetric])
apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
apply(drule_tac x="aa" in spec)
apply(simp)
apply(subst Abs1_eq_iff_fresh(1))
apply(auto simp: fresh_Pair)[2]
apply(simp add: Abs1_eq_iff_fresh(2)[symmetric])
apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
apply(drule_tac x="aa" in spec)
apply(simp)
apply(subst Abs1_eq_iff_fresh(2))
apply(auto simp: fresh_Pair)[2]
apply(simp add: Abs1_eq_iff_fresh(3)[symmetric])
apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
apply(drule_tac x="aa" in spec)
apply(simp)
apply(subst Abs1_eq_iff_fresh(3))
apply(auto simp: fresh_Pair)[2]
done

lemma Abs1_eq_iff:
  fixes x y::"'a::fs"
  and a b::"'b::at"
  shows "[{atom a}]set. x = [{atom b}]set. y  (a = b  x = y)  (a  b  x = (a  b)  y  atom a  y)"
  and   "[{atom a}]res. x = [{atom b}]res. y  (a = b  x = y)  (a  b  x = (a  b)  y  atom a  y)"
  and   "[[atom a]]lst. x = [[atom b]]lst. y  (a = b  x = y)  (a  b  x = (a  b)  y  atom a  y)"
proof -
  { assume "a = b"
    then have "[{atom a}]set. x = [{atom b}]set. y  (a = b  x = y)" by (simp add: Abs1_eq)
  }
  moreover
  { assume *: "a  b" and **: "[{atom a}]set. x = [{atom b}]set. y"
    have #: "atom a  [{atom b}]set. y" by (simp add: **[symmetric] Abs_fresh_iff)
    have "[{atom a}]set. ((a  b)  y) = (a  b)  ([{atom b}]set. y)" by (simp)
    also have " = [{atom b}]set. y"
      by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
    also have " = [{atom a}]set. x" using ** by simp
    finally have "a  b  x = (a  b)  y  atom a  y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
  }
  moreover
  { assume *: "a  b" and **: "x = (a  b)  y  atom a  y"
    have "[{atom a}]set. x = [{atom a}]set. ((a  b)  y)" using ** by simp
    also have " = (a  b)  ([{atom b}]set. y)" by (simp add: permute_set_def)
    also have " = [{atom b}]set. y"
      by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
    finally have "[{atom a}]set. x = [{atom b}]set. y" .
  }
  ultimately
  show "[{atom a}]set. x = [{atom b}]set. y  (a = b  x = y)  (a  b  x = (a  b)  y  atom a  y)"
    by blast
next
  { assume "a = b"
    then have "Abs_res {atom a} x = Abs_res {atom b} y  (a = b  x = y)" by (simp add: Abs1_eq)
  }
  moreover
  { assume *: "a  b" and **: "Abs_res {atom a} x = Abs_res {atom b} y"
    have #: "atom a  Abs_res {atom b} y" by (simp add: **[symmetric] Abs_fresh_iff)
    have "Abs_res {atom a} ((a  b)  y) = (a  b)  (Abs_res {atom b} y)" by simp
    also have " = Abs_res {atom b} y"
      by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
    also have " = Abs_res {atom a} x" using ** by simp
    finally have "a  b  x = (a  b)  y  atom a  y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
  }
  moreover
  { assume *: "a  b" and **: "x = (a  b)  y  atom a  y"
    have "Abs_res {atom a} x = Abs_res {atom a} ((a  b)  y)" using ** by simp
    also have " = (a  b)  Abs_res {atom b} y" by (simp add: permute_set_def)
    also have " = Abs_res {atom b} y"
      by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
    finally have "Abs_res {atom a} x = Abs_res {atom b} y" .
  }
  ultimately
  show "Abs_res {atom a} x = Abs_res {atom b} y  (a = b  x = y)  (a  b  x = (a  b)  y  atom a  y)"
    by blast
next
  { assume "a = b"
    then have "Abs_lst [atom a] x = Abs_lst [atom b] y  (a = b  x = y)" by (simp add: Abs1_eq)
  }
  moreover
  { assume *: "a  b" and **: "Abs_lst [atom a] x = Abs_lst [atom b] y"
    have #: "atom a  Abs_lst [atom b] y" by (simp add: **[symmetric] Abs_fresh_iff)
    have "Abs_lst [atom a] ((a  b)  y) = (a  b)  (Abs_lst [atom b] y)" by simp
    also have " = Abs_lst [atom b] y"
      by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
    also have " = Abs_lst [atom a] x" using ** by simp
    finally have "a  b  x = (a  b)  y  atom a  y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
  }
  moreover
  { assume *: "a  b" and **: "x = (a  b)  y  atom a  y"
    have "Abs_lst [atom a] x = Abs_lst [atom a] ((a  b)  y)" using ** by simp
    also have " = (a  b)  Abs_lst [atom b] y" by simp
    also have " = Abs_lst [atom b] y"
      by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
    finally have "Abs_lst [atom a] x = Abs_lst [atom b] y" .
  }
  ultimately
  show "Abs_lst [atom a] x = Abs_lst [atom b] y  (a = b  x = y)  (a  b  x = (a  b)  y  atom a  y)"
    by blast
qed

lemma Abs1_eq_iff':
  fixes x::"'a::fs"
  and a b::"'b::at"
  shows "[{atom a}]set. x = [{atom b}]set. y  (a = b  x = y)  (a  b  (b  a)  x = y  atom b  x)"
  and   "[{atom a}]res. x = [{atom b}]res. y  (a = b  x = y)  (a  b  (b  a)  x = y  atom b  x)"
  and   "[[atom a]]lst. x = [[atom b]]lst. y  (a = b  x = y)  (a  b  (b  a)  x = y  atom b  x)"
by (auto simp: Abs1_eq_iff fresh_permute_left)


ML fun alpha_single_simproc thm _ ctxt ctrm =
  let
    val thy = Proof_Context.theory_of ctxt
    val _ $ (_ $ x) $ (_ $ y) = Thm.term_of ctrm
    val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y [])
      |> filter (fn (_, ty) => Sign.of_sort thy (ty, @{sort fs}))
      |> map Free
      |> HOLogic.mk_tuple
      |> Thm.cterm_of ctxt
    val cvrs_ty = Thm.ctyp_of_cterm cvrs
    val thm' = thm
      |> Thm.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs]
  in
    SOME thm'
  end

simproc_setup alpha_set ("[{atom a}]set. x = [{atom b}]set. y") =
  alpha_single_simproc @{thm Abs1_eq_iff_all(1)[THEN eq_reflection]}

simproc_setup alpha_res ("[{atom a}]res. x = [{atom b}]res. y") =
  alpha_single_simproc @{thm Abs1_eq_iff_all(2)[THEN eq_reflection]}

simproc_setup alpha_lst ("[[atom a]]lst. x = [[atom b]]lst. y") =
  alpha_single_simproc @{thm Abs1_eq_iff_all(3)[THEN eq_reflection]}


subsection ‹Renaming of bodies of abstractions›

lemma Abs_rename_set:
  fixes x::"'a::fs"
  assumes a: "(p  bs) ♯* x"
  (*and     b: "finite bs"*)
  shows "q. [bs]set. x = [p  bs]set. (q  x)  q  bs = p  bs"
proof -
  from set_renaming_perm2
  obtain q where *: "b  bs. q  b = p  b" and **: "supp q  bs  (p  bs)" by blast
  have ***: "q  bs = p  bs" using *
    unfolding permute_set_eq_image image_def by auto
  have "[bs]set. x =  q  ([bs]set. x)"
    apply(rule perm_supp_eq[symmetric])
    using a **
    unfolding Abs_fresh_star_iff
    unfolding fresh_star_def
    by auto
  also have " = [q  bs]set. (q  x)" by simp
  finally have "[bs]set. x = [p  bs]set. (q  x)" by (simp add: ***)
  then show "q. [bs]set. x = [p  bs]set. (q  x)  q  bs = p  bs" using *** by metis
qed

lemma Abs_rename_res:
  fixes x::"'a::fs"
  assumes a: "(p  bs) ♯* x"
  (*and     b: "finite bs"*)
  shows "q. [bs]res. x = [p  bs]res. (q  x)  q  bs = p  bs"
proof -
  from set_renaming_perm2
  obtain q where *: "b  bs. q  b = p  b" and **: "supp q  bs  (p  bs)" by blast
  have ***: "q  bs = p  bs" using *
    unfolding permute_set_eq_image image_def by auto
  have "[bs]res. x =  q  ([bs]res. x)"
    apply(rule perm_supp_eq[symmetric])
    using a **
    unfolding Abs_fresh_star_iff
    unfolding fresh_star_def
    by auto
  also have " = [q  bs]res. (q  x)" by simp
  finally have "[bs]res. x = [p  bs]res. (q  x)" by (simp add: ***)
  then show "q. [bs]res. x = [p  bs]res. (q  x)  q  bs = p  bs" using *** by metis
qed

lemma Abs_rename_lst:
  fixes x::"'a::fs"
  assumes a: "(p  (set bs)) ♯* x"
  shows "q. [bs]lst. x = [p  bs]lst. (q  x)  q  bs = p  bs"
proof -
  from list_renaming_perm
  obtain q where *: "b  set bs. q  b = p  b" and **: "supp q  set bs  (p  set bs)" by blast
  have ***: "q  bs = p  bs" using * by (induct bs) (simp_all add: insert_eqvt)
  have "[bs]lst. x =  q  ([bs]lst. x)"
    apply(rule perm_supp_eq[symmetric])
    using a **
    unfolding Abs_fresh_star_iff
    unfolding fresh_star_def
    by auto
  also have " = [q  bs]lst. (q  x)" by simp
  finally have "[bs]lst. x = [p  bs]lst. (q  x)" by (simp add: ***)
  then show "q. [bs]lst. x = [p  bs]lst. (q  x)  q  bs = p  bs" using *** by metis
qed


text ‹for deep recursive binders›

lemma Abs_rename_set':
  fixes x::"'a::fs"
  assumes a: "(p  bs) ♯* x"
  (*and     b: "finite bs"*)
  shows "q. [bs]set. x = [q  bs]set. (q  x)  q  bs = p  bs"
using Abs_rename_set[OF a] by metis

lemma Abs_rename_res':
  fixes x::"'a::fs"
  assumes a: "(p  bs) ♯* x"
  (*and     b: "finite bs"*)
  shows "q. [bs]res. x = [q  bs]res. (q  x)  q  bs = p  bs"
using Abs_rename_res[OF a] by metis

lemma Abs_rename_lst':
  fixes x::"'a::fs"
  assumes a: "(p  (set bs)) ♯* x"
  shows "q. [bs]lst. x = [q  bs]lst. (q  x)  q  bs = p  bs"
using Abs_rename_lst[OF a] by metis

section ‹Infrastructure for building tuples of relations and functions›

fun
  prod_fv :: "('a  atom set)  ('b  atom set)  ('a × 'b)  atom set"
where
  "prod_fv fv1 fv2 (x, y) = fv1 x  fv2 y"

definition
  prod_alpha :: "('a  'a  bool)  ('b  'b  bool)  ('a × 'b  'a × 'b  bool)"
where
 "prod_alpha = rel_prod"

lemma [quot_respect]:
  shows "((R1 ===> (=)) ===> (R2 ===> (=)) ===> rel_prod R1 R2 ===> (=)) prod_fv prod_fv"
  unfolding rel_fun_def
  by auto

lemma [quot_preserve]:
  assumes q1: "Quotient3 R1 abs1 rep1"
  and     q2: "Quotient3 R2 abs2 rep2"
  shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_prod rep1 rep2 ---> id) prod_fv = prod_fv"
  by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])

lemma [mono]:
  shows "A <= B  C <= D ==> prod_alpha A C <= prod_alpha B D"
  unfolding prod_alpha_def
  by auto

lemma [eqvt]:
  shows "p  prod_alpha A B x y = prod_alpha (p  A) (p  B) (p  x) (p  y)"
  unfolding prod_alpha_def
  unfolding rel_prod_conv
  by (perm_simp) (rule refl)

lemma [eqvt]:
  shows "p  prod_fv A B (x, y) = prod_fv (p  A) (p  B) (p  x, p  y)"
  unfolding prod_fv.simps
  by (perm_simp) (rule refl)

lemma prod_fv_supp:
  shows "prod_fv supp supp = supp"
by (rule ext)
   (auto simp: supp_Pair)

lemma prod_alpha_eq:
  shows "prod_alpha ((=)) ((=)) = ((=))"
  unfolding prod_alpha_def
  by (auto intro!: ext)

end