Theory TheoremD14
theory TheoremD14
imports TheoremD13
begin
context LocalLexing begin
lemma empty_tokens_of_empty[simp]: "empty_tokens {} = {}"
using empty_tokens_is_filter by blast
lemma items_le_split_via_eq: "items_le (Suc k) J = items_le k J ∪ items_eq (Suc k) J"
by (auto simp add: items_le_def items_eq_def)
lemma paths_le_split_via_eq: "paths_le (Suc k) P = paths_le k P ∪ paths_eq (Suc k) P"
by (auto simp add: paths_le_def paths_eq_def)
lemma natUnion_superset:
shows "g i ⊆ natUnion g"
by (meson natUnion_elem subset_eq)
definition indexle :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ bool" where
"indexle k' u' k u = ((indexlt k' u' k u) ∨ (k' = k ∧ u' = u))"
definition produced_by_scan_step :: "item ⇒ nat ⇒ nat ⇒ bool" where
"produced_by_scan_step x k u = (∃ k' u' y X. indexle k' u' k u ∧ y ∈ 𝒥 k' u' ∧
item_end y = k' ∧ X ∈ (𝒯 k' u') ∧ x = inc_item y (k' + length (chars_of_token X)) ∧
next_symbol y = Some (terminal_of_token X))"
lemma indexle_trans: "indexle k'' u'' k' u' ⟹ indexle k' u' k u ⟹ indexle k'' u'' k u"
using indexle_def indexlt_trans
proof -
assume a1: "indexle k'' u'' k' u'"
assume a2: "indexle k' u' k u"
then have f3: "⋀n na. u' = u ∨ indexlt n na k u ∨ ¬ indexlt n na k' u'"
by (meson indexle_def indexlt_trans)
have "⋀n na. k' = k ∨ indexlt n na k u ∨ ¬ indexlt n na k' u'"
using a2 by (meson indexle_def indexlt_trans)
then show ?thesis
using f3 a2 a1 indexle_def by auto
qed
lemma produced_by_scan_step_trans:
assumes "indexle k' u' k u"
assumes "produced_by_scan_step x k' u'"
shows "produced_by_scan_step x k u"
proof -
from iffD1[OF produced_by_scan_step_def assms(2)] obtain k'a u'a y X where produced_k'_u':
"indexle k'a u'a k' u' ∧
y ∈ 𝒥 k'a u'a ∧
item_end y = k'a ∧
X ∈ 𝒯 k'a u'a ∧
x = inc_item y (k'a + length (chars_of_token X)) ∧ next_symbol y = Some (terminal_of_token X)"
by blast
then show ?thesis using indexle_trans assms(1) produced_by_scan_step_def by blast
qed
lemma 𝒥_induct[consumes 1, case_names Induct]:
assumes "x ∈ 𝒥 k u"
assumes induct: "⋀ x k u . (⋀ x' k' u'. x' ∈ 𝒥 k' u' ⟹ indexlt k' u' k u ⟹ P x' k' u')
⟹ x ∈ 𝒥 k u ⟹ P x k u"
shows "P x k u"
proof -
let ?R = "indexlt_rel <*lex*> {}"
have wf_R: "wf ?R" by (auto simp add: wf_indexlt_rel)
let ?P = "λ a. snd a ∈ 𝒥 (fst (fst a)) (snd (fst a)) ⟶ P (snd a) (fst (fst a)) (snd (fst a))"
have "x ∈ 𝒥 k u ⟶ P x k u"
apply (rule wf_induct[OF wf_R, where P = ?P and a = "((k, u), x)", simplified])
apply (auto simp add: indexlt_def[symmetric])
apply (rule_tac x=ba and k=a and u=b in induct)
by auto
thus ?thesis using assms by auto
qed
lemma π_no_tokens_item_end:
assumes x_in_π: "x ∈ π k {} I"
shows "item_end x = k ∨ x ∈ I"
proof -
have x_in_limit: "x ∈ limit (λI. Complete k (Predict k I)) I"
using x_in_π π_no_tokens by auto
then show ?thesis
proof (induct rule: limit_induct)
case (Init x) then show ?case by auto
next
case (Iterate x J)
from Iterate(2) have "item_end x = k ∨ x ∈ Predict k J"
using Complete_item_end by auto
then show ?case
proof (induct rule: disjCases2)
case 1 then show ?case by blast
next
case 2
then have "item_end x = k ∨ x ∈ J"
using Predict_item_end by auto
then show ?case
proof (induct rule: disjCases2)
case 1 then show ?case by blast
next
case 2 then show ?case using Iterate(1)[OF 2] by blast
qed
qed
qed
qed
lemma natUnion_ex: "x ∈ natUnion f ⟹ ∃ i. x ∈ f i"
by (metis (no_types, opaque_lifting) mk_disjoint_insert natUnion_superset natUnion_upperbound
subsetCE subset_insert)
lemma locate_in_limit:
assumes x_in_limit: "x ∈ limit f X"
assumes x_notin_X: "x ∉ X"
shows "∃ n. x ∈ funpower f (Suc n) X ∧ x ∉ funpower f n X"
proof -
have "∃ N. x ∈ funpower f N X" using x_in_limit limit_def natUnion_ex by fastforce
then obtain N where N: "x ∈ funpower f N X" by blast
{
fix n :: nat
have "x ∈ funpower f n X ⟹ ∃ m < n. x ∈ funpower f (Suc m) X ∧ x ∉ funpower f m X"
proof (induct n)
case 0
with x_notin_X show ?case by auto
next
case (Suc n)
have "x ∉ funpower f n X ∨ x ∈ funpower f n X" by blast
then show ?case
proof (induct rule: disjCases2)
case 1
then show ?case using Suc by fastforce
next
case 2
from Suc(1)[OF 2] show ?case using less_SucI by blast
qed
qed
}
with N show ?thesis by auto
qed
lemma produced_by_scan_step:
"x ∈ 𝒥 k u ⟹ item_end x > k ⟹ produced_by_scan_step x k u"
proof (induct rule: 𝒥_induct)
case (Induct x k u)
have "(k = 0 ∧ u = 0) ∨ (k > 0 ∧ u = 0) ∨ (u > 0)" by arith
then show ?case
proof (induct rule: disjCases3)
case 1
with Induct have "item_end x = 0" using 𝒥_0_0_item_end by blast
with Induct have "False" by arith
then show ?case by blast
next
case 2
then obtain k' where k': "k = Suc k'" using Suc_pred' by blast
with Induct 2 have "x ∈ 𝒥 (Suc k') 0" by auto
then have "x ∈ π k {} (ℐ k')" by (simp add: k')
then have "item_end x = k ∨ x ∈ ℐ k'" using π_no_tokens_item_end by blast
then show ?case
proof (induct rule: disjCases2)
case 1
with Induct have "False" by auto
then show ?case by blast
next
case 2
then have "∃ u'. x ∈ 𝒥 k' u'" using ℐ.simps natUnion_ex by fastforce
then obtain u' where u': "x ∈ 𝒥 k' u'" by blast
have k'_bound: "k' < item_end x" using k' Induct by arith
have indexlt: "indexlt k' u' k u" by (simp add: indexlt_simp k')
from Induct(1)[OF u' this k'_bound]
have pred_produced: "produced_by_scan_step x k' u'" .
then show ?case using indexlt produced_by_scan_step_trans indexle_def by blast
qed
next
case 3
then have ex_u': "∃ u'. u = Suc u'" by arith
then obtain u' where u': "u = Suc u'" by blast
with Induct have "x ∈ 𝒥 k (Suc u')" by metis
then have x_in_π: "x ∈ π k (𝒯 k u) (𝒥 k u')" using u' 𝒥.simps by metis
have "x ∈ 𝒥 k u' ∨ x ∉ 𝒥 k u'" by blast
then show ?case
proof (induct rule: disjCases2)
case 1
have indexlt: "indexlt k u' k u" by (simp add: indexlt_simp u')
with Induct(1)[OF 1 indexlt Induct(3)] show ?case
using indexle_def produced_by_scan_step_trans by blast
next
case 2
have item_end_x: "k < item_end x" using Induct by auto
obtain f where f: "f = Scan (𝒯 k u) k ∘ Complete k ∘ Predict k" by blast
have "x ∈ limit f (𝒥 k u')"
using x_in_π π_functional f by simp
from locate_in_limit[OF this 2] obtain n where n:
"x ∈ funpower f (Suc n) (𝒥 k u') ∧
x ∉ funpower f n (𝒥 k u')" by blast
obtain Y where Y: "Y = funpower f n (𝒥 k u')"
by blast
have x_f_Y: "x ∈ f Y ∧ x ∉ Y" using Y n by auto
then have "x ∈ Scan (𝒯 k u) k (Complete k (Predict k Y))" using comp_apply f by simp
then have "x ∈ (Complete k (Predict k Y)) ∨
x ∈ { inc_item x' (k + length c) | x' t c. x' ∈ bin (Complete k (Predict k Y)) k ∧
(t, c) ∈ (𝒯 k u) ∧ next_symbol x' = Some t }" using Scan_def by simp
then show ?case
proof (induct rule: disjCases2)
case 1
then have "False" using item_end_x x_f_Y Complete_item_end Predict_item_end
using less_not_refl3 by blast
then show ?case by auto
next
case 2
have "Y ⊆ limit f (𝒥 k u')" using Y limit_def natUnion_superset by fastforce
then have "Y ⊆ π k (𝒯 k u) (𝒥 k u')" using f by (simp add: π_functional)
then have Y_in_𝒥: "Y ⊆ 𝒥 k u" using u' by simp
then have in_𝒥: "Complete k (Predict k Y) ⊆ 𝒥 k u"
proof -
have f1: "∀f I Ia i. (¬ mono f ∨ ¬ (I::item set) ⊆ Ia ∨ (i::item) ∉ f I) ∨ i ∈ f Ia"
by (meson mono_subset_elem)
obtain ii :: "item set ⇒ item set ⇒ item" where
"∀x0 x1. (∃v2. v2 ∈ x1 ∧ v2 ∉ x0) = (ii x0 x1 ∈ x1 ∧ ii x0 x1 ∉ x0)"
by moura
then have f2: "∀I Ia. ii Ia I ∈ I ∧ ii Ia I ∉ Ia ∨ I ⊆ Ia"
by blast
obtain nn :: nat where
f3: "u = Suc nn"
using ex_u' by presburger
moreover
{ assume "ii (𝒥 k u) (Complete k (Predict k Y)) ∈ Complete k (π k (𝒯 k (Suc nn)) (𝒥 k nn))"
then have ?thesis
using f3 f2 Complete_π_fix by auto }
ultimately show ?thesis
using f2 f1 by (metis (full_types) Complete_regular Predict_π_fix Predict_regular
𝒥.simps(2) Y_in_𝒥 regular_implies_mono)
qed
from 2 obtain x' t c where x'_t_c:
"x = inc_item x' (k + length c) ∧ x' ∈ bin (Complete k (Predict k Y)) k ∧
(t, c) ∈ 𝒯 k u ∧ next_symbol x' = Some t" by blast
show ?case
apply (simp add: produced_by_scan_step_def)
apply (rule_tac x=k in exI)
apply (rule_tac x=u in exI)
apply (simp add: indexle_def)
apply (rule_tac x=x' in exI)
apply auto
using x'_t_c bin_def in_𝒥 apply auto[1]
using x'_t_c bin_def apply blast
apply (rule_tac x=t in exI)
apply (rule_tac x=c in exI)
using x'_t_c by auto
qed
qed
qed
qed
lemma limit_single_step:
assumes "x ∈ f X"
shows "x ∈ limit f X"
by (metis assms elem_limit_simp funpower.simps(1) funpower.simps(2))
lemma Gen_union: "Gen (A ∪ B) = Gen A ∪ Gen B"
by (simp add: Gen_def, blast)
lemma is_prefix_Prefixes_subset:
assumes "is_prefix q p"
shows "Prefixes q ⊆ Prefixes p"
proof -
show ?thesis
apply (auto simp add: Prefixes_def)
using assms by (metis is_prefix_append is_prefix_def)
qed
lemma Prefixes_subset_𝒫:
assumes "p ∈ 𝒫 k u"
shows "Prefixes p ⊆ 𝒫 k u"
using Prefixes_is_prefix assms prefixes_are_paths by blast
lemma Prefixes_subset_paths_le:
assumes "Prefixes p ⊆ P"
shows "Prefixes p ⊆ paths_le (charslength p) P"
using Prefixes_is_prefix assms charslength_of_prefix paths_le_def by auto
lemma Scan_𝒥_subset_𝒥:
"Scan (𝒯 k (Suc u)) k (𝒥 k u) ⊆ 𝒥 k (Suc u)"
by (metis (no_types, lifting) Scan_π_fix 𝒥.simps(2) 𝒥_subset_Suc_u monoD mono_Scan)
lemma subset_𝒥k: "u ≤ v ⟹ 𝒥 k u ⊆ 𝒥 k v"
thm 𝒥_subset_Suc_u
by (rule subset_fSuc, rule 𝒥_subset_Suc_u)
lemma subset_𝒥ℐk: "𝒥 k u ⊆ ℐ k" by (auto simp add: natUnion_def)
lemma subset_ℐ𝒥Suc: "ℐ k ⊆ 𝒥 (Suc k) u"
proof -
have a: "ℐ k ⊆ 𝒥 (Suc k) 0"
apply (simp only: 𝒥.simps)
using π_apply_setmonotone by blast
show ?thesis
apply (case_tac "u = 0")
apply (simp only: a)
apply (rule subset_trans[OF a subset_𝒥k])
by auto
qed
lemma subset_ℐSuc: "ℐ k ⊆ ℐ (Suc k)"
by (rule subset_trans[OF subset_ℐ𝒥Suc subset_𝒥ℐk])
lemma subset_ℐ: "i ≤ j ⟹ ℐ i ⊆ ℐ j"
by (rule subset_fSuc[where u=i and v=j and f = ℐ, OF subset_ℐSuc])
lemma subset_𝒥 :
assumes leq: "k' < k ∨ (k' = k ∧ u' ≤ u)"
shows "𝒥 k' u' ⊆ 𝒥 k u"
proof -
from leq show ?thesis
proof (induct rule: disjCases2)
case 1
have s1: "𝒥 k' u' ⊆ ℐ k'" by (rule_tac subset_𝒥ℐk)
have s2: "ℐ k' ⊆ ℐ (k - 1)"
apply (rule_tac subset_ℐ)
using 1 by arith
from subset_ℐ𝒥Suc[where k="k - 1"] 1 have s3: "ℐ (k - 1) ⊆ 𝒥 k 0"
by simp
have s4: "𝒥 k 0 ⊆ 𝒥 k u" by (rule_tac subset_𝒥k, simp)
from s1 s2 s3 s4 subset_trans show ?case by blast
next
case 2 thus ?case by (simp add : subset_𝒥k)
qed
qed
lemma 𝒥_subset:
assumes "indexle k' u' k u"
shows "𝒥 k' u' ⊆ 𝒥 k u"
using subset_𝒥 indexle_def indexlt_simp
by (metis assms less_imp_le_nat order_refl)
lemma Scan_items_le:
assumes bounded_T: "⋀ t . t ∈ T ⟹ length (chars_of_token t) ≤ l"
shows "Scan T k (items_le k P) ⊆ items_le (k + l) (Scan T k P)"
proof -
{
fix x :: item
assume x_dom: "x ∈ Scan T k (items_le k P)"
then have x_dom': "x ∈ Scan T k P"
by (meson items_le_is_filter mono_Scan mono_subset_elem)
from x_dom have "x ∈ items_le k P ∨
(∃ y t c. x = inc_item y (k + length c) ∧ y ∈ bin (items_le k P) k ∧ (t, c) ∈ T
∧ next_symbol y = Some t)"
using Scan_def using UnE mem_Collect_eq by auto
then have "item_end x ≤ k + l"
proof (induct rule: disjCases2)
case 1 then show ?case
by (meson items_le_fix_D items_le_idempotent trans_le_add1)
next
case 2
then obtain y t c where y: "x = inc_item y (k + length c) ∧ y ∈ bin (items_le k P) k ∧
(t, c) ∈ T ∧ next_symbol y = Some t" by blast
then have item_end_x: "item_end x = (k + length c)" by simp
from bounded_T y have "length c ≤ l"
using chars_of_token_simp by auto
with item_end_x show ?case by arith
qed
with x_dom' have "x ∈ items_le (k + l) (Scan T k P)"
using items_le_def mem_Collect_eq by blast
}
then show ?thesis by blast
qed
lemma Scan_mono_tokens:
"P ⊆ Q ⟹ Scan P k I ⊆ Scan Q k I"
by (auto simp add: Scan_def)
theorem thmD14: "k ≤ length Doc ⟹ items_le k (𝒥 k u) = Gen (paths_le k (𝒫 k u)) ∧ 𝒯 k u = 𝒵 k u
∧ items_le k (ℐ k) = Gen (paths_le k (𝒬 k))"
proof (induct k arbitrary: u rule: less_induct)
case (less k)
have "k = 0 ∨ k ≠ 0" by arith
then show ?case
proof (induct rule: disjCases2)
case 1
have 𝒥_eq_𝒫: "items_le k (𝒥 k 0) = Gen (paths_le k (𝒫 k 0))"
by (simp only: 1 thmD8 items_le_paths_le)
show ?case using thmD13[OF 𝒥_eq_𝒫 less.prems] by blast
next
case 2
have "∃ k'. k = Suc k'" using 2 by arith
then obtain k' where k': "k = Suc k'" by blast
have k'_less_k: "k' < k" using k' by arith
have "items_le k (𝒥 k 0) = Gen (paths_le k (𝒫 k 0))"
proof -
have simp_left: "items_le k (𝒥 k 0) = π k {} (items_le k (ℐ k'))"
using items_le_π_swap k' wellformed_items_ℐ by auto
have simp_right: "Gen (paths_le k (𝒫 k 0)) = natUnion (λ v. Gen (paths_le k (𝒫 k' v)))"
by (simp add: k' paths_le_pointwise pointwise_Gen pointwise_natUnion_swap)
{
fix v :: nat
have split_𝒥: "items_le k (𝒥 k' v) = items_le k' (𝒥 k' v) ∪ items_eq k (𝒥 k' v)"
using k' items_le_split_via_eq by blast
have sub1: "items_le k' (𝒥 k' v) ⊆ natUnion (λ v. Gen (paths_le k (𝒫 k' v)))"
proof -
have h: "items_le k' (𝒥 k' v) ⊆ Gen (paths_le k (𝒫 k' v))"
proof -
have f1: "items_le k' (Gen (𝒫 k' v)) ∪ items_eq (Suc k') (Gen (𝒫 k' v)) =
Gen (paths_le k (𝒫 k' v))"
using LocalLexing.items_le_split_via_eq LocalLexing_axioms items_le_paths_le k'
by blast
have "k' ≤ length Doc"
by (metis (no_types) dual_order.trans k' less.prems lessI less_imp_le_nat)
then have "items_le k' (𝒥 k' v) = items_le k' (Gen (𝒫 k' v))"
by (simp add: items_le_paths_le k' less.hyps)
then show ?thesis
using f1 by blast
qed
have "Gen (paths_le k (𝒫 k' v)) ⊆ natUnion (λ v. Gen (paths_le k (𝒫 k' v)))"
using natUnion_superset by fastforce
then show ?thesis using h by blast
qed
{
fix x :: item
assume x_dom: "x ∈ items_eq k (𝒥 k' v)"
have x_in_𝒥: "x ∈ 𝒥 k' v" using x_dom items_eq_def by auto
have item_end_x: "item_end x = k" using x_dom items_eq_def by auto
then have k'_bound: "k' < item_end x" using k' by arith
from produced_by_scan_step[OF x_in_𝒥 k'_bound]
have "produced_by_scan_step x k' v" .
from iffD1[OF produced_by_scan_step_def this] obtain k'' v'' y X where scan_step:
"indexle k'' v'' k' v ∧ y ∈ 𝒥 k'' v'' ∧ item_end y = k'' ∧ X ∈ 𝒯 k'' v'' ∧
x = inc_item y (k'' + length (chars_of_token X)) ∧
next_symbol y = Some (terminal_of_token X)" by blast
then have y_in_items_le: "y ∈ items_le k'' (𝒥 k'' v'')"
using items_le_def LocalLexing_axioms le_refl mem_Collect_eq by blast
have y_in_Gen: "y ∈ Gen(paths_le k'' (𝒫 k'' v''))"
proof -
have f1: "⋀n. k' < n ∨ ¬ k < n"
using Suc_lessD k' by blast
have f2: "k'' = k' ∨ k'' < k'"
using indexle_def indexlt_simp scan_step by force
have f3: "k' < k"
using k' by blast
have f4: "k' ≤ length Doc"
using f1 by (meson less.prems less_Suc_eq_le)
have "k'' ≤ length Doc ∨ k' = k''"
using f2 f1 by (meson Suc_lessD less.prems less_Suc_eq_le less_trans_Suc)
then show ?thesis
using f4 f3 f2 Suc_lessD y_in_items_le less.hyps less_trans_Suc by blast
qed
then have "∃ p. p ∈ 𝒫 k'' v'' ∧ pvalid p y"
by (meson Gen_implies_pvalid paths_le_is_filter rev_subsetD)
then obtain p where p: "p ∈ 𝒫 k'' v'' ∧ pvalid p y" by blast
then have charslength_p: "charslength p = k''" using pvalid_item_end scan_step by auto
have pvalid_p_y: "pvalid p y" using p by blast
have "admissible (p@[(fst X, snd X)])"
apply (rule pvalid_next_terminal_admissible)
apply (rule pvalid_p_y)
using scan_step apply (simp add: terminal_of_token_def)
using scan_step by (metis TokensAt_subset_𝒳 𝒯_subset_TokensAt 𝒳_are_terminals
rev_subsetD terminal_of_token_def)
then have admissible_p_X: "admissible (p@[X])" by simp
have X_in_𝒵: "X ∈ 𝒵 k'' (Suc v'')" by (metis (no_types, lifting) Suc_lessD 𝒵_subset_Suc
k'_bound dual_order.trans indexle_def indexlt_simp item_end_of_inc_item item_end_x
le_add1 le_neq_implies_less less.hyps less.prems not_less_eq scan_step subsetCE)
have pX_in_𝒫_k''_v'': "p@[X] ∈ 𝒫 k'' (Suc v'')"
apply (simp only: 𝒫.simps)
apply (rule limit_single_step)
apply (auto simp only: Append_def)
apply (rule_tac x=p in exI)
apply (rule_tac x=X in exI)
apply (simp only: admissible_p_X X_in_𝒵)
using charslength_p p by auto
have "indexle k'' v'' k' v" using scan_step by simp
then have "indexle k'' (Suc v'') k' (Suc v)"
by (simp add: indexle_def indexlt_simp)
then have "𝒫 k'' (Suc v'') ⊆ 𝒫 k' (Suc v)"
by (metis indexle_def indexlt_simp less_or_eq_imp_le subset_𝒫)
with pX_in_𝒫_k''_v'' have pX_in_𝒫_k': "p@[X] ∈ 𝒫 k' (Suc v)" by blast
have "charslength (p@[X]) = k'' + length (chars_of_token X)"
using charslength_p by auto
then have "charslength (p@[X]) = item_end x" using scan_step by simp
then have charslength_p_X: "charslength (p@[X]) = k" using item_end_x by simp
then have pX_dom: "p@[X] ∈ paths_le k (𝒫 k' (Suc v))"
using lessI less_Suc_eq_le mem_Collect_eq pX_in_𝒫_k' paths_le_def by auto
have wellformed_x: "wellformed_item x"
using item_end_x less.prems scan_step wellformed_inc_item wellformed_items_𝒥
wellformed_items_def by auto
have wellformed_p_X: "wellformed_tokens (p@[X])"
using 𝒫_wellformed pX_in_𝒫_k''_v'' by blast
from iffD1[OF pvalid_def pvalid_p_y] obtain r γ where r_γ:
"wellformed_tokens p ∧
wellformed_item y ∧
r ≤ length p ∧
charslength p = item_end y ∧
charslength (take r p) = item_origin y ∧
is_derivation (terminals (take r p) @ [item_nonterminal y] @ γ) ∧
derives (item_α y) (terminals (drop r p))" by blast
have r_le_p: "r ≤ length p" by (simp add: r_γ)
have item_nonterminal_x: "item_nonterminal x = item_nonterminal y"
by (simp add: scan_step)
have item_α_x: "item_α x = (item_α y) @ [terminal_of_token X]"
by (simp add: item_α_of_inc_item r_γ scan_step)
have pvalid_x: "pvalid (p@[X]) x"
apply (auto simp add: pvalid_def wellformed_x wellformed_p_X)
apply (rule_tac x=r in exI)
apply auto
apply (simp add: le_SucI r_γ)
using r_γ scan_step apply auto[1]
using r_γ scan_step apply auto[1]
apply (rule_tac x=γ in exI)
apply (simp add: r_le_p item_nonterminal_x)
using r_γ apply simp
apply (simp add: r_le_p item_α_x)
by (metis terminals_singleton append_Nil2
derives_implies_leftderives derives_is_sentence is_sentence_concat
is_sentence_cons is_symbol_def is_word_append is_word_cons is_word_terminals
is_word_terminals_drop leftderives_implies_derives leftderives_padback
leftderives_refl r_γ terminals_append terminals_drop wellformed_p_X)
then have "x ∈ Gen (paths_le k (𝒫 k' (Suc v)))" using pX_dom Gen_def
LocalLexing_axioms mem_Collect_eq by auto
}
then have sub2: "items_eq k (𝒥 k' v) ⊆ natUnion (λ v. Gen (paths_le k (𝒫 k' v)))"
by (meson dual_order.trans natUnion_superset subsetI)
have suffices3: "items_le k (𝒥 k' v) ⊆ natUnion (λ v. Gen (paths_le k (𝒫 k' v)))"
using split_𝒥 sub1 sub2 by blast
have "items_le k (𝒥 k' v) ⊆ Gen (paths_le k (𝒫 k 0))"
using suffices3 simp_right by blast
}
note suffices2 = this
have items_le_natUnion_swap: "items_le k (ℐ k') = natUnion(λ v. items_le k (𝒥 k' v))"
by (simp add: items_le_pointwise pointwise_natUnion_swap)
then have suffices1: "items_le k (ℐ k') ⊆ Gen (paths_le k (𝒫 k 0))"
using suffices2 natUnion_upperbound by metis
have sub_lemma: "items_le k (𝒥 k 0) ⊆ Gen (paths_le k (𝒫 k 0))"
proof -
have "items_le k (𝒥 k 0) ⊆ Gen (𝒫 k 0)"
apply (subst simp_left)
apply (rule thmD5)
apply (auto simp only: less)
using suffices1 items_le_is_filter items_le_paths_le subsetCE by blast
then show ?thesis
by (simp add: items_le_idempotent remove_paths_le_in_subset_Gen)
qed
have eq1: "π k {} (items_le k (ℐ k')) = π k {} (items_le k (natUnion (𝒥 k')))" by simp
then have eq2: "π k {} (items_le k (natUnion (𝒥 k'))) =
π k {} (natUnion (λ v. items_le k (𝒥 k' v)))"
using items_le_natUnion_swap by auto
from simp_left eq1 eq2
have simp_left': "items_le k (𝒥 k 0) = π k {} (natUnion (λ v. items_le k (𝒥 k' v)))"
by metis
{
fix v :: nat
fix q :: "token list"
fix x :: item
assume q_dom: "q ∈ paths_eq k (𝒫 k' v)"
assume pvalid_q_x: "pvalid q x"
have q_in_𝒫: "q ∈ 𝒫 k' v" using q_dom paths_eq_def by auto
have charslength_q: "charslength q = k" using q_dom paths_eq_def by auto
with k'_less_k have q_nonempty: "q ≠ []"
using "2.hyps" chars.simps(1) charslength.simps list.size(3) by auto
then have "∃ p X. q = p @ [X]" by (metis append_butlast_last_id)
then obtain p X where pX: "q = p @ [X]" by blast
from last_step_of_path[OF q_in_𝒫 pX] obtain k'' v'' where k'':
"indexlt k'' v'' k' v ∧ q ∈ 𝒫 k'' (Suc v'') ∧ charslength p = k'' ∧
X ∈ 𝒵 k'' (Suc v'')" by blast
have h1: "p ∈ 𝔓"
by (metis (no_types, lifting) LocalLexing.𝔓_covers_𝒫 LocalLexing_axioms
append_Nil2 is_prefix_cancel is_prefix_empty pX prefixes_are_paths q_in_𝒫 subsetCE)
have h2: "charslength p = k''" using k'' by blast
obtain T where T: "T = {X}" by blast
have h3: "X ∈ T" using T by blast
have h4: "T ⊆ 𝒳 k''" using 𝒵_subset_𝒳 T k'' by blast
obtain N where N: "N = item_nonterminal x" by blast
obtain α where α: "α = item_α x" by blast
obtain β where β: "β = item_β x" by blast
have wellformed_x: "wellformed_item x" using pvalid_def pvalid_q_x by blast
then have h5: "(N, α @ β) ∈ ℜ"
using N α β item_nonterminal_def item_rhs_def item_rhs_split prod.collapse
wellformed_item_def by auto
have pvalid_left_q_x: "pvalid_left q x" using pvalid_q_x by (simp add: pvalid_left)
from iffD1[OF pvalid_left_def pvalid_left_q_x] obtain r γ where r_γ:
"wellformed_tokens q ∧
wellformed_item x ∧
r ≤ length q ∧
charslength q = item_end x ∧
charslength (take r q) = item_origin x ∧
is_leftderivation (terminals (take r q) @ [item_nonterminal x] @ γ) ∧
leftderives (item_α x) (terminals (drop r q))" by blast
have h6: "r ≤ length q" using r_γ by blast
have h7: "leftderives [𝔖] (terminals (take r q) @ [N] @ γ)"
using r_γ N is_leftderivation_def by blast
have h8: "leftderives α (terminals (drop r q))" using r_γ α by metis
have h9: "k = k'' + length (chars_of_token X)" using r_γ
using charslength_q h2 pX by auto
have h10: "x = Item (N, α @ β) (length α) (charslength (take r q)) k"
by (metis N α β charslength_q item.collapse item_dot_is_α_length item_nonterminal_def
item_rhs_def item_rhs_split prod.collapse r_γ)
from thmD11[OF h1 h2 h3 h4 pX h5 h6 h7 h8 h9 h10]
have "x ∈ items_le k (π k {} (Scan T k'' (Gen (Prefixes p))))"
by blast
then have x_in: "x ∈ π k {} (Scan T k'' (Gen (Prefixes p)))"
using items_le_is_filter by blast
have subset1: "Prefixes p ⊆ Prefixes q"
apply (rule is_prefix_Prefixes_subset)
by (simp add: pX is_prefix_def)
have subset2: "Prefixes q ⊆ 𝒫 k'' (Suc v'')"
apply (rule Prefixes_subset_𝒫)
using k'' by blast
from subset1 subset2 have "Prefixes p ⊆ 𝒫 k'' (Suc v'')" by blast
then have "Prefixes p ⊆ paths_le k'' (𝒫 k'' (Suc v''))"
using k'' Prefixes_subset_paths_le by blast
then have subset3: "Gen (Prefixes p) ⊆ Gen (paths_le k'' (𝒫 k'' (Suc v'')))"
using Gen_def LocalLexing_axioms by auto
have k''_less_k: "k'' < k" using k'' k' using indexlt_simp less_Suc_eq by auto
then have k''_Doc_bound: "k'' ≤ length Doc" using less by auto
from less(1)[OF k''_less_k k''_Doc_bound, of "Suc v''"]
have induct1: "items_le k'' (𝒥 k'' (Suc v'')) = Gen (paths_le k'' (𝒫 k'' (Suc v'')))"
by blast
from less(1)[OF k''_less_k k''_Doc_bound, of "Suc(Suc v'')"]
have induct2: "𝒯 k'' (Suc (Suc v'')) = 𝒵 k'' (Suc (Suc v''))" by blast
have subset4: "Gen (Prefixes p) ⊆ items_le k'' (𝒥 k'' (Suc v''))"
using subset3 induct1 by auto
from induct1 subset4
have subset6: "Scan T k'' (Gen (Prefixes p)) ⊆
Scan T k'' (items_le k'' (𝒥 k'' (Suc v'')))"
apply (rule_tac monoD[OF mono_Scan])
by blast
have "k'' + length (chars_of_token X) = k"
by (simp add: h9)
have "⋀ t. t ∈ T ⟹ length (chars_of_token t) ≤ length (chars_of_token X)"
using T by auto
from Scan_items_le[of T, OF this, simplified, of k'' "𝒥 k'' (Suc v'')"] h9
have subset7: "Scan T k'' (items_le k'' (𝒥 k'' (Suc v'')))
⊆ items_le k (Scan T k'' (𝒥 k'' (Suc v'')))" by simp
have "T ⊆ 𝒵 k'' (Suc (Suc v''))" using T k''
using 𝒵_subset_Suc rev_subsetD singletonD subsetI by blast
then have T_subset_𝒯: "T ⊆ 𝒯 k'' (Suc (Suc v''))" using induct2 by auto
have subset8: "Scan T k'' (𝒥 k'' (Suc v'')) ⊆
Scan (𝒯 k'' (Suc (Suc v''))) k'' (𝒥 k'' (Suc v''))"
using T_subset_𝒯 Scan_mono_tokens by blast
have subset9: "Scan (𝒯 k'' (Suc (Suc v''))) k'' (𝒥 k'' (Suc v'')) ⊆ 𝒥 k'' (Suc (Suc v''))"
by (rule Scan_𝒥_subset_𝒥)
have subset10: "(Scan T k'' (𝒥 k'' (Suc v''))) ⊆ 𝒥 k'' (Suc (Suc v''))"
using subset8 subset9 by blast
have "k'' ≤ k'" using k'' indexlt_simp by auto
then have "indexle k'' (Suc (Suc v'')) k' (Suc (Suc v''))" using indexlt_simp
using indexle_def le_neq_implies_less by auto
then have subset11: "𝒥 k'' (Suc (Suc v'')) ⊆ 𝒥 k' (Suc (Suc v''))"
using 𝒥_subset by blast
have subset12: "Scan T k'' (𝒥 k'' (Suc v'')) ⊆ 𝒥 k' (Suc (Suc v''))"
using subset8 subset9 subset10 subset11 by blast
then have subset13: "items_le k (Scan T k'' (𝒥 k'' (Suc v''))) ⊆
items_le k (𝒥 k' (Suc (Suc v'')))"
using items_le_def mem_Collect_eq rev_subsetD subsetI by auto
have subset14: "Scan T k'' (Gen (Prefixes p)) ⊆ items_le k (𝒥 k' (Suc (Suc v'')))"
using subset6 subset7 subset13 by blast
then have x_in': "x ∈ π k {} (items_le k (𝒥 k' (Suc (Suc v''))))"
using x_in
by (meson π_apply_setmonotone π_subset_elem_trans subsetCE subsetI)
from x_in' have "x ∈ π k {} (natUnion (λ v. items_le k (𝒥 k' v)))"
by (meson k' mono_π mono_subset_elem natUnion_superset)
}
note suffices6 = this
{
fix v :: nat
have "Gen (paths_eq k (𝒫 k' v)) ⊆ π k {} (natUnion (λ v. items_le k (𝒥 k' v)))"
using suffices6 by (meson Gen_implies_pvalid subsetI)
}
note suffices5 = this
{
fix v :: nat
have "paths_le k (𝒫 k' v) = paths_le k' (𝒫 k' v) ∪ paths_eq k (𝒫 k' v)"
using paths_le_split_via_eq k' by metis
then have Gen_split: "Gen (paths_le k (𝒫 k' v)) =
Gen (paths_le k' (𝒫 k' v)) ∪ Gen(paths_eq k (𝒫 k' v))" using Gen_union by metis
have case_le: "Gen (paths_le k' (𝒫 k' v)) ⊆ π k {} (natUnion (λ v. items_le k (𝒥 k' v)))"
proof -
from less k'_less_k have "k' ≤ length Doc" by arith
from less(1)[OF k'_less_k this]
have "items_le k' (𝒥 k' v) = Gen (paths_le k' (𝒫 k' v))" by blast
then have "Gen (paths_le k' (𝒫 k' v)) ⊆ natUnion (λ v. items_le k (𝒥 k' v))"
using items_le_def LocalLexing_axioms k'_less_k natUnion_superset by fastforce
then show ?thesis using π_apply_setmonotone by blast
qed
have "Gen (paths_le k (𝒫 k' v)) ⊆ π k {} (natUnion (λ v. items_le k (𝒥 k' v)))"
using Gen_split case_le suffices5 UnE rev_subsetD subsetI by blast
}
note suffices4 = this
have super_lemma: "Gen (paths_le k (𝒫 k 0)) ⊆ items_le k (𝒥 k 0)"
apply (subst simp_right)
apply (subst simp_left')
using suffices4 by (meson natUnion_ex rev_subsetD subsetI)
from super_lemma sub_lemma show ?thesis by blast
qed
then show ?case using thmD13 less.prems by blast
qed
qed
end
end