Quelle  TheoremD5.thy

theory TheoremD5
imports TheoremD4
begin

context LocalLexing begin

lemma Scan_empty: "Scan {} k I = I"
  by (simp add: Scan_def)

lemma π_no_tokens: "π k {} I = limit (λ I. Complete k (Predict k I)) I"
  by (simp add: π_def Scan_empty)

lemma bin_elem: "x ∈ bin I k ==> x ∈ I"
  by (auto simp add: bin_def)

lemma Gen_implies_pvalid: "x ∈ Gen P ==> ∃ p ∈ P. pvalid p x"
  by (auto simp add: Gen_def)

lemma wellformed_init_item[simp]: "r ∈ R ==> k ≤ length Doc ==> wellformed_item (init_item r k)"
  by (simp add: init_item_def wellformed_item_def)

lemma init_item_origin[simp]: "item_origin (init_item r k) = k"
  by (auto simp add: item_origin_def init_item_def)

lemma init_item_end[simp]: "item_end (init_item r k) = k"
  by (auto simp add: item_end_def init_item_def)

lemma init_item_nonterminal[simp]: "item_nonterminal (init_item r k) = fst r"
  by (auto simp add: init_item_def item_nonterminal_def)

lemma init_item_α[simp]: "item_α (init_item r k) = []"
  by (auto simp add: init_item_def item_α_def)

lemma Predict_elem_in_Gen:
  assumes I_in_Gen_P: "I ⊆ Gen P"
  assumes k: "k ≤ length Doc"
  assumes x_in_Predict: "x ∈ Predict k I"
  shows "x ∈ Gen P"
proof -
  have "x ∈ I ∨ (∃ r y. r ∈ R ∧ x = init_item r k ∧ y ∈ bin I k ∧ next_symbol y = Some(fst r))"
    using x_in_Predict by (auto simp add: Predict_def)
  then show ?thesis
  proof (induct rule: disjCases2)
    case 1 thus ?case using I_in_Gen_P by blast
  next
    case 2 
    then obtain r y where ry: "r ∈ R ∧ x = init_item r k ∧ y ∈ bin I k ∧
      next_symbol y = Some (fst r)" by blast
    then have "∃ p ∈ P. pvalid p y"
      using Gen_implies_pvalid I_in_Gen_P bin_elem subsetCE by blast 
    then obtain p where p: "p ∈ P ∧ pvalid p y" by blast
    have wellformed_p: "wellformed_tokens p" using p by (auto simp add: pvalid_def)
    have wellformed_x: "wellformed_item x"
      by (simp add: ry k)
    from ry have "item_end y = k" by (auto simp add: bin_def)
    with p have charslength_p[simplified]: "charslength p = k" by (auto simp add: pvalid_def)
    have item_end_x: "item_end x = k" by (simp add: ry)
    have pvalid_x: "pvalid p x"
      apply (auto simp add: pvalid_def)
      apply (simp add: wellformed_p)
      apply (simp add: wellformed_x)
      apply (rule_tac x="length p" in exI)
      apply (auto simp add: charslength_p ry)
      by (metis append_Cons next_symbol_starts_item_β p pvalid_def 
        pvalid_is_derivation_terminals_item_β ry)
    then show ?case using Gen_def mem_Collect_eq p by blast
 qed
qed

lemma Predict_subset_Gen:
  assumes "I ⊆ Gen P"
  assumes "k ≤ length Doc"
  shows "Predict k I ⊆ Gen P"
using Predict_elem_in_Gen assms by blast

lemma nth_superfluous_append[simp]: "i < length a ==> (a@b)!i = a!i"
by (simp add: nth_append)

lemma tokens_nth_in_Z: 
  "p ∈ P ==> ∀ i. i < length p ⟶ (∃ u. p ! i ∈ Z (charslength (take i p)) u)"
proof (induct rule: P_induct)
  case Base thus ?case by simp
next
  case (Induct p k u)
  then have "p ∈ limit (Append (Z k (Suc u)) k) (P k u)" by simp
  then show ?case
  proof (induct rule: limit_induct)
    case (Init p) thus ?case using Induct by auto
  next
    case (Iterate p Y)
    from Iterate(2) have "p ∈ Y ∨ (∃ q t. p = q@[t] ∧ q ∈ by_length k Y ∧ t ∈ Z k (Suc u) ∧
      admissible (q @ [t]))"
      by (auto simp add: Append_def)
    then show ?case
    proof (induct rule: disjCases2)
      case 1 thus ?case using Iterate(1) by auto
    next
      case 2 
      then obtain q t where 
        qt: "p = q @ [t] ∧ q ∈ by_length k Y ∧ t ∈ Z k (Suc u) ∧ admissible (q @ [t])" by blast
      then have q_in_Y: "q ∈ Y" by auto
      with qt have k: "k = charslength q" by auto
      with qt have t: "t ∈ Z k (Suc u)" by auto
      show ?case
      proof(auto simp add: qt)
        fix i
        assume i: "i < Suc (length q)"
        then have "i < length q ∨ i = length q" by arith
        then show "∃u. (q @ [t]) ! i ∈ Z (length (chars (take i q))) u"
        proof (induct rule: disjCases2)
          case 1
            from Iterate(1)[OF q_in_Y]
            show ?case by (simp add: 1)
        next
          case 2
            show ?case 
              apply (auto simp add: 2)
              apply (rule_tac x="Suc u" in exI)
              using k t by auto 
        qed
      qed
    qed
  qed
qed

lemma path_append_token:
  assumes p: "p ∈ P k u"
  assumes t: "t ∈ Z k (Suc u)"
  assumes pt: "admissible (p@[t])"
  assumes k: "charslength p = k"
  shows "p@[t] ∈ P k (Suc u)"
apply (simp only: P.simps)
apply (rule_tac n="Suc 0" in limit_elem)
using p t pt k apply (auto simp only: Append_def funpower.simps)
by fastforce

definition indexlt_rel :: "((nat × nat) × (nat × nat)) set" where
  "indexlt_rel = less_than <*lex*> less_than"

definition indexlt :: "nat ==> nat ==> nat ==> nat ==> bool" where
  "indexlt k' u' k u = (((k', u'), (k, u)) ∈ indexlt_rel)"

lemma indexlt_simp: "indexlt k' u' k u = (k' < k ∨ (k' = k ∧ u' < u))"
  by (auto simp add: indexlt_def indexlt_rel_def)

lemma wf_indexlt_rel: "wf indexlt_rel"
  using indexlt_rel_def pair_less_def by auto

lemma P_induct[consumes 1, case_names Induct]:
  assumes "p ∈ P k u"
  assumes induct: "∧ p k u . (∧ p' k' u'. p' ∈ P k' u' ==> indexlt k' u' k u ==> P p' k' u')
                     ==> p ∈ P k u ==> P p k u"
  shows "P p 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 ∈ P (fst (fst a)) (snd (fst a)) ⟶ P (snd a) (fst (fst a)) (snd (fst a))"
  have "p ∈ P k u ⟶ P p k u"
    apply (rule wf_induct[OF wf_R, where P = ?P and a = "((k, u), p)", simplified])
    apply (auto simp add: indexlt_def[symmetric])
    apply (rule_tac p=ba and k=a and u=b in induct)
    by auto
  thus ?thesis using assms by auto 
