Rewriting Entailment #

term/formula morphisms such as Rewritings, substitutions, and embs are handled by the structure FFL.FirstOrder.Rew.

FFL.FirstOrder.Rew.rewrite f is a Rewriting of the free variables occurring in the term by f : ξ₁ → Semiterm L ξ₂ n.
FFL.FirstOrder.Rew.subst v is a substitution of the bounded variables occurring in the term by v : Fin n → Semiterm L ξ n'.
FFL.FirstOrder.Rew.bShift is a transformation of the bounded variables occurring in the term by #x ↦ #(Fin.succ x).
FFL.FirstOrder.Rew.shift is a transformation of the free variables occurring in the term by &x ↦ &(x + 1).
FFL.FirstOrder.Rew.emb is a emb of the term with no free variables.

Rewritings FFL.FirstOrder.Rew is naturally converted to formula Rewritings by FFL.FirstOrder.Rew.hom.

def FFL.FirstOrder.Semiformula.rewAux {L : Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} ⦃n₁ n₂ : ℕ⦄ (ω : Rew L ξ₁ n₁ ξ₂ n₂) :

Semiformula L ξ₁ n₁ → Semiformula L ξ₂ n₂

Equations

FFL.FirstOrder.Semiformula.rewAux ω FFL.FirstOrder.Semiformula.verum = ⊤
FFL.FirstOrder.Semiformula.rewAux ω FFL.FirstOrder.Semiformula.falsum = ⊥
FFL.FirstOrder.Semiformula.rewAux ω (FFL.FirstOrder.Semiformula.rel r v) = FFL.FirstOrder.Semiformula.rel r (⇑ω ∘ v)
FFL.FirstOrder.Semiformula.rewAux ω (FFL.FirstOrder.Semiformula.nrel r v) = FFL.FirstOrder.Semiformula.nrel r (⇑ω ∘ v)
FFL.FirstOrder.Semiformula.rewAux ω (φ.and ψ) = FFL.FirstOrder.Semiformula.rewAux ω φ ⋏ FFL.FirstOrder.Semiformula.rewAux ω ψ
FFL.FirstOrder.Semiformula.rewAux ω (φ.or ψ) = FFL.FirstOrder.Semiformula.rewAux ω φ ⋎ FFL.FirstOrder.Semiformula.rewAux ω ψ
FFL.FirstOrder.Semiformula.rewAux ω φ.all = ∀¹ FFL.FirstOrder.Semiformula.rewAux ω.q φ
FFL.FirstOrder.Semiformula.rewAux ω φ.exs = ∃¹ FFL.FirstOrder.Semiformula.rewAux ω.q φ

Instances For

source

