### 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.

### License

GNU Lesser General Public License (LGPL)

### History

October 16, 2013
  Generalized delta-orders from rationals to Archimedean fields.
September 17, 2010
  Added theories defining several (ordered) semirings related to strong normalization and giving some standard instances.

### Topics

- Logic/Rewriting

### Session Abstract-Rewriting

- Seq
- Abstract_Rewriting
- Relative_Rewriting
- SN_Orders
- SN_Order_Carrier

### Depends on

- Regular Sets and Expressions

### Used by

- Minsky Machines
- First-Order Terms
- The Z Property
- Polynomial Factorization
- Decreasing Diagrams II
- Decreasing Diagrams
- Well-Quasi-Orders
- The Myhill-Nerode Theorem Based on Regular Expressions
- Executable Multivariate Polynomials
- Executable Matrix Operations on Matrices of Arbitrary Dimensions

### Auto-related entries

- A Formalization of Knuth–Bendix Orders

## Cite

×

Abstract-Rewriting-AFP

    @article{Abstract-Rewriting-AFP,
      author  = {Christian Sternagel and René Thiemann},
      title   = {Abstract Rewriting},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2010},
      note    = {\url{https://isa-afp.org/entries/Abstract-Rewriting.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jun 30, 2010 : Isabelle2009-2
- Jun 17, 2010 : Isabelle2009-1