qed

lemma nonempty_path_indices: 
  assumes p: "p ∈ P k u"
  assumes nonempty: "p ≠ []"
  shows "k > 0 ∨ u > 0"
proof (cases "u = 0")
  case True
  note u = True
  have "k > 0"
  proof (cases "k = 0")
    case True
    with p u have "p = []" by simp
    with nonempty have "False" by auto
    then show ?thesis by auto
  next
    case False
    then show ?thesis by arith
  qed
  then show ?thesis by blast
next
  case False
  then show ?thesis by arith
qed

lemma base_paths:
  assumes p: "p ∈ P k 0"
  assumes k: "k > 0"
  shows "∃ u. p ∈ P (k - 1) u"
proof -
  from k have "∃ i. k = Suc i" by arith
  then obtain i where i: "k = Suc i" by blast
  from p show ?thesis
    by (auto simp add: i natUnion_def)
qed

lemma indexlt_trans: "indexlt k'' u'' k' u' ==> indexlt k' u' k u ==> indexlt k'' u'' k u"
using dual_order.strict_trans indexlt_simp by auto

definition is_continuation :: "nat ==> nat ==> tokens ==> tokens ==> bool" where
  "is_continuation k u q ts = (q ∈ P k u ∧ charslength q = k ∧ admissible (q@ts) ∧
     (∀ t ∈ set ts. t ∈ Z k (Suc u)) ∧ (∀ t ∈ set (butlast ts). chars_of_token t = []))"

lemma limit_Append_path_nonelem_split: "p ∈ limit (Append T k) (P k u) ==> p ∉ P k u ==>
  ∃ q ts. p = q@ts ∧ q ∈ P k u ∧ charslength q = k ∧ admissible (q@ts) ∧ (∀ t ∈ set ts. t ∈ T) ∧
    (∀ t ∈ set (butlast ts). chars_of_token t = [])"
proof (induct rule: limit_induct)
  case (Init p) thus ?case by auto
next
  case (Iterate p Y)
  show ?case
  proof (cases "p ∈ Y")
    case True
    from Iterate(1)[OF True Iterate(3)] show ?thesis by blast
  next
    case False
    with Append_def Iterate(2) 
    have "∃ q t. p = q@[t] ∧ q ∈ by_length k Y ∧ t ∈ T ∧ admissible (q @ [t])" by auto
    then obtain q t where qt: "p = q@[t] ∧ q ∈ by_length k Y ∧ t ∈ T ∧ admissible (q @ [t])" 
      by blast
    from qt have qlen: "charslength q = k" by auto
    have "q ∈ P k u ∨ q ∉ P k u" by blast
    then show ?thesis
    proof(induct rule: disjCases2)
      case 1
      show ?case
        apply (rule_tac x=q in exI)
        apply (rule_tac x="[t]" in exI)
        using qlen by (simp add: qt 1)
    next
      case 2
      have q_in_Y: "q ∈ Y" using qt by auto
      from Iterate(1)[OF q_in_Y 2] 
      obtain q' ts where 
        q'ts: "q = q' @ ts ∧ q' ∈ P k u ∧ charslength q' = k ∧ (∀t∈set ts. t ∈ T) ∧
               (∀t∈set(butlast ts). chars_of_token t = [])"
        by blast
      with qlen have "charslength ts = 0" by auto
      hence empty: "∀ t ∈ set(ts). chars_of_token t = []" 
        apply (induct ts)
        by auto
      show ?case
        apply (rule_tac x=q' in exI)
        apply (rule_tac x="ts@[t]" in exI)
        using qt q'ts empty by auto
    qed
  qed
qed

lemma limit_Append_path_nonelem_split': 
  "p ∈ limit (Append (Z k (Suc u)) k) (P k u) ==> p ∉ P k u ==>
   ∃ q ts. p = q@ts ∧ is_continuation k u q ts"
apply (simp only: is_continuation_def)
apply (rule_tac limit_Append_path_nonelem_split)
by auto

lemma final_step_of_path: "p ∈ P k u ==> p ≠ [] ==> (∃ q ts k' u'. p = q@ts ∧ indexlt k' u' k u
  ∧ is_continuation k' u' q ts)"
