Foundation.Modal.NNFormula

source

inductive LO.Modal.NNFormula (α : Type u) :

Type u

atom: {α : Type u} → α → LO.Modal.NNFormula α
natom: {α : Type u} → α → LO.Modal.NNFormula α
falsum: {α : Type u} → LO.Modal.NNFormula α
verum: {α : Type u} → LO.Modal.NNFormula α
or: {α : Type u} → LO.Modal.NNFormula α → LO.Modal.NNFormula α → LO.Modal.NNFormula α
and: {α : Type u} → LO.Modal.NNFormula α → LO.Modal.NNFormula α → LO.Modal.NNFormula α
box: {α : Type u} → LO.Modal.NNFormula α → LO.Modal.NNFormula α
dia: {α : Type u} → LO.Modal.NNFormula α → LO.Modal.NNFormula α

Instances For

source

instance LO.Modal.instDecidableEqNNFormula {α✝ : Type u_1} [DecidableEq α✝] :

DecidableEq (LO.Modal.NNFormula α✝)

Equations

LO.Modal.instDecidableEqNNFormula = LO.Modal.decEqNNFormula✝

source

def LO.Modal.NNFormula.neg {α : Type u} :

LO.Modal.NNFormula α → LO.Modal.NNFormula α

Equations

(LO.Modal.NNFormula.atom a).neg = LO.Modal.NNFormula.natom a
(LO.Modal.NNFormula.natom a).neg = LO.Modal.NNFormula.atom a
LO.Modal.NNFormula.falsum.neg = LO.Modal.NNFormula.verum
LO.Modal.NNFormula.verum.neg = LO.Modal.NNFormula.falsum
(φ.or ψ).neg = φ.neg.and ψ.neg
(φ.and ψ).neg = φ.neg.or ψ.neg
φ.box.neg = φ.neg.dia
φ.dia.neg = φ.neg.box

Instances For

source

def LO.Modal.NNFormula.imp {α : Type u} (φ ψ : LO.Modal.NNFormula α) :

LO.Modal.NNFormula α

Equations

φ.imp ψ = φ.neg.or ψ

Instances For

source

instance LO.Modal.NNFormula.instBasicModalLogicalConnective {α : Type u} :

LO.BasicModalLogicalConnective (LO.Modal.NNFormula α)

Equations

LO.Modal.NNFormula.instBasicModalLogicalConnective = LO.BasicModalLogicalConnective.mk

source

theorem LO.Modal.NNFormula.or_eq {α : Type u} {φ ψ : LO.Modal.NNFormula α} :

φ.or ψ = φ ⋎ ψ

source

theorem LO.Modal.NNFormula.and_eq {α : Type u} {φ ψ : LO.Modal.NNFormula α} :

φ.and ψ = φ ⋏ ψ

source

theorem LO.Modal.NNFormula.imp_eq {α : Type u} {φ ψ : LO.Modal.NNFormula α} :

φ.imp ψ = φ ➝ ψ

source

theorem LO.Modal.NNFormula.box_eq {α : Type u} {φ : LO.Modal.NNFormula α} :

φ.box = □φ

source

theorem LO.Modal.NNFormula.dia_eq {α : Type u} {φ : LO.Modal.NNFormula α} :

φ.dia = ◇φ

source

@[simp]

theorem LO.Modal.NNFormula.imp_eq' {α : Type u} {φ ψ : LO.Modal.NNFormula α} :

φ ➝ ψ = ∼φ ⋎ ψ

source

@[simp]

theorem LO.Modal.NNFormula.iff_eq {α : Type u} {φ ψ : LO.Modal.NNFormula α} :

φ ⭤ ψ = (φ ➝ ψ) ⋏ (ψ ➝ φ)

source

theorem LO.Modal.NNFormula.falsum_eq {α : Type u} :

LO.Modal.NNFormula.falsum = ⊥

source

theorem LO.Modal.NNFormula.verum_eq {α : Type u} :

LO.Modal.NNFormula.verum = ⊤

source

@[simp]

theorem LO.Modal.NNFormula.and_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : LO.Modal.Formula α) :

φ₁ ⋏ φ₂ = ψ₁ ⋏ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

source

@[simp]

theorem LO.Modal.NNFormula.or_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : LO.Modal.Formula α) :

φ₁ ⋎ φ₂ = ψ₁ ⋎ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

source

@[simp]

theorem LO.Modal.NNFormula.imp_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : LO.Modal.Formula α) :

φ₁ ➝ φ₂ = ψ₁ ➝ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

source

@[simp]

theorem LO.Modal.NNFormula.neg_inj {α : Type u} (φ ψ : LO.Modal.Formula α) :

∼φ = ∼ψ ↔ φ = ψ

source

theorem LO.Modal.NNFormula.neg_eq {α : Type u} {φ : LO.Modal.NNFormula α} :

φ.neg = ∼φ

source

theorem LO.Modal.NNFormula.negneg {α : Type u} {φ : LO.Modal.NNFormula α} :

∼∼φ = φ

source

instance LO.Modal.NNFormula.instModalDeMorgan {α : Type u} :

LO.ModalDeMorgan (LO.Modal.NNFormula α)

Equations

⋯ = ⋯

source

def LO.Modal.NNFormula.toStr {α : Type u} [ToString α] :

LO.Modal.NNFormula α → String

Equations

