theory CFG
imports Main
begin

typedecl symbol

type_synonym rule = "symbol × symbol list"

type_synonym sentence = "symbol list"

locale CFG =
  fixes N :: "symbol set"
  fixes T :: "symbol set"
  fixes R :: "rule set"
  fixes S :: "symbol"
  assumes disjunct_symbols: "N ∩ T = {}"
  assumes startsymbol_dom: "S ∈ N"
  assumes validRules: "∀ (N, α) ∈ R. N ∈ N ∧ (∀ s ∈ set α. s ∈ N ∪ T)"
begin

definition is_terminal :: "symbol → bool"
where
  "is_terminal s = (s ∈ T)"

definition is_nonterminal :: "symbol → bool"
where
  "is_nonterminal s = (s ∈ N)"

lemma is_nonterminal_startsymbol:"is_nonterminal S"
  by (simp add: is_nonterminal_def startsymbol_dom)

definition is_symbol :: "symbol → bool"
where
  "is_symbol s = (is_terminal s ∨ is_nonterminal s)"

definition is_sentence :: "sentence → bool"
where
  "is_sentence s = list_all is_symbol s"

definition is_word :: "sentence → bool"
where
  "is_word s = list_all is_terminal s"
   
definition derives1 :: "sentence → sentence → bool"
where
  "derives1 u v =
     (∃ x y N α.
          u = x @ [N] @ y
        ∧ v = x @ α @ y
        ∧ is_sentence x
        ∧ is_sentence y
        ∧ (N, α) ∈ R)"  

definition derivations1 :: "(sentence × sentence) set"
where
  "derivations1 = { (u,v) | u v. derives1 u v }"

definition derivations :: "(sentence × sentence) set"
where 
  "derivations = derivations1^*"

definition derives :: "sentence → sentence → bool"
where
  "derives u v = ((u, v) ∈ derivations)"

definition is_derivation :: "sentence → bool"
where
  "is_derivation u = derives [S] u"

definition L :: "sentence set"
where
  "L = { v | v. is_word v ∧ is_derivation v}"

definition "L_P"  :: "sentence set"
where
  "L_P = { u | u v. is_word u ∧ is_derivation (u@v) }"

end

end