proof (induct rule: P_induct)
  case (Induct p k u)
  from Induct(2) Induct(3) have ku_0: "k > 0 ∨ u > 0"
    using nonempty_path_indices by blast
  show ?case  
  proof (cases "u = 0")
    case True
    with ku_0 have k_0: "k > 0" by arith
    with True Induct(2) base_paths have "∃ u'. p ∈ P (k - 1) u'" by auto
    then obtain u' where u': "p ∈ P (k - 1) u'" by blast
    have indexlt: "indexlt (k - 1) u' k u" by (simp add: indexlt_simp k_0)
    from Induct(1)[OF u' indexlt Induct(3)] show ?thesis
      using indexlt indexlt_trans by blast
  next
    case False 
    then have "∃ u'. u = Suc u'" by arith
    then obtain u' where u': "u = Suc u'" by blast
    with Induct(2) have p_limit: "p ∈ limit (Append (Z k (Suc u')) k) (P k u')"
      using P.simps(2) by blast
    from u' have indexlt: "indexlt k u' k u" by (simp add: indexlt_simp)
    have "p ∈ P k u' ∨ p ∉ P k u'" by blast
    then show ?thesis
    proof (induct rule: disjCases2)
      case 1
      from Induct(1)[OF 1 indexlt Induct(3)] show ?case
        using indexlt indexlt_trans by blast
    next
      case 2
      from limit_Append_path_nonelem_split'[OF p_limit 2]
      show ?case using indexlt u' by auto
    qed
  qed
qed      

lemma terminals_empty[simp]: "terminals [] = []"
  by (auto simp add: terminals_def)

lemma empty_in_L_P[simp]: "[] ∈ L_P"
  apply (simp add: L_{P_def} is_derivation_def)
  apply (rule_tac x="[S]" in exI)
  by simp 
     
lemma admissible_empty[simp]: "admissible []"
  by (auto simp add: admissible_def)

lemma P_are_admissible: "p ∈ P ==> admissible p"
proof (induct rule: P_induct)
  case Base thus ?case by simp
next
  case (Induct p k u)
  from Induct(2)[simplified] show ?case
  proof (induct rule: limit_induct)
    case (Init p) from Induct(1)[OF Init] show ?case .
  next
    case (Iterate p Y) 
    have "Y (Z k u) (P k u) k ⊆ X k" by (metis Z.simps(2) Z_subset_X)
    then have 1: "Append (Y (Z k u) (P k u) k) k Y ⊆ Append (X k) k Y"
      by (rule Append_mono, simp) 
    have 2: "p ∈ Append (X k) k Y ==> admissible p"
      apply (auto simp add: Append_def)
      by (simp add: Iterate)
    show ?case 
      apply (rule 2)
      using "1" Iterate(2) by blast
  qed  
qed

lemma prefix_of_empty_is_empty: "is_prefix q [] ==> q = []"
by (metis  is_prefix_cons neq_Nil_conv)

lemma subset_P :
  assumes leq: "k' < k ∨ (k' = k ∧ u' ≤ u)"
  shows "P k' u' ⊆ P k u"
proof -
  from leq show ?thesis
  proof (induct rule: disjCases2)
    case 1
    have s1: "P k' u' ⊆ Q k'" by (rule_tac subset_PQk) 
    have s2: "Q k' ⊆ Q (k - 1)" 
      apply (rule_tac subset_Q)
      using 1 by arith
    from subset_QPSuc[where k="k - 1"] 1 have s3: "Q (k - 1) ⊆ P k 0"
      by simp
    have s4: "P k 0 ⊆ P k u" by (rule_tac subset_Pk, simp)
    from s1 s2 s3 s4 subset_trans show ?case by blast
  next
    case 2 thus ?case by (simp add : subset_Pk)
  qed
qed  

lemma empty_path_is_elem[simp]: "[] ∈ P k u"
proof -
  have "[] ∈ P 0 0" by simp
  then show "[] ∈ P k u" by (metis le0 not_gr0 subsetCE subset_P) 
qed

lemma is_prefix_of_append:
  assumes "is_prefix p (a@b)"
  shows "is_prefix p a ∨ (∃ b'. b' ≠ [] ∧ is_prefix b' b ∧ p = a@b')"
apply (auto simp add: is_prefix_def) 
by (metis append_Nil2 append_eq_append_conv2 assms is_prefix_cancel is_prefix_def)

lemma prefix_is_continuation: "is_continuation k u p ts ==> is_prefix ts' ts ==>
  is_continuation k u p ts'"
apply (auto simp add: is_continuation_def is_prefix_def)
apply (metis L_{P_split} admissible_def append_assoc terminals_append)
using in_set_butlast_appendI by fastforce 

lemma charslength_0: "(∀ t ∈ set ts. chars_of_token t = []) = (charslength ts = 0)"
by (induct ts, auto)
    
lemma is_continuation_in_P: "is_continuation k u p ts ==> p@ts ∈ P k (Suc u)"
proof(induct ts rule: rev_induct)
  case Nil thus ?case 
    apply (auto simp add: is_continuation_def)
    using subset_PSuc by fastforce
next
  case (snoc t ts)
  from snoc(2) have "is_continuation k u p ts"
    by (metis append_Nil2 is_prefix_cancel is_prefix_empty prefix_is_continuation)
  note induct = snoc(1)[OF this]
  then have pts: "p@ts ∈ limit (Append (Z k (Suc u)) k) (P k u)" by simp
  note is_cont = snoc(2)
  then have admissible: "admissible (p@ts@[t])" by (simp add: is_continuation_def)
  from is_cont have t: "t ∈ Z k (Suc u)" by (simp add: is_continuation_def)
  from is_cont have "∀ t ∈ set ts. chars_of_token t = []" by (simp add: is_continuation_def)
  then have charslength_ts: "charslength ts = 0" by (simp only: charslength_0)
  from is_cont have plen: "charslength p = k" by (simp add: is_continuation_def)
  show ?case
    apply (simp only: P.simps)
    apply (rule_tac limit_step_pointwise[OF pts])
    apply (simp add: pointwise_Append)
    apply (auto simp add: Append_def)
    apply (rule_tac x="fst t" in exI)
    apply (rule_tac x="snd t" in exI)
    apply (auto simp add: admissible)
    using charslength_ts apply simp
    using plen apply simp
    using t by simp
qed    

lemma indexlt_subset_P: "indexlt k' u' k u ==> P k' (Suc u') ⊆ P k u"
apply (rule_tac subset_P)
apply (simp add: indexlt_simp)
apply arith
done

lemma prefixes_are_paths: "p ∈ P k u ==> is_prefix x p ==> x ∈ P k u"
proof (induct arbitrary: x rule: P_induct)
  case (Induct p k u)
  show ?case
  proof (cases "p = []")
    case True
    then have "x = []"
      using Induct.prems prefix_of_empty_is_empty by blast 
    then show "x ∈ P k u" by simp
  next
    case False
    from final_step_of_path[OF Induct(2) False]
    obtain q ts k' u' where step: "p = q@ts ∧ indexlt k' u' k u ∧ is_continuation k' u' q ts"
      by blast
    have subset: "P k' u' ⊆ P k u"
      by (metis indexlt_simp less_or_eq_imp_le step subset_P)
    have "is_prefix x q ∨ (∃ ts'. ts' ≠ [] ∧ is_prefix ts' ts ∧ x = q@ts')"
      apply (rule_tac is_prefix_of_append)
      using Induct(3) step by auto
    then show ?thesis
    proof (induct rule: disjCases2)
      case 1
        have x: "x ∈ P k' u'"
        using 1 Induct step by (auto simp add: is_continuation_def)
        then show "x ∈ P k u" using subset subsetCE by blast
    next
      case 2
      then obtain ts' where ts': "is_prefix ts' ts ∧ x = q@ts'" by blast
      have "is_continuation k' u' q ts'" using step prefix_is_continuation ts' by blast 
      with ts' have "x ∈ P k' (Suc u')"
        apply (simp only: ts')
        apply (rule_tac is_continuation_in_P)
        by simp
      with subset show "x ∈ P k u" using indexlt_subset_P step by blast
    qed
  qed
qed  

lemma empty_or_last_of_suffix:
  assumes "q = q' @ [t]"
  assumes "q = p @ ts"
  shows "ts = [] ∨ (∃ ts'. q' = p @ ts' ∧ ts'@[t] = ts)"
by (metis assms(1) assms(2) butlast_append last_appendR snoc_eq_iff_butlast)

lemma is_prefix_butlast: "is_prefix q (butlast p) ==> is_prefix q p"
by (metis butlast_conv_take is_prefix_append is_prefix_def is_prefix_take)
        
lemma last_step_of_path:
  "q ∈ P k u ==> q = q'@[t] ==>
   ∃ k' u'. indexlt k' u' k u ∧ q ∈ P k' (Suc u') ∧ charslength q' = k' ∧ t ∈ Z k' (Suc u')"
proof (induct arbitrary: q' t rule: P_induct)
  case (Induct q k u)
    have "∃ p ts k' u'. q = p@ts ∧ indexlt k' u' k u ∧ is_continuation k' u' p ts"
      apply (rule_tac final_step_of_path)
      apply (simp add: Induct(2))
      apply (simp add: Induct(3))
      done
    then obtain p ts k' u' where pts: "q = p@ts ∧ indexlt k' u' k u ∧ is_continuation k' u' p ts"
      by blast
    then have indexlt: "indexlt k' u' k u" by auto
    from pts have "ts = [] ∨ (∃ ts'. q' = p @ ts' ∧ ts'@[t] = ts)"
      by (metis empty_or_last_of_suffix Induct(3))
    then show ?case
    proof (induct rule: disjCases2)
      case 1
        with pts have q: "q ∈ P k' u'" by (auto simp add: is_continuation_def)
        from Induct(1)[OF this indexlt Induct(3)] show ?case
          using indexlt indexlt_trans by blast
    next
      case 2
        then obtain ts' where ts': "q' = p @ ts' ∧ ts'@[t] = ts" by blast
        then have "is_prefix ts' ts" using is_prefix_def by blast 
        then have "is_continuation k' u' p ts'" by (metis prefix_is_continuation pts)
        have "charslength ts' = 0" using charslength_0 is_continuation_def pts ts' by auto 
        then have q'len: "charslength q' = k'" using is_continuation_def pts ts' by auto 
        have "t ∈ set ts" using ts' by auto
        with pts have t_in_Z: "t ∈ Z k' (Suc u')" using is_continuation_def by blast 
        have q_dom: "q ∈ P k' (Suc u')" using pts is_continuation_in_P by blast
        show ?case  
          apply (rule_tac x=k' in exI)
          apply (rule_tac x=u' in exI)
          by (simp only: indexlt q'len t_in_Z q_dom)
    qed
qed
      
lemma charslength_of_butlast_0: "p ∈ P k 0 ==> p = q@[t] ==> charslength q < k"
using last_step_of_path LocalLexing_axioms indexlt_simp by blast

lemma charslength_of_butlast: "p ∈ P k u ==> p = q@[t] ==> charslength q ≤ k"
by (metis indexlt_simp last_step_of_path eq_imp_le less_imp_le_nat)

lemma last_token_of_path:
  assumes "q ∈ P k u"
  assumes "q = q'@[t]"
  assumes "charslength q' = k"
  shows "t ∈ Z k u"
proof -
  from assms have "∃ k' u'. indexlt k' u' k u ∧ q ∈ P k' (Suc u') ∧ charslength q' = k' ∧
    t ∈ Z k' (Suc u')" using last_step_of_path by blast
  then obtain k' u' where th: "indexlt k' u' k u ∧ q ∈ P k' (Suc u') ∧ charslength q' = k' ∧
    t ∈ Z k' (Suc u')" by blast
  with assms(3) have k': "k' = k" by blast
  with th have "t ∈ Z k' (Suc u') ∧ u' < u" using indexlt_simp by auto
  then show ?thesis
    by (metis (no_types, opaque_lifting) Z_subset_Suc k' linorder_neqE_nat not_less_eq 
      subsetCE subset_fSuc_strict)
qed

lemma final_step_of_path': "p ∈ P k u ==> p ∉ P k (u - 1) ==>
  ∃ q ts. u > 0 ∧ p = q@ts ∧ is_continuation k (u - 1) q ts"
by (metis Suc_diff_1 P.simps(2) diff_0_eq_0 limit_Append_path_nonelem_split' not_gr0)

lemma is_continuation_continue:
  assumes "is_continuation k u q ts"
  assumes "charslength ts = 0"
  assumes "t ∈ Z k (Suc u)"
  assumes "admissible (q @ ts @ [t])"
  shows "is_continuation k u q (ts@[t])"
proof -
  from assms show ?thesis
    by (simp add: is_continuation_def charslength_0)
qed

(* In an older version of local lexing, compatibility was an assumption we had to make, 
   but now it is a theorem *)

theorem compatibility_def:
  assumes p_in_dom: "p ∈ P k u"
  assumes q_in_dom: "q ∈ P k u"
  assumes p_charslength: "charslength p = k"
  assumes q_split: "q = q'@[t]"
  assumes q'len: "charslength q' = k"
  assumes admissible: "admissible (p @ [t])" 
  shows "p @ [t] ∈ P k u"
proof - 
  have u: "u > 0"
  proof (cases "u = 0")
    case True
      then have "charslength q' < k" 
        using charslength_of_butlast_0 q_in_dom q_split by blast       
      with q'len have "False" by arith
      then show ?thesis by blast
  next
    case False
      then show ?thesis by arith
  qed
  have t_dom: "t ∈ Z k u" using last_token_of_path q'len q_in_dom q_split by blast  
  have "p ∈ P k (u - 1) ∨ p ∉ P k (u - 1)" by blast
  then show ?thesis
  proof (induct rule: disjCases2)
    case 1
      with t_dom p_charslength admissible u have "is_continuation k (u - 1) p [t]"
        by (auto simp add: is_continuation_def)
      with u show "p@[t] ∈ P k u"
        by (metis One_nat_def Suc_pred is_continuation_in_P)
  next
    case 2
      from final_step_of_path'[OF p_in_dom 2] 
      obtain p' ts where p': "p = p' @ ts ∧ is_continuation k (u - 1) p' ts"
        by blast
      from p' p_charslength is_continuation_def have charslength_ts: "charslength ts = 0"
        by auto
      from u have u': "Suc (u - 1) = u" by arith
      have "is_continuation k (u - 1) p' (ts@[t])"
        apply (rule_tac is_continuation_continue)
        using p' apply blast
        using charslength_ts apply blast
        apply (simp only: u' t_dom)
        using admissible p' apply auto
        done
      from is_continuation_in_P[OF this] show ?case by (simp only: p' u', simp)
  qed
qed    

lemma is_prefix_admissible:
  assumes "is_prefix a b"
  assumes "admissible b"
  shows "admissible a"
proof -
  from assms show ?thesis
    by (auto simp add: is_prefix_def admissible_def L_{P_def})
qed  

lemma butlast_split: "n < length q ==> butlast q = (take n q)@(drop n (butlast q))"
by (metis append_take_drop_id take_butlast)

lemma in_P_charslength:
  assumes p_dom: "p ∈ P k u"
  shows "∃ v. p ∈ P (charslength p) v"
proof (cases "charslength p ≥ k")
  case True
    show ?thesis
      apply (rule_tac x=u in exI)
      by (metis True le_neq_implies_less p_dom subsetCE subset_P)
next
  case False
    then have charslength: "charslength p < k" by arith
    have "p = [] ∨ p ≠ []" by blast
    thus ?thesis
    proof (induct rule: disjCases2)
      case 1 thus ?case by simp
    next
      case 2
        from final_step_of_path[OF p_dom 2] obtain q ts k' u' where
          step: "p = q @ ts ∧ indexlt k' u' k u ∧ is_continuation k' u' q ts" by blast
        from step have k': "charslength q = k'" using is_continuation_def by blast  
        from step have "charslength q ≤ charslength p"  by simp       
        with k' have k': "k' ≤ charslength p" by simp
        from step have "p ∈ P k' (Suc u')" using is_continuation_in_P by blast 
        with k' have "p ∈ P (charslength p) (Suc u')"
          by (metis le_neq_implies_less subsetCE subset_P) 
        then show ?case by blast
    qed
qed

theorem general_compatibility:
  "p ∈ P k u ==> q ∈ P k u ==> charslength p = charslength (take n q)
    ==> charslength p ≤ k ==> admissible (p @ (drop n q)) ==> p @ (drop n q) ∈ P k u"
proof (induct "length q - n" arbitrary: p q n k u)
  case 0
    from 0 have "0 = length q - n" by auto
    then have n: "n ≥ length q" by arith
    then have "drop n q = []" by auto
    then show ?case by (simp add: "0.prems"(1)) 
next
  case (Suc l)
    have "n ≥ length q ∨ n < length q" by arith
    then show ?case
    proof (induct rule: disjCases2)
      case 1
        then have "drop n q = []" by auto
        then show ?case by (simp add: Suc.prems(1))
    next
      case 2
        then have "length q > 0" by auto
        then have q_nonempty: "q ≠ []" by auto
        let ?q' = "butlast q"
        from q_nonempty Suc(2) have h1: "l = length ?q' - n" by auto
        have h2: "?q' ∈ P k u"
          by (metis Suc.prems(2) butlast_conv_take is_prefix_take prefixes_are_paths)
        have h3: "charslength p = charslength (take n ?q')"
          using "2.hyps" Suc.prems(3) take_butlast by force
        have "is_prefix (p @ drop n ?q') (p @ drop n q)"
          by (simp add: butlast_conv_take drop_take)
        note h4 = is_prefix_admissible[OF this Suc.prems(5)] 
        note induct = Suc(1)[OF h1 Suc(3) h2 h3 Suc.prems(4) h4] 
        let ?p' = "p @ (drop n (butlast q))"
        from induct have "?p' ∈ P k u" .
        let ?i = "charslength ?p'"
        have charslength_i[symmetric]: "charslength ?q' = ?i"
          using Suc.prems(3) apply simp
          apply (subst butlast_split[OF 2])
          by simp
        have q_split: "q = ?q'@[last q]" by (simp add: q_nonempty)
        with Suc.prems(2) charslength_of_butlast have charslength_q': "charslength ?q' ≤ k" 
          by blast 
        from q_nonempty have p'last: "?p'@[last q] = p@(drop n q)"
          by (metis "2.hyps" append_assoc drop_eq_Nil drop_keep_last not_le q_split)
        have "?i ≤ k" by (simp only: charslength_i charslength_q')
        then have "?i = k ∨ ?i < k" by auto
        then show ?case
        proof (induct rule: disjCases2)
          case 1
            have charslength_q': "charslength ?q' = k" using charslength_i[symmetric] 1 by blast
            from compatibility_def[OF induct Suc.prems(2) 1 q_split charslength_q']
            show ?case by (simp only: p'last Suc.prems(5))
        next
          case 2
            from in_P_charslength[OF induct]
            obtain v1 where v1: "?p' ∈ P ?i v1" by blast 
            from last_step_of_path[OF Suc.prems(2) q_split] 
            have "∃ u. q ∈ P ?i u" by (metis charslength_i)
            then obtain v2 where v2: "q ∈ P ?i v2" by blast
            let ?v = "max v1 v2"
            have "v1 ≤ ?v" by auto
            with v1 have dom1: "?p' ∈ P ?i ?v" by (metis (no_types, opaque_lifting) subsetCE subset_Pk) 
            have "v2 ≤ ?v" by auto
            with v2 have dom2: "q ∈ P ?i ?v" by (metis (no_types, opaque_lifting) subsetCE subset_Pk) 
            from compatibility_def[OF dom1 dom2 _ q_split] 
            have "p @ drop n q ∈ P ?i ?v"
              by (simp only: p'last charslength_i[symmetric] Suc.prems(5))
            then show "p @ drop n q ∈ P k u" by (meson "2.hyps" subsetCE subset_P) 
        qed                                                          
    qed        
qed

lemma wellformed_item_derives:
  assumes wellformed: "wellformed_item x"
  shows "derives [item_nonterminal x] (item_rhs x)"
proof -
  from wellformed have "(item_nonterminal x, item_rhs x) ∈ R"
    by (simp add: item_nonterminal_def item_rhs_def wellformed_item_def)
  then show ?thesis
    by (metis append_Nil2 derives1_def derives1_implies_derives is_sentence_concat 
        rule_α_type self_append_conv2)
qed      

lemma wellformed_complete_item_β:
  assumes wellformed: "wellformed_item x"
  assumes complete: "is_complete x" 
  shows "item_β x = []"
using complete is_complete_def item_β_def by auto

lemma wellformed_complete_item_derives:
  assumes wellformed: "wellformed_item x"
  assumes complete: "is_complete x" 
  shows "derives [item_nonterminal x] (item_α x)"
using complete is_complete_def item_α_def wellformed wellformed_item_derives by auto 

lemma is_derivation_implies_admissible:
  "is_derivation (terminals p @ δ) ==> is_word (terminals p) ==> admissible p"
using L_{P_def} admissible_def by blast

lemma item_rhs_of_inc_item[simp]: "item_rhs (inc_item x k) = item_rhs x"
  by (auto simp add: inc_item_def item_rhs_def)

lemma item_rule_of_inc_item[simp]: "item_rule (inc_item x k) = item_rule x"
  by (simp add: inc_item_def)

lemma item_origin_of_inc_item[simp]: "item_origin (inc_item x k) = item_origin x"
  by (simp add: inc_item_def)

lemma item_end_of_inc_item[simp]: "item_end (inc_item x k) = k"
  by (simp add: inc_item_def)

lemma item_dot_of_inc_item[simp]: "item_dot (inc_item x k) = (item_dot x) + 1"
  by (simp add: inc_item_def)

lemma item_nonterminal_of_inc_item[simp]: "item_nonterminal (inc_item x k) = item_nonterminal x"
  by (simp add: inc_item_def item_nonterminal_def)

lemma wellformed_inc_item:
  assumes wellformed: "wellformed_item x"
  assumes next_symbol: "next_symbol x = Some s"
  assumes k_upper_bound: "k ≤ length Doc"
  assumes k_lower_bound: "k ≥ item_end x"
  shows "wellformed_item (inc_item x k)"
proof -
  have k_lower_bound': "k ≥ item_origin x"
    using k_lower_bound wellformed wellformed_item_def by auto  
  show ?thesis
    apply (auto simp add: wellformed_item_def k_upper_bound k_lower_bound')
    using wellformed wellformed_item_def apply blast
    using is_complete_def next_symbol next_symbol_not_complete not_less_eq_eq by blast
qed    

lemma item_α_of_inc_item:
  assumes wellformed: "wellformed_item x"
  assumes next_symbol: "next_symbol x = Some s"
  shows "item_α (inc_item x k) = item_α x @ [s]"
by (metis (mono_tags, lifting) item_dot_of_inc_item item_rhs_of_inc_item 
  One_nat_def add.right_neutral add_Suc_right is_complete_def item_α_def item_β_def 
  le_neq_implies_less list.sel(1) next_symbol next_symbol_not_complete next_symbol_starts_item_β 
  take_hd_drop wellformed wellformed_item_def)

lemma derives1_pad: 
  assumes derives1: "derives1 α β"
  assumes u: "is_sentence u"
  assumes v: "is_sentence v"
  shows "derives1 (u@α@v) (u@β@v)"
proof -
  from derives1 have 
   "∃x y N δ. α = x @ [N] @ y ∧ β = x @ δ @ y ∧ is_sentence x ∧ is_sentence y ∧ (N, δ) ∈ R"
   by (auto simp add: derives1_def)
  then obtain x y N δ where 
   1: "α = x @ [N] @ y ∧ β = x @ δ @ y ∧ is_sentence x ∧ is_sentence y ∧ (N, δ) ∈ R" by blast
  show ?thesis
    apply (simp only: derives1_def)
    apply (rule_tac x="u@x" in exI)
    apply (rule_tac x="y@v" in exI)
    apply (rule_tac x=N in exI)
    apply (rule_tac x=δ in exI)
    using 1 u v is_sentence_concat by auto
qed

lemma derives_pad:
  "derives α β ==> is_sentence u ==> is_sentence v ==> derives (u@α@v) (u@β@v)"
proof (induct rule: derives_induct)
  case Base thus ?case by simp
next
  case (Step y z) 
    from Step have 1: "derives (u@α@v) (u@y@v)" by auto
    from Step have 2: "derives1 y z" by auto
    then have "derives1 (u@y@v) (u@z@v)" by (simp add: Step.prems derives1_pad)    
    then show ?case
      using "1" derives1_implies_derives derives_trans by blast
qed  

lemma derives1_is_sentence: "derives1 α β ==> is_sentence α ∧ is_sentence β"
using Derives1_sentence1 Derives1_sentence2 derives1_implies_Derives1 by blast

lemma derives_is_sentence: "derives α β ==> (α = β) ∨ (is_sentence α ∧ is_sentence β)"
proof (induct rule: derives_induct)
  case Base thus ?case by simp
next
  case (Step y z) 
    show ?case using Step.hyps(2) Step.hyps(3) derives1_is_sentence by blast
qed

lemma derives_append: 
  assumes au: "derives a u"
  assumes bv: "derives b v"
  assumes is_sentence_a: "is_sentence a"
  assumes is_sentence_b: "is_sentence b"
  shows "derives (a@b) (u@v)"
proof -
  from au have "a = u ∨ (is_sentence a ∧ is_sentence u)"
    using derives_is_sentence by blast
  then have au_sentences: "is_sentence a ∧ is_sentence u" using is_sentence_a by blast 
  from bv have "b = v ∨ (is_sentence b ∧ is_sentence v)"
    using derives_is_sentence by blast
  then have bv_sentences: "is_sentence b ∧ is_sentence v" using is_sentence_b by blast 
  have 1: "derives (a@b) (u@b)"
    apply (rule_tac derives_pad[OF au, where u="[]", simplified])
    using is_sentence_b by auto
  have 2: "derives (u@b) (u@v)"
    apply (rule_tac derives_pad[OF bv, where v="[]", simplified])
    apply (simp add: au_sentences)
    done
  from 1 2 derives_trans show ?thesis by blast
qed  

lemma is_sentence_item_α: "wellformed_item x ==> is_sentence (item_α x)"
  by (metis is_sentence_take item_α_def item_rhs_def prod.collapse rule_α_type wellformed_item_def)

lemma is_nonterminal_item_nonterminal:  "wellformed_item x ==> is_nonterminal (item_nonterminal x)"
  by (metis item_nonterminal_def prod.collapse rule_nonterminal_type wellformed_item_def)
  
lemma Complete_elem_in_Gen:
  assumes I_in_Gen: "I ⊆ Gen (P k u)"
  assumes k: "k ≤ length Doc"
  assumes x_in_Complete: "x ∈ Complete k I"
  shows "x ∈ Gen (P k u)"
proof -
  let ?P = "P k u"
  from x_in_Complete have "x ∈ I ∨ (∃ x1 x2. x = inc_item x1 k ∧
     x1 ∈ bin I (item_origin x2) ∧ x2 ∈ bin I k ∧ is_complete x2 ∧
     next_symbol x1 = Some (item_nonterminal x2))"
     by (auto simp add: Complete_def)
  then show ?thesis
  proof (induct rule: disjCases2)
    case 1 thus ?case using I_in_Gen subsetCE by blast 
  next
    case 2 
    then obtain x1 x2 where x12: "x = inc_item x1 k ∧
      x1 ∈ bin I (item_origin x2) ∧ x2 ∈ bin I k ∧ is_complete x2 ∧
      next_symbol x1 = Some (item_nonterminal x2)" by blast
    from x12 have "∃ p1 p2. p1 ∈ ?P ∧ pvalid p1 x1 ∧ p2 ∈ ?P ∧ pvalid p2 x2"
      by (meson Gen_implies_pvalid I_in_Gen bin_elem subsetCE)
    then obtain p1 p2 where p1: "p1 ∈ ?P ∧ pvalid p1 x1" and p2: "p2 ∈ ?P ∧ pvalid p2 x2"
      by blast
    from p1 obtain w δ where p1valid:
      "wellformed_tokens p1 ∧
       wellformed_item x1 ∧
       w ≤ length p1 ∧
       charslength p1 = item_end x1 ∧
       charslength (take w p1) = item_origin x1 ∧
       is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ δ) ∧
       derives (item_α x1) (terminals (drop w p1))"
       using pvalid_def by blast
    from p2 obtain y γ where p2valid:
      "wellformed_tokens p2 ∧
       wellformed_item x2 ∧
       y ≤ length p2 ∧
       charslength p2 = item_end x2 ∧
       charslength (take y p2) = item_origin x2 ∧
       is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ γ) ∧
       derives (item_α x2) (terminals (drop y p2))"
       using pvalid_def by blast
    let ?r = "p1 @ (drop y p2)"
    have charslength_p1_eq: "charslength p1 = item_end x1" by (simp only: p1valid)
    from x12 have item_end_x1: "item_end x1 = item_origin x2" 
      using bin_def mem_Collect_eq by blast
    have item_end_x2: "item_end x2 = k" using bin_def x12 by blast 
    then have charslength_p1_leq: "charslength p1 ≤ k"
      using charslength_p1_eq item_end_x1 p2valid wellformed_item_def by auto 
    have "∃δ'. item_β x1 = [item_nonterminal x2] @ δ'"
      by (simp add: next_symbol_starts_item_β p1valid x12)  
    then obtain δ' where δ': "item_β x1 = [item_nonterminal x2] @ δ'" by blast
    have "is_derivation ((terminals (take w p1))@(item_rhs x1)@δ)"
      using is_derivation_derives p1valid wellformed_item_derives by blast
    then have "is_derivation ((terminals (take w p1))@(item_α x1 @ item_β x1)@δ)"
       by (simp add: item_rhs_split)
    then have "is_derivation ((terminals (take w p1))@((terminals (drop w p1)) @ item_β x1)@δ)"
      using is_derivation_derives p1valid by auto
    then have "is_derivation ((terminals p1)@(item_β x1)@δ)"
      by (metis append_assoc append_take_drop_id terminals_append)
    then have "is_derivation ((terminals p1)@([item_nonterminal x2] @ δ')@δ)"
      using is_derivation_derives δ' by auto
    then have "is_derivation ((terminals p1)@(terminals (drop y p2)) @ δ' @δ)"
      using is_complete_def is_derivation_derives is_derivation_step item_α_def 
        item_nonterminal_def item_rhs_def p2valid wellformed_item_def x12 by auto
    then have "is_derivation (terminals (p1 @ (drop y p2)) @ (δ' @ δ))" by simp
    then have admissible_r: "admissible (p1 @ (drop y p2))"
      apply (rule_tac is_derivation_implies_admissible)
      apply auto
      apply (rule is_word_terminals)
      apply (simp add: p1valid)
      using p2valid using is_word_terminals_drop terminals_drop by auto 
    have r_in_dom: "?r ∈ P k u"
      apply (rule_tac general_compatibility)
      apply (simp add: p1)
      apply (simp add: p2)
      apply (simp only: p2valid charslength_p1_eq item_end_x1)
      apply (simp only: charslength_p1_leq)
      by (simp add: admissible_r)
    have wellformed_r: "wellformed_tokens ?r" 
      using admissible_r admissible_wellformed_tokens by blast 
    have wellformed_x: "wellformed_item x"
      apply (simp add: x12)
      apply (rule_tac wellformed_inc_item)
      apply (simp add: p1valid)
      apply (simp add: x12)
      apply (simp add: k)
      using charslength_p1_eq charslength_p1_leq by auto
    have charslength_p1_as_p2: "charslength p1 = charslength (take y p2)"
      using charslength_p1_eq item_end_x1 p2valid by linarith     
    then have charslength_r: "charslength ?r = item_end x"
      apply (simp add: x12)
      apply (subst length_append[symmetric])
      apply (subst chars_append[symmetric])
      apply (subst append_take_drop_id)
      using item_end_x2 p2valid by auto
    have item_α_x: "item_α x = item_α x1 @ [item_nonterminal x2]"
      using x12 p1valid by (simp add: item_α_of_inc_item)
    from p2valid have derives_item_nonterminal_x2:
      "derives [item_nonterminal x2] (terminals (drop y p2))"
      using derives_trans wellformed_complete_item_derives x12 by blast
    have "pvalid ?r x"
      apply (auto simp only: pvalid_def)
      apply (rule_tac x=w in exI)
      apply (rule_tac x=δ in exI)
      apply (auto simp only:)
      apply (simp add: wellformed_r)
      apply (simp add: wellformed_x)
      using p1valid apply simp
      apply (simp only: charslength_r)
      using x12 p1valid apply simp
      using x12 p1valid apply simp
      apply (simp add:  item_α_x)
      apply (rule_tac derives_append)
      using p1valid apply simp
      using derives_item_nonterminal_x2 p1valid apply auto[1]
      using is_sentence_item_α p1valid apply blast
      using is_derivation_is_sentence is_sentence_concat p2valid by blast
    with r_in_dom show ?case using Gen_def mem_Collect_eq by blast
  qed
qed

lemma Complete_subset_Gen:
  assumes I_in_Gen_P: "I ⊆ Gen (P k u)"
  assumes k: "k ≤ length Doc"
  shows "Complete k I ⊆ Gen (P k u)"
using Complete_elem_in_Gen I_in_Gen_P k by blast

lemma P_are_admissible: "p ∈ P k u ==> admissible p"
apply (rule_tac P_are_admissible)
using P_covers_P subsetCE by blast

lemma is_continuation_base:
  assumes p_dom: "p ∈ P k u"
  assumes charslength_p: "charslength p = k"
  shows "is_continuation k u p []"
apply (auto simp add: is_continuation_def)
apply (simp add: p_dom)
using charslength_p apply simp
using P_are_admissible p_dom by blast

lemma is_continuation_empty_chars: 
  "is_continuation k u q ts ==> charslength (q@ts) = k ==> chars ts = []"
by (simp add: is_continuation_def)

lemma Z_subset: "u ≤ v ==> Z k u ⊆ Z k v"
using Z_subset_Suc subset_fSuc by blast

lemma is_continuation_increase_u:
  assumes cont: "is_continuation k u q ts"
  assumes uv: "u ≤ v"
  shows "is_continuation k v q ts"
proof -
  have "q ∈ P k u" using cont is_continuation_def by blast
  with uv have q_dom: "q ∈ P k v" by (meson subsetCE subset_Pk) 
  from uv have Z: "∧ t. t ∈ Z k (Suc u) ==> t ∈ Z k (Suc v)"
    using Z_subset le_neq_implies_less less_imp_le_nat not_less_eq subsetCE by blast  
  show ?thesis
    apply (auto simp only: is_continuation_def)
    apply (simp add: q_dom)
    using cont is_continuation_def apply simp
    using cont is_continuation_def apply simp
    using cont is_continuation_def Z apply simp
    using cont is_continuation_def apply (simp only:)
    done
qed

lemma pvalid_next_symbol_derivable:
  assumes pvalid: "pvalid p x" 
  assumes next_symbol: "next_symbol x = Some s"
  shows "∃ δ. is_derivation((terminals p)@[s]@δ)"
proof -
  from pvalid pvalid_def have wellformed_x: "wellformed_item x" by auto
  from next_symbol_starts_item_β[OF wellformed_x next_symbol]
  obtain ψ where ψ: "item_β x = [s] @ ψ" by auto
  from pvalid have "∃ γ. is_derivation((terminals p)@(item_β x)@γ)"
    using pvalid_is_derivation_terminals_item_β by blast
  then obtain γ where "is_derivation((terminals p)@(item_β x)@γ)" by blast
  with ψ have "is_derivation((terminals p)@[s]@ψ@γ)" by auto
  then show ?thesis by blast
qed

lemma pvalid_admissible: 
  assumes pvalid: "pvalid p x" 
  shows "admissible p"
proof -
  have "∃ δ. is_derivation((terminals p)@(item_β x)@δ)"
    by (simp add: pvalid pvalid_is_derivation_terminals_item_β)
  then obtain δ where δ: "is_derivation((terminals p)@(item_β x)@δ)" by blast
  have is_word: "is_word (terminals p)"
    using pvalid_def is_word_terminals pvalid by blast 
  show ?thesis using δ is_derivation_implies_admissible is_word by blast
qed 

lemma pvalid_next_terminal_admissible:
  assumes pvalid: "pvalid p x" 
  assumes next_symbol: "next_symbol x = Some t"
  assumes terminal: "is_terminal t"
  shows "admissible (p@[(t, c)])"
proof -
  have "is_word (terminals p)"
    using is_word_terminals pvalid pvalid_def by blast
  then show ?thesis
    using is_derivation_implies_admissible next_symbol pvalid pvalid_next_symbol_derivable 
      terminal by fastforce
qed

lemma X_wellformed: "t ∈ X k ==> wellformed_token t"
  by (simp add: X_are_terminals wellformed_token_def)

lemma Z_wellformed: "t ∈ Z k u ==> wellformed_token t"
  using X_wellformed Z_subset_X by blast
 
lemma Scan_elem_in_Gen:
  assumes I_in_Gen: "I ⊆ Gen (P k u)"
  assumes k: "k ≤ length Doc"
  assumes T: "T ⊆ Z k u"
  assumes x_in_Scan: "x ∈ Scan T k I"
  shows "x ∈ Gen (P k u)"
proof -
  have "u = 0 ==> x ∈ I" 
  proof -
    assume "u = 0"
    then have "Z k u = {}" by simp
    then have "T = {}" using T by blast
    then have "Scan T k I = I" by (simp add: Scan_empty)
    then show "x ∈ I" using x_in_Scan by simp
  qed
  then have "x ∈ I ∨ (u > 0 ∧ (∃ y t c. x = inc_item y (k + length c) ∧ y ∈ bin I k ∧
    (t, c) ∈ T ∧ next_symbol y = Some t))" using x_in_Scan Scan_def by auto
  then show ?thesis
  proof (induct rule: disjCases2)
    case 1 thus ?case using I_in_Gen by blast
  next
    case 2 
    then obtain y t c where x_is_scan: "x = inc_item y (k + length c) ∧ y ∈ bin I k ∧
       (t, c) ∈ T ∧ next_symbol y = Some t" by blast
    have u_gt_0: "0 < u" using 2 by blast
    have "∃ p ∈ P k u. pvalid p y" using Gen_implies_pvalid I_in_Gen bin_elem x_is_scan by blast 
    then obtain p where p: "p ∈ P k u ∧ pvalid p y" by blast
    have p_dom: "p ∈ P k u" using p by blast
    from p pvalid_def x_is_scan have charslength_p: "charslength p = k"
      using bin_def mem_Collect_eq by auto 
    obtain tok where tok: "tok = (t, c)" using x_is_scan by blast
    have tok_dom: "tok ∈ Z k u" using tok x_is_scan T by blast
    have "p = [] ∨ p ≠ []" by blast
    then have "∃ q ts u'. p = q@ts ∧ u' < u ∧ charslength ts = 0 ∧ is_continuation k u' q ts"
    proof (induct rule: disjCases2)
      case 1 thus ?case
        apply (rule_tac x=p in exI)
        apply (rule_tac x="[]" in exI)
        apply (rule_tac x="0" in exI)
        apply (simp add: 2 is_continuation_def)
        using charslength_p by simp
    next
      case 2
      from final_step_of_path[OF p_dom 2] obtain q ts k' u'
        where final_step: "p = q @ ts ∧ indexlt k' u' k u ∧ is_continuation k' u' q ts" by blast
      then have "k' ≤ k" using indexlt_simp by auto 
      then have "k' < k ∨ k' = k" by arith
      then show ?case
      proof (induct rule: disjCases2)
        case 1 
        have "p ∈ P k' (Suc u')" using final_step is_continuation_in_P by blast 
        then have p_dom: "p ∈ P k 0" by (meson 1 subsetCE subset_P) 
        with charslength_p have "is_continuation k 0 p []" using is_continuation_base by blast 
        then show ?case
          apply (rule_tac x=p in exI)
          apply (rule_tac x="[]" in exI)
          apply (rule_tac x="0" in exI)
          apply (simp add: u_gt_0)
          done
      next
        case 2
        with final_step indexlt_simp have "u' < u" by auto
        then show ?case
          apply (rule_tac x=q in exI)
          apply (rule_tac x=ts in exI)
          apply (rule_tac x=u' in exI)
          using final_step 2 apply auto
          using charslength_p is_continuation_empty_chars by blast
      qed
    qed
    then obtain q ts u' where 
      p_split: "p = q@ts ∧ u' < u ∧ charslength ts = 0 ∧ is_continuation k u' q ts" by blast
    then have "∃ u''. u' ≤ u'' ∧ Suc u'' = u" by (auto, arith)
    then obtain u'' where u'': " u' ≤ u'' ∧ Suc u'' = u" by blast
    with p_split have cont_u'': "is_continuation k u'' q ts" 
      using is_continuation_increase_u by blast 
    have admissible: "admissible (p@[tok])"
      apply (simp add: tok)
      apply (rule_tac pvalid_next_terminal_admissible[where x=y])
      apply (simp add: p)
      apply (simp add: x_is_scan)
      using Z_wellformed tok tok_dom wellformed_token_def by auto 
    have "is_continuation k u'' q (ts@[tok])"
      apply (rule is_continuation_continue)
      apply (simp add: cont_u'')
      using p_split apply simp
      using u'' tok_dom apply simp
      using admissible p_split by auto
    with p_split u'' have ptok_dom: "p@[tok] ∈ P k u" 
      using append_assoc is_continuation_in_P by auto 
    from p obtain i γ where valid:
      "wellformed_tokens p ∧
       wellformed_item y ∧
       i ≤ length p ∧
       charslength p = item_end y ∧
       charslength (take i p) = item_origin y ∧
       is_derivation (terminals (take i p) @ [item_nonterminal y] @ γ) ∧
       derives (item_α y) (terminals (drop i p))" using pvalid_def by blast 
    have clen_ptok: "k + length c = charslength (p@[tok])"
      using charslength_p tok by simp
    from ptok_dom have ptok_doc_tokens: "doc_tokens (p@[tok])"
      using P_are_doc_tokens P_covers_P rev_subsetD by blast
    have wellformed_x: "wellformed_item x"
      apply (simp add: x_is_scan)
      apply (rule_tac wellformed_inc_item)
      apply (simp add: valid)
      apply (simp add: x_is_scan)
      apply (simp only: clen_ptok) 
      using ptok_doc_tokens charslength.simps doc_tokens_length apply presburger 
      apply (simp only: clen_ptok)
      using valid by auto
    have "pvalid (p@[tok]) x"
      apply (auto simp only: pvalid_def)
      apply (rule_tac x=i in exI)
      apply (rule_tac x=γ in exI)
      apply (auto simp only:)
      using ptok_dom admissible admissible_wellformed_tokens apply blast 
      apply (simp add: wellformed_x)
      using valid apply simp
      apply (simp add: x_is_scan clen_ptok)
      using valid apply (simp add: x_is_scan)
      using valid apply (simp add: x_is_scan)
      using valid apply (simp add: x_is_scan)
      apply (subst item_α_of_inc_item)
      using valid apply simp
      using x_is_scan apply simp
      apply (rule_tac derives_append)
      apply simp
      apply (simp add: tok)
      using is_sentence_item_α apply blast
      by (meson pvalid_next_symbol_derivable LocalLexing_axioms is_derivation_is_sentence 
          is_sentence_concat p x_is_scan)
    with ptok_dom show ?thesis
      using Gen_def mem_Collect_eq by blast
  qed
qed

lemma Scan_subset_Gen:
  assumes I_in_Gen: "I ⊆ Gen (P k u)"
  assumes k: "k ≤ length Doc"
  assumes T: "T ⊆ Z k u"
  shows "Scan T k I ⊆ Gen (P k u)"
using I_in_Gen Scan_elem_in_Gen T k by blast

theorem thmD5:
  assumes I: "I ⊆ Gen (P k u)"
  assumes k: "k ≤ length Doc"
  assumes T: "T ⊆ Z k u"
  shows "π k T I ⊆ Gen (P k u)"
apply (simp add: π_def)
apply (rule_tac limit_upperbound)
using I k T Predict_subset_Gen Complete_subset_Gen Scan_subset_Gen apply metis
by (simp add: I)

end

end