Pattern-based Subterm Selection in Isabelle

Abstract. This article presents a pattern-based language designed to se-lect (a set of) subterms of a given term in a concise and robust way. Build-ing 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 language of patterns of Gonthier and Tassi, but provides an elegant way of handling bound variables and a modular semantics.