Theory Applications_Example

(* Author: Tassilo Lemke *)

subsection ‹Examples›

(* TODO: Disjointness and Subset Problem *)

theory Applications_Example
imports Applications
begin

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

datatype n = A | B | C | D
datatype t = a | b | c | d

definition P :: "(n, t) Prods" where "P ≡ {
  ―‹‹A → a | BB | C››
  (A, [Tm a]),
  (A, [Nt B, Nt B]),
  (A, [Nt C]),

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

  ―‹‹C → c | ε››
  (C, [Tm c]),
  (C, []),

  ―‹‹D → d››
  (D, [Tm d])
}"

text‹Checking whether a symbol is nullable is straight-forward:›

value "is_nullable P A"
― ‹@{value "is_nullable P A"}›

value "is_nullable P B"
― ‹@{value "is_nullable P B"}›

value "is_nullable P C"
― ‹@{value "is_nullable P C"}›

value "is_nullable P D"
― ‹@{value "is_nullable P D"}›

text‹Instead of using \texttt{value}, it can also be proven by \texttt{eval} in theorems:›

lemma "is_nullable P A" by eval

lemma "¬ is_nullable P B" by eval

lemma "is_nullable P C" by eval

lemma "¬ is_nullable P D" by eval

text‹Similarily, derivability can also be checked and proven as simple:›

―‹‹A ⇒* ABB› is valid:›
lemma "P ⊢ [Nt A] ⇒* [Nt A, Nt B, Nt B]"
  by eval

―‹But ‹A ⇒* AB› is not:›
lemma "¬ P ⊢ [Nt A] ⇒* [Nt A, Nt B]"
  by eval

text‹Following derivability, the membership problem is straight-forward:›

―‹‹a ∈ L(G)›:›
lemma "[a] ∈ Lang P A"
  by eval

―‹While ‹b ∈ L(G)›:›
lemma "[b] ∉ Lang P A"
  by eval

―‹But ‹bb ∈ L(G)› again holds:›
lemma "[b,b] ∈ Lang P A"
  by eval

text‹
  To check if the accepted language is empty, one first needs to unfold @{thm is_empty_def},
  from which automatic evaluation is again possible:
›

―‹Language obviously not empty:›
lemma "¬ Lang P A = {}"
  unfolding is_empty_def[symmetric] by eval

text‹
  Similar to derivability, reachability (i.e., derivability with an arbitrary prefix and suffix),
  can also be automated:
›

lemma "P ⊢ A ⇒⇧? B"
  by eval

lemma "P ⊢ B ⇒⇧? A"
  by eval

lemma "P ⊢ A ⇒⇧? C"
  by eval

lemma "P ⊢ B ⇒⇧? C"
  by eval

lemma "¬ P ⊢ C ⇒⇧? A"
  by eval

lemma "¬ P ⊢ C ⇒⇧? A"
  by eval

end