Email Gateway (Aug 22 2022 at 12:00): Email Gateway (Aug 22 2022 at 12:00):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Tom,
I don’t know whether it is suitable for your application, but there is a large formalization of term rewriting available, which contains terms: finitely branching, finite trees with labels at the intermediate nodes and at the leafs. They come in combination with several other operations like positions (paths to subtrees), contexts (trees containing one hole), etc.
The whole formalization is available at http://cl-informatik.uibk.ac.at/software/ceta/
where most likely, you’re mainly interested in the theory thys/Rewriting/Term.thy
(e.g., http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/v2.23/thys/Rewriting/Term.thy)
Cheers,
René
Last updated: Apr 19 2024 at 01:05 UTC