def bigCon : List Formula → Formula

Equations

• bigCon [] = ⊤
• bigCon [f] = f
• bigCon (f :: rest) = f⋀bigCon rest

def bigDis : List Formula → Formula

Equations

• bigDis [] = ⊥
• bigDis [f] = f
• bigDis (f :: rest) = f⋁bigDis rest

theorem vocOfBigDis {x : Char} {l : List Formula} : x ∈ HasVocabulary.voc (bigDis l) → ∃ φ ∈ l, x ∈ HasVocabulary.voc φ

theorem vocOfBigCon {x : Char} {l : List Formula} : x ∈ HasVocabulary.voc (bigCon l) → ∃ φ ∈ l, x ∈ HasVocabulary.voc φ

@[simp]

theorem conempty : bigCon ∅ = ⊤

@[simp]

theorem consingle {f : Formula} : bigCon [f] = f

def dis : List Formula → Formula

Equations

• dis [] = ⊥
• dis [f] = f
• dis (f :: rest) = f⋁dis rest

@[simp]

theorem disempty : dis ∅ = ⊥

@[simp]

theorem dissingle {f : Formula} : dis [f] = f

def discon : List (List Formula) → Formula

Equations

• discon [] = ⊥
• discon [X] = bigCon X
• discon (X :: rest) = bigCon X⋁discon rest

@[simp]

theorem disconempty : discon {∅} = ⊤

@[simp]

theorem disconsingle {f : Formula} : discon [[f]] = f

theorem conEvalHT {X : List Formula} {f : Formula} {W : Type} {M : KripkeModel W} {w : W} : Evaluate (M, w) (bigCon (f :: X)) ↔ Evaluate (M, w) f ∧ Evaluate (M, w) (bigCon X)

theorem conEval {W : Type} {M : KripkeModel W} {X : List Formula} {w : W} : Evaluate (M, w) (bigCon X) ↔ ∀ f ∈ X, Evaluate (M, w) f

theorem disconEvalHT {X : List Formula} (XS : List (List Formula)) : discon (X :: XS)≡bigCon X⋁discon XS

theorem disconEval {W : Type} {M : KripkeModel W} {w : W} {N : ℕ} (XS : List (List Formula)) : XS.length = N → (Evaluate (M, w) (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f)

def pairunionList : List (List Formula) → List (List Formula) → List (List Formula)

Equations

• pairunionList x✝¹ x✝ = (List.map (fun (xl : List Formula) => List.map (fun (yl : List Formula) => xl ++ yl) x✝) x✝¹).flatten

def pairunionFinset : Finset (Finset Formula) → Finset (Finset Formula) → Finset (Finset Formula)

Equations

• pairunionFinset x✝¹ x✝ = x✝¹.biUnion fun (ga : Finset Formula) => x✝.biUnion fun (gb : Finset Formula) => {ga ∪ gb}

class HasUplus (α : Type → Type) : Type

• pairunion : α (α Formula) → α (α Formula) → α (α Formula)

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 listHasUplus : HasUplus List

Equations

• listHasUplus = { pairunion := pairunionList }

instance finsetHasUplus : HasUplus Finset

Equations

• finsetHasUplus = { pairunion := pairunionFinset }

theorem disconAnd {XS YS : List (List Formula)} : discon (XS⊎YS)≡discon XS⋀discon YS

theorem disconOr {XS YS : List (List Formula)} : discon (XS ∪ YS)≡discon XS⋁discon YS

theorem union_elem_uplus {XS YS : Finset (Finset Formula)} {X Y : Finset Formula} : X ∈ XS → Y ∈ YS → X ∪ Y ∈ XS⊎YS

@[simp]

theorem bigDis_sat {W : Type} {l : List Formula} {M : KripkeModel W} {w : W} : Evaluate (M, w) (bigDis l) ↔ ∃ φ ∈ l, Evaluate (M, w) φ

@[simp]

theorem bigCon_sat {W : Type} {l : List Formula} {M : KripkeModel W} {w : W} : Evaluate (M, w) (bigCon l) ↔ ∀ φ ∈ l, Evaluate (M, w) φ

theorem bigDis_union_sat_down {X : Finset Formula} {l : List Formula} : HasSat.Satisfiable (X ∪ {bigDis l}) → ∃ φ ∈ l, HasSat.Satisfiable (X ∪ {φ})

theorem bigCon_union_sat_down {X : Finset Formula} {l : List Formula} : HasSat.Satisfiable (X ∪ {bigCon l}) → ∀ φ ∈ l, HasSat.Satisfiable (X ∪ {φ})

theorem bigConNeg_union_sat_down {X : Finset Formula} {l : List Formula} : HasSat.Satisfiable (X ∪ {bigCon (List.map (fun (x : Formula) => ~x) l)}) → ∀ φ ∈ l, HasSat.Satisfiable (X ∪ {~φ})

theorem eval_neg_BigDis_iff_eval_bigConNeg {W : Type} {l : List Formula} {M : KripkeModel W} {w : W} : Evaluate (M, w) (~bigDis l) ↔ Evaluate (M, w) (~~bigCon (List.map (fun (x : Formula) => ~x) l))

theorem eval_negBigCon_iff_eval_bigDisNeg {W : Type} {l : List Formula} {M : KripkeModel W} {w : W} : Evaluate (M, w) (~bigCon l) ↔ Evaluate (M, w) (bigDis (List.map (fun (x : Formula) => ~x) l))

theorem sat_negBigDis_iff_sat_bigConNeg {l : List Formula} : HasSat.Satisfiable (~bigDis l) ↔ HasSat.Satisfiable (~~bigCon (List.map (fun (x : Formula) => ~x) l))

theorem sat_negBigCon_iff_sat_bigDisNeg {l : List Formula} : HasSat.Satisfiable (~bigCon l) ↔ HasSat.Satisfiable (bigDis (List.map (fun (x : Formula) => ~x) l))