Theory CFG

theory CFG
imports Main
begin

typedecl symbol

type_synonym rule = "symbol × symbol list"

type_synonym sentence = "symbol list"

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

definition is_terminal :: "symbol ⇒ bool"
where
  "is_terminal s = (s ∈ 𝔗)"

definition is_nonterminal :: "symbol ⇒ bool"
where
  "is_nonterminal s = (s ∈ 𝔑)"

lemma is_nonterminal_startsymbol:"is_nonterminal 𝔖"
  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, α) ∈ ℜ)"  

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 [𝔖] u"

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

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

end

end