Re: [isabelle] Theory of finitely-branching, finite trees and tree contexts?

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
where most likely, youâre mainly interested in the theory thys/Rewriting/Term.thy


> Am 01.12.2015 um 15:50 schrieb Tom Ridge via Cl-isabelle-users <cl-isabelle-users at>:
> Dear All,
> I am looking for a theory of trees that includes a notion of "subtree
> within a tree" (similar to a framestack presentation for an operational
> semantics).
> A "subtree within a tree" would be something like a triple: a path to a
> subtree, a tree with a hole where the subtree should be (the "tree
> context"), and a subtree that fits in the hole.
> A general theory (for non-finite, non-finitely-branching) would be
> reasonable, but my use case is only for finitely-branching, finite trees.
> Does anyone have any pointers to such a theory?
> Thanks

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