ofFun

def Trestle.Model.PropForm.ofBool {V : Type u_1} (b : Bool) : PropForm V

Equations

• Trestle.Model.PropForm.ofBool b = if b = true then Trestle.Model.PropForm.tr else Trestle.Model.PropForm.fls

@[simp]

theorem Trestle.Model.PropForm.eval_ofBool {ν✝ : Type u_1} {τ : PropAssignment ν✝} (b : Bool) : eval τ (ofBool b) = b

def Trestle.Model.PropForm.ofFun {V : Type u_1} [DecidableEq V] (p : PropAssignment V → Bool) (L : List V) (h : ∀ (v : V), v ∈ L) : PropForm V

Any function from assignments to Prop over a list of variables can be written as a PropForm, by truth table construction.

Equations

• Trestle.Model.PropForm.ofFun p L h = Trestle.Model.PropForm.ofFun.aux p L fun (v : V) (h_1 : v ∉ L) => ⋯.elim

def Trestle.Model.PropForm.ofFun.aux {V : Type u_1} [DecidableEq V] (p : PropAssignment V → Bool) (rem : List V) (passn : (v : V) → v ∉ rem → Bool) : PropForm V

Equations

• One or more equations did not get rendered due to their size.
• Trestle.Model.PropForm.ofFun.aux p [] passn_2 = Trestle.Model.PropForm.ofBool (p fun (v : V) => passn_2 v ⋯)

@[simp]

theorem Trestle.Model.PropForm.eval_ofFun {V : Type u_1} {p : PropAssignment V → Bool} {τ : PropAssignment V} [DecidableEq V] {L : List V} {hc : ∀ (v : V), v ∈ L} : eval τ (ofFun p L hc) = p τ

@[simp]

theorem Trestle.Model.PropForm.entails_ofFun {V : Type u_1} [DecidableEq V] {L : List V} {hc : ∀ (v : V), v ∈ L} (p : PropAssignment V → Bool) (τ : PropAssignment V) : τ ⊨ ofFun p L hc ↔ p τ = true

def Trestle.Model.PropFun.ofFun {V : Type u} [DecidableEq V] [Fintype V] (p : PropAssignment V → Bool) : PropFun V

Equations

• Trestle.Model.PropFun.ofFun p = Fintype.elim_elems (fun (L : List V) (h1 : ∀ (v : V), v ∈ L) (x : L.Nodup) => ⟦Trestle.Model.PropForm.ofFun p L h1⟧) ⋯

@[simp]

theorem Trestle.Model.PropFun.entails_ofFun {V : Type u_1} [DecidableEq V] [Fintype V] (p : PropAssignment V → Bool) (τ : PropAssignment V) : τ ⊨ ofFun p ↔ p τ = true

ofSet

def Trestle.Model.PropFun.ofSet {V : Type u} [DecidableEq V] [Fintype V] (S : Set (PropAssignment V)) [DecidablePred fun (x : PropAssignment V) => x ∈ S] : PropFun V

Equations

• Trestle.Model.PropFun.ofSet S = Trestle.Model.PropFun.ofFun fun (x : Trestle.Model.PropAssignment V) => decide (x ∈ S)

@[simp]

theorem Trestle.Model.PropFun.satisfies_ofSet {V : Type u_1} {τ : PropAssignment V} [DecidableEq V] [Fintype V] (S : Set (PropAssignment V)) [DecidablePred fun (x : PropAssignment V) => x ∈ S] : τ ⊨ ofSet S ↔ τ ∈ S