[STATEMENT]
lemma Scan_elem_in_Gen:
  assumes I_in_Gen: "I \<subseteq> Gen (\<P> k u)"
  assumes k: "k \<le> length Doc"
  assumes T: "T \<subseteq> \<Z> k u"
  assumes x_in_Scan: "x \<in> Scan T 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]
have "u = 0 \<Longrightarrow> x \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = 0 \<Longrightarrow> x \<in> I
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u = 0 \<Longrightarrow> x \<in> I
[PROOF STEP]
assume "u = 0"
[PROOF STATE]
proof (state)
this:
u = 0

goal (1 subgoal):
 1. u = 0 \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = 0
[PROOF STEP]
have "\<Z> k u = {}"
[PROOF STATE]
proof (prove)
using this:
u = 0

goal (1 subgoal):
 1. \<Z> k u = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Z> k u = {}

goal (1 subgoal):
 1. u = 0 \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Z> k u = {}
[PROOF STEP]
have "T = {}"
[PROOF STATE]
proof (prove)
using this:
\<Z> k u = {}

goal (1 subgoal):
 1. T = {}
[PROOF STEP]
using T
[PROOF STATE]
proof (prove)
using this:
\<Z> k u = {}
T \<subseteq> \<Z> k u

goal (1 subgoal):
 1. T = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T = {}

goal (1 subgoal):
 1. u = 0 \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T = {}
[PROOF STEP]
have "Scan T k I = I"
[PROOF STATE]
proof (prove)
using this:
T = {}

goal (1 subgoal):
 1. Scan T k I = I
[PROOF STEP]
by (simp add: Scan_empty)
[PROOF STATE]
proof (state)
this:
Scan T k I = I

goal (1 subgoal):
 1. u = 0 \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Scan T k I = I
[PROOF STEP]
show "x \<in> I"
[PROOF STATE]
proof (prove)
using this:
Scan T k I = I

goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
using x_in_Scan
[PROOF STATE]
proof (prove)
using this:
Scan T k I = I
x \<in> Scan T k I

goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> I

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u = 0 \<Longrightarrow> x \<in> I

goal (1 subgoal):
 1. x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = 0 \<Longrightarrow> x \<in> I
[PROOF STEP]
have "x \<in> I \<or> (u > 0 \<and> (\<exists> y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and>
    (t, c) \<in> T \<and> next_symbol y = Some t))"
[PROOF STATE]
proof (prove)
using this:
u = 0 \<Longrightarrow> x \<in> I

goal (1 subgoal):
 1. x \<in> I \<or> 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t)
[PROOF STEP]
using x_in_Scan Scan_def
[PROOF STATE]
proof (prove)
using this:
u = 0 \<Longrightarrow> x \<in> I
x \<in> Scan T k I
Scan ?T ?k ?I = ?I \<union> {uu_. \<exists>x t c. uu_ = inc_item x (?k + length c) \<and> x \<in> bin ?I ?k \<and> (t, c) \<in> ?T \<and> next_symbol x = Some t}

goal (1 subgoal):
 1. x \<in> I \<or> 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> I \<or> 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t)

goal (1 subgoal):
 1. x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> I \<or> 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> I \<or> 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t)

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. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<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. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<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
[PROOF STATE]
proof (prove)
using this:
x \<in> I
I \<subseteq> Gen (\<P> k u)

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. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t)

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t)
[PROOF STEP]
obtain y t c where x_is_scan: "x = inc_item y (k + length c) \<and> y \<in> bin I k \<and>
       (t, c) \<in> T \<and> next_symbol y = Some t"
[PROOF STATE]
proof (prove)
using this:
0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t)

goal (1 subgoal):
 1. (\<And>y c t. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have u_gt_0: "0 < u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < u
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t)

goal (1 subgoal):
 1. 0 < u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < u

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have "\<exists> p \<in> \<P> k u. pvalid p y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p\<in>\<P> k u. pvalid p y
[PROOF STEP]
using Gen_implies_pvalid I_in_Gen bin_elem x_is_scan
[PROOF STATE]
proof (prove)
using this:
?x \<in> Gen ?P \<Longrightarrow> \<exists>p\<in>?P. pvalid p ?x
I \<subseteq> Gen (\<P> k u)
?x \<in> bin ?I ?k \<Longrightarrow> ?x \<in> ?I
x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t

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

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p\<in>\<P> k u. pvalid p y
[PROOF STEP]
obtain p where p: "p \<in> \<P> k u \<and> pvalid p y"
[PROOF STATE]
proof (prove)
using this:
\<exists>p\<in>\<P> k u. pvalid p y

goal (1 subgoal):
 1. (\<And>p. p \<in> \<P> k u \<and> pvalid p y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<in> \<P> k u \<and> pvalid p y

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have p_dom: "p \<in> \<P> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<P> k u
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u \<and> pvalid p y

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

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
from p pvalid_def x_is_scan
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<P> k u \<and> pvalid p y
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)))
x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t
[PROOF STEP]
have charslength_p: "charslength p = k"
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u \<and> pvalid p y
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)))
x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t

goal (1 subgoal):
 1. charslength p = k
[PROOF STEP]
using bin_def mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u \<and> pvalid p y
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)))
x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t
bin ?I ?k = {x \<in> ?I. item_end x = ?k}
(?a \<in> Collect ?P) = ?P ?a

goal (1 subgoal):
 1. charslength p = k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
charslength p = k

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
obtain tok where tok: "tok = (t, c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>tok. tok = (t, c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using x_is_scan
[PROOF STATE]
proof (prove)
using this:
x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t

