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

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

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?


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