theory CFG
  imports Main
begin

section ‹Adjusted content from AFP/LocalLexing›

type_synonym 'a rule = "'a × 'a list"

type_synonym 'a rules = "'a rule list"

datatype 'a cfg = CFG (R : "'a rules") (S : "'a")

definition nonterminals :: "'a cfg → 'a set" where
  "nonterminals G = set (map fst (R G)) ∪ {S G}"

definition is_word :: "'a cfg → 'a list → bool" where
  "is_word G ψ = (nonterminals G ∩ set ψ = {})"

definition derives1 :: "'a cfg → 'a list → 'a list → bool" where
  "derives1 G u v ≡ ∃ x y A α.
    u = x @ [A] @ y ∧
    v = x @ α @ y ∧
    (A, α) ∈ set (R G)"  

definition derivations1 :: "'a cfg → ('a list × 'a list) set" where
  "derivations1 G ≡ { (u,v) | u v. derives1 G u v }"

definition derivations :: "'a cfg → ('a list × 'a list) set" where 
  "derivations G ≡ (derivations1 G)^*"

definition derives :: "'a cfg → 'a list → 'a list → bool" where
  "derives G u v ≡ ((u, v) ∈ derivations G)"

syntax
  "derives1" :: "'a cfg → 'a list → 'a list → bool" (‹_ ⊨ _ → _› [1000,0,0] 1000)

syntax
  "derives" :: "'a cfg → 'a list → 'a list → bool" (‹_ ⊨ _ →^* _› [1000,0,0] 1000)

notation (latex output)
  derives1 (‹_ ⊨ _ → _› [1000,0,0] 1000)

notation (latex output)
  derives (‹_ ⊨ _ 🚫‹\ensuremath{\Rightarrow^{\ast}}› _› [1000,0,0] 1000)

end