Documentation

Foundation.Modal.NNFormula

source
inductive LO.Modal.NNFormula (α : Type u) :
Type u
Instances For
    source
    instance LO.Modal.instDecidableEqNNFormula {α✝ : Type u_1} [DecidableEq α✝] :
    DecidableEq (NNFormula α✝)
    Equations
    source
    def LO.Modal.NNFormula.neg {α : Type u} :
    NNFormula α → NNFormula α
    Equations
    Instances For
      source
      def LO.Modal.NNFormula.imp {α : Type u} (φ ψ : NNFormula α) :
      NNFormula α
      Equations
      • φ.imp ψ = φ.neg.or ψ
      Instances For
        source
        instance LO.Modal.NNFormula.instBasicModalLogicalConnective {α : Type u} :
        BasicModalLogicalConnective (NNFormula α)
        Equations
        source
        theorem LO.Modal.NNFormula.or_eq {α : Type u} {φ ψ : NNFormula α} :
        φ.or ψ = φ ⋎ ψ
        source
        theorem LO.Modal.NNFormula.and_eq {α : Type u} {φ ψ : NNFormula α} :
        φ.and ψ = φ ⋏ ψ
        source
        theorem LO.Modal.NNFormula.imp_eq {α : Type u} {φ ψ : NNFormula α} :
        φ.imp ψ = φ ➝ ψ
        source
        theorem LO.Modal.NNFormula.box_eq {α : Type u} {φ : NNFormula α} :
        φ.box = □φ
        source
        theorem LO.Modal.NNFormula.dia_eq {α : Type u} {φ : NNFormula α} :
        φ.dia = ◇φ
        source
        @[simp]
        theorem LO.Modal.NNFormula.imp_eq' {α : Type u} {φ ψ : NNFormula α} :
        φ ➝ ψ = ∼φ ⋎ ψ
        source
        @[simp]
        theorem LO.Modal.NNFormula.iff_eq {α : Type u} {φ ψ : NNFormula α} :
        φ ⭤ ψ = (φ ➝ ψ) ⋏ (ψ ➝ φ)
        source
        theorem LO.Modal.NNFormula.falsum_eq {α : Type u} :
        falsum = ⊥
        source
        theorem LO.Modal.NNFormula.verum_eq {α : Type u} :
        verum = ⊤
        source
        @[simp]
        theorem LO.Modal.NNFormula.and_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) :
        φ₁ ⋏ φ₂ = ψ₁ ⋏ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂
        source
        @[simp]
        theorem LO.Modal.NNFormula.or_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) :
        φ₁ ⋎ φ₂ = ψ₁ ⋎ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂
        source
        @[simp]
        theorem LO.Modal.NNFormula.imp_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) :
        φ₁ ➝ φ₂ = ψ₁ ➝ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂
        source
        @[simp]
        theorem LO.Modal.NNFormula.neg_inj {α : Type u} (φ ψ : Formula α) :
        ∼φ = ∼ψ ↔ φ = ψ
        source
        theorem LO.Modal.NNFormula.neg_eq {α : Type u} {φ : NNFormula α} :
        φ.neg = ∼φ
        source
        @[simp]
        theorem LO.Modal.NNFormula.neg_atom {α : Type u} (a : α) :
        ∼atom a = natom a
        source
        @[simp]
        theorem LO.Modal.NNFormula.neg_natom {α : Type u} (a : α) :
        ∼natom a = atom a
        source
        theorem LO.Modal.NNFormula.negneg {α : Type u} {φ : NNFormula α} :
        ∼∼φ = φ
        source
        instance LO.Modal.NNFormula.instModalDeMorgan {α : Type u} :
        ModalDeMorgan (NNFormula α)
        source
        def LO.Modal.NNFormula.toStr {α : Type u} [ToString α] :
        NNFormula α → String
        Equations
        Instances For
          source
          instance LO.Modal.NNFormula.instRepr {α : Type u} [ToString α] :
          Repr (NNFormula α)
          Equations
          source
          def LO.Modal.NNFormula.toFormula {α : Type u} :
          NNFormula α → Formula α
          Equations
          Instances For
            source
            instance LO.Modal.NNFormula.instCoeFormula {α : Type u} :
            Coe (NNFormula α) (Formula α)
            Equations
            source
            @[simp]
            theorem LO.Modal.NNFormula.toFormula_atom {α : Type u} (a : α) :
            (atom a).toFormula = Formula.atom a
            source
            @[simp]
            theorem LO.Modal.NNFormula.toFormula_natom {α : Type u} (a : α) :
            (natom a).toFormula = ∼Formula.atom a
            source
            @[simp]
            theorem LO.Modal.NNFormula.toFormula_falsum {α : Type u} :
            ⊥.toFormula = ⊥
            source
            @[simp]
            theorem LO.Modal.NNFormula.toFormula_verum {α : Type u} :
            ⊤.toFormula = ⊤
            source
            def LO.Modal.NNFormula.cases' {α : Type u} {C : NNFormula α → Sort v} (hAtom : (a : α) → C (atom a)) (hNatom : (a : α) → C (natom a)) (hFalsum : C ⊥) (hVerum : C ⊤) (hOr : (φ ψ : NNFormula α) → C (φ ⋎ ψ)) (hAnd : (φ ψ : NNFormula α) → C (φ ⋏ ψ)) (hBox : (φ : NNFormula α) → C (□φ)) (hDia : (φ : NNFormula α) → C (◇φ)) (φ : NNFormula α) :
            C φ
            Equations
            Instances For
              source
              def LO.Modal.NNFormula.rec' {α : Type u} {C : NNFormula α → Sort v} (hAtom : (a : α) → C (atom a)) (hNatom : (a : α) → C (natom a)) (hFalsum : C ⊥) (hVerum : C ⊤) (hOr : (φ ψ : NNFormula α) → C φ → C ψ → C (φ ⋎ ψ)) (hAnd : (φ ψ : NNFormula α) → C φ → C ψ → C (φ ⋏ ψ)) (hBox : (φ : NNFormula α) → C φ → C (□φ)) (hDia : (φ : NNFormula α) → C φ → C (◇φ)) (φ : NNFormula α) :
              C φ
              Equations
              Instances For
                source
                def LO.Modal.NNFormula.toNat {α : Type u} [Encodable α] :
                NNFormula α → ℕ
                Equations
                Instances For
                  source
                  @[irreducible]
                  def LO.Modal.NNFormula.ofNat {α : Type u} [Encodable α] :
                  ℕ → Option (NNFormula α)
                  Equations
                  Instances For
                    source
                    instance LO.Modal.NNFormula.instEncodable {α : Type u} [Encodable α] :
                    Encodable (NNFormula α)
                    Equations
                    source
                    def LO.Modal.Formula.toNNFormula {α : Type u} :
                    Formula α → NNFormula α
                    Equations
                    Instances For
                      source
                      instance LO.Modal.Formula.instCoeNNFormula {α : Type u} :
                      Coe (Formula α) (NNFormula α)
                      Equations
                      source
                      @[simp]
                      theorem LO.Modal.Formula.toNNFormula_atom {α : Type u} (a : α) :
                      (atom a).toNNFormula = NNFormula.atom a
                      source
                      @[simp]
                      theorem LO.Modal.Formula.toNNFormula_falsum {α : Type u} :
                      ⊥.toNNFormula = ⊥