Theory Pre_Star_Example

(* Author: Tassilo Lemke *)

subsection‹$Pre^*$ Example›

text‹The algorithm is executable. This theory shows a quick example.›

theory Pre_Star_Example
  imports Pre_Star
begin

text‹Consider the following grammar, with ‹V = {A,B}› and ‹Σ = {a,b}›:›

datatype n = A | B
datatype t = a | b

definition "P ≡ {
  ― ‹‹A → a | BB››
  (A, [Tm a]),
  (A, [Nt B, Nt B]),

  ― ‹‹B → AB | b››
  (B, [Nt A, Nt B]),
  (B, [Tm b])
}"

text‹The following NFA accepts the regular language, whose predecessors we want to find:›

definition M :: "(nat, (n, t) sym) auto" where "M ≡ ⦇
  auto.lts = {
    (0, Tm a, 1),
    (1, Tm b, 2),
    (2, Tm a, 1)
  },
  start = 0 :: nat,
  finals = {0, 1, 2}
⦈"

lemma "pre_star_auto P M =
  ⦇auto.lts =
    {(2, Tm a, 1), (1, Tm b, 2), (0, Tm a, 1), (0, Nt A, 1), (0, Nt A, 2), (0, Nt B, 2), (0, Nt A, 1),
     (1, Nt A, 2), (1, Nt B, 2), (2, Nt A, 1), (2, Nt A, 2), (2, Nt B, 2), (2, Nt A, 1), (1, Nt A, 2),
     (1, Nt B, 2)},
   start = 0, finals = {0, 1, 2}⦈"
by eval

end