Pattern-based Subterm Selection in Isabelle

TL;DR

This paper introduces a pattern-based language for subterm selection in Isabelle, enabling concise, robust term manipulation and simplifying rewriting tactics by eliminating the need for occurrence numbers.

Contribution

It presents a novel pattern language for subterm selection and implements a single-step rewriting tactic in Isabelle, improving usability and robustness.

Findings

Simplifies subterm selection in Isabelle

Eliminates need for occurrence numbers in rewriting

Provides a modular semantics for pattern handling

Abstract

This article presents a pattern-based language designed to select (a set of) subterms of a given term in a concise and robust way. Building on this language, we implement a single-step rewriting tactic in the Isabelle theorem prover, which removes the need for obscure "occurrence numbers" for subterm selection. The language was inspired by the \emph{language of patterns} of Gonthier and Tassi, but provides an elegant way of handling bound variables and a modular semantics.