Theory FL_Transition_System

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