Abstract

We present an Isabelle formalization of abstract rewriting (see, e.g., the
book by Baader and Nipkow). First, we define standard relations like
joinability, meetability, conversion, etc. Then, we formalize important
properties of abstract rewrite systems, e.g., confluence and strong
normalization. Our main concern is on strong normalization, since this
formalization is the basis of CeTA (which is mainly about strong
normalization of term rewrite systems). Hence lemmas involving strong
normalization constitute by far the biggest part of this theory. One of
those is Newman’s lemma.

BibTeX

@incollection{CSRT-AFP10a,
  author      = "Christian Sternagel and Ren{\'e} Thiemann",
  title       = "{A}bstract {R}ewriting}",
  booktitle   = "The Archive of Formal Proofs",
  editor      = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher   = "\url{http://afp.sf.net/entries/Abstract-Rewriting.shtml}",
  year        = 2010,
  month       = Jun,
  note        = "Formal proof development"
  ISSN        = "2150-914x", 
}