- 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 α
Instances For
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
Instances For
theorem
LO.Propositional.Classical.Formula.neg_neg
{α : Type u}
(p : LO.Propositional.Classical.Formula α)
:
p.neg.neg = p
Equations
- LO.Propositional.Classical.Formula.instLogicalConnective = LO.LogicalConnective.mk
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)"
Instances For
Equations
- LO.Propositional.Classical.Formula.instRepr = { reprPrec := fun (t : LO.Propositional.Classical.Formula α) (x : ℕ) => Std.Format.text t.toStr }
Equations
- LO.Propositional.Classical.Formula.instToString = { toString := LO.Propositional.Classical.Formula.toStr }
@[simp]
@[simp]
@[simp]
theorem
LO.Propositional.Classical.Formula.neg_and
{α : Type u}
(p : LO.Propositional.Classical.Formula α)
(q : LO.Propositional.Classical.Formula α)
:
@[simp]
theorem
LO.Propositional.Classical.Formula.neg_or
{α : Type u}
(p : LO.Propositional.Classical.Formula α)
(q : LO.Propositional.Classical.Formula α)
:
@[simp]
theorem
LO.Propositional.Classical.Formula.neg_neg'
{α : Type u}
(p : LO.Propositional.Classical.Formula α)
:
@[simp]
theorem
LO.Propositional.Classical.Formula.neg_inj
{α : Type u}
(p : LO.Propositional.Classical.Formula α)
(q : LO.Propositional.Classical.Formula α)
:
theorem
LO.Propositional.Classical.Formula.neg_eq
{α : Type u}
(p : LO.Propositional.Classical.Formula α)
:
theorem
LO.Propositional.Classical.Formula.imp_eq
{α : Type u}
(p : LO.Propositional.Classical.Formula α)
(q : LO.Propositional.Classical.Formula α)
:
theorem
LO.Propositional.Classical.Formula.iff_eq
{α : Type u}
(p : LO.Propositional.Classical.Formula α)
(q : LO.Propositional.Classical.Formula α)
:
@[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 α)
:
@[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 α)
:
Equations
- LO.Propositional.Classical.Formula.instDeMorgan = { verum := ⋯, falsum := ⋯, imply := ⋯, and := ⋯, or := ⋯, neg := ⋯ }
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
Instances For
@[simp]
@[simp]
@[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 α)
:
@[simp]
theorem
LO.Propositional.Classical.Formula.complexity_and'
{α : Type u}
(p : LO.Propositional.Classical.Formula α)
(q : LO.Propositional.Classical.Formula α)
:
@[simp]
theorem
LO.Propositional.Classical.Formula.complexity_or
{α : Type u}
(p : LO.Propositional.Classical.Formula α)
(q : LO.Propositional.Classical.Formula α)
:
@[simp]
theorem
LO.Propositional.Classical.Formula.complexity_or'
{α : Type u}
(p : LO.Propositional.Classical.Formula α)
(q : LO.Propositional.Classical.Formula α)
:
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.
Instances For
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
Instances For
@[simp]
theorem
LO.Propositional.Classical.Formula.complexity_neg
{α : Type u}
(p : LO.Propositional.Classical.Formula α)
:
def
LO.Propositional.Classical.Formula.hasDecEq
{α : Type u}
[DecidableEq α]
(p : LO.Propositional.Classical.Formula α)
(q : LO.Propositional.Classical.Formula α)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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]
Equations
Instances For
Equations
- LO.Propositional.Classical.instCollectionFormulaTheory = inferInstance