# Theory Weak_Validity

```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
```