Proof Terms for Term Rewriting

Proof terms are first-order terms that represent reductions in term rewriting. They were initially introduced in TeReSe by van Oostrom and de Vrijer to study equivalences of reductions in left-linear rewrite systems. This entry formalizes proof terms for multi-steps in first-order term rewrite systems. We define simple proof terms (i.e., without a composition operator) and establish the correspondence to multi-steps: each proof term represents a multi-step with the same source and target, and every multi-step can be expressed as a proof term. The formalization moreover includes operations on proof terms, such as residuals, join, and deletion and a method for labeling proof term sources to identify overlaps between two proof terms.
This formalization is part of the Isabelle Formalization of Rewriting (IsaFoR) and is an essential component of several formalized confluence and commutation results involving multi-steps.