Theory Weak_Transition_System

theory Weak_Transition_System
imports
  Transition_System
begin

section ‹Nominal Transition Systems and Bisimulations with Unobservable Transitions›

subsection ‹Nominal transition systems with unobservable transitions›

locale weak_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 τ :: 'act
  assumes tau_eqvt [eqvt]: "p ∙ τ = τ"
begin

  lemma bn_tau_empty [simp]: "bn τ = {}"
  using bn_eqvt bn_finite tau_eqvt by (metis eqvt_def supp_finite_atom_set supp_fun_eqvt)

  lemma bn_tau_fresh [simp]: "bn τ ♯* P"
  by (simp add: fresh_star_def)

  inductive tau_transition :: "'state ⇒ 'state ⇒ bool" (infix ‹⇒› 70) where
    tau_refl [simp]: "P ⇒ P"
  | tau_step: "⟦ P → ⟨τ, P'⟩; P' ⇒ P'' ⟧ ⟹ P ⇒ P''"

  definition observable_transition :: "'state ⇒ 'act ⇒ 'state ⇒ bool" (‹_/ ⇒{_}/ _› [70, 70, 71] 71) where
    "P ⇒{α} P' ≡ ∃Q Q'. P ⇒ Q ∧ Q → ⟨α, Q'⟩ ∧ Q' ⇒ P'"

  definition weak_transition :: "'state ⇒ 'act ⇒ 'state ⇒ bool" (‹_/ ⇒⟨_⟩/ _› [70, 70, 71] 71) where
    "P ⇒⟨α⟩ P' ≡ if α = τ then P ⇒ P' else P ⇒{α} P'"

  text ‹The transition relations defined above are equivariant.›

  lemma tau_transition_eqvt (*[eqvt]*):
    assumes "P ⇒ P'" shows "p ∙ P ⇒ p ∙ P'"
  using assms proof (induction)
    case (tau_refl P) show ?case
      by (fact tau_transition.tau_refl)
  next
    case (tau_step P P' P'')
      from ‹P → ⟨τ,P'⟩› have "p ∙ P → ⟨τ,p ∙ P'⟩"
        using tau_eqvt transition_eqvt' by fastforce
      with ‹p ∙ P' ⇒ p ∙ P''› show ?case
        using tau_transition.tau_step by blast
  qed

  lemma observable_transition_eqvt (*[eqvt]*):
    assumes "P ⇒{α} P'" shows "p ∙ P ⇒{p ∙ α} p ∙ P'"
  using assms unfolding observable_transition_def by (metis transition_eqvt' tau_transition_eqvt)

  lemma weak_transition_eqvt (*[eqvt]*):
    assumes "P ⇒⟨α⟩ P'" shows "p ∙ P ⇒⟨p ∙ α⟩ p ∙ P'"
  using assms unfolding weak_transition_def by (metis (full_types) observable_transition_eqvt permute_minus_cancel(2) tau_eqvt tau_transition_eqvt)

  text ‹Additional lemmas about @{const tau_transition}, @{const observable_transition} and
  @{const weak_transition}.›

  lemma tau_transition_trans:
    assumes "P ⇒ Q" and "Q ⇒ R"
    shows "P ⇒ R"
  using assms by (induction, auto simp add: tau_step)

  lemma observable_transitionI:
    assumes "P ⇒ Q" and "Q → ⟨α, Q'⟩" and "Q' ⇒ P'"
    shows "P ⇒{α} P'"
  using assms observable_transition_def by blast

  lemma observable_transition_stepI [simp]:
    assumes "P → ⟨α, P'⟩"
    shows "P ⇒{α} P'"
  using assms observable_transitionI tau_refl by blast

  lemma observable_tau_transition:
    assumes "P ⇒{τ} P'"
    shows "P ⇒ P'"
  proof -
    from ‹P ⇒{τ} P'› obtain Q Q' where "P ⇒ Q" and "Q → ⟨τ, Q'⟩" and "Q' ⇒ P'"
      unfolding observable_transition_def by blast
    then show ?thesis
      by (metis tau_step tau_transition_trans)
  qed

  lemma weak_transition_tau_iff [simp]:
    "P ⇒⟨τ⟩ P' ⟷ P ⇒ P'"
  by (simp add: weak_transition_def)

  lemma weak_transition_not_tau_iff [simp]:
    assumes "α ≠ τ"
    shows "P ⇒⟨α⟩ P' ⟷ P ⇒{α} P'"
  using assms by (simp add: weak_transition_def)

  lemma weak_transition_stepI [simp]:
    assumes "P ⇒{α} P'"
    shows "P ⇒⟨α⟩ P'"
  using assms by (cases "α = τ", simp_all add: observable_tau_transition)

  lemma weak_transition_weakI:
    assumes "P ⇒ Q" and "Q ⇒⟨α⟩ Q'" and "Q' ⇒ P'"
    shows "P ⇒⟨α⟩ P'"
  proof (cases "α = τ")
    case True with assms show ?thesis
      by (metis tau_transition_trans weak_transition_tau_iff)
  next
    case False with assms show ?thesis
      using observable_transition_def tau_transition_trans weak_transition_not_tau_iff by blast
  qed

end


subsection ‹Weak bisimulations›

context weak_nominal_ts
begin

  definition is_weak_bisimulation :: "('state ⇒ 'state ⇒ bool) ⇒ bool" where
    "is_weak_bisimulation R ≡
      symp R ∧
      ― ‹weak static implication›
      (∀P Q φ. R P Q ∧ P ⊢ φ ⟶ (∃Q'. Q ⇒ Q' ∧ R P Q' ∧ Q' ⊢ φ)) ∧
      ― ‹weak simulation›
      (∀P Q. R P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q ⇒⟨α⟩ Q' ∧ R P' Q')))"

  definition weakly_bisimilar :: "'state ⇒ 'state ⇒ bool"  (infix ‹≈⋅› 100) where
    "P ≈⋅ Q ≡ ∃R. is_weak_bisimulation R ∧ R P Q"

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

  lemma is_weak_bisimulation_eqvt (*[eqvt]*):
    assumes "is_weak_bisimulation R" shows "is_weak_bisimulation (p ∙ R)"
  using assms unfolding is_weak_bisimulation_def
  proof (clarify)
    assume 1: "symp R"
    assume 2: "∀P Q φ. R P Q ∧ P ⊢ φ ⟶ (∃Q'. Q ⇒ Q' ∧ R P Q' ∧ 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'. Q ⇒ Q' ∧ (p ∙ R) P Q' ∧ Q' ⊢ φ)" (is ?T)
      proof (clarify)
        fix P Q φ
        assume pR: "(p ∙ R) P Q" and phi: "P ⊢ φ"
        from pR have "R (-p ∙ P) (-p ∙ Q)"
          by (simp add: eqvt_lambda permute_bool_def unpermute_def)
        moreover from phi have "(-p ∙ P) ⊢ (-p ∙ φ)"
          by (metis satisfies_eqvt)
        ultimately obtain Q' where *: "-p ∙ Q ⇒ Q'" and **: "R (-p ∙ P) Q'" and ***: "Q' ⊢ (-p ∙ φ)"
          using 2 by blast
        from * have "Q ⇒ p ∙ Q'"
          by (metis permute_minus_cancel(1) tau_transition_eqvt)
        moreover from ** have "(p ∙ R) P (p ∙ Q')"
          by (simp add: eqvt_lambda permute_bool_def unpermute_def)
        moreover from *** have "p ∙ Q' ⊢ φ"
          by (metis permute_minus_cancel(1) satisfies_eqvt)
        ultimately show "∃Q'. Q ⇒ Q' ∧ (p ∙ R) P Q' ∧ Q' ⊢ φ"
          by metis
      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) weak_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 weakly_bisimilar_eqvt (*[eqvt]*):
    assumes "P ≈⋅ Q" shows "(p ∙ P) ≈⋅ (p ∙ Q)"
  proof -
    from assms obtain R where *: "is_weak_bisimulation R ∧ R P Q"
      unfolding weakly_bisimilar_def ..
    then have "is_weak_bisimulation (p ∙ R)"
      by (simp add: is_weak_bisimulation_eqvt)
    moreover from "*" have "(p ∙ R) (p ∙ P) (p ∙ Q)"
      by (metis eqvt_apply permute_boolI)
    ultimately show "(p ∙ P) ≈⋅ (p ∙ Q)"
      unfolding weakly_bisimilar_def by auto
  qed

  lemma weakly_bisimilar_reflp: "reflp weakly_bisimilar"
  proof (rule reflpI)
    fix x
    have "is_weak_bisimulation (=)"
      unfolding is_weak_bisimulation_def by (simp add: symp_def)
    then show "x ≈⋅ x"
      unfolding weakly_bisimilar_def by auto
  qed

  lemma weakly_bisimilar_symp: "symp weakly_bisimilar"
  proof (rule sympI)
    fix P Q
    assume "P ≈⋅ Q"
    then obtain R where *: "is_weak_bisimulation R ∧ R P Q"
      unfolding weakly_bisimilar_def ..
    then have "R Q P"
      unfolding is_weak_bisimulation_def by (simp add: symp_def)
    with "*" show "Q ≈⋅ P"
      unfolding weakly_bisimilar_def by auto
  qed

  lemma weakly_bisimilar_is_weak_bisimulation: "is_weak_bisimulation weakly_bisimilar"
  unfolding is_weak_bisimulation_def proof
    show "symp (≈⋅)"
      by (fact weakly_bisimilar_symp)
  next
    show "(∀P Q φ. P ≈⋅ Q ∧ P ⊢ φ ⟶ (∃Q'. Q ⇒ Q' ∧ P ≈⋅ Q' ∧ Q' ⊢ φ)) ∧
      (∀P Q. P ≈⋅ Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q ⇒⟨α⟩ Q' ∧ P' ≈⋅ Q')))"
      by (auto simp add: is_weak_bisimulation_def weakly_bisimilar_def) blast+
  qed

  lemma weakly_bisimilar_tau_simulation_step:
    assumes "P ≈⋅ Q" and "P ⇒ P'"
    obtains Q' where "Q ⇒ Q'" and "P' ≈⋅ Q'"
  using ‹P ⇒ P'› ‹P ≈⋅ Q› proof (induct arbitrary: Q)
    case (tau_refl P) then show ?case
      by (metis tau_transition.tau_refl)
  next
    case (tau_step P P'' P')
    from ‹P → ⟨τ,P''⟩› and ‹P ≈⋅ Q› obtain Q'' where "Q ⇒ Q''" and "P'' ≈⋅ Q''"
      by (metis bn_tau_fresh is_weak_bisimulation_def weak_transition_def weakly_bisimilar_is_weak_bisimulation)
    then show ?case
      using tau_step.hyps(3) tau_step.prems(1) by (metis tau_transition_trans)
  qed

  lemma weakly_bisimilar_weak_simulation_step:
    assumes "P ≈⋅ Q" and "bn α ♯* Q" and "P ⇒⟨α⟩ P'"
    obtains Q' where "Q ⇒⟨α⟩ Q'" and "P' ≈⋅ Q'"
  proof (cases "α = τ")
    case True with ‹P ≈⋅ Q› and ‹P ⇒⟨α⟩ P'› and that show ?thesis
      using weak_transition_tau_iff weakly_bisimilar_tau_simulation_step by force
  next
    case False with ‹P ⇒⟨α⟩ P'› have "P ⇒{α} P'"
      by simp
    then obtain P1 P2 where tauP: "P ⇒ P1" and trans: "P1 → ⟨α,P2⟩" and tauP2: "P2 ⇒ P'"
      using observable_transition_def by blast
    from ‹P ≈⋅ Q› and tauP obtain Q1 where tauQ: "Q ⇒ Q1" and P1Q1: "P1 ≈⋅ Q1"
      by (metis weakly_bisimilar_tau_simulation_step)

    ― ‹rename~@{term "⟨α,P2⟩"} to avoid~@{term Q1}, without touching~@{term Q}›
    obtain p where 1: "(p ∙ bn α) ♯* Q1" and 2: "supp (⟨α,P2⟩, Q) ♯* p"
      proof (rule at_set_avoiding2[of "bn α" Q1 "(⟨α,P2⟩, Q)", THEN exE])
        show "finite (bn α)" by (fact bn_finite)
      next
        show "finite (supp Q1)" by (fact finite_supp)
      next
        show "finite (supp (⟨α,P2⟩, Q))" by (simp add: finite_supp supp_Pair)
      next
        show "bn α ♯* (⟨α,P2⟩, Q)" using ‹bn α ♯* Q› by (simp add: fresh_star_Pair)
      qed metis
    from 2 have 3: "supp ⟨α,P2⟩ ♯* p" and 4: "supp Q ♯* p"
      by (simp add: fresh_star_Un supp_Pair)+
    from 3 have "⟨p ∙ α, p ∙ P2⟩ = ⟨α,P2⟩"
      using supp_perm_eq by fastforce
    then obtain Q2 where trans': "Q1 ⇒⟨p ∙ α⟩ Q2" and P2Q2: "(p ∙ P2) ≈⋅ Q2"
      using P1Q1 trans 1 by (metis (mono_tags, lifting) weakly_bisimilar_is_weak_bisimulation bn_eqvt is_weak_bisimulation_def)

    from tauP2 have "p ∙ P2 ⇒ p ∙ P'"
      by (fact tau_transition_eqvt)
    with P2Q2 obtain Q' where tauQ2: "Q2 ⇒ Q'" and P'Q': "(p ∙ P') ≈⋅ Q'"
      by (metis weakly_bisimilar_tau_simulation_step)

    from tauQ and trans' and tauQ2 have "Q ⇒⟨p ∙ α⟩ Q'"
      by (rule weak_transition_weakI)
    with 4 have "Q ⇒⟨α⟩ (-p ∙ Q')"
      by (metis permute_minus_cancel(2) supp_perm_eq weak_transition_eqvt)
    moreover from P'Q' have "P' ≈⋅ (-p ∙ Q')"
      by (metis permute_minus_cancel(2) weakly_bisimilar_eqvt)
    ultimately show ?thesis ..
  qed

  lemma weakly_bisimilar_transp: "transp weakly_bisimilar"
  proof (rule transpI)
    fix P Q R
    assume PQ: "P ≈⋅ Q" and QR: "Q ≈⋅ R"
    let ?bisim = "weakly_bisimilar OO weakly_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 weakly_bisimilar_symp sympE)+
        then show "?bisim R P"
          by blast
      qed
    moreover have "∀P Q φ. ?bisim P Q ∧ P ⊢ φ ⟶ (∃Q'. Q ⇒ Q' ∧ ?bisim P Q' ∧ Q' ⊢ φ)"
      proof (clarify)
        fix P Q φ R
        assume phi: "P ⊢ φ" and PR: "P ≈⋅ R" and RQ: "R ≈⋅ Q"
        from PR and phi obtain R' where "R ⇒ R'" and "P ≈⋅ R'" and *: "R' ⊢ φ"
          using weakly_bisimilar_is_weak_bisimulation is_weak_bisimulation_def by force
        from RQ and ‹R ⇒ R'› obtain Q' where "Q ⇒ Q'" and "R' ≈⋅ Q'"
          by (metis weakly_bisimilar_tau_simulation_step)
        from ‹R' ≈⋅ Q'› and * obtain Q'' where "Q' ⇒ Q''" and "R' ≈⋅ Q''" and **: "Q'' ⊢ φ"
          using weakly_bisimilar_is_weak_bisimulation is_weak_bisimulation_def by force
        from ‹Q ⇒ Q'› and ‹Q' ⇒ Q''› have "Q ⇒ Q''"
          by (fact tau_transition_trans)
        moreover from ‹P ≈⋅ R'› and ‹R' ≈⋅ Q''› have "?bisim P Q''"
          by blast
        ultimately show "∃Q'. Q ⇒ Q' ∧ ?bisim P Q' ∧ Q' ⊢ φ"
          using ** by metis
      qed
    moreover have "∀P Q. ?bisim P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q ⇒⟨α⟩ Q' ∧ ?bisim P' Q'))"
      proof (clarify)
        fix P Q R α 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
        with trans obtain pR' where 5: "R ⇒⟨p ∙ α⟩ pR'" and 6: "(p ∙ P') ≈⋅ pR'"
          using PR 1 by (metis bn_eqvt weakly_bisimilar_is_weak_bisimulation is_weak_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 weakly_bisimilar_weak_simulation_step)
        from 7 have "Q ⇒⟨α⟩ (-p ∙ pQ')"
          using 4 by (metis permute_minus_cancel(2) supp_perm_eq weak_transition_eqvt)
        moreover from 6 and 8 have "?bisim P' (-p ∙ pQ')"
          by (metis (no_types, opaque_lifting) weakly_bisimilar_eqvt permute_minus_cancel(2) relcompp.simps)
        ultimately show "∃Q'. Q ⇒⟨α⟩ Q' ∧ ?bisim P' Q'"
          by metis
      qed
    ultimately have "is_weak_bisimulation ?bisim"
      unfolding is_weak_bisimulation_def by metis
    moreover have "?bisim P R"
      using PQ QR by blast
    ultimately show "P ≈⋅ R"
      unfolding weakly_bisimilar_def by meson
  qed

  lemma weakly_bisimilar_equivp: "equivp weakly_bisimilar"
  by (metis weakly_bisimilar_reflp weakly_bisimilar_symp weakly_bisimilar_transp equivp_reflp_symp_transp)

end

end