[isabelle] Theory of finitely-branching, finite trees and tree contexts?
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