Theory CFG

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 (ℜ : "'a rules") (𝔖 : "'a")

definition nonterminals :: "'a cfg ⇒ 'a set" where
  "nonterminals G = set (map fst (ℜ G)) ∪ {𝔖 G}"

definition is_word :: "'a cfg ⇒ 'a list ⇒ bool" where
  "is_word 𝒢 ω = (nonterminals 𝒢 ∩ set ω = {})"

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

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

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

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

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 ("_ ⊢ _ \<^latex>‹\\ensuremath{\\Rightarrow^{\\ast}}› _" [1000,0,0] 1000)

end