Licensed trees

A relation R a ks says that a node labelled a may have daughters labelled ks, in order: it is a set of local trees, each a node's label with its daughters' labels. R licenses a tree when every subtree of the tree satisfies it at its root, and the trees R licenses form a local tree language. The derivation trees of a context-free grammar are the trees its rules license, and any well-formedness condition on a node and its daughters' labels takes the same form; a condition on the root alone is a separate conjunct, and a condition that reads the daughters' subtrees is not of this form. A tree is licensed exactly when each of its local trees is (licensed_iff_forall_mem_localTrees), which decides licensing.

Main definitions

• RoseTree.Licensed R t: every subtree of t satisfies R at its root.

Main results

• RoseTree.licensed_node_iff: a tree is licensed when its root's local tree satisfies R and its children are licensed; RoseTree.Licensed.induction is the induction principle.
• RoseTree.Licensed.of_subtreeAt: licensing passes to subtrees.
• RoseTree.Licensed.replaceAt: replacing a subtree by a licensed tree with the same root value keeps the tree licensed.
• RoseTree.licensed_of_perm: a relation that ignores the order of the children licenses permuted trees alike, so it licenses unordered trees.

def RoseTree.Licensed {α : Type u_1} (R : α → List α → Prop) (t : RoseTree α) : Prop

R licenses t when every subtree of t satisfies it at its root, R a ks reading "a node labelled a may have daughters labelled ks, in order".

Equations

• RoseTree.Licensed R t = ∀ (s : RoseTree α), s.IsSubtree t → R s.value (List.map RoseTree.value s.children)

theorem RoseTree.licensed_node_iff {α : Type u_1} {R : α → List α → Prop} {a : α} {cs : List (RoseTree α)} : Licensed R (node a cs) ↔ R a (List.map value cs) ∧ ∀ c ∈ cs, Licensed R c

@[simp]

theorem RoseTree.licensed_leaf_iff {α : Type u_1} {R : α → List α → Prop} {a : α} : Licensed R (leaf a) ↔ R a []

theorem RoseTree.licensed_iff_forall_mem_localTrees {α : Type u_1} {R : α → List α → Prop} {t : RoseTree α} : Licensed R t ↔ ∀ e ∈ t.localTrees, R e.1 e.2

A tree is licensed exactly when each of its local trees is.

@[instance_reducible]

instance RoseTree.instDecidableLicensed {α : Type u_1} {R : α → List α → Prop} [(a : α) → (ks : List α) → Decidable (R a ks)] (t : RoseTree α) : Decidable (Licensed R t)

Equations

• t.instDecidableLicensed = decidable_of_iff (∀ e ∈ t.localTrees, R e.1 e.2) ⋯

theorem RoseTree.Licensed.rel_root {α : Type u_1} {R : α → List α → Prop} {a : α} {cs : List (RoseTree α)} (h : Licensed R (node a cs)) : R a (List.map value cs)

In a licensed tree the root's local tree satisfies R.

theorem RoseTree.Licensed.of_mem {α : Type u_1} {R : α → List α → Prop} {a : α} {cs : List (RoseTree α)} (h : Licensed R (node a cs)) {c : RoseTree α} (hc : c ∈ cs) : Licensed R c

theorem RoseTree.Licensed.induction {α : Type u_1} {R : α → List α → Prop} {motive : (t : RoseTree α) → Licensed R t → Prop} (node : ∀ (a : α) (cs : List (RoseTree α)) (hR : R a (List.map value cs)) (hcs : ∀ c ∈ cs, Licensed R c), (∀ (c : RoseTree α) (hc : c ∈ cs), motive c ⋯) → motive (node a cs) ⋯) {t : RoseTree α} (ht : Licensed R t) : motive t ht

Induction over the trees R licenses.

theorem RoseTree.Licensed.mono {α : Type u_1} {R R' : α → List α → Prop} (h : ∀ (a : α) (ks : List α), R a ks → R' a ks) {t : RoseTree α} (ht : Licensed R t) : Licensed R' t

theorem RoseTree.Licensed.of_isSubtree {α : Type u_1} {R : α → List α → Prop} {s t : RoseTree α} (ht : Licensed R t) (hs : s.IsSubtree t) : Licensed R s

theorem RoseTree.Licensed.of_subtreeAt {α : Type u_1} {R : α → List α → Prop} {t s : RoseTree α} (ht : Licensed R t) {p : List ℕ} (hs : t.subtreeAt p = some s) : Licensed R s

theorem RoseTree.Licensed.replaceAt {α : Type u_1} {R : α → List α → Prop} {t s new : RoseTree α} (ht : Licensed R t) {p : List ℕ} (hs : t.subtreeAt p = some s) (hnew : Licensed R new) (hv : new.value = s.value) : Licensed R (t.replaceAt p new)

Replacing a subtree by a licensed tree with the same root value keeps a tree licensed.

theorem RoseTree.licensed_of_perm {α : Type u_1} {R : α → List α → Prop} (hR : ∀ (a : α) {ks ls : List α}, ks.Perm ls → (R a ks ↔ R a ls)) {t s : RoseTree α} : t.Perm s → (Licensed R t ↔ Licensed R s)

A relation that ignores the order of the children licenses a tree exactly when it licenses any permutation of it.