theory Weak_Validity imports Weak_Formula Validity begin section ‹Weak Validity› text ‹Weak formulas are a subset of (strong) formulas, and the definition of validity is simply taken from the latter. Here we prove some useful lemmas about the validity of weak modalities. These are similar to corresponding lemmas about the validity of the (strong) action modality.› context indexed_weak_nominal_ts begin lemma valid_weak_tau_modality_iff_tau_steps: "P ⊨ weak_tau_modality x ⟷ (∃n. P ⊨ tau_steps x n)" unfolding weak_tau_modality_def by (auto simp add: map_bset.rep_eq) lemma tau_steps_iff_tau_transition: "(∃n. P ⊨ tau_steps x n) ⟷ (∃P'. P ⇒ P' ∧ P' ⊨ x)" proof assume "∃n. P ⊨ tau_steps x n" then obtain n where "P ⊨ tau_steps x n" by meson then show "∃P'. P ⇒ P' ∧ P' ⊨ x" proof (induct n arbitrary: P) case 0 then show ?case by simp (metis tau_refl) next case (Suc n) then obtain P' where "P → ⟨τ, P'⟩" and "P' ⊨ tau_steps x n" by (auto simp add: valid_Act_fresh[OF bn_tau_fresh]) with Suc.hyps show ?case using tau_step by blast qed next assume "∃P'. P ⇒ P' ∧ P' ⊨ x" then obtain P' where "P ⇒ P'" and "P' ⊨ x" by meson then show "∃n. P ⊨ tau_steps x n" proof (induct) case (tau_refl P) then have "P ⊨ tau_steps x 0" by simp then show ?case by meson next case (tau_step P P' P'') then obtain n where "P' ⊨ tau_steps x n" by meson with ‹P → ⟨τ,P'⟩› have "P ⊨ tau_steps x (Suc n)" by (auto simp add: valid_Act_fresh[OF bn_tau_fresh]) then show ?case by meson qed qed lemma valid_weak_tau_modality: "P ⊨ weak_tau_modality x ⟷ (∃P'. P ⇒ P' ∧ P' ⊨ x)" by (metis valid_weak_tau_modality_iff_tau_steps tau_steps_iff_tau_transition) lemma valid_weak_action_modality: "P ⊨ (⟨⟨α⟩⟩x) ⟷ (∃α' x' P'. Act α x = Act α' x' ∧ P ⇒⟨α'⟩ P' ∧ P' ⊨ x')" (is "?l ⟷ ?r") proof (cases "α = τ") case True show ?thesis proof assume "?l" with ‹α = τ› obtain P' where trans: "P ⇒ P'" and valid: "P' ⊨ x" by (metis valid_weak_tau_modality weak_action_modality_tau) from trans have "P ⇒⟨τ⟩ P'" by simp with ‹α = τ› and valid show "?r" by blast next assume "?r" then obtain α' x' P' where eq: "Act α x = Act α' x'" and trans: "P ⇒⟨α'⟩ P'" and valid: "P' ⊨ x'" by blast from eq have "α' = τ ∧ x' = x" using ‹α = τ› by simp with trans and valid have "P ⇒ P'" and "P' ⊨ x" by simp+ with ‹α = τ› show "?l" by (metis valid_weak_tau_modality weak_action_modality_tau) qed next case False show ?thesis proof assume "?l" with ‹α ≠ τ› obtain Q where trans: "P ⇒ Q" and valid: "Q ⊨ Act α (weak_tau_modality x)" by (metis valid_weak_tau_modality weak_action_modality_not_tau) from valid obtain α' x' Q' where eq: "Act α (weak_tau_modality x) = Act α' x'" and trans': "Q → ⟨α',Q'⟩" and valid': "Q' ⊨ x'" by (metis valid_Act) from eq obtain p where p_α: "α' = p ∙ α" and p_x: "x' = p ∙ weak_tau_modality x" by (metis Act_eq_iff_perm) with eq have "Act α x = Act α' (p ∙ x)" using Act_weak_tau_modality_eq_iff by simp moreover from valid' and p_x have "Q' ⊨ weak_tau_modality (p ∙ x)" by simp then obtain P' where trans'': "Q' ⇒ P'" and valid'': "P' ⊨ p ∙ x" by (metis valid_weak_tau_modality) from trans and trans' and trans'' have "P ⇒⟨α'⟩ P'" by (metis observable_transitionI weak_transition_stepI) ultimately show "?r" using valid'' by blast next assume "?r" then obtain α' x' P' where eq: "Act α x = Act α' x'" and trans: "P ⇒⟨α'⟩ P'" and valid: "P' ⊨ x'" by blast with ‹α ≠ τ› have α': "α' ≠ τ" using eq by (metis Act_tau_eq_iff) with trans obtain Q Q' where trans': "P ⇒ Q" and trans'': "Q → ⟨α',Q'⟩" and trans''': "Q' ⇒ P'" by (meson observable_transition_def weak_transition_def) from trans''' and valid have "Q' ⊨ weak_tau_modality x'" by (metis valid_weak_tau_modality) with trans'' have "Q ⊨ Act α' (weak_tau_modality x')" by (metis valid_Act) with trans' and α' have "P ⊨ ⟨⟨α'⟩⟩x'" by (metis valid_weak_tau_modality weak_action_modality_not_tau) moreover from eq have "(⟨⟨α⟩⟩x) = (⟨⟨α'⟩⟩x')" by (metis weak_action_modality_eq) ultimately show "?l" by simp qed qed text ‹The binding names in the alpha-variant that witnesses validity may be chosen fresh for any finitely supported context.› lemma valid_weak_action_modality_strong: assumes "finite (supp X)" shows "P ⊨ (⟨⟨α⟩⟩x) ⟷ (∃α' x' P'. Act α x = Act α' x' ∧ P ⇒⟨α'⟩ P' ∧ P' ⊨ x' ∧ bn α' ♯* X)" proof assume "P ⊨ ⟨⟨α⟩⟩x" then obtain α' x' P' where eq: "Act α x = Act α' x'" and trans: "P ⇒⟨α'⟩ P'" and valid: "P' ⊨ x'" by (metis valid_weak_action_modality) show "∃α' x' P'. Act α x = Act α' x' ∧ P ⇒⟨α'⟩ P' ∧ P' ⊨ x' ∧ bn α' ♯* X" proof (cases "α' = τ") case True then show ?thesis using eq and trans and valid and bn_tau_fresh by blast next case False with trans obtain Q Q' where trans': "P ⇒ Q" and trans'': "Q → ⟨α', Q'⟩" and trans''': "Q' ⇒ P'" by (metis weak_transition_def observable_transition_def) have "finite (bn α')" by (fact bn_finite) moreover note ‹finite (supp X)› moreover have "finite (supp (Act α' x', ⟨α',Q'⟩))" by (metis finite_Diff finite_UnI finite_supp supp_Pair supp_abs_residual_pair) moreover have "bn α' ♯* (Act α' x', ⟨α',Q'⟩)" by (auto simp add: fresh_star_def fresh_def supp_Pair supp_abs_residual_pair) ultimately obtain p where fresh_X: "(p ∙ bn α') ♯* X" and "supp (Act α' x', ⟨α',Q'⟩) ♯* p" by (metis at_set_avoiding2) then have "supp (Act α' x') ♯* p" and "supp ⟨α',Q'⟩ ♯* p" by (metis fresh_star_Un supp_Pair)+ then have 1: "Act (p ∙ α') (p ∙ x') = Act α' x'" and 2: "⟨p ∙ α', p ∙ Q'⟩ = ⟨α',Q'⟩" by (metis Act_eqvt supp_perm_eq, metis abs_residual_pair_eqvt supp_perm_eq) from trans' and trans'' and trans''' have "P ⇒⟨p ∙ α'⟩ (p ∙ P')" using 2 by (metis observable_transitionI tau_transition_eqvt weak_transition_stepI) then show ?thesis using eq and 1 and valid and fresh_X by (metis bn_eqvt valid_eqvt) qed next assume "∃α' x' P'. Act α x = Act α' x' ∧ P ⇒⟨α'⟩ P' ∧ P' ⊨ x' ∧ bn α' ♯* X" then show "P ⊨ ⟨⟨α⟩⟩x" by (metis valid_weak_action_modality) qed lemma valid_weak_action_modality_fresh: assumes "bn α ♯* P" shows "P ⊨ (⟨⟨α⟩⟩x) ⟷ (∃P'. P ⇒⟨α⟩ P' ∧ P' ⊨ x)" proof assume "P ⊨ ⟨⟨α⟩⟩x" moreover have "finite (supp P)" by (fact finite_supp) ultimately obtain α' x' P' where eq: "Act α x = Act α' x'" and trans: "P ⇒⟨α'⟩ P'" and valid: "P' ⊨ x'" and fresh: "bn α' ♯* P" by (metis valid_weak_action_modality_strong) from eq obtain p where p_α: "α' = p ∙ α" and p_x: "x' = p ∙ x" and supp_p: "supp p ⊆ bn α ∪ p ∙ bn α" by (metis Act_eq_iff_perm_renaming) from assms and fresh have "(bn α ∪ p ∙ bn α) ♯* P" using p_α by (metis bn_eqvt fresh_star_Un) then have "supp p ♯* P" using supp_p by (metis fresh_star_def subset_eq) then have p_P: "-p ∙ P = P" by (metis perm_supp_eq supp_minus_perm) from trans have "P ⇒⟨α⟩ (-p ∙ P')" using p_P p_α by (metis permute_minus_cancel(1) weak_transition_eqvt) moreover from valid have "-p ∙ P' ⊨ x" using p_x by (metis permute_minus_cancel(1) valid_eqvt) ultimately show "∃P'. P ⇒⟨α⟩ P' ∧ P' ⊨ x" by meson next assume "∃P'. P ⇒⟨α⟩ P' ∧ P' ⊨ x" then show "P ⊨ ⟨⟨α⟩⟩x" by (metis valid_weak_action_modality) qed end end