Theory TheoremD11
theory TheoremD11
imports TheoremD10
begin
context LocalLexing begin
lemma LeftDerivationLadder_length_1:
assumes ladder: "LeftDerivationLadder α D L γ"
assumes singleton_L: "length L = 1"
shows "LeftDerivationFix α (ladder_i L 0) D (ladder_last_j L) γ"
proof -
have ldfix: "LeftDerivationFix α (ladder_i L 0) (take (ladder_n L 0) D) (ladder_j L 0)
(ladder_γ α D L 0)"
using ladder LeftDerivationLadder_def by blast
have ladder_n_0: "ladder_n L 0 = length D"
using ladder singleton_L
by (metis LeftDerivationLadder_def One_nat_def diff_Suc_1 is_ladder_def ladder_last_n_intro)
from ldfix ladder_n_0 ladder singleton_L show ?thesis
by (metis Derivation_unique_dest LeftDerivationLadder_def
LeftDerivationLadder_implies_LeftDerivation_at_index LeftDerivationLadder_ladder_n_bound
LeftDerivation_implies_Derivation One_nat_def diff_Suc_1 ladder_last_j_def take_all
zero_less_one)
qed
lemma LeftDerivationFix_from_singleton_helper:
assumes "LeftDerivationFix [A] 0 D (length u) (u @ [B] @ v)"
shows "D = []"
proof -
from iffD1[OF LeftDerivationFix_def assms] obtain E F where EF:
"is_sentence [A] ∧
is_sentence (u @ [B] @ v) ∧
LeftDerivation [A] D (u @ [B] @ v) ∧
0 < length [A] ∧
length u < length (u @ [B] @ v) ∧
[A] ! 0 = (u @ [B] @ v) ! length u ∧
D = E @ derivation_shift F 0 (Suc (length u)) ∧
LeftDerivation (take 0 [A]) E (take (length u) (u @ [B] @ v)) ∧
LeftDerivation (drop (Suc 0) [A]) F (drop (Suc (length u)) (u @ [B] @ v))"
by blast
from EF have E: "E = []"
by (metis Derivation.elims(2) Derives1_split LeftDerivation_implies_Derivation
Nil_is_append_conv list.distinct(1) take_0)
from EF have F: "F = []"
by (metis E LeftDerivation.simps(1) LeftDerivation_ge_take LeftDerivation_implies_Derivation
append_eq_conv_conj derivation_ge_shift is_word_Derivation length_Cons length_derivation_shift
list.size(3) nth_Cons_0 nth_append self_append_conv2 take_0)
from EF E F show "D = []" by auto
qed
lemma LeftDerivationFix_from_singleton:
assumes "LeftDerivationFix [A] i D j γ"
shows "D = []"
proof -
have "∃ u B v. splits_at γ j u B v" using assms
using LeftDerivationFix_splits_at_derives by blast
then obtain u B v where s: "splits_at γ j u B v" by blast
from s have s1: "γ = u @ [B] @ v" using splits_at_combine by blast
from s have s2: "j = length u" using splits_at_def by auto
from assms s1 s2 LeftDerivationFix_from_singleton_helper
show ?thesis by (metis LeftDerivationFix_def length_Cons less_Suc0 list.size(3))
qed
lemma LeftDerivationLadder_ladder_γ_last:
assumes "LeftDerivationLadder α D L γ"
shows "γ = ladder_γ α D L (length L - 1)"
by (metis Derive LeftDerivationLadder_def LeftDerivation_implies_Derivation One_nat_def assms
is_ladder_def last_ladder_γ)
theorem thmD11_helper:
"p ∈ 𝔓 ⟹
charslength p = k ⟹
X ∈ T ⟹
T ⊆ 𝒳 k ⟹
q = p @ [X] ⟹
(N, α@β) ∈ ℜ ⟹
r ≤ length q ⟹
LeftDerivation [𝔖] D ((terminals (take r q))@[N]@γ) ⟹
leftderives α (terminals (drop r q)) ⟹
k' = k + length (chars_of_token X) ⟹
x = Item (N, α@β) (length α) (charslength (take r q)) k' ⟹
I = items_le k' (π k' {} (Scan T k (Gen (Prefixes p)))) ⟹
x ∈ I"
proof (induct "length D" arbitrary: D r N γ α β x rule: less_induct)
case less
have "D = [] ∨ D ≠ []" by blast
then show ?case
proof (induct rule: disjCases2)
case 1
then have r: "r = 0"
by (metis LeftDerivation.simps(1) diff_add_0 diff_add_inverse2 le_0_eq length_0_conv
length_append length_terminals less.prems(7) less.prems(8) list.size(4) take_eq_Nil)
with 1 have γ: "γ = []"
using LeftDerivation.simps(1) append_Cons append_self_conv2 less.prems(8) list.inject
take_eq_Nil terminals_empty by auto
from r γ 1 have start_is_N: "𝔖 = N"
using LeftDerivation.simps(1) append_eq_Cons_conv less.prems(8) list.inject take_eq_Nil
terminals_empty by auto
have h1: "r ≤ length p" using r by auto
have h2: "leftderives [𝔖] (terminals (take r p) @ [N] @ γ)"
by (simp add: r γ start_is_N)
have h3: "leftderives α (terminals (drop r p @ [X]))"
using "less.prems" by (simp add: r "less.prems")
have h4: "x = Item (N, α @ β) (length α) (charslength (take r p)) k'"
using "less.prems" by (simp add: r "less.prems")
from thmD10[OF "less.prems"(1, 2, 3, 4, 6) h1 h2 h3 "less.prems"(10) h4 "less.prems"(12)]
show ?case .
next
case 2
note D_non_empty = 2
have "r < length q ∨ r = length q" using less by arith
then show ?case
proof (induct rule: disjCases2)
case 1
have h1: "r ≤ length p" using less.prems 1 by auto
have take_q_p: "take r q = take r p"
using 1 less.prems
by (simp add: drop_keep_last le_neq_implies_less nat_le_linear not_less_eq not_less_eq_eq)
have h2: "leftderives [𝔖] (terminals (take r p) @ [N] @ γ)"
apply (simp only: take_q_p[symmetric])
using less.prems LeftDerivation_implies_leftderives by blast
have h3: "leftderives α (terminals (drop r p @ [X]))"
using less.prems(5, 9) h1 by simp
have h4: "k' = k + length (chars_of_token X)" using less.prems by blast
have h5: "x = Item (N, α @ β) (length α) (charslength (take r p)) k'"
using less.prems take_q_p by simp
from thmD10[OF "less.prems"(1, 2, 3, 4, 6) h1 h2 h3 h4 h5 less.prems(12)] show ?case .
next
case 2
from 2 have ld: "LeftDerivation [𝔖] D (terminals q @ [N] @ γ)"
using less.prems(8) by auto
from 2 have α_derives_empty: "derives α []"
using less.prems(9) by auto
have is_sentence_p: "is_sentence (terminals p)"
using less.prems(1) ℒ⇩P_derives 𝔓_are_admissible admissible_def is_derivation_def
is_derivation_is_sentence is_sentence_concat by blast
have is_symbol_X: "is_symbol (terminal_of_token X)"
using less.prems(3, 4) 𝒳_are_terminals is_symbol_def rev_subsetD by blast
have is_sentence_q: "is_sentence (terminals q)" using is_sentence_p is_symbol_X
less.prems LeftDerivation_implies_leftderives is_derivation_def
is_derivation_is_sentence is_sentence_concat ld leftderives_implies_derives by blast
have is_symbol_N: "is_symbol N"
using less.prems(6) is_symbol_def rule_nonterminal_type by blast
have is_sentence_γ: "is_sentence γ"
by (meson LeftDerivation_implies_leftderives is_derivation_def is_derivation_is_sentence
is_sentence_concat ld leftderives_implies_derives)
have ld_exists_h1: "is_sentence (terminals q @ [N] @ γ)"
using is_sentence_q is_sentence_γ is_symbol_N is_sentence_concat
LeftDerivation_implies_leftderives is_derivation_def is_derivation_is_sentence ld
leftderives_implies_derives by blast
have ld_exists_h2: "length q < length (terminals q @ [N] @ γ)" by simp
from LeftDerivationLadder_exists[OF ld ld_exists_h1 ld_exists_h2] obtain L where
L: "LeftDerivationLadder [𝔖] D L (terminals q @ [N] @ γ)" and
L_last_j: "ladder_last_j L = length q" by blast
note r_eq_length_q = 2
have ladder_i_0_eq_0: "ladder_i L 0 = 0" using L append_Nil ladder_i_0_bound
length_append_singleton less_Suc0 list.size(3) by fastforce
have "length L = 1 ∨ length L > 1" using L
by (metis LeftDerivationLadder_def Suc_eq_plus1 Suc_eq_plus1_left butlast_conv_take
butlast_snoc diff_add_inverse2 is_ladder_def le_add1 le_neq_implies_less
length_append_singleton old.nat.exhaust take_0)
then show ?case
proof (induct rule: disjCases2)
case 1
from LeftDerivationLadder_length_1[OF L 1] ladder_i_0_eq_0
have ldfix: "LeftDerivationFix [𝔖] 0 D (ladder_last_j L) (terminals q @ [N] @ γ)"
by auto
with LeftDerivationFix_from_singleton have "D = []" by blast
with D_non_empty have "False" by auto
then show ?case by blast
next
case 2
obtain a where a: "a = ladder_α [𝔖] D L (length L - 1)" by blast
then have a_as_γ: "a = ladder_γ [𝔖] D L (length L - 2)" using 2 ladder_α_def
by (metis diff_diff_left diff_is_0_eq not_le one_add_one)
have introsAt: "LeftDerivationIntrosAt [𝔖] D L (length L - 1)" using L
by (metis "2.hyps" LeftDerivationIntros_def LeftDerivationLadder_def One_nat_def
Suc_leI Suc_lessD diff_less less_not_refl not_less_eq zero_less_diff)
obtain i where i: "i = ladder_i L (length L - 1)" by blast
obtain j where j: "j = ladder_j L (length L - 1)" by blast
obtain ix where ix: "ix = ladder_ix L (length L - 1)" by blast
obtain c where c: "c = ladder_γ [𝔖] D L (length L - 1)" by blast
obtain n where n: "n = ladder_n L (length L - 1 - 1)" by blast
obtain m where m: "m = ladder_n L (length L - 1)" by blast
obtain e where e: "e = D ! n" by blast
obtain E where E: "E = drop (Suc n) (take m D)" by blast
from iffD1[OF LeftDerivationIntrosAt_def introsAt]
have "i = fst e ∧ LeftDerivationIntro a i (snd e) ix E j c"
by (metis E a c e i ix j m n)
then have i_eq_fst_e: "i = fst e" and
ldintro: "LeftDerivationIntro a i (snd e) ix E j c" by auto
have c_def: "c = terminals q @ [N] @ γ"
using c L LeftDerivationLadder_ladder_γ_last by simp
from iffD1[OF LeftDerivationIntro_def ldintro] obtain b where b:
"LeftDerives1 a i (snd e) b ∧ ix < length (snd (snd e)) ∧
snd (snd e) ! ix = c ! j ∧ LeftDerivationFix b (i + ix) E j c" by blast
obtain M ω where Mω: "(M, ω) = snd e" using prod.collapse by blast
have j_q: "j = length q" using L_last_j j ladder_last_j_def by auto
with c_def have c_at_j: "c ! j = N"
by (metis append_Cons length_terminals nth_append_length)
with b Mω have ω_at_ix: "ω ! ix = N" by (metis snd_conv)
obtain μ1 μ2 where split_ω: "splits_at ω ix μ1 N μ2"
by (metis Mω ω_at_ix b snd_conv splits_at_def)
obtain a1 a2 where split_a: "splits_at a i a1 M a2" using b
by (metis LeftDerivationIntro_bounds_ij LeftDerivationIntro_examine_rule Mω
fst_conv ldintro splits_at_def)
then have is_word_a1: "is_word a1"
using LeftDerives1_splits_at_is_word b by blast
have "b = a1 @ ω @ a2" using split_a b Mω
by (metis LeftDerives1_implies_Derives1 snd_conv splits_at_combine_dest)
then have b_def: "b = a1 @ μ1 @ [N] @ μ2 @ a2" using split_ω splits_at_combine
by simp
have is_nonterminal_N: "is_nonterminal N"
using less.prems(6) rule_nonterminal_type by blast
with LeftDerivationFix_splits_at_nonterminal split_a b
have "∃ U b1 b2 c1. splits_at b (i + ix) b1 U b2 ∧ splits_at c j c1 U b2 ∧
LeftDerivation b1 E c1" by (simp add: LeftDerivationFix_def c_at_j)
then obtain b1 b2 c1 where b1b2c1:
"splits_at b (i + ix) b1 N b2 ∧ splits_at c j c1 N b2 ∧
LeftDerivation b1 E c1" using c_at_j splits_at_def by auto
then have c1_q: "c1 = terminals q" using c_def j_q
by (simp add: append_eq_conv_conj splits_at_def)
have length_a1_eq_i: "length a1 = i" using split_a splits_at_def by auto
have length_μ1_eq_ix: "length μ1 = ix" using split_ω splits_at_def by auto
have "b1 = take (i + ix) b" using b1b2c1 splits_at_def by blast
then have b1_eq_a1_μ1: "b1 = a1 @ μ1" using b_def length_a1_eq_i length_μ1_eq_ix
by (simp add: append_eq_conv_conj take_add)
have "LeftDerivation (a1 @ μ1) E c1" using b1b2c1 b1_eq_a1_μ1 by blast
from LeftDerivation_skip_prefixword_ex[OF this is_word_a1]
obtain w where w: "c1 = a1 @ w ∧
LeftDerivation μ1 (derivation_shift E (length a1) 0) w" by blast
have a1_eq_take_i: "a1 = take i (terminals q)"
using w c1_q split_a append_eq_conv_conj length_a1_eq_i by blast
have μ1_leftderives: "leftderives μ1 (terminals (drop i q))" using w c1_q split_a
LeftDerivation_implies_leftderives append_eq_conv_conj length_a1_eq_i by auto
have "LeftDerivation [𝔖] (take n D) a"
by (metis "2.hyps" L LeftDerivationLadder_implies_LeftDerivation_at_index
One_nat_def Suc_lessD a_as_γ diff_Suc_eq_diff_pred diff_Suc_less n numeral_2_eq_2)
then have LD_to_M: "LeftDerivation [𝔖] (take n D) ((terminals (take i q))@[M]@a2)"
using split_a splits_at_combine a1_eq_take_i terminals_take by auto
have is_ladder: "is_ladder D L" using L by (simp add: LeftDerivationLadder_def)
then have n_less_m: "n < m" using n m is_ladder_def
by (metis (no_types, lifting) "2.hyps" One_nat_def diff_Suc_less
length_greater_0_conv zero_less_diff)
have m_le_D: "m ≤ length D" using m is_ladder_def is_ladder dual_order.refl
ladder_n_last_is_length by auto
have "length (take n D) = n" using n_less_m m_le_D
using length_take less_irrefl less_le_trans linear min.absorb2 by auto
then have length_take_n_D: "length (take n D) < length D"
using n_less_m m_le_D less_le_trans by linarith
have ω_decompose: "ω = μ1@(N#μ2)" using split_ω splits_at_combine by simp
have "(M, ω) ∈ ℜ" by (metis Derives1_rule LeftDerives1_implies_Derives1 Mω b)
with ω_decompose have M_rule: "(M, μ1@(N#μ2)) ∈ ℜ" by simp
have i_le_q: "i ≤ length q" using a1_eq_take_i length_a1_eq_i by auto
obtain y where
y: "y = Item (M, μ1 @ N # μ2) (length μ1) (charslength (take i q)) k'" by blast
from less.hyps[OF length_take_n_D less.prems(1, 2, 3, 4, 5) M_rule i_le_q LD_to_M
μ1_leftderives less.prems(10) y less.prems(12)]
have y_in_I: "y ∈ I" by blast
obtain z where z: "z = Item (N, α@β) 0 k' k'" by blast
then have z_is_init_item: "z = init_item (N, α@β) k'" by (simp add: init_item_def)
have "z ∈ Predict k' {y}"
apply (simp add: z_is_init_item)
apply (rule next_symbol_predicts)
apply (simp add: is_complete_def next_symbol_def y)
apply (simp add: less.prems(6))
apply (simp add: y item_end_def)
done
then have "z ∈ Predict k' I" using Predict_def bin_def y_in_I by auto
then have z_in_I: "z ∈ I" by (metis Predict_π_fix items_le_Predict less.prems(12))
have length_chars_q: "length (chars q) = k'" using less.prems by simp
have x_is_inc_dot: "x = inc_dot (length α) z"
by (simp add: less.prems(11) r_eq_length_q length_chars_q z inc_dot_def)
have wellformed_items_I: "wellformed_items I"
apply (subst less.prems(12))
by (meson LocalLexing.items_le_is_filter LocalLexing.wellformed_items_Gen
LocalLexing_axioms empty_subsetI less.prems(4) subsetCE wellformed_items_Scan
wellformed_items_π wellformed_items_def)
with z_in_I have wellformed_z: "wellformed_item z"
using wellformed_items_def by blast
have item_β_z: "item_β z = α@β" by (simp add: z_is_init_item)
have item_end_z: "item_end z = k'" by (simp add: z_is_init_item)
have "x ∈ π k' {} {z}"
apply (simp add: x_is_inc_dot)
apply (rule thmD6)
apply (rule wellformed_z)
apply (rule item_β_z)
apply (rule item_end_z)
by (simp add: α_derives_empty)
then have "x ∈ π k' {} I" using z_in_I
by (meson contra_subsetD empty_subsetI insert_subset monoD mono_π)
then show ?case
by (metis (no_types, lifting) LocalLexing.wellformed_item_def LocalLexing_axioms
π_subset_elem_trans item.sel(3) item.sel(4) items_le_def items_le_is_filter
less.prems(11) less.prems(12) mem_Collect_eq wellformed_z z)
qed
qed
qed
qed
theorem thmD11:
assumes p_dom: "p ∈ 𝔓"
assumes p_charslength: "charslength p = k"
assumes X_dom: "X ∈ T"
assumes T_dom: "T ⊆ 𝒳 k"
assumes q_def: "q = p @ [X]"
assumes rule_dom: "(N, α@β) ∈ ℜ"
assumes r: "r ≤ length q"
assumes leftderives_start: "leftderives [𝔖] ((terminals (take r q))@[N]@γ)"
assumes leftderives_α: "leftderives α (terminals (drop r q))"
assumes k': "k' = k + length (chars_of_token X)"
assumes item_def: "x = Item (N, α@β) (length α) (charslength (take r q)) k'"
assumes I: "I = items_le k' (π k' {} (Scan T k (Gen (Prefixes p))))"
shows "x ∈ I"
proof -
have "∃ D. LeftDerivation [𝔖] D ((terminals (take r q))@[N]@γ)"
using leftderives_start leftderives_implies_LeftDerivation by blast
then obtain D where D: "LeftDerivation [𝔖] D ((terminals (take r q))@[N]@γ)" by blast
from thmD11_helper[OF assms(1, 2, 3, 4, 5, 6, 7) D assms(9, 10, 11, 12)]
show ?thesis .
qed
end
end