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)"
    by (simp add: residual.abs_eq_iff)
  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"
    by (simp add: residual.abs_eq_iff)
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)"
    by (simp add: residual.abs_eq_iff)
  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