Theory Greibach_Hardest
section ‹Greibach's Hardest Context-Free Language›
theory Greibach_Hardest
imports
"Context_Free_Grammar.Context_Free_Language"
"Greibach_Normal_Form.Greibach_Normal_Form"
"Dyck_Language.Dyck_Language"
begin
text ‹
Formalization of Theorem 2.1 by Sheila Greibach \cite{Greibach73}:
\textbf{Theorem} For every context-free language ‹L› there is a homomorphism ‹h› with
‹L - {ε} = h⇧-⇧1(L⇩0 - {ε})›, where ‹L⇩0› is one fixed ``hardest'' context-free language.
The construction encodes the leftmost derivations of a
Greibach Normal Form (GNF) grammar as a nondeterministic Dyck word (the encoding homomorphism ‹enc_h›);
the general case is reduced to GNF using the AFP entry \verb!Greibach_Normal_Form! (the function ‹gnf_of›).
›
abbreviation Cons_power :: "'a ⇒ nat ⇒ 'a list" (infixl "#^" 70) where
"a #^ n ≡ replicate n a"
lemma bal_stk_append_split:
assumes "bal_stk s (xs @ ys) = (t, [])"
obtains s' where "bal_stk s xs = (s', [])" and "bal_stk s' ys = (t, [])"
using assms by (auto simp: bal_stk_append split: prod.splits if_splits)
lemma bal_stk_replicate_Open: "bal_stk s (Open a #^i) = (a#^i @ s, [])"
by (induction i arbitrary: s) (auto simp: replicate_append_same)
lemma bal_stk_replicate_Close: "bal_stk (a#^i @ t) (Close a #^ i) = (t, [])"
by (induction i arbitrary: t) auto
lemma bal_stk_replicate_Close_inv:
"bal_stk t (replicate i (Close a) @ rest) = (s, []) ⟹
∃t'. t = replicate i a @ t' ∧ bal_stk t' rest = (s, [])"
proof (induction i arbitrary: t)
case 0 thus ?case by auto
next
case (Suc i)
from Suc.prems obtain b t1 where t: "t = b # t1" by (cases t) auto
with Suc.prems have "a = b" "bal_stk t1 (replicate i (Close a) @ rest) = (s, [])"
by (auto split: if_splits)
with Suc.IH obtain t' where "t1 = replicate i a @ t'" "bal_stk t' rest = (s, [])" by blast
with t ‹a = b› show ?case by auto
qed
lemmas derives_Nt_map_TmD = derives_start1
lemma Lang_lfp_unfold:
"Lang_lfp P A = (⋃α ∈ Rhss P A. inst_syms (Lang_lfp P) α)"
unfolding Lang_lfp_def
using fun_cong[OF subst_lang_def[of P "lfp(subst_lang P)"], of A,symmetric]
by (metis lfp_unfold[OF mono_if_omega_cont[OF omega_cont_Lang_lfp]])
corollary Lang_unfold: "Lang P A = (⋃α ∈ Rhss P A. inst_syms (Lang P) α)"
by(fact Lang_lfp_unfold[unfolded Lang_lfp_eq_Lang])
lemma concats_simps[simp]:
"concats [] = {[]}"
"concats (L#Ls) = L @@ concats Ls"
by(auto simp: concats_def)
lemma concats_append[simp]: "concats (Ls1 @ Ls2) = concats Ls1 @@ concats Ls2"
by (simp add: concats_def foldr_conc_conc)
lemma inst_sym_simps[simp]:
"inst_sym L (Tm a) = {[a]}"
"inst_sym L (Nt A) = L A"
by(auto simp: inst_sym_def)
lemma inst_syms_Nil[simp]: "inst_syms L [] = {[]}"
by(simp add: inst_syms_def)
lemma inst_syms_Cons[simp]: "inst_syms L (s # β) = inst_sym L s @@ inst_syms L β"
by(simp add: inst_syms_def)
lemma inst_syms_append[simp]: "inst_syms L (α @ β) = inst_syms L α @@ inst_syms L β"
by(simp add: inst_syms_def)
lemma Lang_I: "(A, α) ∈ P ⟹ w ∈ inst_syms (Lang P) α ⟹ w ∈ Lang P A"
by (subst Lang_unfold) (auto simp: Rhss_def)
lemma Lang_subset_if:
assumes "⋀A α. (A,α) ∈ P ⟹ inst_syms R α ⊆ R A"
shows "Lang P A ⊆ R A"
proof -
have "subst_lang P R ≤ R"
using assms by (fastforce simp: subst_lang_def le_fun_def Rhss_def)
hence "lfp (subst_lang P) ≤ R" by (rule lfp_lowerbound)
hence "Lang_lfp P ≤ R" by (simp add: Lang_lfp_def)
thus ?thesis by (simp add: Lang_lfp_eq_Lang le_fun_def)
qed
subsection ‹The hardest language ‹L⇩0››
subsubsection ‹The terminal alphabet of ‹L⇩0››
text ‹Greibach's alphabet is ‹T = {a⇩1, a⇩2, ¦a⇩1, ¦a⇩2, c, ¢}› together with a fresh separator ‹d›.
There are two bracket ∗‹kinds› ‹a⇩1, a⇩2›, modelled by the type ‹t0_A›. A bracket letter is ‹Aa›
applied to an opening or closing bracket (of type @{typ ‹'a bracket›}) over a kind: thus
‹Aa (Open A1) = a⇩1›, ‹Aa (Close A1) = ¦a⇩1›, and analogously for ‹a⇩2›. The remaining letters are
‹Cc› for ‹c›, ‹Ce› for ‹¢›, and ‹Dd› for ‹d›.›
datatype t0_A = A1 | A2