Theory DPDA_Complement_HU
section ‹DCFLs are Closed Under Complementation›
theory DPDA_Complement_HU
imports Det_Pushdown_Automata
begin
subsection ‹Setup and Auxiliary Lemmas›
context pda begin
definition steps1 :: "'q × 'a list × 's list ⇒ 'q × 'a list × 's list ⇒ bool" (infix "↝+" 55) where
"steps1 ≡ step⇩1 ^++"
abbreviation no_step⇩1 ("(_ ↝|)" [1000] 999) where
"cf ↝| ≡ (∀cf'. ¬cf ↝ cf')"
lemma steps1_induct[consumes 1, case_names base step]:
assumes "x1 ↝+ x2"
and "⋀q w α p u γ. (q, w, α) ↝ (p, u, γ) ⟹ P (q, w, α) (p, u, γ)"
and "⋀q w α r v β p u γ. (q, w, α) ↝ (r, v, β) ⟹ (r, v, β) ↝+ (p, u, γ) ⟹
P (r, v, β) (p, u, γ) ⟹ P (q, w, α) (p, u, γ)"
shows "P x1 x2"
using assms[unfolded steps1_def]
proof(induction rule: converse_tranclp_induct)
case base thus ?case by (metis prod_cases3)
next
case step thus ?case by simp (metis prod_cases3 step⇩1.simps)
qed
lemma steps1_converse_induct[consumes 1, case_names base step]:
assumes "x1 ↝+ x2"
and "⋀q w α p u γ. (q, w, α) ↝ (p, u, γ) ⟹ P (q, w, α) (p, u, γ)"
and "⋀q w α r v β p u γ. (q, w, α) ↝+ (r, v, β) ⟹ (r, v, β) ↝ (p, u, γ) ⟹
P (q, w, α) (r, v, β) ⟹ P (q, w, α) (p, u, γ)"
shows "P x1 x2"
using assms[unfolded steps1_def]
proof(induction rule: tranclp_induct)
case base
then show ?case by (metis prod_cases3)
next
case (step)
then show ?case by simp (metis prod_cases3 step⇩1.simps)
qed
lemma steps1_steps:
"(q, w, α) ↝+ (p, u, γ) ⟹ (q, w, α) ↝* (p, u, γ)"
by (simp add: steps_def steps1_def)
lemma steps1_step:
"(q, w, α) ↝ (p, u, γ) ⟹ (q, w, α) ↝+ (p, u, γ)"
by (simp add: steps1_def tranclp.r_into_trancl)
lemma steps1_trans:
"(q, w, α) ↝+ (p, u, γ) ⟹ (p, u, γ) ↝+ (r, v, β) ⟹ (q, w, α) ↝+ (r, v, β)"
using steps1_def by force
lemma steps_steps1:
assumes "(q, w, α) ↝* (p, u, γ)"
and "(q, w, α) ≠ (p, u, γ)"
shows "(q, w, α) ↝+ (p, u, γ)"
using assms unfolding steps_def steps1_def by (meson rtranclpD)
lemma steps1_split_last: "(∃r v β. (q, w, α) ↝* (r, v, β) ∧ (r, v, β) ↝ (p, u, γ))
⟷ (q, w, α) ↝+ (p, u, γ)"
by (smt (verit, ccfv_threshold) rtranclp_into_tranclp1 step⇩1.elims(2) steps1_def steps_def steps_refl tranclp.simps
tranclp_into_rtranclp)
lemma split_path:
assumes "(q, w, α) ↝(n) (p, [], γ)"
and "m ≤ n"
shows "∃r u β. (q, w, α) ↝(m) (r, u, β) ∧ (r, u, β) ↝(n-m) (p, [], γ)"
using assms proof (induction "n-m" arbitrary: m)
case (Suc x)
from Suc.prems(2) consider (a) "m=n" | (b) "m<n" by linarith
then show ?case
proof cases
case a
with Suc.prems(1) show ?thesis by auto
next
case b
with Suc.hyps(1)[of "Suc m"] Suc.hyps(2) Suc.prems(1) obtain r u β
where p1: "(q, w, α) ↝(Suc m) (r, u, β)" and p2: "(r, u, β) ↝(n - Suc m) (p, [], γ)" by fastforce
from p1 obtain s v ζ where *: "(q, w, α) ↝(m) (s, v, ζ)" and s: "(s, v, ζ) ↝ (r, u, β)"
using stepn_split_last[of m q w α r u β] by auto
from s p2 b have **: "(s, v, ζ) ↝(n - m) (p, [], γ)"
using stepn_split_first[of s v ζ "n - Suc m" p "[]" γ] Suc_diff_Suc by force
from * ** show ?thesis by blast
qed
qed auto
end
context dpda begin
lemma max_eps_steps:
assumes "(q, w, α) ↝(n) (p, u, γ)"
and "(p, [], γ) ↝|"
and "(q, w, α) ↝(m) (r, u, β)"
shows "m ≤ n"
proof (rule ccontr)
assume "¬ m ≤ n"
then have n_less_m: "Suc n ≤ m" by simp
from assms(1) obtain v where w_def: "w = v@u"
using stepn_steps[of q w α p u γ] decreasing_word[of q w α p u γ] by blast
from assms(3)[unfolded w_def] have p: "(q, v, α) ↝(m) (r, [], β)"
using stepn_word_app[of m q v α r "[]" β u] by simp
obtain s y ζ where *: "(q, v, α) ↝(Suc n) (s, y, ζ)"
using split_path[OF p n_less_m] by fastforce
from assms(1)[unfolded w_def] have **: "(q, v, α) ↝(n) (p, [], γ)"
using stepn_word_app[of n q v α p "[]" γ u] by simp
from * ** have "(p, [], γ) ↝ (s, y, ζ)"
using stepn_split_last[of n q v α s y ζ] dpda_stepn_det[of n q v α p "[]" γ] by metis
with assms(2) show False by simp
qed
end
text ‹In what follows, we show that the complement of a deterministic context-free language is also a
deterministic context-free language. For this purpose, we construct a deterministic pushdown automaton
that recognizes the complement language of a given deterministic pushdown automaton. The proof
follows that of Hopcroft and Ullman \cite{HopcroftU79}. The construction is divided into two parts: First, construct an equivalent
deterministic pushdown automaton that scans the entire input for all given input words, and then construct the automaton that recognizes the complement
language out of this automaton.›
subsection ‹Scan Construction›
text ‹To scan the entire input, we address two complications: ensuring that every configuration has a possible step and that
no configuration allows infinite epsilon steps. For the first problem, we introduce a new stack symbol to prevent the
stack from becoming empty and a dead state that the automaton moves to when there are no possible steps. For the second
problem, we introduce a new final state that the automaton moves to if an infinite number of epsilon steps pass through
a final state; otherwise, the automaton moves to the dead state.›
subsubsection ‹Definition›