Theory Transition_System

theory Transition_System
imports
  Residual
begin

section ‹Nominal Transition Systems and Bisimulations›

subsection ‹Basic Lemmas›

lemma symp_on_eqvt [eqvt]:
  assumes "symp_on A R" shows "symp_on (p ∙ A) (p ∙ R)"
  using assms
  by (auto simp: symp_on_def permute_fun_def permute_set_def permute_pure)

lemma symp_eqvt:
  assumes "symp R" shows "symp (p ∙ R)"
  using assms
  by (auto simp: symp_on_def permute_fun_def permute_pure)


subsection ‹Nominal transition systems›

locale nominal_ts =
  fixes satisfies :: "'state::fs ⇒ 'pred::fs ⇒ bool"                (infix ‹⊢› 70)
    and transition :: "'state ⇒ ('act::bn,'state) residual ⇒ bool"  (infix ‹→› 70)
  assumes satisfies_eqvt [eqvt]: "P ⊢ φ ⟹ p ∙ P ⊢ p ∙ φ"
      and transition_eqvt [eqvt]: "P → αQ ⟹ p ∙ P → p ∙ αQ"
begin

  lemma transition_eqvt':
    assumes "P → ⟨α,Q⟩" shows "p ∙ P → ⟨p ∙ α, p ∙ Q⟩"
  using assms by (metis abs_residual_pair_eqvt transition_eqvt)

end


subsection ‹Bisimulations›

