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