[STATEMENT]
lemma Complete_elem_in_Gen:
  assumes I_in_Gen: "I \<subseteq> Gen (\<P> k u)"
  assumes k: "k \<le> length Doc"
  assumes x_in_Complete: "x \<in> Complete k I"
  shows "x \<in> Gen (\<P> k u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Gen (\<P> k u)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> Gen (\<P> k u)
[PROOF STEP]
let ?P = "\<P> k u"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> Gen (\<P> k u)
[PROOF STEP]
from x_in_Complete
[PROOF STATE]
proof (chain)
picking this:
x \<in> Complete k I
[PROOF STEP]
have "x \<in> I \<or> (\<exists> x1 x2. x = inc_item x1 k \<and>
     x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and>
     next_symbol x1 = Some (item_nonterminal x2))"
[PROOF STATE]
proof (prove)
using this:
x \<in> Complete k I

goal (1 subgoal):
 1. x \<in> I \<or> (\<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2))
[PROOF STEP]
by (auto simp add: Complete_def)
[PROOF STATE]
proof (state)
this:
x \<in> I \<or> (\<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2))

goal (1 subgoal):
 1. x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> I \<or> (\<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> I \<or> (\<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2))

goal (1 subgoal):
 1. x \<in> Gen (\<P> k u)
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> I \<Longrightarrow> x \<in> Gen (\<P> k u)
 2. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
x \<in> I

goal (2 subgoals):
 1. x \<in> I \<Longrightarrow> x \<in> Gen (\<P> k u)
 2. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> I

goal (1 subgoal):
 1. x \<in> Gen (\<P> k u)
[PROOF STEP]
using I_in_Gen subsetCE
[PROOF STATE]
proof (prove)
using this:
x \<in> I
I \<subseteq> Gen (\<P> k u)
\<lbrakk>?A \<subseteq> ?B; ?c \<notin> ?A \<Longrightarrow> ?P; ?c \<in> ?B \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. x \<in> Gen (\<P> k u)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> Gen (\<P> k u)

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)
[PROOF STEP]
obtain x1 x2 where x12: "x = inc_item x1 k \<and>
      x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and>
      next_symbol x1 = Some (item_nonterminal x2)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)

goal (1 subgoal):
 1. (\<And>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
from x12
[PROOF STATE]
proof (chain)
picking this:
x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)
[PROOF STEP]
have "\<exists> p1 p2. p1 \<in> ?P \<and> pvalid p1 x1 \<and> p2 \<in> ?P \<and> pvalid p2 x2"
[PROOF STATE]
proof (prove)
using this:
x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)

goal (1 subgoal):
 1. \<exists>p1 p2. p1 \<in> \<P> k u \<and> pvalid p1 x1 \<and> p2 \<in> \<P> k u \<and> pvalid p2 x2
[PROOF STEP]
by (meson Gen_implies_pvalid I_in_Gen bin_elem subsetCE)
[PROOF STATE]
proof (state)
this:
\<exists>p1 p2. p1 \<in> \<P> k u \<and> pvalid p1 x1 \<and> p2 \<in> \<P> k u \<and> pvalid p2 x2

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p1 p2. p1 \<in> \<P> k u \<and> pvalid p1 x1 \<and> p2 \<in> \<P> k u \<and> pvalid p2 x2
[PROOF STEP]
obtain p1 p2 where p1: "p1 \<in> ?P \<and> pvalid p1 x1" and p2: "p2 \<in> ?P \<and> pvalid p2 x2"
[PROOF STATE]
proof (prove)
using this:
\<exists>p1 p2. p1 \<in> \<P> k u \<and> pvalid p1 x1 \<and> p2 \<in> \<P> k u \<and> pvalid p2 x2

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>p1 \<in> \<P> k u \<and> pvalid p1 x1; p2 \<in> \<P> k u \<and> pvalid p2 x2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p1 \<in> \<P> k u \<and> pvalid p1 x1
p2 \<in> \<P> k u \<and> pvalid p2 x2

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
from p1
[PROOF STATE]
proof (chain)
picking this:
p1 \<in> \<P> k u \<and> pvalid p1 x1
[PROOF STEP]
obtain w \<delta> where p1valid:
      "wellformed_tokens p1 \<and>
       wellformed_item x1 \<and>
       w \<le> length p1 \<and>
       charslength p1 = item_end x1 \<and>
       charslength (take w p1) = item_origin x1 \<and>
       is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ \<delta>) \<and>
       derives (item_\<alpha> x1) (terminals (drop w p1))"
[PROOF STATE]
proof (prove)
using this:
p1 \<in> \<P> k u \<and> pvalid p1 x1

