Commit fba1955c authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

Merge (generating index again)

......@@ -870,6 +870,18 @@ topic = Computer Science/Automata and Formal Languages
date = 2011-08-26
abstract = There are many proofs of the Myhill-Nerode theorem using automata. In this library we give a proof entirely based on regular expressions, since regularity of languages can be conveniently defined using regular expressions (it is more painful in HOL to define regularity in terms of automata). We prove the first direction of the Myhill-Nerode theorem by solving equational systems that involve regular expressions. For the second direction we give two proofs: one using tagging-functions and another using partial derivatives. We also establish various closure properties of regular languages. Most details of the theories are described in our ITP 2011 paper.
[CYK]
title = A formalisation of the Cocke-Younger-Kasami algorithm
author = Maksym Bortin <mailto:Maksym.Bortin@nicta.com.au>
date = 2016-04-27
topic = Computer Science/Algorithms, Computer Science/Automata and Formal Languages
abstract =
The theory provides a formalisation of the Cocke-Younger-Kasami
algorithm (CYK for short), an approach to solving the word problem
for context-free languages. CYK decides if a word is in the
languages generated by a context-free grammar in Chomsky normal form.
The formalized algorithm is executable.
[Boolean_Expression_Checkers]
title = Boolean Expression Checkers
author = Tobias Nipkow <http://www.in.tum.de/~nipkow>
......
(* 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 \<times> ('n, 't) RHS) list"
text "Abbreviating the list append symbol for better readability"
abbreviation list_append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "\<cdot>" 65)
where "xs \<cdot> ys \<equiv> 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 \<Rightarrow> (('n, 't) word_form \<times> ('n, 't) word_form) set"
where "DSTEP G = {(l \<cdot> [Inl N] \<cdot> r, x) | l N r rhs x. (N, rhs) \<in> set G \<and>
(case rhs of
Branch A B \<Rightarrow> x = l \<cdot> [Inl A, Inl B] \<cdot> r
| Leaf t \<Rightarrow> x = l \<cdot> [Inr t] \<cdot> r)}"
abbreviation DSTEP' :: "('n, 't) word_form \<Rightarrow> ('n, 't) CNG \<Rightarrow> ('n, 't) word_form \<Rightarrow> bool" ("_ -_\<rightarrow> _" [60, 61, 60] 61)
where "w -G\<rightarrow> w' \<equiv> (w, w') \<in> DSTEP G"
abbreviation DSTEP_reflc :: "('n, 't) word_form \<Rightarrow> ('n, 't) CNG \<Rightarrow> ('n, 't) word_form \<Rightarrow> bool" ("_ -_\<rightarrow>\<^sup>= _" [60, 61, 60] 61)
where "w -G\<rightarrow>\<^sup>= w' \<equiv> (w, w') \<in> (DSTEP G)\<^sup>="
abbreviation DSTEP_transc :: "('n, 't) word_form \<Rightarrow> ('n, 't) CNG \<Rightarrow> ('n, 't) word_form \<Rightarrow> bool" ("_ -_\<rightarrow>\<^sup>+ _" [60, 61, 60] 61)
where "w -G\<rightarrow>\<^sup>+ w' \<equiv> (w, w') \<in> (DSTEP G)\<^sup>+"
abbreviation DSTEP_rtransc :: "('n, 't) word_form \<Rightarrow> ('n, 't) CNG \<Rightarrow> ('n, 't) word_form \<Rightarrow> bool" ("_ -_\<rightarrow>\<^sup>* _" [60, 61, 60] 61)
where "w -G\<rightarrow>\<^sup>* w' \<equiv> (w, w') \<in> (DSTEP G)\<^sup>*"
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 \<Rightarrow> 'n \<Rightarrow> 't word set"
where "Lang G S = {w. [Inl S] -G\<rightarrow>\<^sup>+ 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) \<in> set G \<Longrightarrow>
L \<cdot> [Inl S] \<cdot> R -G\<rightarrow> L \<cdot> [Inl A, Inl B] \<cdot> R"
by(simp add: DSTEP_def, rule_tac x="L" in exI, force)
lemma prod_into_DSTEP2 :
"(S, Leaf a) \<in> set G \<Longrightarrow>
L \<cdot> [Inl S] \<cdot> R -G\<rightarrow> L \<cdot> [Inr a] \<cdot> R"
by(simp add: DSTEP_def, rule_tac x="L" in exI, force)
lemma DSTEP_D :
"s -G\<rightarrow> t \<Longrightarrow>
\<exists>L N R rhs. s = L \<cdot> [Inl N] \<cdot> R \<and> (N, rhs) \<in> set G \<and>
(\<forall>A B. rhs = Branch A B \<longrightarrow> t = L \<cdot> [Inl A, Inl B] \<cdot> R) \<and>
(\<forall>x. rhs = Leaf x \<longrightarrow> t = L \<cdot> [Inr x] \<cdot> R)"
by(unfold DSTEP_def, clarsimp, simp split: RHS.split_asm, blast+)
lemma DSTEP_append :
assumes a: "s -G\<rightarrow> t"
shows "L \<cdot> s \<cdot> R -G\<rightarrow> L \<cdot> t \<cdot> R"
proof -
from a have "\<exists>l N r rhs. s = l \<cdot> [Inl N] \<cdot> r \<and> (N, rhs) \<in> set G \<and>
(\<forall>A B. rhs = Branch A B \<longrightarrow> t = l \<cdot> [Inl A, Inl B] \<cdot> r) \<and>
(\<forall>x. rhs = Leaf x \<longrightarrow> t = l \<cdot> [Inr x] \<cdot> r)" (is "\<exists>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 \<cdot> l" in exI,
rule_tac x=N in exI, rule_tac x="r \<cdot> R" in exI,
simp, rule_tac x=rhs in exI, simp split: RHS.split)
qed
lemma DSTEP_star_mono :
"s -G\<rightarrow>\<^sup>* t \<Longrightarrow> length s \<le> length t"
proof(erule rtrancl_induct, simp)
fix t u
assume "s -G\<rightarrow>\<^sup>* t"
assume a: "t -G\<rightarrow> u"
assume b: "length s \<le> length t"
show "length s \<le> length u"
proof -
from a have "\<exists>L N R rhs. t = L \<cdot> [Inl N] \<cdot> R \<and> (N, rhs) \<in> set G \<and>
(\<forall>A B. rhs = Branch A B \<longrightarrow> u = L \<cdot> [Inl A, Inl B] \<cdot> R) \<and>
(\<forall>x. rhs = Leaf x \<longrightarrow> u = L \<cdot> [Inr x] \<cdot> R)" (is "\<exists>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 \<cdot> r -G\<rightarrow> t"
shows "\<exists>l' r'. l -G\<rightarrow>\<^sup>= l' \<and> r -G\<rightarrow>\<^sup>= r' \<and> t = l' \<cdot> r'"
proof -
from a have "\<exists>L N R rhs. l \<cdot> r = L \<cdot> [Inl N] \<cdot> R \<and> (N, rhs) \<in> set G \<and>
(\<forall>A B. rhs = Branch A B \<longrightarrow> t = L \<cdot> [Inl A, Inl B] \<cdot> R) \<and>
(\<forall>x. rhs = Leaf x \<longrightarrow> t = L \<cdot> [Inr x] \<cdot> R)" (is "\<exists>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 \<cdot> r = L \<cdot> Inl N # R" by simp
hence "\<exists>u. (l = L \<cdot> u \<and> u \<cdot> r = Inl N # R) \<or> (l \<cdot> u = L \<and> r = u \<cdot> Inl N # R)" by(rule append_eq_append_conv2[THEN iffD1])
then obtain xs where c: "l = L \<cdot> xs \<and> xs \<cdot> r = Inl N # R \<or> l \<cdot> xs = L \<and> r = xs \<cdot> Inl N # R" (is "?C1 \<or> ?C2") by blast
show ?thesis
proof(cases rhs)
case (Leaf x)
with b have d: "t = L \<cdot> [Inr x] \<cdot> R \<and> (N, Leaf x) \<in> 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 \<cdot> 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 \<cdot> [Inl A, Inl B] \<cdot> R \<and> (N, Branch A B) \<in> 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 \<cdot> [Inl A, Inl B] \<cdot> 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 \<cdot> r -G\<rightarrow>\<^sup>* t"
shows "\<exists>l' r'. l -G\<rightarrow>\<^sup>* l' \<and> r -G\<rightarrow>\<^sup>* r' \<and> t = l' \<cdot> r'"
proof -
have "\<And>s. s -G\<rightarrow>\<^sup>* t \<Longrightarrow>
\<forall>l r. s = l \<cdot> r \<longrightarrow> (\<exists>l' r'. l -G\<rightarrow>\<^sup>* l' \<and> r -G\<rightarrow>\<^sup>* r' \<and> t = l' \<cdot> r')" (is "\<And>s. ?P s t \<Longrightarrow> ?Q s t")
proof(erule rtrancl_induct, force)
fix s t u
assume "?P s t"
assume a: "t -G\<rightarrow> u"
assume b: "?Q s t"
show "?Q s u"
proof(clarify)
fix l r
assume "s = l \<cdot> r"
with b have "\<exists>l' r'. l -G\<rightarrow>\<^sup>* l' \<and> r -G\<rightarrow>\<^sup>* r' \<and> t = l' \<cdot> r'" by simp
then obtain l' r' where c: "l -G\<rightarrow>\<^sup>* l' \<and> r -G\<rightarrow>\<^sup>* r' \<and> t = l' \<cdot> r'" by blast
with a have "l' \<cdot> r' -G\<rightarrow> u" by simp
hence "\<exists>l'' r''. l' -G\<rightarrow>\<^sup>= l'' \<and> r' -G\<rightarrow>\<^sup>= r'' \<and> u = l'' \<cdot> r''" by(rule DSTEP_comp)
then obtain l'' r'' where "l' -G\<rightarrow>\<^sup>= l'' \<and> r' -G\<rightarrow>\<^sup>= r'' \<and> u = l'' \<cdot> r''" by blast
hence "l' -G\<rightarrow>\<^sup>* l'' \<and> r' -G\<rightarrow>\<^sup>* r'' \<and> u = l'' \<cdot> r''" by blast
with c show "\<exists>l' r'. l -G\<rightarrow>\<^sup>* l' \<and> r -G\<rightarrow>\<^sup>* r' \<and> u = l' \<cdot> 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\<rightarrow>\<^sup>* l'"
and B: "r -G\<rightarrow>\<^sup>* r'"
shows "l \<cdot> r -G\<rightarrow>\<^sup>* l' \<cdot> r'"
proof -
have "l -G\<rightarrow>\<^sup>* l' \<Longrightarrow>
\<forall>r r'. r -G\<rightarrow>\<^sup>* r' \<longrightarrow> l \<cdot> r -G\<rightarrow>\<^sup>* l' \<cdot> r'" (is "?P l l' \<Longrightarrow> ?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\<rightarrow> t"
assume b: "l \<cdot> r -G\<rightarrow>\<^sup>* l \<cdot> s"
show "l \<cdot> r -G\<rightarrow>\<^sup>* l \<cdot> t"
proof -
from a have "l \<cdot> s -G\<rightarrow> l \<cdot> 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\<rightarrow> t"
assume b: "?Q l s"
show "?Q l t"
proof(clarsimp)
fix r r'
assume "r -G\<rightarrow>\<^sup>* r'"
with b have c: "l \<cdot> r -G\<rightarrow>\<^sup>* s \<cdot> r'" by simp
from a have "s \<cdot> r' -G\<rightarrow> t \<cdot> r'" by(drule_tac L="[]" and R=r' in DSTEP_append, simp)
with c show "l \<cdot> r -G\<rightarrow>\<^sup>* t \<cdot> r'" by simp
qed
qed
with A and B show ?thesis by simp
qed
lemma DSTEP_trancl_term :
assumes A: "[Inl S] -G\<rightarrow>\<^sup>+ t"
and B: "Inr x \<in> set t"
shows "\<exists>N. (N, Leaf x) \<in> set G"
proof -
have "[Inl S] -G\<rightarrow>\<^sup>+ t \<Longrightarrow>
\<forall>x. Inr x \<in> set t \<longrightarrow> (\<exists>N. (N, Leaf x) \<in> set G)" (is "?P t \<Longrightarrow> ?Q t")
proof(erule trancl_induct)
fix t
assume a: "[Inl S] -G\<rightarrow> t"
show "?Q t"
proof -
from a have "\<exists>rhs. (S, rhs) \<in> set G \<and>
(\<forall>A B. rhs = Branch A B \<longrightarrow> t = [Inl A, Inl B]) \<and>
(\<forall>x. rhs = Leaf x \<longrightarrow> t = [Inr x])" (is "\<exists>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\<rightarrow> t"
assume b: "?Q s"
show "?Q t"
proof -
from a have "\<exists>L N R rhs. s = L \<cdot> [Inl N] \<cdot> R \<and> (N, rhs) \<in> set G \<and>
(\<forall>A B. rhs = Branch A B \<longrightarrow> t = L \<cdot> [Inl A, Inl B] \<cdot> R) \<and>
(\<forall>x. rhs = Leaf x \<longrightarrow> t = L \<cdot> [Inr x] \<cdot> R)" (is "\<exists>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 \<in> Lang G S \<Longrightarrow> w \<noteq> []"
by(simp add: Lang_def, drule trancl_into_rtrancl, drule DSTEP_star_mono, force)
lemma Lang_rtrancl_eq :
"(w \<in> Lang G S) = [Inl S] -G\<rightarrow>\<^sup>* map Inr w" (is "?L = (?p \<in> ?R\<^sup>*)")
proof(simp add: Lang_def, rule iffI, erule trancl_into_rtrancl)
assume "?p \<in> ?R\<^sup>*"
hence "?p \<in> (?R\<^sup>+)\<^sup>=" by(subst rtrancl_trancl_reflcl[THEN sym], assumption)
hence "[Inl S] = map Inr w \<or> ?p \<in> ?R\<^sup>+" by force
thus "?p \<in> ?R\<^sup>+" by(case_tac w, simp_all)
qed
lemma Lang_term :
"w \<in> Lang G S \<Longrightarrow>
\<forall>x \<in> set w. \<exists>N. (N, Leaf x) \<in> set G"
by(clarsimp simp add: Lang_def, drule DSTEP_trancl_term,
simp, erule imageI, assumption)
lemma Lang_eq1 :
"([x] \<in> Lang G S) = ((S, Leaf x) \<in> set G)"
proof(simp add: Lang_def, rule iffI, subst (asm) trancl_unfold_left, clarsimp)
fix t
assume a: "[Inl S] -G\<rightarrow> t"
assume b: "t -G\<rightarrow>\<^sup>* [Inr x]"
note DSTEP_star_mono[OF b, simplified]
hence c: "length t \<le> 1" by simp
have "\<exists>z. t = [z]"
proof(cases t)
assume "t = []"
with b have d: "[] -G\<rightarrow>\<^sup>* [Inr x]" by simp
have "\<And>s. ([], s) \<in> (DSTEP G)\<^sup>* \<Longrightarrow> 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 "\<exists>z. (S, Leaf z) \<in> set G \<and> 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) \<in> set G"
proof(clarsimp)
fix z
assume c: "(S, Leaf z) \<in> set G"
assume "[Inr z] -G\<rightarrow>\<^sup>* [Inr x]"
hence "([Inr z], [Inr x]) \<in> ((DSTEP G)\<^sup>+)\<^sup>=" by simp
hence "[Inr z] = [Inr x] \<or> [Inr z] -G\<rightarrow>\<^sup>+ [Inr x]" by force
hence "x = z"
proof
assume "[Inr z] = [Inr x]" thus ?thesis by simp
next
assume "[Inr z] -G\<rightarrow>\<^sup>+ [Inr x]"
hence "\<exists>u. [Inr z] -G\<rightarrow> u \<and> u -G\<rightarrow>\<^sup>* [Inr x]" by(subst (asm) trancl_unfold_left, force)
then obtain u where "[Inr z] -G\<rightarrow> 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) \<in> set G"
show "[Inl S] -G\<rightarrow>\<^sup>+ [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 \<in> Lang G S \<and> 1 < length w) =
(\<exists>A B. (S, Branch A B) \<in> set G \<and> (\<exists>l r. w = l \<cdot> r \<and> l \<in> Lang G A \<and> r \<in> 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 : "\<And>xs. \<forall>zs w. map Inr w = xs \<cdot> zs \<longrightarrow>
(\<exists>u v. w = u \<cdot> v \<and> xs = map Inr u \<and> zs = map Inr v)"
by(induct_tac xs, simp, force)
fix t
assume a: "Suc 0 < length w"
assume b: "[Inl S] -G\<rightarrow> t"
assume c: "t -G\<rightarrow>\<^sup>* map Inr w"
from b have "\<exists>A B. (S, Branch A B) \<in> set G \<and> 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\<rightarrow>\<^sup>* map Inr w"by simp
have "\<And>x s. [Inr x] -G\<rightarrow>\<^sup>* s \<Longrightarrow> 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) \<in> set G \<and> t = [Inl A, Inl B]" by blast
with c have e: "[Inl A] \<cdot> [Inl B] -G\<rightarrow>\<^sup>* map Inr w" by simp
note DSTEP_star_comp1[OF e]
then obtain l' r' where e: "[Inl A] -G\<rightarrow>\<^sup>* l' \<and> [Inl B] -G\<rightarrow>\<^sup>* r' \<and>
map Inr w = l' \<cdot> r'" by blast
note map_Inr_split[rule_format, OF e[THEN conjunct2, THEN conjunct2]]
then obtain u v where f: "w = u \<cdot> v \<and> l' = map Inr u \<and> r' = map Inr v" by blast
with e have g: "[Inl A] -G\<rightarrow>\<^sup>* map Inr u \<and> [Inl B] -G\<rightarrow>\<^sup>* 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) \<in> set G \<and> w = l \<cdot> r \<and> l \<in> Lang G A \<and> r \<in> Lang G B" by blast
have "[Inl A] \<cdot> [Inl B] -G\<rightarrow>\<^sup>* map Inr l \<cdot> 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] \<cdot> [Inl B] -G\<rightarrow>\<^sup>* map Inr w" by(simp add: a)
have c: "w \<in> Lang G S"
by(simp add: Lang_def, subst trancl_unfold_left, rule_tac b="[Inl A] \<cdot> [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 \<le> Suc 0"
hence "l = [] \<or> r = []" by(case_tac l, simp_all)
thus "False"
proof
assume "l = []"
with a have "[] \<in> Lang G A" by simp
note Lang_no_Nil[OF this]
thus ?thesis by simp
next
assume "r = []"
with a have "[] \<in> 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 \<in> Lang G S}"
subsection {* Properties of @{term "subword"} *}
lemma subword_length :
"i + j \<le> length w \<Longrightarrow> length(subword w i j) = j"
by(simp add: subword_def)
lemma subword_nth1 :
"i + j \<le> length w \<Longrightarrow> k < j \<Longrightarrow>
(subword w i j)!k = w!(i + k)"
by(simp add: subword_def)
lemma subword_nth2 :
assumes A: "i + 1 \<le> length w"
shows "subword w i 1 = [w!i]"
proof -
note subword_length[OF A]
hence "\<exists>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] :
"\<forall>n m. n \<le> length xs \<longrightarrow> n \<le> m \<longrightarrow>
take n xs \<cdot> 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 \<le> length w \<Longrightarrow> 0 < k \<Longrightarrow> k < j \<Longrightarrow>
subword w i j = subword w i k \<cdot> subword w (i + k) (j - k)"
by(simp add: subword_def, subst take_split[where n=k, THEN sym], simp_all,
rule_tac f="\<lambda>x. take (j - k) (drop x w)" in arg_cong, simp)
lemma subword_split2 :
assumes A: "subword w i j = l \<cdot> r"
and B: "i + j \<le> length w"
and C: "0 < length l"
and D: "0 < length r"
shows "l = subword w i (length l) \<and> 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 \<le> length w" by force
have "subword w i j = subword w i (length l) \<cdot> subword w (i + length l) (j - length l)"
by(rule subword_split, rule B, rule C, rule b)
with A have d: "l \<cdot> r = subword w i (length l) \<cdot> 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 \<in> CYK G w 0 (length w)) = (w \<in> Lang G S)"
by(simp add: CYK_def subword_self)
lemma CYK_eq1 :
"i + 1 \<le> length w \<Longrightarrow>
CYK G w i 1 = {S. (S, Leaf (w!i)) \<in> set G}"
by(simp add: CYK_def, subst subword_nth2[simplified], assumption,
subst Lang_eq1, rule refl)
theorem CYK_eq2 :
assumes A: "i + j \<le> length w"
and B: "1 < j"
shows "CYK G w i j = {X | X A B k. (X, Branch A B) \<in> set G \<and> A \<in> CYK G w i k \<and> B \<in> CYK G w (i + k) (j - k) \<and> 1 \<le> k \<and> k < j}"
proof(rule set_eqI, rule iffI, simp_all add: CYK_def)
fix X
assume a: "subword w i j \<in> Lang G X"
show "\<exists>A B. (X, Branch A B) \<in> set G \<and> (\<exists>k. subword w i k \<in> Lang G A \<and> subword w (i + k) (j - k) \<in> Lang G B \<and> Suc 0 \<le> k \<and> 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) \<in> set G \<and> subword w i j = l \<cdot> r \<and> l \<in> Lang G A \<and> r \<in> 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 \<le> length l \<and> length l < j" (is "?A \<and> ?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 "\<exists>A B. (X, Branch A B) \<in> set G \<and> (\<exists>k. subword w i k \<in> Lang G A \<and> subword w (i + k) (j - k) \<in> Lang G B \<and> Suc 0 \<le> k \<and> k < j)"
then obtain A B k where a: "(X, Branch A B) \<in> set G \<and> subword w i k \<in> Lang G A \<and> subword w (i + k) (j - k) \<in> Lang G B \<and> Suc 0 \<le> k \<and> k < j" by blast
show "subword w i j \<in> 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