# Theory Residual

theory Residual
imports
Nominal2.Nominal2
begin

section ‹Residuals›

subsection ‹Binding names›

text ‹To define $\alpha$-equivalence, we require actions to be equipped with an equivariant
function~@{term bn} that gives their binding names. Actions may only bind finitely many names. This
is necessary to ensure that we can use a finite permutation to rename the binding names in an
action.›

class bn = fs +
fixes bn :: "'a ⇒ atom set"
assumes bn_eqvt: "p ∙ (bn α) = bn (p ∙ α)"
and bn_finite: "finite (bn α)"

lemma bn_subset_supp: "bn α ⊆ supp α"
by (metis (erased, opaque_lifting) bn_eqvt bn_finite eqvt_at_def finite_supp supp_eqvt_at supp_finite_atom_set)

subsection ‹Raw residuals and \texorpdfstring{$\alpha$}{alpha}-equivalence›

text ‹Raw residuals are simply pairs of actions and states. Binding names in the action bind into
(the action and) the state.›

fun alpha_residual :: "('act::bn × 'state::pt) ⇒ ('act × 'state) ⇒ bool" where
"alpha_residual (α1,P1) (α2,P2) ⟷ [bn α1]set. (α1, P1) = [bn α2]set. (α2, P2)"

text ‹$\alpha$-equivalence is equivariant.›

lemma alpha_residual_eqvt [eqvt]:
assumes "alpha_residual r1 r2"
shows "alpha_residual (p ∙ r1) (p ∙ r2)"
using assms by (cases r1, cases r2) (simp, metis Pair_eqvt bn_eqvt permute_Abs_set)

text ‹$\alpha$-equivalence is an equivalence relation.›

lemma alpha_residual_reflp: "reflp alpha_residual"
by (metis alpha_residual.simps prod.exhaust reflpI)

lemma alpha_residual_symp: "symp alpha_residual"
by (metis alpha_residual.simps prod.exhaust sympI)

lemma alpha_residual_transp: "transp alpha_residual"
by (rule transpI) (metis alpha_residual.simps prod.exhaust)

lemma alpha_residual_equivp: "equivp alpha_residual"
by (metis alpha_residual_reflp alpha_residual_symp alpha_residual_transp equivpI)

subsection ‹Residuals›

text ‹Residuals are raw residuals quotiented by $\alpha$-equivalence.›

quotient_type
('act,'state) residual = "'act::bn × 'state::pt" / "alpha_residual"
by (fact alpha_residual_equivp)

lemma residual_abs_rep [simp]: "abs_residual (rep_residual res) = res"
by (metis Quotient_residual Quotient_abs_rep)

lemma residual_rep_abs [simp]: "alpha_residual (rep_residual (abs_residual r)) r"
by (metis residual.abs_eq_iff residual_abs_rep)

text ‹The permutation operation is lifted from raw residuals.›

instantiation residual :: (bn,pt) pt
begin

lift_definition permute_residual :: "perm ⇒ ('a,'b) residual ⇒ ('a,'b) residual"
is permute
by (fact alpha_residual_eqvt)

instance
proof
fix res :: "(_,_) residual"
show "0 ∙ res = res"
by transfer (metis alpha_residual_equivp equivp_reflp permute_zero)
next
fix p q :: perm and res :: "(_,_) residual"
show "(p + q) ∙ res = p ∙ q ∙ res"
by transfer (metis alpha_residual_equivp equivp_reflp permute_plus)
qed

end

text ‹The abstraction function from raw residuals to residuals is equivariant. The representation
function is equivariant modulo $\alpha$-equivalence.›

lemmas permute_residual.abs_eq [eqvt, simp]

lemma alpha_residual_permute_rep_commute [simp]: "alpha_residual (p ∙ rep_residual res) (rep_residual (p ∙ res))"
by (metis residual.abs_eq_iff residual_abs_rep permute_residual.abs_eq)

subsection ‹Notation for pairs as residuals›

abbreviation abs_residual_pair :: "'act::bn ⇒ 'state::pt ⇒ ('act,'state) residual" ("⟨_,_⟩" [0,0] 1000)
where
"⟨α,P⟩ == abs_residual (α,P)"

lemma abs_residual_pair_eqvt [simp]: "p ∙ ⟨α,P⟩ = ⟨p ∙ α, p ∙ P⟩"
by (metis Pair_eqvt permute_residual.abs_eq)

subsection ‹Support of residuals›

text ‹We only consider finitely supported states now.›

lemma supp_abs_residual_pair: "supp ⟨α, P::'state::fs⟩ = supp (α,P) - bn α"
proof -
have "supp ⟨α,P⟩ = supp ([bn α]set. (α, P))"
by (simp add: supp_def residual.abs_eq_iff bn_eqvt)
then show ?thesis by (simp add: supp_Abs)
qed

lemma bn_abs_residual_fresh [simp]: "bn α ♯* ⟨α,P::'state::fs⟩"
by (simp add: fresh_star_def fresh_def supp_abs_residual_pair)

lemma finite_supp_abs_residual_pair [simp]: "finite (supp ⟨α, P::'state::fs⟩)"
by (metis finite_Diff finite_supp supp_abs_residual_pair)

subsection ‹Equality between residuals›