theorem FFL.FirstOrder.Semiformula.rewAux_neg {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (φ : Semiformula L ξ₁ n₁) :

rewAux ω (∼φ) = ∼rewAux ω φ

source

theorem FFL.FirstOrder.Semiformula.ext_rewAux' {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂} (h : ω₁ = ω₂) (φ : Semiformula L ξ₁ n₁) :

rewAux ω₁ φ = rewAux ω₂ φ

source

def FFL.FirstOrder.Semiformula.rew {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) :

Semiformula L ξ₁ n₁ →ˡᶜ Semiformula L ξ₂ n₂

Equations

FFL.FirstOrder.Semiformula.rew ω = { toTr := FFL.FirstOrder.Semiformula.rewAux ω, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

Instances For

source

@[instance_reducible]

instance FFL.FirstOrder.Semiformula.instRewriting {L : Language} {ξ : Type u_2} {ζ : Type u_3} :

Rewriting L ξ (Semiformula L ξ) ζ (Semiformula L ζ)

Equations

FFL.FirstOrder.Semiformula.instRewriting = { app := fun {n₁ n₂ : ℕ} => FFL.FirstOrder.Semiformula.rew, app_all := ⋯, app_exs := ⋯ }

source

@[reducible, inline]

abbrev FFL.FirstOrder.Semiformula.subst {L : Language} {ξ : Type u_2} {n m : ℕ} (φ : Semiformula L ξ n) (v : Fin n → Semiterm L ξ m) :

Semiformula L ξ m

Equations

φ.subst v = φ ⇜ v

Instances For

source

@[reducible, inline]

abbrev FFL.FirstOrder.Semiformula.emb {o : Type u_1} {L : Language} {n : ℕ} {ξ : Type u_3} [IsEmpty o] (φ : Semiformula L o n) :

Semiformula L ξ n

Equations

↑φ = FFL.FirstOrder.Rewriting.emb φ

Instances For

source

@[reducible, inline]

abbrev FFL.FirstOrder.Semiformula.free {L : Language} {n : ℕ} (φ : Semiproposition L (n + 1)) :

Semiproposition L n

Equations

FFL.FirstOrder.Semiformula.free φ = FFL.FirstOrder.Rewriting.free φ

Instances For

source

@[reducible, inline]

abbrev FFL.FirstOrder.Semiformula.shift {L : Language} {n : ℕ} (φ : Semiproposition L n) :

Semiproposition L n

Equations

FFL.FirstOrder.Semiformula.shift φ = FFL.FirstOrder.Rewriting.shift φ

Instances For

source

theorem FFL.FirstOrder.Semiformula.rew_rel {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ₁ n₁) :

(Rewriting.app ω) (rel r v) = rel r fun (i : Fin k) => ω (v i)

source

theorem FFL.FirstOrder.Semiformula.rew_nrel {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ₁ n₁) :

(Rewriting.app ω) (nrel r v) = nrel r fun (i : Fin k) => ω (v i)

source

@[simp]

theorem FFL.FirstOrder.Semiformula.rew_rel_eq_comp {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (rel r v) = rel r (⇑ω ∘ v)

source

@[simp]

theorem FFL.FirstOrder.Semiformula.rew_nrel_eq_comp {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (nrel r v) = nrel r (⇑ω ∘ v)

source

@[simp]

theorem FFL.FirstOrder.Semiformula.rew_rel0 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 0} {v : Fin 0 → Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (rel r v) = rel r ![]

source

@[simp]

theorem FFL.FirstOrder.Semiformula.rew_rel1 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 1} {t : Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (rel r ![t]) = rel r ![ω t]

source

@[simp]

theorem FFL.FirstOrder.Semiformula.rew_rel2 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 2} {t₁ t₂ : Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (rel r ![t₁, t₂]) = rel r ![ω t₁, ω t₂]

source

@[simp]

theorem FFL.FirstOrder.Semiformula.rew_rel3 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 3} {t₁ t₂ t₃ : Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (rel r ![t₁, t₂, t₃]) = rel r ![ω t₁, ω t₂, ω t₃]

source

@[simp]

theorem FFL.FirstOrder.Semiformula.rew_nrel0 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 0} {v : Fin 0 → Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (nrel r v) = nrel r ![]

source

@[simp]

theorem FFL.FirstOrder.Semiformula.rew_nrel1 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 1} {t : Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (nrel r ![t]) = nrel r ![ω t]

source

@[simp]

theorem FFL.FirstOrder.Semiformula.rew_nrel2 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 2} {t₁ t₂ : Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (nrel r ![t₁, t₂]) = nrel r ![ω t₁, ω t₂]

source

@[simp]

theorem FFL.FirstOrder.Semiformula.rew_nrel3 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 3} {t₁ t₂ t₃ : Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (nrel r ![t₁, t₂, t₃]) = nrel r ![ω t₁, ω t₂, ω t₃]

source

instance FFL.FirstOrder.Semiformula.instReflectiveRewriting {L : Language} {ξ : Type u_2} :

ReflectiveRewriting L ξ (Semiformula L ξ)

source

instance FFL.FirstOrder.Semiformula.instTransitiveRewriting {L : Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {ξ₃ : Type u_4} :

TransitiveRewriting L ξ₁ (Semiformula L ξ₁) ξ₂ (Semiformula L ξ₂) ξ₃ (Semiformula L ξ₃)

source

instance FFL.FirstOrder.Semiformula.instInjMapRewriting {L : Language} {ξ : Type u_2} {ζ : Type u_3} :

InjMapRewriting L ξ (Semiformula L ξ) ζ (Semiformula L ζ)

source

instance FFL.FirstOrder.Semiformula.instLawfulSyntacticRewritingSemiproposition {L : Language} :

LawfulSyntacticRewriting L (Semiproposition L)

source

@[simp]

theorem FFL.FirstOrder.Semiformula.complexity_rew {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (φ : Semiformula L ξ₁ n₁) :

((Rewriting.app ω) φ).complexity = φ.complexity

source

@[simp]

theorem FFL.FirstOrder.Semiformula.eq_top_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} :

(Rewriting.app ω) φ = ⊤ ↔ φ = ⊤

source

@[simp]

theorem FFL.FirstOrder.Semiformula.eq_bot_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} :

(Rewriting.app ω) φ = ⊥ ↔ φ = ⊥

source

theorem FFL.FirstOrder.Semiformula.eq_rel_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ξ₂ n₂} :

(Rewriting.app ω) φ = rel r v ↔ ∃ (v' : Fin k → Semiterm L ξ₁ n₁), ⇑ω ∘ v' = v ∧ φ = rel r v'

source

theorem FFL.FirstOrder.Semiformula.eq_nrel_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ξ₂ n₂} :

(Rewriting.app ω) φ = nrel r v ↔ ∃ (v' : Fin k → Semiterm L ξ₁ n₁), ⇑ω ∘ v' = v ∧ φ = nrel r v'

source

@[simp]

theorem FFL.FirstOrder.Semiformula.eq_and_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ n₂} :

(Rewriting.app ω) φ = ψ₁ ⋏ ψ₂ ↔ ∃ (φ₁ : Semiformula L ξ₁ n₁) (φ₂ : Semiformula L ξ₁ n₁), (Rewriting.app ω) φ₁ = ψ₁ ∧ (Rewriting.app ω) φ₂ = ψ₂ ∧ φ = φ₁ ⋏ φ₂

source

@[simp]

theorem FFL.FirstOrder.Semiformula.eq_or_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ n₂} :

(Rewriting.app ω) φ = ψ₁ ⋎ ψ₂ ↔ ∃ (φ₁ : Semiformula L ξ₁ n₁) (φ₂ : Semiformula L ξ₁ n₁), (Rewriting.app ω) φ₁ = ψ₁ ∧ (Rewriting.app ω) φ₂ = ψ₂ ∧ φ = φ₁ ⋎ φ₂

source

theorem FFL.FirstOrder.Semiformula.eq_all_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ : Semiformula L ξ₂ (n₂ + 1)} :

(Rewriting.app ω) φ = ∀¹ ψ ↔ ∃ (φ' : Semiformula L ξ₁ (n₁ + 1)), (Rewriting.app ω.q) φ' = ψ ∧ φ = ∀¹ φ'

source

theorem FFL.FirstOrder.Semiformula.eq_exs_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ : Semiformula L ξ₂ (n₂ + 1)} :

(Rewriting.app ω) φ = ∃¹ ψ ↔ ∃ (φ' : Semiformula L ξ₁ (n₁ + 1)), (Rewriting.app ω.q) φ' = ψ ∧ φ = ∃¹ φ'

source

@[simp]

theorem FFL.FirstOrder.Semiformula.eq_neg_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ n₂} :

(Rewriting.app ω) φ = ψ₁ 🡒 ψ₂ ↔ ∃ (φ₁ : Semiformula L ξ₁ n₁) (φ₂ : Semiformula L ξ₁ n₁), (Rewriting.app ω) φ₁ = ψ₁ ∧ (Rewriting.app ω) φ₂ = ψ₂ ∧ φ = φ₁ 🡒 φ₂

source

theorem FFL.FirstOrder.Semiformula.eq_ball_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ (n₂ + 1)} :

