[isabelle] New AFP entries: Abstract Rewriting and Matrices

There are two nicely modular new entries by Christian Sternagel and René
Thiemann from Innsbruck:

Abstract Rewriting

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.

Executable Matrix Operations on Matrices of Arbitrary Dimensions

We provide the operations of matrix addition, multiplication,
transposition, and matrix comparisons as executable functions over
ordered semirings. Moreover, it is proven that strongly normalizing
(monotone) orders can be lifted to strongly normalizing (monotone)
orders over matrices. We further show that the standard semirings over
the naturals, integers, and rationals, as well as the arctic semirings
satisfy the axioms that are required by our matrix theory. Our
formalization is part of the CeTA system which contains several
termination techniques. The provided theories have been essential to
formalize matrix-interpretations and arctic interpretations.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.