lemma residual_eq_iff_perm: "⟨α1,P1⟩ = ⟨α2,P2⟩ ⟷
(∃p. supp (α1, P1) - bn α1 = supp (α2, P2) - bn α2 ∧ (supp (α1, P1) - bn α1) ♯* p ∧ p ∙ (α1, P1) = (α2, P2) ∧ p ∙ bn α1 = bn α2)"
(is "?l ⟷ ?r")
proof
assume *: "?l"
then have "[bn α1]set. (α1, P1) = [bn α2]set. (α2, P2)"
then obtain p where "(bn α1, (α1,P1)) ≈set ((=)) supp p (bn α2, (α2,P2))"
using Abs_eq_iff(1) by blast
then show "?r"
by (metis (mono_tags, lifting) alpha_set.simps)
next
assume *: "?r"
then obtain p where "(bn α1, (α1,P1)) ≈set ((=)) supp p (bn α2, (α2,P2))"
using alpha_set.simps by blast
then have "[bn α1]set. (α1, P1) = [bn α2]set. (α2, P2)"
using Abs_eq_iff(1) by blast
then show "?l"
qed

lemma residual_eq_iff_perm_renaming: "⟨α1,P1⟩ = ⟨α2,P2⟩ ⟷
(∃p. supp (α1, P1) - bn α1 = supp (α2, P2) - bn α2 ∧ (supp (α1, P1) - bn α1) ♯* p ∧ p ∙ (α1, P1) = (α2, P2) ∧ p ∙ bn α1 = bn α2 ∧ supp p ⊆ bn α1 ∪ p ∙ bn α1)"
(is "?l ⟷ ?r")
proof
assume "?l"
then obtain p where p: "supp (α1, P1) - bn α1 = supp (α2, P2) - bn α2 ∧ (supp (α1, P1) - bn α1) ♯* p ∧ p ∙ (α1, P1) = (α2, P2) ∧ p ∙ bn α1 = bn α2"
by (metis residual_eq_iff_perm)
moreover obtain q where q_p: "∀b∈bn α1. q ∙ b = p ∙ b" and supp_q: "supp q ⊆ bn α1 ∪ p ∙ bn α1"
by (metis set_renaming_perm2)
have "supp q ⊆ supp p"
proof
fix a assume *: "a ∈ supp q" then show "a ∈ supp p"
proof (cases "a ∈ bn α1")
case True then show ?thesis
using "*" q_p by (metis mem_Collect_eq supp_perm)
next
case False then have "a ∈ p ∙ bn α1"
using "*" supp_q using UnE subsetCE by blast
with False have "p ∙ a ≠ a"
by (metis mem_permute_iff)
then show ?thesis
using fresh_def fresh_perm by blast
qed
qed
with p have "(supp (α1, P1) - bn α1) ♯* q"
by (meson fresh_def fresh_star_def subset_iff)
moreover with p and q_p have "⋀a. a ∈ supp α1 ⟹ q ∙ a = p ∙ a" and "⋀a. a ∈ supp P1 ⟹ q ∙ a = p ∙ a"
by (metis Diff_iff fresh_perm fresh_star_def UnCI supp_Pair)+
then have "q ∙ α1 = p ∙ α1" and "q ∙ P1 = p ∙ P1"
by (metis supp_perm_perm_eq)+
ultimately show "?r"
using supp_q by (metis Pair_eqvt bn_eqvt)
next
assume "?r" then show "?l"
by (meson residual_eq_iff_perm)
qed

subsection ‹Strong induction›

lemma residual_strong_induct:
assumes "⋀(act::'act::bn) (state::'state::fs) (c::'a::fs). bn act ♯* c ⟹ P c ⟨act,state⟩"
shows "P c residual"
proof (rule residual.abs_induct, clarify)
fix act :: 'act and state :: 'state
obtain p where 1: "(p ∙ bn act) ♯* c" and 2: "supp ⟨act,state⟩ ♯* p"
proof (rule at_set_avoiding2[of "bn act" c "⟨act,state⟩", THEN exE])
show "finite (bn act)" by (fact bn_finite)
next
show "finite (supp c)" by (fact finite_supp)
next
show "finite (supp ⟨act,state⟩)" by (fact finite_supp_abs_residual_pair)
next
show "bn act ♯* ⟨act,state⟩" by (fact bn_abs_residual_fresh)
qed metis
from 2 have "⟨p ∙ act, p ∙ state⟩ = ⟨act,state⟩"
using supp_perm_eq by fastforce
then show "P c ⟨act,state⟩"
using assms 1 by (metis bn_eqvt)
qed

subsection ‹Other lemmas›

lemma residual_empty_bn_eq_iff:
assumes "bn α1 = {}"
shows "⟨α1,P1⟩ = ⟨α2,P2⟩ ⟷ α1 = α2 ∧ P1 = P2"
proof
assume "⟨α1,P1⟩ = ⟨α2,P2⟩"
with assms have "[{}]set. (α1, P1) = [bn α2]set. (α2, P2)"
then obtain p where "({}, (α1, P1)) ≈set ((=)) supp p (bn α2, (α2, P2))"
using Abs_eq_iff(1) by blast
then show "α1 = α2 ∧ P1 = P2"
unfolding alpha_set using supp_perm_eq by fastforce
next
assume "α1 = α2 ∧ P1 = P2" then show "⟨α1,P1⟩ = ⟨α2,P2⟩"
by simp
qed

― ‹The following lemma is not about residuals, but we have no better place for it.›
lemma set_bounded_supp:
assumes "finite S" and "⋀x. x∈X ⟹ supp x ⊆ S"
shows "supp X ⊆ S"
proof -
have "S supports X"
unfolding supports_def proof (clarify)
fix a b
assume a: "a ∉ S" and b: "b ∉ S"
{
fix x
assume "x ∈ X"
then have "(a ⇌ b) ∙ x = x"
using a b ‹⋀x. x∈X ⟹ supp x ⊆ S› by (meson fresh_def subsetCE swap_fresh_fresh)
}
then show "(a ⇌ b) ∙ X = X"
by auto (metis (full_types) eqvt_bound mem_permute_iff, metis mem_permute_iff)
qed
then show "supp X ⊆ S"
using assms(1) by (fact supp_is_subset)
qed

end