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

• verum: {α : Type u} → LO.Propositional.Classical.Formula α
• falsum: {α : Type u} → LO.Propositional.Classical.Formula α
• atom: {α : Type u} → α → LO.Propositional.Classical.Formula α
• natom: {α : Type u} → α → LO.Propositional.Classical.Formula α
• and: {α : Type u} → LO.Propositional.Classical.Formula α → LO.Propositional.Classical.Formula α → LO.Propositional.Classical.Formula α
• or: {α : Type u} → LO.Propositional.Classical.Formula α → LO.Propositional.Classical.Formula α → LO.Propositional.Classical.Formula α

def LO.Propositional.Classical.Formula.neg {α : Type u} : LO.Propositional.Classical.Formula α → LO.Propositional.Classical.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
• (p.and q).neg = p.neg.or q.neg
• (p.or q).neg = p.neg.and q.neg

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

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

Equations

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

def LO.Propositional.Classical.Formula.toStr {α : Type u} [ToString α] : LO.Propositional.Classical.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 ++ "}"
• (p.and q).toStr = "\left(" ++ p.toStr ++ " \land " ++ q.toStr ++ "\right)"
• (p.or q).toStr = "\left(" ++ p.toStr ++ " \lor " ++ q.toStr ++ "\right)"

instance LO.Propositional.Classical.Formula.instRepr {α : Type u} [ToString α] : Repr (LO.Propositional.Classical.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 (LO.Propositional.Classical.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 : α) : ∼LO.Propositional.Classical.Formula.atom a = LO.Propositional.Classical.Formula.natom a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

Equations

• LO.Propositional.Classical.Formula.instDeMorgan = { verum := ⋯, falsum := ⋯, imply := ⋯, and := ⋯, or := ⋯, neg := ⋯ }

def LO.Propositional.Classical.Formula.complexity {α : Type u} : LO.Propositional.Classical.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
• (p.and q).complexity = max p.complexity q.complexity + 1
• (p.or q).complexity = max p.complexity q.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 : α) : (LO.Propositional.Classical.Formula.atom a).complexity = 0

@[simp]

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

@[simp]

theorem LO.Propositional.Classical.Formula.complexity_and {α : Type u} (p : LO.Propositional.Classical.Formula α) (q : LO.Propositional.Classical.Formula α) : (p ⋏ q).complexity = max p.complexity q.complexity + 1

@[simp]

theorem LO.Propositional.Classical.Formula.complexity_and' {α : Type u} (p : LO.Propositional.Classical.Formula α) (q : LO.Propositional.Classical.Formula α) : (p.and q).complexity = max p.complexity q.complexity + 1

@[simp]

theorem LO.Propositional.Classical.Formula.complexity_or {α : Type u} (p : LO.Propositional.Classical.Formula α) (q : LO.Propositional.Classical.Formula α) : (p ⋎ q).complexity = max p.complexity q.complexity + 1

@[simp]

theorem LO.Propositional.Classical.Formula.complexity_or' {α : Type u} (p : LO.Propositional.Classical.Formula α) (q : LO.Propositional.Classical.Formula α) : (p.or q).complexity = max p.complexity q.complexity + 1

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

Equations

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

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

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} (p : LO.Propositional.Classical.Formula α) : (∼p).complexity = p.complexity

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

Equations

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

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

Equations

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

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

@[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 (LO.Propositional.Classical.Formula α) (LO.Propositional.Classical.Theory α)

Equations

• LO.Propositional.Classical.instCollectionFormulaTheory = inferInstance