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