Theory Det_Pushdown_Automata

(* TODO mv to Pushdown_Automata *)

section ‹Deterministic Pushdown Automata›

theory Det_Pushdown_Automata
  imports Pushdown_Automata.Pushdown_Automata
begin

text ‹A deterministic pushdown automaton, following Hopcroft and Ullman \cite{HopcroftU79}:›

locale dpda = pda M for M :: "('q :: finite, 'a :: finite, 's :: finite) pda" +
  assumes δ_nonempty: "δ M q a X ≠ {} ⟶ δε M q X = {}"
      and δ_singleton: "δ M q a X = {} ∨ (∃p γ. δ M q a X = {(p, γ)})"
      and δε_singleton: "δε M q X = {} ∨ (∃p γ. δε M q X = {(p, γ)})"
begin

text ‹In every configuration,
\begin{itemize}
\item @{thm [source] δ_nonempty} enforces that not both an epsilon step and a true step can be enabled.
\item @{thm [source] δ_singleton} allows for at most one true step.
\item @{thm [source] δε_singleton} allows for at most one epsilon step.
\end{itemize}›

text ‹The automaton can take at most one step from any configuration:›
lemma dpda_step: "step (q, w, α) = {} ∨ (∃p u γ. step (q, w, α) = {(p, u, γ)})"
proof (cases α)
  case [simp]: (Cons X α')
  show ?thesis proof (cases w)
    case Nil
    then show ?thesis
      using δε_singleton[of q X] by auto
  next
    case [simp]: (Cons a w')
    consider (a) "δ M q a X = {}" | (b) "δ M q a X ≠ {}" by satx
    then show ?thesis proof cases
      case a
      then show ?thesis
        using δε_singleton[of q X] by auto
    next
      case b
      then show ?thesis
        using δ_nonempty[of q a X] δ_singleton[of q a X] by auto
    qed
  qed
qed auto

text ‹A step of the automaton is indeed deterministic:›
lemma dpda_step⇩1_det:
  assumes "(q, w, α) ↝ (p, u, γ)"
      and "(q, w, α) ↝ (p', u', γ')"
    shows "p = p' ∧ u = u' ∧ γ = γ'"
using assms dpda_step by fastforce

lemma dpda_stepn_det:
  assumes "(q, w, α) ↝(n) (p, u, γ)"
      and "(q, w, α) ↝(n) (p', u', γ')"
    shows "p = p' ∧ u = u' ∧ γ = γ'"
using assms proof (induction "(q, w, α)" "(p, u, γ)" arbitrary: q w α rule: stepn_induct)
  case (stepn n q w α r u β)
  from stepn(4) have *: "(r, u, β) ↝(n) (p', u', γ')"
    using stepn_split_first[of q w α n p' u' γ'] dpda_step⇩1_det[OF stepn(1)] by auto
  from stepn(3)[OF *] show ?case .
qed auto

end

end