Theory CYK

(* Title:      A formalisation of the Cocke-Younger-Kasami algorithm
   Author:     Maksym Bortin <Maksym.Bortin@nicta.com.au>
*)


theory CYK
imports Main 
begin

text ‹The theory is structured as follows. First section deals with modelling
      of grammars, derivations, and the language semantics. Then the basic 
      properties are proved. Further, CYK is abstractly specified and its 
      underlying recursive relationship proved. The final section contains a 
      prototypical implementation accompanied by a proof of its correctness.›




section "Basic modelling"

subsection "Grammars in Chomsky normal form"

text "A grammar in Chomsky normal form is here simply modelled  
      by a list of production rules (the type CNG below), each having a non-terminal 
      symbol on the lhs and either two non-terminals or one terminal 
      symbol on the rhs."

datatype ('n, 't) RHS = Branch 'n 'n
                      | Leaf 't 

type_synonym ('n, 't) CNG = "('n × ('n, 't) RHS) list"

text "Abbreviating the list append symbol for better readability"
abbreviation list_append :: "'a list ⇒ 'a list ⇒ 'a list" (infixr "⋅" 65)
where "xs ⋅ ys ≡ xs @ ys"


subsection "Derivation by grammars"

text‹A \emph{word form} (or sentential form) may be built of both non-terminal and terminal 
       symbols, as opposed to a \emph{word} that contains only terminals. By the usage of disjoint 
       union, non-terminals are injected into a word form by @{term "Inl"} whereas terminals -- 
       by @{term "Inr"}.›
type_synonym ('n, 't) word_form = "('n + 't) list"
type_synonym 't word = "'t list"


text "A single step derivation relation on word forms is induced by a grammar in the standard way,
      replacing a non-terminal within a word form in accordance to the production rules."
definition DSTEP :: "('n, 't) CNG ⇒ (('n, 't) word_form × ('n, 't) word_form) set"
where "DSTEP G = {(l ⋅ [Inl N] ⋅ r, x) | l N r rhs x. (N, rhs) ∈ set G ∧ 
                                     (case rhs of
                                       Branch A B ⇒ x = l ⋅ [Inl A, Inl B] ⋅ r
                                     | Leaf t ⇒ x = l ⋅ [Inr t] ⋅ r)}"

abbreviation DSTEP'  :: "('n, 't) word_form ⇒ ('n, 't) CNG ⇒ ('n, 't) word_form ⇒ bool" ("_ -_→ _" [60, 61, 60] 61) 
where "w -G→ w' ≡ (w, w') ∈ DSTEP G"

abbreviation DSTEP_reflc  :: "('n, 't) word_form ⇒ ('n, 't) CNG ⇒ ('n, 't) word_form ⇒ bool" ("_ -_→⇧= _" [60, 61, 60] 61) 
where "w -G→⇧= w' ≡ (w, w') ∈ (DSTEP G)⇧="

abbreviation DSTEP_transc  :: "('n, 't) word_form ⇒ ('n, 't) CNG ⇒ ('n, 't) word_form ⇒ bool" ("_ -_→⇧+ _" [60, 61, 60] 61) 
where "w -G→⇧+ w' ≡ (w, w') ∈ (DSTEP G)⇧+"


abbreviation DSTEP_rtransc  :: "('n, 't) word_form ⇒ ('n, 't) CNG ⇒ ('n, 't) word_form ⇒ bool" ("_ -_→⇧* _" [60, 61, 60] 61) 
where "w -G→⇧* w' ≡ (w, w') ∈ (DSTEP G)⇧*"




subsection "The generated language semantics"

text "The language generated by a grammar from a non-terminal symbol 
      comprises all words that can be derived from the non-terminal 
      in one or more steps.
      Notice that by the presented grammar modelling, languages containing 
      the empty word cannot be generated. Hence in rare situations when such 
      languages are required, the empty word case should be treated separately."
definition Lang :: "('n, 't) CNG ⇒ 'n ⇒ 't word set"
where "Lang G S = {w. [Inl S] -G→⇧+ map Inr w }" 


text‹So, for instance, a grammar generating the language $a^nb^n$  
       from the non-terminal @{term "''S''"} might look as follows.›
definition "G_anbn = 
[(''S'', Branch ''A'' ''T''),
 (''S'', Branch ''A'' ''B''),
 (''T'', Branch ''S'' ''B''),
 (''A'', Leaf ''a''),
 (''B'', Leaf ''b'')]"

text‹Now the term @{term "Lang G_anbn ''S''"} denotes the set of words of
       the form $a^nb^n$ with $n > 0$. This is intuitively clear, but not 
       straight forward to show, and a lengthy proof for that is out of scope.›



section "Basic properties"


lemma prod_into_DSTEP1 :
"(S, Branch A B) ∈ set G ⟹
 L ⋅ [Inl S] ⋅ R -G→ L ⋅ [Inl A, Inl B] ⋅ R"
by(simp add: DSTEP_def, rule_tac x="L" in exI, force)


lemma prod_into_DSTEP2 :
"(S, Leaf a) ∈ set G ⟹
 L ⋅ [Inl S] ⋅ R -G→ L ⋅ [Inr a] ⋅ R"
by(simp add: DSTEP_def, rule_tac x="L" in exI, force)




lemma DSTEP_D :
"s -G→ t ⟹ 
 ∃L N R rhs. s = L ⋅ [Inl N] ⋅ R ∧ (N, rhs) ∈ set G ∧ 
 (∀A B. rhs = Branch A B ⟶ t = L ⋅ [Inl A, Inl B] ⋅ R) ∧
 (∀x. rhs = Leaf x ⟶ t = L ⋅ [Inr x] ⋅ R)"
by(unfold DSTEP_def, clarsimp, simp split: RHS.split_asm, blast+)


lemma DSTEP_append :
assumes a: "s -G→ t"
shows "L  ⋅  s  ⋅  R -G→ L  ⋅  t  ⋅  R"
proof -
 from a have "∃l N r rhs. s = l ⋅ [Inl N] ⋅ r ∧ (N, rhs) ∈ set G ∧ 
                         (∀A B. rhs = Branch A B ⟶ t = l ⋅ [Inl A, Inl B] ⋅ r) ∧
                         (∀x. rhs = Leaf x ⟶ t = l ⋅ [Inr x] ⋅ r)" (is "∃l N r rhs. ?P l N r rhs")
 by(rule DSTEP_D)
 then obtain l N r rhs where "?P l N r rhs" by blast
 thus ?thesis
 by(simp add: DSTEP_def, rule_tac x="L ⋅ l" in exI,
    rule_tac x=N in exI, rule_tac x="r ⋅ R" in exI,
    simp, rule_tac x=rhs in exI, simp split: RHS.split)
