inductive Formula : Type

• bottom : Formula
• atom_prop : Char → Formula
• neg : Formula → Formula
• And : Formula → Formula → Formula
• box : Formula → Formula

instance instDecidableEqFormula : DecidableEq Formula

Equations

• instDecidableEqFormula = decEqFormula✝

def p : Formula

Equations

• p = ·'p'

def q : Formula

Equations

• q = ·'q'

def r : Formula

Equations

• r = ·'r'

def «term·_» : Lean.ParserDescr

Equations

• «term·_» = Lean.ParserDescr.node `«term·_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "·") (Lean.ParserDescr.cat `term 0))

def «term~_» : Lean.ParserDescr

Equations

• «term~_» = Lean.ParserDescr.node `«term~_» 88 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 88))

def «term□_» : Lean.ParserDescr

Equations

• «term□_» = Lean.ParserDescr.node `«term□_» 77 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□") (Lean.ParserDescr.cat `term 77))

def «term_⋀_» : Lean.TrailingParserDescr

Equations

• «term_⋀_» = Lean.ParserDescr.trailingNode `«term_⋀_» 66 67 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋀") (Lean.ParserDescr.cat `term 66))

def Formula.or : Formula → Formula → Formula

Equations

• x✝¹⋁x✝ = ~(~x✝¹⋀~x✝)

def «term_⋁_» : Lean.TrailingParserDescr

Equations

• «term_⋁_» = Lean.ParserDescr.trailingNode `«term_⋁_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋁") (Lean.ParserDescr.cat `term 60))

def impl (φ ψ : Formula) : Formula

Equations

• φ↣ψ = ~(φ⋀~ψ)

def «term_↣_» : Lean.TrailingParserDescr

Equations

• «term_↣_» = Lean.ParserDescr.trailingNode `«term_↣_» 55 56 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↣") (Lean.ParserDescr.cat `term 55))

def «term_⟷_» : Lean.TrailingParserDescr

Equations

• «term_⟷_» = Lean.ParserDescr.trailingNode `«term_⟷_» 77 77 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⟷") (Lean.ParserDescr.cat `term 78))

instance instBotFormula : Bot Formula

Equations

• instBotFormula = { bot := Formula.bottom }

instance instTopFormula : Top Formula

Equations

• instTopFormula = { top := ~Formula.bottom }

def BigConjunction : List Formula → Formula

Equations

• BigConjunction = List.foldl Formula.And (~Formula.bottom)

def BigDisjunction : List Formula → Formula

Equations

• BigDisjunction = List.foldl (fun (ϕ ψ : Formula) => ~(~ϕ⋀~ψ)) Formula.bottom

def formToString : Formula → ℕ → Std.Format

Equations

• formToString Formula.bottom x✝ = Std.Format.text "⊥"
• formToString (·c) x✝ = Std.Format.text "·" ++ repr c
• formToString (~ϕ) x✝ = Std.Format.text "~" ++ formToString ϕ x✝
• formToString (ϕ⋀ψ) x✝ = Std.Format.text "(" ++ formToString ϕ x✝ ++ Std.Format.text " ⋀ " ++ formToString ψ x✝ ++ Std.Format.text ")"
• formToString (□ϕ) x✝ = Std.Format.text "(□ " ++ formToString ϕ x✝ ++ Std.Format.text ")"

instance instReprFormula : Repr Formula

Equations

• instReprFormula = { reprPrec := formToString }

def lengthOfFormula : Formula → ℕ

Equations

• lengthOfFormula Formula.bottom = 1
• lengthOfFormula (·a) = 1
• lengthOfFormula (~φ) = 1 + lengthOfFormula φ
• lengthOfFormula (φ⋀ψ) = 1 + lengthOfFormula φ + lengthOfFormula ψ
• lengthOfFormula (□φ) = 1 + lengthOfFormula φ

def lengthOfSet : Finset Formula → ℕ

Equations

• lengthOfSet x✝ = x✝.sum lengthOfFormula

class HasLength (α : Type) : Type

• lengthOf : α → ℕ

instance formulaHasLength : HasLength Formula

Equations

• formulaHasLength = { lengthOf := lengthOfFormula }

instance setFormulaHasLength : HasLength (Finset Formula)

Equations

• setFormulaHasLength = { lengthOf := lengthOfSet }

def complexityOfFormula : Formula → ℕ

Equations

• complexityOfFormula Formula.bottom = 1
• complexityOfFormula (·a) = 1
• complexityOfFormula (~φ) = 1 + complexityOfFormula φ
• complexityOfFormula (φ⋀ψ) = 1 + complexityOfFormula φ ⊔ complexityOfFormula ψ
• complexityOfFormula (□φ) = 1 + complexityOfFormula φ

def complexityOfSet : Finset Formula → ℕ

Equations

• complexityOfSet x✝ = x✝.sum complexityOfFormula

class HasComplexity (α : Type) : Type

• complexityOf : α → ℕ

instance formulaHasComplexity : HasComplexity Formula

Equations

• formulaHasComplexity = { complexityOf := complexityOfFormula }

instance setFormulaHasComplexity : HasComplexity (Finset Formula)

Equations

• setFormulaHasComplexity = { complexityOf := complexityOfSet }