goal (1 subgoal):
 1. (\<And>w \<delta>. wellformed_tokens p1 \<and> wellformed_item x1 \<and> w \<le> length p1 \<and> charslength p1 = item_end x1 \<and> charslength (take w p1) = item_origin x1 \<and> is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ \<delta>) \<and> derives (item_\<alpha> x1) (terminals (drop w p1)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pvalid_def
[PROOF STATE]
proof (prove)
using this:
p1 \<in> \<P> k u \<and> pvalid p1 x1
pvalid ?p ?x = (\<exists>u \<gamma>. wellformed_tokens ?p \<and> wellformed_item ?x \<and> u \<le> length ?p \<and> charslength ?p = item_end ?x \<and> charslength (take u ?p) = item_origin ?x \<and> is_derivation (terminals (take u ?p) @ [item_nonterminal ?x] @ \<gamma>) \<and> derives (item_\<alpha> ?x) (terminals (drop u ?p)))

goal (1 subgoal):
 1. (\<And>w \<delta>. wellformed_tokens p1 \<and> wellformed_item x1 \<and> w \<le> length p1 \<and> charslength p1 = item_end x1 \<and> charslength (take w p1) = item_origin x1 \<and> is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ \<delta>) \<and> derives (item_\<alpha> x1) (terminals (drop w p1)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
wellformed_tokens p1 \<and> wellformed_item x1 \<and> w \<le> length p1 \<and> charslength p1 = item_end x1 \<and> charslength (take w p1) = item_origin x1 \<and> is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ \<delta>) \<and> derives (item_\<alpha> x1) (terminals (drop w p1))

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
from p2
[PROOF STATE]
proof (chain)
picking this:
p2 \<in> \<P> k u \<and> pvalid p2 x2
[PROOF STEP]
obtain y \<gamma> where p2valid:
      "wellformed_tokens p2 \<and>
       wellformed_item x2 \<and>
       y \<le> length p2 \<and>
       charslength p2 = item_end x2 \<and>
       charslength (take y p2) = item_origin x2 \<and>
       is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and>
       derives (item_\<alpha> x2) (terminals (drop y p2))"
[PROOF STATE]
proof (prove)
using this:
p2 \<in> \<P> k u \<and> pvalid p2 x2

goal (1 subgoal):
 1. (\<And>y \<gamma>. wellformed_tokens p2 \<and> wellformed_item x2 \<and> y \<le> length p2 \<and> charslength p2 = item_end x2 \<and> charslength (take y p2) = item_origin x2 \<and> is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and> derives (item_\<alpha> x2) (terminals (drop y p2)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pvalid_def
[PROOF STATE]
proof (prove)
using this:
p2 \<in> \<P> k u \<and> pvalid p2 x2
pvalid ?p ?x = (\<exists>u \<gamma>. wellformed_tokens ?p \<and> wellformed_item ?x \<and> u \<le> length ?p \<and> charslength ?p = item_end ?x \<and> charslength (take u ?p) = item_origin ?x \<and> is_derivation (terminals (take u ?p) @ [item_nonterminal ?x] @ \<gamma>) \<and> derives (item_\<alpha> ?x) (terminals (drop u ?p)))

goal (1 subgoal):
 1. (\<And>y \<gamma>. wellformed_tokens p2 \<and> wellformed_item x2 \<and> y \<le> length p2 \<and> charslength p2 = item_end x2 \<and> charslength (take y p2) = item_origin x2 \<and> is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and> derives (item_\<alpha> x2) (terminals (drop y p2)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
wellformed_tokens p2 \<and> wellformed_item x2 \<and> y \<le> length p2 \<and> charslength p2 = item_end x2 \<and> charslength (take y p2) = item_origin x2 \<and> is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and> derives (item_\<alpha> x2) (terminals (drop y p2))

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
let ?r = "p1 @ (drop y p2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have charslength_p1_eq: "charslength p1 = item_end x1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. charslength p1 = item_end x1
[PROOF STEP]
by (simp only: p1valid)
[PROOF STATE]
proof (state)
this:
charslength p1 = item_end x1

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
from x12
[PROOF STATE]
proof (chain)
picking this:
x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)
[PROOF STEP]
have item_end_x1: "item_end x1 = item_origin x2"
[PROOF STATE]
proof (prove)
using this:
x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)

goal (1 subgoal):
 1. item_end x1 = item_origin x2
[PROOF STEP]
using bin_def mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)
bin ?I ?k = {x \<in> ?I. item_end x = ?k}
(?a \<in> Collect ?P) = ?P ?a

goal (1 subgoal):
 1. item_end x1 = item_origin x2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
item_end x1 = item_origin x2

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have item_end_x2: "item_end x2 = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_end x2 = k
[PROOF STEP]
using bin_def x12
[PROOF STATE]
proof (prove)
using this:
bin ?I ?k = {x \<in> ?I. item_end x = ?k}
x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)

goal (1 subgoal):
 1. item_end x2 = k
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
item_end x2 = k

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
item_end x2 = k
[PROOF STEP]
have charslength_p1_leq: "charslength p1 \<le> k"
[PROOF STATE]
proof (prove)
using this:
item_end x2 = k

goal (1 subgoal):
 1. charslength p1 \<le> k
[PROOF STEP]
using charslength_p1_eq item_end_x1 p2valid wellformed_item_def
[PROOF STATE]
proof (prove)
using this:
item_end x2 = k
charslength p1 = item_end x1
item_end x1 = item_origin x2
wellformed_tokens p2 \<and> wellformed_item x2 \<and> y \<le> length p2 \<and> charslength p2 = item_end x2 \<and> charslength (take y p2) = item_origin x2 \<and> is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and> derives (item_\<alpha> x2) (terminals (drop y p2))
wellformed_item ?x = (item_rule ?x \<in> \<RR> \<and> item_origin ?x \<le> item_end ?x \<and> item_end ?x \<le> length Doc \<and> item_dot ?x \<le> length (item_rhs ?x))

goal (1 subgoal):
 1. charslength p1 \<le> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
charslength p1 \<le> k

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have "\<exists>\<delta>'. item_\<beta> x1 = [item_nonterminal x2] @ \<delta>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<delta>'. item_\<beta> x1 = [item_nonterminal x2] @ \<delta>'
[PROOF STEP]
by (simp add: next_symbol_starts_item_\<beta> p1valid x12)
[PROOF STATE]
proof (state)
this:
\<exists>\<delta>'. item_\<beta> x1 = [item_nonterminal x2] @ \<delta>'

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<delta>'. item_\<beta> x1 = [item_nonterminal x2] @ \<delta>'
[PROOF STEP]
obtain \<delta>' where \<delta>': "item_\<beta> x1 = [item_nonterminal x2] @ \<delta>'"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<delta>'. item_\<beta> x1 = [item_nonterminal x2] @ \<delta>'

goal (1 subgoal):
 1. (\<And>\<delta>'. item_\<beta> x1 = [item_nonterminal x2] @ \<delta>' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
item_\<beta> x1 = [item_nonterminal x2] @ \<delta>'

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have "is_derivation ((terminals (take w p1))@(item_rhs x1)@\<delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_derivation (terminals (take w p1) @ item_rhs x1 @ \<delta>)
[PROOF STEP]
using is_derivation_derives p1valid wellformed_item_derives
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>derives ?\<alpha> ?\<beta>; is_derivation (?u @ ?\<alpha> @ ?v)\<rbrakk> \<Longrightarrow> is_derivation (?u @ ?\<beta> @ ?v)
wellformed_tokens p1 \<and> wellformed_item x1 \<and> w \<le> length p1 \<and> charslength p1 = item_end x1 \<and> charslength (take w p1) = item_origin x1 \<and> is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ \<delta>) \<and> derives (item_\<alpha> x1) (terminals (drop w p1))
wellformed_item ?x \<Longrightarrow> derives [item_nonterminal ?x] (item_rhs ?x)

goal (1 subgoal):
 1. is_derivation (terminals (take w p1) @ item_rhs x1 @ \<delta>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_derivation (terminals (take w p1) @ item_rhs x1 @ \<delta>)

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_derivation (terminals (take w p1) @ item_rhs x1 @ \<delta>)
[PROOF STEP]
have "is_derivation ((terminals (take w p1))@(item_\<alpha> x1 @ item_\<beta> x1)@\<delta>)"
[PROOF STATE]
proof (prove)
using this:
is_derivation (terminals (take w p1) @ item_rhs x1 @ \<delta>)

goal (1 subgoal):
 1. is_derivation (terminals (take w p1) @ (item_\<alpha> x1 @ item_\<beta> x1) @ \<delta>)
[PROOF STEP]
by (simp add: item_rhs_split)
[PROOF STATE]
proof (state)
this:
is_derivation (terminals (take w p1) @ (item_\<alpha> x1 @ item_\<beta> x1) @ \<delta>)

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_derivation (terminals (take w p1) @ (item_\<alpha> x1 @ item_\<beta> x1) @ \<delta>)
[PROOF STEP]
have "is_derivation ((terminals (take w p1))@((terminals (drop w p1)) @ item_\<beta> x1)@\<delta>)"
[PROOF STATE]
proof (prove)
using this:
is_derivation (terminals (take w p1) @ (item_\<alpha> x1 @ item_\<beta> x1) @ \<delta>)

goal (1 subgoal):
 1. is_derivation (terminals (take w p1) @ (terminals (drop w p1) @ item_\<beta> x1) @ \<delta>)
[PROOF STEP]
using is_derivation_derives p1valid
[PROOF STATE]
proof (prove)
using this:
is_derivation (terminals (take w p1) @ (item_\<alpha> x1 @ item_\<beta> x1) @ \<delta>)
\<lbrakk>derives ?\<alpha> ?\<beta>; is_derivation (?u @ ?\<alpha> @ ?v)\<rbrakk> \<Longrightarrow> is_derivation (?u @ ?\<beta> @ ?v)
wellformed_tokens p1 \<and> wellformed_item x1 \<and> w \<le> length p1 \<and> charslength p1 = item_end x1 \<and> charslength (take w p1) = item_origin x1 \<and> is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ \<delta>) \<and> derives (item_\<alpha> x1) (terminals (drop w p1))

goal (1 subgoal):
 1. is_derivation (terminals (take w p1) @ (terminals (drop w p1) @ item_\<beta> x1) @ \<delta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_derivation (terminals (take w p1) @ (terminals (drop w p1) @ item_\<beta> x1) @ \<delta>)

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_derivation (terminals (take w p1) @ (terminals (drop w p1) @ item_\<beta> x1) @ \<delta>)
[PROOF STEP]
have "is_derivation ((terminals p1)@(item_\<beta> x1)@\<delta>)"
[PROOF STATE]
proof (prove)
using this:
is_derivation (terminals (take w p1) @ (terminals (drop w p1) @ item_\<beta> x1) @ \<delta>)

goal (1 subgoal):
 1. is_derivation (terminals p1 @ item_\<beta> x1 @ \<delta>)
[PROOF STEP]
by (metis append_assoc append_take_drop_id terminals_append)
[PROOF STATE]
proof (state)
this:
is_derivation (terminals p1 @ item_\<beta> x1 @ \<delta>)

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_derivation (terminals p1 @ item_\<beta> x1 @ \<delta>)
[PROOF STEP]
have "is_derivation ((terminals p1)@([item_nonterminal x2] @ \<delta>')@\<delta>)"
[PROOF STATE]
proof (prove)
using this:
is_derivation (terminals p1 @ item_\<beta> x1 @ \<delta>)

goal (1 subgoal):
 1. is_derivation (terminals p1 @ ([item_nonterminal x2] @ \<delta>') @ \<delta>)
[PROOF STEP]
using is_derivation_derives \<delta>'
[PROOF STATE]
proof (prove)
using this:
is_derivation (terminals p1 @ item_\<beta> x1 @ \<delta>)
\<lbrakk>derives ?\<alpha> ?\<beta>; is_derivation (?u @ ?\<alpha> @ ?v)\<rbrakk> \<Longrightarrow> is_derivation (?u @ ?\<beta> @ ?v)
item_\<beta> x1 = [item_nonterminal x2] @ \<delta>'

goal (1 subgoal):
 1. is_derivation (terminals p1 @ ([item_nonterminal x2] @ \<delta>') @ \<delta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_derivation (terminals p1 @ ([item_nonterminal x2] @ \<delta>') @ \<delta>)

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_derivation (terminals p1 @ ([item_nonterminal x2] @ \<delta>') @ \<delta>)
[PROOF STEP]
have "is_derivation ((terminals p1)@(terminals (drop y p2)) @ \<delta>' @\<delta>)"
[PROOF STATE]
proof (prove)
using this:
is_derivation (terminals p1 @ ([item_nonterminal x2] @ \<delta>') @ \<delta>)

goal (1 subgoal):
 1. is_derivation (terminals p1 @ terminals (drop y p2) @ \<delta>' @ \<delta>)
[PROOF STEP]
using is_complete_def is_derivation_derives is_derivation_step item_\<alpha>_def
        item_nonterminal_def item_rhs_def p2valid wellformed_item_def x12
[PROOF STATE]
proof (prove)
using this:
is_derivation (terminals p1 @ ([item_nonterminal x2] @ \<delta>') @ \<delta>)
is_complete ?x = (length (item_rhs ?x) \<le> item_dot ?x)
\<lbrakk>derives ?\<alpha> ?\<beta>; is_derivation (?u @ ?\<alpha> @ ?v)\<rbrakk> \<Longrightarrow> is_derivation (?u @ ?\<beta> @ ?v)
\<lbrakk>is_derivation (?u @ [?N] @ ?v); (?N, ?\<alpha>) \<in> \<RR>\<rbrakk> \<Longrightarrow> is_derivation (?u @ ?\<alpha> @ ?v)
item_\<alpha> ?x = take (item_dot ?x) (item_rhs ?x)
item_nonterminal ?x = fst (item_rule ?x)
item_rhs ?x = snd (item_rule ?x)
wellformed_tokens p2 \<and> wellformed_item x2 \<and> y \<le> length p2 \<and> charslength p2 = item_end x2 \<and> charslength (take y p2) = item_origin x2 \<and> is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and> derives (item_\<alpha> x2) (terminals (drop y p2))
wellformed_item ?x = (item_rule ?x \<in> \<RR> \<and> item_origin ?x \<le> item_end ?x \<and> item_end ?x \<le> length Doc \<and> item_dot ?x \<le> length (item_rhs ?x))
x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)

goal (1 subgoal):
 1. is_derivation (terminals p1 @ terminals (drop y p2) @ \<delta>' @ \<delta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_derivation (terminals p1 @ terminals (drop y p2) @ \<delta>' @ \<delta>)

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_derivation (terminals p1 @ terminals (drop y p2) @ \<delta>' @ \<delta>)
[PROOF STEP]
have "is_derivation (terminals (p1 @ (drop y p2)) @ (\<delta>' @ \<delta>))"
[PROOF STATE]
proof (prove)
using this:
is_derivation (terminals p1 @ terminals (drop y p2) @ \<delta>' @ \<delta>)

goal (1 subgoal):
 1. is_derivation (terminals (p1 @ drop y p2) @ \<delta>' @ \<delta>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_derivation (terminals (p1 @ drop y p2) @ \<delta>' @ \<delta>)

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_derivation (terminals (p1 @ drop y p2) @ \<delta>' @ \<delta>)
[PROOF STEP]
have admissible_r: "admissible (p1 @ (drop y p2))"
[PROOF STATE]
proof (prove)
using this:
is_derivation (terminals (p1 @ drop y p2) @ \<delta>' @ \<delta>)

goal (1 subgoal):
 1. admissible (p1 @ drop y p2)
[PROOF STEP]
apply (rule_tac is_derivation_implies_admissible)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. is_derivation (terminals (p1 @ drop y p2) @ \<delta>' @ \<delta>) \<Longrightarrow> is_derivation (terminals (p1 @ drop y p2) @ ?\<delta>1)
 2. is_derivation (terminals (p1 @ drop y p2) @ \<delta>' @ \<delta>) \<Longrightarrow> is_word (terminals (p1 @ drop y p2))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. is_derivation (terminals p1 @ drop y (terminals p2) @ \<delta>' @ \<delta>) \<Longrightarrow> is_word (terminals p1)
 2. is_derivation (terminals p1 @ drop y (terminals p2) @ \<delta>' @ \<delta>) \<Longrightarrow> is_word (drop y (terminals p2))
[PROOF STEP]
apply (rule is_word_terminals)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. is_derivation (terminals p1 @ drop y (terminals p2) @ \<delta>' @ \<delta>) \<Longrightarrow> wellformed_tokens p1
 2. is_derivation (terminals p1 @ drop y (terminals p2) @ \<delta>' @ \<delta>) \<Longrightarrow> is_word (drop y (terminals p2))
[PROOF STEP]
apply (simp add: p1valid)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_derivation (terminals p1 @ drop y (terminals p2) @ \<delta>' @ \<delta>) \<Longrightarrow> is_word (drop y (terminals p2))
[PROOF STEP]
using p2valid
[PROOF STATE]
proof (prove)
using this:
wellformed_tokens p2 \<and> wellformed_item x2 \<and> y \<le> length p2 \<and> charslength p2 = item_end x2 \<and> charslength (take y p2) = item_origin x2 \<and> is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and> derives (item_\<alpha> x2) (terminals (drop y p2))

goal (1 subgoal):
 1. is_derivation (terminals p1 @ drop y (terminals p2) @ \<delta>' @ \<delta>) \<Longrightarrow> is_word (drop y (terminals p2))
[PROOF STEP]
using is_word_terminals_drop terminals_drop
[PROOF STATE]
proof (prove)
using this:
wellformed_tokens p2 \<and> wellformed_item x2 \<and> y \<le> length p2 \<and> charslength p2 = item_end x2 \<and> charslength (take y p2) = item_origin x2 \<and> is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and> derives (item_\<alpha> x2) (terminals (drop y p2))
wellformed_tokens ?p \<Longrightarrow> is_word (terminals (drop ?n ?p))
terminals (drop ?n ?p) = drop ?n (terminals ?p)

goal (1 subgoal):
 1. is_derivation (terminals p1 @ drop y (terminals p2) @ \<delta>' @ \<delta>) \<Longrightarrow> is_word (drop y (terminals p2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
admissible (p1 @ drop y p2)

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have r_in_dom: "?r \<in> \<P> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 @ drop y p2 \<in> \<P> k u
[PROOF STEP]
apply (rule_tac general_compatibility)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. p1 \<in> \<P> k u
 2. p2 \<in> \<P> k u
 3. charslength p1 = charslength (take y p2)
 4. charslength p1 \<le> k
 5. admissible (p1 @ drop y p2)
[PROOF STEP]
apply (simp add: p1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. p2 \<in> \<P> k u
 2. charslength p1 = charslength (take y p2)
 3. charslength p1 \<le> k
 4. admissible (p1 @ drop y p2)
[PROOF STEP]
apply (simp add: p2)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. charslength p1 = charslength (take y p2)
 2. charslength p1 \<le> k
 3. admissible (p1 @ drop y p2)
[PROOF STEP]
apply (simp only: p2valid charslength_p1_eq item_end_x1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. charslength p1 \<le> k
 2. admissible (p1 @ drop y p2)
[PROOF STEP]
apply (simp only: charslength_p1_leq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admissible (p1 @ drop y p2)
[PROOF STEP]
by (simp add: admissible_r)
[PROOF STATE]
proof (state)
this:
p1 @ drop y p2 \<in> \<P> k u

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have wellformed_r: "wellformed_tokens ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_tokens (p1 @ drop y p2)
[PROOF STEP]
using admissible_r admissible_wellformed_tokens
[PROOF STATE]
proof (prove)
using this:
admissible (p1 @ drop y p2)
admissible ?p \<Longrightarrow> wellformed_tokens ?p

goal (1 subgoal):
 1. wellformed_tokens (p1 @ drop y p2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
wellformed_tokens (p1 @ drop y p2)

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have wellformed_x: "wellformed_item x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_item x
[PROOF STEP]
apply (simp add: x12)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_item (inc_item x1 k)
[PROOF STEP]
apply (rule_tac wellformed_inc_item)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. wellformed_item x1
 2. next_symbol x1 = Some ?s2
 3. k \<le> length Doc
 4. item_end x1 \<le> k
[PROOF STEP]
apply (simp add: p1valid)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. next_symbol x1 = Some ?s2
 2. k \<le> length Doc
 3. item_end x1 \<le> k
[PROOF STEP]
apply (simp add: x12)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. k \<le> length Doc
 2. item_end x1 \<le> k
[PROOF STEP]
apply (simp add: k)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_end x1 \<le> k
[PROOF STEP]
using charslength_p1_eq charslength_p1_leq
[PROOF STATE]
proof (prove)
using this:
charslength p1 = item_end x1
charslength p1 \<le> k

goal (1 subgoal):
 1. item_end x1 \<le> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wellformed_item x

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have charslength_p1_as_p2: "charslength p1 = charslength (take y p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. charslength p1 = charslength (take y p2)
[PROOF STEP]
using charslength_p1_eq item_end_x1 p2valid
[PROOF STATE]
proof (prove)
using this:
charslength p1 = item_end x1
item_end x1 = item_origin x2
wellformed_tokens p2 \<and> wellformed_item x2 \<and> y \<le> length p2 \<and> charslength p2 = item_end x2 \<and> charslength (take y p2) = item_origin x2 \<and> is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and> derives (item_\<alpha> x2) (terminals (drop y p2))

goal (1 subgoal):
 1. charslength p1 = charslength (take y p2)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
charslength p1 = charslength (take y p2)

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
charslength p1 = charslength (take y p2)
[PROOF STEP]
have charslength_r: "charslength ?r = item_end x"
[PROOF STATE]
proof (prove)
using this:
charslength p1 = charslength (take y p2)

goal (1 subgoal):
 1. charslength (p1 @ drop y p2) = item_end x
[PROOF STEP]
apply (simp add: x12)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (chars p1) = length (chars (take y p2)) \<Longrightarrow> length (chars (take y p2)) + length (chars (drop y p2)) = k
[PROOF STEP]
apply (subst length_append[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (chars p1) = length (chars (take y p2)) \<Longrightarrow> length (chars (take y p2) @ chars (drop y p2)) = k
[PROOF STEP]
apply (subst chars_append[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (chars p1) = length (chars (take y p2)) \<Longrightarrow> length (chars (take y p2 @ drop y p2)) = k
[PROOF STEP]
apply (subst append_take_drop_id)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (chars p1) = length (chars (take y p2)) \<Longrightarrow> length (chars p2) = k
[PROOF STEP]
using item_end_x2 p2valid
[PROOF STATE]
proof (prove)
using this:
item_end x2 = k
wellformed_tokens p2 \<and> wellformed_item x2 \<and> y \<le> length p2 \<and> charslength p2 = item_end x2 \<and> charslength (take y p2) = item_origin x2 \<and> is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and> derives (item_\<alpha> x2) (terminals (drop y p2))

goal (1 subgoal):
 1. length (chars p1) = length (chars (take y p2)) \<Longrightarrow> length (chars p2) = k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
charslength (p1 @ drop y p2) = item_end x

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have item_\<alpha>_x: "item_\<alpha> x = item_\<alpha> x1 @ [item_nonterminal x2]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_\<alpha> x = item_\<alpha> x1 @ [item_nonterminal x2]
[PROOF STEP]
using x12 p1valid
[PROOF STATE]
proof (prove)
using this:
x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)
wellformed_tokens p1 \<and> wellformed_item x1 \<and> w \<le> length p1 \<and> charslength p1 = item_end x1 \<and> charslength (take w p1) = item_origin x1 \<and> is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ \<delta>) \<and> derives (item_\<alpha> x1) (terminals (drop w p1))

goal (1 subgoal):
 1. item_\<alpha> x = item_\<alpha> x1 @ [item_nonterminal x2]
[PROOF STEP]
by (simp add: item_\<alpha>_of_inc_item)
[PROOF STATE]
proof (state)
this:
item_\<alpha> x = item_\<alpha> x1 @ [item_nonterminal x2]

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
from p2valid
[PROOF STATE]
proof (chain)
picking this:
wellformed_tokens p2 \<and> wellformed_item x2 \<and> y \<le> length p2 \<and> charslength p2 = item_end x2 \<and> charslength (take y p2) = item_origin x2 \<and> is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and> derives (item_\<alpha> x2) (terminals (drop y p2))
[PROOF STEP]
have derives_item_nonterminal_x2:
      "derives [item_nonterminal x2] (terminals (drop y p2))"
[PROOF STATE]
proof (prove)
using this:
wellformed_tokens p2 \<and> wellformed_item x2 \<and> y \<le> length p2 \<and> charslength p2 = item_end x2 \<and> charslength (take y p2) = item_origin x2 \<and> is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and> derives (item_\<alpha> x2) (terminals (drop y p2))

goal (1 subgoal):
 1. derives [item_nonterminal x2] (terminals (drop y p2))
[PROOF STEP]
using derives_trans wellformed_complete_item_derives x12
[PROOF STATE]
proof (prove)
using this:
wellformed_tokens p2 \<and> wellformed_item x2 \<and> y \<le> length p2 \<and> charslength p2 = item_end x2 \<and> charslength (take y p2) = item_origin x2 \<and> is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and> derives (item_\<alpha> x2) (terminals (drop y p2))
\<lbrakk>derives ?a ?b; derives ?b ?c\<rbrakk> \<Longrightarrow> derives ?a ?c
\<lbrakk>wellformed_item ?x; is_complete ?x\<rbrakk> \<Longrightarrow> derives [item_nonterminal ?x] (item_\<alpha> ?x)
x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)

goal (1 subgoal):
 1. derives [item_nonterminal x2] (terminals (drop y p2))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
derives [item_nonterminal x2] (terminals (drop y p2))

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have "pvalid ?r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pvalid (p1 @ drop y p2) x
[PROOF STEP]
apply (auto simp only: pvalid_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u \<gamma>. wellformed_tokens (p1 @ drop y p2) \<and> wellformed_item x \<and> u \<le> length (p1 @ drop y p2) \<and> charslength (p1 @ drop y p2) = item_end x \<and> charslength (take u (p1 @ drop y p2)) = item_origin x \<and> is_derivation (terminals (take u (p1 @ drop y p2)) @ [item_nonterminal x] @ \<gamma>) \<and> derives (item_\<alpha> x) (terminals (drop u (p1 @ drop y p2)))
[PROOF STEP]
apply (rule_tac x=w in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<gamma>. wellformed_tokens (p1 @ drop y p2) \<and> wellformed_item x \<and> w \<le> length (p1 @ drop y p2) \<and> charslength (p1 @ drop y p2) = item_end x \<and> charslength (take w (p1 @ drop y p2)) = item_origin x \<and> is_derivation (terminals (take w (p1 @ drop y p2)) @ [item_nonterminal x] @ \<gamma>) \<and> derives (item_\<alpha> x) (terminals (drop w (p1 @ drop y p2)))
[PROOF STEP]
apply (rule_tac x=\<delta> in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_tokens (p1 @ drop y p2) \<and> wellformed_item x \<and> w \<le> length (p1 @ drop y p2) \<and> charslength (p1 @ drop y p2) = item_end x \<and> charslength (take w (p1 @ drop y p2)) = item_origin x \<and> is_derivation (terminals (take w (p1 @ drop y p2)) @ [item_nonterminal x] @ \<delta>) \<and> derives (item_\<alpha> x) (terminals (drop w (p1 @ drop y p2)))
[PROOF STEP]
apply (auto simp only:)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. wellformed_tokens (p1 @ drop y p2)
 2. wellformed_item x
 3. w \<le> length (p1 @ drop y p2)
 4. charslength (p1 @ drop y p2) = item_end x
 5. charslength (take w (p1 @ drop y p2)) = item_origin x
 6. is_derivation (terminals (take w (p1 @ drop y p2)) @ [item_nonterminal x] @ \<delta>)
 7. derives (item_\<alpha> x) (terminals (drop w (p1 @ drop y p2)))
[PROOF STEP]
apply (simp add: wellformed_r)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. wellformed_item x
 2. w \<le> length (p1 @ drop y p2)
 3. charslength (p1 @ drop y p2) = item_end x
 4. charslength (take w (p1 @ drop y p2)) = item_origin x
 5. is_derivation (terminals (take w (p1 @ drop y p2)) @ [item_nonterminal x] @ \<delta>)
 6. derives (item_\<alpha> x) (terminals (drop w (p1 @ drop y p2)))
[PROOF STEP]
apply (simp add: wellformed_x)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. w \<le> length (p1 @ drop y p2)
 2. charslength (p1 @ drop y p2) = item_end x
 3. charslength (take w (p1 @ drop y p2)) = item_origin x
 4. is_derivation (terminals (take w (p1 @ drop y p2)) @ [item_nonterminal x] @ \<delta>)
 5. derives (item_\<alpha> x) (terminals (drop w (p1 @ drop y p2)))
[PROOF STEP]
using p1valid
[PROOF STATE]
proof (prove)
using this:
wellformed_tokens p1 \<and> wellformed_item x1 \<and> w \<le> length p1 \<and> charslength p1 = item_end x1 \<and> charslength (take w p1) = item_origin x1 \<and> is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ \<delta>) \<and> derives (item_\<alpha> x1) (terminals (drop w p1))

goal (5 subgoals):
 1. w \<le> length (p1 @ drop y p2)
 2. charslength (p1 @ drop y p2) = item_end x
 3. charslength (take w (p1 @ drop y p2)) = item_origin x
 4. is_derivation (terminals (take w (p1 @ drop y p2)) @ [item_nonterminal x] @ \<delta>)
 5. derives (item_\<alpha> x) (terminals (drop w (p1 @ drop y p2)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. charslength (p1 @ drop y p2) = item_end x
 2. charslength (take w (p1 @ drop y p2)) = item_origin x
 3. is_derivation (terminals (take w (p1 @ drop y p2)) @ [item_nonterminal x] @ \<delta>)
 4. derives (item_\<alpha> x) (terminals (drop w (p1 @ drop y p2)))
[PROOF STEP]
apply (simp only: charslength_r)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. charslength (take w (p1 @ drop y p2)) = item_origin x
 2. is_derivation (terminals (take w (p1 @ drop y p2)) @ [item_nonterminal x] @ \<delta>)
 3. derives (item_\<alpha> x) (terminals (drop w (p1 @ drop y p2)))
[PROOF STEP]
using x12 p1valid
[PROOF STATE]
proof (prove)
using this:
x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)
wellformed_tokens p1 \<and> wellformed_item x1 \<and> w \<le> length p1 \<and> charslength p1 = item_end x1 \<and> charslength (take w p1) = item_origin x1 \<and> is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ \<delta>) \<and> derives (item_\<alpha> x1) (terminals (drop w p1))

goal (3 subgoals):
 1. charslength (take w (p1 @ drop y p2)) = item_origin x
 2. is_derivation (terminals (take w (p1 @ drop y p2)) @ [item_nonterminal x] @ \<delta>)
 3. derives (item_\<alpha> x) (terminals (drop w (p1 @ drop y p2)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. is_derivation (terminals (take w (p1 @ drop y p2)) @ [item_nonterminal x] @ \<delta>)
 2. derives (item_\<alpha> x) (terminals (drop w (p1 @ drop y p2)))
[PROOF STEP]
using x12 p1valid
[PROOF STATE]
proof (prove)
using this:
x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2)
wellformed_tokens p1 \<and> wellformed_item x1 \<and> w \<le> length p1 \<and> charslength p1 = item_end x1 \<and> charslength (take w p1) = item_origin x1 \<and> is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ \<delta>) \<and> derives (item_\<alpha> x1) (terminals (drop w p1))

goal (2 subgoals):
 1. is_derivation (terminals (take w (p1 @ drop y p2)) @ [item_nonterminal x] @ \<delta>)
 2. derives (item_\<alpha> x) (terminals (drop w (p1 @ drop y p2)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives (item_\<alpha> x) (terminals (drop w (p1 @ drop y p2)))
[PROOF STEP]
apply (simp add:  item_\<alpha>_x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives (item_\<alpha> x1 @ [item_nonterminal x2]) (drop w (terminals p1) @ drop (w - length p1 + y) (terminals p2))
[PROOF STEP]
apply (rule_tac derives_append)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. derives (item_\<alpha> x1) (drop w (terminals p1))
 2. derives [item_nonterminal x2] (drop (w - length p1 + y) (terminals p2))
 3. is_sentence (item_\<alpha> x1)
 4. is_sentence [item_nonterminal x2]
[PROOF STEP]
using p1valid
[PROOF STATE]
proof (prove)
using this:
wellformed_tokens p1 \<and> wellformed_item x1 \<and> w \<le> length p1 \<and> charslength p1 = item_end x1 \<and> charslength (take w p1) = item_origin x1 \<and> is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ \<delta>) \<and> derives (item_\<alpha> x1) (terminals (drop w p1))

goal (4 subgoals):
 1. derives (item_\<alpha> x1) (drop w (terminals p1))
 2. derives [item_nonterminal x2] (drop (w - length p1 + y) (terminals p2))
 3. is_sentence (item_\<alpha> x1)
 4. is_sentence [item_nonterminal x2]
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. derives [item_nonterminal x2] (drop (w - length p1 + y) (terminals p2))
 2. is_sentence (item_\<alpha> x1)
 3. is_sentence [item_nonterminal x2]
[PROOF STEP]
using derives_item_nonterminal_x2 p1valid
[PROOF STATE]
proof (prove)
using this:
derives [item_nonterminal x2] (terminals (drop y p2))
wellformed_tokens p1 \<and> wellformed_item x1 \<and> w \<le> length p1 \<and> charslength p1 = item_end x1 \<and> charslength (take w p1) = item_origin x1 \<and> is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ \<delta>) \<and> derives (item_\<alpha> x1) (terminals (drop w p1))

goal (3 subgoals):
 1. derives [item_nonterminal x2] (drop (w - length p1 + y) (terminals p2))
 2. is_sentence (item_\<alpha> x1)
 3. is_sentence [item_nonterminal x2]
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. is_sentence (item_\<alpha> x1)
 2. is_sentence [item_nonterminal x2]
[PROOF STEP]
using is_sentence_item_\<alpha> p1valid
[PROOF STATE]
proof (prove)
using this:
wellformed_item ?x \<Longrightarrow> is_sentence (item_\<alpha> ?x)
wellformed_tokens p1 \<and> wellformed_item x1 \<and> w \<le> length p1 \<and> charslength p1 = item_end x1 \<and> charslength (take w p1) = item_origin x1 \<and> is_derivation (terminals (take w p1) @ [item_nonterminal x1] @ \<delta>) \<and> derives (item_\<alpha> x1) (terminals (drop w p1))

goal (2 subgoals):
 1. is_sentence (item_\<alpha> x1)
 2. is_sentence [item_nonterminal x2]
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sentence [item_nonterminal x2]
[PROOF STEP]
using is_derivation_is_sentence is_sentence_concat p2valid
[PROOF STATE]
proof (prove)
using this:
is_derivation ?s \<Longrightarrow> is_sentence ?s
is_sentence (?x @ ?y) = (is_sentence ?x \<and> is_sentence ?y)
wellformed_tokens p2 \<and> wellformed_item x2 \<and> y \<le> length p2 \<and> charslength p2 = item_end x2 \<and> charslength (take y p2) = item_origin x2 \<and> is_derivation (terminals (take y p2) @ [item_nonterminal x2] @ \<gamma>) \<and> derives (item_\<alpha> x2) (terminals (drop y p2))

goal (1 subgoal):
 1. is_sentence [item_nonterminal x2]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pvalid (p1 @ drop y p2) x

goal (1 subgoal):
 1. \<exists>x1 x2. x = inc_item x1 k \<and> x1 \<in> bin I (item_origin x2) \<and> x2 \<in> bin I k \<and> is_complete x2 \<and> next_symbol x1 = Some (item_nonterminal x2) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
with r_in_dom
[PROOF STATE]
proof (chain)
picking this:
p1 @ drop y p2 \<in> \<P> k u
pvalid (p1 @ drop y p2) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p1 @ drop y p2 \<in> \<P> k u
pvalid (p1 @ drop y p2) x

goal (1 subgoal):
 1. x \<in> Gen (\<P> k u)
[PROOF STEP]
using Gen_def mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
p1 @ drop y p2 \<in> \<P> k u
pvalid (p1 @ drop y p2) x
Gen ?P = {uu_. \<exists>x p. uu_ = x \<and> p \<in> ?P \<and> pvalid p x}
(?a \<in> Collect ?P) = ?P ?a

goal (1 subgoal):
 1. x \<in> Gen (\<P> k u)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> Gen (\<P> k u)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> Gen (\<P> k u)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Complete_subset_Gen:
  assumes I_in_Gen_P: "I \<subseteq> Gen (\<P> k u)"
  assumes k: "k \<le> length Doc"
  shows "Complete k I \<subseteq> Gen (\<P> k u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complete k I \<subseteq> Gen (\<P> k u)
[PROOF STEP]
using Complete_elem_in_Gen I_in_Gen_P k
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?I \<subseteq> Gen (\<P> ?k ?u); ?k \<le> length Doc; ?x \<in> Complete ?k ?I\<rbrakk> \<Longrightarrow> ?x \<in> Gen (\<P> ?k ?u)
I \<subseteq> Gen (\<P> k u)
k \<le> length Doc

goal (1 subgoal):
 1. Complete k I \<subseteq> Gen (\<P> k u)
[PROOF STEP]
by blast


[STATEMENT]
lemma \<P>_are_admissible: "p \<in> \<P> k u \<Longrightarrow> admissible p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<P> k u \<Longrightarrow> admissible p
[PROOF STEP]
apply (rule_tac \<PP>_are_admissible)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<P> k u \<Longrightarrow> p \<in> \<PP>
[PROOF STEP]
using \<PP>_covers_\<P> subsetCE
[PROOF STATE]
proof (prove)
using this:
\<P> ?k ?u \<subseteq> \<PP>
\<lbrakk>?A \<subseteq> ?B; ?c \<notin> ?A \<Longrightarrow> ?P; ?c \<in> ?B \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. p \<in> \<P> k u \<Longrightarrow> p \<in> \<PP>
[PROOF STEP]
by blast


[STATEMENT]
lemma is_continuation_base:
  assumes p_dom: "p \<in> \<P> k u"
  assumes charslength_p: "charslength p = k"
  shows "is_continuation k u p []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_continuation k u p []
[PROOF STEP]
apply (auto simp add: is_continuation_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. p \<in> \<P> k u
 2. length (chars p) = k
 3. admissible p
[PROOF STEP]
apply (simp add: p_dom)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (chars p) = k
 2. admissible p
[PROOF STEP]
using charslength_p
[PROOF STATE]
proof (prove)
using this:
charslength p = k

goal (2 subgoals):
 1. length (chars p) = k
 2. admissible p
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admissible p
[PROOF STEP]
using \<P>_are_admissible p_dom
[PROOF STATE]
proof (prove)
using this:
?p \<in> \<P> ?k ?u \<Longrightarrow> admissible ?p
p \<in> \<P> k u

goal (1 subgoal):
 1. admissible p
[PROOF STEP]
by blast


[STATEMENT]
lemma is_continuation_empty_chars:
  "is_continuation k u q ts \<Longrightarrow> charslength (q@ts) = k \<Longrightarrow> chars ts = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_continuation k u q ts; charslength (q @ ts) = k\<rbrakk> \<Longrightarrow> chars ts = []
[PROOF STEP]
by (simp add: is_continuation_def)


[STATEMENT]
lemma \<Z>_subset: "u \<le> v \<Longrightarrow> \<Z> k u \<subseteq> \<Z> k v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<le> v \<Longrightarrow> \<Z> k u \<subseteq> \<Z> k v
[PROOF STEP]
using \<Z>_subset_Suc subset_fSuc
[PROOF STATE]
proof (prove)
using this:
\<Z> ?k ?n \<subseteq> \<Z> ?k (Suc ?n)
\<lbrakk>\<And>u. ?f u \<subseteq> ?f (Suc u); ?u \<le> ?v\<rbrakk> \<Longrightarrow> ?f ?u \<subseteq> ?f ?v

goal (1 subgoal):
 1. u \<le> v \<Longrightarrow> \<Z> k u \<subseteq> \<Z> k v
[PROOF STEP]
by blast


[STATEMENT]
lemma is_continuation_increase_u:
  assumes cont: "is_continuation k u q ts"
  assumes uv: "u \<le> v"
  shows "is_continuation k v q ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_continuation k v q ts
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_continuation k v q ts
[PROOF STEP]
have "q \<in> \<P> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> \<P> k u
[PROOF STEP]
using cont is_continuation_def
[PROOF STATE]
proof (prove)
using this:
is_continuation k u q ts
is_continuation ?k ?u ?q ?ts = (?q \<in> \<P> ?k ?u \<and> charslength ?q = ?k \<and> admissible (?q @ ?ts) \<and> (\<forall>t\<in>set ?ts. t \<in> \<Z> ?k (Suc ?u)) \<and> (\<forall>t\<in>set (butlast ?ts). chars_of_token t = []))

goal (1 subgoal):
 1. q \<in> \<P> k u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q \<in> \<P> k u

goal (1 subgoal):
 1. is_continuation k v q ts
[PROOF STEP]
with uv
[PROOF STATE]
proof (chain)
picking this:
u \<le> v
q \<in> \<P> k u
[PROOF STEP]
have q_dom: "q \<in> \<P> k v"
[PROOF STATE]
proof (prove)
using this:
u \<le> v
q \<in> \<P> k u

goal (1 subgoal):
 1. q \<in> \<P> k v
[PROOF STEP]
by (meson subsetCE subset_\<P>k)
[PROOF STATE]
proof (state)
this:
q \<in> \<P> k v

goal (1 subgoal):
 1. is_continuation k v q ts
[PROOF STEP]
from uv
[PROOF STATE]
proof (chain)
picking this:
u \<le> v
[PROOF STEP]
have \<Z>: "\<And> t. t \<in> \<Z> k (Suc u) \<Longrightarrow> t \<in> \<Z> k (Suc v)"
[PROOF STATE]
proof (prove)
using this:
u \<le> v

goal (1 subgoal):
 1. \<And>t. t \<in> \<Z> k (Suc u) \<Longrightarrow> t \<in> \<Z> k (Suc v)
[PROOF STEP]
using \<Z>_subset le_neq_implies_less less_imp_le_nat not_less_eq subsetCE
[PROOF STATE]
proof (prove)
using this:
u \<le> v
?u \<le> ?v \<Longrightarrow> \<Z> ?k ?u \<subseteq> \<Z> ?k ?v
\<lbrakk>?m \<le> ?n; ?m \<noteq> ?n\<rbrakk> \<Longrightarrow> ?m < ?n
?m < ?n \<Longrightarrow> ?m \<le> ?n
(\<not> ?m < ?n) = (?n < Suc ?m)
\<lbrakk>?A \<subseteq> ?B; ?c \<notin> ?A \<Longrightarrow> ?P; ?c \<in> ?B \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<And>t. t \<in> \<Z> k (Suc u) \<Longrightarrow> t \<in> \<Z> k (Suc v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?t \<in> \<Z> k (Suc u) \<Longrightarrow> ?t \<in> \<Z> k (Suc v)

goal (1 subgoal):
 1. is_continuation k v q ts
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_continuation k v q ts
[PROOF STEP]
apply (auto simp only: is_continuation_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. q \<in> \<P> k v
 2. charslength q = k
 3. admissible (q @ ts)
 4. \<And>a b. (a, b) \<in> set ts \<Longrightarrow> (a, b) \<in> \<Z> k (Suc v)
 5. \<And>a b. (a, b) \<in> set (butlast ts) \<Longrightarrow> chars_of_token (a, b) = []
[PROOF STEP]
apply (simp add: q_dom)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. charslength q = k
 2. admissible (q @ ts)
 3. \<And>a b. (a, b) \<in> set ts \<Longrightarrow> (a, b) \<in> \<Z> k (Suc v)
 4. \<And>a b. (a, b) \<in> set (butlast ts) \<Longrightarrow> chars_of_token (a, b) = []
[PROOF STEP]
using cont is_continuation_def
[PROOF STATE]
proof (prove)
using this:
is_continuation k u q ts
is_continuation ?k ?u ?q ?ts = (?q \<in> \<P> ?k ?u \<and> charslength ?q = ?k \<and> admissible (?q @ ?ts) \<and> (\<forall>t\<in>set ?ts. t \<in> \<Z> ?k (Suc ?u)) \<and> (\<forall>t\<in>set (butlast ?ts). chars_of_token t = []))

goal (4 subgoals):
 1. charslength q = k
 2. admissible (q @ ts)
 3. \<And>a b. (a, b) \<in> set ts \<Longrightarrow> (a, b) \<in> \<Z> k (Suc v)
 4. \<And>a b. (a, b) \<in> set (butlast ts) \<Longrightarrow> chars_of_token (a, b) = []
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. admissible (q @ ts)
 2. \<And>a b. (a, b) \<in> set ts \<Longrightarrow> (a, b) \<in> \<Z> k (Suc v)
 3. \<And>a b. (a, b) \<in> set (butlast ts) \<Longrightarrow> chars_of_token (a, b) = []
[PROOF STEP]
using cont is_continuation_def
[PROOF STATE]
proof (prove)
using this:
is_continuation k u q ts
is_continuation ?k ?u ?q ?ts = (?q \<in> \<P> ?k ?u \<and> charslength ?q = ?k \<and> admissible (?q @ ?ts) \<and> (\<forall>t\<in>set ?ts. t \<in> \<Z> ?k (Suc ?u)) \<and> (\<forall>t\<in>set (butlast ?ts). chars_of_token t = []))

goal (3 subgoals):
 1. admissible (q @ ts)
 2. \<And>a b. (a, b) \<in> set ts \<Longrightarrow> (a, b) \<in> \<Z> k (Suc v)
 3. \<And>a b. (a, b) \<in> set (butlast ts) \<Longrightarrow> chars_of_token (a, b) = []
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> set ts \<Longrightarrow> (a, b) \<in> \<Z> k (Suc v)
 2. \<And>a b. (a, b) \<in> set (butlast ts) \<Longrightarrow> chars_of_token (a, b) = []
[PROOF STEP]
using cont is_continuation_def \<Z>
[PROOF STATE]
proof (prove)
using this:
is_continuation k u q ts
is_continuation ?k ?u ?q ?ts = (?q \<in> \<P> ?k ?u \<and> charslength ?q = ?k \<and> admissible (?q @ ?ts) \<and> (\<forall>t\<in>set ?ts. t \<in> \<Z> ?k (Suc ?u)) \<and> (\<forall>t\<in>set (butlast ?ts). chars_of_token t = []))
?t \<in> \<Z> k (Suc u) \<Longrightarrow> ?t \<in> \<Z> k (Suc v)

goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> set ts \<Longrightarrow> (a, b) \<in> \<Z> k (Suc v)
 2. \<And>a b. (a, b) \<in> set (butlast ts) \<Longrightarrow> chars_of_token (a, b) = []
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set (butlast ts) \<Longrightarrow> chars_of_token (a, b) = []
[PROOF STEP]
using cont is_continuation_def
[PROOF STATE]
proof (prove)
using this:
is_continuation k u q ts
is_continuation ?k ?u ?q ?ts = (?q \<in> \<P> ?k ?u \<and> charslength ?q = ?k \<and> admissible (?q @ ?ts) \<and> (\<forall>t\<in>set ?ts. t \<in> \<Z> ?k (Suc ?u)) \<and> (\<forall>t\<in>set (butlast ?ts). chars_of_token t = []))

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set (butlast ts) \<Longrightarrow> chars_of_token (a, b) = []
[PROOF STEP]
apply (simp only:)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
is_continuation k v q ts

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pvalid_next_symbol_derivable:
  assumes pvalid: "pvalid p x"
  assumes next_symbol: "next_symbol x = Some s"
  shows "\<exists> \<delta>. is_derivation((terminals p)@[s]@\<delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<delta>. is_derivation (terminals p @ [s] @ \<delta>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<delta>. is_derivation (terminals p @ [s] @ \<delta>)
[PROOF STEP]
from pvalid pvalid_def
[PROOF STATE]
proof (chain)
picking this:
pvalid p x
pvalid ?p ?x = (\<exists>u \<gamma>. wellformed_tokens ?p \<and> wellformed_item ?x \<and> u \<le> length ?p \<and> charslength ?p = item_end ?x \<and> charslength (take u ?p) = item_origin ?x \<and> is_derivation (terminals (take u ?p) @ [item_nonterminal ?x] @ \<gamma>) \<and> derives (item_\<alpha> ?x) (terminals (drop u ?p)))
[PROOF STEP]
have wellformed_x: "wellformed_item x"
[PROOF STATE]
proof (prove)
using this:
pvalid p x
pvalid ?p ?x = (\<exists>u \<gamma>. wellformed_tokens ?p \<and> wellformed_item ?x \<and> u \<le> length ?p \<and> charslength ?p = item_end ?x \<and> charslength (take u ?p) = item_origin ?x \<and> is_derivation (terminals (take u ?p) @ [item_nonterminal ?x] @ \<gamma>) \<and> derives (item_\<alpha> ?x) (terminals (drop u ?p)))

goal (1 subgoal):
 1. wellformed_item x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wellformed_item x

goal (1 subgoal):
 1. \<exists>\<delta>. is_derivation (terminals p @ [s] @ \<delta>)
[PROOF STEP]
from next_symbol_starts_item_\<beta>[OF wellformed_x next_symbol]
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<delta>. item_\<beta> x = s # \<delta>
[PROOF STEP]
obtain \<omega> where \<omega>: "item_\<beta> x = [s] @ \<omega>"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<delta>. item_\<beta> x = s # \<delta>

goal (1 subgoal):
 1. (\<And>\<omega>. item_\<beta> x = [s] @ \<omega> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
item_\<beta> x = [s] @ \<omega>

goal (1 subgoal):
 1. \<exists>\<delta>. is_derivation (terminals p @ [s] @ \<delta>)
[PROOF STEP]
from pvalid
[PROOF STATE]
proof (chain)
picking this:
pvalid p x
[PROOF STEP]
have "\<exists> \<gamma>. is_derivation((terminals p)@(item_\<beta> x)@\<gamma>)"
[PROOF STATE]
proof (prove)
using this:
pvalid p x

goal (1 subgoal):
 1. \<exists>\<gamma>. is_derivation (terminals p @ item_\<beta> x @ \<gamma>)
[PROOF STEP]
using pvalid_is_derivation_terminals_item_\<beta>
[PROOF STATE]
proof (prove)
using this:
pvalid p x
pvalid ?p ?x \<Longrightarrow> \<exists>\<delta>. is_derivation (terminals ?p @ item_\<beta> ?x @ \<delta>)

goal (1 subgoal):
 1. \<exists>\<gamma>. is_derivation (terminals p @ item_\<beta> x @ \<gamma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<gamma>. is_derivation (terminals p @ item_\<beta> x @ \<gamma>)

goal (1 subgoal):
 1. \<exists>\<delta>. is_derivation (terminals p @ [s] @ \<delta>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<gamma>. is_derivation (terminals p @ item_\<beta> x @ \<gamma>)
[PROOF STEP]
obtain \<gamma> where "is_derivation((terminals p)@(item_\<beta> x)@\<gamma>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<gamma>. is_derivation (terminals p @ item_\<beta> x @ \<gamma>)

goal (1 subgoal):
 1. (\<And>\<gamma>. is_derivation (terminals p @ item_\<beta> x @ \<gamma>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_derivation (terminals p @ item_\<beta> x @ \<gamma>)

goal (1 subgoal):
 1. \<exists>\<delta>. is_derivation (terminals p @ [s] @ \<delta>)
[PROOF STEP]
with \<omega>
[PROOF STATE]
proof (chain)
picking this:
item_\<beta> x = [s] @ \<omega>
is_derivation (terminals p @ item_\<beta> x @ \<gamma>)
[PROOF STEP]
have "is_derivation((terminals p)@[s]@\<omega>@\<gamma>)"
[PROOF STATE]
proof (prove)
using this:
item_\<beta> x = [s] @ \<omega>
is_derivation (terminals p @ item_\<beta> x @ \<gamma>)

goal (1 subgoal):
 1. is_derivation (terminals p @ [s] @ \<omega> @ \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_derivation (terminals p @ [s] @ \<omega> @ \<gamma>)

goal (1 subgoal):
 1. \<exists>\<delta>. is_derivation (terminals p @ [s] @ \<delta>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_derivation (terminals p @ [s] @ \<omega> @ \<gamma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_derivation (terminals p @ [s] @ \<omega> @ \<gamma>)

goal (1 subgoal):
 1. \<exists>\<delta>. is_derivation (terminals p @ [s] @ \<delta>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<delta>. is_derivation (terminals p @ [s] @ \<delta>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pvalid_admissible:
  assumes pvalid: "pvalid p x"
  shows "admissible p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admissible p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. admissible p
[PROOF STEP]
have "\<exists> \<delta>. is_derivation((terminals p)@(item_\<beta> x)@\<delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<delta>. is_derivation (terminals p @ item_\<beta> x @ \<delta>)
[PROOF STEP]
by (simp add: pvalid pvalid_is_derivation_terminals_item_\<beta>)
[PROOF STATE]
proof (state)
this:
\<exists>\<delta>. is_derivation (terminals p @ item_\<beta> x @ \<delta>)

goal (1 subgoal):
 1. admissible p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<delta>. is_derivation (terminals p @ item_\<beta> x @ \<delta>)
[PROOF STEP]
obtain \<delta> where \<delta>: "is_derivation((terminals p)@(item_\<beta> x)@\<delta>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<delta>. is_derivation (terminals p @ item_\<beta> x @ \<delta>)

goal (1 subgoal):
 1. (\<And>\<delta>. is_derivation (terminals p @ item_\<beta> x @ \<delta>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_derivation (terminals p @ item_\<beta> x @ \<delta>)

goal (1 subgoal):
 1. admissible p
[PROOF STEP]
have is_word: "is_word (terminals p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_word (terminals p)
[PROOF STEP]
using pvalid_def is_word_terminals pvalid
[PROOF STATE]
proof (prove)
using this:
pvalid ?p ?x = (\<exists>u \<gamma>. wellformed_tokens ?p \<and> wellformed_item ?x \<and> u \<le> length ?p \<and> charslength ?p = item_end ?x \<and> charslength (take u ?p) = item_origin ?x \<and> is_derivation (terminals (take u ?p) @ [item_nonterminal ?x] @ \<gamma>) \<and> derives (item_\<alpha> ?x) (terminals (drop u ?p)))
wellformed_tokens ?p \<Longrightarrow> is_word (terminals ?p)
pvalid p x

goal (1 subgoal):
 1. is_word (terminals p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_word (terminals p)

goal (1 subgoal):
 1. admissible p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admissible p
[PROOF STEP]
using \<delta> is_derivation_implies_admissible is_word
[PROOF STATE]
proof (prove)
using this:
is_derivation (terminals p @ item_\<beta> x @ \<delta>)
\<lbrakk>is_derivation (terminals ?p @ ?\<delta>); is_word (terminals ?p)\<rbrakk> \<Longrightarrow> admissible ?p
is_word (terminals p)

goal (1 subgoal):
 1. admissible p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
admissible p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. admissible (p @ [(t, c)])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. admissible (p @ [(t, c)])
[PROOF STEP]
have "is_word (terminals p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_word (terminals p)
[PROOF STEP]
using is_word_terminals pvalid pvalid_def
[PROOF STATE]
proof (prove)
using this:
wellformed_tokens ?p \<Longrightarrow> is_word (terminals ?p)
pvalid p x
pvalid ?p ?x = (\<exists>u \<gamma>. wellformed_tokens ?p \<and> wellformed_item ?x \<and> u \<le> length ?p \<and> charslength ?p = item_end ?x \<and> charslength (take u ?p) = item_origin ?x \<and> is_derivation (terminals (take u ?p) @ [item_nonterminal ?x] @ \<gamma>) \<and> derives (item_\<alpha> ?x) (terminals (drop u ?p)))

goal (1 subgoal):
 1. is_word (terminals p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_word (terminals p)

goal (1 subgoal):
 1. admissible (p @ [(t, c)])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_word (terminals p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_word (terminals p)

goal (1 subgoal):
 1. admissible (p @ [(t, c)])
[PROOF STEP]
using is_derivation_implies_admissible next_symbol pvalid pvalid_next_symbol_derivable
      terminal
[PROOF STATE]
proof (prove)
using this:
is_word (terminals p)
\<lbrakk>is_derivation (terminals ?p @ ?\<delta>); is_word (terminals ?p)\<rbrakk> \<Longrightarrow> admissible ?p
next_symbol x = Some t
pvalid p x
\<lbrakk>pvalid ?p ?x; next_symbol ?x = Some ?s\<rbrakk> \<Longrightarrow> \<exists>\<delta>. is_derivation (terminals ?p @ [?s] @ \<delta>)
is_terminal t

goal (1 subgoal):
 1. admissible (p @ [(t, c)])
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
admissible (p @ [(t, c)])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<X>_wellformed: "t \<in> \<X> k \<Longrightarrow> wellformed_token t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> \<X> k \<Longrightarrow> wellformed_token t
[PROOF STEP]
by (simp add: \<X>_are_terminals wellformed_token_def)


[STATEMENT]
lemma \<Z>_wellformed: "t \<in> \<Z> k u \<Longrightarrow> wellformed_token t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> \<Z> k u \<Longrightarrow> wellformed_token t
[PROOF STEP]
using \<X>_wellformed \<Z>_subset_\<X>
[PROOF STATE]
proof (prove)
using this:
?t \<in> \<X> ?k \<Longrightarrow> wellformed_token ?t
\<Z> ?k ?n \<subseteq> \<X> ?k

goal (1 subgoal):
 1. t \<in> \<Z> k u \<Longrightarrow> wellformed_token t
[PROOF STEP]
by blast