Theory Weak_Logical_Equivalence

theory Weak_Logical_Equivalence
imports
  Weak_Formula
  Weak_Validity
begin

section ‹Weak Logical Equivalence›

context indexed_weak_nominal_ts
begin

  text ‹Two states are weakly logically equivalent if they validate the same weak formulas.›

  definition weakly_logically_equivalent :: "'state ⇒ 'state ⇒ bool" where
    "weakly_logically_equivalent P Q ≡ (∀x::('idx,'pred,'act) formula. weak_formula x ⟶ P ⊨ x ⟷ Q ⊨ x)"

  notation weakly_logically_equivalent (infix ‹≡⋅› 50)

  lemma weakly_logically_equivalent_eqvt:
    assumes "P ≡⋅ Q" shows "p ∙ P ≡⋅ p ∙ Q"
  unfolding weakly_logically_equivalent_def proof (clarify)
    fix x :: "('idx,'pred,'act) formula"
    assume "weak_formula x"
    then have "weak_formula (-p ∙ x)"
      by simp
    then show "p ∙ P ⊨ x ⟷ p ∙ Q ⊨ x"
      using assms by (metis (no_types, lifting) weakly_logically_equivalent_def permute_minus_cancel(2) valid_eqvt)
  qed

end

end