Abstract Substitution

Martin Desharnais 📧

September 16, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This entry provides a small, reusable, theory that specifies the abstract concept of substition as monoid action. Both the substitution type and the object type are kept abstract. The theory provides multiple useful definitions and lemmas. Two example usages are provided for first order terms: one for terms from the AFP/First_Order_Terms session and one for terms from the Isabelle/HOL-ex session.

License

BSD License

Topics

Session Abstract_Substitution

Depends on

Used by

Cite

× 
@article{Abstract_Substitution-AFP,
  author  = {Martin Desharnais},
  title   = {Abstract Substitution},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Abstract_Substitution.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest