Theory Earley_Fixpoint

theory Earley_Fixpoint
  imports
    Earley
    Limit
begin

section ‹Earley fixpoint›

subsection ‹Definitions›

definition init_item :: "'a rule ⇒ nat ⇒ 'a item" where
  "init_item r k ≡ Item r 0 k k"

definition inc_item :: "'a item ⇒ nat ⇒ 'a item" where
  "inc_item x k ≡ Item (rule_item x) (dot_item x + 1) (start_item x) k"

definition bin :: "'a item set ⇒ nat ⇒ 'a item set" where
  "bin I k ≡ { x . x ∈ I ∧ end_item x = k }"

definition prev_symbol :: "'a item ⇒ 'a option" where
  "prev_symbol x ≡ if dot_item x = 0 then None else Some (rhs_item x ! (dot_item x - 1))"

definition base :: "'a list ⇒ 'a item set ⇒ nat ⇒ 'a item set" where
  "base ω I k ≡ { x . x ∈ I ∧ end_item x = k ∧ k > 0 ∧ prev_symbol x = Some (ω!(k-1)) }"

definition InitF :: "'a cfg ⇒ 'a item set" where
  "InitF 𝒢 ≡ { init_item r 0 | r. r ∈ set (ℜ 𝒢) ∧ fst r = (𝔖 𝒢) }"

definition ScanF :: "nat ⇒ 'a list ⇒ 'a item set ⇒ 'a item set" where
  "ScanF k ω I ≡ { inc_item x (k+1) | x a.
    x ∈ bin I k ∧
    ω!k = a ∧
    k < length ω ∧
    next_symbol x = Some a }"

definition PredictF :: "nat ⇒ 'a cfg ⇒ 'a item set ⇒ 'a item set" where
  "PredictF k 𝒢 I ≡ { init_item r k | r x.
    r ∈ set (ℜ 𝒢) ∧
    x ∈ bin I k ∧
    next_symbol x = Some (lhs_rule r) }"

definition CompleteF :: "nat ⇒ 'a item set ⇒ 'a item set" where
  "CompleteF k I ≡ { inc_item x k | x y.
    x ∈ bin I (start_item y) ∧
    y ∈ bin I k ∧
    is_complete y ∧
    next_symbol x = Some (lhs_item y) }"

definition EarleyF_bin_step :: "nat ⇒ 'a cfg ⇒ 'a list ⇒ 'a item set ⇒ 'a item set" where
  "EarleyF_bin_step k 𝒢 ω I = I ∪ ScanF k ω I ∪ CompleteF k I ∪ PredictF k 𝒢 I"

definition EarleyF_bin :: "nat ⇒ 'a cfg ⇒ 'a list ⇒ 'a item set ⇒ 'a item set" where
  "EarleyF_bin k 𝒢 ω I ≡ limit (EarleyF_bin_step k 𝒢 ω) I"

fun EarleyF_bins :: "nat ⇒ 'a cfg ⇒ 'a list ⇒ 'a item set" where
  "EarleyF_bins 0 𝒢 ω = EarleyF_bin 0 𝒢 ω (InitF 𝒢)"
| "EarleyF_bins (Suc n) 𝒢 ω = EarleyF_bin (Suc n) 𝒢 ω (EarleyF_bins n 𝒢 ω)"

definition EarleyF :: "'a cfg ⇒ 'a list ⇒ 'a item set" where
  "EarleyF 𝒢 ω ≡ EarleyF_bins (length ω) 𝒢 ω"


subsection ‹Monotonicity and Absorption›

lemma EarleyF_bin_step_empty:
  "EarleyF_bin_step k 𝒢 ω {} = {}"
  unfolding EarleyF_bin_step_def ScanF_def CompleteF_def PredictF_def bin_def by blast

lemma EarleyF_bin_step_setmonotone:
  "setmonotone (EarleyF_bin_step k 𝒢 ω)"
  by (simp add: Un_assoc EarleyF_bin_step_def setmonotone_def)

lemma EarleyF_bin_step_continuous:
  "continuous (EarleyF_bin_step k 𝒢 ω)"
  unfolding continuous_def
proof (standard, standard, standard)
  fix C :: "nat ⇒ 'a item set"
  assume "chain C"
  thus "chain (EarleyF_bin_step k 𝒢 ω ∘ C)"
    unfolding chain_def EarleyF_bin_step_def by (auto simp: ScanF_def PredictF_def CompleteF_def bin_def subset_eq)
next
  fix C :: "nat ⇒ 'a item set"
  assume *: "chain C"
  show "EarleyF_bin_step k 𝒢 ω (natUnion C) = natUnion (EarleyF_bin_step k 𝒢 ω ∘ C)"
    unfolding natUnion_def
  proof standard
    show "EarleyF_bin_step k 𝒢 ω (⋃ {C n |n. True}) ⊆ ⋃ {(EarleyF_bin_step k 𝒢 ω ∘ C) n |n. True}"
    proof standard
      fix x
      assume #: "x ∈ EarleyF_bin_step k 𝒢 ω (⋃ {C n |n. True})"
      show "x ∈ ⋃ {(EarleyF_bin_step k 𝒢 ω ∘ C) n |n. True}"
      proof (cases "x ∈ CompleteF k (⋃ {C n |n. True})")
        case True
        then show ?thesis
          using * unfolding chain_def EarleyF_bin_step_def CompleteF_def bin_def
          apply auto
        proof -
          fix y :: "'a item" and z :: "'a item" and n :: nat and m :: nat
          assume a1: "is_complete z"
          assume a2: "end_item y = start_item z"
          assume a3: "y ∈ C n"
          assume a4: "z ∈ C m"
          assume a5: "next_symbol y = Some (lhs_item z)"
          assume "∀i. C i ⊆ C (Suc i)"
          hence f6: "⋀n m. ¬ n ≤ m ∨ C n ⊆ C m"
            by (meson lift_Suc_mono_le)
          hence f7: "⋀n. ¬ m ≤ n ∨ z ∈ C n"
            using a4 by blast
          have "∃n ≥ m. y ∈ C n"
            using f6 a3 by (meson le_sup_iff subset_eq sup_ge1)
          thus "∃I.
                  (∃n. I = C n ∪
                           ScanF (end_item z) ω (C n) ∪
                           {inc_item i (end_item z) |i.
                              i ∈ C n ∧
                              (∃j.
                                end_item i = start_item j ∧
                                j ∈ C n ∧
                                end_item j = end_item z ∧
                                is_complete j ∧
                                next_symbol i = Some (lhs_item j))} ∪
                           PredictF (end_item z) 𝒢 (C n))
                  ∧ inc_item y (end_item z) ∈ I"
            using f7 a5 a2 a1 by blast
        qed
      next
        case False
        thus ?thesis
          using # Un_iff by (auto simp: EarleyF_bin_step_def ScanF_def PredictF_def bin_def; blast)
      qed
    qed
  next
    show "⋃ {(EarleyF_bin_step k 𝒢 ω ∘ C) n |n. True} ⊆ EarleyF_bin_step k 𝒢 ω (⋃ {C n |n. True})"
      unfolding EarleyF_bin_step_def
      using * by (auto simp: ScanF_def PredictF_def CompleteF_def chain_def bin_def, metis+)
  qed
qed

lemma EarleyF_bin_step_regular:
  "regular (EarleyF_bin_step k 𝒢 ω)"
  by (simp add: EarleyF_bin_step_continuous EarleyF_bin_step_setmonotone regular_def)

lemma EarleyF_bin_idem:
  "EarleyF_bin k 𝒢 ω (EarleyF_bin k 𝒢 ω I) = EarleyF_bin k 𝒢 ω I"
  by (simp add: EarleyF_bin_def EarleyF_bin_step_regular limit_is_idempotent)

lemma ScanF_bin_absorb:
  "ScanF k ω (bin I k) = ScanF k ω I"
  unfolding ScanF_def bin_def by simp

lemma PredictF_bin_absorb:
  "PredictF k 𝒢 (bin I k) = PredictF k 𝒢 I"
  unfolding PredictF_def bin_def by simp

lemma ScanF_Un:
  "ScanF k ω (I ∪ J) = ScanF k ω I ∪ ScanF k ω J"
  unfolding ScanF_def bin_def by blast

lemma PredictF_Un:
  "PredictF k 𝒢 (I ∪ J) = PredictF k 𝒢 I ∪ PredictF k 𝒢 J"
  unfolding PredictF_def bin_def by blast

lemma ScanF_sub_mono:
  "I ⊆ J ⟹ ScanF k ω I ⊆ ScanF k ω J"
  unfolding ScanF_def bin_def by blast

lemma PredictF_sub_mono:
  "I ⊆ J ⟹ PredictF k 𝒢 I ⊆ PredictF k 𝒢 J"
  unfolding PredictF_def bin_def by blast

lemma CompleteF_sub_mono:
  "I ⊆ J ⟹ CompleteF k I ⊆ CompleteF k J"
  unfolding CompleteF_def bin_def by blast

lemma EarleyF_bin_step_sub_mono:
  "I ⊆ J ⟹ EarleyF_bin_step k 𝒢 ω I ⊆ EarleyF_bin_step k 𝒢 ω J"
  unfolding EarleyF_bin_step_def using ScanF_sub_mono PredictF_sub_mono CompleteF_sub_mono by (metis sup.mono)

lemma funpower_sub_mono:
  "I ⊆ J ⟹ funpower (EarleyF_bin_step k 𝒢 ω) n I ⊆ funpower (EarleyF_bin_step k 𝒢 ω) n J"
  by (induction n) (auto simp: EarleyF_bin_step_sub_mono)

lemma EarleyF_bin_sub_mono:
  "I ⊆ J ⟹ EarleyF_bin k 𝒢 ω I ⊆ EarleyF_bin k 𝒢 ω J"
proof standard
  fix x
  assume "I ⊆ J" "x ∈ EarleyF_bin k 𝒢 ω I"
  then obtain n where "x ∈ funpower (EarleyF_bin_step k 𝒢 ω) n I"
    unfolding EarleyF_bin_def limit_def natUnion_def by blast
  hence "x ∈ funpower (EarleyF_bin_step k 𝒢 ω) n J"
    using ‹I ⊆ J› funpower_sub_mono by blast
  thus "x ∈ EarleyF_bin k 𝒢 ω J"
    unfolding EarleyF_bin_def limit_def natUnion_def by blast
qed

lemma ScanF_EarleyF_bin_step_mono:
  "ScanF k ω I ⊆ EarleyF_bin_step k 𝒢 ω I"
  using EarleyF_bin_step_def by blast

lemma PredictF_EarleyF_bin_step_mono:
  "PredictF k 𝒢 I ⊆ EarleyF_bin_step k 𝒢 ω I"
  using EarleyF_bin_step_def by blast

lemma CompleteF_EarleyF_bin_step_mono:
  "CompleteF k I ⊆ EarleyF_bin_step k 𝒢 ω I"
  using EarleyF_bin_step_def by blast

lemma EarleyF_bin_step_EarleyF_bin_mono:
  "EarleyF_bin_step k 𝒢 ω I ⊆ EarleyF_bin k 𝒢 ω I"
proof -
  have "EarleyF_bin_step k 𝒢 ω I ⊆ funpower (EarleyF_bin_step k 𝒢 ω) 1 I"
    by simp
  thus ?thesis
    by (metis EarleyF_bin_def limit_elem subset_eq)
qed

lemma ScanF_EarleyF_bin_mono:
  "ScanF k ω  I ⊆ EarleyF_bin k 𝒢 ω I"
  using ScanF_EarleyF_bin_step_mono EarleyF_bin_step_EarleyF_bin_mono by force

lemma PredictF_EarleyF_bin_mono:
  "PredictF k 𝒢 I ⊆ EarleyF_bin k 𝒢 ω I"
  using PredictF_EarleyF_bin_step_mono EarleyF_bin_step_EarleyF_bin_mono by force

lemma CompleteF_EarleyF_bin_mono:
  "CompleteF k I ⊆ EarleyF_bin k 𝒢 ω I"
  using CompleteF_EarleyF_bin_step_mono EarleyF_bin_step_EarleyF_bin_mono by force

lemma EarleyF_bin_mono:
  "I ⊆ EarleyF_bin k 𝒢 ω I"
  using EarleyF_bin_step_EarleyF_bin_mono EarleyF_bin_step_def by blast

lemma InitF_sub_EarleyF_bins:
  "InitF 𝒢 ⊆ EarleyF_bins n 𝒢 ω"
  apply (induction n)
   apply auto
  using EarleyF_bin_mono by blast+


subsection ‹Soundness›

lemma InitF_sub_Earley:
  "InitF 𝒢 ⊆ Earley 𝒢 ω"
  unfolding InitF_def init_item_def using Init by blast

lemma ScanF_sub_Earley:
  assumes "I ⊆ Earley 𝒢 ω"
  shows "ScanF k ω I ⊆ Earley 𝒢 ω"
  unfolding ScanF_def inc_item_def bin_def using assms Scan 
  by (smt (verit, ccfv_SIG) item.exhaust_sel mem_Collect_eq subsetD subsetI)

lemma PredictF_sub_Earley:
  assumes "I ⊆ Earley 𝒢 ω"
  shows "PredictF k 𝒢 I ⊆ Earley 𝒢 ω"
  unfolding PredictF_def init_item_def bin_def using assms Predict
  using item.exhaust_sel by blast

lemma CompleteF_sub_Earley:
  assumes "I ⊆ Earley 𝒢 ω"
  shows "CompleteF k I ⊆ Earley 𝒢 ω"
  unfolding CompleteF_def inc_item_def bin_def using assms Complete
  by (smt (verit, del_insts) item.exhaust_sel mem_Collect_eq subset_eq)

lemma EarleyF_bin_step_sub_Earley:
  assumes "I ⊆ Earley 𝒢 ω"
  shows "EarleyF_bin_step k 𝒢 ω I ⊆ Earley 𝒢 ω"
  unfolding EarleyF_bin_step_def using assms CompleteF_sub_Earley PredictF_sub_Earley ScanF_sub_Earley by (metis le_supI)

lemma EarleyF_bin_sub_Earley:
  assumes "I ⊆ Earley 𝒢 ω"
  shows "EarleyF_bin k 𝒢 ω I ⊆ Earley 𝒢 ω"
  using assms EarleyF_bin_step_sub_Earley by (metis EarleyF_bin_def limit_upperbound)

lemma EarleyF_bins_sub_Earley:
  shows "EarleyF_bins n 𝒢 ω ⊆ Earley 𝒢 ω"
  by (induction n) (auto simp: EarleyF_bin_sub_Earley InitF_sub_Earley)

lemma EarleyF_sub_Earley:
  shows "EarleyF 𝒢 ω ⊆ Earley 𝒢 ω"
  by (simp add: EarleyF_bins_sub_Earley EarleyF_def)

theorem soundness_EarleyF:
  assumes "recognizing (EarleyF 𝒢 ω) 𝒢 ω"
  shows "𝒢 ⊢ [𝔖 𝒢] ⇒* ω"
  using soundness_Earley EarleyF_sub_Earley assms recognizing_def by (metis subsetD)


subsection ‹Completeness›

lemma EarleyF_bin_sub_EarleyF_bin:
  assumes "InitF 𝒢 ⊆ I"
  assumes "∀k' < k. bin (Earley 𝒢 ω) k' ⊆ I"
  assumes "base ω (Earley 𝒢 ω) k ⊆ I"
  shows "bin (Earley 𝒢 ω) k ⊆ bin (EarleyF_bin k 𝒢 ω I) k"
proof standard
  fix x
  assume *: "x ∈ bin (Earley 𝒢 ω) k" 
  hence "x ∈ Earley 𝒢 ω"
    using bin_def by blast
  thus "x ∈ bin (EarleyF_bin k 𝒢 ω I) k"
    using assms *
  proof (induction rule: Earley.induct)
    case (Init r)
    thus ?case
      unfolding InitF_def init_item_def bin_def using EarleyF_bin_mono by fast
  next
    case (Scan x r b i j a)
    have "j+1 = k"
      using Scan.prems(4) bin_def by (metis (mono_tags, lifting) CollectD item.sel(4))
    have "prev_symbol (Item r (b+1) i (j+1)) = Some (ω!(k-1))"
      using Scan.hyps(1,3,5) ‹j+1 = k› by (auto simp: next_symbol_def prev_symbol_def rhs_item_def split: if_splits)
    hence "Item r (b+1) i (j+1) ∈ base ω (Earley 𝒢 ω) k"
      unfolding base_def using Scan.prems(4) bin_def by fastforce
    hence "Item r (b+1) i (j+1) ∈ I"
      using Scan.prems(3) by blast
    hence "Item r (b+1) i (j+1) ∈ EarleyF_bin k 𝒢 ω I"
      using EarleyF_bin_mono by blast
    thus ?case
      using ‹j+1 = k› bin_def by fastforce
  next
    case (Predict x r b i j r')
    have "j = k"
      using Predict.prems(4) bin_def by (metis (mono_tags, lifting) CollectD item.sel(4))
    hence "x ∈ bin (Earley 𝒢 ω) k"
      using Predict.hyps(1,2) bin_def by fastforce
    hence "x ∈ bin (EarleyF_bin k 𝒢 ω I) k"
      using Predict.IH Predict.prems(1-3) by blast
    hence "Item r' 0 j j ∈ PredictF k 𝒢 (EarleyF_bin k 𝒢 ω I)"
      unfolding PredictF_def init_item_def using Predict.hyps(1,3,4) ‹j = k› by blast
    hence "Item r' 0 j j ∈ EarleyF_bin_step k 𝒢 ω (EarleyF_bin k 𝒢 ω I)"
      using PredictF_EarleyF_bin_step_mono by blast
    hence "Item r' 0 j j ∈ EarleyF_bin k 𝒢 ω I"
      using EarleyF_bin_idem EarleyF_bin_step_EarleyF_bin_mono by blast
    thus ?case
      by (simp add: ‹j = k› bin_def)
  next
    case (Complete x rx bx i j y ry by l)
    have "l = k"
      using Complete.prems(4) bin_def by (metis (mono_tags, lifting) CollectD item.sel(4))
    hence "y ∈ bin (Earley 𝒢 ω) l"
      using Complete.hyps(3,4) bin_def by fastforce
    hence 0: "y ∈ bin (EarleyF_bin k 𝒢 ω I) k"
      using Complete.IH(2) Complete.prems(1-3) ‹l = k› by blast
    have 1: "x ∈ bin (EarleyF_bin k 𝒢 ω I) (start_item y)"
    proof (cases "j = k")
      case True
      hence "x ∈ bin (Earley 𝒢 ω) k"
        using Complete.hyps(1,2) bin_def by fastforce
      hence "x ∈ bin (EarleyF_bin k 𝒢 ω I) k"
        using Complete.IH(1) Complete.prems(1-3) by blast
      thus ?thesis
        using Complete.hyps(3) True by simp
    next
      case False
      hence "j < k"
        using ‹l = k› wf_Earley wf_item_def Complete.hyps(3,4) by force
      moreover have "x ∈ bin (Earley 𝒢 ω) j"
        using Complete.hyps(1,2) bin_def by force
      ultimately have "x ∈ I"
        using Complete.prems(2) by blast
      hence "x ∈ bin (EarleyF_bin k 𝒢 ω I) j"
        using Complete.hyps(1) EarleyF_bin_mono bin_def by fastforce
      thus ?thesis
        using Complete.hyps(3) by simp
    qed
    have "Item rx (bx + 1) i k ∈ CompleteF k (EarleyF_bin k 𝒢 ω I)"
      unfolding CompleteF_def inc_item_def using 0 1 Complete.hyps(1,5,6) by force
    hence "Item rx (bx + 1) i k ∈ EarleyF_bin_step k 𝒢 ω (EarleyF_bin k 𝒢 ω I)"
      unfolding EarleyF_bin_step_def by blast
    hence "Item rx (bx + 1) i k ∈ EarleyF_bin k 𝒢 ω I"
      using EarleyF_bin_idem EarleyF_bin_step_EarleyF_bin_mono by blast
    thus ?case
      using bin_def ‹l = k› by fastforce
  qed
qed

lemma Earley_base_sub_EarleyF_bin:
  assumes "InitF 𝒢 ⊆ I"
  assumes "∀k' < k. bin (Earley 𝒢 ω) k' ⊆ I"
  assumes "base ω (Earley 𝒢 ω) k ⊆ I"
  assumes "is_word 𝒢 ω"
  shows "base ω (Earley 𝒢 ω) (k+1) ⊆ bin (EarleyF_bin k 𝒢 ω I) (k+1)"
proof standard
  fix x
  assume *: "x ∈ base ω (Earley 𝒢 ω) (k+1)" 
  hence "x ∈ Earley 𝒢 ω"
    using base_def by blast
  thus "x ∈ bin (EarleyF_bin k 𝒢 ω I) (k+1)"
    using assms *
  proof (induction rule: Earley.induct)
    case (Init r)
    have "k = 0"
      using Init.prems(5) unfolding base_def by simp
    hence False
      using Init.prems(5) unfolding base_def by simp
    thus ?case
      by blast
  next
    case (Scan x r b i j a)
    have "j = k"
      using Scan.prems(5) base_def by (metis (mono_tags, lifting) CollectD add_right_cancel item.sel(4))
    hence "x ∈ bin (EarleyF_bin k 𝒢 ω I) k"
      using EarleyF_bin_sub_EarleyF_bin Scan.prems Scan.hyps(1,2) bin_def
      by (metis (mono_tags, lifting) CollectI item.sel(4) subsetD)
    hence "Item r (b+1) i (j+1) ∈ ScanF k ω (EarleyF_bin k 𝒢 ω I)"
      unfolding ScanF_def inc_item_def using Scan.hyps ‹j = k› by force
    hence "Item r (b+1) i (j+1) ∈ EarleyF_bin_step k 𝒢 ω (EarleyF_bin k 𝒢 ω I)"
      using ScanF_EarleyF_bin_step_mono by blast
    hence "Item r (b+1) i (j+1) ∈ EarleyF_bin k 𝒢 ω I"
      using EarleyF_bin_idem EarleyF_bin_step_EarleyF_bin_mono by blast
    thus ?case
      using ‹j = k› bin_def by fastforce
  next
    case (Predict x r b i j r')
    have False
      using Predict.prems(5) unfolding base_def by (auto simp: prev_symbol_def)
    thus ?case
      by blast
  next
    case (Complete x rx bx i j y ry by l)
    have "l-1 < length ω"
      using Complete.prems(5) base_def wf_Earley wf_item_def
      by (metis (mono_tags, lifting) CollectD add.right_neutral add_Suc_right add_diff_cancel_right' item.sel(4) less_eq_Suc_le plus_1_eq_Suc)
    hence "ω!(l-1) ∉ nonterminals 𝒢"
      using Complete.prems(4) is_word_def by force
    moreover have "lhs_item y ∈ nonterminals 𝒢"
      using Complete.hyps(3,4) wf_Earley wf_item_def lhs_item_def lhs_rule_def nonterminals_def
      by (metis UnCI image_eqI list.set_map)
    moreover have "prev_symbol (Item rx (bx+1) i l) = next_symbol x"
      using Complete.hyps(1,6)
      by (auto simp: next_symbol_def prev_symbol_def is_complete_def rhs_item_def split: if_splits)
    moreover have "prev_symbol (Item rx (bx+1) i l) = Some (ω!(l-1))"
      using Complete.prems(5) base_def by (metis (mono_tags, lifting) CollectD item.sel(4))
    ultimately have False
      using Complete.hyps(6) Complete.prems(4) by simp
    thus ?case
      by blast
  qed
qed

lemma EarleyF_bin_k_sub_EarleyF_bins:
  assumes "is_word 𝒢 ω" "k ≤ n"
  shows "bin (Earley 𝒢 ω) k ⊆ EarleyF_bins n 𝒢 ω"
  using assms
proof (induction n arbitrary: k)
  case 0
  have "bin (Earley 𝒢 ω) 0 ⊆ bin (EarleyF_bin 0 𝒢 ω (InitF 𝒢)) 0"
    using EarleyF_bin_sub_EarleyF_bin base_def by fastforce
  thus ?case
    unfolding bin_def using "0.prems"(2) by auto
next
  case (Suc n)
  show ?case
  proof (cases "k ≤ n")
    case True
    thus ?thesis
      using Suc EarleyF_bin_mono by force
  next
    case False
    hence "k = n+1"
      using Suc.prems(2) by force
    have 0: "∀k' < k. bin (Earley 𝒢 ω) k' ⊆ EarleyF_bins n 𝒢 ω"
      using Suc by simp
    moreover have "base ω (Earley 𝒢 ω) k ⊆ EarleyF_bins n 𝒢 ω"
    proof -
      have "∀k' < k-1. bin (Earley 𝒢 ω) k' ⊆ EarleyF_bins n 𝒢 ω"
        using Suc ‹k = n + 1› by auto
      moreover have "base ω (Earley 𝒢 ω) (k-1) ⊆ EarleyF_bins n 𝒢 ω"
        using 0 bin_def base_def False ‹k = n+1› 
        by (smt (verit) Suc_eq_plus1 diff_Suc_1 linorder_not_less mem_Collect_eq subsetD subsetI)
      ultimately have "base ω (Earley 𝒢 ω) k ⊆ bin (EarleyF_bin n 𝒢 ω (EarleyF_bins n 𝒢 ω)) k"
        using Suc.prems(1,2) Earley_base_sub_EarleyF_bin ‹k = n + 1› InitF_sub_EarleyF_bins by (metis add_diff_cancel_right')
      hence "base ω (Earley 𝒢 ω) k ⊆ bin (EarleyF_bins n 𝒢 ω) k"
        by (metis EarleyF_bins.elims EarleyF_bin_idem)
      thus ?thesis
        using bin_def by blast
    qed
    ultimately have "bin (Earley 𝒢 ω) k ⊆ bin (EarleyF_bin k 𝒢 ω (EarleyF_bins n 𝒢 ω)) k"
      using EarleyF_bin_sub_EarleyF_bin InitF_sub_EarleyF_bins by metis
    thus ?thesis
      using EarleyF_bins.simps(2) ‹k = n + 1› bin_def by auto
  qed
qed

lemma Earley_sub_EarleyF:
  assumes "is_word 𝒢 ω"
  shows "Earley 𝒢 ω ⊆ EarleyF 𝒢 ω"
proof -
  have "∀k ≤ length ω. bin (Earley 𝒢 ω) k ⊆ EarleyF 𝒢 ω"
    by (simp add: EarleyF_bin_k_sub_EarleyF_bins EarleyF_def assms)
  thus ?thesis
    using wf_Earley wf_item_def bin_def by blast
qed

theorem completeness_EarleyF:
  assumes "𝒢 ⊢ [𝔖 𝒢] ⇒* ω" "is_word 𝒢 ω"
  shows "recognizing (EarleyF 𝒢 ω) 𝒢 ω"
  using assms Earley_sub_EarleyF EarleyF_sub_Earley completeness_Earley by (metis subset_antisym)


subsection ‹Correctness›

theorem Earley_eq_EarleyF:
  assumes "is_word 𝒢 ω"
  shows "Earley 𝒢 ω = EarleyF 𝒢 ω"
  using Earley_sub_EarleyF EarleyF_sub_Earley assms by blast

theorem correctness_EarleyF:
  assumes "is_word 𝒢 ω"
  shows "recognizing (EarleyF 𝒢 ω) 𝒢 ω ⟷ 𝒢 ⊢ [𝔖 𝒢] ⇒* ω"
  using assms Earley_eq_EarleyF correctness_Earley by fastforce

end