Subtrees of nonplanar trees

UnorderedTree.subtrees t is the multiset of all subtrees of t, the root included, one per vertex, so its cardinality is t.numNodes. It is computed on a planar representative by RoseTree.unorderedSubtrees, which also serves proofs that recurse over planar children.

Main definitions

• UnorderedTree.subtrees, RoseTree.unorderedSubtrees

Main results

• UnorderedTree.subtrees_node: a node's subtrees are the node itself and its children's subtrees.
• UnorderedTree.card_subtrees: one subtree per vertex.
• RoseTree.mem_unorderedSubtrees: the nonplanar subtrees of a planar tree are the images of its subtrees at its positions.

Implementation notes

subtrees is lifted from the planar recursion, not defined by UnorderedTree.para, whose tupling rebuilds every subtree with node and so slows kernel decide on c-command. It is well-defined because the planar recursion computes the paramorphism.

def RoseTree.unorderedSubtrees {α : Type u_1} : RoseTree α → Multiset (UnorderedTree α)

The nonplanar subtrees of a planar tree, root included.

Equations

• (RoseTree.node a cs).unorderedSubtrees = UnorderedTree.mk (RoseTree.node a cs) ::ₘ RoseTree.unorderedSubtreesList cs

def RoseTree.unorderedSubtreesList {α : Type u_1} : List (RoseTree α) → Multiset (UnorderedTree α)

The nonplanar subtrees of a list of trees.

Equations

• RoseTree.unorderedSubtreesList [] = 0
• RoseTree.unorderedSubtreesList (c :: cs) = c.unorderedSubtrees + RoseTree.unorderedSubtreesList cs

theorem RoseTree.unorderedSubtrees_eq_map {α : Type u_1} (p : RoseTree α) : p.unorderedSubtrees = ↑(List.map UnorderedTree.mk p.subtrees)

The nonplanar subtrees of a planar tree are the images of its subtrees.

theorem RoseTree.unorderedSubtreesList_eq_map {α : Type u_1} (cs : List (RoseTree α)) : unorderedSubtreesList cs = ↑(List.map UnorderedTree.mk (List.flatMap subtrees cs))

theorem RoseTree.mem_unorderedSubtrees {α : Type u_1} {p : RoseTree α} {x : UnorderedTree α} : x ∈ p.unorderedSubtrees ↔ ∃ (q : List ℕ) (s : RoseTree α), p.subtreeAt q = some s ∧ UnorderedTree.mk s = x

def UnorderedTree.subtrees {α : Type u_1} : UnorderedTree α → Multiset (UnorderedTree α)

All subtrees of a nonplanar tree, root included.

Equations

• UnorderedTree.subtrees = Quotient.lift RoseTree.unorderedSubtrees ⋯

@[simp]

theorem UnorderedTree.subtrees_mk {α : Type u_1} (t : RoseTree α) : (mk t).subtrees = t.unorderedSubtrees

@[simp]

theorem UnorderedTree.subtrees_node {α : Type u_1} (a : α) (F : Multiset (UnorderedTree α)) : (node a F).subtrees = node a F ::ₘ (Multiset.map subtrees F).sum

theorem UnorderedTree.subtrees_leaf {α : Type u_1} (a : α) : (leaf a).subtrees = {leaf a}

theorem UnorderedTree.subtrees_node_pair {α : Type u_1} (a : α) (l r : UnorderedTree α) : (node a {l, r}).subtrees = node a {l, r} ::ₘ (l.subtrees + r.subtrees)

@[simp]

theorem UnorderedTree.mem_subtrees_leaf {α : Type u_1} {m : UnorderedTree α} {a : α} : m ∈ (leaf a).subtrees ↔ m = leaf a

@[simp]

theorem UnorderedTree.mem_subtrees_node_pair {α : Type u_1} {m : UnorderedTree α} {a : α} {l r : UnorderedTree α} : m ∈ (node a {l, r}).subtrees ↔ m = node a {l, r} ∨ m ∈ l.subtrees ∨ m ∈ r.subtrees

theorem UnorderedTree.self_mem_subtrees {α : Type u_1} (t : UnorderedTree α) : t ∈ t.subtrees

theorem UnorderedTree.card_subtrees {α : Type u_1} (t : UnorderedTree α) : t.subtrees.card = t.numNodes

One subtree per vertex.