goal (1 subgoal):
 1. (\<And>tok. tok = (t, c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
tok = (t, c)

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have tok_dom: "tok \<in> \<Z> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tok \<in> \<Z> k u
[PROOF STEP]
using tok x_is_scan T
[PROOF STATE]
proof (prove)
using this:
tok = (t, c)
x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t
T \<subseteq> \<Z> k u

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

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have "p = [] \<or> p \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = [] \<or> p \<noteq> []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p = [] \<or> p \<noteq> []

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = [] \<or> p \<noteq> []
[PROOF STEP]
have "\<exists> q ts u'. p = q@ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts"
[PROOF STATE]
proof (prove)
using this:
p = [] \<or> p \<noteq> []

goal (1 subgoal):
 1. \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = [] \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
 2. p \<noteq> [] \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
p = []

goal (2 subgoals):
 1. p = [] \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
 2. p \<noteq> [] \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
p = []

goal (1 subgoal):
 1. \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
apply (rule_tac x=p in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = [] \<Longrightarrow> \<exists>ts u'. p = p @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' p ts
[PROOF STEP]
apply (rule_tac x="[]" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = [] \<Longrightarrow> \<exists>u'. p = p @ [] \<and> u' < u \<and> charslength [] = 0 \<and> is_continuation k u' p []
[PROOF STEP]
apply (rule_tac x="0" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = [] \<Longrightarrow> p = p @ [] \<and> 0 < u \<and> charslength [] = 0 \<and> is_continuation k 0 p []
[PROOF STEP]
apply (simp add: 2 is_continuation_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = [] \<Longrightarrow> k = 0
[PROOF STEP]
using charslength_p
[PROOF STATE]
proof (prove)
using this:
charslength p = k

goal (1 subgoal):
 1. p = [] \<Longrightarrow> k = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
p \<noteq> []

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
from final_step_of_path[OF p_dom 2]
[PROOF STATE]
proof (chain)
picking this:
\<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
obtain q ts k' u'
        where final_step: "p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts"
[PROOF STATE]
proof (prove)
using this:
\<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts

goal (1 subgoal):
 1. (\<And>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
have "k' \<le> k"
[PROOF STATE]
proof (prove)
using this:
p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts

goal (1 subgoal):
 1. k' \<le> k
[PROOF STEP]
using indexlt_simp
[PROOF STATE]
proof (prove)
using this:
p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
indexlt ?k' ?u' ?k ?u = (?k' < ?k \<or> ?k' = ?k \<and> ?u' < ?u)

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

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k' \<le> k
[PROOF STEP]
have "k' < k \<or> k' = k"
[PROOF STATE]
proof (prove)
using this:
k' \<le> k

goal (1 subgoal):
 1. k' < k \<or> k' = k
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
k' < k \<or> k' = k

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k' < k \<or> k' = k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
k' < k \<or> k' = k

goal (1 subgoal):
 1. \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k' < k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
 2. k' = k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
k' < k

goal (2 subgoals):
 1. k' < k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
 2. k' = k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
have "p \<in> \<P> k' (Suc u')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<P> k' (Suc u')
[PROOF STEP]
using final_step is_continuation_in_\<P>
[PROOF STATE]
proof (prove)
using this:
p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
is_continuation ?k ?u ?p ?ts \<Longrightarrow> ?p @ ?ts \<in> \<P> ?k (Suc ?u)

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

goal (2 subgoals):
 1. k' < k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
 2. k' = k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<P> k' (Suc u')
[PROOF STEP]
have p_dom: "p \<in> \<P> k 0"
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k' (Suc u')

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

goal (2 subgoals):
 1. k' < k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
 2. k' = k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
with charslength_p
[PROOF STATE]
proof (chain)
picking this:
charslength p = k
p \<in> \<P> k 0
[PROOF STEP]
have "is_continuation k 0 p []"
[PROOF STATE]
proof (prove)
using this:
charslength p = k
p \<in> \<P> k 0

goal (1 subgoal):
 1. is_continuation k 0 p []
[PROOF STEP]
using is_continuation_base
[PROOF STATE]
proof (prove)
using this:
charslength p = k
p \<in> \<P> k 0
\<lbrakk>?p \<in> \<P> ?k ?u; charslength ?p = ?k\<rbrakk> \<Longrightarrow> is_continuation ?k ?u ?p []

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

goal (2 subgoals):
 1. k' < k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
 2. k' = k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_continuation k 0 p []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_continuation k 0 p []

goal (1 subgoal):
 1. \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
apply (rule_tac x=p in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_continuation k 0 p [] \<Longrightarrow> \<exists>ts u'. p = p @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' p ts
[PROOF STEP]
apply (rule_tac x="[]" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_continuation k 0 p [] \<Longrightarrow> \<exists>u'. p = p @ [] \<and> u' < u \<and> charslength [] = 0 \<and> is_continuation k u' p []
[PROOF STEP]
apply (rule_tac x="0" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_continuation k 0 p [] \<Longrightarrow> p = p @ [] \<and> 0 < u \<and> charslength [] = 0 \<and> is_continuation k 0 p []
[PROOF STEP]
apply (simp add: u_gt_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts

goal (1 subgoal):
 1. k' = k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k' = k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
k' = k

goal (1 subgoal):
 1. k' = k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
with final_step indexlt_simp
[PROOF STATE]
proof (chain)
picking this:
p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
indexlt ?k' ?u' ?k ?u = (?k' < ?k \<or> ?k' = ?k \<and> ?u' < ?u)
k' = k
[PROOF STEP]
have "u' < u"
[PROOF STATE]
proof (prove)
using this:
p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
indexlt ?k' ?u' ?k ?u = (?k' < ?k \<or> ?k' = ?k \<and> ?u' < ?u)
k' = k

goal (1 subgoal):
 1. u' < u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u' < u

goal (1 subgoal):
 1. k' = k \<Longrightarrow> \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u' < u
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
u' < u

goal (1 subgoal):
 1. \<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
apply (rule_tac x=q in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u' < u \<Longrightarrow> \<exists>ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
apply (rule_tac x=ts in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u' < u \<Longrightarrow> \<exists>u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
apply (rule_tac x=u' in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u' < u \<Longrightarrow> p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
using final_step 2
[PROOF STATE]
proof (prove)
using this:
p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
k' = k

goal (1 subgoal):
 1. u' < u \<Longrightarrow> p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u' < u; k' = k; p = q @ ts; indexlt k u' k u; is_continuation k u' q ts\<rbrakk> \<Longrightarrow> chars ts = []
[PROOF STEP]
using charslength_p is_continuation_empty_chars
[PROOF STATE]
proof (prove)
using this:
charslength p = k
\<lbrakk>is_continuation ?k ?u ?q ?ts; charslength (?q @ ?ts) = ?k\<rbrakk> \<Longrightarrow> chars ?ts = []

goal (1 subgoal):
 1. \<lbrakk>u' < u; k' = k; p = q @ ts; indexlt k u' k u; is_continuation k u' q ts\<rbrakk> \<Longrightarrow> chars ts = []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
obtain q ts u' where
      p_split: "p = q@ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts"
[PROOF STATE]
proof (prove)
using this:
\<exists>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts

goal (1 subgoal):
 1. (\<And>q ts u'. p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
[PROOF STEP]
have "\<exists> u''. u' \<le> u'' \<and> Suc u'' = u"
[PROOF STATE]
proof (prove)
using this:
p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts

goal (1 subgoal):
 1. \<exists>u''\<ge>u'. Suc u'' = u
[PROOF STEP]
by (auto, arith)
[PROOF STATE]
proof (state)
this:
\<exists>u''\<ge>u'. Suc u'' = u

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>u''\<ge>u'. Suc u'' = u
[PROOF STEP]
obtain u'' where u'': " u' \<le> u'' \<and> Suc u'' = u"
[PROOF STATE]
proof (prove)
using this:
\<exists>u''\<ge>u'. Suc u'' = u

goal (1 subgoal):
 1. (\<And>u''. u' \<le> u'' \<and> Suc u'' = u \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u' \<le> u'' \<and> Suc u'' = u

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
with p_split
[PROOF STATE]
proof (chain)
picking this:
p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
u' \<le> u'' \<and> Suc u'' = u
[PROOF STEP]
have cont_u'': "is_continuation k u'' q ts"
[PROOF STATE]
proof (prove)
using this:
p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
u' \<le> u'' \<and> Suc u'' = u

goal (1 subgoal):
 1. is_continuation k u'' q ts
[PROOF STEP]
using is_continuation_increase_u
[PROOF STATE]
proof (prove)
using this:
p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
u' \<le> u'' \<and> Suc u'' = u
\<lbrakk>is_continuation ?k ?u ?q ?ts; ?u \<le> ?v\<rbrakk> \<Longrightarrow> is_continuation ?k ?v ?q ?ts

goal (1 subgoal):
 1. is_continuation k u'' q ts
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_continuation k u'' q ts

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have admissible: "admissible (p@[tok])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admissible (p @ [tok])
[PROOF STEP]
apply (simp add: tok)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admissible (p @ [(t, c)])
[PROOF STEP]
apply (rule_tac pvalid_next_terminal_admissible[where x=y])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. pvalid p y
 2. next_symbol y = Some t
 3. is_terminal t
[PROOF STEP]
apply (simp add: p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. next_symbol y = Some t
 2. is_terminal t
[PROOF STEP]
apply (simp add: x_is_scan)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_terminal t
[PROOF STEP]
using \<Z>_wellformed tok tok_dom wellformed_token_def
[PROOF STATE]
proof (prove)
using this:
?t \<in> \<Z> ?k ?u \<Longrightarrow> wellformed_token ?t
tok = (t, c)
tok \<in> \<Z> k u
wellformed_token ?t = is_terminal (terminal_of_token ?t)

goal (1 subgoal):
 1. is_terminal t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
admissible (p @ [tok])

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have "is_continuation k u'' q (ts@[tok])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_continuation k u'' q (ts @ [tok])
[PROOF STEP]
apply (rule is_continuation_continue)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. is_continuation k u'' q ts
 2. charslength ts = 0
 3. tok \<in> \<Z> k (Suc u'')
 4. admissible (q @ ts @ [tok])
[PROOF STEP]
apply (simp add: cont_u'')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. charslength ts = 0
 2. tok \<in> \<Z> k (Suc u'')
 3. admissible (q @ ts @ [tok])
[PROOF STEP]
using p_split
[PROOF STATE]
proof (prove)
using this:
p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts

goal (3 subgoals):
 1. charslength ts = 0
 2. tok \<in> \<Z> k (Suc u'')
 3. admissible (q @ ts @ [tok])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. tok \<in> \<Z> k (Suc u'')
 2. admissible (q @ ts @ [tok])
[PROOF STEP]
using u'' tok_dom
[PROOF STATE]
proof (prove)
using this:
u' \<le> u'' \<and> Suc u'' = u
tok \<in> \<Z> k u

goal (2 subgoals):
 1. tok \<in> \<Z> k (Suc u'')
 2. admissible (q @ ts @ [tok])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admissible (q @ ts @ [tok])
[PROOF STEP]
using admissible p_split
[PROOF STATE]
proof (prove)
using this:
admissible (p @ [tok])
p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts

goal (1 subgoal):
 1. admissible (q @ ts @ [tok])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_continuation k u'' q (ts @ [tok])

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
with p_split u''
[PROOF STATE]
proof (chain)
picking this:
p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
u' \<le> u'' \<and> Suc u'' = u
is_continuation k u'' q (ts @ [tok])
[PROOF STEP]
have ptok_dom: "p@[tok] \<in> \<P> k u"
[PROOF STATE]
proof (prove)
using this:
p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
u' \<le> u'' \<and> Suc u'' = u
is_continuation k u'' q (ts @ [tok])

goal (1 subgoal):
 1. p @ [tok] \<in> \<P> k u
[PROOF STEP]
using append_assoc is_continuation_in_\<P>
[PROOF STATE]
proof (prove)
using this:
p = q @ ts \<and> u' < u \<and> charslength ts = 0 \<and> is_continuation k u' q ts
u' \<le> u'' \<and> Suc u'' = u
is_continuation k u'' q (ts @ [tok])
(?xs @ ?ys) @ ?zs = ?xs @ ?ys @ ?zs
is_continuation ?k ?u ?p ?ts \<Longrightarrow> ?p @ ?ts \<in> \<P> ?k (Suc ?u)

goal (1 subgoal):
 1. p @ [tok] \<in> \<P> k u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p @ [tok] \<in> \<P> k u

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

goal (1 subgoal):
 1. (\<And>i \<gamma>. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> charslength p = item_end y \<and> charslength (take i p) = item_origin y \<and> is_derivation (terminals (take i p) @ [item_nonterminal y] @ \<gamma>) \<and> derives (item_\<alpha> y) (terminals (drop i p)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pvalid_def
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u \<and> pvalid p y
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>i \<gamma>. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> charslength p = item_end y \<and> charslength (take i p) = item_origin y \<and> is_derivation (terminals (take i p) @ [item_nonterminal y] @ \<gamma>) \<and> derives (item_\<alpha> y) (terminals (drop i p)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> charslength p = item_end y \<and> charslength (take i p) = item_origin y \<and> is_derivation (terminals (take i p) @ [item_nonterminal y] @ \<gamma>) \<and> derives (item_\<alpha> y) (terminals (drop i p))

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have clen_ptok: "k + length c = charslength (p@[tok])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k + length c = charslength (p @ [tok])
[PROOF STEP]
using charslength_p tok
[PROOF STATE]
proof (prove)
using this:
charslength p = k
tok = (t, c)

goal (1 subgoal):
 1. k + length c = charslength (p @ [tok])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k + length c = charslength (p @ [tok])

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
from ptok_dom
[PROOF STATE]
proof (chain)
picking this:
p @ [tok] \<in> \<P> k u
[PROOF STEP]
have ptok_doc_tokens: "doc_tokens (p@[tok])"
[PROOF STATE]
proof (prove)
using this:
p @ [tok] \<in> \<P> k u

goal (1 subgoal):
 1. doc_tokens (p @ [tok])
[PROOF STEP]
using \<PP>_are_doc_tokens \<PP>_covers_\<P> rev_subsetD
[PROOF STATE]
proof (prove)
using this:
p @ [tok] \<in> \<P> k u
?p \<in> \<PP> \<Longrightarrow> doc_tokens ?p
\<P> ?k ?u \<subseteq> \<PP>
\<lbrakk>?c \<in> ?A; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> ?c \<in> ?B

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

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<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: x_is_scan)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_item (inc_item y (k + length c))
[PROOF STEP]
apply (rule_tac wellformed_inc_item)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. wellformed_item y
 2. next_symbol y = Some ?s2
 3. k + length c \<le> length Doc
 4. item_end y \<le> k + length c
[PROOF STEP]
apply (simp add: valid)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. next_symbol y = Some ?s2
 2. k + length c \<le> length Doc
 3. item_end y \<le> k + length c
[PROOF STEP]
apply (simp add: x_is_scan)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. k + length c \<le> length Doc
 2. item_end y \<le> k + length c
[PROOF STEP]
apply (simp only: clen_ptok)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. charslength (p @ [tok]) \<le> length Doc
 2. item_end y \<le> k + length c
[PROOF STEP]
using ptok_doc_tokens charslength.simps doc_tokens_length
[PROOF STATE]
proof (prove)
using this:
doc_tokens (p @ [tok])
charslength ?cs = length (chars ?cs)
doc_tokens ?p \<Longrightarrow> length (chars ?p) \<le> length Doc

goal (2 subgoals):
 1. charslength (p @ [tok]) \<le> length Doc
 2. item_end y \<le> k + length c
[PROOF STEP]
apply presburger
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_end y \<le> k + length c
[PROOF STEP]
apply (simp only: clen_ptok)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_end y \<le> charslength (p @ [tok])
[PROOF STEP]
using valid
[PROOF STATE]
proof (prove)
using this:
wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> charslength p = item_end y \<and> charslength (take i p) = item_origin y \<and> is_derivation (terminals (take i p) @ [item_nonterminal y] @ \<gamma>) \<and> derives (item_\<alpha> y) (terminals (drop i p))

goal (1 subgoal):
 1. item_end y \<le> charslength (p @ [tok])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wellformed_item x

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
have "pvalid (p@[tok]) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pvalid (p @ [tok]) x
[PROOF STEP]
apply (auto simp only: pvalid_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u \<gamma>. wellformed_tokens (p @ [tok]) \<and> wellformed_item x \<and> u \<le> length (p @ [tok]) \<and> charslength (p @ [tok]) = item_end x \<and> charslength (take u (p @ [tok])) = item_origin x \<and> is_derivation (terminals (take u (p @ [tok])) @ [item_nonterminal x] @ \<gamma>) \<and> derives (item_\<alpha> x) (terminals (drop u (p @ [tok])))
[PROOF STEP]
apply (rule_tac x=i in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<gamma>. wellformed_tokens (p @ [tok]) \<and> wellformed_item x \<and> i \<le> length (p @ [tok]) \<and> charslength (p @ [tok]) = item_end x \<and> charslength (take i (p @ [tok])) = item_origin x \<and> is_derivation (terminals (take i (p @ [tok])) @ [item_nonterminal x] @ \<gamma>) \<and> derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
apply (rule_tac x=\<gamma> in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_tokens (p @ [tok]) \<and> wellformed_item x \<and> i \<le> length (p @ [tok]) \<and> charslength (p @ [tok]) = item_end x \<and> charslength (take i (p @ [tok])) = item_origin x \<and> is_derivation (terminals (take i (p @ [tok])) @ [item_nonterminal x] @ \<gamma>) \<and> derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
apply (auto simp only:)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. wellformed_tokens (p @ [tok])
 2. wellformed_item x
 3. i \<le> length (p @ [tok])
 4. charslength (p @ [tok]) = item_end x
 5. charslength (take i (p @ [tok])) = item_origin x
 6. is_derivation (terminals (take i (p @ [tok])) @ [item_nonterminal x] @ \<gamma>)
 7. derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
using ptok_dom admissible admissible_wellformed_tokens
[PROOF STATE]
proof (prove)
using this:
p @ [tok] \<in> \<P> k u
admissible (p @ [tok])
admissible ?p \<Longrightarrow> wellformed_tokens ?p

goal (7 subgoals):
 1. wellformed_tokens (p @ [tok])
 2. wellformed_item x
 3. i \<le> length (p @ [tok])
 4. charslength (p @ [tok]) = item_end x
 5. charslength (take i (p @ [tok])) = item_origin x
 6. is_derivation (terminals (take i (p @ [tok])) @ [item_nonterminal x] @ \<gamma>)
 7. derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. wellformed_item x
 2. i \<le> length (p @ [tok])
 3. charslength (p @ [tok]) = item_end x
 4. charslength (take i (p @ [tok])) = item_origin x
 5. is_derivation (terminals (take i (p @ [tok])) @ [item_nonterminal x] @ \<gamma>)
 6. derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
apply (simp add: wellformed_x)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. i \<le> length (p @ [tok])
 2. charslength (p @ [tok]) = item_end x
 3. charslength (take i (p @ [tok])) = item_origin x
 4. is_derivation (terminals (take i (p @ [tok])) @ [item_nonterminal x] @ \<gamma>)
 5. derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
using valid
[PROOF STATE]
proof (prove)
using this:
wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> charslength p = item_end y \<and> charslength (take i p) = item_origin y \<and> is_derivation (terminals (take i p) @ [item_nonterminal y] @ \<gamma>) \<and> derives (item_\<alpha> y) (terminals (drop i p))

goal (5 subgoals):
 1. i \<le> length (p @ [tok])
 2. charslength (p @ [tok]) = item_end x
 3. charslength (take i (p @ [tok])) = item_origin x
 4. is_derivation (terminals (take i (p @ [tok])) @ [item_nonterminal x] @ \<gamma>)
 5. derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. charslength (p @ [tok]) = item_end x
 2. charslength (take i (p @ [tok])) = item_origin x
 3. is_derivation (terminals (take i (p @ [tok])) @ [item_nonterminal x] @ \<gamma>)
 4. derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
apply (simp add: x_is_scan clen_ptok)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. charslength (take i (p @ [tok])) = item_origin x
 2. is_derivation (terminals (take i (p @ [tok])) @ [item_nonterminal x] @ \<gamma>)
 3. derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
using valid
[PROOF STATE]
proof (prove)
using this:
wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> charslength p = item_end y \<and> charslength (take i p) = item_origin y \<and> is_derivation (terminals (take i p) @ [item_nonterminal y] @ \<gamma>) \<and> derives (item_\<alpha> y) (terminals (drop i p))

goal (3 subgoals):
 1. charslength (take i (p @ [tok])) = item_origin x
 2. is_derivation (terminals (take i (p @ [tok])) @ [item_nonterminal x] @ \<gamma>)
 3. derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
apply (simp add: x_is_scan)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. is_derivation (terminals (take i (p @ [tok])) @ [item_nonterminal x] @ \<gamma>)
 2. derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
using valid
[PROOF STATE]
proof (prove)
using this:
wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> charslength p = item_end y \<and> charslength (take i p) = item_origin y \<and> is_derivation (terminals (take i p) @ [item_nonterminal y] @ \<gamma>) \<and> derives (item_\<alpha> y) (terminals (drop i p))

goal (2 subgoals):
 1. is_derivation (terminals (take i (p @ [tok])) @ [item_nonterminal x] @ \<gamma>)
 2. derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
apply (simp add: x_is_scan)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
using valid
[PROOF STATE]
proof (prove)
using this:
wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> charslength p = item_end y \<and> charslength (take i p) = item_origin y \<and> is_derivation (terminals (take i p) @ [item_nonterminal y] @ \<gamma>) \<and> derives (item_\<alpha> y) (terminals (drop i p))

goal (1 subgoal):
 1. derives (item_\<alpha> x) (terminals (drop i (p @ [tok])))
[PROOF STEP]
apply (simp add: x_is_scan)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> derives (item_\<alpha> (inc_item y (k + length c))) (drop i (terminals p) @ [terminal_of_token tok])
[PROOF STEP]
apply (subst item_\<alpha>_of_inc_item)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> wellformed_item y
 2. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> next_symbol y = Some ?s22
 3. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> derives (item_\<alpha> y @ [?s22]) (drop i (terminals p) @ [terminal_of_token tok])
[PROOF STEP]
using valid
[PROOF STATE]
proof (prove)
using this:
wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> charslength p = item_end y \<and> charslength (take i p) = item_origin y \<and> is_derivation (terminals (take i p) @ [item_nonterminal y] @ \<gamma>) \<and> derives (item_\<alpha> y) (terminals (drop i p))

goal (3 subgoals):
 1. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> wellformed_item y
 2. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> next_symbol y = Some ?s22
 3. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> derives (item_\<alpha> y @ [?s22]) (drop i (terminals p) @ [terminal_of_token tok])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> next_symbol y = Some ?s22
 2. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> derives (item_\<alpha> y @ [?s22]) (drop i (terminals p) @ [terminal_of_token tok])
[PROOF STEP]
using x_is_scan
[PROOF STATE]
proof (prove)
using this:
x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t

goal (2 subgoals):
 1. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> next_symbol y = Some ?s22
 2. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> derives (item_\<alpha> y @ [?s22]) (drop i (terminals p) @ [terminal_of_token tok])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> derives (item_\<alpha> y @ [t]) (drop i (terminals p) @ [terminal_of_token tok])
[PROOF STEP]
apply (rule_tac derives_append)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> derives (item_\<alpha> y) (drop i (terminals p))
 2. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> derives [t] [terminal_of_token tok]
 3. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> is_sentence (item_\<alpha> y)
 4. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> is_sentence [t]
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> derives [t] [terminal_of_token tok]
 2. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> is_sentence (item_\<alpha> y)
 3. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> is_sentence [t]
[PROOF STEP]
apply (simp add: tok)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> is_sentence (item_\<alpha> y)
 2. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> is_sentence [t]
[PROOF STEP]
using is_sentence_item_\<alpha>
[PROOF STATE]
proof (prove)
using this:
wellformed_item ?x \<Longrightarrow> is_sentence (item_\<alpha> ?x)

goal (2 subgoals):
 1. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> is_sentence (item_\<alpha> y)
 2. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> is_sentence [t]
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_tokens p \<and> wellformed_item y \<and> i \<le> length p \<and> length (chars p) = item_end y \<and> length (chars (take i p)) = item_origin y \<and> is_derivation (take i (terminals p) @ item_nonterminal y # \<gamma>) \<and> derives (item_\<alpha> y) (drop i (terminals p)) \<Longrightarrow> is_sentence [t]
[PROOF STEP]
by (meson pvalid_next_symbol_derivable LocalLexing_axioms is_derivation_is_sentence
          is_sentence_concat p x_is_scan)
[PROOF STATE]
proof (state)
this:
pvalid (p @ [tok]) x

goal (1 subgoal):
 1. 0 < u \<and> (\<exists>y t c. x = inc_item y (k + length c) \<and> y \<in> bin I k \<and> (t, c) \<in> T \<and> next_symbol y = Some t) \<Longrightarrow> x \<in> Gen (\<P> k u)
[PROOF STEP]
with ptok_dom
[PROOF STATE]
proof (chain)
picking this:
p @ [tok] \<in> \<P> k u
pvalid (p @ [tok]) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p @ [tok] \<in> \<P> k u
pvalid (p @ [tok]) 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:
p @ [tok] \<in> \<P> k u
pvalid (p @ [tok]) 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 Scan_subset_Gen:
  assumes I_in_Gen: "I \<subseteq> Gen (\<P> k u)"
  assumes k: "k \<le> length Doc"
  assumes T: "T \<subseteq> \<Z> k u"
  shows "Scan T k I \<subseteq> Gen (\<P> k u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Scan T k I \<subseteq> Gen (\<P> k u)
[PROOF STEP]
using I_in_Gen Scan_elem_in_Gen T k
[PROOF STATE]
proof (prove)
using this:
I \<subseteq> Gen (\<P> k u)
\<lbrakk>?I \<subseteq> Gen (\<P> ?k ?u); ?k \<le> length Doc; ?T \<subseteq> \<Z> ?k ?u; ?x \<in> Scan ?T ?k ?I\<rbrakk> \<Longrightarrow> ?x \<in> Gen (\<P> ?k ?u)
T \<subseteq> \<Z> k u
k \<le> length Doc

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


[STATEMENT]
theorem thmD5:
  assumes I: "I \<subseteq> Gen (\<P> k u)"
  assumes k: "k \<le> length Doc"
  assumes T: "T \<subseteq> \<Z> k u"
  shows "\<pi> k T I \<subseteq> Gen (\<P> k u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> k T I \<subseteq> Gen (\<P> k u)
[PROOF STEP]
apply (simp add: \<pi>_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit (\<lambda>I. Scan T k (Complete k (Predict k I))) I \<subseteq> Gen (\<P> k u)
[PROOF STEP]
apply (rule_tac limit_upperbound)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>I. I \<subseteq> Gen (\<P> k u) \<Longrightarrow> Scan T k (Complete k (Predict k I)) \<subseteq> Gen (\<P> k u)
 2. I \<subseteq> Gen (\<P> k u)
[PROOF STEP]
using I k T Predict_subset_Gen Complete_subset_Gen Scan_subset_Gen
[PROOF STATE]
proof (prove)
using this:
I \<subseteq> Gen (\<P> k u)
k \<le> length Doc
T \<subseteq> \<Z> k u
\<lbrakk>?I \<subseteq> Gen ?P; ?k \<le> length Doc\<rbrakk> \<Longrightarrow> Predict ?k ?I \<subseteq> Gen ?P
\<lbrakk>?I \<subseteq> Gen (\<P> ?k ?u); ?k \<le> length Doc\<rbrakk> \<Longrightarrow> Complete ?k ?I \<subseteq> Gen (\<P> ?k ?u)
\<lbrakk>?I \<subseteq> Gen (\<P> ?k ?u); ?k \<le> length Doc; ?T \<subseteq> \<Z> ?k ?u\<rbrakk> \<Longrightarrow> Scan ?T ?k ?I \<subseteq> Gen (\<P> ?k ?u)

goal (2 subgoals):
 1. \<And>I. I \<subseteq> Gen (\<P> k u) \<Longrightarrow> Scan T k (Complete k (Predict k I)) \<subseteq> Gen (\<P> k u)
 2. I \<subseteq> Gen (\<P> k u)
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<subseteq> Gen (\<P> k u)
[PROOF STEP]
by (simp add: I)


[STATEMENT]
lemma bot_Boolean_def : "(bot::('\<AA>)Boolean) = (\<lambda> \<tau>. \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UML_Types.bot_class.bot = Map.empty
[PROOF STEP]
by(simp add: bot_fun_def bot_option_def)


[STATEMENT]
lemma null_Boolean_def : "(null::('\<AA>)Boolean) = (\<lambda> \<tau>. \<lfloor>\<bottom>\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. null = (\<lambda>\<tau>. \<lfloor>\<bottom>\<rfloor>)
[PROOF STEP]
by(simp add: null_fun_def null_option_def bot_option_def)


[STATEMENT]
lemma bool_split_0: "X \<tau> = invalid \<tau> \<or> X \<tau> = null \<tau> \<or>
                   X \<tau> = true \<tau>    \<or> X \<tau> = false \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<tau> = invalid \<tau> \<or> X \<tau> = null \<tau> \<or> X \<tau> = true \<tau> \<or> X \<tau> = false \<tau>
[PROOF STEP]
apply(simp add: invalid_def null_def true_def false_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<tau> = UML_Types.bot_class.bot \<or> X \<tau> = null \<tau> \<or> X \<tau> = \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<or> X \<tau> = \<lfloor>\<lfloor>False\<rfloor>\<rfloor>
[PROOF STEP]
apply(case_tac "X \<tau>",simp_all add: null_fun_def null_option_def bot_option_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. X \<tau> = \<lfloor>a\<rfloor> \<Longrightarrow> a = \<bottom> \<or> a = \<lfloor>True\<rfloor> \<or> a = \<lfloor>False\<rfloor>
[PROOF STEP]
apply(case_tac "a",simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>X \<tau> = \<lfloor>a\<rfloor>; a = \<lfloor>aa\<rfloor>\<rbrakk> \<Longrightarrow> a = \<bottom> \<or> a = \<lfloor>True\<rfloor> \<or> a = \<lfloor>False\<rfloor>
[PROOF STEP]
apply(case_tac "aa",simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>X \<tau> = \<lfloor>a\<rfloor>; a = \<lfloor>aa\<rfloor>; \<not> aa\<rbrakk> \<Longrightarrow> a = \<bottom> \<or> a = \<lfloor>True\<rfloor> \<or> a = \<lfloor>False\<rfloor>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]: "false (a, b) = \<lfloor>\<lfloor>False\<rfloor>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. false (a, b) = \<lfloor>\<lfloor>False\<rfloor>\<rfloor>
[PROOF STEP]
by(simp add:false_def)


[STATEMENT]
lemma [simp]: "true (a, b) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. true (a, b) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor>
[PROOF STEP]
by(simp add:true_def)


[STATEMENT]
lemma textbook_true: "I\<lbrakk>true\<rbrakk> \<tau> = \<lfloor>\<lfloor>True\<rfloor>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I\<lbrakk>true\<rbrakk> \<tau> = \<lfloor>\<lfloor>True\<rfloor>\<rfloor>
[PROOF STEP]
by(simp add: Sem_def true_def)


[STATEMENT]
lemma textbook_false: "I\<lbrakk>false\<rbrakk> \<tau> = \<lfloor>\<lfloor>False\<rfloor>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I\<lbrakk>false\<rbrakk> \<tau> = \<lfloor>\<lfloor>False\<rfloor>\<rfloor>
[PROOF STEP]
by(simp add: Sem_def false_def)


[STATEMENT]
lemma valid1[simp]: "\<upsilon> invalid = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> invalid = false
[PROOF STEP]
by(rule ext,simp add: valid_def bot_fun_def bot_option_def
                        invalid_def true_def false_def)


[STATEMENT]
lemma valid2[simp]: "\<upsilon> null = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> null = true
[PROOF STEP]
by(rule ext,simp add: valid_def bot_fun_def bot_option_def null_is_valid
                        null_fun_def invalid_def true_def false_def)


[STATEMENT]
lemma valid3[simp]: "\<upsilon> true = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> true = true
[PROOF STEP]
by(rule ext,simp add: valid_def bot_fun_def bot_option_def null_is_valid
                        null_fun_def invalid_def true_def false_def)


[STATEMENT]
lemma valid4[simp]: "\<upsilon> false = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> false = true
[PROOF STEP]
by(rule ext,simp add: valid_def bot_fun_def bot_option_def null_is_valid
                        null_fun_def invalid_def true_def false_def)


[STATEMENT]
lemma cp_valid: "(\<upsilon> X) \<tau> = (\<upsilon> (\<lambda> _. X \<tau>)) \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<upsilon> X) \<tau> = (\<upsilon> (\<lambda>_. X \<tau>)) \<tau>
[PROOF STEP]
by(simp add: valid_def)


[STATEMENT]
lemma defined1[simp]: "\<delta> invalid = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> invalid = false
[PROOF STEP]
by(rule ext,simp add: defined_def bot_fun_def bot_option_def
                        null_def invalid_def true_def false_def)


[STATEMENT]
lemma defined2[simp]: "\<delta> null = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> null = false
[PROOF STEP]
by(rule ext,simp add: defined_def bot_fun_def bot_option_def
                        null_def null_option_def null_fun_def invalid_def true_def false_def)


[STATEMENT]
lemma defined3[simp]: "\<delta> true = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> true = true
[PROOF STEP]
by(rule ext,simp add: defined_def bot_fun_def bot_option_def null_is_valid null_option_def
                        null_fun_def invalid_def true_def false_def)


[STATEMENT]
lemma defined4[simp]: "\<delta> false = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> false = true
[PROOF STEP]
by(rule ext,simp add: defined_def bot_fun_def bot_option_def null_is_valid null_option_def
                        null_fun_def invalid_def true_def false_def)


[STATEMENT]
lemma defined5[simp]: "\<delta> \<delta> X = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> \<delta> X = true
[PROOF STEP]
by(rule ext,
     auto simp:           defined_def true_def false_def
                bot_fun_def bot_option_def null_option_def null_fun_def)


[STATEMENT]
lemma defined6[simp]: "\<delta> \<upsilon> X = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> \<upsilon> X = true
[PROOF STEP]
by(rule ext,
     auto simp: valid_def defined_def true_def false_def
                bot_fun_def bot_option_def null_option_def null_fun_def)


[STATEMENT]
lemma valid5[simp]: "\<upsilon> \<upsilon> X = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> \<upsilon> X = true
[PROOF STEP]
by(rule ext,
     auto simp: valid_def             true_def false_def
                bot_fun_def bot_option_def null_option_def null_fun_def)


[STATEMENT]
lemma valid6[simp]: "\<upsilon> \<delta> X = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> \<delta> X = true
[PROOF STEP]
by(rule ext,
     auto simp: valid_def defined_def true_def false_def
                bot_fun_def bot_option_def null_option_def null_fun_def)


[STATEMENT]
lemma cp_defined:"(\<delta> X)\<tau> = (\<delta> (\<lambda> _. X \<tau>)) \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<delta> X) \<tau> = (\<delta> (\<lambda>_. X \<tau>)) \<tau>
[PROOF STEP]
by(simp add: defined_def)


[STATEMENT]
lemma textbook_defined: "I\<lbrakk>\<delta>(X)\<rbrakk> \<tau> = (if I\<lbrakk>X\<rbrakk> \<tau> = I\<lbrakk>bot\<rbrakk> \<tau>  \<or> I\<lbrakk>X\<rbrakk> \<tau> = I\<lbrakk>null\<rbrakk> \<tau>
                                     then I\<lbrakk>false\<rbrakk> \<tau>
                                     else I\<lbrakk>true\<rbrakk> \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I\<lbrakk>\<delta> X\<rbrakk> \<tau> = (if I\<lbrakk>X\<rbrakk> \<tau> = I\<lbrakk>UML_Types.bot_class.bot\<rbrakk> \<tau> \<or> I\<lbrakk>X\<rbrakk> \<tau> = I\<lbrakk>null\<rbrakk> \<tau> then I\<lbrakk>false\<rbrakk> \<tau> else I\<lbrakk>true\<rbrakk> \<tau>)
[PROOF STEP]
by(simp add: Sem_def defined_def)


[STATEMENT]
lemma textbook_valid: "I\<lbrakk>\<upsilon>(X)\<rbrakk> \<tau> = (if I\<lbrakk>X\<rbrakk> \<tau> = I\<lbrakk>bot\<rbrakk> \<tau>
                                   then I\<lbrakk>false\<rbrakk> \<tau>
                                   else I\<lbrakk>true\<rbrakk> \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I\<lbrakk>\<upsilon> X\<rbrakk> \<tau> = (if I\<lbrakk>X\<rbrakk> \<tau> = I\<lbrakk>UML_Types.bot_class.bot\<rbrakk> \<tau> then I\<lbrakk>false\<rbrakk> \<tau> else I\<lbrakk>true\<rbrakk> \<tau>)
[PROOF STEP]
by(simp add: Sem_def valid_def)


[STATEMENT]
lemma [simp,code_unfold]: "(true \<triangleq> false) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (true \<triangleq> false) = false
[PROOF STEP]
by(rule ext, auto simp: StrongEq_def)


[STATEMENT]
lemma [simp,code_unfold]: "(false \<triangleq> true) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (false \<triangleq> true) = false
[PROOF STEP]
by(rule ext, auto simp: StrongEq_def)


[STATEMENT]
lemma StrongEq_refl [simp]: "(X \<triangleq> X) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X \<triangleq> X) = true
[PROOF STEP]
by(rule ext, simp add: null_def invalid_def true_def false_def StrongEq_def)


[STATEMENT]
lemma StrongEq_sym: "(X \<triangleq> Y) = (Y \<triangleq> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X \<triangleq> Y) = (Y \<triangleq> X)
[PROOF STEP]
by(rule ext, simp add: eq_sym_conv invalid_def true_def false_def StrongEq_def)


[STATEMENT]
lemma StrongEq_trans_strong [simp]:
  assumes A: "(X \<triangleq> Y) = true"
  and     B: "(Y \<triangleq> Z) = true"
  shows   "(X \<triangleq> Z) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X \<triangleq> Z) = true
[PROOF STEP]
apply(insert A B)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(X \<triangleq> Y) = true; (Y \<triangleq> Z) = true\<rbrakk> \<Longrightarrow> (X \<triangleq> Z) = true
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(X \<triangleq> Y) = true; (Y \<triangleq> Z) = true\<rbrakk> \<Longrightarrow> (X \<triangleq> Z) x = true x
[PROOF STEP]
apply(simp add: null_def invalid_def true_def false_def StrongEq_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(\<lambda>\<tau>. \<lfloor>\<lfloor>X \<tau> = Y \<tau>\<rfloor>\<rfloor>) = (\<lambda>\<tau>. \<lfloor>\<lfloor>True\<rfloor>\<rfloor>); (\<lambda>\<tau>. \<lfloor>\<lfloor>Y \<tau> = Z \<tau>\<rfloor>\<rfloor>) = (\<lambda>\<tau>. \<lfloor>\<lfloor>True\<rfloor>\<rfloor>)\<rbrakk> \<Longrightarrow> X x = Z x
[PROOF STEP]
apply(drule_tac x=x in fun_cong)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lfloor>\<lfloor>X x = Y x\<rfloor>\<rfloor> = \<lfloor>\<lfloor>True\<rfloor>\<rfloor>; \<lfloor>\<lfloor>Y x = Z x\<rfloor>\<rfloor> = \<lfloor>\<lfloor>True\<rfloor>\<rfloor>\<rbrakk> \<Longrightarrow> X x = Z x
[PROOF STEP]
by auto


[STATEMENT]
lemma StrongEq_subst :
  assumes cp: "\<And>X. P(X)\<tau> = P(\<lambda> _. X \<tau>)\<tau>"
  and     eq: "(X \<triangleq> Y)\<tau> = true \<tau>"
  shows   "(P X \<triangleq> P Y)\<tau> = true \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P X \<triangleq> P Y) \<tau> = true \<tau>
[PROOF STEP]
apply(insert cp eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>X. P X \<tau> = P (\<lambda>_. X \<tau>) \<tau>; (X \<triangleq> Y) \<tau> = true \<tau>\<rbrakk> \<Longrightarrow> (P X \<triangleq> P Y) \<tau> = true \<tau>
[PROOF STEP]
apply(simp add: null_def invalid_def true_def false_def StrongEq_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>X. P X \<tau> = P (\<lambda>_. X \<tau>) \<tau>; X \<tau> = Y \<tau>\<rbrakk> \<Longrightarrow> P X \<tau> = P Y \<tau>
[PROOF STEP]
apply(subst cp[of X])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>X. P X \<tau> = P (\<lambda>_. X \<tau>) \<tau>; X \<tau> = Y \<tau>\<rbrakk> \<Longrightarrow> P (\<lambda>_. X \<tau>) \<tau> = P Y \<tau>
[PROOF STEP]
apply(subst cp[of Y])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>X. P X \<tau> = P (\<lambda>_. X \<tau>) \<tau>; X \<tau> = Y \<tau>\<rbrakk> \<Longrightarrow> P (\<lambda>_. X \<tau>) \<tau> = P (\<lambda>_. Y \<tau>) \<tau>
[PROOF STEP]
by simp


[STATEMENT]
lemma defined7[simp]: "\<delta> (X \<triangleq> Y) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> (X \<triangleq> Y) = true
[PROOF STEP]
by(rule ext,
     auto simp: defined_def           true_def false_def StrongEq_def
                bot_fun_def bot_option_def null_option_def null_fun_def)


[STATEMENT]
lemma valid7[simp]: "\<upsilon> (X \<triangleq> Y) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> (X \<triangleq> Y) = true
[PROOF STEP]
by(rule ext,
     auto simp: valid_def true_def false_def StrongEq_def
                bot_fun_def bot_option_def null_option_def null_fun_def)


[STATEMENT]
lemma cp_StrongEq: "(X \<triangleq> Y) \<tau> = ((\<lambda> _. X \<tau>) \<triangleq> (\<lambda> _. Y \<tau>)) \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X \<triangleq> Y) \<tau> = ((\<lambda>_. X \<tau>) \<triangleq> (\<lambda>_. Y \<tau>)) \<tau>
[PROOF STEP]
by(simp add: StrongEq_def)


[STATEMENT]
lemma cp_OclNot: "(not X)\<tau> = (not (\<lambda> _. X \<tau>)) \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not X \<tau> = not (\<lambda>_. X \<tau>) \<tau>
[PROOF STEP]
by(simp add: OclNot_def)


[STATEMENT]
lemma OclNot1[simp]: "not invalid = invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not invalid = invalid
[PROOF STEP]
by(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def bot_option_def)


[STATEMENT]
lemma OclNot2[simp]: "not null = null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not null = null
[PROOF STEP]
by(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def
                        bot_option_def null_fun_def null_option_def )


[STATEMENT]
lemma OclNot3[simp]: "not true = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not true = false
[PROOF STEP]
by(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def)


[STATEMENT]
lemma OclNot4[simp]: "not false = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not false = true
[PROOF STEP]
by(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def)


[STATEMENT]
lemma OclNot_not[simp]: "not (not X) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not (not X) = X
[PROOF STEP]
apply(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (case case X x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>xa\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> xa\<rfloor>\<rfloor> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>xa\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> xa\<rfloor>\<rfloor>) = X x
[PROOF STEP]
apply(case_tac "X x", simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a. X x = \<lfloor>a\<rfloor> \<Longrightarrow> (case case a of \<bottom> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>x\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> x\<rfloor>\<rfloor> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>xa\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> xa\<rfloor>\<rfloor>) = \<lfloor>a\<rfloor>
[PROOF STEP]
apply(case_tac "a", simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma OclNot_inject: "\<And> x y. not x = not y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. not x = not y \<Longrightarrow> x = y
[PROOF STEP]
by(subst OclNot_not[THEN sym], simp)


[STATEMENT]
lemma textbook_OclNot:
     "I\<lbrakk>not(X)\<rbrakk> \<tau> =  (case I\<lbrakk>X\<rbrakk> \<tau> of   \<bottom>   \<Rightarrow> \<bottom>
                                 |  \<lfloor> \<bottom> \<rfloor> \<Rightarrow> \<lfloor> \<bottom> \<rfloor>
                                 | \<lfloor>\<lfloor> x \<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor> \<not> x \<rfloor>\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I\<lbrakk>not X\<rbrakk> \<tau> = (case I\<lbrakk>X\<rbrakk> \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>x\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> x\<rfloor>\<rfloor>)
[PROOF STEP]
by(simp add: Sem_def OclNot_def)


[STATEMENT]
lemma textbook_OclAnd:
     "I\<lbrakk>X and Y\<rbrakk> \<tau> = (case I\<lbrakk>X\<rbrakk> \<tau> of
                            \<bottom>  \<Rightarrow> (case I\<lbrakk>Y\<rbrakk> \<tau> of
                                             \<bottom> \<Rightarrow>  \<bottom>
                                          | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom>
                                          | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow>  \<bottom>
                                          | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow>  \<lfloor>\<lfloor>False\<rfloor>\<rfloor>)
                        | \<lfloor> \<bottom> \<rfloor> \<Rightarrow> (case I\<lbrakk>Y\<rbrakk> \<tau> of
                                             \<bottom> \<Rightarrow>  \<bottom>
                                          | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor>
                                          | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor>
                                          | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow>  \<lfloor>\<lfloor>False\<rfloor>\<rfloor>)
                        | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> (case I\<lbrakk>Y\<rbrakk> \<tau> of
                                             \<bottom> \<Rightarrow>  \<bottom>
                                          | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor>
                                          | \<lfloor>\<lfloor>y\<rfloor>\<rfloor> \<Rightarrow>  \<lfloor>\<lfloor>y\<rfloor>\<rfloor>)
                        | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow>  \<lfloor>\<lfloor> False \<rfloor>\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I\<lbrakk>X and Y\<rbrakk> \<tau> = (case I\<lbrakk>X\<rbrakk> \<tau> of \<bottom> \<Rightarrow> case I\<lbrakk>Y\<rbrakk> \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case I\<lbrakk>Y\<rbrakk> \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> case I\<lbrakk>Y\<rbrakk> \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>y\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>y\<rfloor>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>)
[PROOF STEP]
by(simp add: OclAnd_def Sem_def split: option.split bool.split)


[STATEMENT]
lemma cp_OclAnd:"(X and Y) \<tau> = ((\<lambda> _. X \<tau>) and (\<lambda> _. Y \<tau>)) \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X and Y) \<tau> = ((\<lambda>_. X \<tau>) and (\<lambda>_. Y \<tau>)) \<tau>
[PROOF STEP]
by(simp add: OclAnd_def)


[STATEMENT]
lemma cp_OclOr:"((X::('\<AA>)Boolean) or Y) \<tau> = ((\<lambda> _. X \<tau>) or (\<lambda> _. Y \<tau>)) \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X or Y) \<tau> = ((\<lambda>_. X \<tau>) or (\<lambda>_. Y \<tau>)) \<tau>
[PROOF STEP]
apply(simp add: OclOr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not (not X and not Y) \<tau> = not (not (\<lambda>_. X \<tau>) and not (\<lambda>_. Y \<tau>)) \<tau>
[PROOF STEP]
apply(subst cp_OclNot[of "not (\<lambda>_. X \<tau>) and not (\<lambda>_. Y \<tau>)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not (not X and not Y) \<tau> = not (\<lambda>_. (not (\<lambda>_. X \<tau>) and not (\<lambda>_. Y \<tau>)) \<tau>) \<tau>
[PROOF STEP]
apply(subst cp_OclAnd[of "not (\<lambda>_. X \<tau>)" "not (\<lambda>_. Y \<tau>)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not (not X and not Y) \<tau> = not (\<lambda>_. ((\<lambda>_. not (\<lambda>_. X \<tau>) \<tau>) and (\<lambda>_. not (\<lambda>_. Y \<tau>) \<tau>)) \<tau>) \<tau>
[PROOF STEP]
by(simp add: cp_OclNot[symmetric] cp_OclAnd[symmetric] )


[STATEMENT]
lemma cp_OclImplies:"(X implies Y) \<tau> = ((\<lambda> _. X \<tau>) implies (\<lambda> _. Y \<tau>)) \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X implies Y) \<tau> = ((\<lambda>_. X \<tau>) implies (\<lambda>_. Y \<tau>)) \<tau>
[PROOF STEP]
apply(simp add: OclImplies_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (not X or Y) \<tau> = (not (\<lambda>_. X \<tau>) or (\<lambda>_. Y \<tau>)) \<tau>
[PROOF STEP]
apply(subst cp_OclOr[of "not (\<lambda>_. X \<tau>)" "(\<lambda>_. Y \<tau>)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (not X or Y) \<tau> = ((\<lambda>_. not (\<lambda>_. X \<tau>) \<tau>) or (\<lambda>_. Y \<tau>)) \<tau>
[PROOF STEP]
by(simp add: cp_OclNot[symmetric] cp_OclOr[symmetric] )


[STATEMENT]
lemma OclAnd1[simp]: "(invalid and true) = invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (invalid and true) = invalid
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def)


[STATEMENT]
lemma OclAnd2[simp]: "(invalid and false) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (invalid and false) = false
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def)


[STATEMENT]
lemma OclAnd3[simp]: "(invalid and null) = invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (invalid and null) = invalid
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)


[STATEMENT]
lemma OclAnd4[simp]: "(invalid and invalid) = invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (invalid and invalid) = invalid
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def)


[STATEMENT]
lemma OclAnd5[simp]: "(null and true) = null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null and true) = null
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)


[STATEMENT]
lemma OclAnd6[simp]: "(null and false) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null and false) = false
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)


[STATEMENT]
lemma OclAnd7[simp]: "(null and null) = null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null and null) = null
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)


[STATEMENT]
lemma OclAnd8[simp]: "(null and invalid) = invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null and invalid) = invalid
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)


[STATEMENT]
lemma OclAnd9[simp]: "(false and true) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (false and true) = false
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)


[STATEMENT]
lemma OclAnd10[simp]: "(false and false) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (false and false) = false
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)


[STATEMENT]
lemma OclAnd11[simp]: "(false and null) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (false and null) = false
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)


[STATEMENT]
lemma OclAnd12[simp]: "(false and invalid) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (false and invalid) = false
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)


[STATEMENT]
lemma OclAnd13[simp]: "(true and true) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (true and true) = true
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)


[STATEMENT]
lemma OclAnd14[simp]: "(true and false) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (true and false) = false
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)


[STATEMENT]
lemma OclAnd16[simp]: "(true and invalid) = invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (true and invalid) = invalid
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)


[STATEMENT]
lemma OclAnd_idem[simp]: "(X and X) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X and X) = X
[PROOF STEP]
apply(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (case X x of \<bottom> \<Rightarrow> case X x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case X x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> X x | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = X x
[PROOF STEP]
apply(case_tac "X x", simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a. X x = \<lfloor>a\<rfloor> \<Longrightarrow> (case a of \<bottom> \<Rightarrow> case X x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>True\<rfloor> \<Rightarrow> X x | \<lfloor>False\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = \<lfloor>a\<rfloor>
[PROOF STEP]
apply(case_tac "a", simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a aa. \<lbrakk>X x = \<lfloor>\<lfloor>aa\<rfloor>\<rfloor>; a = \<lfloor>aa\<rfloor>\<rbrakk> \<Longrightarrow> (case aa of True \<Rightarrow> X x | False \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = \<lfloor>\<lfloor>aa\<rfloor>\<rfloor>
[PROOF STEP]
apply(case_tac "aa", simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma OclAnd_commute: "(X and Y) = (Y and X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X and Y) = (Y and X)
[PROOF STEP]
by(rule ext,auto simp:true_def false_def OclAnd_def invalid_def
                   split: option.split option.split_asm
                          bool.split bool.split_asm)


[STATEMENT]
lemma OclAnd_false1[simp]: "(false and X) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (false and X) = false
[PROOF STEP]
apply(rule ext, simp add: OclAnd_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (case false x of \<bottom> \<Rightarrow> case X x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case X x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> X x | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = false x
[PROOF STEP]
apply(auto simp:true_def false_def invalid_def
             split: option.split option.split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma OclAnd_false2[simp]: "(X and false) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X and false) = false
[PROOF STEP]
by(simp add: OclAnd_commute)


[STATEMENT]
lemma OclAnd_true1[simp]: "(true and X) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (true and X) = X
[PROOF STEP]
apply(rule ext, simp add: OclAnd_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (case true x of \<bottom> \<Rightarrow> case X x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case X x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> X x | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = X x
[PROOF STEP]
apply(auto simp:true_def false_def invalid_def
             split: option.split option.split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma OclAnd_true2[simp]: "(X and true) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X and true) = X
[PROOF STEP]
by(simp add: OclAnd_commute)


[STATEMENT]
lemma OclAnd_bot1[simp]: "\<And>\<tau>. X \<tau> \<noteq> false \<tau> \<Longrightarrow> (bot and X) \<tau> = bot \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. X \<tau> \<noteq> false \<tau> \<Longrightarrow> (UML_Types.bot_class.bot and X) \<tau> = UML_Types.bot_class.bot \<tau>
[PROOF STEP]
apply(simp add: OclAnd_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. X \<tau> \<noteq> false \<tau> \<Longrightarrow> (case UML_Types.bot_class.bot \<tau> of \<bottom> \<Rightarrow> case X \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case X \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> X \<tau> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = UML_Types.bot_class.bot \<tau>
[PROOF STEP]
apply(auto simp:true_def false_def bot_fun_def bot_option_def
             split: option.split option.split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma OclAnd_bot2[simp]: "\<And>\<tau>. X \<tau> \<noteq> false \<tau> \<Longrightarrow> (X and bot) \<tau> = bot \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. X \<tau> \<noteq> false \<tau> \<Longrightarrow> (X and UML_Types.bot_class.bot) \<tau> = UML_Types.bot_class.bot \<tau>
[PROOF STEP]
by(simp add: OclAnd_commute)


[STATEMENT]
lemma OclAnd_null1[simp]: "\<And>\<tau>. X \<tau> \<noteq> false \<tau> \<Longrightarrow> X \<tau> \<noteq> bot \<tau> \<Longrightarrow> (null and X) \<tau> = null \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. \<lbrakk>X \<tau> \<noteq> false \<tau>; X \<tau> \<noteq> UML_Types.bot_class.bot \<tau>\<rbrakk> \<Longrightarrow> (null and X) \<tau> = null \<tau>
[PROOF STEP]
apply(simp add: OclAnd_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. \<lbrakk>X \<tau> \<noteq> false \<tau>; X \<tau> \<noteq> UML_Types.bot_class.bot \<tau>\<rbrakk> \<Longrightarrow> (case null \<tau> of \<bottom> \<Rightarrow> case X \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case X \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> X \<tau> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = null \<tau>
[PROOF STEP]
apply(auto simp:true_def false_def bot_fun_def bot_option_def null_fun_def null_option_def
             split: option.split option.split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma OclAnd_assoc: "(X and (Y and Z)) = (X and Y and Z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X and (Y and Z)) = (X and Y and Z)
[PROOF STEP]
apply(rule ext, simp add: OclAnd_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (case X x of \<bottom> \<Rightarrow> case case Y x of \<bottom> \<Rightarrow> case Z x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case Z x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> Z x | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case case Y x of \<bottom> \<Rightarrow> case Z x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case Z x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> Z x | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> case Y x of \<bottom> \<Rightarrow> case Z x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case Z x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> Z x | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = (case case X x of \<bottom> \<Rightarrow> case Y x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case Y x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> Y x | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> of \<bottom> \<Rightarrow> case Z x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case Z x of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> Z x | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>)
[PROOF STEP]
apply(auto simp:true_def false_def null_def invalid_def
             split: option.split option.split_asm
                    bool.split bool.split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done