((Rewriting.app ω) φ = ∀¹[ψ₁] ψ₂) ↔ ∃ (φ₁ : Semiformula L ξ₁ (n₁ + 1)) (φ₂ : Semiformula L ξ₁ (n₁ + 1)), (Rewriting.app ω.q) φ₁ = ψ₁ ∧ (Rewriting.app ω.q) φ₂ = ψ₂ ∧ φ = ∀¹[φ₁] φ₂

source

theorem FFL.FirstOrder.Semiformula.eq_bexs_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ (n₂ + 1)} :

((Rewriting.app ω) φ = ∃¹[ψ₁] ψ₂) ↔ ∃ (φ₁ : Semiformula L ξ₁ (n₁ + 1)) (φ₂ : Semiformula L ξ₁ (n₁ + 1)), (Rewriting.app ω.q) φ₁ = ψ₁ ∧ (Rewriting.app ω.q) φ₂ = ψ₂ ∧ φ = ∃¹[φ₁] φ₂

source

@[instance_reducible]

instance FFL.FirstOrder.Semiformula.instCoeSemisentenceSemiproposition {L : Language} {n : ℕ} :

Coe (Semisentence L n) (Semiproposition L n)

Equations

FFL.FirstOrder.Semiformula.instCoeSemisentenceSemiproposition = { coe := ⇑FFL.FirstOrder.Rewriting.emb }

