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