Context-Free Derivation Toolbox

This file provides basic closure lemmas for the derivation relation of a context-free grammar.

Main declarations

• CF_deri_self
• CF_deri_of_deri_deri
• CF_deri_with_prefix_and_postfix

theorem CF_deri_of_tran {T : Type} {g : CF_grammar T} {v w : List (symbol T g.nt)} : CF_transforms g v w → CF_derives g v w

theorem CF_deri_self {T : Type} {g : CF_grammar T} {w : List (symbol T g.nt)} : CF_derives g w w

The Relation CF_derives is reflexive.

theorem CF_deri_of_deri_deri {T : Type} {g : CF_grammar T} {u v w : List (symbol T g.nt)} (huv : CF_derives g u v) (hvw : CF_derives g v w) : CF_derives g u w

The Relation CF_derives is transitive.

theorem CF_deri_of_deri_tran {T : Type} {g : CF_grammar T} {u v w : List (symbol T g.nt)} (huv : CF_derives g u v) (hvw : CF_transforms g v w) : CF_derives g u w

theorem CF_deri_of_tran_deri {T : Type} {g : CF_grammar T} {u v w : List (symbol T g.nt)} (huv : CF_transforms g u v) (hvw : CF_derives g v w) : CF_derives g u w

theorem CF_tran_or_id_of_deri {T : Type} {g : CF_grammar T} {u w : List (symbol T g.nt)} (ass : CF_derives g u w) : u = w ∨ ∃ (v : List (symbol T g.nt)), CF_transforms g u v ∧ CF_derives g v w

theorem CF_deri_with_prefix {T : Type} {g : CF_grammar T} {w₁ w₂ : List (symbol T g.nt)} (pᵣ : List (symbol T g.nt)) (ass : CF_derives g w₁ w₂) : CF_derives g (pᵣ ++ w₁) (pᵣ ++ w₂)

theorem CF_deri_with_postfix {T : Type} {g : CF_grammar T} {w₁ w₂ : List (symbol T g.nt)} (pₒ : List (symbol T g.nt)) (ass : CF_derives g w₁ w₂) : CF_derives g (w₁ ++ pₒ) (w₂ ++ pₒ)

theorem CF_deri_with_prefix_and_postfix {T : Type} {g : CF_grammar T} {w₁ w₂ : List (symbol T g.nt)} (pᵣ pₒ : List (symbol T g.nt)) (ass : CF_derives g w₁ w₂) : CF_derives g (pᵣ ++ w₁ ++ pₒ) (pᵣ ++ w₂ ++ pₒ)