source

@[simp]

theorem FFL.FirstOrder.Semiformula.coe_inj {L : Language} {n : ℕ} (σ π : Semisentence L n) :

Rewriting.emb σ = Rewriting.emb π ↔ σ = π

source

theorem FFL.FirstOrder.Semiformula.coe_rel {ο : Type u_1} {L : Language} {n : ℕ} {ξ : Type u_3} [IsEmpty ο] {k : ℕ} (R : L.Rel k) (v : Fin k → Semiterm L ο n) :

Rewriting.emb (rel R v) = rel R fun (i : Fin k) => Rew.emb (v i)

source

theorem FFL.FirstOrder.Semiformula.coe_nrel {ο : Type u_1} {L : Language} {n : ℕ} {ξ : Type u_3} [IsEmpty ο] {k : ℕ} (R : L.Rel k) (v : Fin k → Semiterm L ο n) :

Rewriting.emb (nrel R v) = nrel R fun (i : Fin k) => Rew.emb (v i)

source

theorem FFL.FirstOrder.Semiformula.coe_subst_eq_subst_coe {L : Language} {k n : ℕ} (φ : Semisentence L k) (v : Fin k → ClosedSemiterm L n) :

Rewriting.emb (φ ⇜ v) = Rewriting.emb φ ⇜ fun (i : Fin k) => Rew.emb (v i)

source

theorem FFL.FirstOrder.Semiformula.coe_subst_eq_subst_coe₁ {L : Language} {n : ℕ} (φ : Semisentence L 1) (t : ClosedSemiterm L n) :

Rewriting.emb (φ/[t]) = (Rewriting.emb φ)/[Rew.emb t]

source

@[irreducible]

def FFL.FirstOrder.Semiformula.formulaRec {L : Language} {C : Proposition L → Sort u_2} (verum : C ⊤) (falsum : C ⊥) (rel : {l : ℕ} → (r : L.Rel l) → (v : Fin l → SyntacticTerm L) → C (rel r v)) (nrel : {l : ℕ} → (r : L.Rel l) → (v : Fin l → SyntacticTerm L) → C (nrel r v)) (and : (φ ψ : Proposition L) → C φ → C ψ → C (φ ⋏ ψ)) (or : (φ ψ : Proposition L) → C φ → C ψ → C (φ ⋎ ψ)) (all : (φ : Semiproposition L 1) → C (Rewriting.free φ) → C (∀¹ φ)) (ex : (φ : Semiproposition L 1) → C (Rewriting.free φ) → C (∃¹ φ)) (φ : Proposition L) :

C φ

Equations

One or more equations did not get rendered due to their size.
FFL.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex FFL.FirstOrder.Semiformula.verum = verum
FFL.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex FFL.FirstOrder.Semiformula.falsum = falsum
FFL.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex (FFL.FirstOrder.Semiformula.rel r v) = rel r v
FFL.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex (FFL.FirstOrder.Semiformula.nrel r v) = nrel r v

Instances For

source

theorem FFL.FirstOrder.Semiformula.fvar?_rew {ξ₁ : Type u_1} {ξ₂ : Type u_2} {L : Language} {n₁ n₂ : ℕ} [DecidableEq ξ₁] [DecidableEq ξ₂] {φ : Semiformula L ξ₁ n₁} {ω : Rew L ξ₁ n₁ ξ₂ n₂} {x : ξ₂} (h : ((Rewriting.app ω) φ).FVar? x) :

(∃ (i : Fin n₁), (ω (Semiterm.bvar i)).FVar? x) ∨ ∃ (z : ξ₁), φ.FVar? z ∧ (ω (Semiterm.fvar z)).FVar? x

source

@[simp]

