Quelle  TheoremD14.thy

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 ∈ J k' u' ∧
   item_end y = k' ∧ X ∈ (T 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 ∈ J k'a u'a ∧
     item_end y = k'a ∧
     X ∈ T 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 J_induct[consumes 1, case_names Induct]:
  assumes "x ∈ J k u"
  assumes induct: "∧ x k u . (∧ x' k' u'. x' ∈ J k' u' ==> indexlt k' u' k u ==> P x' k' u')
                     ==> x ∈ J 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 ∈ J (fst (fst a)) (snd (fst a)) ⟶ P (snd a) (fst (fst a)) (snd (fst a))"
  have "x ∈ J 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 ∈ J k u ==> item_end x > k ==> produced_by_scan_step x k u"
proof (induct rule: J_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 J_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 ∈ J (Suc k') 0" by auto
        then have "x ∈ π k {} (I k')" by (simp add: k') 
        then have "item_end x = k ∨ x ∈ I 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 ∈ J k' u'" using I.simps natUnion_ex by fastforce
            then obtain u' where u': "x ∈ J 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 ∈ J k (Suc u')" by metis
        then have x_in_π: "x ∈ π k (T k u) (J k u')" using u' J.simps by metis
        have "x ∈ J k u' ∨ x ∉ J 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 (T k u) k ∘ Complete k ∘ Predict k" by blast
            have "x ∈ limit f (J 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) (J k u') ∧
               x ∉ funpower f n (J k u')" by blast
            obtain Y where Y: "Y = funpower f n (J k u')"
              by blast
            have x_f_Y: "x ∈ f Y ∧ x ∉ Y" using Y n by auto
            then have "x ∈ Scan (T 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) ∈ (T 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 (J k u')" using Y limit_def natUnion_superset by fastforce
                then have "Y ⊆ π k (T k u) (J k u')" using f by (simp add: π_functional)  
                then have Y_in_J: "Y ⊆ J k u" using u' by simp
                then have in_J: "Complete k (Predict k Y) ⊆ J k u"
                proof - (* automatically generated *)
                  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 (J k u) (Complete k (Predict k Y)) ∈ Complete k (π k (T k (Suc nn)) (J 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 
                      J.simps(2) Y_in_J 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) ∈ T 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_J 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_P:
  assumes "p ∈ P k u"
  shows "Prefixes p ⊆ 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_J_subset_J:
  "Scan (T k (Suc u)) k (J k u) ⊆ J k (Suc u)"
by (metis (no_types, lifting) Scan_π_fix J.simps(2) J_subset_Suc_u monoD mono_Scan)

lemma subset_Jk: "u ≤ v ==> J k u ⊆ J k v"
  thm J_subset_Suc_u
  by (rule subset_fSuc, rule J_subset_Suc_u) 

lemma subset_JIk: "J k u ⊆ I k" by (auto simp add: natUnion_def)

lemma subset_IJSuc: "I k ⊆ J (Suc k) u" 
proof -
  have a: "I k ⊆ J (Suc k) 0" 
    apply (simp only: J.simps)
    using π_apply_setmonotone by blast    
  show ?thesis 
    apply (case_tac "u = 0")
    apply (simp only: a)
    apply (rule subset_trans[OF a subset_Jk])
    by auto
qed

lemma subset_ISuc: "I k ⊆ I (Suc k)"
  by (rule subset_trans[OF subset_IJSuc subset_JIk])

lemma subset_I: "i ≤ j ==> I i ⊆ I j"
  by (rule subset_fSuc[where u=i and v=j and f = I, OF subset_ISuc])

lemma subset_J :
  assumes leq: "k' < k ∨ (k' = k ∧ u' ≤ u)"
  shows "J k' u' ⊆ J k u"
proof -
  from leq show ?thesis
  proof (induct rule: disjCases2)
    case 1
    have s1: "J k' u' ⊆ I k'" by (rule_tac subset_JIk) 
    have s2: "I k' ⊆ I (k - 1)" 
      apply (rule_tac subset_I)
      using 1 by arith
    from subset_IJSuc[where k="k - 1"] 1 have s3: "I (k - 1) ⊆ J k 0"
      by simp
    have s4: "J k 0 ⊆ J k u" by (rule_tac subset_Jk, simp)
    from s1 s2 s3 s4 subset_trans show ?case by blast
  next
    case 2 thus ?case by (simp add : subset_Jk)
  qed
qed  

lemma J_subset:
  assumes "indexle k' u' k u"
  shows "J k' u' ⊆ J k u"
using subset_J 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 (J k u) = Gen (paths_le k (P k u)) ∧ T k u = Z k u
    ∧ items_le k (I k) = Gen (paths_le k (Q 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 J_eq_P: "items_le k (J k 0) = Gen (paths_le k (P k 0))" 
          by (simp only: 1 thmD8 items_le_paths_le)
        show ?case using thmD13[OF J_eq_P 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 (J k 0) = Gen (paths_le k (P k 0))"          
        proof -
          have simp_left: "items_le k (J k 0) = π k {} (items_le k (I k'))"
            using items_le_π_swap k' wellformed_items_I by auto 
          have simp_right: "Gen (paths_le k (P k 0)) = natUnion (λ v. Gen (paths_le k (P k' v)))"
            by (simp add: k' paths_le_pointwise pointwise_Gen pointwise_natUnion_swap)            
          {
            fix v :: nat
            have split_J: "items_le k (J k' v) = items_le k' (J k' v) ∪ items_eq k (J k' v)" 
              using k'  items_le_split_via_eq by blast
            have sub1: "items_le k' (J k' v) ⊆ natUnion (λ v. Gen (paths_le k (P k' v)))"
            proof -
              have h: "items_le k' (J k' v) ⊆ Gen (paths_le k (P k' v))"
              proof - (* automatically generated *)
                have f1: "items_le k' (Gen (P k' v)) ∪ items_eq (Suc k') (Gen (P k' v)) =
                  Gen (paths_le k (P 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' (J k' v) = items_le k' (Gen (P 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 (P k' v)) ⊆ natUnion (λ v. Gen (paths_le k (P 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 (J k' v)"
              have x_in_J: "x ∈ J 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_J 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 ∈ J k'' v'' ∧ item_end y = k'' ∧ X ∈ T 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'' (J k'' v'')"
                using items_le_def LocalLexing_axioms le_refl mem_Collect_eq by blast 
              have y_in_Gen: "y ∈ Gen(paths_le k'' (P k'' v''))"
              proof - (* automatically generated *)
                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 ∈ P k'' v'' ∧ pvalid p y"
                by (meson Gen_implies_pvalid paths_le_is_filter rev_subsetD)
              then obtain p where p: "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_X T_subset_TokensAt X_are_terminals 
                  rev_subsetD terminal_of_token_def) 
              then have admissible_p_X: "admissible (p@[X])" by simp
              have X_in_Z: "X ∈ Z k'' (Suc v'')" by (metis (no_types, lifting) Suc_lessD Z_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_P_k''_v'': "p@[X] ∈ P k'' (Suc v'')"   
                apply (simp only: P.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_Z)
                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 "P k'' (Suc v'') ⊆ P k' (Suc v)"
                by (metis indexle_def indexlt_simp less_or_eq_imp_le subset_P) 
              with pX_in_P_k''_v'' have pX_in_P_k': "p@[X] ∈ P 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 (P k' (Suc v))"
                using lessI less_Suc_eq_le mem_Collect_eq pX_in_P_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_J 
                  wellformed_items_def by auto
              have wellformed_p_X: "wellformed_tokens (p@[X])"
                using P_wellformed pX_in_P_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 (P k' (Suc v)))" using pX_dom Gen_def 
                LocalLexing_axioms mem_Collect_eq by auto 
            }
            then have sub2: "items_eq k (J k' v) ⊆ natUnion (λ v. Gen (paths_le k (P k' v)))"
              by (meson dual_order.trans natUnion_superset subsetI)                                       
            have suffices3: "items_le k (J k' v) ⊆ natUnion (λ v. Gen (paths_le k (P k' v)))"
              using split_J sub1 sub2 by blast
            have "items_le k (J k' v) ⊆ Gen (paths_le k (P k 0))"
              using suffices3 simp_right by blast
          }
          note suffices2 = this
          have items_le_natUnion_swap: "items_le k (I k') = natUnion(λ v. items_le k (J k' v))"
            by (simp add: items_le_pointwise pointwise_natUnion_swap)            
          then have suffices1: "items_le k (I k') ⊆ Gen (paths_le k (P k 0))"
            using suffices2 natUnion_upperbound by metis    
          have sub_lemma: "items_le k (J k 0) ⊆ Gen (paths_le k (P k 0))"
          proof -
            have "items_le k (J k 0) ⊆ Gen (P 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 (I k')) = π k {} (items_le k (natUnion (J k')))" by simp
          then have eq2: "π k {} (items_le k (natUnion (J k'))) =
            π k {} (natUnion (λ v. items_le k (J k' v)))"
            using items_le_natUnion_swap by auto
          from simp_left eq1 eq2 
          have simp_left': "items_le k (J k 0) = π k {} (natUnion (λ v. items_le k (J k' v)))"
            by metis
          {
            fix v :: nat
            fix q :: "token list"
            fix x :: item
            assume q_dom: "q ∈ paths_eq k (P k' v)"
            assume pvalid_q_x: "pvalid q x"
            have q_in_P: "q ∈ P 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_P pX] obtain k'' v'' where k'':
              "indexlt k'' v'' k' v ∧ q ∈ P k'' (Suc v'') ∧ charslength p = k'' ∧
               X ∈ Z k'' (Suc v'')" by blast
            have h1: "p ∈ P"
              by (metis (no_types, lifting) LocalLexing.P_covers_P LocalLexing_axioms 
                append_Nil2 is_prefix_cancel is_prefix_empty pX prefixes_are_paths q_in_P 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 ⊆ X k''" using Z_subset_X 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, α @ β) ∈ R"
              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 [S] (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 ⊆ P k'' (Suc v'')" 
              apply (rule Prefixes_subset_P)
              using k'' by blast
            from subset1 subset2 have "Prefixes p ⊆ P k'' (Suc v'')" by blast
            then have "Prefixes p ⊆ paths_le k'' (P k'' (Suc v''))" 
              using k'' Prefixes_subset_paths_le by blast            
            then have subset3: "Gen (Prefixes p) ⊆ Gen (paths_le k'' (P 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'' (J k'' (Suc v'')) = Gen (paths_le k'' (P k'' (Suc v'')))"
              by blast
            from less(1)[OF k''_less_k k''_Doc_bound, of "Suc(Suc v'')"]
            have induct2: "T k'' (Suc (Suc v'')) = Z k'' (Suc (Suc v''))" by blast
            have subset4: "Gen (Prefixes p) ⊆ items_le k'' (J 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'' (J 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'' "J k'' (Suc v'')"] h9
            have subset7: "Scan T k'' (items_le k'' (J k'' (Suc v'')))
              ⊆ items_le k (Scan T k'' (J k'' (Suc v'')))" by simp
            have "T ⊆ Z k'' (Suc (Suc v''))" using T k''
              using Z_subset_Suc rev_subsetD singletonD subsetI by blast 
            then have T_subset_T: "T ⊆ T k'' (Suc (Suc v''))" using induct2 by auto
            have subset8: "Scan T k'' (J k'' (Suc v'')) ⊆
              Scan (T k'' (Suc (Suc v''))) k'' (J k'' (Suc v''))" 
              using T_subset_T Scan_mono_tokens by blast
            have subset9: "Scan (T k'' (Suc (Suc v''))) k'' (J k'' (Suc v'')) ⊆ J k'' (Suc (Suc v''))"
              by (rule Scan_J_subset_J)
            have subset10: "(Scan T k'' (J k'' (Suc v''))) ⊆ J 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: "J k'' (Suc (Suc v'')) ⊆ J k' (Suc (Suc v''))"
              using J_subset by blast
            have subset12: "Scan T k'' (J k'' (Suc v'')) ⊆ J k' (Suc (Suc v''))"
              using subset8 subset9 subset10 subset11 by blast
            then have subset13: "items_le k (Scan T k'' (J k'' (Suc v''))) ⊆
              items_le k (J 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 (J k' (Suc (Suc v'')))"
              using subset6 subset7 subset13 by blast
            then have x_in': "x ∈ π k {} (items_le k (J 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 (J k' v)))"
              by (meson k' mono_π mono_subset_elem natUnion_superset)
          }
          note suffices6 = this
          {
            fix v :: nat
            have "Gen (paths_eq k (P k' v)) ⊆ π k {} (natUnion (λ v. items_le k (J k' v)))"
              using suffices6 by (meson Gen_implies_pvalid subsetI) 
          }
          note suffices5 = this
          {
            fix v :: nat
            have "paths_le k (P k' v) = paths_le k' (P k' v) ∪ paths_eq k (P k' v)"
              using  paths_le_split_via_eq k' by metis
            then have Gen_split: "Gen (paths_le k (P k' v)) =
              Gen (paths_le k' (P k' v)) ∪ Gen(paths_eq k (P k' v))" using Gen_union by metis
            have case_le: "Gen (paths_le k' (P k' v)) ⊆ π k {} (natUnion (λ v. items_le k (J 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' (J k' v) = Gen (paths_le k' (P k' v))" by blast
              then have "Gen (paths_le k' (P k' v)) ⊆ natUnion (λ v. items_le k (J 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 (P k' v)) ⊆ π k {} (natUnion (λ v. items_le k (J k' v)))"
              using Gen_split case_le suffices5 UnE rev_subsetD subsetI by blast 
          }
          note suffices4 = this
          have super_lemma: "Gen (paths_le k (P k 0)) ⊆ items_le k (J 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