Substitution of subtrees

UnorderedTree.replace target replacement t rebuilds t with every subtree equal to target replaced by replacement. It is defined on planar representatives, where the equality test is taken in the quotient, and descends because both the test and the rebuilt children multiset are invariant under permutation of children. It is noncomputable since it rebuilds through the smart constructor UnorderedTree.node; concrete cases reduce by replace_leaf, replace_node_pair, and replace_self.

Main definitions

• UnorderedTree.replace

noncomputable 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.

noncomputable 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

theorem RoseTree.unorderedReplace_perm {α : Type u_1} [DecidableEq α] (target replacement : UnorderedTree α) {t s : RoseTree α} : t.Perm s → unorderedReplace target replacement t = unorderedReplace target replacement s

theorem RoseTree.unorderedReplaceList_permList {α : Type u_1} [DecidableEq α] (target replacement : UnorderedTree α) {cs ds : List (RoseTree α)} : PermList cs ds → unorderedReplaceList target replacement cs = unorderedReplaceList target replacement ds

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

Replace every subtree equal to target by replacement.

Equations

• target.replace replacement = UnorderedTree.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_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.