qed
  


lemma DSTEP_star_mono :
"s -G→⇧* t ⟹ length s ≤ length t"
proof(erule rtrancl_induct, simp)
 fix t u 
 assume "s -G→⇧* t"
 assume a: "t -G→ u"
 assume b: "length s ≤ length t"
 show "length s ≤ length u"
 proof -
  from a have "∃L N R rhs. t = L ⋅ [Inl N] ⋅ R ∧ (N, rhs) ∈ set G ∧ 
                          (∀A B. rhs = Branch A B ⟶ u = L ⋅ [Inl A, Inl B] ⋅ R) ∧
                          (∀x. rhs = Leaf x ⟶ u = L ⋅ [Inr x] ⋅ R)" (is "∃L N R rhs. ?P L N R rhs")
  by(rule DSTEP_D)
  then obtain L N R rhs where "?P L N R rhs" by blast
  with b show ?thesis
  by(case_tac rhs, clarsimp+)
 qed
qed


lemma DSTEP_comp :
assumes a: "l ⋅ r -G→ t" 
shows "∃l' r'. l -G→⇧= l' ∧ r -G→⇧= r' ∧ t = l' ⋅ r'"
proof -
 from a have "∃L N R rhs. l ⋅ r = L ⋅ [Inl N] ⋅ R ∧ (N, rhs) ∈ set G ∧ 
                         (∀A B. rhs = Branch A B ⟶ t = L ⋅ [Inl A, Inl B] ⋅ R) ∧
                        (∀x. rhs = Leaf x ⟶ t = L ⋅ [Inr x] ⋅ R)" (is "∃L N R rhs. ?T L N R rhs")
 by(rule DSTEP_D)
 then obtain L N R rhs where b: "?T L N R rhs" by blast
 hence "l ⋅ r = L ⋅ Inl N # R" by simp
 hence "∃u. (l = L ⋅ u ∧ u ⋅ r = Inl N # R) ∨ (l ⋅ u = L ∧ r = u ⋅ Inl N # R)" by(rule append_eq_append_conv2[THEN iffD1])
 then obtain xs where c: "l = L ⋅ xs ∧ xs ⋅ r = Inl N # R ∨ l ⋅ xs = L ∧ r = xs  ⋅  Inl N # R" (is "?C1 ∨ ?C2") by blast
 show ?thesis
 proof(cases rhs)
    case (Leaf x)
    with b have d: "t = L ⋅ [Inr x] ⋅ R ∧ (N, Leaf x) ∈ set G" by simp
    from c show ?thesis
    proof
     assume e: "?C1"
     show ?thesis
     proof(cases xs)
      case Nil with d and e show ?thesis
      by(clarsimp, rule_tac x=L in exI, simp add: DSTEP_def, simp split: RHS.split, blast)
     next
      case (Cons z zs) with d and e show ?thesis
      by(rule_tac x="L ⋅ Inr x # zs" in exI, clarsimp, simp add: DSTEP_def, simp split: RHS.split, blast)
     qed
    next
     assume e: "?C2"
     show ?thesis
     proof(cases xs)
      case Nil with d and e show ?thesis
      by(rule_tac x=L in exI, clarsimp, simp add: DSTEP_def, simp split: RHS.split, blast)
     next
      case (Cons z zs) with d and e show ?thesis
      by(rule_tac x="l" in exI, clarsimp, simp add: DSTEP_def, simp split: RHS.split, 
         rule_tac x="z#zs" in exI, rule_tac x=N in exI, rule_tac x=R in exI, simp, rule_tac x="Leaf x" in exI, simp)
     qed
    qed
 next
    case (Branch A B)
    with b have d: "t = L ⋅ [Inl A, Inl B] ⋅ R ∧ (N, Branch A B) ∈ set G" by simp
    from c show ?thesis
    proof
     assume e: "?C1"
     show ?thesis
     proof(cases xs)
      case Nil with d and e show ?thesis
      by(clarsimp, rule_tac x=L in exI, simp add: DSTEP_def, simp split: RHS.split, blast)
     next
      case (Cons z zs) with d and e show ?thesis
      by(rule_tac x="L ⋅ [Inl A, Inl B] ⋅ zs" in exI, clarsimp, simp add: DSTEP_def, simp split: RHS.split, blast)
     qed
    next
     assume e: "?C2"
     show ?thesis
     proof(cases xs)
      case Nil with d and e show ?thesis
      by(rule_tac x=L in exI, clarsimp, simp add: DSTEP_def, simp split: RHS.split, blast)
     next
      case (Cons z zs) with d and e show ?thesis
      by(rule_tac x="l" in exI, clarsimp, simp add: DSTEP_def, simp split: RHS.split, 
         rule_tac x="z#zs" in exI, rule_tac x=N in exI, rule_tac x=R in exI, simp, rule_tac x="Branch A B" in exI, simp)
     qed
   qed
 qed
qed




theorem DSTEP_star_comp1 :
assumes A: "l ⋅ r -G→⇧* t" 
shows "∃l' r'. l -G→⇧* l' ∧ r -G→⇧* r' ∧ t = l' ⋅ r'"
proof -
 have "⋀s. s -G→⇧* t ⟹ 
       ∀l r. s = l ⋅ r ⟶ (∃l' r'. l -G→⇧* l' ∧ r -G→⇧* r' ∧ t = l' ⋅ r')" (is "⋀s. ?P s t ⟹ ?Q s t")
 proof(erule rtrancl_induct, force)
  fix s t u
  assume "?P s t"
  assume a: "t -G→ u"
  assume b: "?Q s t"
  show "?Q s u"
  proof(clarify)
   fix l r
   assume "s = l ⋅ r"
   with b have "∃l' r'. l -G→⇧* l' ∧ r -G→⇧* r' ∧ t = l' ⋅ r'" by simp
   then obtain l' r' where c: "l -G→⇧* l' ∧ r -G→⇧* r' ∧ t = l' ⋅ r'" by blast
   with a have "l' ⋅ r' -G→ u" by simp
   hence "∃l'' r''. l' -G→⇧=  l'' ∧ r' -G→⇧= r'' ∧ u = l'' ⋅ r''" by(rule DSTEP_comp)
   then obtain l'' r'' where "l' -G→⇧=  l'' ∧ r' -G→⇧= r'' ∧ u = l'' ⋅ r''" by blast
   hence "l' -G→⇧* l'' ∧ r' -G→⇧* r'' ∧ u = l'' ⋅ r''" by blast
   with c show "∃l' r'. l -G→⇧* l' ∧ r -G→⇧* r' ∧ u = l' ⋅ r'" 
   by(rule_tac x=l'' in exI, rule_tac x=r'' in exI, force)
  qed
 qed
