Theory Residual

theory Residual

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

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.›

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

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

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


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

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

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")
  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: "bbn α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"
    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)
      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
  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)
  assume "?r" then show "?l"
    by (meson residual_eq_iff_perm)

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)
      show "finite (supp c)" by (fact finite_supp)
      show "finite (supp act,state)" by (fact finite_supp_abs_residual_pair)
      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)

subsection ‹Other lemmas›

lemma residual_empty_bn_eq_iff:
  assumes "bn α1 = {}"
  shows "α1,P1 = α2,P2  α1 = α2  P1 = P2"
  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
  assume "α1 = α2  P1 = P2" then show "α1,P1 = α2,P2"
    by simp

― ‹The following lemma is not about residuals, but we have no better place for it.›
lemma set_bounded_supp:
  assumes "finite S" and "x. xX  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. xX  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)
  then show "supp X  S"
    using assms(1) by (fact supp_is_subset)