Theory Ogdens_Lemma
section ‹Ogden's Lemma for Context-Free Grammars›
theory Ogdens_Lemma
imports
"Context_Free_Grammar.Chomsky_Normal_Form"
"Context_Free_Grammar.Parse_Tree"
begin
text ‹
Ogden's Lemma \cite{Ogden68} (see also \cite{HopcroftU79}) is a refinement of the pumping lemma
in which one first ∗‹marks› (``distinguishes'') a set of positions of the word,
and the pumped parts are guaranteed to interact with the marked positions.
Unlike the pumping lemma (theory ‹Pumping_Lemma_CFG›), whose proof
follows a single path and therefore does ∗‹not› need explicit parse trees, Ogden's lemma
is genuinely a parse-tree argument: a ∗‹branch point› is a node ∗‹both› of whose subtrees
contain a marked leaf, and that notion cannot be expressed along one path only. We therefore
build on theory ‹Parse_Tree›.
This theory was generated with the help of Claude and the above literature.
›
subsection ‹Markings›
text ‹A ∗‹marking› of a word/fringe is a boolean list of the same length; position ‹i› is
distinguished iff the marking carries \<^const>‹True› there. \<^term>‹dcount ms› counts the
distinguished positions in (a slice) ‹ms›.›
abbreviation dcount :: "bool list ⇒ nat" where
"dcount ms ≡ count_list ms True"
subsection ‹CNF parse trees and branch points›
text ‹\<^term>‹cnf_tree t› characterises the shape of a complete parse tree of a terminal word
under a CNF grammar: every internal node either has a single terminal-leaf child
(‹A → a›) or two nonterminal-rooted subtrees (‹A → B C›); all leaves are terminals.›
fun cnf_tree :: "('n,'t) ptree ⇒ bool" where
"cnf_tree (Sym (Tm _)) = True" |
"cnf_tree (Sym (Nt _)) = False" |
"cnf_tree (Prod _ [Sym (Tm _)]) = True" |
"cnf_tree (Prod _ [t1, t2]) =
((∃B. root t1 = Nt B) ∧ (∃C. root t2 = Nt C) ∧ cnf_tree t1 ∧ cnf_tree t2)" |
"cnf_tree (Prod _ _) = False"
text ‹Following Hopcroft \& Ullman, descend from the root choosing, at each branch point, the
subtree with more distinguished leaves (and otherwise the unique marked subtree). \<^term>‹bspine t ms›
collects the nonterminals labelling the ∗‹branch points› met on this ``heavy'' path, top to
bottom. The marking \<^term>‹ms› is the slice of the global marking aligned with \<^term>‹fringe t›;
a binary node splits it at \<^term>‹length (fringe t1)›.›
fun bspine :: "('n,'t) ptree ⇒ bool list ⇒ 'n list" where
"bspine (Prod A [t1, t2]) ms =
(let ms1 = take (length (fringe t1)) ms; ms2 = drop (length (fringe t1)) ms in
if 0 < dcount ms1 ∧ 0 < dcount ms2
then A # (if dcount ms2 ≤ dcount ms1 then bspine t1 ms1 else bspine t2 ms2)
else if 0 < dcount ms1 then bspine t1 ms1
else bspine t2 ms2)" |
"bspine _ _ = []"
text ‹❙‹Building block 1.› A complete parse tree of a terminal word under a CNF grammar is a
\<^const>‹cnf_tree›. ∗‹Proof:› induction on ‹t›; \<^const>‹CNF› forces ‹(A, map root ts) ∈ P› to be
either ‹[Tm a]› or ‹[Nt B, Nt C]›, and \<^prop>‹fringe t = map Tm w› forces every leaf to be a
\<^const>‹Tm›.›
lemma cnf_tree_if_parse_tree:
"⟦ CNF P; parse_tree P t; fringe t = map Tm w ⟧ ⟹ cnf_tree t"
proof (induction t arbitrary: w)
case (Sym s) thus ?case by fastforce
next
case (Prod A ts)
have disj: "(∃B C. map root ts = [Nt B, Nt C]) ∨ (∃a. map root ts = [Tm a])"
using Prod.prems(1,2) by (auto simp: CNF_def)
then show ?case
proof (elim disjE exE)
fix B C assume "map root ts = [Nt B, Nt C]"
then obtain t1 t2 where ts: "ts = [t1, t2]"
and r1: "root t1 = Nt B" and r2: "root t2 = Nt C"
by (auto simp: map_eq_Cons_conv)
have "map Tm w = fringe t1 @ fringe t2" using Prod.prems(3) ts by simp
then obtain w1 w2 where w12: "fringe t1 = map Tm w1" "fringe t2 = map Tm w2"
by (auto simp: map_eq_append_conv)
have "cnf_tree t1" "cnf_tree t2"
using Prod.IH Prod.prems(1,2) ts w12 by auto
thus "cnf_tree (Prod A ts)" using ts r1 r2 by auto
next
fix a assume "map root ts = [Tm a]"
then obtain t' where t': "ts = [t']" and r: "root t' = Tm a"
by (auto simp: map_eq_Cons_conv)
from t' r have "ts = [Sym (Tm a)]" by (cases t') auto
thus "cnf_tree (Prod A ts)" by simp
qed
qed
text ‹❙‹Building block 2.› Each branch point at least halves the number of distinguished leaves
on the heavy side, so a tree with ‹d› distinguished leaves has a heavy path with at least
‹log2 d› branch points. ∗‹Proof:› induction on ‹t›. At a binary node ‹ms = ms1 @ ms2› and
\<^prop>‹dcount ms = dcount ms1 + dcount ms2›; at a branch point we recurse into the heavier child
‹h›, with \<^prop>‹dcount ms ≤ 2 * dcount h› and one more branch point; otherwise all marks lie in one
child and the bound is preserved.›
lemma dcount_aux: "length ms = Suc 0 ⟹ dcount ms ≤ Suc 0"
by (metis count_le_length)
lemma dcount_le_pow_bspine:
"⟦ cnf_tree t; length ms = length (fringe t) ⟧ ⟹ dcount ms ≤ 2 ^ length (bspine t ms)"
proof (induction t arbitrary: ms rule: cnf_tree.induct)
case (4 A t1 t2 ms)
let ?n1 = "length (fringe t1)"
let ?ms1 = "take ?n1 ms"
let ?ms2 = "drop ?n1 ms"
have ct1: "cnf_tree t1" and ct2: "cnf_tree t2" using "4.prems"(1) by auto
have len: "length ms = length (fringe t1) + length (fringe t2)" using "4.prems"(2) by simp
have l1: "length ?ms1 = length (fringe t1)" using len by simp
have l2: "length ?ms2 = length (fringe t2)" using len by simp
have dc: "dcount ms = dcount ?ms1 + dcount ?ms2"
by (metis append_take_drop_id count_list_append)
have IH1: "dcount ?ms1 ≤ 2 ^ length (bspine t1 ?ms1)" using "4.IH"(1) ct1 l1 by blast
have IH2: "dcount ?ms2 ≤ 2 ^ length (bspine t2 ?ms2)" using "4.IH"(2) ct2 l2 by blast
consider (both) "0 < dcount ?ms1 ∧ 0 < dcount ?ms2"
| (left) "¬ (0 < dcount ?ms1 ∧ 0 < dcount ?ms2)" "0 < dcount ?ms1"
| (right) "¬ (0 < dcount ?ms1 ∧ 0 < dcount ?ms2)" "¬ 0 < dcount ?ms1"
by blast
then show ?case
proof cases
case both
show ?thesis
proof (cases "dcount ?ms2 ≤ dcount ?ms1")
case True
hence bs: "bspine (Prod A [t1, t2]) ms = A # bspine t1 ?ms1"
using both by (simp add: Let_def)
have "dcount ms ≤ 2 * dcount ?ms1" using dc True by simp
also have "… ≤ 2 * 2 ^ length (bspine t1 ?ms1)" using IH1 by simp
also have "… = 2 ^ length (bspine (Prod A [t1, t2]) ms)" using bs by simp
finally show ?thesis .
next
case False
hence bs: "bspine (Prod A [t1, t2]) ms = A # bspine t2 ?ms2"
using both by (simp add: Let_def)
have "dcount ms ≤ 2 * dcount ?ms2" using dc False by simp
also have "… ≤ 2 * 2 ^ length (bspine t2 ?ms2)" using IH2 by simp
also have "… = 2 ^ length (bspine (Prod A [t1, t2]) ms)" using bs by simp
finally show ?thesis .
qed
next
case left
hence z2: "dcount ?ms2 = 0" by simp
have bs: "bspine (Prod A [t1, t2]) ms = bspine t1 ?ms1"
using left by (simp add: Let_def)
have "dcount ms = dcount ?ms1" using dc z2 by simp
also have "… ≤ 2 ^ length (bspine t1 ?ms1)" using IH1 by simp
also have "… = 2 ^ length (bspine (Prod A [t1, t2]) ms)" using bs by simp
finally show ?thesis .
next
case right
hence z1: "dcount ?ms1 = 0" by simp
have bs: "bspine (Prod A [t1, t2]) ms = bspine t2 ?ms2"
using right by (simp add: Let_def)
have "dcount ms = dcount ?ms2" using dc z1 by simp
also have "… ≤ 2 ^ length (bspine t2 ?ms2)" using IH2 by simp
also have "… = 2 ^ length (bspine (Prod A [t1, t2]) ms)" using bs by simp
finally show ?thesis .
qed
qed (simp_all add: dcount_aux)
text ‹❙‹Building block 3.› Every label on the spine is a left-hand side of ‹P›, hence a
nonterminal of ‹P›. ∗‹Proof:› induction on ‹t›; a label ‹A› is emitted only at a
\<^term>‹Prod A [t1,t2]› node, where \<^prop>‹(A, [root t1, root t2]) ∈ P›.›
lemma bspine_in_Nts:
"parse_tree P t ⟹ set (bspine t ms) ⊆ Nts P"
proof (induction t arbitrary: ms rule: cnf_tree.induct)
case (4 A t1 t2 ms)
let ?ms1 = "take (length (fringe t1)) ms"
let ?ms2 = "drop (length (fringe t1)) ms"
have pt1: "parse_tree P t1" and pt2: "parse_tree P t2"
and inP: "(A, [root t1, root t2]) ∈ P" using "4.prems" by auto
have A: "A ∈ Nts P" using inP by (auto simp: Nts_def)
have s1: "set (bspine t1 ?ms1) ⊆ Nts P" using "4.IH"(1) pt1 by blast
have s2: "set (bspine t2 ?ms2) ⊆ Nts P" using "4.IH"(2) pt2 by blast
have "set (bspine (Prod A [t1, t2]) ms)
⊆ insert A (set (bspine t1 ?ms1) ∪ set (bspine t2 ?ms2))"
by (auto simp: Let_def)
thus ?case using A s1 s2 by auto
qed simp_all
subsection ‹Locating a labelled branch point and lifting through a CNF node›
lemma derives_bin:
assumes "(A0, [Nt B, Nt C]) ∈ P" "P ⊢ [Nt B] ⇒* α" "P ⊢ [Nt C] ⇒* β"
shows "P ⊢ [Nt A0] ⇒* α @ β"
using derives_append_append[OF assms(2,3)]
by (simp add: derives_Cons_rule[OF assms(1)])
text ‹If ‹A› labels a branch point on the heavy path of ‹t›, read off the context derivation
‹[root t] ⇒* v [Nt A] x› and the subterminal yield ‹[Nt A] ⇒* w›, threading the marking.›
lemma ctx_label:
"⟦ cnf_tree t; parse_tree P t; length ms = length (fringe t); fringe t = map Tm zt;
A ∈ set (bspine t ms) ⟧ ⟹
∃v w x dv dw dx. zt = v @ w @ x ∧ ms = dv @ dw @ dx ∧
length dv = length v ∧ length dw = length w ∧ length dx = length x ∧
P ⊢ [root t] ⇒* map Tm v @ [Nt A] @ map Tm x ∧ P ⊢ [Nt A] ⇒* map Tm w"
proof (induction t arbitrary: ms zt rule: cnf_tree.induct)
case (4 A0 t1 t2 ms zt)
from "4.prems"(1) obtain B C where rB: "root t1 = Nt B" and rC: "root t2 = Nt C"
and ct1: "cnf_tree t1" and ct2: "cnf_tree t2" by auto
from "4.prems"(2) have pt1: "parse_tree P t1" and pt2: "parse_tree P t2"
and inP: "(A0, [root t1, root t2]) ∈ P" by auto
have inP': "(A0, [Nt B, Nt C]) ∈ P" using inP rB rC by simp
let ?n1 = "length (fringe t1)"
let ?ms1 = "take ?n1 ms"
let ?ms2 = "drop ?n1 ms"
have len: "length ms = length (fringe t1) + length (fringe t2)" using "4.prems"(3) by simp
have l1: "length ?ms1 = length (fringe t1)" and l2: "length ?ms2 = length (fringe t2)"
using len by auto
have msplit: "ms = ?ms1 @ ?ms2" by simp
from "4.prems"(4) have "map Tm zt = fringe t1 @ fringe t2" by simp
then obtain z1 z2 where z1: "fringe t1 = map Tm z1" and z2: "fringe t2 = map Tm z2"
and zt: "zt = z1 @ z2" by (auto simp: map_eq_append_conv)
have dB: "P ⊢ [Nt B] ⇒* map Tm z1" using derives_fringe_if_parse_tree[OF pt1] rB z1 by simp
have dC: "P ⊢ [Nt C] ⇒* map Tm z2" using derives_fringe_if_parse_tree[OF pt2] rC z2 by simp
have recL: ?case if AL: "A ∈ set (bspine t1 ?ms1)"
proof -
from "4.IH"(1)[OF ct1 pt1 l1 z1 AL] obtain v1 w1 x1 dv1 dw1 dx1 where
Q: "z1 = v1 @ w1 @ x1" "?ms1 = dv1 @ dw1 @ dx1"
"length dv1 = length v1" "length dw1 = length w1" "length dx1 = length x1"
"P ⊢ [root t1] ⇒* map Tm v1 @ [Nt A] @ map Tm x1" "P ⊢ [Nt A] ⇒* map Tm w1" by blast
have dB1: "P ⊢ [Nt B] ⇒* map Tm v1 @ [Nt A] @ map Tm x1" using Q(6) rB by simp
have "P ⊢ [Nt A0] ⇒* (map Tm v1 @ [Nt A] @ map Tm x1) @ map Tm z2"
by (rule derives_bin[OF inP' dB1 dC])
hence d: "P ⊢ [Nt A0] ⇒* map Tm v1 @ [Nt A] @ map Tm (x1 @ z2)" by simp
have "zt = v1 @ w1 @ (x1 @ z2) ∧ ms = dv1 @ dw1 @ (dx1 @ ?ms2) ∧
length dv1 = length v1 ∧ length dw1 = length w1 ∧
length (dx1 @ ?ms2) = length (x1 @ z2) ∧
P ⊢ [root (Prod A0 [t1,t2])] ⇒* map Tm v1 @ [Nt A] @ map Tm (x1 @ z2) ∧
P ⊢ [Nt A] ⇒* map Tm w1"
using Q zt z2 l2 d msplit by simp
thus ?case by blast
qed
have recR: ?case if AR: "A ∈ set (bspine t2 ?ms2)"
proof -
from "4.IH"(2)[OF ct2 pt2 l2 z2 AR] obtain v2 w2 x2 dv2 dw2 dx2 where
Q: "z2 = v2 @ w2 @ x2" "?ms2 = dv2 @ dw2 @ dx2"
"length dv2 = length v2" "length dw2 = length w2" "length dx2 = length x2"
"P ⊢ [root t2] ⇒* map Tm v2 @ [Nt A] @ map Tm x2" "P ⊢ [Nt A] ⇒* map Tm w2" by blast
have dC2: "P ⊢ [Nt C] ⇒* map Tm v2 @ [Nt A] @ map Tm x2" using Q(6) rC by simp
have "P ⊢ [Nt A0] ⇒* map Tm z1 @ (map Tm v2 @ [Nt A] @ map Tm x2)"
by (rule derives_bin[OF inP' dB dC2])
hence d: "P ⊢ [Nt A0] ⇒* map Tm (z1 @ v2) @ [Nt A] @ map Tm x2" by simp
have "zt = (z1 @ v2) @ w2 @ x2 ∧ ms = (?ms1 @ dv2) @ dw2 @ dx2 ∧
length (?ms1 @ dv2) = length (z1 @ v2) ∧ length dw2 = length w2 ∧
length dx2 = length x2 ∧
P ⊢ [root (Prod A0 [t1,t2])] ⇒* map Tm (z1 @ v2) @ [Nt A] @ map Tm x2 ∧
P ⊢ [Nt A] ⇒* map Tm w2"
using Q zt z1 l1 d msplit by simp
thus ?case by blast
qed
have lenzt: "length ms = length zt" using "4.prems"(3,4) by (metis length_map)
show ?case
proof (cases "A = A0 ∧ 0 < dcount ?ms1 ∧ 0 < dcount ?ms2")
case True
hence rt: "root (Prod A0 [t1,t2]) = Nt A" by simp
have D1: "P ⊢ [root (Prod A0 [t1,t2])] ⇒* map Tm [] @ [Nt A] @ map Tm []"
using rt by simp
have D2: "P ⊢ [Nt A] ⇒* map Tm zt"
using derives_fringe_if_parse_tree[OF "4.prems"(2)] "4.prems"(4) rt by simp
show ?thesis using D1 D2 lenzt
by (metis append.right_neutral append_Nil list.size(3))
next
case False
hence "A ∈ set (bspine t1 ?ms1) ∨ A ∈ set (bspine t2 ?ms2)"
using "4.prems"(5) by (auto simp: Let_def split: if_splits)
thus ?thesis using recL recR by blast
qed
qed simp_all
text ‹Descend the heavy path to the ∗‹lowest› repeated branch-point label, lifting the
decomposition through each CNF node. When the heavy child's spine is already distinct, the
repeat is the current label, and the bound ‹2 ^ (card (Nts P) + 1)› holds because a distinct
spine has at most ‹card (Nts P)› labels.›
lemma :
"⟦ cnf_tree t; parse_tree P t; length ms = length (fringe t); fringe t = map Tm zt;
finite P; ¬ distinct (bspine t ms) ⟧ ⟹
∃A u v w x y du dv dw dx dy. A ∈ Nts P ∧
zt = u @ v @ w @ x @ y ∧ ms = du @ dv @ dw @ dx @ dy ∧
length du = length u ∧ length dv = length v ∧ length dw = length w ∧
length dx = length x ∧ length dy = length y ∧
P ⊢ [root t] ⇒* map Tm u @ [Nt A] @ map Tm y ∧
P ⊢ [Nt A] ⇒* map Tm v @ [Nt A] @ map Tm x ∧
P ⊢ [Nt A] ⇒* map Tm w ∧
1 ≤ dcount (dv @ dx) ∧ dcount (dv @ dw @ dx) ≤ 2 ^ (card (Nts P) + 1)"
proof (induction t arbitrary: ms zt rule: cnf_tree.induct)
case (4 A0 t1 t2 ms zt)
from "4.prems"(1) obtain B C where rB: "root t1 = Nt B" and rC: "root t2 = Nt C"
and ct1: "cnf_tree t1" and ct2: "cnf_tree t2" by auto
from "4.prems"(2) have pt1: "parse_tree P t1" and pt2: "parse_tree P t2"
and inP: "(A0, [root t1, root t2]) ∈ P" by auto
have inP': "(A0, [Nt B, Nt C]) ∈ P" using inP rB rC by simp
have A0Nts: "A0 ∈ Nts P" using inP by (auto simp: Nts_def)
let ?n1 = "length (fringe t1)"
let ?ms1 = "take ?n1 ms"
let ?ms2 = "drop ?n1 ms"
have len: "length ms = length (fringe t1) + length (fringe t2)" using "4.prems"(3) by simp
have l1: "length ?ms1 = length (fringe t1)" and l2: "length ?ms2 = length (fringe t2)"
using len by auto
have msplit: "ms = ?ms1 @ ?ms2" by simp
from "4.prems"(4) have "map Tm zt = fringe t1 @ fringe t2" by simp
then obtain z1 z2 where z1: "fringe t1 = map Tm z1" and z2: "fringe t2 = map Tm z2"
and zt: "zt = z1 @ z2" by (auto simp: map_eq_append_conv)
have dB: "P ⊢ [Nt B] ⇒* map Tm z1" using derives_fringe_if_parse_tree[OF pt1] rB z1 by simp
have dC: "P ⊢ [Nt C] ⇒* map Tm z2" using derives_fringe_if_parse_tree[OF pt2] rC z2 by simp
have recurseL: ?case if D: "¬ distinct (bspine t1 ?ms1)"
proof -
from "4.IH"(1)[OF ct1 pt1 l1 z1 "4.prems"(5) D] obtain A u1 v1 w1 x1 y1 du1 dv1 dw1 dx1 dy1
where Q: "A ∈ Nts P" "z1 = u1 @ v1 @ w1 @ x1 @ y1" "?ms1 = du1 @ dv1 @ dw1 @ dx1 @ dy1"
"length du1 = length u1" "length dv1 = length v1" "length dw1 = length w1"
"length dx1 = length x1" "length dy1 = length y1"
"P ⊢ [root t1] ⇒* map Tm u1 @ [Nt A] @ map Tm y1"
"P ⊢ [Nt A] ⇒* map Tm v1 @ [Nt A] @ map Tm x1" "P ⊢ [Nt A] ⇒* map Tm w1"
"1 ≤ dcount (dv1 @ dx1)" "dcount (dv1 @ dw1 @ dx1) ≤ 2 ^ (card (Nts P) + 1)" by blast
have dBu: "P ⊢ [Nt B] ⇒* map Tm u1 @ [Nt A] @ map Tm y1" using Q(9) rB by simp
have "P ⊢ [Nt A0] ⇒* (map Tm u1 @ [Nt A] @ map Tm y1) @ map Tm z2"
by (rule derives_bin[OF inP' dBu dC])
hence d: "P ⊢ [Nt A0] ⇒* map Tm u1 @ [Nt A] @ map Tm (y1 @ z2)" by simp
have "A ∈ Nts P ∧ zt = u1 @ v1 @ w1 @ x1 @ (y1 @ z2) ∧
ms = du1 @ dv1 @ dw1 @ dx1 @ (dy1 @ ?ms2) ∧
length du1 = length u1 ∧ length dv1 = length v1 ∧ length dw1 = length w1 ∧
length dx1 = length x1 ∧ length (dy1 @ ?ms2) = length (y1 @ z2) ∧
P ⊢ [root (Prod A0 [t1,t2])] ⇒* map Tm u1 @ [Nt A] @ map Tm (y1 @ z2) ∧
P ⊢ [Nt A] ⇒* map Tm v1 @ [Nt A] @ map Tm x1 ∧ P ⊢ [Nt A] ⇒* map Tm w1 ∧
1 ≤ dcount (dv1 @ dx1) ∧ dcount (dv1 @ dw1 @ dx1) ≤ 2 ^ (card (Nts P) + 1)"
using Q zt z2 l2 d msplit by simp
thus ?case by blast
qed
have recurseR: ?case if D: "¬ distinct (bspine t2 ?ms2)"
proof -
from "4.IH"(2)[OF ct2 pt2 l2 z2 "4.prems"(5) D] obtain A u2 v2 w2 x2 y2 du2 dv2 dw2 dx2 dy2
where Q: "A ∈ Nts P" "z2 = u2 @ v2 @ w2 @ x2 @ y2" "?ms2 = du2 @ dv2 @ dw2 @ dx2 @ dy2"
"length du2 = length u2" "length dv2 = length v2" "length dw2 = length w2"
"length dx2 = length x2" "length dy2 = length y2"
"P ⊢ [root t2] ⇒* map Tm u2 @ [Nt A] @ map Tm y2"
"P ⊢ [Nt A] ⇒* map Tm v2 @ [Nt A] @ map Tm x2" "P ⊢ [Nt A] ⇒* map Tm w2"
"1 ≤ dcount (dv2 @ dx2)" "dcount (dv2 @ dw2 @ dx2) ≤ 2 ^ (card (Nts P) + 1)" by blast
have dCu: "P ⊢ [Nt C] ⇒* map Tm u2 @ [Nt A] @ map Tm y2" using Q(9) rC by simp
have "P ⊢ [Nt A0] ⇒* map Tm z1 @ (map Tm u2 @ [Nt A] @ map Tm y2)"
by (rule derives_bin[OF inP' dB dCu])
hence d: "P ⊢ [Nt A0] ⇒* map Tm (z1 @ u2) @ [Nt A] @ map Tm y2" by simp
have "A ∈ Nts P ∧ zt = (z1 @ u2) @ v2 @ w2 @ x2 @ y2 ∧
ms = (?ms1 @ du2) @ dv2 @ dw2 @ dx2 @ dy2 ∧
length (?ms1 @ du2) = length (z1 @ u2) ∧ length dv2 = length v2 ∧
length dw2 = length w2 ∧ length dx2 = length x2 ∧ length dy2 = length y2 ∧
P ⊢ [root (Prod A0 [t1,t2])] ⇒* map Tm (z1 @ u2) @ [Nt A] @ map Tm y2 ∧
P ⊢ [Nt A] ⇒* map Tm v2 @ [Nt A] @ map Tm x2 ∧ P ⊢ [Nt A] ⇒* map Tm w2 ∧
1 ≤ dcount (dv2 @ dx2) ∧ dcount (dv2 @ dw2 @ dx2) ≤ 2 ^ (card (Nts P) + 1)"
using Q zt z1 l1 d msplit by simp
thus ?case by blast
qed
have top: ?case
if heavy: "bspine (Prod A0 [t1,t2]) ms = A0 # bspine tc mc"
and DI: "distinct (bspine tc mc)" and AIN: "A0 ∈ set (bspine tc mc)"
and tc: "tc = t1 ∧ mc = ?ms1 ∧ od = ?ms2 ∧ co = z2 ∨ tc = t2 ∧ mc = ?ms2 ∧ od = ?ms1 ∧ co = z1"
and ctc: "cnf_tree tc" and ptc: "parse_tree P tc"
and lc: "length mc = length (fringe tc)" and zc: "fringe tc = map Tm zc"
and side: "0 < dcount od"
and ctxbin: "⋀v1 x1. P ⊢ [root tc] ⇒* map Tm v1 @ [Nt A0] @ map Tm x1
⟹ P ⊢ [Nt A0] ⇒* map Tm (v @ v1) @ [Nt A0] @ map Tm (x1 @ x)"
and split: "zt = v @ zc @ x ∧ ms = dv @ mc @ dx ∧ length dv = length v ∧ length dx = length x
∧ dcount (dv @ dx) = dcount od"
for tc mc od co zc v x dv dx
proof -
from ctx_label[OF ctc ptc lc zc AIN] obtain v1 w1 x1 dv1 dw1 dx1 where
Q: "zc = v1 @ w1 @ x1" "mc = dv1 @ dw1 @ dx1"
"length dv1 = length v1" "length dw1 = length w1" "length dx1 = length x1"
"P ⊢ [root tc] ⇒* map Tm v1 @ [Nt A0] @ map Tm x1" "P ⊢ [Nt A0] ⇒* map Tm w1" by blast
have dctx: "P ⊢ [Nt A0] ⇒* map Tm (v @ v1) @ [Nt A0] @ map Tm (x1 @ x)"
by (rule ctxbin[OF Q(6)])
have fin: "finite (Nts P)" using "4.prems"(5) by (rule finite_Nts)
have dwms: "dcount ((dv @ dv1) @ dw1 @ (dx1 @ dx)) = dcount ms"
using split Q(2) by (simp)
have bound: "dcount ms ≤ 2 ^ (card (Nts P) + 1)"
proof -
have "card (set (bspine tc mc)) ≤ card (Nts P)"
by (rule card_mono[OF fin bspine_in_Nts[OF ptc]])
hence le: "length (bspine tc mc) ≤ card (Nts P)" using DI distinct_card by fastforce
have "dcount ms ≤ 2 ^ length (bspine (Prod A0 [t1,t2]) ms)"
by (rule dcount_le_pow_bspine[OF "4.prems"(1) "4.prems"(3)])
also have "… = 2 ^ (length (bspine tc mc) + 1)" using heavy by simp
also have "… ≤ 2 ^ (card (Nts P) + 1)" using le by simp
finally show ?thesis .
qed
have sidefull: "1 ≤ dcount ((dv @ dv1) @ (dx1 @ dx))"
using less_eq_Suc_le side split by auto
have "A0 ∈ Nts P ∧ zt = (v @ v1) @ w1 @ (x1 @ x) @ [] ∧
ms = (dv @ dv1) @ dw1 @ (dx1 @ dx) @ [] ∧
length (dv @ dv1) = length (v @ v1) ∧ length dw1 = length w1 ∧
length (dx1 @ dx) = length (x1 @ x) ∧ length ([]::bool list) = length ([]::'b list) ∧
P ⊢ [root (Prod A0 [t1,t2])] ⇒* map Tm [] @ [Nt A0] @ map Tm [] ∧
P ⊢ [Nt A0] ⇒* map Tm (v @ v1) @ [Nt A0] @ map Tm (x1 @ x) ∧
P ⊢ [Nt A0] ⇒* map Tm w1 ∧
1 ≤ dcount ((dv @ dv1) @ (dx1 @ dx)) ∧
dcount ((dv @ dv1) @ dw1 @ (dx1 @ dx)) ≤ 2 ^ (card (Nts P) + 1)"
using A0Nts split Q(1) Q(2) Q(3) Q(4) Q(5) dctx Q(7) sidefull dwms bound by simp
thus ?case by blast
qed
show ?case
proof (cases "0 < dcount ?ms1 ∧ 0 < dcount ?ms2")
case bpc: True
show ?thesis
proof (cases "dcount ?ms2 ≤ dcount ?ms1")
case hl: True
have sp: "bspine (Prod A0 [t1,t2]) ms = A0 # bspine t1 ?ms1" using bpc hl by (simp add: Let_def)
show ?thesis
proof (cases "distinct (bspine t1 ?ms1)")
case True
hence AIN: "A0 ∈ set (bspine t1 ?ms1)" using "4.prems"(6) sp by auto
show ?thesis
proof (rule top[where tc = t1 and mc = ?ms1 and od = ?ms2 and co = z2 and zc = z1
and v = "[]" and x = z2 and dv = "[]" and dx = ?ms2])
show "⋀v1 x1. P ⊢ [root t1] ⇒* map Tm v1 @ [Nt A0] @ map Tm x1
⟹ P ⊢ [Nt A0] ⇒* map Tm ([] @ v1) @ [Nt A0] @ map Tm (x1 @ z2)"
proof -
fix v1 x1 assume "P ⊢ [root t1] ⇒* map Tm v1 @ [Nt A0] @ map Tm x1"
hence "P ⊢ [Nt B] ⇒* map Tm v1 @ [Nt A0] @ map Tm x1" using rB by simp
from derives_bin[OF inP' this dC]
show "P ⊢ [Nt A0] ⇒* map Tm ([] @ v1) @ [Nt A0] @ map Tm (x1 @ z2)" by simp
qed
show "zt = [] @ z1 @ z2 ∧ ms = [] @ ?ms1 @ ?ms2 ∧ length ([]::bool list) = length ([]::'b list)
∧ length ?ms2 = length z2 ∧ dcount ([] @ ?ms2) = dcount ?ms2"
using zt msplit l2 z2 by simp
show "0 < dcount ?ms2" using bpc by simp
qed (use sp True AIN ct1 pt1 l1 z1 in simp_all)
next
case False thus ?thesis by (rule recurseL)
qed
next
case hr: False
have sp: "bspine (Prod A0 [t1,t2]) ms = A0 # bspine t2 ?ms2" using bpc hr by (simp add: Let_def)
show ?thesis
proof (cases "distinct (bspine t2 ?ms2)")
case True
hence AIN: "A0 ∈ set (bspine t2 ?ms2)" using "4.prems"(6) sp by auto
show ?thesis
proof (rule top[where tc = t2 and mc = ?ms2 and od = ?ms1 and co = z1 and zc = z2
and v = z1 and x = "[]" and dv = ?ms1 and dx = "[]"])
show "⋀v1 x1. P ⊢ [root t2] ⇒* map Tm v1 @ [Nt A0] @ map Tm x1
⟹ P ⊢ [Nt A0] ⇒* map Tm (z1 @ v1) @ [Nt A0] @ map Tm (x1 @ [])"
proof -
fix v1 x1 assume "P ⊢ [root t2] ⇒* map Tm v1 @ [Nt A0] @ map Tm x1"
hence "P ⊢ [Nt C] ⇒* map Tm v1 @ [Nt A0] @ map Tm x1" using rC by simp
from derives_bin[OF inP' dB this]
show "P ⊢ [Nt A0] ⇒* map Tm (z1 @ v1) @ [Nt A0] @ map Tm (x1 @ [])" by simp
qed
show "zt = z1 @ z2 @ [] ∧ ms = ?ms1 @ ?ms2 @ [] ∧ length ?ms1 = length z1
∧ length ([]::bool list) = length ([]::'b list) ∧ dcount (?ms1 @ []) = dcount ?ms1"
using zt msplit l1 z1 by simp
show "0 < dcount ?ms1" using bpc by simp
qed (use sp True AIN ct2 pt2 l2 z2 in simp_all)
next
case False thus ?thesis by (rule recurseR)
qed
qed
next
case nbp: False
show ?thesis
proof (cases "0 < dcount ?ms1")
case True thus ?thesis
using "4.prems"(6) nbp recurseL by auto
next
case False thus ?thesis
using "4.prems"(6) recurseR by fastforce
qed
qed
qed simp_all
subsection ‹The combinatorial core: extracting a pumpable nonterminal›
text ‹❙‹The heart of Ogden's lemma› (Hopcroft \& Ullman, Ch.\ 6). Given a CNF grammar and a
marking with at least ‹2 ^ (card (Nts P) + 1)› distinguished positions, we extract a
nonterminal ‹A› and a decomposition ‹z = u v w x y› together with the three derivations that
drive the pumping, plus the two marking conditions.
❙‹Proof.› From \<^prop>‹z ∈ Lang P S› take a parse tree ‹t› (via @{thm [source] parse_tree_if_derives});
it is a \<^const>‹cnf_tree› by ‹cnf_tree_if_parse_tree›. By ‹dcount_le_pow_bspine›,
\<^prop>‹dcount ds ≤ 2 ^ length (bspine t ds)›, so with ‹big› the heavy path carries more than
‹card (Nts P)› branch-point labels; since these lie in ‹Nts P› (‹bspine_in_Nts›) and ‹Nts P›
has only ‹card (Nts P)› elements, the spine ‹bspine t ds› cannot be distinct. The branch-point
extraction ‹ogden_extract› then descends the heavy path to the ❙‹lowest› repeated label,
reading off the decomposition together with \<^prop>‹1 ≤ dcount (dv @ dx)› and the bound
\<^prop>‹dcount (dv @ dw @ dx) ≤ 2 ^ (card (Nts P) + 1)› (the latter because the child spine below
the repeat is distinct, hence of length ‹≤ card (Nts P)›). Finally \<^prop>‹root t = Nt S› turns
the extracted context derivation into one from ‹[Nt S]›.›
lemma ogden_split:
assumes P: "CNF P" "finite P" and z: "z ∈ Lang P S"
and ds: "length ds = length z"
and big: "2 ^ (card (Nts P) + 1) ≤ dcount ds"
shows "∃A u v w x y du dv dw dx dy.
A ∈ Nts P ∧
z = u @ v @ w @ x @ y ∧ ds = du @ dv @ dw @ dx @ dy ∧
length du = length u ∧ length dv = length v ∧ length dw = length w ∧
length dx = length x ∧ length dy = length y ∧
P ⊢ [Nt S] ⇒* map Tm u @ [Nt A] @ map Tm y ∧
P ⊢ [Nt A] ⇒* map Tm v @ [Nt A] @ map Tm x ∧
P ⊢ [Nt A] ⇒* map Tm w ∧
1 ≤ dcount (dv @ dx) ∧
dcount (dv @ dw @ dx) ≤ 2 ^ (card (Nts P) + 1)"
proof -
from z have derz: "P ⊢ [Nt S] ⇒* map Tm z" by (simp add: Lang_def)
from parse_tree_if_derives[OF derz]
obtain t where t: "parse_tree P t ∧ fringe t = map Tm z ∧ root t = Nt S" ..
hence pt: "parse_tree P t" and fr: "fringe t = map Tm z" and rt: "root t = Nt S" by auto
have ct: "cnf_tree t" by (rule cnf_tree_if_parse_tree[OF P(1) pt fr])
have len: "length ds = length (fringe t)" using ds fr by simp
have dpow: "dcount ds ≤ 2 ^ length (bspine t ds)" by (rule dcount_le_pow_bspine[OF ct len])
have nd: "¬ distinct (bspine t ds)"
proof
assume D: "distinct (bspine t ds)"
have "length (bspine t ds) = card (set (bspine t ds))" using D by (simp add: distinct_card)
also have "… ≤ card (Nts P)"
by (rule card_mono[OF finite_Nts[OF P(2)] bspine_in_Nts[OF pt]])
finally have le: "length (bspine t ds) ≤ card (Nts P)" .
have "(2::nat) ^ (card (Nts P) + 1) ≤ dcount ds" using big .
also have "dcount ds ≤ 2 ^ length (bspine t ds)" using dpow .
also have "… ≤ 2 ^ card (Nts P)" by (rule power_increasing[OF le]) simp
finally show False by simp
qed
from ogden_extract[OF ct pt len fr P(2) nd]
obtain A u v w x y du dv dw dx dy where
Q: "A ∈ Nts P" "z = u @ v @ w @ x @ y" "ds = du @ dv @ dw @ dx @ dy"
"length du = length u" "length dv = length v" "length dw = length w"
"length dx = length x" "length dy = length y"
"P ⊢ [root t] ⇒* map Tm u @ [Nt A] @ map Tm y"
"P ⊢ [Nt A] ⇒* map Tm v @ [Nt A] @ map Tm x"
"P ⊢ [Nt A] ⇒* map Tm w"
"1 ≤ dcount (dv @ dx)" "dcount (dv @ dw @ dx) ≤ 2 ^ (card (Nts P) + 1)"
by blast
have S: "P ⊢ [Nt S] ⇒* map Tm u @ [Nt A] @ map Tm y" using Q(9) rt by simp
show ?thesis using Q S by blast
qed
subsection ‹Derivation-level pumping›
text ‹Once the nonterminal ‹A› and its contexts have been extracted, the actual pumping is a
pure derivation argument with no further reference to parse trees, exactly as in the
inherent-ambiguity development.›
lemma pump_derives:
assumes S: "P ⊢ [Nt S] ⇒* map Tm u @ [Nt A] @ map Tm y"
and V: "P ⊢ [Nt A] ⇒* map Tm v @ [Nt A] @ map Tm x"
and W: "P ⊢ [Nt A] ⇒* map Tm w"
shows "u @ v ^^ i @ w @ x ^^ i @ y ∈ Lang P S"
proof -
have inner: "P ⊢ [Nt A] ⇒* map Tm (v ^^ i) @ [Nt A] @ map Tm (x ^^ i)" for i
proof (induction i)
case 0 show ?case by simp
next
case (Suc i)
have "P ⊢ [Nt A] ⇒* map Tm (v ^^ i) @ (map Tm v @ [Nt A] @ map Tm x) @ map Tm (x ^^ i)"
using Suc.IH derives_embed[OF V, of "map Tm (v ^^ i)" "map Tm (x ^^ i)"]
by (meson rtranclp_trans)
thus ?case
by (metis append.assoc map_append pow_list_Suc pow_list_Suc2)
qed
have mid: "P ⊢ [Nt A] ⇒* map Tm (v ^^ i) @ map Tm w @ map Tm (x ^^ i)"
using inner derives_embed[OF W, of "map Tm (v ^^ i)" "map Tm (x ^^ i)"]
by (meson rtranclp_trans)
have "P ⊢ [Nt S] ⇒* map Tm u @ (map Tm (v ^^ i) @ map Tm w @ map Tm (x ^^ i)) @ map Tm y"
using S derives_embed[OF mid, of "map Tm u" "map Tm y"]
by (meson rtranclp_trans)
hence "P ⊢ [Nt S] ⇒* map Tm (u @ v ^^ i @ w @ x ^^ i @ y)"
by simp
thus ?thesis by (simp add: Lang_def)
qed
subsection ‹Assembling Ogden's lemma›
text ‹The ``inner'' Ogden lemma for a CNF grammar: ‹2 ^ (card (Nts P) + 1)› distinguished
positions force a marked pumpable decomposition.›
lemma inner_ogden:
assumes P: "CNF P" "finite P" and z: "z ∈ Lang P S"
and ds: "length ds = length z"
and big: "2 ^ (card (Nts P) + 1) ≤ dcount ds"
shows "∃u v w x y du dv dw dx dy.
z = u @ v @ w @ x @ y ∧ ds = du @ dv @ dw @ dx @ dy ∧
length du = length u ∧ length dv = length v ∧ length dw = length w ∧
length dx = length x ∧ length dy = length y ∧
1 ≤ dcount (dv @ dx) ∧ dcount (dv @ dw @ dx) ≤ 2 ^ (card (Nts P) + 1) ∧
(∀i. u @ v ^^ i @ w @ x ^^ i @ y ∈ Lang P S)"
proof -
from ogden_split[OF P z ds big] obtain A u v w x y du dv dw dx dy where
sp: "z = u @ v @ w @ x @ y" "ds = du @ dv @ dw @ dx @ dy"
"length du = length u" "length dv = length v" "length dw = length w"
"length dx = length x" "length dy = length y"
"P ⊢ [Nt S] ⇒* map Tm u @ [Nt A] @ map Tm y"
"P ⊢ [Nt A] ⇒* map Tm v @ [Nt A] @ map Tm x"
"P ⊢ [Nt A] ⇒* map Tm w"
"1 ≤ dcount (dv @ dx)" "dcount (dv @ dw @ dx) ≤ 2 ^ (card (Nts P) + 1)"
by blast
have "∀i. u @ v ^^ i @ w @ x ^^ i @ y ∈ Lang P S"
using pump_derives[OF sp(8) sp(9) sp(10)] by blast
with sp show ?thesis by blast
qed
text ‹\<^term>‹ogden_property L n› is the conclusion of Ogden's lemma for a language ‹L› with
constant ‹n›: any word marked in ‹n› or more positions splits as ‹u v w x y› with the marking
conditions and the pumping property. The marking is carried as a boolean list parallel to the
word; ‹dv @ dx› and ‹dv @ dw @ dx› are the markings of ‹v x› and ‹v w x›.›
abbreviation ogden_property :: "'t list set ⇒ nat ⇒ bool" where
"ogden_property L n ≡
(∀z ∈ L. ∀ds. length ds = length z ∧ n ≤ dcount ds ⟶
(∃u v w x y du dv dw dx dy.
z = u @ v @ w @ x @ y ∧ ds = du @ dv @ dw @ dx @ dy ∧
length du = length u ∧ length dv = length v ∧ length dw = length w ∧
length dx = length x ∧ length dy = length y ∧
1 ≤ dcount (dv @ dx) ∧ dcount (dv @ dw @ dx) ≤ n ∧
(∀i. u @ v ^^ i @ w @ x ^^ i @ y ∈ L)))"
theorem Ogden_Lemma_CNF:
assumes "CNF P" "finite P"
shows "∃n. ogden_property (Lang P S) n"
proof
show "ogden_property (Lang P S) (2 ^ (card (Nts P) + 1))"
using inner_ogden[OF assms] by blast
qed
text ‹For an arbitrary (finite) grammar we pass to a CNF grammar with the same language modulo
the empty word (@{thm [source] cnf_exists}); the empty word carries no marks, so bumping the
constant by one excludes it, exactly as in ‹Pumping_Lemma›.›
theorem Ogden_Lemma:
assumes "finite (P :: ('n::fresh0,'t) Prods)"
shows "∃n. ogden_property (Lang P S) n"
proof -
obtain P' :: "('n,'t) Prods" where P':
"finite P'" "CNF P'" "Lang P' S = Lang P S - {[]}"
using cnf_exists[OF assms] by blast
from Ogden_Lemma_CNF[OF P'(2) P'(1)]
obtain n where n: "ogden_property (Lang P' S) n" ..
have "ogden_property (Lang P S) (Suc n)"
proof (intro ballI allI impI)
fix z ds assume z: "z ∈ Lang P S" and m: "length ds = length z ∧ Suc n ≤ dcount ds"
from m have lz: "length ds = length z" and dc: "Suc n ≤ dcount ds" by auto
have "0 < length z" using dc lz count_le_length[of ds True] by linarith
hence "z ≠ []" by auto
with z P'(3) have z': "z ∈ Lang P' S" by simp
have prem: "length ds = length z ∧ n ≤ dcount ds" using lz dc by simp
from bspec[OF n z', rule_format, OF prem]
obtain u v w x y du dv dw dx dy where o:
"z = u @ v @ w @ x @ y" "ds = du @ dv @ dw @ dx @ dy"
"length du = length u" "length dv = length v" "length dw = length w"
"length dx = length x" "length dy = length y"
"1 ≤ dcount (dv @ dx)" "dcount (dv @ dw @ dx) ≤ n"
"∀i. u @ v ^^ i @ w @ x ^^ i @ y ∈ Lang P' S"
by blast
have pumpP: "∀i. u @ v ^^ i @ w @ x ^^ i @ y ∈ Lang P S"
using o(10) by (auto simp: P'(3))
have le: "dcount (dv @ dw @ dx) ≤ Suc n" using o(9) by linarith
show "∃u v w x y du dv dw dx dy.
z = u @ v @ w @ x @ y ∧ ds = du @ dv @ dw @ dx @ dy ∧
length du = length u ∧ length dv = length v ∧ length dw = length w ∧
length dx = length x ∧ length dy = length y ∧
1 ≤ dcount (dv @ dx) ∧ dcount (dv @ dw @ dx) ≤ Suc n ∧
(∀i. u @ v ^^ i @ w @ x ^^ i @ y ∈ Lang P S)"
using o le pumpP by blast
qed
thus ?thesis by blast
qed
end