inductive LO.Propositional.Classical.Formula (α : Type u) : Type u

• verum {α : Type u} : Formula α
• falsum {α : Type u} : Formula α
• atom {α : Type u} : α → Formula α
• natom {α : Type u} : α → Formula α
• and {α : Type u} : Formula α → Formula α → Formula α
• or {α : Type u} : Formula α → Formula α → Formula α

def LO.Propositional.Classical.Formula.neg {α : Type u} : Formula α → Formula α

Equations

• LO.Propositional.Classical.Formula.verum.neg = LO.Propositional.Classical.Formula.falsum
• LO.Propositional.Classical.Formula.falsum.neg = LO.Propositional.Classical.Formula.verum
• (LO.Propositional.Classical.Formula.atom a).neg = LO.Propositional.Classical.Formula.natom a
• (LO.Propositional.Classical.Formula.natom a).neg = LO.Propositional.Classical.Formula.atom a
• (φ.and ψ).neg = φ.neg.or ψ.neg
• (φ.or ψ).neg = φ.neg.and ψ.neg

theorem LO.Propositional.Classical.Formula.neg_neg {α : Type u} (φ : Formula α) : φ.neg.neg = φ

instance LO.Propositional.Classical.Formula.instLogicalConnective {α : Type u} : LogicalConnective (Formula α)

Equations

• LO.Propositional.Classical.Formula.instLogicalConnective = LO.LogicalConnective.mk

def LO.Propositional.Classical.Formula.toStr {α : Type u} [ToString α] : Formula α → String

Equations

• LO.Propositional.Classical.Formula.verum.toStr = "\\top"
• LO.Propositional.Classical.Formula.falsum.toStr = "\\bot"
• (LO.Propositional.Classical.Formula.atom a).toStr = "{" ++ toString a ++ "}"
• (LO.Propositional.Classical.Formula.natom a).toStr = "\\lnot {" ++ toString a ++ "}"
• (φ.and ψ).toStr = "\\left(" ++ φ.toStr ++ " \\land " ++ ψ.toStr ++ "\\right)"
• (φ.or ψ).toStr = "\\left(" ++ φ.toStr ++ " \\lor " ++ ψ.toStr ++ "\\right)"

instance LO.Propositional.Classical.Formula.instRepr {α : Type u} [ToString α] : Repr (Formula α)

Equations

• LO.Propositional.Classical.Formula.instRepr = { reprPrec := fun (t : LO.Propositional.Classical.Formula α) (x : ℕ) => Std.Format.text t.toStr }

instance LO.Propositional.Classical.Formula.instToString {α : Type u} [ToString α] : ToString (Formula α)

Equations

• LO.Propositional.Classical.Formula.instToString = { toString := LO.Propositional.Classical.Formula.toStr }

@[simp]

theorem LO.Propositional.Classical.Formula.neg_top {α : Type u} : ∼⊤ = ⊥

@[simp]

theorem LO.Propositional.Classical.Formula.neg_bot {α : Type u} : ∼⊥ = ⊤

@[simp]

theorem LO.Propositional.Classical.Formula.neg_atom {α : Type u} (a : α) : ∼atom a = natom a

@[simp]

theorem LO.Propositional.Classical.Formula.neg_natom {α : Type u} (a : α) : ∼natom a = atom a

@[simp]

theorem LO.Propositional.Classical.Formula.neg_and {α : Type u} (φ ψ : Formula α) : ∼(φ ⋏ ψ) = ∼φ ⋎ ∼ψ

@[simp]

theorem LO.Propositional.Classical.Formula.neg_or {α : Type u} (φ ψ : Formula α) : ∼(φ ⋎ ψ) = ∼φ ⋏ ∼ψ

@[simp]

theorem LO.Propositional.Classical.Formula.neg_neg' {α : Type u} (φ : Formula α) : ∼∼φ = φ

@[simp]

theorem LO.Propositional.Classical.Formula.neg_inj {α : Type u} (φ ψ : Formula α) : ∼φ = ∼ψ ↔ φ = ψ

theorem LO.Propositional.Classical.Formula.neg_eq {α : Type u} (φ : Formula α) : ∼φ = φ.neg

theorem LO.Propositional.Classical.Formula.imp_eq {α : Type u} (φ ψ : Formula α) : φ ➝ ψ = ∼φ ⋎ ψ

theorem LO.Propositional.Classical.Formula.iff_eq {α : Type u} (φ ψ : Formula α) : φ ⭤ ψ = (∼φ ⋎ ψ) ⋏ (∼ψ ⋎ φ)

@[simp]

theorem LO.Propositional.Classical.Formula.and_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) : φ₁ ⋏ φ₂ = ψ₁ ⋏ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.Propositional.Classical.Formula.or_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) : φ₁ ⋎ φ₂ = ψ₁ ⋎ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

instance LO.Propositional.Classical.Formula.instDeMorgan {α : Type u} : DeMorgan (Formula α)

def LO.Propositional.Classical.Formula.complexity {α : Type u} : Formula α → ℕ

Equations

