# Theory 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

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

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)
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(rotate_tac -1)
apply(drule_tac p="q" in permute_boolI)
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(rotate_tac -1)
apply(drule_tac p="q" in permute_boolI)
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(rotate_tac -1)
apply(drule_tac p="q" in permute_boolI)
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)

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)

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)"
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)"
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)))"
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
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)"
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)"
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)
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

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(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)

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)

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)"

instance abs_set :: (fs) fs
apply standard
apply(case_tac x)
done

instance abs_res :: (fs) fs
apply standard
apply(case_tac x)
done

instance abs_lst :: (fs) fs
apply standard
apply(case_tac x)
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"
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"
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"
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(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(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(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"
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"
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"
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"
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"
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"
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
```