Foundation.IntProp.Formula

LO.IntProp.Formula.verum.toStr = "\top"
LO.IntProp.Formula.falsum.toStr = "\bot"
(LO.IntProp.Formula.atom a).toStr = "{" ++ toString a ++ "}"
φ.neg.toStr = "\lnot " ++ φ.toStr
(φ.and ψ).toStr = "\left(" ++ φ.toStr ++ " \land " ++ ψ.toStr ++ "\right)"
(φ.or ψ).toStr = "\left(" ++ φ.toStr ++ " \lor " ++ ψ.toStr ++ "\right)"
(φ.imp ψ).toStr = "\left(" ++ φ.toStr ++ " \rightarrow " ++ ψ.toStr ++ "\right)"

source

instance LO.IntProp.Formula.instRepr {α : Type u_1} [ToString α] :

Repr (Formula α)

Equations

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

source

instance LO.IntProp.Formula.instToString {α : Type u_1} [ToString α] :

ToString (Formula α)

Equations

LO.IntProp.Formula.instToString = { toString := LO.IntProp.Formula.toStr }

source

@[simp]

theorem LO.IntProp.Formula.and_inj {α : Type u_1} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) :

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

source

@[simp]

theorem LO.IntProp.Formula.or_inj {α : Type u_1} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) :

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

source

@[simp]

theorem LO.IntProp.Formula.imp_inj {α : Type u_1} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) :

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

source

@[simp]

theorem LO.IntProp.Formula.neg_inj {α : Type u_1} (φ ψ : Formula α) :

∼φ = ∼ψ ↔ φ = ψ

source

theorem LO.IntProp.Formula.iff_def {α : Type u_1} (φ ψ : Formula α) :

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

source

def LO.IntProp.Formula.complexity {α : Type u_1} :

Formula α → ℕ

Equations

(LO.IntProp.Formula.atom a).complexity = 0
LO.IntProp.Formula.verum.complexity = 0
LO.IntProp.Formula.falsum.complexity = 0
φ.neg.complexity = φ.complexity + 1
(φ.imp ψ).complexity = φ.complexity ⊔ ψ.complexity + 1
(φ.and ψ).complexity = φ.complexity ⊔ ψ.complexity + 1
(φ.or ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

source

@[simp]

theorem LO.IntProp.Formula.complexity_bot {α : Type u_1} :

⊥.complexity = 0

source

@[simp]

theorem LO.IntProp.Formula.complexity_top {α : Type u_1} :

⊤.complexity = 0

source

@[simp]

theorem LO.IntProp.Formula.complexity_atom {α : Type u_1} (a : α) :

(atom a).complexity = 0

source

@[simp]

theorem LO.IntProp.Formula.complexity_imp {α : Type u_1} (φ ψ : Formula α) :

(φ ➝ ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

source

@[simp]

theorem LO.IntProp.Formula.complexity_imp' {α : Type u_1} (φ ψ : Formula α) :

(φ.imp ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

source

@[simp]

theorem LO.IntProp.Formula.complexity_and {α : Type u_1} (φ ψ : Formula α) :

(φ ⋏ ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

source

@[simp]

theorem LO.IntProp.Formula.complexity_and' {α : Type u_1} (φ ψ : Formula α) :

(φ.and ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

source

@[simp]

theorem LO.IntProp.Formula.complexity_or {α : Type u_1} (φ ψ : Formula α) :

(φ ⋎ ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

source

@[simp]

theorem LO.IntProp.Formula.complexity_or' {α : Type u_1} (φ ψ : Formula α) :

(φ.or ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

source

def LO.IntProp.Formula.cases' {α : Type u_1} {C : Formula α → Sort w} (hfalsum : C ⊥) (hverum : C ⊤) (hatom : (a : α) → C (atom a)) (hneg : (φ : Formula α) → C (∼φ)) (himp : (φ ψ : Formula α) → C (φ ➝ ψ)) (hand : (φ ψ : Formula α) → C (φ ⋏ ψ)) (hor : (φ ψ : Formula α) → C (φ ⋎ ψ)) (φ : Formula α) :

C φ

Equations

LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor LO.IntProp.Formula.falsum = hfalsum
LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor LO.IntProp.Formula.verum = hverum
LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor (LO.IntProp.Formula.atom a) = hatom a
LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor φ.neg = hneg φ
LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor (φ.imp ψ) = himp φ ψ
LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor (φ.and ψ) = hand φ ψ
LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor (φ.or ψ) = hor φ ψ

source

def LO.IntProp.Formula.rec' {α : Type u_1} {C : Formula α → Sort w} (hfalsum : C ⊥) (hverum : C ⊤) (hatom : (a : α) → C (atom a)) (hneg : (φ : Formula α) → C φ → C (∼φ)) (himp : (φ ψ : Formula α) → C φ → C ψ → C (φ ➝ ψ)) (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.IntProp.Formula.rec' hfalsum hverum hatom hneg himp hand hor LO.IntProp.Formula.falsum = hfalsum
LO.IntProp.Formula.rec' hfalsum hverum hatom hneg himp hand hor LO.IntProp.Formula.verum = hverum
LO.IntProp.Formula.rec' hfalsum hverum hatom hneg himp hand hor (LO.IntProp.Formula.atom a) = hatom a
LO.IntProp.Formula.rec' hfalsum hverum hatom hneg himp hand hor φ.neg = hneg φ (LO.IntProp.Formula.rec' hfalsum hverum hatom hneg himp hand hor φ)