(LO.Modal.NNFormula.atom a).toStr = toString "+" ++ toString a ++ toString ""
(LO.Modal.NNFormula.natom a).toStr = toString "-" ++ toString a ++ toString ""
LO.Modal.NNFormula.falsum.toStr = "⊥"
LO.Modal.NNFormula.verum.toStr = "⊤"
(φ.or ψ).toStr = toString "(" ++ toString φ.toStr ++ toString " ∨ " ++ toString ψ.toStr ++ toString ")"
(φ.and ψ).toStr = toString "(" ++ toString φ.toStr ++ toString " ∧ " ++ toString ψ.toStr ++ toString ")"
φ.box.toStr = toString "□" ++ toString φ.toStr ++ toString ""
φ.dia.toStr = toString "◇" ++ toString φ.toStr ++ toString ""

Instances For

source

instance LO.Modal.NNFormula.instRepr {α : Type u} [ToString α] :

Repr (LO.Modal.NNFormula α)

Equations

LO.Modal.NNFormula.instRepr = { reprPrec := fun (t : LO.Modal.NNFormula α) (x : ℕ) => Std.Format.text t.toStr }

source

def LO.Modal.NNFormula.toFormula {α : Type u} :

LO.Modal.NNFormula α → LO.Modal.Formula α

Equations

(LO.Modal.NNFormula.atom a).toFormula = LO.Modal.Formula.atom a
(LO.Modal.NNFormula.natom a).toFormula = ∼LO.Modal.Formula.atom a
LO.Modal.NNFormula.falsum.toFormula = ⊥
LO.Modal.NNFormula.verum.toFormula = ⊤
(φ.or ψ).toFormula = φ.toFormula ⋎ ψ.toFormula
(φ.and ψ).toFormula = φ.toFormula ⋏ ψ.toFormula
φ.box.toFormula = □φ.toFormula
φ.dia.toFormula = ◇φ.toFormula

Instances For

source

instance LO.Modal.NNFormula.instCoeFormula {α : Type u} :

Coe (LO.Modal.NNFormula α) (LO.Modal.Formula α)

Equations

LO.Modal.NNFormula.instCoeFormula = { coe := LO.Modal.NNFormula.toFormula }

source

def LO.Modal.NNFormula.cases' {α : Type u} {C : LO.Modal.NNFormula α → Sort v} (hAtom : (a : α) → C (LO.Modal.NNFormula.atom a)) (hNatom : (a : α) → C (LO.Modal.NNFormula.natom a)) (hFalsum : C ⊥) (hVerum : C ⊤) (hOr : (φ ψ : LO.Modal.NNFormula α) → C (φ ⋎ ψ)) (hAnd : (φ ψ : LO.Modal.NNFormula α) → C (φ ⋏ ψ)) (hBox : (φ : LO.Modal.NNFormula α) → C (□φ)) (hDia : (φ : LO.Modal.NNFormula α) → C (◇φ)) (φ : LO.Modal.NNFormula α) :

C φ

Equations

LO.Modal.NNFormula.cases' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia (LO.Modal.NNFormula.atom a) = hAtom a
LO.Modal.NNFormula.cases' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia (LO.Modal.NNFormula.natom a) = hNatom a
LO.Modal.NNFormula.cases' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia LO.Modal.NNFormula.falsum = hFalsum
LO.Modal.NNFormula.cases' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia LO.Modal.NNFormula.verum = hVerum
LO.Modal.NNFormula.cases' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia (φ.or ψ) = hOr φ ψ
LO.Modal.NNFormula.cases' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia (φ.and ψ) = hAnd φ ψ
LO.Modal.NNFormula.cases' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia φ.box = hBox φ
LO.Modal.NNFormula.cases' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia φ.dia = hDia φ

Instances For

source

def LO.Modal.NNFormula.rec' {α : Type u} {C : LO.Modal.NNFormula α → Sort v} (hAtom : (a : α) → C (LO.Modal.NNFormula.atom a)) (hNatom : (a : α) → C (LO.Modal.NNFormula.natom a)) (hFalsum : C ⊥) (hVerum : C ⊤) (hOr : (φ ψ : LO.Modal.NNFormula α) → C φ → C ψ → C (φ ⋎ ψ)) (hAnd : (φ ψ : LO.Modal.NNFormula α) → C φ → C ψ → C (φ ⋏ ψ)) (hBox : (φ : LO.Modal.NNFormula α) → C φ → C (□φ)) (hDia : (φ : LO.Modal.NNFormula α) → C φ → C (◇φ)) (φ : LO.Modal.NNFormula α) :

C φ

Equations

One or more equations did not get rendered due to their size.
LO.Modal.NNFormula.rec' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia (LO.Modal.NNFormula.atom a) = hAtom a
LO.Modal.NNFormula.rec' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia (LO.Modal.NNFormula.natom a) = hNatom a
LO.Modal.NNFormula.rec' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia LO.Modal.NNFormula.falsum = hFalsum
LO.Modal.NNFormula.rec' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia LO.Modal.NNFormula.verum = hVerum
LO.Modal.NNFormula.rec' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia φ.box = hBox φ (LO.Modal.NNFormula.rec' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia φ)
LO.Modal.NNFormula.rec' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia φ.dia = hDia φ (LO.Modal.NNFormula.rec' hAtom hNatom hFalsum hVerum hOr hAnd hBox hDia φ)