theorem FFL.FirstOrder.Semiformula.freeVariables_emb {ξ : Type u_2} {L : Language} {n : ℕ} [DecidableEq ξ] {ο : Type u_1} [IsEmpty ο] (φ : Semiformula L ο n) :

(Rewriting.emb φ).freeVariables = ∅

source

theorem FFL.FirstOrder.Semiformula.rew_eq_of_funEqOn {ξ₁ : Type u_1} {L : Language} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} [DecidableEq ξ₁] {ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂} {φ : Semiformula L ξ₁ n₁} (hb : ∀ (x : Fin n₁), ω₁ (Semiterm.bvar x) = ω₂ (Semiterm.bvar x)) (hf : Function.funEqOn φ.FVar? (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)) :

(Rewriting.app ω₁) φ = (Rewriting.app ω₂) φ

source

theorem FFL.FirstOrder.Semiformula.rew_eq_of_funEqOn₀ {ξ₁ : Type u_1} {L : Language} {ξ₂ : Type u_3} {n₂ : ℕ} [DecidableEq ξ₁] {ω₁ ω₂ : Rew L ξ₁ 0 ξ₂ n₂} {φ : Semiformula L ξ₁ 0} (hf : Function.funEqOn φ.FVar? (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)) :

(Rewriting.app ω₁) φ = (Rewriting.app ω₂) φ

source

theorem FFL.FirstOrder.Semiformula.rew_eq_self_of {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] {ω : Rew L ξ n ξ n} {φ : Semiformula L ξ n} (hb : ∀ (x : Fin n), ω (Semiterm.bvar x) = Semiterm.bvar x) (hf : ∀ (x : ξ), φ.FVar? x → ω (Semiterm.fvar x) = Semiterm.fvar x) :

(Rewriting.app ω) φ = φ

source

@[simp]

theorem FFL.FirstOrder.Semiformula.ex_ne_subst {L : Language} {ξ : Type u_2} (φ : Semiformula L ξ 1) (t : Semiterm L ξ 0) :

φ/[t] ≠ ∃¹ φ

source

@[simp]

theorem FFL.FirstOrder.Semiformula.fvSup_sentence {L : Language} {n : ℕ} (σ : Semisentence L n) :

(Rewriting.emb σ).fvSup = 0

source

@[simp]

theorem FFL.FirstOrder.Semiformula.subst_comp_fixitr_eq_map {L : Language} (φ : Proposition L) (f : ℕ → SyntacticTerm L) :

((Rewriting.app (Rew.fixitr 0 (fvSup φ))) φ ⇜ fun (x : Fin (0 + fvSup φ)) => f ↑x) = (Rewriting.app (Rew.rewrite f)) φ

source

@[simp]

theorem FFL.FirstOrder.Semiformula.subst_comp_fixitr {L : Language} (φ : Proposition L) :

((Rewriting.app (Rew.fixitr 0 (fvSup φ))) φ ⇜ fun (x : Fin (0 + fvSup φ)) => Semiterm.fvar ↑x) = φ

source

def FFL.FirstOrder.Semiformula.univCl' {L : Language} (φ : Proposition L) :

Proposition L

Equations

FFL.FirstOrder.Semiformula.univCl' φ = ∀¹* (FFL.FirstOrder.Rewriting.app (FFL.FirstOrder.Rew.fixitr 0 (FFL.FirstOrder.Semiformula.fvSup φ))) φ

Instances For

source

@[simp]

theorem FFL.FirstOrder.Semiformula.rew_univCl' {L : Language} (φ : Proposition L) (ω : SyntacticRew L 0 0) :

