Theory TheoremD2
theory TheoremD2
imports LocalLexingLemmas Validity Derivations
begin
context LocalLexing begin
definition splits_at :: "sentence ⇒ nat ⇒ sentence ⇒ symbol ⇒ sentence ⇒ bool"
where
"splits_at δ i α N β = (i < length δ ∧ α = take i δ ∧ N = δ ! i ∧ β = drop (Suc i) δ)"
lemma splits_at_combine: "splits_at δ i α N β ⟹ δ = α @ [N] @ β"
by (simp add: id_take_nth_drop splits_at_def)
lemma splits_at_combine_dest: "Derives1 a i r b ⟹ splits_at a i α N β ⟹ b = α @ (snd r) @ β"
by (metis (no_types, lifting) Derives1_drop Derives1_split append_assoc append_eq_conv_conj
length_append splits_at_def)
lemma Derives1_nonterminal:
assumes "Derives1 a i r b"
assumes "splits_at a i α N β"
shows "fst r = N ∧ is_nonterminal N"
proof -
from assms have fst: "fst r = N"
by (metis Derives1_split append_Cons nth_append_length splits_at_def)
then have "is_nonterminal N"
by (metis Derives1_def assms(1) prod.collapse rule_nonterminal_type)
with fst show ?thesis by auto
qed
lemma splits_at_ex: "Derives1 δ i r s ⟹ ∃ α N β. splits_at δ i α N β"
by (simp add: Derives1_bound splits_at_def)
lemma splits_at_α: "Derives1 δ i r s ⟹ splits_at δ i α N β ⟹
α = take i δ ∧ α = take i s ∧ length α = i"
by (metis Derives1_split append_eq_conv_conj splits_at_def)
lemma LeftDerives1_splits_at_is_word: "LeftDerives1 δ i r s ⟹ splits_at δ i α N β ⟹ is_word α"
by (metis LeftDerives1_def leftmost_def splits_at_def)
lemma splits_at_β: "Derives1 δ i r s ⟹ splits_at δ i α N β ⟹
β = drop (Suc i) δ ∧ β = drop (i + length (snd r)) s ∧ length β = length δ - i - 1"
by (metis Derives1_drop Suc_eq_plus1 diff_diff_left length_drop splits_at_def)
lemma Derives1_prefix:
assumes ab: "Derives1 δ i r (a@b)"
assumes split: "splits_at δ i α N β"
shows "is_prefix α a ∨ is_prefix a α"
proof -
have take: "α = take i (a@b)" using ab split splits_at_α by blast
show ?thesis
proof (cases "i ≤ length a")
case True
then have "α = take i a" by (simp add: take)
then have "is_prefix α a"
by (metis append_take_drop_id is_prefix_def)
with True show ?thesis by auto
next
case False
then have "is_prefix a α"
by (simp add: is_prefix_def nat_le_linear take)
with False show ?thesis by auto
qed
qed
lemma Derives1_suffix:
assumes ab: "Derives1 δ i r (a@b)"
assumes split: "splits_at δ i α N β"
shows "is_suffix β b ∨ is_suffix b β"
proof -
have drop1: "β = drop (i + length (snd r)) (a@b)" using ab split splits_at_β by blast
have drop2: "b = drop (length a) (a@b)" by simp
show ?thesis
proof (cases "(i + length (snd r)) ≤ length a")
case True
with drop1 drop2 have "is_suffix b β" by (simp add: is_suffix_def)
then show ?thesis by auto
next
case False
then have "length a ≤ (i + length (snd r))" by arith
with drop1 drop2 have "is_suffix β b"
by (metis append_Nil append_take_drop_id drop_append drop_eq_Nil is_suffix_def)
then show ?thesis by auto
qed
qed
lemma Derives1_skip_prefix:
"length a ≤ i ⟹ Derives1 (a@b) i r (a@c) ⟹ Derives1 b (i - length a) r c"
apply (auto simp add: Derives1_def)
by (metis append_eq_append_conv_if is_sentence_concat is_sentence_cons is_symbol_def
length_drop rule_nonterminal_type)
lemma cancel_suffix:
assumes "a @ c = b @ d"
assumes "length c ≤ length d"
shows "a = b @ (take (length d - length c) d)"
proof -
have "a @ c = (b @ take (length d - length c) d) @ drop (length d - length c) d"
by (metis append_assoc append_take_drop_id assms(1))
then show ?thesis
by (metis append_eq_append_conv assms(2) diff_diff_cancel length_drop)
qed
lemma is_sentence_take:
"is_sentence y ⟹ is_sentence (take n y)"
by (metis append_take_drop_id is_sentence_concat)
lemma Derives1_skip_suffix:
assumes i: "i < length a"
assumes D: "Derives1 (a@c) i r (b@c)"
shows "Derives1 a i r b"
proof -
note Derives1_def[where u="a@c" and v="b@c" and i=i and r=r]
then have "∃x y N α.
a @ c = x @ [N] @ y ∧
b @ c = x @ α @ y ∧ is_sentence x ∧ is_sentence y ∧ (N, α) ∈ ℜ ∧ r = (N, α) ∧ i = length x"
using D by blast
then obtain x y N α where split:
"a @ c = x @ [N] @ y ∧
b @ c = x @ α @ y ∧ is_sentence x ∧ is_sentence y ∧ (N, α) ∈ ℜ ∧ r = (N, α) ∧ i = length x"
by blast
from split have "length (a@c) = length (x @ [N] @ y)" by auto
then have "length a + length c = length x + length y + 1" by simp
with split have "length a + length c = i + length y + 1" by simp
with i have len_c_y: "length c ≤ length y" by arith
let ?y = "take (length y - length c) y"
from split have ac: "a @ c = (x @ [N]) @ y" by auto
note cancel_suffix[where a=a and c = c and b = "x@[N]" and d = "y", OF ac len_c_y]
then have a: "a = x @ [N] @ ?y" by auto
from split have bc: "b @ c = (x @ α) @ y" by auto
note cancel_suffix[where a=b and c = c and b = "x@α" and d = "y", OF bc len_c_y]
then have b: "b = x @ α @ ?y" by auto
from split len_c_y a b show ?thesis
apply (simp only: Derives1_def)
apply (rule_tac x=x in exI)
apply (rule_tac x="?y" in exI)
apply (rule_tac x="N" in exI)
apply (rule_tac x="α" in exI)
apply auto
by (rule is_sentence_take)
qed
lemma drop_cancel_suffix: "a@c = drop n (b@c) ⟹ a = drop n b"
proof -
assume a1: "a @ c = drop n (b @ c)"
have "length (drop n b) = length b + length c - n - length c"
by (metis add_diff_cancel_right' diff_commute length_drop)
then show ?thesis
using a1 by (metis add_diff_cancel_right' append_eq_append_conv drop_append
length_append length_drop)
qed
lemma drop_keep_last: "u ≠ [] ⟹ u = drop n (a@[X]) ⟹ u = drop n a @ [X]"
by (metis append_take_drop_id drop_butlast last_appendR snoc_eq_iff_butlast)
lemma Derives1_X_is_part_of_rule[consumes 2, case_names Suffix Prefix]:
assumes aXb: "Derives1 δ i r (a@[X]@b)"
assumes split: "splits_at δ i α N β"
assumes prefix: "⋀ β. δ = a @ [X] @ β ⟹ length a < i ⟹
Derives1 β (i - length a - 1) r b ⟹ False"
assumes suffix: "⋀ α. δ = α @ [X] @ b ⟹ Derives1 α i r a ⟹ False"
shows "∃ u v. a = α @ u ∧ b = v @ β ∧ (snd r) = u@[X]@v"
proof -
have prefix_or: "is_prefix α a ∨ is_proper_prefix a α"
by (metis Derives1_prefix split aXb is_prefix_eq_proper_prefix)
have "is_proper_prefix a α ⟹ False"
proof -
assume proper:"is_proper_prefix a α"
then have "∃ u. u ≠ [] ∧ α = a@u" by (metis is_proper_prefix_def)
then obtain u where u: "u ≠ [] ∧ α = a@u" by blast
note splits_at = splits_at_α[OF aXb split] splits_at_combine[OF split]
from splits_at have α1: "α = take i δ" by blast
from splits_at have α2: "α = take i (a@[X]@b)" by blast
from splits_at have lenα: "length α = i" by blast
with proper have lena: "length a < i"
using append_eq_conv_conj drop_eq_Nil leI u by auto
from u α2 have "a@u = take i (a@[X]@b)" by auto
with lena have "u = take (i - length a) ([X]@b)" by (simp add: less_or_eq_imp_le)
with lena have uX: "u = [X]@(take (i - length a - 1) b)" by (simp add: not_less take_Cons')
let ?β = "(take (i - length a - 1) b) @ [N] @ β"
from splits_at have f1: "δ = α @ [N] @ β" by blast
with u uX have f2: "δ = a @ [X] @ ?β" by simp
note skip = Derives1_skip_prefix[where a = "a @ [X]" and b = "?β" and
r = r and i = i and c = b]
then have D: "Derives1 ?β (i - length a - 1) r b"
using One_nat_def Suc_leI aXb append_assoc diff_diff_left f2 lena length_Cons
length_append length_append_singleton list.size(3) by fastforce
note prefix[OF f2 lena D]
then show "False" .
qed
with prefix_or have is_prefix: "is_prefix α a" by blast
from aXb have aXb': "Derives1 δ i r ((a@[X])@b)" by auto
note Derives1_suffix[OF aXb' split]
then have suffix_or: "is_suffix β b ∨ is_proper_suffix b β"
by (metis is_suffix_eq_proper_suffix)
have "is_proper_suffix b β ⟹ False"
proof -
assume proper: "is_proper_suffix b β"
then have "∃ u. u ≠ [] ∧ β = u@b" by (metis is_proper_suffix_def)
then obtain u where u: "u ≠ [] ∧ β = u@b" by blast
note splits_at = splits_at_β[OF aXb split] splits_at_combine[OF split]
from splits_at have β1: "β = drop (Suc i) δ" by blast
from splits_at have β2: "β = drop (i + length (snd r)) (a @ [X] @ b)" by blast
from splits_at have lenβ: "length β = length δ - i - 1" by blast
with proper have lenb: "length b < length β" by (metis is_proper_suffix_length_cmp)
from u β2 have "u@b = drop (i + length (snd r)) ((a @ [X]) @ b)" by auto
hence "u = drop (i + length (snd r)) (a @ [X])"
by (metis drop_cancel_suffix)
hence uX: "u = drop (i + length (snd r)) a @ [X]" by (metis drop_keep_last u)
let ?α = "α @ [N] @ (drop (i + length (snd r)) a)"
from splits_at have f1: "δ = α @ [N] @ β" by blast
with u uX have f2: "δ = ?α @ [X] @ b" by simp
note skip = Derives1_skip_suffix[where a = "?α" and c = "[X]@b" and b="a" and
r = r and i = i]
have f3: "i < length (α @ [N] @ drop (i + length (snd r)) a)"
proof -
have f1: "1 + i + length b = length [X] + length b + i"
by (metis Groups.add_ac(2) Suc_eq_plus1_left length_Cons list.size(3) list.size(4) semiring_normalization_rules(22))
have f2: "length δ - i - 1 = length ((α @ [N] @ drop (i + length (snd r)) a) @ [X] @ b) - Suc i"
by (metis f2 length_drop splits_at(1))
have "length ([]::symbol list) ≠ length δ - i - 1 - length b"
by (metis add_diff_cancel_right' append_Nil2 append_eq_append_conv lenβ length_append u)
then have "length ([]::symbol list) ≠ length α + length ([N] @ drop (i + length (snd r)) a) - i"
using f2 f1 by (metis Suc_eq_plus1_left add_diff_cancel_right' diff_diff_left length_append)
then show ?thesis
by auto
qed
from aXb f2 have D: "Derives1 (?α @ [X] @ b) i r (a@[X]@b)" by auto
note skip[OF f3 D]
note suffix[OF f2 skip[OF f3 D]]
then show "False" .
qed
with suffix_or have is_suffix: "is_suffix β b" by blast
from is_prefix have "∃ u. a = α @ u" by (auto simp add: is_prefix_def)
then obtain u where u: "a = α @ u" by blast
from is_suffix have "∃ v. b = v @ β" by (auto simp add: is_suffix_def)
then obtain v where v: "b = v @ β" by blast
from u v splits_at_combine[OF split] aXb have D:"Derives1 (α@[N]@β) i r (α@(u@[X]@v)@β)"
by simp
from splits_at_α[OF aXb split] have i: "length α = i" by blast
from i have i1: "length α ≤ i" and i2: "i ≤ length α" by auto
note Derives1_skip_suffix[OF _ Derives1_skip_prefix[OF i1 D], simplified, OF i2]
then have "Derives1 [N] 0 r (u @ [X] @ v)" by auto
then have r: "snd r = u @ [X] @ v"
by (metis Derives1_split append_Cons append_Nil length_0_conv list.inject self_append_conv)
show ?thesis using u v r by auto
qed
lemma ℒ⇩P_derives: "a ∈ ℒ⇩P ⟹ ∃ b. derives [𝔖] (a@b)"
by (simp add: ℒ⇩P_def is_derivation_def)
lemma ℒ⇩P_leftderives: "a ∈ ℒ⇩P ⟹ ∃ b. leftderives [𝔖] (a@b)"
by (metis ℒ⇩P_derives ℒ⇩P_is_word derives_implies_leftderives_gen)
lemma Derives1_rule: "Derives1 a i r b ⟹ r ∈ ℜ"
by (auto simp add: Derives1_def)
lemma is_prefix_empty[simp]: "is_prefix [] a"
by (simp add: is_prefix_def)
lemma is_prefix_cons: "is_prefix (x # a) b = (∃ c. b = x # c ∧ is_prefix a c)"
by (metis append_Cons is_prefix_def)
lemma is_prefix_cancel[simp]: "is_prefix (a@b) (a@c) = is_prefix b c"
by (metis append_assoc is_prefix_def same_append_eq)
lemma is_prefix_chars: "is_prefix a b ⟹ is_prefix (chars a) (chars b)"
proof (induct a arbitrary: b)
case Nil thus ?case by simp
next
case (Cons x a)
from Cons(2) have "∃ c. b = x # c ∧ is_prefix a c"
by (simp add: is_prefix_cons)
then obtain c where c: "b = x # c ∧ is_prefix a c" by blast
from c Cons(1) show ?case by simp
qed
lemma is_prefix_length: "is_prefix a b ⟹ length a ≤ length b"
by (auto simp add: is_prefix_def)
lemma is_prefix_take[simp]: "is_prefix (take n a) a"
apply (auto simp add: is_prefix_def)
apply (rule_tac x="drop n a" in exI)
by simp
lemma doc_tokens_length: "doc_tokens p ⟹ length (chars p) ≤ length Doc"
by (metis doc_tokens_def is_prefix_length)
fun count_terminals :: "sentence ⇒ nat" where
"count_terminals [] = 0"
| "count_terminals (x#xs) = (if (is_terminal x) then Suc (count_terminals xs) else (count_terminals xs))"
lemma count_terminals_upper_bound: "count_terminals p ≤ length p"
by (induct p, auto)
lemma count_terminals_append[simp]: "count_terminals (a@b) = count_terminals a + count_terminals b"
by (induct a arbitrary: b, auto)
lemma Derives1_count_terminals:
assumes D: "Derives1 a i r b"
shows "count_terminals b = count_terminals a + count_terminals (snd r)"
proof -
have "∃ α N β. splits_at a i α N β" using D splits_at_ex by simp
then obtain α N β where split: "splits_at a i α N β" by blast
from D split have N: "is_nonterminal N" by (simp add: Derives1_nonterminal)
have a: "a = α @ [N] @ β" by (metis split splits_at_combine)
from D split have b: "b = α @ (snd r) @ β" using splits_at_combine_dest by simp
show ?thesis
apply (simp add: a b)
using N by (metis is_terminal_nonterminal)
qed
lemma Derives1_count_terminals_leq:
assumes D: "Derives1 a i r b"
shows "count_terminals a ≤ count_terminals b"
by (metis Derives1_count_terminals assms le_less_linear not_add_less1)
lemma Derivation_count_terminals_leq:
"Derivation a E b ⟹ count_terminals a ≤ count_terminals b"
proof (induct E arbitrary: a)
case Nil thus ?case by auto
next
case (Cons e E)
then have "∃ x i r. Derives1 a i r x ∧ Derivation x E b" using Derivation.simps(2) by blast
then obtain x i r where axb: "Derives1 a i r x ∧ Derivation x E b" by blast
from axb have ax: "count_terminals a ≤ count_terminals x"
using Derives1_count_terminals_leq by blast
from axb have xb: "count_terminals x ≤ count_terminals b" using Cons by simp
show ?case using ax xb by arith
qed
lemma derives_count_terminals_leq: "derives a b ⟹ count_terminals a ≤ count_terminals b"
using Derivation_count_terminals_leq derives_implies_Derivation by force
lemma is_word_cons[simp]: "is_word (x#xs) = (is_terminal x ∧ is_word xs)"
by (simp add: is_word_def)
lemma count_terminals_of_word: "is_word w ⟹ count_terminals w = length w"
by (induct w, auto)
lemma length_terminals[simp]: "length (terminals p) = length p"
by (auto simp add: terminals_def)
lemma path_length_is_upper_bound:
assumes p: "wellformed_tokens p"
assumes α: "is_word α"
assumes derives: "derives (α@u) (terminals p)"
shows "length α ≤ length p"
proof -
have counts: "count_terminals α ≤ count_terminals (terminals p)"
using derives derives_count_terminals_leq by fastforce
have len1: "length α = count_terminals α" by (simp add: α count_terminals_of_word)
have len2: "length (terminals p) = count_terminals (terminals p)"
by (simp add: count_terminals_of_word is_word_terminals p)
show ?thesis using counts len1 len2 by auto
qed
lemma is_word_Derives1_index:
assumes w: "is_word w"
assumes derives1: "Derives1 (w@a) i r b"
shows "i ≥ length w"
proof -
from derives1 have n: "is_nonterminal ((w@a) ! i)"
using Derives1_nonterminal splits_at_def splits_at_ex by auto
from w have t: "i < length w ⟹ is_terminal ((w@a) ! i)"
by (simp add: is_word_is_terminal nth_append)
show ?thesis
by (metis t n is_terminal_nonterminal less_le_not_le nat_le_linear)
qed
lemma is_word_Derivation_derivation_ge:
assumes w: "is_word w"
assumes D: "Derivation (w@a) D b"
shows "derivation_ge D (length w)"
by (metis D Derivation_leftmost derivation_ge_empty leftmost_Derivation leftmost_append w)
lemma derives_word_is_prefix:
assumes w: "is_word w"
assumes derives: "derives (w@a) b"
shows "is_prefix w b"
by (metis Derivation_take append_eq_conv_conj derives derives_implies_Derivation
is_prefix_take is_word_Derivation_derivation_ge w)
lemma terminals_take[simp]: "terminals (take n p) = take n (terminals p)"
by (simp add: take_map terminals_def)
lemma terminals_drop[simp]: "terminals (drop n p) = drop n (terminals p)"
by (simp add: drop_map terminals_def)
lemma take_prefix[simp]: "is_prefix a b ⟹ take (length a) b = a"
by (metis append_eq_conv_conj is_prefix_unsplit)
lemma Derives1_drop_prefixword:
assumes w: "is_word w"
assumes wa_b: "Derives1 (w@a) i r b"
shows "Derives1 a (i - length w) r (drop (length w) b)"
proof -
have i: "length w ≤ i" using wa_b is_word_Derives1_index w by blast
have "is_prefix w b" by (metis append_eq_conv_conj i is_prefix_take le_Derives1_take wa_b)
then have b: "b = w @ (drop (length w) b)" by (simp add: is_prefix_unsplit)
show ?thesis
apply (rule_tac Derives1_skip_prefix[OF i])
by (simp add: b[symmetric] wa_b)
qed
lemma derives1_drop_prefixword:
assumes w: "is_word w"
assumes wa_b: "derives1 (w@a) b"
shows "derives1 a (drop (length w) b)"
by (metis Derives1_drop_prefixword Derives1_implies_derives1 derives1_implies_Derives1 w wa_b)
lemma derives1_is_word_is_prefix_drop:
assumes w: "is_word w"
assumes w_a: "is_prefix w a"
assumes ab: "derives1 a b"
shows "derives1 (drop (length w) a) (drop (length w) b)"
by (metis ab append_take_drop_id derives1_drop_prefixword take_prefix w w_a)
lemma derives_drop_prefixword_helper:
"derives a b ⟹ is_word w ⟹ is_prefix w a ⟹ derives (drop (length w) a) (drop (length w) b)"
proof (induct rule: derives_induct)
case Base thus ?case by auto
next
case (Step y z)
have is_prefix_w_y: "is_prefix w y"
by (metis Step.hyps(1) Step.prems(1) Step.prems(2) derives_word_is_prefix is_prefix_def)
thus ?case
by (metis Step.hyps(2) Step.hyps(3) Step.prems(1) Step.prems(2) derives1_implies_derives
derives1_is_word_is_prefix_drop derives_trans)
qed
lemma derive_drop_prefixword:
"is_word w ⟹ derives (w@a) b ⟹ derives a (drop (length w) b)"
by (metis append_eq_conv_conj derives_drop_prefixword_helper is_prefix_take)
lemma thmD2':
assumes X: "is_terminal X"
assumes p: "doc_tokens p"
assumes pX: "(terminals p)@[X] ∈ ℒ⇩P"
shows "∃ x. pvalid p x ∧ next_symbol x = Some X"
proof -
from p have wellformed_p: "wellformed_tokens p" by (simp add: doc_tokens_def)
have "∃ ω. leftderives [𝔖] (((terminals p)@[X]) @ ω)" using ℒ⇩P_leftderives pX by blast
then obtain ω where "leftderives [𝔖] (((terminals p)@[X]) @ ω)" by blast
then have "∃ D. LeftDerivation [𝔖] D (((terminals p)@[X]) @ ω)"
using leftderives_implies_LeftDerivation by blast
then obtain D where D: "LeftDerivation [𝔖] D (((terminals p)@[X]) @ ω)" by blast
let ?P = "λ k. (∃ a b. LeftDerivation [𝔖] (take k D) (a@[X]@b) ∧ derives a (terminals p))"
have "?P (length D)"
apply (rule_tac x="terminals p" in exI)
apply (rule_tac x="ω" in exI)
using D by simp
then show ?thesis
proof (induct rule: minimal_witness[where P="?P"])
case (Minimal K)
from Minimal(2) obtain a b where
aXb: "LeftDerivation [𝔖] (take K D) (a @ [X] @ b)" and
a: "derives a (terminals p)" by blast
have KD: "K > 0 ∧ length D > 0"
proof (cases "K = 0 ∨ length D = 0")
case True
hence "take K D = []" by auto
with True aXb have "[𝔖] = a @ [X] @ b" by simp
hence "𝔖 = X"
by (metis Nil_is_append_conv append_self_conv2 butlast.simps(2)
butlast_append hd_append2 list.sel(1) not_Cons_self2)
then have "False"
using X is_nonterminal_startsymbol is_terminal_nonterminal by auto
then show ?thesis by blast
next
case False thus ?thesis by arith
qed
then have "take K D = take (K - 1) D @ [D ! (K - 1)]"
by (metis Minimal.hyps(1) One_nat_def Suc_less_eq Suc_pred hd_drop_conv_nth
le_imp_less_Suc take_hd_drop)
then have "∃ δ. LeftDerivation [𝔖] (take (K - 1) D) δ ∧ LeftDerivation δ [D ! (K - 1)] (a@[X]@b)"
by (metis LeftDerivation_append aXb)
then obtain δ where
δ1: "LeftDerivation [𝔖] (take (K - 1) D) δ"
and δ2: "LeftDerivation δ [D ! (K - 1)] (a@[X]@b)"
by blast
from δ2 have "∃ i r. LeftDerives1 δ i r (a@[X]@b)" by fastforce
then obtain i r where LeftDerives1_δ: "LeftDerives1 δ i r (a@[X]@b)" by blast
then have Derives1_δ: "Derives1 δ i r (a@[X]@b)"
by (metis LeftDerives1_implies_Derives1)
then have "∃ α N β . splits_at δ i α N β" by (simp add: splits_at_ex)
then obtain α N β where split_δ: "splits_at δ i α N β" by blast
have is_word_α: "is_word α" by (metis LeftDerives1_δ LeftDerives1_splits_at_is_word split_δ)
have "¬ (?P (K - 1))" using KD Minimal(3) by auto
with δ1 have min_δ: "¬ (∃ a b. δ = a@[X]@b ∧ derives a (terminals p))" by blast
from Derives1_δ split_δ have "∃ u v. a = α @ u ∧ b = v @ β ∧ (snd r) = u@[X]@v"
proof (induction rule: Derives1_X_is_part_of_rule)
case (Suffix γ)
from min_δ Suffix(1) a show ?case by auto
next
case (Prefix γ)
have "derives γ (terminals p)"
by (metis Derives1_implies_derives1 Prefix(2) a
derives1_implies_derives derives_trans)
with min_δ Prefix(1) show ?case by auto
qed
then obtain u v where uXv: "a = α @ u ∧ b = v @ β ∧ (snd r) = u@[X]@v" by blast
let ?l = "length α"
let ?q = "take ?l p"
let ?x = "Item r (length u) (charslength ?q) (charslength p)"
have "item_rhs ?x = snd r" by (simp add: item_rhs_def)
then have item_rhs_x: "item_rhs ?x = u@[X]@v" using uXv by simp
have wellformed_x: "wellformed_item ?x"
apply (auto simp add: wellformed_item_def)
apply (metis Derives1_δ Derives1_rule)
apply (rule is_prefix_length)
apply (rule is_prefix_chars)
apply simp
apply (simp add: doc_tokens_length[OF p])
using item_rhs_x by simp
from item_rhs_x have next_symbol_x: "next_symbol ?x = Some X"
by (auto simp add: next_symbol_def is_complete_def)
have len_α_p: "length α ≤ length p"
apply (rule_tac path_length_is_upper_bound[where u=u])
apply (simp add: wellformed_p)
apply (simp add: is_word_α)
using a uXv by blast
have item_nonterminal_x: "item_nonterminal ?x = N"
apply (simp add: item_nonterminal_def)
using Derives1_δ Derives1_nonterminal split_δ by blast
have take_terminals: "take (length α) (terminals p) = α"
apply (rule_tac take_prefix)
using a derives_word_is_prefix is_word_α uXv by blast
have item_α_x: "item_α ?x = u" using item_α_def item_rhs_x by auto
from wellformed_x next_symbol_x len_α_p show ?thesis
apply (rule_tac x="?x" in exI)
apply (auto simp add: pvalid_def wellformed_p)
apply (rule_tac x="length α" in exI)
apply (auto)
using item_nonterminal_x apply (simp)
apply (simp add: take_terminals)
apply (rule_tac x="β" in exI)
using LeftDerivation_implies_leftderives δ1 is_leftderivation_def split_δ splits_at_combine
apply auto[1]
using item_α_x apply simp
by (metis a derive_drop_prefixword is_word_α uXv)
qed
qed
lemma admissible_wellformed_tokens: "admissible p ⟹ wellformed_tokens p"
by (auto simp add: admissible_def ℒ⇩P_wellformed_tokens)
lemma chars_append[simp]: "chars (a@b) = (chars a)@(chars b)"
by (induct a arbitrary: b, auto)
lemma chars_of_token_simp[simp]: "chars_of_token (a, b) = b"
by (simp add: chars_of_token_def)
lemma 𝒳_is_prefix: "t ∈ 𝒳 k ⟹ is_prefix (snd t) (drop k Doc)"
by (auto simp add: 𝒳_def)
lemma is_prefix_append: "is_prefix (a@b) D = (is_prefix a D ∧ is_prefix b (drop (length a) D))"
by (metis append_assoc is_prefix_cancel is_prefix_def is_prefix_unsplit)
lemma 𝔓_are_doc_tokens: "p ∈ 𝔓 ⟹ doc_tokens p"
proof (induct rule: 𝔓_induct)
case Base thus ?case
by (simp add: doc_tokens_def wellformed_tokens_def)
next
case (Induct p k u)
from Induct(2)[simplified] show ?case
proof (induct rule: limit_induct)
case (Init p) from Induct(1)[OF Init] show ?case .
next
case (Iterate p Y)
have Y_is_prefix: "⋀ p. p ∈ Y ⟹ is_prefix (chars p) Doc"
apply (drule Iterate(1))
by (simp add: doc_tokens_def)
have "𝒴 (𝒵 k u) (𝒫 k u) k ⊆ 𝒳 k" by (metis 𝒵.simps(2) 𝒵_subset_𝒳)
then have 1: "Append (𝒴 (𝒵 k u) (𝒫 k u) k) k Y ⊆ Append (𝒳 k) k Y"
by (rule Append_mono, simp)
have 2: "p ∈ Append (𝒳 k) k Y ⟹ doc_tokens p"
apply (auto simp add: Append_def)
apply (simp add: Iterate)
apply (auto simp add: doc_tokens_def admissible_wellformed_tokens
is_prefix_append Y_is_prefix)
by (metis 𝒳_is_prefix snd_conv)
show ?case
apply (rule 2)
by (metis (mono_tags, lifting) "1" Iterate(2) subsetCE)
qed
qed
theorem thmD2:
assumes X: "is_terminal X"
assumes p: "p ∈ 𝔓"
assumes pX: "(terminals p)@[X] ∈ ℒ⇩P"
shows "∃ x. pvalid p x ∧ next_symbol x = Some X"
by (metis X 𝔓_are_doc_tokens p pX thmD2')
end
end