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