Indexed languages under injective terminal maps

This file proves that indexed languages are both preserved and reflected by injective terminal maps.

Main declarations

• IndexedGrammar.language_mapTerminals
• Indexed_of_map_injective_Indexed
• Indexed_of_map_injective_Indexed_rev

def IndexedGrammar.mapIRhsSymbol {T₁ T₂ : Type} (f : T₁ → T₂) {N F : Type} : IRhsSymbol T₁ N F → IRhsSymbol T₂ N F

Equations

• IndexedGrammar.mapIRhsSymbol f (IRhsSymbol.terminal t) = IRhsSymbol.terminal (f t)
• IndexedGrammar.mapIRhsSymbol f (IRhsSymbol.nonterminal n push) = IRhsSymbol.nonterminal n push

def IndexedGrammar.mapTerminals {T₁ T₂ : Type} (f : T₁ → T₂) (g : IndexedGrammar T₁) : IndexedGrammar T₂

Equations

• One or more equations did not get rendered due to their size.

def IndexedGrammar.mapISym {T₁ T₂ : Type} (f : T₁ → T₂) (g : IndexedGrammar T₁) : g.ISym → (mapTerminals f g).ISym

Equations

• IndexedGrammar.mapISym f g (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal (f t)
• IndexedGrammar.mapISym f g (IndexedGrammar.ISym.indexed n σ) = IndexedGrammar.ISym.indexed n σ

theorem IndexedGrammar.language_mapTerminals {T₁ T₂ : Type} [Nonempty T₁] {f : T₁ → T₂} (hf : Function.Injective f) (g : IndexedGrammar T₁) : (mapTerminals f g).Language = (Language.map f) g.Language

Mapping an indexed grammar along an injective terminal map maps its language exactly.

theorem Indexed_of_map_injective_Indexed {T₁ T₂ : Type} [Nonempty T₁] {f : T₁ → T₂} (hf : Function.Injective f) (L : Language T₁) : is_Indexed L → is_Indexed ((Language.map f) L)

Indexedness is preserved by an injective terminal map.

theorem Indexed_of_map_injective_Indexed_rev {T₁ T₂ : Type} [Nonempty T₁] {f : T₁ → T₂} (hf : Function.Injective f) (L : Language T₁) (hL : is_Indexed ((Language.map f) L)) : is_Indexed L

Indexedness is reflected along an injective terminal map.