import Langlib.Grammars.ContextFree.EquivMathlibCFG
import Langlib.Classes.ContextFree.Closure.Substitution.Core
import Langlib.Classes.ContextFree.Definition
import Langlib.Utilities.ClosurePredicates

/-! # Context-Free Closure Under Substitution

This file imports mathlib's proof that context-free languages are closed under substitution and
repackages it for this project's `is_CF` predicate.

## Main declarations

- `CF_of_subst_CF`
-/

variable {α β : Type}

/-- The class of context-free languages is closed under substitution. -/
theorem CF_of_subst_CF (L : Language α) (f : α → Language β) :
    is_CF L → (∀ a, is_CF (f a)) → is_CF (L.subst f) := by
  intro hL hf
  rw [is_CF_iff_isContextFree]
  exact Language.IsContextFree.subst L f
    ((is_CF_iff_isContextFree).mp hL)
    (fun a => (is_CF_iff_isContextFree).mp (hf a))

/-- The class of context-free languages is closed under substitution. -/
theorem CF_closedUnderSubstitution [Fintype α] :
    ClosedUnderSubstitution is_CF := by
  intro α β _ L f hL hf
  exact CF_of_subst_CF L f hL hf