Substitution of subtrees

UnorderedTree.replace target replacement t rebuilds t with every subtree equal to target replaced by replacement. It is computed on a planar representative by RoseTree.unorderedReplace, and is well-defined because that recursion computes the UnorderedTree.para testing each subtree before rebuilding it from its substituted children.

Main definitions

• UnorderedTree.replace, RoseTree.unorderedReplace

def RoseTree.unorderedReplace {α : Type u_1} [DecidableEq α] (target replacement : UnorderedTree α) : RoseTree α → UnorderedTree α

Substitution on a planar tree: replace every subtree equal, in the quotient, to target by replacement.

Equations

• One or more equations did not get rendered due to their size.

def RoseTree.unorderedReplaceList {α : Type u_1} [DecidableEq α] (target replacement : UnorderedTree α) : List (RoseTree α) → Multiset (UnorderedTree α)

Substitution in each child, collected as a multiset.

Equations

• RoseTree.unorderedReplaceList target replacement [] = 0
• RoseTree.unorderedReplaceList target replacement (c :: cs) = RoseTree.unorderedReplace target replacement c ::ₘ RoseTree.unorderedReplaceList target replacement cs

def UnorderedTree.replace {α : Type u_1} [DecidableEq α] (target replacement : UnorderedTree α) : UnorderedTree α → UnorderedTree α

Replace every subtree equal to target by replacement.

Equations

• target.replace replacement = Quotient.lift (RoseTree.unorderedReplace target replacement) ⋯

@[simp]

theorem UnorderedTree.replace_mk {α : Type u_1} [DecidableEq α] (target replacement : UnorderedTree α) (p : RoseTree α) : target.replace replacement (mk p) = RoseTree.unorderedReplace target replacement p

theorem UnorderedTree.replace_node {α : Type u_1} [DecidableEq α] (target replacement : UnorderedTree α) (a : α) (F : Multiset (UnorderedTree α)) : target.replace replacement (node a F) = if node a F = target then replacement else node a (Multiset.map (target.replace replacement) F)

theorem UnorderedTree.replace_leaf {α : Type u_1} [DecidableEq α] (target replacement : UnorderedTree α) (x : α) : target.replace replacement (leaf x) = if leaf x = target then replacement else leaf x

theorem UnorderedTree.replace_node_pair {α : Type u_1} [DecidableEq α] (target replacement : UnorderedTree α) (a : α) (l r : UnorderedTree α) : target.replace replacement (node a {l, r}) = if node a {l, r} = target then replacement else node a {target.replace replacement l, target.replace replacement r}

theorem UnorderedTree.replace_self {α : Type u_1} [DecidableEq α] (t r : UnorderedTree α) : t.replace r t = r

Replacing the whole tree yields the replacement.