theory FL_Transition_System imports Transition_System FS_Set begin section ‹Nominal Transition Systems with Effects and \texorpdfstring{$F/L$}{F/L}-Bisimilarity› subsection ‹Nominal transition systems with effects› text ‹The paper defines an effect as a finitely supported function from states to states. It then fixes an equivariant set~@{term ℱ} of effects. In our formalization, we avoid working with such a (carrier) set, and instead introduce a type of (finitely supported) effects together with an (equivariant) application operator for effects and states. Equivariance (of the type of effects) is implicitly guaranteed (by the type of~@{const permute}). \emph{First} represents the (finitely supported) set of effects that must be observed before following a transition.› type_synonym 'eff first = "'eff fs_set" text ‹\emph{Later} is a function that represents how the set~$F$ (for \emph{first}) changes depending on the action of a transition and the chosen effect.› type_synonym ('a,'eff) later = "'a × 'eff first × 'eff ⇒ 'eff first" locale effect_nominal_ts = nominal_ts satisfies transition for satisfies :: "'state::fs ⇒ 'pred::fs ⇒ bool" (infix "⊢" 70) and transition :: "'state ⇒ ('act::bn,'state) residual ⇒ bool" (infix "→" 70) + fixes effect_apply :: "'effect::fs ⇒ 'state ⇒ 'state" ("⟨_⟩_" [0,101] 100) and L :: "('act,'effect) later" assumes effect_apply_eqvt: "eqvt effect_apply" (* using [eqvt] here generates an error message *) and L_eqvt: "eqvt L" ― ‹@{term L} is assumed to be equivariant.› (* using [eqvt] here generates an error message *) begin lemma effect_apply_eqvt_aux [simp]: "p ∙ effect_apply = effect_apply" by (metis effect_apply_eqvt eqvt_def) lemma effect_apply_eqvt' [eqvt]: "p ∙ ⟨f⟩P = ⟨p ∙ f⟩(p ∙ P)" by simp lemma L_eqvt_aux [simp]: "p ∙ L = L" by (metis L_eqvt eqvt_def) lemma L_eqvt' [eqvt]: "p ∙ L (α, P, f) = L (p ∙ α, p ∙ P, p ∙ f)" by simp end subsection ‹\texorpdfstring{$L$}{L}-bisimulations and \texorpdfstring{$F/L$}{F/L}-bisimilarity› context effect_nominal_ts begin definition is_L_bisimulation:: "('effect first ⇒ 'state ⇒ 'state ⇒ bool) ⇒ bool" where "is_L_bisimulation R ≡ ∀F. symp (R F) ∧ (∀P Q. R F P Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))) ∧ (∀P Q. R F P Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶ ⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ R (L (α,F,f)) P' Q'))))" definition FL_bisimilar :: "'effect first ⇒ 'state ⇒ 'state ⇒ bool" where "FL_bisimilar F P Q ≡ ∃R. is_L_bisimulation R ∧ (R F) P Q" abbreviation FL_bisimilar' ("_ ∼⋅[_] _" [51,0,51] 50) where "P ∼⋅[F] Q ≡ FL_bisimilar F P Q" text ‹@{term "FL_bisimilar"} is an equivariant relation, and (for every~@{term F}) an equivalence.› lemma is_L_bisimulation_eqvt [eqvt]: assumes "is_L_bisimulation R" shows "is_L_bisimulation (p ∙ R)" unfolding is_L_bisimulation_def proof (clarify) fix F have "symp ((p ∙ R) F)" (is ?S) using assms unfolding is_L_bisimulation_def by (metis eqvt_lambda symp_eqvt) moreover have "∀P Q. (p ∙ R) F P Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))" (is ?T) proof (clarify) fix P Q f φ assume pR: "(p ∙ R) F P Q" and effect: "f ∈⇩_{f}⇩_{s}F" and satisfies: "⟨f⟩P ⊢ φ" from pR have "R (-p ∙ F) (-p ∙ P) (-p ∙ Q)" by (simp add: eqvt_lambda permute_bool_def unpermute_def) moreover have "(-p ∙ f) ∈⇩_{f}⇩_{s}(-p ∙ F)" using effect by simp moreover have "⟨-p ∙ f⟩(-p ∙ P) ⊢ -p ∙ φ" using satisfies by (metis effect_apply_eqvt' satisfies_eqvt) ultimately have "⟨-p ∙ f⟩(-p ∙ Q) ⊢ -p ∙ φ" using assms unfolding is_L_bisimulation_def by auto then show "⟨f⟩Q ⊢ φ" by (metis (full_types) effect_apply_eqvt' permute_minus_cancel(1) satisfies_eqvt) qed moreover have "∀P Q. (p ∙ R) F P Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶ ⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ (p ∙ R) (L (α, F, f)) P' Q')))" (is ?U) proof (clarify) fix P Q f α P' assume pR: "(p ∙ R) F P Q" and effect: "f ∈⇩_{f}⇩_{s}F" and fresh: "bn α ♯* (⟨f⟩Q, F, f)" and trans: "⟨f⟩P → ⟨α,P'⟩" from pR have "R (-p ∙ F) (-p ∙ P) (-p ∙ Q)" by (simp add: eqvt_lambda permute_bool_def unpermute_def) moreover have "(-p ∙ f) ∈⇩_{f}⇩_{s}(-p ∙ F)" using effect by simp moreover have "bn (-p ∙ α) ♯* (⟨-p ∙ f⟩(-p ∙ Q), -p ∙ F, -p ∙ f)" using fresh by (metis (full_types) effect_apply_eqvt' bn_eqvt fresh_star_Pair fresh_star_permute_iff) moreover have "⟨-p ∙ f⟩(-p ∙ P) → ⟨-p ∙ α, -p ∙ P'⟩" using trans by (metis effect_apply_eqvt' transition_eqvt') ultimately obtain Q' where T: "⟨-p ∙ f⟩(-p ∙ Q) → ⟨-p ∙ α,Q'⟩" and R: "R (L (-p ∙ α, -p ∙ F, -p ∙ f)) (-p ∙ P') Q'" using assms unfolding is_L_bisimulation_def by meson from T have "⟨f⟩Q → ⟨α, p ∙ Q'⟩" by (metis (no_types, lifting) effect_apply_eqvt' abs_residual_pair_eqvt permute_minus_cancel(1) transition_eqvt) moreover from R have "(p ∙ R) (p ∙ L (-p ∙ α, -p ∙ F, -p ∙ f)) (p ∙ -p ∙ P') (p ∙ Q')" by (metis permute_boolI permute_fun_def permute_minus_cancel(2)) then have "(p ∙ R) (L (α,F,f)) P' (p ∙ Q')" by (simp add: permute_self) ultimately show "∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ (p ∙ R) (L (α,F,f)) P' Q'" by metis qed ultimately show "?S ∧ ?T ∧ ?U" by simp qed lemma FL_bisimilar_eqvt: assumes "P ∼⋅[F] Q" shows "(p ∙ P) ∼⋅[p ∙ F] (p ∙ Q)" using assms by (metis eqvt_apply permute_boolI is_L_bisimulation_eqvt FL_bisimilar_def) lemma FL_bisimilar_reflp: "reflp (FL_bisimilar F)" proof (rule reflpI) fix x have "is_L_bisimulation (λ_. (=))" unfolding is_L_bisimulation_def by (simp add: symp_def) then show "x ∼⋅[F] x" unfolding FL_bisimilar_def by auto qed lemma FL_bisimilar_symp: "symp (FL_bisimilar F)" proof (rule sympI) fix P Q assume "P ∼⋅[F] Q" then obtain R where *: "is_L_bisimulation R ∧ R F P Q" unfolding FL_bisimilar_def .. then have "R F Q P" unfolding is_L_bisimulation_def by (simp add: symp_def) with "*" show "Q ∼⋅[F] P" unfolding FL_bisimilar_def by auto qed lemma FL_bisimilar_is_L_bisimulation: "is_L_bisimulation FL_bisimilar" unfolding is_L_bisimulation_def proof fix F have "symp (FL_bisimilar F)" (is ?R) by (fact FL_bisimilar_symp) moreover have "∀P Q. P ∼⋅[F] Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))" (is ?S) by (auto simp add: is_L_bisimulation_def FL_bisimilar_def) moreover have "∀P Q. P ∼⋅[F] Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶ ⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ P' ∼⋅[L (α, F, f)] Q')))" (is ?T) by (auto simp add: is_L_bisimulation_def FL_bisimilar_def) blast ultimately show "?R ∧ ?S ∧ ?T" by metis qed lemma FL_bisimilar_simulation_step: assumes "P ∼⋅[F] Q" and "f ∈⇩_{f}⇩_{s}F" and "bn α ♯* (⟨f⟩Q, F, f)" and "⟨f⟩P → ⟨α,P'⟩" obtains Q' where "⟨f⟩Q → ⟨α,Q'⟩" and "P' ∼⋅[L (α,F,f)] Q'" using assms by (metis (poly_guards_query) FL_bisimilar_is_L_bisimulation is_L_bisimulation_def) lemma FL_bisimilar_transp: "transp (FL_bisimilar F)" proof (rule transpI) fix P Q R assume PQ: "P ∼⋅[F] Q" and QR: "Q ∼⋅[F] R" let ?FL_bisim = "λF. (FL_bisimilar F) OO (FL_bisimilar F)" have "⋀F. symp (?FL_bisim F)" proof (rule sympI) fix F P R assume "?FL_bisim F P R" then obtain Q where "P ∼⋅[F] Q" and "Q ∼⋅[F] R" by blast then have "R ∼⋅[F] Q" and "Q ∼⋅[F] P" by (metis FL_bisimilar_symp sympE)+ then show "?FL_bisim F R P" by blast qed moreover have "⋀F. ∀P Q. ?FL_bisim F P Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))" using FL_bisimilar_is_L_bisimulation is_L_bisimulation_def by auto moreover have "⋀F. ∀P Q. ?FL_bisim F P Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶ ⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ ?FL_bisim (L (α,F,f)) P' Q')))" proof (clarify) fix F P R Q f α P' assume PR: "P ∼⋅[F] R" and RQ: "R ∼⋅[F] Q" and effect: "f ∈⇩_{f}⇩_{s}F" and fresh: "bn α ♯* (⟨f⟩Q, F, f)" and trans: "⟨f⟩P → ⟨α,P'⟩" ― ‹rename~@{term "⟨α,P'⟩"} to avoid~@{term "(⟨f⟩R, F)"}, without touching~@{term "(⟨f⟩Q, F, f)"}› obtain p where 1: "(p ∙ bn α) ♯* (⟨f⟩R, F, f)" and 2: "supp (⟨α,P'⟩, (⟨f⟩Q, F, f)) ♯* p" proof (rule at_set_avoiding2[of "bn α" "(⟨f⟩R, F, f)" "(⟨α,P'⟩, (⟨f⟩Q, F, f))", THEN exE]) show "finite (bn α)" by (fact bn_finite) next show "finite (supp (⟨f⟩R, F, f))" by (fact finite_supp) next show "finite (supp (⟨α,P'⟩, (⟨f⟩Q, F, f)))" by (simp add: finite_supp supp_Pair) next show "bn α ♯* (⟨α,P'⟩, (⟨f⟩Q, F, f))" using bn_abs_residual_fresh fresh fresh_star_Pair by blast qed metis from 2 have 3: "supp ⟨α,P'⟩ ♯* p" and 4: "supp (⟨f⟩Q, F, f) ♯* p" by (simp add: fresh_star_Un supp_Pair)+ from 3 have "⟨p ∙ α, p ∙ P'⟩ = ⟨α,P'⟩" using supp_perm_eq by fastforce then obtain pR' where 5: "⟨f⟩R → ⟨p ∙ α, pR'⟩" and 6: "(p ∙ P') ∼⋅[L (p ∙ α,F,f)] pR'" using PR effect trans 1 by (metis FL_bisimilar_simulation_step bn_eqvt) from fresh and 4 have "bn (p ∙ α) ♯* (⟨f⟩Q, F, f)" by (metis bn_eqvt fresh_star_permute_iff supp_perm_eq) then obtain pQ' where 7: "⟨f⟩Q → ⟨p ∙ α, pQ'⟩" and 8: "pR' ∼⋅[L (p ∙ α,F,f)] pQ'" using RQ effect 5 by (metis FL_bisimilar_simulation_step) from 4 have "supp (⟨f⟩Q) ♯* p" by (simp add: fresh_star_Un supp_Pair) with 7 have "⟨f⟩Q → ⟨α, -p ∙ pQ'⟩" by (metis permute_minus_cancel(2) supp_perm_eq transition_eqvt') moreover from 6 and 8 have "?FL_bisim (L (p ∙ α, F, f)) (p ∙ P') pQ'" by (metis relcompp.relcompI) then have "?FL_bisim (-p ∙ L (p ∙ α, F, f)) (-p ∙ p ∙ P') (-p ∙ pQ')" using FL_bisimilar_eqvt by blast then have "?FL_bisim (L (α, -p ∙ F, -p ∙ f)) P' (-p ∙ pQ')" by (simp add: L_eqvt') then have "?FL_bisim (L (α,F,f)) P' (-p ∙ pQ')" using 4 by (metis fresh_star_Un permute_minus_cancel(2) supp_Pair supp_perm_eq) ultimately show "∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ ?FL_bisim (L (α,F,f)) P' Q'" by metis qed ultimately have "is_L_bisimulation ?FL_bisim" unfolding is_L_bisimulation_def by metis moreover have "?FL_bisim F P R" using PQ QR by blast ultimately show "P ∼⋅[F] R" unfolding FL_bisimilar_def by meson qed lemma FL_bisimilar_equivp: "equivp (FL_bisimilar F)" by (metis FL_bisimilar_reflp FL_bisimilar_symp FL_bisimilar_transp equivp_reflp_symp_transp) end end