context nominal_ts
begin

  definition is_bisimulation :: "('state ⇒ 'state ⇒ bool) ⇒ bool" where
    "is_bisimulation R ≡
      symp R ∧
      (∀P Q. R P Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)) ∧
      (∀P Q. R P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ R P' Q')))"

  definition bisimilar :: "'state ⇒ 'state ⇒ bool"  (infix ‹∼⋅› 100) where
    "P ∼⋅ Q ≡ ∃R. is_bisimulation R ∧ R P Q"

  text ‹@{const bisimilar} is an equivariant equivalence relation.›

  lemma is_bisimulation_eqvt (*[eqvt]*):
    assumes "is_bisimulation R" shows "is_bisimulation (p ∙ R)"
  using assms unfolding is_bisimulation_def
  proof (clarify)
    assume 1: "symp R"
    assume 2: "∀P Q. R P Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)"
    assume 3: "∀P Q. R P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ R P' Q'))"
    have "symp (p ∙ R)" (is ?S)
      using 1 by (simp add: symp_eqvt)
    moreover have "∀P Q. (p ∙ R) P Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)" (is ?T)
      proof (clarify)
        fix P Q φ
        assume *: "(p ∙ R) P Q" and **: "P ⊢ φ"
        from * have "R (-p ∙ P) (-p ∙ Q)"
          by (simp add: eqvt_lambda permute_bool_def unpermute_def)
        then show "Q ⊢ φ"
          using 2 ** by (metis permute_minus_cancel(1) satisfies_eqvt)
      qed
    moreover have "∀P Q. (p ∙ R) P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ (p ∙ R) P' Q'))" (is ?U)
      proof (clarify)
        fix P Q α P'
        assume *: "(p ∙ R) P Q" and **: "bn α ♯* Q" and ***: "P → ⟨α,P'⟩"
        from * have "R (-p ∙ P) (-p ∙ Q)"
          by (simp add: eqvt_lambda permute_bool_def unpermute_def)
        moreover have "bn (-p ∙ α) ♯* (-p ∙ Q)"
          using ** by (metis bn_eqvt fresh_star_permute_iff)
        moreover have "-p ∙ P → ⟨-p ∙ α, -p ∙ P'⟩"
          using *** by (metis transition_eqvt')
        ultimately obtain Q' where T: "-p ∙ Q → ⟨-p ∙ α,Q'⟩" and R: "R (-p ∙ P') Q'"
          using 3 by metis
        from T have "Q → ⟨α, p ∙ Q'⟩"
          by (metis permute_minus_cancel(1) transition_eqvt')
        moreover from R have "(p ∙ R) P' (p ∙ Q')"
          by (metis eqvt_apply eqvt_lambda permute_bool_def unpermute_def)
        ultimately show "∃Q'. Q → ⟨α,Q'⟩ ∧ (p ∙ R) P' Q'"
          by metis
      qed
    ultimately show "?S ∧ ?T ∧ ?U" by simp
  qed

  lemma bisimilar_eqvt (*[eqvt]*):
    assumes "P ∼⋅ Q" shows "(p ∙ P) ∼⋅ (p ∙ Q)"
  proof -
    from assms obtain R where *: "is_bisimulation R ∧ R P Q"
      unfolding bisimilar_def ..
    then have "is_bisimulation (p ∙ R)"
      by (simp add: is_bisimulation_eqvt)
    moreover from "*" have "(p ∙ R) (p ∙ P) (p ∙ Q)"
      by (metis eqvt_apply permute_boolI)
    ultimately show "(p ∙ P) ∼⋅ (p ∙ Q)"
      unfolding bisimilar_def by auto
  qed

  lemma bisimilar_reflp: "reflp bisimilar"
  proof (rule reflpI)
    fix x
    have "is_bisimulation (=)"
      unfolding is_bisimulation_def by (simp add: symp_def)
    then show "x ∼⋅ x"
      unfolding bisimilar_def by auto
  qed

  lemma bisimilar_symp: "symp bisimilar"
  proof (rule sympI)
    fix P Q
    assume "P ∼⋅ Q"
    then obtain R where *: "is_bisimulation R ∧ R P Q"
      unfolding bisimilar_def ..
    then have "R Q P"
      unfolding is_bisimulation_def by (simp add: symp_def)
    with "*" show "Q ∼⋅ P"
      unfolding bisimilar_def by auto
  qed

  lemma bisimilar_is_bisimulation: "is_bisimulation bisimilar"
  unfolding is_bisimulation_def proof
    show "symp (∼⋅)"
      by (fact bisimilar_symp)
  next
    show "(∀P Q. P ∼⋅ Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)) ∧
      (∀P Q. P ∼⋅ Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ P' ∼⋅ Q')))"
      by (auto simp add: is_bisimulation_def bisimilar_def) blast
  qed

  lemma bisimilar_transp: "transp bisimilar"
  proof (rule transpI)
    fix P Q R
    assume PQ: "P ∼⋅ Q" and QR: "Q ∼⋅ R"
    let ?bisim = "bisimilar OO bisimilar"
    have "symp ?bisim"
      proof (rule sympI)
        fix P R
        assume "?bisim P R"
        then obtain Q where "P ∼⋅ Q" and "Q ∼⋅ R"
          by blast
        then have "R ∼⋅ Q" and "Q ∼⋅ P"
          by (metis bisimilar_symp sympE)+
        then show "?bisim R P"
          by blast
      qed
    moreover have "∀P Q. ?bisim P Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)"
      using bisimilar_is_bisimulation is_bisimulation_def by auto
    moreover have "∀P Q. ?bisim P Q ⟶
           (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ ?bisim P' Q'))"
      proof (clarify)
        fix P R Q α P'
        assume PR: "P ∼⋅ R" and RQ: "R ∼⋅ Q" and fresh: "bn α ♯* Q" and trans: "P → ⟨α,P'⟩"
        ― ‹rename~@{term "⟨α,P'⟩"} to avoid~@{term R}, without touching~@{term Q}›
        obtain p where 1: "(p ∙ bn α) ♯* R" and 2: "supp (⟨α,P'⟩, Q) ♯* p"
          proof (rule at_set_avoiding2[of "bn α" R "(⟨α,P'⟩, Q)", THEN exE])
            show "finite (bn α)" by (fact bn_finite)
          next
            show "finite (supp R)" by (fact finite_supp)
          next
            show "finite (supp (⟨α,P'⟩, Q))" by (simp add: finite_supp supp_Pair)
          next
            show "bn α ♯* (⟨α,P'⟩, Q)" by (simp add: fresh fresh_star_Pair)
          qed metis
        from 2 have 3: "supp ⟨α,P'⟩ ♯* p" and 4: "supp Q ♯* 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: "R → ⟨p ∙ α, pR'⟩" and 6: "(p ∙ P') ∼⋅ pR'"
          using PR trans 1 by (metis (mono_tags, lifting) bisimilar_is_bisimulation bn_eqvt is_bisimulation_def)
        from fresh and 4 have "bn (p ∙ α) ♯* Q"
          by (metis bn_eqvt fresh_star_permute_iff supp_perm_eq)
        then obtain pQ' where 7: "Q → ⟨p ∙ α, pQ'⟩" and 8: "pR' ∼⋅ pQ'"
          using RQ 5 by (metis (full_types) bisimilar_is_bisimulation is_bisimulation_def)
        from 7 have "Q → ⟨α, -p ∙ pQ'⟩"
          using 4 by (metis permute_minus_cancel(2) supp_perm_eq transition_eqvt')
        moreover from 6 and 8 have "?bisim P' (-p ∙ pQ')"
          by (metis (no_types, opaque_lifting) bisimilar_eqvt permute_minus_cancel(2) relcompp.simps)
        ultimately show "∃Q'. Q → ⟨α,Q'⟩ ∧ ?bisim P' Q'"
          by metis
      qed
    ultimately have "is_bisimulation ?bisim"
      unfolding is_bisimulation_def by metis
    moreover have "?bisim P R"
      using PQ QR by blast
    ultimately show "P ∼⋅ R"
      unfolding bisimilar_def by meson
  qed

  lemma bisimilar_equivp: "equivp bisimilar"
  by (metis bisimilar_reflp bisimilar_symp bisimilar_transp equivp_reflp_symp_transp)

  lemma bisimilar_simulation_step:
    assumes "P ∼⋅ Q" and "bn α ♯* Q" and "P → ⟨α,P'⟩"
    obtains Q' where "Q → ⟨α,Q'⟩" and "P' ∼⋅ Q'"
  using assms by (metis (poly_guards_query) bisimilar_is_bisimulation is_bisimulation_def)

end

end