Pattern-based Subterm Selection in Isabelle
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 obsucure "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.
The Isabelle theories with our implementation are available here (updated 2014-07-14). They are intended to work with the Isabelle 2013-2 release.