Unrestricted Derivation Toolbox

This file provides basic lemmas for unrestricted derivations and terminal bookkeeping.

Main declarations

• grammar_deri_self
• grammar_deri_with_prefix
• all_used_terminals

theorem grammar_deri_self {T : Type} {g : grammar T} {w : List (symbol T g.nt)} : grammar_derives g w w

The Relation grammar_derives is reflexive.

theorem grammar_deri_of_tran {T : Type} {g : grammar T} {v w : List (symbol T g.nt)} : grammar_transforms g v w → grammar_derives g v w

theorem grammar_deri_of_deri_deri {T : Type} {g : grammar T} {u v w : List (symbol T g.nt)} (huv : grammar_derives g u v) (hvw : grammar_derives g v w) : grammar_derives g u w

The Relation grammar_derives is transitive.

theorem grammar_deri_of_deri_tran {T : Type} {g : grammar T} {u v w : List (symbol T g.nt)} (huv : grammar_derives g u v) (hvw : grammar_transforms g v w) : grammar_derives g u w

theorem grammar_deri_of_tran_deri {T : Type} {g : grammar T} {u v w : List (symbol T g.nt)} (huv : grammar_transforms g u v) (hvw : grammar_derives g v w) : grammar_derives g u w

theorem grammar_tran_or_id_of_deri {T : Type} {g : grammar T} {u w : List (symbol T g.nt)} (ass : grammar_derives g u w) : u = w ∨ ∃ (v : List (symbol T g.nt)), grammar_transforms g u v ∧ grammar_derives g v w

theorem grammar_deri_with_prefix {T : Type} {g : grammar T} {w₁ w₂ : List (symbol T g.nt)} (pᵣ : List (symbol T g.nt)) (ass : grammar_derives g w₁ w₂) : grammar_derives g (pᵣ ++ w₁) (pᵣ ++ w₂)

theorem grammar_deri_with_postfix {T : Type} {g : grammar T} {w₁ w₂ : List (symbol T g.nt)} (pₒ : List (symbol T g.nt)) (ass : grammar_derives g w₁ w₂) : grammar_derives g (w₁ ++ pₒ) (w₂ ++ pₒ)

def as_terminal {T N : Type} : symbol T N → Option T

Equations

• as_terminal (symbol.terminal t) = some t
• as_terminal (symbol.nonterminal a) = none

def all_used_terminals {T : Type} (g : grammar T) : List T

Equations

• all_used_terminals g = List.filterMap as_terminal (List.map grule.output_string g.rules).flatten