with A show ?thesis by force
qed



theorem DSTEP_star_comp2 :
assumes A: "l -G→⇧* l'" 
    and B: "r -G→⇧* r'"
shows "l ⋅ r -G→⇧* l' ⋅ r'"
proof -
 have "l -G→⇧* l' ⟹ 
       ∀r r'. r -G→⇧* r' ⟶ l ⋅ r -G→⇧* l' ⋅ r'" (is "?P l l' ⟹ ?Q l l'")
 proof(erule rtrancl_induct)
  show "?Q l l"
  proof(clarify, erule rtrancl_induct, simp)
   fix r s t
   assume a: "s -G→ t"
   assume b: "l ⋅ r -G→⇧* l ⋅ s"
   show "l ⋅ r -G→⇧* l ⋅ t"
   proof -
    from a have "l ⋅ s -G→ l ⋅ t" by(drule_tac L=l and R="[]" in DSTEP_append, simp)
    with b show ?thesis by simp
   qed
  qed
 next
   fix s t
   assume a: "s -G→ t"
   assume b: "?Q l s"
   show "?Q l t"
   proof(clarsimp)
    fix r r'
    assume "r -G→⇧* r'"
    with b have c: "l ⋅ r -G→⇧* s ⋅ r'" by simp
    from a have "s ⋅ r' -G→ t ⋅ r'" by(drule_tac L="[]" and R=r' in DSTEP_append, simp)
    with c show "l ⋅ r -G→⇧* t ⋅ r'" by simp
   qed
  qed
 with A and B show ?thesis by simp
qed
   


lemma DSTEP_trancl_term :
assumes A: "[Inl S] -G→⇧+ t"
    and B: "Inr x ∈ set t" 
 shows "∃N. (N, Leaf x) ∈ set G"
proof -
 have "[Inl S] -G→⇧+ t ⟹ 
       ∀x. Inr x ∈ set t ⟶ (∃N. (N, Leaf x) ∈ set G)" (is "?P t ⟹ ?Q t")
 proof(erule trancl_induct)
  fix t 
  assume a: "[Inl S] -G→ t"
  show "?Q t"
  proof -
   from a have "∃rhs. (S, rhs) ∈ set G ∧ 
                      (∀A B. rhs = Branch A B ⟶ t = [Inl A, Inl B]) ∧
                      (∀x. rhs = Leaf x ⟶ t = [Inr x])" (is "∃rhs. ?P rhs")
   by(simp add: DSTEP_def, clarsimp, simp split: RHS.split_asm, case_tac l, force, simp,
      clarsimp, simp split: RHS.split_asm, case_tac l, force, simp)
   then obtain rhs where "?P rhs" by blast
   thus ?thesis
   by(case_tac rhs, clarsimp, force)
  qed
 next
  fix s t
  assume a: "s -G→ t"
  assume b: "?Q s"
  show "?Q t"
  proof -
   from a have "∃L N R rhs. s = L ⋅ [Inl N] ⋅ R ∧ (N, rhs) ∈ set G ∧ 
                         (∀A B. rhs = Branch A B ⟶ t = L ⋅ [Inl A, Inl B] ⋅ R) ∧
                         (∀x. rhs = Leaf x ⟶ t = L ⋅ [Inr x] ⋅ R)" (is "∃L N R rhs. ?P L N R rhs")
   by(rule DSTEP_D)
   then obtain L N R rhs where "?P L N R rhs" by blast
   with b show ?thesis
   by(case_tac rhs, clarsimp, force)
  qed
 qed
 with A and B show ?thesis by simp
qed




subsection "Properties of generated languages"


lemma Lang_no_Nil :
"w ∈ Lang G S ⟹ w ≠ []"
by(simp add: Lang_def, drule trancl_into_rtrancl, drule DSTEP_star_mono, force)


lemma Lang_rtrancl_eq :
"(w ∈ Lang G S) = [Inl S] -G→⇧* map Inr w"          (is "?L = (?p ∈ ?R⇧*)")
proof(simp add: Lang_def, rule iffI, erule trancl_into_rtrancl)
 assume "?p ∈ ?R⇧*"
 hence "?p ∈ (?R⇧+)⇧=" by(subst rtrancl_trancl_reflcl[THEN sym], assumption)
 hence "[Inl S] = map Inr w ∨ ?p ∈ ?R⇧+" by force
 thus "?p ∈ ?R⇧+" by(case_tac w, simp_all)
qed
 



lemma Lang_term :
"w ∈ Lang G S ⟹ 
 ∀x ∈ set w. ∃N. (N, Leaf x) ∈ set G"
by(clarsimp simp add: Lang_def, drule DSTEP_trancl_term, 
   simp, erule imageI, assumption)




lemma Lang_eq1 :
"([x] ∈ Lang G S) = ((S, Leaf x) ∈ set G)"
proof(simp add: Lang_def, rule iffI, subst (asm) trancl_unfold_left, clarsimp)
 fix t
 assume a: "[Inl S] -G→ t"
 assume b: "t -G→⇧* [Inr x]"
 note DSTEP_star_mono[OF b, simplified]
 hence c: "length t ≤ 1" by simp
 have "∃z. t = [z]"
 proof(cases t)
  assume "t = []"
  with b have d: "[] -G→⇧* [Inr x]" by simp
  have "⋀s. ([], s) ∈ (DSTEP G)⇧* ⟹ s = []"
  by(erule rtrancl_induct, simp_all, drule DSTEP_D, clarsimp)
  note this[OF d]
  thus ?thesis by simp
 next
  fix z zs
  assume "t = z#zs"
  with c show ?thesis by force
 qed
 with a have "∃z. (S, Leaf z) ∈ set G ∧ t = [Inr z]"
 by(clarsimp simp add: DSTEP_def, simp split: RHS.split_asm, case_tac l, simp_all) 
 with b show "(S, Leaf x) ∈ set G"
 proof(clarsimp)
  fix z
  assume c: "(S, Leaf z) ∈ set G"
  assume "[Inr z] -G→⇧* [Inr x]"
  hence "([Inr z], [Inr x]) ∈ ((DSTEP G)⇧+)⇧=" by simp
  hence "[Inr z] = [Inr x] ∨ [Inr z] -G→⇧+ [Inr x]" by force
  hence "x = z"
  proof
   assume "[Inr z] = [Inr x]" thus ?thesis by simp
  next
   assume "[Inr z] -G→⇧+ [Inr x]"
   hence "∃u. [Inr z] -G→ u ∧ u -G→⇧* [Inr x]" by(subst (asm) trancl_unfold_left, force)
   then obtain u where "[Inr z] -G→ u" by blast
   thus ?thesis by(clarsimp simp add: DSTEP_def, case_tac l, simp_all)
  qed
  with c show ?thesis by simp
 qed
next
 assume a: "(S, Leaf x) ∈ set G"
 show "[Inl S] -G→⇧+ [Inr x]"
 by(rule r_into_trancl, simp add: DSTEP_def, rule_tac x="[]" in exI,
    rule_tac x="S" in exI, rule_tac x="[]" in exI, simp, rule_tac x="Leaf x" in exI,
    simp add: a)
qed



theorem Lang_eq2 :
"(w ∈ Lang G S ∧ 1 < length w) = 
 (∃A B. (S, Branch A B) ∈ set G ∧ (∃l r. w = l ⋅ r ∧ l ∈ Lang G A ∧ r ∈ Lang G B))"  
(is "?L = ?R")
proof(rule iffI, clarify, subst (asm) Lang_def, simp, subst (asm) trancl_unfold_left, clarsimp)
  have map_Inr_split : "⋀xs. ∀zs w. map Inr w = xs ⋅ zs ⟶ 
                       (∃u v. w = u ⋅ v ∧ xs = map Inr u ∧ zs = map Inr v)" 
  by(induct_tac xs, simp, force)
  fix t
  assume a: "Suc 0 < length w"
  assume b: "[Inl S] -G→ t"
  assume c: "t -G→⇧* map Inr w"
  from b have  "∃A B. (S, Branch A B) ∈ set G ∧ t = [Inl A, Inl B]"
  proof(simp add: DSTEP_def, clarify, case_tac l, simp_all, simp split: RHS.split_asm, clarify)
   fix x
   assume "t = [Inr x]"
   with c have d: "[Inr x] -G→⇧* map Inr w"by simp
   have "⋀x s. [Inr x] -G→⇧* s ⟹ s = [Inr x]"
   by(erule rtrancl_induct, simp_all, drule DSTEP_D, clarsimp, case_tac L, simp_all)
   note this[OF d]
   hence "w = [x]" by(case_tac w, simp_all)
   with a show "False" by simp
  qed
  then obtain A B where d: "(S, Branch A B) ∈ set G ∧ t = [Inl A, Inl B]" by blast
  with c have e: "[Inl A] ⋅ [Inl B] -G→⇧* map Inr w" by simp
  note DSTEP_star_comp1[OF e]
  then obtain l' r' where e: "[Inl A] -G→⇧* l' ∧ [Inl B] -G→⇧* r' ∧ 
                              map Inr w = l'  ⋅  r'" by blast 
  note map_Inr_split[rule_format, OF e[THEN conjunct2, THEN conjunct2]]
  then obtain u v where f: "w = u ⋅ v ∧ l' = map Inr u ∧ r' = map Inr v" by blast
  with e have g: "[Inl A] -G→⇧* map Inr u ∧ [Inl B] -G→⇧* map Inr v" by simp
  show "?R"
  by(rule_tac x=A in exI, rule_tac x=B in exI, simp add: d,
     rule_tac x=u in exI, rule_tac x=v in exI, simp add: f,
     (subst Lang_rtrancl_eq)+, rule g)
 next
  assume "?R" 
  then obtain A B l r where a: "(S, Branch A B) ∈ set G ∧ w = l ⋅ r ∧ l ∈ Lang G A ∧ r ∈ Lang G B" by blast
  have "[Inl A] ⋅ [Inl B] -G→⇧* map Inr l ⋅ map Inr r"  
  by(rule DSTEP_star_comp2, subst Lang_rtrancl_eq[THEN sym], simp add: a,
     subst Lang_rtrancl_eq[THEN sym], simp add: a)
  hence b: "[Inl A] ⋅ [Inl B] -G→⇧* map Inr w" by(simp add: a)
  have c: "w ∈ Lang G S" 
  by(simp add: Lang_def, subst trancl_unfold_left, rule_tac b="[Inl A] ⋅ [Inl B]" in relcompI,
     simp add: DSTEP_def, rule_tac x="[]" in exI, rule_tac x="S" in exI, rule_tac x="[]" in exI,
     simp, rule_tac x="Branch A B" in exI, simp add:  a[THEN conjunct1], rule b)
  thus "?L"
  proof    
   show "1 < length w"
   proof(simp add: a, rule ccontr, drule leI)
    assume "length l + length r ≤ Suc 0"
    hence "l = [] ∨ r = []" by(case_tac l, simp_all)
    thus "False"
    proof
     assume "l = []" 
     with a have "[] ∈ Lang G A" by simp
     note Lang_no_Nil[OF this] 
     thus ?thesis by simp 
    next
     assume "r = []" 
     with a have "[] ∈ Lang G B" by simp
     note Lang_no_Nil[OF this] 
     thus ?thesis by simp 
    qed
   qed
 qed
qed




section "Abstract specification of CYK"

text "A subword of a word $w$, starting at the position $i$ 
      (first element is at the position $0$) and having the length $j$, is defined as follows." 
definition "subword w i j = take j (drop i w)"

text "Thus, to any subword of the given word $w$ CYK assigns all non-terminals
      from which this subword is derivable by the grammar $G$." 
definition "CYK G w i j = {S. subword w i j ∈ Lang G S}"



subsection ‹Properties of @{term "subword"}›

lemma subword_length :
"i + j ≤ length w ⟹ length(subword w i j) = j"
by(simp add: subword_def)


lemma subword_nth1 :
"i + j ≤ length w ⟹ k < j ⟹ 
(subword w i j)!k = w!(i + k)"
by(simp add: subword_def)


lemma subword_nth2 :
assumes A: "i + 1 ≤ length w" 
shows "subword w i 1 = [w!i]"
proof -
 note subword_length[OF A]
 hence "∃x. subword w i 1 = [x]" by(case_tac "subword w i 1", simp_all)
 then obtain x where a:"subword w i 1 = [x]" by blast
 note subword_nth1[OF A, where k="(0 :: nat)", simplified]
 with a have "x = w!i" by simp
 with a show ?thesis by simp
qed



lemma subword_self :
"subword w 0 (length w) = w"
by(simp add: subword_def)



lemma take_split[rule_format] :
"∀n m. n ≤ length xs ⟶ n ≤ m ⟶
 take n xs ⋅ take (m - n) (drop n xs) = take m xs"
by(induct_tac xs, clarsimp+, case_tac n, simp_all, case_tac m, simp_all)


lemma subword_split :
"i + j ≤ length w ⟹ 0 < k ⟹ k < j ⟹
 subword w i j = subword w i k ⋅ subword w (i + k) (j - k)"
by(simp add: subword_def, subst take_split[where n=k, THEN sym], simp_all,
   rule_tac f="λx. take (j - k) (drop x w)" in arg_cong, simp)


lemma subword_split2 :
assumes A: "subword w i j = l ⋅ r"
    and B: "i + j ≤ length w"
    and C: "0 < length l"
    and D: "0 < length r"
shows "l = subword w i (length l) ∧ r = subword w (i + length l) (j - length l)"
proof -
 have a: "length(subword w i j) = j" by(rule subword_length, rule B)
 note arg_cong[where f=length, OF A]
 with a and D have b: "length l < j" by force
 with B have c: "i + length l ≤ length w" by force
 have "subword w i j = subword w i (length l) ⋅ subword w (i + length l) (j - length l)" 
  by(rule subword_split, rule B, rule C, rule b)
 with A have d: "l ⋅ r = subword w i (length l) ⋅ subword w (i + length l) (j - length l)" by simp
 show ?thesis
 by(rule append_eq_append_conv[THEN iffD1], subst subword_length, rule c, simp, rule d)
qed
 




subsection ‹Properties of @{term "CYK"}›


lemma CYK_Lang :
"(S ∈ CYK G w 0 (length w)) = (w ∈ Lang G S)"
by(simp add: CYK_def subword_self)



lemma CYK_eq1 :
"i + 1 ≤ length w ⟹
 CYK G w i 1 = {S. (S, Leaf (w!i)) ∈ set G}"
by(simp add: CYK_def, subst subword_nth2[simplified], assumption,
   subst Lang_eq1, rule refl)


theorem CYK_eq2 :
assumes A: "i + j ≤ length w"
    and B: "1 < j"
shows "CYK G w i j = {X | X A B k. (X, Branch A B) ∈ set G ∧ A ∈ CYK G w i k ∧ B ∈ CYK G w (i + k) (j - k) ∧ 1 ≤ k ∧ k < j}"
proof(rule set_eqI, rule iffI, simp_all add: CYK_def)
 fix X
 assume a: "subword w i j ∈ Lang G X"
 show "∃A B. (X, Branch A B) ∈ set G ∧ (∃k. subword w i k ∈ Lang G A ∧ subword w (i + k) (j - k) ∈ Lang G B ∧ Suc 0 ≤ k ∧ k < j)"
 proof -
  have b: "1 < length(subword w i j)" by(subst subword_length, rule A, rule B)
  note Lang_eq2[THEN iffD1, OF conjI, OF a b]
  then obtain A B l r where c: "(X, Branch A B) ∈ set G ∧ subword w i j = l ⋅ r ∧ l ∈ Lang G A ∧ r ∈ Lang G B" by blast
  note Lang_no_Nil[OF c[THEN conjunct2, THEN conjunct2, THEN conjunct1]]
  hence d: "0 < length l" by(case_tac l, simp_all)
  note Lang_no_Nil[OF c[THEN conjunct2, THEN conjunct2, THEN conjunct2]]
  hence e: "0 < length r" by(case_tac r, simp_all)
  note subword_split2[OF c[THEN conjunct2, THEN conjunct1], OF A, OF d, OF e]
  with c show ?thesis 
  proof(rule_tac x=A in exI, rule_tac x=B in exI, simp, 
        rule_tac x="length l" in exI, simp)
   show "Suc 0 ≤ length l ∧ length l < j" (is "?A ∧ ?B")
   proof
    from d show "?A" by(case_tac l, simp_all)
   next
    note arg_cong[where f=length, OF c[THEN conjunct2, THEN conjunct1], THEN sym]
    also have "length(subword w i j) = j" by(rule subword_length, rule A)
    finally have "length l + length r = j" by simp
    with e show ?B by force
   qed
  qed
 qed
next
 fix X
 assume "∃A B. (X, Branch A B) ∈ set G ∧ (∃k. subword w i k ∈ Lang G A ∧ subword w (i + k) (j - k) ∈ Lang G B ∧ Suc 0 ≤ k ∧ k < j)"
 then obtain A B k where a: "(X, Branch A B) ∈ set G ∧ subword w i k ∈ Lang G A ∧ subword w (i + k) (j - k) ∈ Lang G B ∧ Suc 0 ≤ k ∧ k < j" by blast
 show "subword w i j ∈ Lang G X" 
 proof(rule Lang_eq2[THEN iffD2, THEN conjunct1], rule_tac x=A in exI, rule_tac x=B in exI, simp add: a,
       rule_tac x="subword w i k" in exI, rule_tac x="subword w (i + k) (j - k)" in exI, simp add: a,
       rule subword_split, rule A)
  from a show "0 < k" by force
 next
  from a show "k < j" by simp
 qed
qed



section "Implementation"

text "One of the particularly interesting features of CYK implementation 
is that it follows the principles of dynamic programming, constructing a 
table of solutions for sub-problems in the bottom-up style reusing already 
stored results."



subsection "Main cycle"


text "This is an auxiliary implementation of the membership test on lists."
fun mem :: "'a ⇒ 'a list ⇒ bool"
where 
"mem a [] = False" |
"mem a (x#xs) = (x = a ∨ mem a xs)"

lemma mem[simp] :
"mem x xs = (x ∈ set xs)"
by(induct_tac xs, simp, force)



text "The purpose of the following is to collect non-terminals that appear on the lhs of a production
      such that the first non-terminal on its rhs appears in the first of two given lists and the second
      non-terminal -- in the second list."
fun match_prods :: "('n, 't) CNG ⇒ 'n list ⇒ 'n list ⇒ 'n list"
where "match_prods [] ls rs = []" |
      "match_prods ((X, Branch A B)#ps) ls rs = 
          (if mem A ls ∧ mem B rs then X # match_prods ps ls rs
           else match_prods ps ls rs)" |
      "match_prods ((X, Leaf a)#ps) ls rs = match_prods ps ls rs"


lemma match_prods :
"(X ∈ set(match_prods G ls rs)) = 
 (∃A ∈ set ls. ∃B ∈ set rs. (X, Branch A B) ∈ set G)"
by(induct_tac G, clarsimp+, rename_tac l r ps, case_tac r, force+)



     
text "The following function is the inner cycle of the algorithm. The parameters $i$ and $j$
      identify a subword starting at $i$ with the length $j$, whereas $k$ is used to iterate through
      its splits (which are of course subwords as well) all having the length greater $0$ but less than $j$. 
      The parameter $T$ represents a table containing CYK solutions for those splits."
function inner :: "('n, 't) CNG ⇒ (nat × nat ⇒ 'n list) ⇒ nat ⇒ nat ⇒ nat ⇒ 'n list"
where "inner G T i k j = 
(if k < j then match_prods G (T(i, k)) (T(i + k, j - k)) @ inner G T i (k + 1) j
 else [])"
by pat_completeness auto
termination 
by(relation "measure(λ(a, b, c, d, e). e - d)", rule wf_measure, simp)


declare inner.simps[simp del]

lemma inner :
"(X ∈ set(inner G T i k j)) =
 (∃l. k ≤ l ∧ l < j ∧ X ∈ set(match_prods G (T(i, l)) (T(i + l, j - l))))" 
(is "?L G T i k j = ?R G T i k j")
proof(induct_tac G T i k j rule: inner.induct)
 fix G T i k j
 assume a: "k < j ⟹ ?L G T i (k + 1) j = ?R G T i (k + 1) j"
 show "?L G T i k j = ?R G T i k j"
 proof(case_tac "k < j")
  assume b: "k < j" 
  with a have c: "?L G T i (k + 1) j = ?R G T i (k + 1) j" by simp
  show ?thesis
  proof(subst inner.simps, simp add: b, rule iffI, erule disjE, rule_tac x=k in exI, simp add: b)
   assume "X ∈ set(inner G T i (Suc k) j)"
   with c have "?R G T i (k + 1) j" by simp
   thus "?R G T i k j" by(clarsimp, rule_tac x=l in exI, simp)
  next
   assume "?R G T i k j"
   then obtain l where d: "k ≤ l ∧ l < j ∧ X ∈ set(match_prods G (T(i, l)) (T(i + l, j - l)))" by blast
   show "X ∈ set(match_prods G (T(i, k)) (T(i + k, j - k))) ∨ ?L G T i (Suc k) j"
   proof(case_tac "Suc k ≤ l", rule disjI2, subst c[simplified], rule_tac x=l in exI, simp add: d, 
         rule disjI1)
    assume "¬ Suc k ≤ l"
    with d have "l = k" by force
    with d show "X ∈ set(match_prods G (T(i, k)) (T(i + k, j - k)))" by simp
   qed
  qed
 next
  assume "¬ k < j"
  thus ?thesis by(subst inner.simps, simp)
 qed
qed

   
   

text‹Now the main part of the algorithm just iterates through all subwords up to the given length $len$,
       calls @{term "inner"} on these, and stores the results in the table $T$. The length $j$ is supposed to 
       be greater than $1$ -- the subwords of length $1$ will be handled in the initialisation phase below.› 
function main :: "('n, 't) CNG ⇒ (nat × nat ⇒ 'n list) ⇒ nat ⇒ nat ⇒ nat ⇒ (nat × nat ⇒ 'n list)"
where "main G T len i j = (let T' = T((i, j) := inner G T i 1 j) in
                            if i + j < len then main G T' len (i + 1) j
                            else if j < len then main G T' len 0 (j + 1)
                                 else T')"
by pat_completeness auto
termination 
by(relation "inv_image (less_than <*lex*> less_than) (λ(a, b, c, d, e). (c - e, c - (d + e)))", rule wf_inv_image, rule wf_lex_prod, (rule wf_less_than)+, simp_all)



declare main.simps[simp del]


lemma main :
 assumes "1 < j"
     and "i + j ≤ length w"
     and "⋀i' j'. j' < j ⟹ 1 ≤ j' ⟹ i' + j' ≤ length w ⟹ set(T(i', j')) = CYK G w i' j'"
     and "⋀i'. i' < i ⟹ i' + j ≤ length w ⟹ set(T(i', j)) = CYK G w i' j"
     and "1 ≤ j'"
     and "i' + j' ≤ length w"
 shows "set((main G T (length w) i j)(i', j')) = CYK G w i' j'"
proof -
 have "∀len T' w. main G T len i j = T' ⟶ length w = len ⟶ 1 < j ⟶ i + j ≤ len ⟶
      (∀j' < j. ∀i'. 1 ≤ j' ⟶ i' + j' ≤ len ⟶ set(T(i', j')) = CYK G w i' j') ⟶
      (∀i' < i. i' + j ≤ len ⟶ set(T(i', j)) = CYK G w i' j) ⟶
      (∀j' ≥ 1. ∀i'. i' + j' ≤ len ⟶ set(T'(i', j')) = CYK G w i' j')" (is "∀len. ?P G T len i j")
 proof(rule allI, induct_tac G T len i j rule: main.induct, (drule meta_spec, drule meta_mp, rule refl)+, clarify)
  fix G T i j i' j'
  fix w :: "'a list" 
  assume a: "i + j < length w ⟹ ?P G (T((i, j) := inner G T i 1 j)) (length w) (i + 1) j"
  assume b: "¬ i + j < length w ⟹ j < length w ⟹ ?P G (T((i, j) := inner G T i 1 j)) (length w) 0 (j + 1)"
  assume c: "1 < j"
  assume d: "i + j ≤ length w"
  assume e: "(1::nat) ≤ j'"
  assume f: "i' + j' ≤ length w"
  assume g: "∀j' < j. ∀i'. 1 ≤ j' ⟶ i' + j' ≤ length w ⟶ set(T(i', j')) = CYK G w i' j'"
  assume h: "∀i' < i. i' + j ≤ length w ⟶ set(T(i', j)) = CYK G w i' j"

   have inner: "set (inner G T i (Suc 0) j) = CYK G w i j"
   proof(rule set_eqI, subst inner, subst match_prods, subst CYK_eq2, rule d, rule c, simp)
    fix X
    show "(∃l≥Suc 0. l < j ∧ (∃A ∈ set(T(i, l)). ∃B ∈ set(T(i + l, j - l)). (X, Branch A B) ∈ set G)) =
          (∃A B. (X, Branch A B) ∈ set G ∧ (∃k. A ∈ CYK G w i k ∧ B ∈ CYK G w (i + k) (j - k) ∧ Suc 0 ≤ k ∧ k < j))" (is "?L = ?R")
    proof
     assume "?L"
     thus "?R"
     proof(clarsimp, rule_tac x=A in exI, rule_tac x=B in exI, simp, rule_tac x=l in exI, simp)
      fix l A B
      assume i: "Suc 0 ≤ l"
      assume j: "l < j"
      assume k: "A ∈ set(T(i, l))"
      assume l: "B ∈ set(T(i + l, j - l))"
      note g[rule_format, where i'=i and j'=l]
      with d i j have A: "set(T(i, l)) = CYK G w i l" by force
      note g[rule_format, where i'="i + l" and j'="j - l"]
      with d i j have "set(T(i + l, j - l)) = CYK G w (i + l) (j - l)" by force
      with k l A show "A ∈ CYK G w i l ∧ B ∈ CYK G w (i + l) (j - l)" by simp
     qed
    next
     assume "?R"
     thus "?L"
     proof(clarsimp, rule_tac x=k in exI, simp)
      fix A B k
      assume i: "Suc 0 ≤ k"
      assume j: "k < j"
      assume k: "A ∈ CYK G w i k"
      assume l: "B ∈ CYK G w (i + k) (j - k)"
      assume m: "(X, Branch A B) ∈ set G"
      note g[rule_format, where i'=i and j'=k]
      with d i j have A: "CYK G w i k = set(T(i, k))" by force
      note g[rule_format, where i'="i + k" and j'="j - k"]
      with d i j have "CYK G w (i + k) (j - k) = set(T(i + k, j - k))" by force
      with k l A have "A ∈ set(T(i, k)) ∧ B ∈ set(T(i + k, j - k))" by simp
      with m show "∃A ∈ set(T(i, k)). ∃B ∈ set(T(i + k, j - k)). (X, Branch A B) ∈ set G" by force
     qed
    qed
   qed  (* inner *)

  show "set((main G T (length w) i j)(i', j')) = CYK G w i' j'"
  proof(case_tac "i + j = length w")
   assume i: "i + j = length w"
   show ?thesis
   proof(case_tac "j < length w")
    assume j: "j < length w"
    show ?thesis
    proof(subst main.simps, simp add: Let_def i j, 
          rule b[rule_format, where w=w and i'=i' and j'=j', OF _ _ refl, simplified], 
          simp_all add: inner)
     from i show "¬ i + j < length w" by simp
    next 
     from c show "0 < j" by simp
    next
     from j show "Suc j ≤ length w" by simp
    next 
     from e show "Suc 0 ≤ j'" by simp
    next
     from f show "i' + j' ≤ length w" by assumption
    next
     fix i'' j''
     assume k: "j'' < Suc j"
     assume l: "Suc 0 ≤ j''"
     assume m: "i'' + j'' ≤ length w"
     show "(i'' = i ⟶ j'' ≠ j) ⟶ set(T(i'',j'')) = CYK G w i'' j''"
     proof(case_tac "j'' = j", simp_all, clarify)
      assume n: "j'' = j"
      assume "i'' ≠ i"
      with i m n have "i'' < i" by simp
      with n m h show "set(T(i'', j)) = CYK G w i'' j" by simp
     next
      assume "j'' ≠ j"
      with k have "j'' < j" by simp
      with l m g show "set(T(i'', j'')) = CYK G w i'' j''" by simp
     qed
    qed
   next
    assume "¬ j < length w"
    with i have j: "i = 0 ∧ j = length w" by simp
    show ?thesis
    proof(subst main.simps, simp add: Let_def j, intro conjI, clarify)
     from j and inner show "set (inner G T 0 (Suc 0) (length w)) = CYK G w 0 (length w)" by simp
    next
     show "0 < i' ⟶ set(T(i', j')) = CYK G w i' j'"
     proof
      assume "0 < i'"
      with j and f have "j' < j" by simp
      with e g f show "set(T(i', j')) = CYK G w i' j'" by simp
     qed
    next
     show "j' ≠ length w ⟶ set(T(i', j')) = CYK G w i' j'"
     proof
      assume "j' ≠ length w "
      with j and f have "j' < j" by simp
      with e g f show "set(T(i', j')) = CYK G w i' j'" by simp
     qed
    qed
   qed
  next
   assume "i + j ≠ length w"
   with d have i: "i + j < length w" by simp
   show ?thesis
   proof(subst main.simps, simp add: Let_def i,
         rule a[rule_format, where w=w and i'=i' and j'=j', OF i, OF refl, simplified])
    from c show "Suc 0 < j" by simp
   next
    from i show "Suc(i + j) ≤ length w" by simp
   next
    from e show "Suc 0 ≤ j'" by simp
   next
    from f show "i' + j' ≤ length w" by assumption
   next
    fix i'' j''
    assume "j'' < j"
    and "Suc 0 ≤ j''"
    and "i'' + j'' ≤ length w"
    with g show "set(T(i'', j'')) = CYK G w i'' j''" by simp
   next
    fix i'' assume j: "i'' < Suc i" 
    show "set(if i'' = i then inner G T i (Suc 0) j else T(i'', j)) = CYK G w i'' j"
    proof(simp split: if_split, rule conjI, clarify, rule inner, clarify)
     assume "i'' ≠ i"
     with j have "i'' < i" by simp
     with d h show "set(T(i'', j)) = CYK G w i'' j" by simp
    qed
   qed
  qed
 qed
 with assms show ?thesis by force
qed

 




subsection "Initialisation phase"

text‹Similarly to @{term "match_prods"} above, here we collect non-terminals from which
       the given terminal symbol can be derived.› 
fun init_match :: "('n, 't) CNG ⇒ 't ⇒ 'n list"
where "init_match [] t = []" |
      "init_match ((X, Branch A B)#ps) t = init_match ps t" |
      "init_match ((X, Leaf a)#ps) t = (if a = t then X # init_match ps t
                                        else init_match ps t)"


lemma init_match :
"(X ∈ set(init_match G a)) = 
 ((X, Leaf a) ∈ set G)"
by(induct_tac G a rule: init_match.induct, simp_all)


text "Representing the empty table."
definition "emptyT = (λ(i, j). [])" 

text "The following function initialises the empty table for subwords of
      length $1$, i.e. each symbol occurring in the given word."
fun init' :: "('n, 't) CNG ⇒ 't list ⇒ nat ⇒ nat × nat ⇒ 'n list"
where "init' G [] k = emptyT" |
      "init' G (t#ts) k = (init' G ts (k + 1))((k, 1) := init_match G t)" 



lemma init' :
assumes "i + 1 ≤ length w"
shows "set(init' G w 0 (i, 1)) = CYK G w i 1"
proof -
 have "∀i. Suc i ≤ length w ⟶
      (∀k. set(init' G w k (k + i, Suc 0)) = CYK G w i (Suc 0))" (is "∀i. ?P i w ⟶ (∀k. ?Q i k w)")
 proof(induct_tac w, clarsimp+, rule conjI, clarsimp, rule set_eqI, subst init_match)
  fix x w S
  show "((S, Leaf x) ∈ set G) = (S ∈ CYK G (x#w) 0 (Suc 0))" by(subst CYK_eq1[simplified], simp_all)
 next
  fix x w i
  assume a: "∀i. ?P i w ⟶ (∀k. ?Q i k w)"
  assume b: "i ≤ length w"
  show "0 < i ⟶ (∀k. set(init' G w (Suc k) (k + i, Suc 0)) = CYK G (x#w) i (Suc 0))"
  proof(clarify, case_tac i, simp_all, subst CYK_eq1[simplified], simp, erule subst, rule b, simp)
   fix k j
   assume c: "i = Suc j"
   note a[rule_format, where i=j and k="Suc k"]
   with b and c have "set(init' G w (Suc k) (Suc k + j, Suc 0)) = CYK G w j (Suc 0)" by simp
   also with b and c have "... = {S. (S, Leaf (w ! j)) ∈ set G}" by(subst CYK_eq1[simplified], simp_all)
   finally show "set(init' G w (Suc k) (Suc (k + j), Suc 0)) = {S. (S, Leaf (w ! j)) ∈ set G}" by simp
  qed
 qed
 with assms have "∀k. ?Q i k w" by simp
 note this[rule_format, where k=0]
 thus ?thesis by simp
qed





text‹The next version of initialization refines @{term "init'"} in that
      it takes additional account of the cases when the given word is 
      empty or contains a terminal symbol that does not have any matching 
      production (that is, @{term "init_match"} is an empty list). No initial 
      table is then needed as such words can immediately be rejected.›  
fun init :: "('n, 't) CNG ⇒ 't list ⇒ nat ⇒ (nat × nat ⇒ 'n list) option"
where "init G [] k = None" |
      "init G [t] k = (case (init_match G t) of
                        [] ⇒ None
                      | xs ⇒ Some(emptyT((k, 1) := xs)))" |
      "init G (t#ts) k = (case (init_match G t) of
                           [] ⇒ None
                         | xs ⇒ (case (init G ts (k + 1)) of
                                  None ⇒ None
                                | Some T ⇒ Some(T((k, 1) := xs))))" 


lemma init1:
  ‹init' G w k = T› if ‹init G w k = Some T› 
  using that by (induction G w k arbitrary: T rule: init.induct)
    (simp_all split: list.splits option.splits)

lemma init2 :
"(init G w k = None) =
 (w = [] ∨ (∃a ∈ set w. init_match G a = []))"
by(induct_tac G w k rule: init.induct, simp, simp split: list.split, 
   simp split: list.split option.split, force)



subsection ‹The overall procedure›


definition "cyk G S w = (case init G w 0 of
                          None ⇒ False
                        | Some T ⇒ let len = length w in
                                     if len = 1 then mem S (T(0, 1))
                                     else let T' = main G T len 0 2 in
                                            mem S (T'(0, len)))"



theorem cyk :
"cyk G S w = (w ∈ Lang G S)"
proof(simp add: cyk_def split: option.split, simp_all add: Let_def,
      rule conjI, subst init2, simp, rule conjI)
 show "w = [] ⟶ [] ∉ Lang G S" by(clarify, drule Lang_no_Nil, clarify)
next
 show "(∃x∈set w. init_match G x = []) ⟶ w ∉ Lang G S" by(clarify, drule Lang_term, subst (asm) init_match[THEN sym], force)
next 
 show "∀T. init G w 0 = Some T ⟶ 
       ((length w = Suc 0 ⟶ S ∈ set(T(0, Suc 0))) ∧
        (length w ≠ Suc 0 ⟶ S ∈ set(main G T (length w) 0 2 (0, length w)))) =
       (w ∈ Lang G S)" (is "∀T. ?P T ⟶ ?L T = ?R")
 proof clarify
  fix T
  assume a: "?P T"
  hence b: "init' G w 0 = T" by(rule init1)
  note init2[THEN iffD2, OF disjI1]
  have c: "w ≠ []" by(clarify, drule init2[where G=G and k=0, THEN iffD2, OF disjI1], simp add: a)
  have "?L (init' G w 0) = ?R"
  proof(case_tac "length w = 1", simp_all)
   assume d: "length w = Suc 0"   
   show "S ∈ set(init' G w 0 (0, Suc 0)) = ?R"
   by(subst init'[simplified], simp add: d, subst CYK_Lang[THEN sym], simp add: d)
  next
   assume "length w ≠ Suc 0"   
   with c have "1 < length w" by(case_tac w, simp_all)
   hence d: "Suc(Suc 0) ≤ length w" by simp
   show "(S ∈ set(main G (init' G w 0) (length w) 0 2 (0, length w))) = (w ∈ Lang G S)"
   proof(subst main, simp_all, rule d)
    fix i' j'
    assume "j' < 2" and "Suc 0 ≤ j'"
    hence e: "j' = 1" by simp
    assume "i' + j' ≤ length w"
    with e have f: "i' + 1 ≤ length w" by simp
    have "set(init' G w 0 (i', 1)) = CYK G w i' 1" by(rule init', rule f)
    with e show "set(init' G w 0 (i', j')) = CYK G w i' j'" by simp
   next
    from d show "Suc 0 ≤ length w" by simp
   next
    show "(S ∈ CYK G w 0 (length w)) = (w ∈ Lang G S)" by(rule CYK_Lang)
   qed
  qed
  with b show "?L T = ?R" by simp
 qed
qed

value [code]
  "let G = [(0::int, Branch 1 2), (0, Branch 2 3),
            (1, Branch 2 1), (1, Leaf ''a''),
            (2, Branch 3 3), (2, Leaf ''b''),
            (3, Branch 1 2), (3, Leaf ''a'')]
  in map (cyk G 0)
     [[''b'',''a'',''a'',''b'',''a''],
      [''b'',''a'',''b'',''a'']]"

end