Theory Earley_Parser
theory Earley_Parser
imports
Earley_Recognizer
"HOL-Library.Monad_Syntax"
begin
section ‹Earley parser›
subsection ‹Pointer lemmas›
definition predicts :: "'a item ⇒ bool" where
"predicts x ≡ start_item x = end_item x ∧ dot_item x = 0"
definition scans :: "'a list ⇒ nat ⇒ 'a item ⇒ 'a item ⇒ bool" where
"scans ω k x y ≡ y = inc_item x k ∧ (∃a. next_symbol x = Some a ∧ ω!(k-1) = a)"
definition completes :: "nat ⇒ 'a item ⇒ 'a item ⇒ 'a item ⇒ bool" where
"completes k x y z ≡ y = inc_item x k ∧ is_complete z ∧ start_item z = end_item x ∧
(∃N. next_symbol x = Some N ∧ N = lhs_item z)"
definition sound_null_ptr :: "'a item × pointer ⇒ bool" where
"sound_null_ptr e ≡ (snd e = Null ⟶ predicts (fst e))"
definition sound_pre_ptr :: "'a list ⇒ 'a bins ⇒ nat ⇒ 'a item × pointer ⇒ bool" where
"sound_pre_ptr ω bs k e ≡ ∀pre. snd e = Pre pre ⟶
k > 0 ∧ pre < length (bs!(k-1)) ∧ scans ω k (fst (bs!(k-1)!pre)) (fst e)"
definition sound_prered_ptr :: "'a bins ⇒ nat ⇒ 'a item × pointer ⇒ bool" where
"sound_prered_ptr bs k e ≡ ∀p ps k' pre red. snd e = PreRed p ps ∧ (k', pre, red) ∈ set (p#ps) ⟶
k' < k ∧ pre < length (bs!k') ∧ red < length (bs!k) ∧ completes k (fst (bs!k'!pre)) (fst e) (fst (bs!k!red))"
definition sound_ptrs :: "'a list ⇒ 'a bins ⇒ bool" where
"sound_ptrs ω bs ≡ ∀k < length bs. ∀e ∈ set (bs!k).
sound_null_ptr e ∧ sound_pre_ptr ω bs k e ∧ sound_prered_ptr bs k e"
definition mono_red_ptr :: "'a bins ⇒ bool" where
"mono_red_ptr bs ≡ ∀k < length bs. ∀i < length (bs!k).
∀k' pre red ps. snd (bs!k!i) = PreRed (k', pre, red) ps ⟶ red < i"
lemma nth_item_upd_bin:
"n < length es ⟹ fst (upd_bin e es ! n) = fst (es!n)"
by (induction es arbitrary: e n) (auto simp: less_Suc_eq_0_disj split: prod.splits pointer.splits)
lemma upd_bin_append:
"fst e ∉ set (items es) ⟹ upd_bin e es = es @ [e]"
by (induction es arbitrary: e) (auto simp: items_def split: prod.splits pointer.splits)
lemma upd_bin_null_pre:
"fst e ∈ set (items es) ⟹ snd e = Null ∨ snd e = Pre pre ⟹ upd_bin e es = es"
by (induction es arbitrary: e) (auto simp: items_def split: prod.splits, fastforce+)
lemma upd_bin_prered_nop:
assumes "distinct (items es)" "i < length es"
assumes "fst e = fst (es!i)" "snd e = PreRed p ps" "∄p ps. snd (es!i) = PreRed p ps"
shows "upd_bin e es = es"
using assms
by (induction es arbitrary: e i) (auto simp: less_Suc_eq_0_disj items_def split: prod.splits pointer.splits)
lemma upd_bin_prered_upd:
assumes "distinct (items es)" "i < length es"
assumes "fst e = fst (es!i)" "snd e = PreRed p rs" "snd (es!i) = PreRed p' rs'" "upd_bin e es = es'"
shows "snd (es'!i) = PreRed p' (p#rs@rs') ∧ (∀j < length es'. i≠j ⟶ es'!j = es!j) ∧ length (upd_bin e es) = length es"
using assms
proof (induction es arbitrary: e i es')
case (Cons e' es)
show ?case
proof cases
assume *: "fst e = fst e'"
show ?thesis
proof (cases "∃x xp xs y yp ys. e = (x, PreRed xp xs) ∧ e' = (y, PreRed yp ys)")
case True
then obtain x xp xs y yp ys where ee': "e = (x, PreRed xp xs)" "e' = (y, PreRed yp ys)" "x = y"
using * by auto
have simp: "upd_bin e (e' # es') = (x, PreRed yp (xp # xs @ ys)) # es'"
using True ee' by simp
show ?thesis
using Cons simp ee' apply (auto simp: items_def)
using less_Suc_eq_0_disj by fastforce+
next
case False
hence "upd_bin e (e' # es') = e' # es'"
using * by (auto split: pointer.splits prod.splits)
thus ?thesis
using False * Cons.prems(1,2,3,4,5) by (auto simp: less_Suc_eq_0_disj items_def split: prod.splits)
qed
next
assume *: "fst e ≠ fst e'"
have simp: "upd_bin e (e' # es) = e' # upd_bin e es"
using * by (auto split: pointer.splits prod.splits)
have 0: "distinct (items es)"
using Cons.prems(1) unfolding items_def by simp
have 1: "i-1 < length es"
using Cons.prems(2,3) * by (metis One_nat_def leI less_diff_conv2 less_one list.size(4) nth_Cons_0)
have 2: "fst e = fst (es!(i-1))"
using Cons.prems(3) * by (metis nth_Cons')
have 3: "snd e = PreRed p rs"
using Cons.prems(4) by simp
have 4: "snd (es!(i-1)) = PreRed p' rs' "
using Cons.prems(3,5) * by (metis nth_Cons')
have "snd (upd_bin e es!(i-1)) = PreRed p' (p # rs @ rs') ∧
(∀j < length (upd_bin e es). i-1 ≠ j ⟶ (upd_bin e es) ! j = es ! j)"
using Cons.IH[OF 0 1 2 3 4] by blast
hence "snd ((e' # upd_bin e es) ! i) = PreRed p' (p # rs @ rs') ∧
(∀j < length (e' # upd_bin e es). i ≠ j ⟶ (e' # upd_bin e es) ! j = (e' # es) ! j)"
using * Cons.prems(2,3) less_Suc_eq_0_disj by auto
moreover have "e' # upd_bin e es = es'"
using Cons.prems(6) simp by auto
ultimately show ?thesis
by (metis 0 1 2 3 4 Cons.IH Cons.prems(6) length_Cons)
qed
qed simp
lemma sound_ptrs_upd_bin:
assumes "sound_ptrs ω bs" "k < length bs" "es = bs!k" "distinct (items es)"
assumes "sound_null_ptr e" "sound_pre_ptr ω bs k e" "sound_prered_ptr bs k e"
shows "sound_ptrs ω (bs[k := upd_bin e es])"
unfolding sound_ptrs_def
proof (standard, standard, standard)
fix idx elem
let ?bs = "bs[k := upd_bin e es]"
assume a0: "idx < length ?bs"
assume a1: "elem ∈ set (?bs ! idx)"
show "sound_null_ptr elem ∧ sound_pre_ptr ω ?bs idx elem ∧ sound_prered_ptr ?bs idx elem"
proof cases
assume a2: "idx = k"
have "elem ∈ set es ⟹ sound_pre_ptr ω bs idx elem"
using a0 a2 assms(1-3) sound_ptrs_def by blast
hence pre_es: "elem ∈ set es ⟹ sound_pre_ptr ω ?bs idx elem"
using a2 unfolding sound_pre_ptr_def by force
have "elem = e ⟹ sound_pre_ptr ω bs idx elem"
using a2 assms(6) by auto
hence pre_e: "elem = e ⟹ sound_pre_ptr ω ?bs idx elem"
using a2 unfolding sound_pre_ptr_def by force
have "elem ∈ set es ⟹ sound_prered_ptr bs idx elem"
using a0 a2 assms(1-3) sound_ptrs_def by blast
hence prered_es: "elem ∈ set es ⟹ sound_prered_ptr (bs[k := upd_bin e es]) idx elem"
using a2 assms(2,3) length_upd_bin nth_item_upd_bin unfolding sound_prered_ptr_def
by (smt (verit, ccfv_SIG) dual_order.strict_trans1 nth_list_update)
have "elem = e ⟹ sound_prered_ptr bs idx elem"
using a2 assms(7) by auto
hence prered_e: "elem = e ⟹ sound_prered_ptr ?bs idx elem"
using a2 assms(2,3) length_upd_bin nth_item_upd_bin unfolding sound_prered_ptr_def
by (smt (verit, best) dual_order.strict_trans1 nth_list_update)
consider (A) "fst e ∉ set (items es)" |
(B) "fst e ∈ set (items es) ∧ (∃pre. snd e = Null ∨ snd e = Pre pre)" |
(C) "fst e ∈ set (items es) ∧ ¬ (∃pre. snd e = Null ∨ snd e = Pre pre)"
by blast
thus ?thesis
proof cases
case A
hence "elem ∈ set (es @ [e])"
using a1 a2 upd_bin_append assms(2) by fastforce
thus ?thesis
using assms(1-3,5) pre_e pre_es prered_e prered_es sound_ptrs_def by auto
next
case B
hence "elem ∈ set es"
using a1 a2 upd_bin_null_pre assms(2) by fastforce
thus ?thesis
using assms(1-3) pre_es prered_es sound_ptrs_def by blast
next
case C
then obtain i p ps where C: "i < length es ∧ fst e = fst (es!i) ∧ snd e = PreRed p ps"
by (metis assms(4) distinct_Ex1 items_def length_map nth_map pointer.exhaust)
show ?thesis
proof cases
assume "∄p' ps'. snd (es!i) = PreRed p' ps'"
hence C: "elem ∈ set es"
using a1 a2 C upd_bin_prered_nop assms(2,4) by (metis nth_list_update_eq)
thus ?thesis
using assms(1-3) sound_ptrs_def pre_es prered_es by blast
next
assume "¬ (∄p' ps'. snd (es!i) = PreRed p' ps')"
then obtain p' ps' where D: "snd (es!i) = PreRed p' ps'"
by blast
hence 0: "snd (upd_bin e es!i) = PreRed p' (p#ps@ps') ∧ (∀j < length (upd_bin e es). i≠j ⟶ upd_bin e es!j = es!j)"
using C assms(4) upd_bin_prered_upd by blast
obtain j where 1: "j < length es ∧ elem = upd_bin e es!j"
using a1 a2 assms(2) C items_def bin_eq_items_upd_bin by (metis in_set_conv_nth length_map nth_list_update_eq nth_map)
show ?thesis
proof cases
assume a3: "i=j"
hence a3: "snd elem = PreRed p' (p#ps@ps')"
using 0 1 by blast
have "sound_null_ptr elem"
using a3 unfolding sound_null_ptr_def by simp
moreover have "sound_pre_ptr ω ?bs idx elem"
using a3 unfolding sound_pre_ptr_def by simp
moreover have "sound_prered_ptr ?bs idx elem"
unfolding sound_prered_ptr_def
proof (standard, standard, standard, standard, standard, standard)
fix P PS k' pre red
assume a4: "snd elem = PreRed P PS ∧ (k', pre, red) ∈ set (P#PS)"
show "k' < idx ∧ pre < length (bs[k := upd_bin e es]!k') ∧ red < length (bs[k := upd_bin e es]!idx) ∧
completes idx (fst (bs[k := upd_bin e es]!k'!pre)) (fst elem) (fst (bs[k := upd_bin e es]!idx!red))"
proof cases
assume a5: "(k', pre, red) ∈ set (p#ps)"
show ?thesis
using 0 1 C a2 a4 a5 prered_es assms(2,3,7) sound_prered_ptr_def length_upd_bin nth_item_upd_bin
by (smt (verit) dual_order.strict_trans1 nth_list_update_eq nth_list_update_neq nth_mem)
next
assume a5: "(k', pre, red) ∉ set (p#ps)"
hence a5: "(k', pre, red) ∈ set (p'#ps')"
using a3 a4 by auto
have "k' < idx ∧ pre < length (bs!k') ∧ red < length (bs!idx) ∧
completes idx (fst (bs!k'!pre)) (fst e) (fst (bs!idx!red))"
using assms(1-3) C D a2 a5 unfolding sound_ptrs_def sound_prered_ptr_def by (metis nth_mem)
thus ?thesis
using 0 1 C a4 assms(2,3) length_upd_bin nth_item_upd_bin prered_es sound_prered_ptr_def
by (smt (verit, best) dual_order.strict_trans1 nth_list_update_eq nth_list_update_neq nth_mem)
qed
qed
ultimately show ?thesis
by blast
next
assume a3: "i≠j"
hence "elem ∈ set es"
using 0 1 by (metis length_upd_bin nth_mem order_less_le_trans)
thus ?thesis
using assms(1-3) pre_es prered_es sound_ptrs_def by blast
qed
qed
qed
next
assume a2: "idx ≠ k"
have null: "sound_null_ptr elem"
using a0 a1 a2 assms(1) sound_ptrs_def by auto
have "sound_pre_ptr ω bs idx elem"
using a0 a1 a2 assms(1,2) unfolding sound_ptrs_def by simp
hence pre: "sound_pre_ptr ω ?bs idx elem"
using assms(2,3) length_upd_bin nth_item_upd_bin unfolding sound_pre_ptr_def
using dual_order.strict_trans1 nth_list_update by (metis (no_types, lifting))
have "sound_prered_ptr bs idx elem"
using a0 a1 a2 assms(1,2) unfolding sound_ptrs_def by simp
hence prered: "sound_prered_ptr ?bs idx elem"
using assms(2,3) length_upd_bin nth_item_upd_bin unfolding sound_prered_ptr_def
by (smt (verit, best) dual_order.strict_trans1 nth_list_update)
show ?thesis
using null pre prered by blast
qed
qed
lemma mono_red_ptr_upd_bin:
assumes "mono_red_ptr bs" "k < length bs" "es = bs!k" "distinct (items es)"
assumes "∀k' pre red ps. snd e = PreRed (k', pre, red) ps ⟶ red < length es"
shows "mono_red_ptr (bs[k := upd_bin e es])"
unfolding mono_red_ptr_def
proof (standard, standard)
fix idx
let ?bs = "bs[k := upd_bin e es]"
assume a0: "idx < length ?bs"
show "∀i < length (?bs!idx). ∀k' pre red ps. snd (?bs!idx!i) = PreRed (k', pre, red) ps ⟶ red < i"
proof cases
assume a1: "idx=k"
consider (A) "fst e ∉ set (items es)" |
(B) "fst e ∈ set (items es) ∧ (∃pre. snd e = Null ∨ snd e = Pre pre)" |
(C) "fst e ∈ set (items es) ∧ ¬ (∃pre. snd e = Null ∨ snd e = Pre pre)"
by blast
thus ?thesis
proof cases
case A
hence "upd_bin e es = es @ [e]"
using upd_bin_append by blast
thus ?thesis
using a1 assms(1-3,5) mono_red_ptr_def
by (metis length_append_singleton less_antisym nth_append nth_append_length nth_list_update_eq)
next
case B
hence "upd_bin e es = es"
using upd_bin_null_pre by blast
thus ?thesis
using a1 assms(1-3) mono_red_ptr_def by force
next
case C
then obtain i p ps where C: "i < length es" "fst e = fst (es!i)" "snd e = PreRed p ps"
by (metis in_set_conv_nth items_def length_map nth_map pointer.exhaust)
show ?thesis
proof cases
assume "∄p' ps'. snd (es!i) = PreRed p' ps'"
hence "upd_bin e es = es"
using upd_bin_prered_nop C assms(4) by blast
thus ?thesis
using a1 assms(1-3) mono_red_ptr_def by (metis nth_list_update_eq)
next
assume "¬ (∄p' ps'. snd (es!i) = PreRed p' ps')"
then obtain p' ps' where D: "snd (es!i) = PreRed p' ps'"
by blast
have 0: "snd (upd_bin e es!i) = PreRed p' (p#ps@ps') ∧
(∀j < length (upd_bin e es). i ≠ j ⟶ upd_bin e es!j = es!j) ∧
length (upd_bin e es) = length es"
using C D assms(4) upd_bin_prered_upd by blast
show ?thesis
proof (standard, standard, standard, standard, standard, standard, standard)
fix j k' pre red PS
assume a2: "j < length (?bs!idx)"
assume a3: "snd (?bs!idx!j) = PreRed (k', pre, red) PS"
have 1: "?bs!idx = upd_bin e es"
by (simp add: a1 assms(2))
show "red < j"
proof cases
assume a4: "i=j"
show ?thesis
using 0 1 C(1) D a3 a4 assms(1-3) unfolding mono_red_ptr_def by (metis pointer.inject(2))
next
assume a4: "i≠j"
thus ?thesis
using 0 1 a2 a3 assms(1) assms(2) assms(3) mono_red_ptr_def by force
qed
qed
qed
qed
next
assume a1: "idx≠k"
show ?thesis
using a0 a1 assms(1) mono_red_ptr_def by fastforce
qed
qed
lemma sound_mono_ptrs_upds_bin:
assumes "sound_ptrs ω bs" "mono_red_ptr bs" "k < length bs" "b = bs!k" "distinct (items b)"
assumes "∀e ∈ set es. sound_null_ptr e ∧ sound_pre_ptr ω bs k e ∧ sound_prered_ptr bs k e"
assumes "∀e ∈ set es. ∀k' pre red ps. snd e = PreRed (k', pre, red) ps ⟶ red < length b"
shows "sound_ptrs ω (bs[k := upds_bin es b]) ∧ mono_red_ptr (bs[k := upds_bin es b])"
using assms
proof (induction es arbitrary: b bs)
case (Cons e es)
let ?bs = "bs[k := upd_bin e b]"
have 0: "sound_ptrs ω ?bs"
using sound_ptrs_upd_bin Cons.prems(1,3-5,6) by (metis list.set_intros(1))
have 1: "mono_red_ptr ?bs"
using mono_red_ptr_upd_bin Cons.prems(2-5,7) by (metis list.set_intros(1))
have 2: "k < length ?bs"
using Cons.prems(3) by simp
have 3: "upd_bin e b = ?bs!k"
using Cons.prems(3) by simp
have 4: "∀e' ∈ set es. sound_null_ptr e' ∧ sound_pre_ptr ω ?bs k e' ∧ sound_prered_ptr ?bs k e'"
using Cons.prems(3,4,6) length_upd_bin nth_item_upd_bin sound_pre_ptr_def sound_prered_ptr_def
by (smt (verit, ccfv_threshold) list.set_intros(2) nth_list_update order_less_le_trans)
have 5: "∀e' ∈ set es. ∀k' pre red ps. snd e' = PreRed (k', pre, red) ps ⟶ red < length (upd_bin e b)"
by (meson Cons.prems(7) length_upd_bin order_less_le_trans set_subset_Cons subsetD)
have "sound_ptrs ω ((bs[k := upd_bin e b])[k := upds_bin es (upd_bin e b)]) ∧
mono_red_ptr (bs[k := upd_bin e b, k := upds_bin es (upd_bin e b)])"
using Cons.IH[OF 0 1 2 3 _ _] distinct_upd_bin Cons.prems(4,5,6) items_def 4 5 by blast
thus ?case
by simp
qed simp
lemma sound_mono_ptrs_Earley⇩L_bin':
assumes "(k, 𝒢, ω, bs) ∈ wf_earley_input"
assumes "sound_ptrs ω bs" "∀x ∈ bins bs. sound_item 𝒢 ω x"
assumes "mono_red_ptr bs"
assumes "nonempty_derives 𝒢"
shows "sound_ptrs ω (Earley⇩L_bin' k 𝒢 ω bs i) ∧ mono_red_ptr (Earley⇩L_bin' k 𝒢 ω bs i)"
using assms
proof (induction i rule: Earley⇩L_bin'_induct[OF assms(1), case_names Base Complete⇩F Scan⇩F Pass Predict⇩F])
case (Complete⇩F k 𝒢 ω bs i x)
let ?bs' = "upd_bins bs k (Complete⇩L k x bs i)"
have x: "x ∈ set (items (bs ! k))"
using Complete⇩F.hyps(1,2) by force
hence "∀x ∈ set (items (Complete⇩L k x bs i)). sound_item 𝒢 ω x"
using sound_Complete⇩L Complete⇩F.hyps(3) Complete⇩F.prems wf_earley_input_elim wf_bins_impl_wf_items x
by (metis dual_order.refl)
hence sound: "∀x ∈ bins ?bs'. sound_item 𝒢 ω x"
by (metis Complete⇩F.prems(1,3) UnE bins_upd_bins wf_earley_input_elim)
have 0: "k < length bs"
using Complete⇩F.prems(1) wf_earley_input_elim by auto
have 1: "∀e ∈ set (Complete⇩L k x bs i). sound_null_ptr e"
unfolding Complete⇩L_def sound_null_ptr_def by auto
have 2: "∀e ∈ set (Complete⇩L k x bs i). sound_pre_ptr ω bs k e"
unfolding Complete⇩L_def sound_pre_ptr_def by auto
{
fix e
assume a0: "e ∈ set (Complete⇩L k x bs i)"
fix p ps k' pre red
assume a1: "snd e = PreRed p ps" "(k', pre, red) ∈ set (p#ps)"
have "k' = start_item x"
using a0 a1 unfolding Complete⇩L_def by auto
moreover have "wf_item 𝒢 ω x" "end_item x = k"
using Complete⇩F.prems(1) x wf_earley_input_elim wf_bins_kth_bin by blast+
ultimately have 0: "k' ≤ k"
using wf_item_def by blast
have 1: "k' ≠ k"
proof (rule ccontr)
assume "¬ k' ≠ k"
have "sound_item 𝒢 ω x"
using Complete⇩F.prems(1,3) x kth_bin_sub_bins wf_earley_input_elim by (metis subset_eq)
moreover have "is_complete x"
using Complete⇩F.hyps(3) by (auto simp: next_symbol_def split: if_splits)
moreover have "start_item x = k"
using ‹¬ k' ≠ k› ‹k' = start_item x› by auto
ultimately show False
using impossible_complete_item Complete⇩F.prems(1,5) wf_earley_input_elim ‹end_item x = k› ‹wf_item 𝒢 ω x› by blast
qed
have 2: "pre < length (bs!k')"
using a0 a1 index_filter_with_index_lt_length unfolding Complete⇩L_def by (auto simp: items_def; fastforce)
have 3: "red < i+1"
using a0 a1 unfolding Complete⇩L_def by auto
have "fst e = inc_item (fst (bs!k'!pre)) k"
using a0 a1 0 2 Complete⇩F.hyps(1,2,3) Complete⇩F.prems(1) ‹k' = start_item x› unfolding Complete⇩L_def
by (auto simp: items_def, metis filter_with_index_nth nth_map)
moreover have "is_complete (fst (bs!k!red))"
using a0 a1 0 2 Complete⇩F.hyps(1,2,3) Complete⇩F.prems(1) ‹k' = start_item x› unfolding Complete⇩L_def
by (auto simp: next_symbol_def items_def split: if_splits)
moreover have "start_item (fst (bs!k!red)) = end_item (fst (bs!k'!pre))"
using a0 a1 0 2 Complete⇩F.hyps(1,2,3) Complete⇩F.prems(1) ‹k' = start_item x› unfolding Complete⇩L_def
apply (auto simp: items_def)
by (metis dual_order.strict_trans index_filter_with_index_lt_length items_def le_neq_implies_less nth_map nth_mem wf_bins_kth_bin wf_earley_input_elim)
moreover have "(∃N. next_symbol (fst (bs ! k' ! pre)) = Some N ∧ N = lhs_item (fst (bs ! k ! red)))"
using a0 a1 0 2 Complete⇩F.hyps(1,2,3) Complete⇩F.prems(1) ‹k' = start_item x› unfolding Complete⇩L_def
by (auto simp: items_def, metis (mono_tags, lifting) filter_with_index_P filter_with_index_nth nth_map)
ultimately have 4: "completes k (fst (bs!k'!pre)) (fst e) (fst (bs!k!red))"
unfolding completes_def by blast
have "k' < k" "pre < length (bs!k')" "red < i+1" "completes k (fst (bs!k'!pre)) (fst e) (fst (bs!k!red))"
using 0 1 2 3 4 by simp_all
}
hence "∀e ∈ set (Complete⇩L k x bs i). ∀p ps k' pre red. snd e = PreRed p ps ∧ (k', pre, red) ∈ set (p#ps) ⟶
k' < k ∧ pre < length (bs!k') ∧ red < i+1 ∧ completes k (fst (bs!k'!pre)) (fst e) (fst (bs!k!red))"
by force
hence 3: "∀e ∈ set (Complete⇩L k x bs i). sound_prered_ptr bs k e"
unfolding sound_prered_ptr_def using Complete⇩F.hyps(1) items_def
by (smt (verit, del_insts) le_antisym le_eq_less_or_eq le_trans length_map length_pos_if_in_set less_imp_add_positive less_one nat_add_left_cancel_le nat_neq_iff plus_nat.add_0)
have "sound_ptrs ω ?bs' ∧ mono_red_ptr ?bs'"
using sound_mono_ptrs_upds_bin[OF Complete⇩F.prems(2) Complete⇩F.prems(4) 0] 1 2 3 sound_prered_ptr_def
Complete⇩F.prems(1) upd_bins_def wf_earley_input_elim wf_bin_def wf_bins_def
by (smt (verit, ccfv_SIG) list.set_intros(1))
moreover have "(k, 𝒢, ω, ?bs') ∈ wf_earley_input"
using Complete⇩F.hyps Complete⇩F.prems(1) wf_earley_input_Complete⇩L by blast
ultimately have "sound_ptrs ω (Earley⇩L_bin' k 𝒢 ω ?bs' (i+1)) ∧ mono_red_ptr (Earley⇩L_bin' k 𝒢 ω ?bs' (i+1))"
using Complete⇩F.IH Complete⇩F.prems(4-5) sound by blast
thus ?case
using Complete⇩F.hyps by simp
next
case (Scan⇩F k 𝒢 ω bs i x a)
let ?bs' = "upd_bins bs (k+1) (Scan⇩L k ω a x i)"
have "x ∈ set (items (bs ! k))"
using Scan⇩F.hyps(1,2) by force
hence "∀x ∈ set (items (Scan⇩L k ω a x i)). sound_item 𝒢 ω x"
using sound_Scan⇩L Scan⇩F.hyps(3,5) Scan⇩F.prems(1,2,3) wf_earley_input_elim wf_bins_impl_wf_items wf_bins_impl_wf_items by fast
hence sound: "∀x ∈ bins ?bs'. sound_item 𝒢 ω x"
using Scan⇩F.hyps(5) Scan⇩F.prems(1,3) bins_upd_bins wf_earley_input_elim
by (metis UnE add_less_cancel_right)
have 0: "k+1 < length bs"
using Scan⇩F.hyps(5) Scan⇩F.prems(1) wf_earley_input_elim by force
have 1: "∀e ∈ set (Scan⇩L k ω a x i). sound_null_ptr e"
unfolding Scan⇩L_def sound_null_ptr_def by auto
have 2: "∀e ∈ set (Scan⇩L k ω a x i). sound_pre_ptr ω bs (k+1) e"
using Scan⇩F.hyps(1,2,3) unfolding sound_pre_ptr_def Scan⇩L_def scans_def items_def by auto
have 3: "∀e ∈ set (Scan⇩L k ω a x i). sound_prered_ptr bs (k+1) e"
unfolding Scan⇩L_def sound_prered_ptr_def by simp
have "sound_ptrs ω ?bs' ∧ mono_red_ptr ?bs'"
using sound_mono_ptrs_upds_bin[OF Scan⇩F.prems(2) Scan⇩F.prems(4) 0] 0 1 2 3 sound_prered_ptr_def
Scan⇩F.prems(1) upd_bins_def wf_earley_input_elim wf_bin_def wf_bins_def
by (smt (verit, ccfv_threshold) list.set_intros(1))
moreover have "(k, 𝒢, ω, ?bs') ∈ wf_earley_input"
using Scan⇩F.hyps Scan⇩F.prems(1) wf_earley_input_Scan⇩L by metis
ultimately have "sound_ptrs ω (Earley⇩L_bin' k 𝒢 ω ?bs' (i+1)) ∧ mono_red_ptr (Earley⇩L_bin' k 𝒢 ω ?bs' (i+1))"
using Scan⇩F.IH Scan⇩F.prems(4-5) sound by blast
thus ?case
using Scan⇩F.hyps by simp
next
case (Predict⇩F k 𝒢 ω bs i x a)
let ?bs' = "upd_bins bs k (Predict⇩L k 𝒢 a)"
have "x ∈ set (items (bs ! k))"
using Predict⇩F.hyps(1,2) by force
hence "∀x ∈ set (items(Predict⇩L k 𝒢 a)). sound_item 𝒢 ω x"
using sound_Predict⇩L Predict⇩F.hyps(3) Predict⇩F.prems wf_earley_input_elim wf_bins_impl_wf_items by fast
hence sound: "∀x ∈ bins ?bs'. sound_item 𝒢 ω x"
using Predict⇩F.prems(1,3) UnE bins_upd_bins wf_earley_input_elim by metis
have 0: "k < length bs"
using Predict⇩F.prems(1) wf_earley_input_elim by force
have 1: "∀e ∈ set (Predict⇩L k 𝒢 a). sound_null_ptr e"
unfolding sound_null_ptr_def Predict⇩L_def predicts_def by (auto simp: init_item_def)
have 2: "∀e ∈ set (Predict⇩L k 𝒢 a). sound_pre_ptr ω bs k e"
unfolding sound_pre_ptr_def Predict⇩L_def by simp
have 3: "∀e ∈ set (Predict⇩L k 𝒢 a). sound_prered_ptr bs k e"
unfolding sound_prered_ptr_def Predict⇩L_def by simp
have "sound_ptrs ω ?bs' ∧ mono_red_ptr ?bs'"
using sound_mono_ptrs_upds_bin[OF Predict⇩F.prems(2) Predict⇩F.prems(4) 0] 0 1 2 3 sound_prered_ptr_def
Predict⇩F.prems(1) upd_bins_def wf_earley_input_elim wf_bin_def wf_bins_def
by (smt (verit, ccfv_threshold) list.set_intros(1))
moreover have "(k, 𝒢, ω, ?bs') ∈ wf_earley_input"
using Predict⇩F.hyps Predict⇩F.prems(1) wf_earley_input_Predict⇩L by metis
ultimately have "sound_ptrs ω (Earley⇩L_bin' k 𝒢 ω ?bs' (i+1)) ∧ mono_red_ptr (Earley⇩L_bin' k 𝒢 ω ?bs' (i+1))"
using Predict⇩F.IH Predict⇩F.prems(4-5) sound by blast
thus ?case
using Predict⇩F.hyps by simp
qed simp_all
lemma sound_mono_ptrs_Earley⇩L_bin:
assumes "(k, 𝒢, ω, bs) ∈ wf_earley_input"
assumes "sound_ptrs ω bs" "∀x ∈ bins bs. sound_item 𝒢 ω x"
assumes "mono_red_ptr bs"
assumes "nonempty_derives 𝒢"
shows "sound_ptrs ω (Earley⇩L_bin k 𝒢 ω bs) ∧ mono_red_ptr (Earley⇩L_bin k 𝒢 ω bs)"
using assms sound_mono_ptrs_Earley⇩L_bin' Earley⇩L_bin_def by metis
lemma sound_ptrs_Init⇩L:
"sound_ptrs ω (Init⇩L 𝒢 ω)"
unfolding sound_ptrs_def sound_null_ptr_def sound_pre_ptr_def sound_prered_ptr_def
predicts_def scans_def completes_def Init⇩L_def
by (auto simp: init_item_def less_Suc_eq_0_disj)
lemma mono_red_ptr_Init⇩L:
"mono_red_ptr (Init⇩L 𝒢 ω)"
unfolding mono_red_ptr_def Init⇩L_def
by (auto simp: init_item_def less_Suc_eq_0_disj)
lemma sound_mono_ptrs_Earley⇩L_bins:
assumes "k ≤ length ω" "nonempty_derives 𝒢"
shows "sound_ptrs ω (Earley⇩L_bins k 𝒢 ω) ∧ mono_red_ptr (Earley⇩L_bins k 𝒢 ω)"
using assms
proof (induction k)
case 0
have "(0, 𝒢, ω, (Init⇩L 𝒢 ω)) ∈ wf_earley_input"
using assms(2) wf_earley_input_Init⇩L by blast
moreover have "∀x ∈ bins (Init⇩L 𝒢 ω). sound_item 𝒢 ω x"
by (metis Init⇩L_eq_Init⇩F Init⇩F_sub_Earley sound_Earley subsetD wf_Earley)
ultimately show ?case
using sound_mono_ptrs_Earley⇩L_bin sound_ptrs_Init⇩L mono_red_ptr_Init⇩L "0.prems" by fastforce
next
case (Suc k)
have "(Suc k, 𝒢, ω, Earley⇩L_bins k 𝒢 ω) ∈ wf_earley_input"
by (simp add: Suc.prems(1) Suc_leD assms(2) wf_earley_input_intro)
moreover have "sound_ptrs ω (Earley⇩L_bins k 𝒢 ω)"
using Suc by simp
moreover have "∀x ∈ bins (Earley⇩L_bins k 𝒢 ω). sound_item 𝒢 ω x"
by (meson Suc.prems(1) Suc_leD Earley⇩L_bins_sub_Earley⇩F_bins Earley⇩F_bins_sub_Earley assms(2)
sound_Earley subsetD wf_bins_Earley⇩L_bins wf_bins_impl_wf_items)
ultimately show ?case
using Suc.prems sound_mono_ptrs_Earley⇩L_bin Suc.IH by fastforce
qed
lemma sound_mono_ptrs_Earley⇩L:
assumes "nonempty_derives 𝒢"
shows "sound_ptrs ω (Earley⇩L 𝒢 ω) ∧ mono_red_ptr (Earley⇩L 𝒢 ω)"
using assms sound_mono_ptrs_Earley⇩L_bins Earley⇩L_def by (metis dual_order.refl)
subsection ‹Common Definitions›