Theory Logical_Equivalence

theory Logical_Equivalence
imports
  Validity
begin

section ‹(Strong) Logical Equivalence›

text ‹The definition of formulas is parametric in the index type, but from now on we want to work
with a fixed (sufficiently large) index type.›

locale indexed_nominal_ts = nominal_ts satisfies transition
  for satisfies :: "'state::fs ⇒ 'pred::fs ⇒ bool" (infix "⊢" 70)
  and transition :: "'state ⇒ ('act::bn,'state) residual ⇒ bool" (infix "→" 70) +
  assumes card_idx_perm: "|UNIV::perm set| <o |UNIV::'idx set|"
      and card_idx_state: "|UNIV::'state set| <o |UNIV::'idx set|"
begin

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

  notation logically_equivalent (infix "=⋅" 50)

  lemma logically_equivalent_eqvt:
    assumes "P =⋅ Q" shows "p ∙ P =⋅ p ∙ Q"
  using assms unfolding logically_equivalent_def
  by (metis (mono_tags) permute_minus_cancel(1) valid_eqvt)

end

end