Substitution in first-order terms

Mathlib's FirstOrder.Language.Term.subst replaces each variable of a term by a term. This file records its algebra: substituting variables for themselves is the identity, two substitutions compose to one, relabelling is the substitution of variables, and both relabelling and language maps commute with substitution. These are the term cases of the corresponding laws for substitution into formulas.

Main results

• FirstOrder.Language.Term.subst_var: substituting each variable by itself.
• FirstOrder.Language.Term.subst_subst: two substitutions compose to one.
• FirstOrder.Language.Term.relabel_eq_subst: relabelling is substitution of variables.
• FirstOrder.Language.Term.relabel_subst, FirstOrder.Language.Term.subst_relabel: relabelling after and before a substitution.
• FirstOrder.Language.LHom.onTerm_subst: language maps commute with substitution.

@[simp]

theorem FirstOrder.Language.Term.subst_var {L : Language} {α : Type uα} (t : L.Term α) : t.subst var = t

Substituting each variable by itself leaves a term unchanged.

@[simp]

theorem FirstOrder.Language.Term.subst_subst {L : Language} {α : Type uα} {β : Type uβ} {γ : Type uγ} (t : L.Term α) (f : α → L.Term β) (g : β → L.Term γ) : (t.subst f).subst g = t.subst fun (a : α) => (f a).subst g

Two successive substitutions are one substitution, by the substituted terms.

theorem FirstOrder.Language.Term.relabel_eq_subst {L : Language} {α : Type uα} {β : Type uβ} (t : L.Term α) (f : α → β) : relabel f t = t.subst (var ∘ f)

Relabelling the variables of a term is substituting variables for them.

@[simp]

theorem FirstOrder.Language.Term.relabel_subst {L : Language} {α : Type uα} {β : Type uβ} {γ : Type uγ} (t : L.Term α) (f : α → L.Term β) (g : β → γ) : relabel g (t.subst f) = t.subst fun (a : α) => relabel g (f a)

Relabelling after a substitution relabels the substituted terms.

@[simp]

theorem FirstOrder.Language.Term.subst_relabel {L : Language} {α : Type uα} {β : Type uβ} {γ : Type uγ} (t : L.Term α) (f : α → β) (g : β → L.Term γ) : (relabel f t).subst g = t.subst (g ∘ f)

Substitution after a relabelling is substitution along the composite.

@[simp]

theorem FirstOrder.Language.LHom.onTerm_subst {L : Language} {α : Type uα} {β : Type uβ} {L' : Language} (g : L →ᴸ L') (t : L.Term α) (f : α → L.Term β) : g.onTerm (t.subst f) = (g.onTerm t).subst fun (a : α) => g.onTerm (f a)

A language map commutes with substitution, acting on the substituted terms.