(Rewriting.app ω) (univCl' φ) = univCl' φ

source

theorem FFL.FirstOrder.Semiformula.univCl'_eq_self_of {L : Language} (φ : Proposition L) (h : freeVariables φ = ∅) :

univCl' φ = φ

source

@[simp]

theorem FFL.FirstOrder.Semiformula.senetnce_univCl'_eq_self {L : Language} (σ : Sentence L) :

univCl' (Rewriting.emb σ) = Rewriting.emb σ

source

@[simp]

theorem FFL.FirstOrder.Semiformula.fvarList_univCl' {L : Language} (φ : Proposition L) :

freeVariables (univCl' φ) = ∅

source

@[simp]

theorem FFL.FirstOrder.Semiformula.univCl'_univCl'_eq_univCl' {L : Language} (φ : Proposition L) :

univCl' (univCl' φ) = univCl' φ

source

def FFL.FirstOrder.Semiformula.toEmpty {ξ : Type u_1} {L : Language} [DecidableEq ξ] {n : ℕ} (φ : Semiformula L ξ n) :

φ.freeVariables = ∅ → Semisentence L n

Equations

(FFL.FirstOrder.Semiformula.rel R v).toEmpty h = FFL.FirstOrder.Semiformula.rel R fun (i : Fin arity) => (v i).toEmpty ⋯
(FFL.FirstOrder.Semiformula.nrel R v).toEmpty h = FFL.FirstOrder.Semiformula.nrel R fun (i : Fin arity) => (v i).toEmpty ⋯
FFL.FirstOrder.Semiformula.verum.toEmpty x_2 = ⊤
FFL.FirstOrder.Semiformula.falsum.toEmpty x_2 = ⊥
(φ.and ψ).toEmpty h = φ.toEmpty ⋯ ⋏ ψ.toEmpty ⋯
(φ.or ψ).toEmpty h = φ.toEmpty ⋯ ⋎ ψ.toEmpty ⋯
φ.all.toEmpty h = ∀¹ φ.toEmpty h
φ.exs.toEmpty h = ∃¹ φ.toEmpty h

Instances For

source

@[simp]

theorem FFL.FirstOrder.Semiformula.emb_toEmpty {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ n) (hp : φ.freeVariables = ∅) :

Rewriting.emb (φ.toEmpty hp) = φ

source

@[simp]

theorem FFL.FirstOrder.Semiformula.toEmpty_emb {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ : Semisentence L n) :

(Rewriting.emb φ).toEmpty ⋯ = φ

source

@[simp]

theorem FFL.FirstOrder.Semiformula.toEmpty_verum {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] :

⊤.toEmpty ⋯ = ⊤

source

@[simp]

theorem FFL.FirstOrder.Semiformula.toEmpty_falsum {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] :

⊥.toEmpty ⋯ = ⊥

source

@[simp]

theorem FFL.FirstOrder.Semiformula.toEmpty_and {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ ψ : Semiformula L ξ n) (h : (φ ⋏ ψ).freeVariables = ∅) :

(φ ⋏ ψ).toEmpty h = φ.toEmpty ⋯ ⋏ ψ.toEmpty ⋯

source

@[simp]

theorem FFL.FirstOrder.Semiformula.toEmpty_or {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ ψ : Semiformula L ξ n) (h : (φ ⋎ ψ).freeVariables = ∅) :

(φ ⋎ ψ).toEmpty h = φ.toEmpty ⋯ ⋎ ψ.toEmpty ⋯

source

@[simp]

theorem FFL.FirstOrder.Semiformula.toEmpty_all {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ (n + 1)) (h : (∀¹ φ).freeVariables = ∅) :

(∀¹ φ).toEmpty h = ∀¹ φ.toEmpty h

source

@[simp]

theorem FFL.FirstOrder.Semiformula.toEmpty_ex {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ (n + 1)) (h : (∃¹ φ).freeVariables = ∅) :

(∃¹ φ).toEmpty h = ∃¹ φ.toEmpty h

source

def FFL.FirstOrder.Semiformula.univCl {L : Language} (φ : Proposition L) :

Sentence L

An universal closure of formula

Equations

FFL.FirstOrder.Semiformula.univCl φ = FFL.FirstOrder.Semiformula.toEmpty (FFL.FirstOrder.Semiformula.univCl' φ) ⋯

Instances For

source

@[simp]

theorem FFL.FirstOrder.Semiformula.coe_univCl_eq_univCl' {L : Language} (φ : Proposition L) :

Rewriting.emb (univCl φ) = univCl' φ

source

@[simp]

theorem FFL.FirstOrder.Semiformula.univCl_coe_sentence {L : Language} (σ : Sentence L) :

univCl (Rewriting.emb σ) = σ

source

def FFL.FirstOrder.Semiformula.toEmpty' {ξ : Type u_1} {L : Language} [DecidableEq ξ] {n : ℕ} (φ : Semiformula L ξ n) :

Semisentence L n

Equations

φ.toEmpty' = if h : φ.freeVariables = ∅ then φ.toEmpty h else ⊥

Instances For

source

@[simp]

theorem FFL.FirstOrder.Semiformula.toEmpty'_coe {ξ : Type u_1} {L : Language} [DecidableEq ξ] {n : ℕ} {φ : Semisentence L n} :

(Rewriting.emb φ).toEmpty' = φ

source

theorem FFL.FirstOrder.Semiformula.lMap_bind {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {ξ₁ : Type u_3} (b : Fin n₁ → Semiterm L₁ ξ₂ n₂) (e : ξ₁ → Semiterm L₁ ξ₂ n₂) (φ : Semiformula L₁ ξ₁ n₁) :

(lMap Φ) ((Rewriting.app (Rew.bind b e)) φ) = (Rewriting.app (Rew.bind (Semiterm.lMap Φ ∘ b) (Semiterm.lMap Φ ∘ e))) ((lMap Φ) φ)

source

theorem FFL.FirstOrder.Semiformula.lMap_map {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n₁ n₂ : ℕ} {ξ₁ : Type u_2} {ξ₂ : Type u_3} (b : Fin n₁ → Fin n₂) (e : ξ₁ → ξ₂) (φ : Semiformula L₁ ξ₁ n₁) :

(lMap Φ) ((Rewriting.app (Rew.map b e)) φ) = (Rewriting.app (Rew.map b e)) ((lMap Φ) φ)

source

theorem FFL.FirstOrder.Semiformula.lMap_rewrite {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n : ℕ} (f : ξ₁ → Semiterm L₁ ξ₂ n) (φ : Semiformula L₁ ξ₁ n) :

(lMap Φ) ((Rewriting.app (Rew.rewrite f)) φ) = (Rewriting.app (Rew.rewrite (Semiterm.lMap Φ ∘ f))) ((lMap Φ) φ)

source

theorem FFL.FirstOrder.Semiformula.lMap_subst {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {Φ : L₁.Hom L₂} {k n : ℕ} (w : Fin k → Semiterm L₁ ξ n) (φ : Semiformula L₁ ξ k) :

(lMap Φ) (φ ⇜ w) = (lMap Φ) φ ⇜ (Semiterm.lMap Φ ∘ w)

source

theorem FFL.FirstOrder.Semiformula.lMap_shift {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n : ℕ} (φ : Semiproposition L₁ n) :

(lMap Φ) ((Rewriting.app Rew.shift) φ) = (Rewriting.app Rew.shift) ((lMap Φ) φ)

source

theorem FFL.FirstOrder.Semiformula.lMap_free {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n : ℕ} (φ : Semiproposition L₁ (n + 1)) :

(lMap Φ) ((Rewriting.app Rew.free) φ) = (Rewriting.app Rew.free) ((lMap Φ) φ)

source

theorem FFL.FirstOrder.Semiformula.lMap_fix {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n : ℕ} (φ : Semiproposition L₁ n) :

(lMap Φ) ((Rewriting.app Rew.fix) φ) = (Rewriting.app Rew.fix) ((lMap Φ) φ)

source

theorem FFL.FirstOrder.Semiformula.lMap_emb {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {Φ : L₁.Hom L₂} {n : ℕ} {ο : Type u_2} [IsEmpty ο] (φ : Semiformula L₁ ο n) :

(lMap Φ) (Rewriting.emb φ) = Rewriting.emb ((lMap Φ) φ)

source

theorem FFL.FirstOrder.Semiformula.lMap_rewriteMap {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {ξ₁ : Type u_2} {n : ℕ} {ξ₂ : Type u_3} (φ : Semiformula L₁ ξ₁ n) (f : ξ₁ → ξ₂) :

(lMap Φ) ((Rewriting.app (Rew.rewriteMap f)) φ) = (Rewriting.app (Rew.rewriteMap f)) ((lMap Φ) φ)

source

@[simp]

theorem FFL.FirstOrder.Semiformula.rew_open_iff {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} {ω : Rew L ξ₁ n₁ ξ₂ n₂} {φ : Semiformula L ξ₁ n₁} :

((Rewriting.app ω) φ).Open ↔ φ.Open

Documentation

Foundation.FirstOrder.Syntax.Classical.Rew

Rewriting Entailment #