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