• LO.Propositional.Classical.Formula.verum.complexity = 0
• LO.Propositional.Classical.Formula.falsum.complexity = 0
• (LO.Propositional.Classical.Formula.atom a).complexity = 0
• (LO.Propositional.Classical.Formula.natom a).complexity = 0
• (φ.and ψ).complexity = φ.complexity ⊔ ψ.complexity + 1
• (φ.or ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

@[simp]

theorem LO.Propositional.Classical.Formula.complexity_top {α : Type u} : ⊤.complexity = 0

@[simp]

theorem LO.Propositional.Classical.Formula.complexity_bot {α : Type u} : ⊥.complexity = 0

@[simp]

theorem LO.Propositional.Classical.Formula.complexity_atom {α : Type u} (a : α) : (atom a).complexity = 0

@[simp]

theorem LO.Propositional.Classical.Formula.complexity_natom {α : Type u} (a : α) : (natom a).complexity = 0

@[simp]

theorem LO.Propositional.Classical.Formula.complexity_and {α : Type u} (φ ψ : Formula α) : (φ ⋏ ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

@[simp]

theorem LO.Propositional.Classical.Formula.complexity_and' {α : Type u} (φ ψ : Formula α) : (φ.and ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

@[simp]

theorem LO.Propositional.Classical.Formula.complexity_or {α : Type u} (φ ψ : Formula α) : (φ ⋎ ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

@[simp]

theorem LO.Propositional.Classical.Formula.complexity_or' {α : Type u} (φ ψ : Formula α) : (φ.or ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

def LO.Propositional.Classical.Formula.cases' {α : Type u} {C : Formula α → Sort w} (hverum : C ⊤) (hfalsum : C ⊥) (hatom : (a : α) → C (atom a)) (hnatom : (a : α) → C (natom a)) (hand : (φ ψ : Formula α) → C (φ ⋏ ψ)) (hor : (φ ψ : Formula α) → C (φ ⋎ ψ)) (φ : Formula α) : C φ

Equations

• LO.Propositional.Classical.Formula.cases' hverum hfalsum hatom hnatom hand hor LO.Propositional.Classical.Formula.verum = hverum
• LO.Propositional.Classical.Formula.cases' hverum hfalsum hatom hnatom hand hor LO.Propositional.Classical.Formula.falsum = hfalsum
• LO.Propositional.Classical.Formula.cases' hverum hfalsum hatom hnatom hand hor (LO.Propositional.Classical.Formula.atom a) = hatom a
• LO.Propositional.Classical.Formula.cases' hverum hfalsum hatom hnatom hand hor (LO.Propositional.Classical.Formula.natom a) = hnatom a
• LO.Propositional.Classical.Formula.cases' hverum hfalsum hatom hnatom hand hor (φ.and ψ) = hand φ ψ
• LO.Propositional.Classical.Formula.cases' hverum hfalsum hatom hnatom hand hor (φ.or ψ) = hor φ ψ

def LO.Propositional.Classical.Formula.rec' {α : Type u} {C : Formula α → Sort w} (hverum : C ⊤) (hfalsum : C ⊥) (hatom : (a : α) → C (atom a)) (hnatom : (a : α) → C (natom a)) (hand : (φ ψ : Formula α) → C φ → C ψ → C (φ ⋏ ψ)) (hor : (φ ψ : Formula α) → C φ → C ψ → C (φ ⋎ ψ)) (φ : Formula α) : C φ

Equations

• One or more equations did not get rendered due to their size.
• LO.Propositional.Classical.Formula.rec' hverum hfalsum hatom hnatom hand hor LO.Propositional.Classical.Formula.verum = hverum
• LO.Propositional.Classical.Formula.rec' hverum hfalsum hatom hnatom hand hor LO.Propositional.Classical.Formula.falsum = hfalsum
• LO.Propositional.Classical.Formula.rec' hverum hfalsum hatom hnatom hand hor (LO.Propositional.Classical.Formula.atom a) = hatom a
• LO.Propositional.Classical.Formula.rec' hverum hfalsum hatom hnatom hand hor (LO.Propositional.Classical.Formula.natom a) = hnatom a

@[simp]

theorem LO.Propositional.Classical.Formula.complexity_neg {α : Type u} (φ : Formula α) : (∼φ).complexity = φ.complexity

def LO.Propositional.Classical.Formula.hasDecEq {α : Type u} [DecidableEq α] (φ ψ : Formula α) : Decidable (φ = ψ)

Equations

• One or more equations did not get rendered due to their size.

instance LO.Propositional.Classical.Formula.instDecidableEq {α : Type u} [DecidableEq α] : DecidableEq (Formula α)

Equations

• LO.Propositional.Classical.Formula.instDecidableEq = LO.Propositional.Classical.Formula.hasDecEq

theorem LO.Propositional.Classical.Formula.ne_of_ne_complexity {α : Type u} {φ ψ : Formula α} (h : φ.complexity ≠ ψ.complexity) : φ ≠ ψ

@[reducible, inline]

abbrev LO.Propositional.Classical.Theory (α : Type u_1) : Type u_1

Equations

• LO.Propositional.Classical.Theory α = Set (LO.Propositional.Classical.Formula α)

instance LO.Propositional.Classical.instCollectionFormulaTheory {α : Type u_1} : Collection (Formula α) (Theory α)

Equations

• LO.Propositional.Classical.instCollectionFormulaTheory = inferInstance