[STATEMENT]
lemma thmD2':
  assumes X: "is_terminal X"
  assumes p: "doc_tokens p"
  assumes pX: "(terminals p)@[X] \<in> \<L>\<^sub>P"
  shows "\<exists> x. pvalid p x \<and> next_symbol x = Some X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
doc_tokens p
[PROOF STEP]
have wellformed_p: "wellformed_tokens p"
[PROOF STATE]
proof (prove)
using this:
doc_tokens p

goal (1 subgoal):
 1. wellformed_tokens p
[PROOF STEP]
by (simp add: doc_tokens_def)
[PROOF STATE]
proof (state)
this:
wellformed_tokens p

goal (1 subgoal):
 1. \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
have "\<exists> \<omega>. leftderives [\<SS>] (((terminals p)@[X]) @ \<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<omega>. leftderives [\<SS>] ((terminals p @ [X]) @ \<omega>)
[PROOF STEP]
using \<L>\<^sub>P_leftderives pX
[PROOF STATE]
proof (prove)
using this:
?a \<in> \<L>\<^sub>P \<Longrightarrow> \<exists>b. leftderives [\<SS>] (?a @ b)
terminals p @ [X] \<in> \<L>\<^sub>P

goal (1 subgoal):
 1. \<exists>\<omega>. leftderives [\<SS>] ((terminals p @ [X]) @ \<omega>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<omega>. leftderives [\<SS>] ((terminals p @ [X]) @ \<omega>)

goal (1 subgoal):
 1. \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<omega>. leftderives [\<SS>] ((terminals p @ [X]) @ \<omega>)
[PROOF STEP]
obtain \<omega> where "leftderives [\<SS>] (((terminals p)@[X]) @ \<omega>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<omega>. leftderives [\<SS>] ((terminals p @ [X]) @ \<omega>)

goal (1 subgoal):
 1. (\<And>\<omega>. leftderives [\<SS>] ((terminals p @ [X]) @ \<omega>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
leftderives [\<SS>] ((terminals p @ [X]) @ \<omega>)

goal (1 subgoal):
 1. \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
leftderives [\<SS>] ((terminals p @ [X]) @ \<omega>)
[PROOF STEP]
have "\<exists> D. LeftDerivation [\<SS>] D (((terminals p)@[X]) @ \<omega>)"
[PROOF STATE]
proof (prove)
using this:
leftderives [\<SS>] ((terminals p @ [X]) @ \<omega>)

goal (1 subgoal):
 1. \<exists>D. LeftDerivation [\<SS>] D ((terminals p @ [X]) @ \<omega>)
[PROOF STEP]
using leftderives_implies_LeftDerivation
[PROOF STATE]
proof (prove)
using this:
leftderives [\<SS>] ((terminals p @ [X]) @ \<omega>)
leftderives ?a ?b \<Longrightarrow> \<exists>D. LeftDerivation ?a D ?b

goal (1 subgoal):
 1. \<exists>D. LeftDerivation [\<SS>] D ((terminals p @ [X]) @ \<omega>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>D. LeftDerivation [\<SS>] D ((terminals p @ [X]) @ \<omega>)

goal (1 subgoal):
 1. \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>D. LeftDerivation [\<SS>] D ((terminals p @ [X]) @ \<omega>)
[PROOF STEP]
obtain D where D: "LeftDerivation [\<SS>] D (((terminals p)@[X]) @ \<omega>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>D. LeftDerivation [\<SS>] D ((terminals p @ [X]) @ \<omega>)

goal (1 subgoal):
 1. (\<And>D. LeftDerivation [\<SS>] D ((terminals p @ [X]) @ \<omega>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
LeftDerivation [\<SS>] D ((terminals p @ [X]) @ \<omega>)

goal (1 subgoal):
 1. \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
let ?P = "\<lambda> k. (\<exists> a b. LeftDerivation [\<SS>] (take k D) (a@[X]@b) \<and> derives a (terminals p))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
have "?P (length D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a b. LeftDerivation [\<SS>] (take (length D) D) (a @ [X] @ b) \<and> derives a (terminals p)
[PROOF STEP]
apply (rule_tac x="terminals p" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b. LeftDerivation [\<SS>] (take (length D) D) (terminals p @ [X] @ b) \<and> derives (terminals p) (terminals p)
[PROOF STEP]
apply (rule_tac x="\<omega>" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LeftDerivation [\<SS>] (take (length D) D) (terminals p @ [X] @ \<omega>) \<and> derives (terminals p) (terminals p)
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
LeftDerivation [\<SS>] D ((terminals p @ [X]) @ \<omega>)

goal (1 subgoal):
 1. LeftDerivation [\<SS>] (take (length D) D) (terminals p @ [X] @ \<omega>) \<and> derives (terminals p) (terminals p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>a b. LeftDerivation [\<SS>] (take (length D) D) (a @ [X] @ b) \<and> derives a (terminals p)

goal (1 subgoal):
 1. \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b. LeftDerivation [\<SS>] (take (length D) D) (a @ [X] @ b) \<and> derives a (terminals p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. LeftDerivation [\<SS>] (take (length D) D) (a @ [X] @ b) \<and> derives a (terminals p)

goal (1 subgoal):
 1. \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
proof (induct rule: minimal_witness[where P="?P"])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
case (Minimal K)
[PROOF STATE]
proof (state)
this:
K \<le> length D
\<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p)
?k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take ?k D) (a @ [X] @ b) \<and> derives a (terminals p)

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
from Minimal(2)
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p)
[PROOF STEP]
obtain a b where
       aXb: "LeftDerivation [\<SS>] (take K D) (a @ [X] @ b)" and
       a: "derives a (terminals p)"
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p)

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>LeftDerivation [\<SS>] (take K D) (a @ [X] @ b); derives a (terminals p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
LeftDerivation [\<SS>] (take K D) (a @ [X] @ b)
derives a (terminals p)

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
have KD: "K > 0 \<and> length D > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < K \<and> 0 < length D
[PROOF STEP]
proof (cases "K = 0 \<or> length D = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. K = 0 \<or> length D = 0 \<Longrightarrow> 0 < K \<and> 0 < length D
 2. \<not> (K = 0 \<or> length D = 0) \<Longrightarrow> 0 < K \<and> 0 < length D
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
K = 0 \<or> length D = 0

goal (2 subgoals):
 1. K = 0 \<or> length D = 0 \<Longrightarrow> 0 < K \<and> 0 < length D
 2. \<not> (K = 0 \<or> length D = 0) \<Longrightarrow> 0 < K \<and> 0 < length D
[PROOF STEP]
hence "take K D = []"
[PROOF STATE]
proof (prove)
using this:
K = 0 \<or> length D = 0

goal (1 subgoal):
 1. take K D = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
take K D = []

goal (2 subgoals):
 1. K = 0 \<or> length D = 0 \<Longrightarrow> 0 < K \<and> 0 < length D
 2. \<not> (K = 0 \<or> length D = 0) \<Longrightarrow> 0 < K \<and> 0 < length D
[PROOF STEP]
with True aXb
[PROOF STATE]
proof (chain)
picking this:
K = 0 \<or> length D = 0
LeftDerivation [\<SS>] (take K D) (a @ [X] @ b)
take K D = []
[PROOF STEP]
have "[\<SS>] = a @ [X] @ b"
[PROOF STATE]
proof (prove)
using this:
K = 0 \<or> length D = 0
LeftDerivation [\<SS>] (take K D) (a @ [X] @ b)
take K D = []

goal (1 subgoal):
 1. [\<SS>] = a @ [X] @ b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[\<SS>] = a @ [X] @ b

goal (2 subgoals):
 1. K = 0 \<or> length D = 0 \<Longrightarrow> 0 < K \<and> 0 < length D
 2. \<not> (K = 0 \<or> length D = 0) \<Longrightarrow> 0 < K \<and> 0 < length D
[PROOF STEP]
hence "\<SS> = X"
[PROOF STATE]
proof (prove)
using this:
[\<SS>] = a @ [X] @ b

goal (1 subgoal):
 1. \<SS> = X
[PROOF STEP]
by (metis Nil_is_append_conv append_self_conv2 butlast.simps(2)
              butlast_append hd_append2 list.sel(1) not_Cons_self2)
[PROOF STATE]
proof (state)
this:
\<SS> = X

goal (2 subgoals):
 1. K = 0 \<or> length D = 0 \<Longrightarrow> 0 < K \<and> 0 < length D
 2. \<not> (K = 0 \<or> length D = 0) \<Longrightarrow> 0 < K \<and> 0 < length D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<SS> = X
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
\<SS> = X

goal (1 subgoal):
 1. False
[PROOF STEP]
using X is_nonterminal_startsymbol is_terminal_nonterminal
[PROOF STATE]
proof (prove)
using this:
\<SS> = X
is_terminal X
is_nonterminal \<SS>
\<lbrakk>is_terminal ?x; is_nonterminal ?x\<rbrakk> \<Longrightarrow> False

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

goal (2 subgoals):
 1. K = 0 \<or> length D = 0 \<Longrightarrow> 0 < K \<and> 0 < length D
 2. \<not> (K = 0 \<or> length D = 0) \<Longrightarrow> 0 < K \<and> 0 < length D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. 0 < K \<and> 0 < length D
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < K \<and> 0 < length D

goal (1 subgoal):
 1. \<not> (K = 0 \<or> length D = 0) \<Longrightarrow> 0 < K \<and> 0 < length D
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (K = 0 \<or> length D = 0) \<Longrightarrow> 0 < K \<and> 0 < length D
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (K = 0 \<or> length D = 0)

goal (1 subgoal):
 1. \<not> (K = 0 \<or> length D = 0) \<Longrightarrow> 0 < K \<and> 0 < length D
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (K = 0 \<or> length D = 0)

goal (1 subgoal):
 1. 0 < K \<and> 0 < length D
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
0 < K \<and> 0 < length D

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < K \<and> 0 < length D

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < K \<and> 0 < length D
[PROOF STEP]
have "take K D = take (K - 1) D @ [D ! (K - 1)]"
[PROOF STATE]
proof (prove)
using this:
0 < K \<and> 0 < length D

goal (1 subgoal):
 1. take K D = take (K - 1) D @ [D ! (K - 1)]
[PROOF STEP]
by (metis Minimal.hyps(1) One_nat_def Suc_less_eq Suc_pred hd_drop_conv_nth
          le_imp_less_Suc take_hd_drop)
[PROOF STATE]
proof (state)
this:
take K D = take (K - 1) D @ [D ! (K - 1)]

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take K D = take (K - 1) D @ [D ! (K - 1)]
[PROOF STEP]
have "\<exists> \<delta>. LeftDerivation [\<SS>] (take (K - 1) D) \<delta> \<and> LeftDerivation \<delta> [D ! (K - 1)] (a@[X]@b)"
[PROOF STATE]
proof (prove)
using this:
take K D = take (K - 1) D @ [D ! (K - 1)]

goal (1 subgoal):
 1. \<exists>\<delta>. LeftDerivation [\<SS>] (take (K - 1) D) \<delta> \<and> LeftDerivation \<delta> [D ! (K - 1)] (a @ [X] @ b)
[PROOF STEP]
by (metis LeftDerivation_append aXb)
[PROOF STATE]
proof (state)
this:
\<exists>\<delta>. LeftDerivation [\<SS>] (take (K - 1) D) \<delta> \<and> LeftDerivation \<delta> [D ! (K - 1)] (a @ [X] @ b)

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<delta>. LeftDerivation [\<SS>] (take (K - 1) D) \<delta> \<and> LeftDerivation \<delta> [D ! (K - 1)] (a @ [X] @ b)
[PROOF STEP]
obtain \<delta> where
      \<delta>1: "LeftDerivation [\<SS>] (take (K - 1) D) \<delta>"
      and \<delta>2: "LeftDerivation \<delta> [D ! (K - 1)] (a@[X]@b)"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<delta>. LeftDerivation [\<SS>] (take (K - 1) D) \<delta> \<and> LeftDerivation \<delta> [D ! (K - 1)] (a @ [X] @ b)

goal (1 subgoal):
 1. (\<And>\<delta>. \<lbrakk>LeftDerivation [\<SS>] (take (K - 1) D) \<delta>; LeftDerivation \<delta> [D ! (K - 1)] (a @ [X] @ b)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
LeftDerivation [\<SS>] (take (K - 1) D) \<delta>
LeftDerivation \<delta> [D ! (K - 1)] (a @ [X] @ b)

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
from \<delta>2
[PROOF STATE]
proof (chain)
picking this:
LeftDerivation \<delta> [D ! (K - 1)] (a @ [X] @ b)
[PROOF STEP]
have "\<exists> i r. LeftDerives1 \<delta> i r (a@[X]@b)"
[PROOF STATE]
proof (prove)
using this:
LeftDerivation \<delta> [D ! (K - 1)] (a @ [X] @ b)

goal (1 subgoal):
 1. \<exists>i r. LeftDerives1 \<delta> i r (a @ [X] @ b)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>i r. LeftDerives1 \<delta> i r (a @ [X] @ b)

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i r. LeftDerives1 \<delta> i r (a @ [X] @ b)
[PROOF STEP]
obtain i r where LeftDerives1_\<delta>: "LeftDerives1 \<delta> i r (a@[X]@b)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i r. LeftDerives1 \<delta> i r (a @ [X] @ b)

goal (1 subgoal):
 1. (\<And>i r. LeftDerives1 \<delta> i r (a @ [X] @ b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
LeftDerives1 \<delta> i r (a @ [X] @ b)

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
LeftDerives1 \<delta> i r (a @ [X] @ b)
[PROOF STEP]
have Derives1_\<delta>: "Derives1 \<delta> i r (a@[X]@b)"
[PROOF STATE]
proof (prove)
using this:
LeftDerives1 \<delta> i r (a @ [X] @ b)

goal (1 subgoal):
 1. Derives1 \<delta> i r (a @ [X] @ b)
[PROOF STEP]
by (metis LeftDerives1_implies_Derives1)
[PROOF STATE]
proof (state)
this:
Derives1 \<delta> i r (a @ [X] @ b)

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Derives1 \<delta> i r (a @ [X] @ b)
[PROOF STEP]
have "\<exists> \<alpha> N \<beta> . splits_at \<delta> i \<alpha> N \<beta>"
[PROOF STATE]
proof (prove)
using this:
Derives1 \<delta> i r (a @ [X] @ b)

goal (1 subgoal):
 1. \<exists>\<alpha> N \<beta>. splits_at \<delta> i \<alpha> N \<beta>
[PROOF STEP]
by (simp add: splits_at_ex)
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha> N \<beta>. splits_at \<delta> i \<alpha> N \<beta>

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<alpha> N \<beta>. splits_at \<delta> i \<alpha> N \<beta>
[PROOF STEP]
obtain \<alpha> N \<beta> where split_\<delta>: "splits_at \<delta> i \<alpha> N \<beta>"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<alpha> N \<beta>. splits_at \<delta> i \<alpha> N \<beta>

goal (1 subgoal):
 1. (\<And>\<alpha> N \<beta>. splits_at \<delta> i \<alpha> N \<beta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
splits_at \<delta> i \<alpha> N \<beta>

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
have is_word_\<alpha>: "is_word \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_word \<alpha>
[PROOF STEP]
by (metis LeftDerives1_\<delta> LeftDerives1_splits_at_is_word split_\<delta>)
[PROOF STATE]
proof (state)
this:
is_word \<alpha>

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
have "\<not> (?P (K - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>a b. LeftDerivation [\<SS>] (take (K - 1) D) (a @ [X] @ b) \<and> derives a (terminals p)
[PROOF STEP]
using KD Minimal(3)
[PROOF STATE]
proof (prove)
using this:
0 < K \<and> 0 < length D
?k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take ?k D) (a @ [X] @ b) \<and> derives a (terminals p)

goal (1 subgoal):
 1. \<nexists>a b. LeftDerivation [\<SS>] (take (K - 1) D) (a @ [X] @ b) \<and> derives a (terminals p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>a b. LeftDerivation [\<SS>] (take (K - 1) D) (a @ [X] @ b) \<and> derives a (terminals p)

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
with \<delta>1
[PROOF STATE]
proof (chain)
picking this:
LeftDerivation [\<SS>] (take (K - 1) D) \<delta>
\<nexists>a b. LeftDerivation [\<SS>] (take (K - 1) D) (a @ [X] @ b) \<and> derives a (terminals p)
[PROOF STEP]
have min_\<delta>: "\<not> (\<exists> a b. \<delta> = a@[X]@b \<and> derives a (terminals p))"
[PROOF STATE]
proof (prove)
using this:
LeftDerivation [\<SS>] (take (K - 1) D) \<delta>
\<nexists>a b. LeftDerivation [\<SS>] (take (K - 1) D) (a @ [X] @ b) \<and> derives a (terminals p)

goal (1 subgoal):
 1. \<nexists>a b. \<delta> = a @ [X] @ b \<and> derives a (terminals p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<nexists>a b. \<delta> = a @ [X] @ b \<and> derives a (terminals p)

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
from Derives1_\<delta> split_\<delta>
[PROOF STATE]
proof (chain)
picking this:
Derives1 \<delta> i r (a @ [X] @ b)
splits_at \<delta> i \<alpha> N \<beta>
[PROOF STEP]
have "\<exists> u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> (snd r) = u@[X]@v"
[PROOF STATE]
proof (prove)
using this:
Derives1 \<delta> i r (a @ [X] @ b)
splits_at \<delta> i \<alpha> N \<beta>

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
proof (induction rule: Derives1_X_is_part_of_rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<beta>. \<lbrakk>\<delta> = a @ [X] @ \<beta>; length a < i; Derives1 \<beta> (i - length a - 1) r b\<rbrakk> \<Longrightarrow> False
 2. \<And>\<alpha>. \<lbrakk>\<delta> = \<alpha> @ [X] @ b; Derives1 \<alpha> i r a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (Suffix \<gamma>)
[PROOF STATE]
proof (state)
this:
\<delta> = a @ [X] @ \<gamma>
length a < i
Derives1 \<gamma> (i - length a - 1) r b

goal (2 subgoals):
 1. \<And>\<beta>. \<lbrakk>\<delta> = a @ [X] @ \<beta>; length a < i; Derives1 \<beta> (i - length a - 1) r b\<rbrakk> \<Longrightarrow> False
 2. \<And>\<alpha>. \<lbrakk>\<delta> = \<alpha> @ [X] @ b; Derives1 \<alpha> i r a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from min_\<delta> Suffix(1) a
[PROOF STATE]
proof (chain)
picking this:
\<nexists>a b. \<delta> = a @ [X] @ b \<and> derives a (terminals p)
\<delta> = a @ [X] @ \<gamma>
derives a (terminals p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<nexists>a b. \<delta> = a @ [X] @ b \<and> derives a (terminals p)
\<delta> = a @ [X] @ \<gamma>
derives a (terminals p)

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

goal (1 subgoal):
 1. \<And>\<alpha>. \<lbrakk>\<delta> = \<alpha> @ [X] @ b; Derives1 \<alpha> i r a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<alpha>. \<lbrakk>\<delta> = \<alpha> @ [X] @ b; Derives1 \<alpha> i r a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (Prefix \<gamma>)
[PROOF STATE]
proof (state)
this:
\<delta> = \<gamma> @ [X] @ b
Derives1 \<gamma> i r a

goal (1 subgoal):
 1. \<And>\<alpha>. \<lbrakk>\<delta> = \<alpha> @ [X] @ b; Derives1 \<alpha> i r a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "derives \<gamma> (terminals p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives \<gamma> (terminals p)
[PROOF STEP]
by (metis Derives1_implies_derives1 Prefix(2) a
              derives1_implies_derives derives_trans)
[PROOF STATE]
proof (state)
this:
derives \<gamma> (terminals p)

goal (1 subgoal):
 1. \<And>\<alpha>. \<lbrakk>\<delta> = \<alpha> @ [X] @ b; Derives1 \<alpha> i r a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with min_\<delta> Prefix(1)
[PROOF STATE]
proof (chain)
picking this:
\<nexists>a b. \<delta> = a @ [X] @ b \<and> derives a (terminals p)
\<delta> = \<gamma> @ [X] @ b
derives \<gamma> (terminals p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<nexists>a b. \<delta> = a @ [X] @ b \<and> derives a (terminals p)
\<delta> = \<gamma> @ [X] @ b
derives \<gamma> (terminals p)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
obtain u v where uXv: "a = \<alpha> @ u \<and> b = v @ \<beta> \<and> (snd r) = u@[X]@v"
[PROOF STATE]
proof (prove)
using this:
\<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v

goal (1 subgoal):
 1. (\<And>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
let ?l = "length \<alpha>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
let ?q = "take ?l p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
let ?x = "Item r (length u) (charslength ?q) (charslength p)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
have "item_rhs ?x = snd r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_rhs (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = snd r
[PROOF STEP]
by (simp add: item_rhs_def)
[PROOF STATE]
proof (state)
this:
item_rhs (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = snd r

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
item_rhs (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = snd r
[PROOF STEP]
have item_rhs_x: "item_rhs ?x = u@[X]@v"
[PROOF STATE]
proof (prove)
using this:
item_rhs (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = snd r

goal (1 subgoal):
 1. item_rhs (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = u @ [X] @ v
[PROOF STEP]
using uXv
[PROOF STATE]
proof (prove)
using this:
item_rhs (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = snd r
a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v

goal (1 subgoal):
 1. item_rhs (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = u @ [X] @ v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
item_rhs (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = u @ [X] @ v

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
have wellformed_x: "wellformed_item ?x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_item (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p))
[PROOF STEP]
apply (auto simp add: wellformed_item_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. r \<in> \<RR>
 2. length (chars (take (length \<alpha>) p)) \<le> length (chars p)
 3. length (chars p) \<le> length Doc
 4. length u \<le> length (item_rhs (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))))
[PROOF STEP]
apply (metis Derives1_\<delta> Derives1_rule)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. length (chars (take (length \<alpha>) p)) \<le> length (chars p)
 2. length (chars p) \<le> length Doc
 3. length u \<le> length (item_rhs (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))))
[PROOF STEP]
apply (rule is_prefix_length)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. is_prefix (chars (take (length \<alpha>) p)) (chars p)
 2. length (chars p) \<le> length Doc
 3. length u \<le> length (item_rhs (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))))
[PROOF STEP]
apply (rule is_prefix_chars)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. is_prefix (take (length \<alpha>) p) p
 2. length (chars p) \<le> length Doc
 3. length u \<le> length (item_rhs (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (chars p) \<le> length Doc
 2. length u \<le> length (item_rhs (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))))
[PROOF STEP]
apply (simp add: doc_tokens_length[OF p])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length u \<le> length (item_rhs (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))))
[PROOF STEP]
using item_rhs_x
[PROOF STATE]
proof (prove)
using this:
item_rhs (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = u @ [X] @ v

goal (1 subgoal):
 1. length u \<le> length (item_rhs (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wellformed_item (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p))

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
from item_rhs_x
[PROOF STATE]
proof (chain)
picking this:
item_rhs (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = u @ [X] @ v
[PROOF STEP]
have next_symbol_x: "next_symbol ?x = Some X"
[PROOF STATE]
proof (prove)
using this:
item_rhs (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = u @ [X] @ v

goal (1 subgoal):
 1. next_symbol (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = Some X
[PROOF STEP]
by (auto simp add: next_symbol_def is_complete_def)
[PROOF STATE]
proof (state)
this:
next_symbol (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = Some X

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
have len_\<alpha>_p: "length \<alpha> \<le> length p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length \<alpha> \<le> length p
[PROOF STEP]
apply (rule_tac path_length_is_upper_bound[where u=u])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. wellformed_tokens p
 2. is_word \<alpha>
 3. derives (\<alpha> @ u) (terminals p)
[PROOF STEP]
apply (simp add: wellformed_p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. is_word \<alpha>
 2. derives (\<alpha> @ u) (terminals p)
[PROOF STEP]
apply (simp add: is_word_\<alpha>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives (\<alpha> @ u) (terminals p)
[PROOF STEP]
using a uXv
[PROOF STATE]
proof (prove)
using this:
derives a (terminals p)
a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v

goal (1 subgoal):
 1. derives (\<alpha> @ u) (terminals p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length \<alpha> \<le> length p

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
have item_nonterminal_x: "item_nonterminal ?x = N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_nonterminal (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = N
[PROOF STEP]
apply (simp add: item_nonterminal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst r = N
[PROOF STEP]
using Derives1_\<delta> Derives1_nonterminal split_\<delta>
[PROOF STATE]
proof (prove)
using this:
Derives1 \<delta> i r (a @ [X] @ b)
\<lbrakk>Derives1 ?a ?i ?r ?b; splits_at ?a ?i ?\<alpha> ?N ?\<beta>\<rbrakk> \<Longrightarrow> fst ?r = ?N \<and> is_nonterminal ?N
splits_at \<delta> i \<alpha> N \<beta>

goal (1 subgoal):
 1. fst r = N
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
item_nonterminal (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = N

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
have take_terminals: "take (length \<alpha>) (terminals p) = \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length \<alpha>) (terminals p) = \<alpha>
[PROOF STEP]
apply (rule_tac take_prefix)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix \<alpha> (terminals p)
[PROOF STEP]
using a derives_word_is_prefix is_word_\<alpha> uXv
[PROOF STATE]
proof (prove)
using this:
derives a (terminals p)
\<lbrakk>is_word ?w; derives (?w @ ?a) ?b\<rbrakk> \<Longrightarrow> is_prefix ?w ?b
is_word \<alpha>
a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v

goal (1 subgoal):
 1. is_prefix \<alpha> (terminals p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
take (length \<alpha>) (terminals p) = \<alpha>

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
have item_\<alpha>_x: "item_\<alpha> ?x = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_\<alpha> (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = u
[PROOF STEP]
using item_\<alpha>_def item_rhs_x
[PROOF STATE]
proof (prove)
using this:
item_\<alpha> ?x = take (item_dot ?x) (item_rhs ?x)
item_rhs (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = u @ [X] @ v

goal (1 subgoal):
 1. item_\<alpha> (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
item_\<alpha> (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = u

goal (1 subgoal):
 1. \<And>K. \<lbrakk>K \<le> length D; \<exists>a b. LeftDerivation [\<SS>] (take K D) (a @ [X] @ b) \<and> derives a (terminals p); \<And>k. k < K \<Longrightarrow> \<nexists>a b. LeftDerivation [\<SS>] (take k D) (a @ [X] @ b) \<and> derives a (terminals p)\<rbrakk> \<Longrightarrow> \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
from wellformed_x next_symbol_x len_\<alpha>_p
[PROOF STATE]
proof (chain)
picking this:
wellformed_item (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p))
next_symbol (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = Some X
length \<alpha> \<le> length p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wellformed_item (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p))
next_symbol (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = Some X
length \<alpha> \<le> length p

goal (1 subgoal):
 1. \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
apply (rule_tac x="?x" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wellformed_item (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)); next_symbol (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = Some X; length \<alpha> \<le> length p\<rbrakk> \<Longrightarrow> pvalid p (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) \<and> next_symbol (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = Some X
[PROOF STEP]
apply (auto simp add: pvalid_def wellformed_p)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p\<rbrakk> \<Longrightarrow> \<exists>ua\<le>length p. length (chars (take ua p)) = length (chars (take (length \<alpha>) p)) \<and> (\<exists>\<gamma>. is_derivation (take ua (terminals p) @ item_nonterminal (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) # \<gamma>)) \<and> derives (item_\<alpha> (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p)))) (drop ua (terminals p))
[PROOF STEP]
apply (rule_tac x="length \<alpha>" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p\<rbrakk> \<Longrightarrow> length \<alpha> \<le> length p \<and> length (chars (take (length \<alpha>) p)) = length (chars (take (length \<alpha>) p)) \<and> (\<exists>\<gamma>. is_derivation (take (length \<alpha>) (terminals p) @ item_nonterminal (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) # \<gamma>)) \<and> derives (item_\<alpha> (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p)))) (drop (length \<alpha>) (terminals p))
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p\<rbrakk> \<Longrightarrow> \<exists>\<gamma>. is_derivation (take (length \<alpha>) (terminals p) @ item_nonterminal (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) # \<gamma>)
 2. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p\<rbrakk> \<Longrightarrow> derives (item_\<alpha> (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p)))) (drop (length \<alpha>) (terminals p))
[PROOF STEP]
using item_nonterminal_x
[PROOF STATE]
proof (prove)
using this:
item_nonterminal (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = N

goal (2 subgoals):
 1. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p\<rbrakk> \<Longrightarrow> \<exists>\<gamma>. is_derivation (take (length \<alpha>) (terminals p) @ item_nonterminal (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) # \<gamma>)
 2. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p\<rbrakk> \<Longrightarrow> derives (item_\<alpha> (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p)))) (drop (length \<alpha>) (terminals p))
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p; item_nonterminal (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = N\<rbrakk> \<Longrightarrow> \<exists>\<gamma>. is_derivation (take (length \<alpha>) (terminals p) @ N # \<gamma>)
 2. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p\<rbrakk> \<Longrightarrow> derives (item_\<alpha> (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p)))) (drop (length \<alpha>) (terminals p))
[PROOF STEP]
apply (simp add: take_terminals)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p; item_nonterminal (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = N\<rbrakk> \<Longrightarrow> \<exists>\<gamma>. is_derivation (\<alpha> @ N # \<gamma>)
 2. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p\<rbrakk> \<Longrightarrow> derives (item_\<alpha> (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p)))) (drop (length \<alpha>) (terminals p))
[PROOF STEP]
apply (rule_tac x="\<beta>" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p; item_nonterminal (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = N\<rbrakk> \<Longrightarrow> is_derivation (\<alpha> @ N # \<beta>)
 2. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p\<rbrakk> \<Longrightarrow> derives (item_\<alpha> (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p)))) (drop (length \<alpha>) (terminals p))
[PROOF STEP]
using LeftDerivation_implies_leftderives \<delta>1 is_leftderivation_def split_\<delta> splits_at_combine
[PROOF STATE]
proof (prove)
using this:
LeftDerivation ?a ?D ?b \<Longrightarrow> leftderives ?a ?b
LeftDerivation [\<SS>] (take (K - 1) D) \<delta>
is_leftderivation ?u = leftderives [\<SS>] ?u
splits_at \<delta> i \<alpha> N \<beta>
splits_at ?\<delta> ?i ?\<alpha> ?N ?\<beta> \<Longrightarrow> ?\<delta> = ?\<alpha> @ [?N] @ ?\<beta>

goal (2 subgoals):
 1. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p; item_nonterminal (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = N\<rbrakk> \<Longrightarrow> is_derivation (\<alpha> @ N # \<beta>)
 2. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p\<rbrakk> \<Longrightarrow> derives (item_\<alpha> (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p)))) (drop (length \<alpha>) (terminals p))
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p\<rbrakk> \<Longrightarrow> derives (item_\<alpha> (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p)))) (drop (length \<alpha>) (terminals p))
[PROOF STEP]
using item_\<alpha>_x
[PROOF STATE]
proof (prove)
using this:
item_\<alpha> (Item r (length u) (charslength (take (length \<alpha>) p)) (charslength p)) = u

goal (1 subgoal):
 1. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p\<rbrakk> \<Longrightarrow> derives (item_\<alpha> (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p)))) (drop (length \<alpha>) (terminals p))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wellformed_item (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))); next_symbol (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = Some X; length \<alpha> \<le> length p; item_\<alpha> (Item r (length u) (length (chars (take (length \<alpha>) p))) (length (chars p))) = u\<rbrakk> \<Longrightarrow> derives u (drop (length \<alpha>) (terminals p))
[PROOF STEP]
by (metis a derive_drop_prefixword is_word_\<alpha> uXv)
[PROOF STATE]
proof (state)
this:
\<exists>x. pvalid p x \<and> next_symbol x = Some X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. pvalid p x \<and> next_symbol x = Some X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma admissible_wellformed_tokens: "admissible p \<Longrightarrow> wellformed_tokens p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admissible p \<Longrightarrow> wellformed_tokens p
[PROOF STEP]
by (auto simp add: admissible_def \<L>\<^sub>P_wellformed_tokens)


[STATEMENT]
lemma chars_append[simp]: "chars (a@b) = (chars a)@(chars b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chars (a @ b) = chars a @ chars b
[PROOF STEP]
by (induct a arbitrary: b, auto)


[STATEMENT]
lemma chars_of_token_simp[simp]: "chars_of_token (a, b) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chars_of_token (a, b) = b
[PROOF STEP]
by (simp add: chars_of_token_def)


[STATEMENT]
lemma is_prefix_append: "is_prefix (a@b) D = (is_prefix a D \<and> is_prefix b (drop (length a) D))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix (a @ b) D = (is_prefix a D \<and> is_prefix b (drop (length a) D))
[PROOF STEP]
by (metis append_assoc is_prefix_cancel is_prefix_def is_prefix_unsplit)


[STATEMENT]
lemma \<PP>_are_doc_tokens: "p \<in> \<PP> \<Longrightarrow> doc_tokens p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<PP> \<Longrightarrow> doc_tokens p
[PROOF STEP]
proof (induct rule: \<PP>_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. doc_tokens []
 2. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> doc_tokens q; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
case Base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. doc_tokens []
 2. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> doc_tokens q; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. doc_tokens []
[PROOF STEP]
by (simp add: doc_tokens_def wellformed_tokens_def)
[PROOF STATE]
proof (state)
this:
doc_tokens []

goal (1 subgoal):
 1. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> doc_tokens q; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> doc_tokens q; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
case (Induct p k u)
[PROOF STATE]
proof (state)
this:
?q \<in> \<P> k u \<Longrightarrow> doc_tokens ?q
p \<in> \<P> k (Suc u)

goal (1 subgoal):
 1. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> doc_tokens q; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
from Induct(2)[simplified]
[PROOF STATE]
proof (chain)
picking this:
p \<in> limit (Append (\<Y> (\<Z> k u) (\<P> k u) k) k) (\<P> k u)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> limit (Append (\<Y> (\<Z> k u) (\<P> k u) k) k) (\<P> k u)

goal (1 subgoal):
 1. doc_tokens p
[PROOF STEP]
proof (induct rule: limit_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. p \<in> \<P> k u \<Longrightarrow> doc_tokens p
 2. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> doc_tokens q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
case (Init p)
[PROOF STATE]
proof (state)
this:
p \<in> \<P> k u

goal (2 subgoals):
 1. \<And>p. p \<in> \<P> k u \<Longrightarrow> doc_tokens p
 2. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> doc_tokens q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
from Induct(1)[OF Init]
[PROOF STATE]
proof (chain)
picking this:
doc_tokens p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
doc_tokens p

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

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> doc_tokens q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> doc_tokens q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
case (Iterate p Y)
[PROOF STATE]
proof (state)
this:
?q \<in> Y \<Longrightarrow> doc_tokens ?q
p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> doc_tokens q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
have Y_is_prefix: "\<And> p. p \<in> Y \<Longrightarrow> is_prefix (chars p) Doc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. p \<in> Y \<Longrightarrow> is_prefix (chars p) Doc
[PROOF STEP]
apply (drule Iterate(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. doc_tokens p \<Longrightarrow> is_prefix (chars p) Doc
[PROOF STEP]
by (simp add: doc_tokens_def)
[PROOF STATE]
proof (state)
this:
?p \<in> Y \<Longrightarrow> is_prefix (chars ?p) Doc

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> doc_tokens q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
have "\<Y> (\<Z> k u) (\<P> k u) k \<subseteq> \<X> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Y> (\<Z> k u) (\<P> k u) k \<subseteq> \<X> k
[PROOF STEP]
by (metis \<Z>.simps(2) \<Z>_subset_\<X>)
[PROOF STATE]
proof (state)
this:
\<Y> (\<Z> k u) (\<P> k u) k \<subseteq> \<X> k

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> doc_tokens q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Y> (\<Z> k u) (\<P> k u) k \<subseteq> \<X> k
[PROOF STEP]
have 1: "Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y \<subseteq> Append (\<X> k) k Y"
[PROOF STATE]
proof (prove)
using this:
\<Y> (\<Z> k u) (\<P> k u) k \<subseteq> \<X> k

goal (1 subgoal):
 1. Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y \<subseteq> Append (\<X> k) k Y
[PROOF STEP]
by (rule Append_mono, simp)
[PROOF STATE]
proof (state)
this:
Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y \<subseteq> Append (\<X> k) k Y

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> doc_tokens q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
have 2: "p \<in> Append (\<X> k) k Y \<Longrightarrow> doc_tokens p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> Append (\<X> k) k Y \<Longrightarrow> doc_tokens p
[PROOF STEP]
apply (auto simp add: Append_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p \<in> Y \<Longrightarrow> doc_tokens p
 2. \<And>p a b. \<lbrakk>p = p @ [(a, b)]; p \<in> Y; k = length (chars p); (a, b) \<in> \<X> (length (chars p)); admissible (p @ [(a, b)])\<rbrakk> \<Longrightarrow> doc_tokens (p @ [(a, b)])
[PROOF STEP]
apply (simp add: Iterate)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p a b. \<lbrakk>p = p @ [(a, b)]; p \<in> Y; k = length (chars p); (a, b) \<in> \<X> (length (chars p)); admissible (p @ [(a, b)])\<rbrakk> \<Longrightarrow> doc_tokens (p @ [(a, b)])
[PROOF STEP]
apply (auto simp add: doc_tokens_def admissible_wellformed_tokens
             is_prefix_append Y_is_prefix)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p a b. \<lbrakk>p = p @ [(a, b)]; p \<in> Y; k = length (chars p); (a, b) \<in> \<X> (length (chars p)); admissible (p @ [(a, b)])\<rbrakk> \<Longrightarrow> is_prefix b (drop (length (chars p)) Doc)
[PROOF STEP]
by (metis \<X>_is_prefix snd_conv)
[PROOF STATE]
proof (state)
this:
p \<in> Append (\<X> k) k Y \<Longrightarrow> doc_tokens p

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> doc_tokens q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> doc_tokens p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. doc_tokens p
[PROOF STEP]
apply (rule 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> Append (\<X> k) k Y
[PROOF STEP]
by (metis (mono_tags, lifting) "1" Iterate(2) subsetCE)
[PROOF STATE]
proof (state)
this:
doc_tokens p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
doc_tokens p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem thmD2:
  assumes X: "is_terminal X"
  assumes p: "p \<in> \<PP>"
  assumes pX: "(terminals p)@[X] \<in> \<L>\<^sub>P"
  shows "\<exists> x. pvalid p x \<and> next_symbol x = Some X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. pvalid p x \<and> next_symbol x = Some X
[PROOF STEP]
by (metis X \<PP>_are_doc_tokens p pX thmD2')


[STATEMENT]
lemma value_cases:
fixes v :: "value"
obtains (PVal) pst where "v = Inl (Post_ISSUER.PVal pst)"
      | (PValS) aid pst where "v = Inl (Post_ISSUER.PValS aid pst)"
      | (PValR) pst where "v = Inr (Post_RECEIVER.PValR pst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>pst. v = Inl (Post_ISSUER.PVal pst) \<Longrightarrow> thesis; \<And>aid pst. v = Inl (Post_ISSUER.PValS aid pst) \<Longrightarrow> thesis; \<And>pst. v = Inr (Post_RECEIVER.PValR pst) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof (cases v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<And>pst. v = Inl (Post_ISSUER.PVal pst) \<Longrightarrow> thesis; \<And>aid pst. v = Inl (Post_ISSUER.PValS aid pst) \<Longrightarrow> thesis; \<And>pst. v = Inr (Post_RECEIVER.PValR pst) \<Longrightarrow> thesis; v = Inl a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>b. \<lbrakk>\<And>pst. v = Inl (Post_ISSUER.PVal pst) \<Longrightarrow> thesis; \<And>aid pst. v = Inl (Post_ISSUER.PValS aid pst) \<Longrightarrow> thesis; \<And>pst. v = Inr (Post_RECEIVER.PValR pst) \<Longrightarrow> thesis; v = Inr b\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (Inl vl)
[PROOF STATE]
proof (state)
this:
v = Inl vl

goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<And>pst. v = Inl (Post_ISSUER.PVal pst) \<Longrightarrow> thesis; \<And>aid pst. v = Inl (Post_ISSUER.PValS aid pst) \<Longrightarrow> thesis; \<And>pst. v = Inr (Post_RECEIVER.PValR pst) \<Longrightarrow> thesis; v = Inl a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>b. \<lbrakk>\<And>pst. v = Inl (Post_ISSUER.PVal pst) \<Longrightarrow> thesis; \<And>aid pst. v = Inl (Post_ISSUER.PValS aid pst) \<Longrightarrow> thesis; \<And>pst. v = Inr (Post_RECEIVER.PValR pst) \<Longrightarrow> thesis; v = Inr b\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v = Inl vl
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
v = Inl vl

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using PVal PValS
[PROOF STATE]
proof (prove)
using this:
v = Inl vl
v = Inl (Post_ISSUER.PVal ?pst) \<Longrightarrow> thesis
v = Inl (Post_ISSUER.PValS ?aid ?pst) \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (cases vl rule: Post_ISSUER.value.exhaust) auto
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<And>pst. v = Inl (Post_ISSUER.PVal pst) \<Longrightarrow> thesis; \<And>aid pst. v = Inl (Post_ISSUER.PValS aid pst) \<Longrightarrow> thesis; \<And>pst. v = Inr (Post_RECEIVER.PValR pst) \<Longrightarrow> thesis; v = Inr b\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<And>pst. v = Inl (Post_ISSUER.PVal pst) \<Longrightarrow> thesis; \<And>aid pst. v = Inl (Post_ISSUER.PValS aid pst) \<Longrightarrow> thesis; \<And>pst. v = Inr (Post_RECEIVER.PValR pst) \<Longrightarrow> thesis; v = Inr b\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (Inr vr)
[PROOF STATE]
proof (state)
this:
v = Inr vr

goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<And>pst. v = Inl (Post_ISSUER.PVal pst) \<Longrightarrow> thesis; \<And>aid pst. v = Inl (Post_ISSUER.PValS aid pst) \<Longrightarrow> thesis; \<And>pst. v = Inr (Post_RECEIVER.PValR pst) \<Longrightarrow> thesis; v = Inr b\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v = Inr vr
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
v = Inr vr

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using PValR
[PROOF STATE]
proof (prove)
using this:
v = Inr vr
v = Inr (Post_RECEIVER.PValR ?pst) \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (cases vr rule: Post_RECEIVER.value.exhaust) auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma syncVI: "syncV AID (Inl (Post_ISSUER.PValS aid' pst)) aid' (Inr (Post_RECEIVER.PValR pst))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. syncV AID (Inl (Iss.PValS aid' pst)) aid' (Inr (Post_RECEIVER.PValR pst))
[PROOF STEP]
unfolding syncV_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>psta. AID = AID \<and> Inl (Iss.PValS aid' pst) = Inl (Iss.PValS aid' psta) \<and> Inr (Post_RECEIVER.PValR pst) = Inr (Post_RECEIVER.PValR psta)
[PROOF STEP]
by auto


[STATEMENT]
lemma syncVE:
assumes "syncV aid1 v1 aid2 v2"
obtains pst where "aid1 = AID" "v1 = Inl (Post_ISSUER.PValS aid2 pst)" "v2 = Inr (Post_RECEIVER.PValR pst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pst. \<lbrakk>aid1 = AID; v1 = Inl (Iss.PValS aid2 pst); v2 = Inr (Post_RECEIVER.PValR pst)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
syncV aid1 v1 aid2 v2

goal (1 subgoal):
 1. (\<And>pst. \<lbrakk>aid1 = AID; v1 = Inl (Iss.PValS aid2 pst); v2 = Inr (Post_RECEIVER.PValR pst)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding syncV_def
[PROOF STATE]
proof (prove)
using this:
\<exists>pst. aid1 = AID \<and> v1 = Inl (Iss.PValS aid2 pst) \<and> v2 = Inr (Post_RECEIVER.PValR pst)

goal (1 subgoal):
 1. (\<And>pst. \<lbrakk>aid1 = AID; v1 = Inl (Iss.PValS aid2 pst); v2 = Inr (Post_RECEIVER.PValR pst)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma comOfV_AID:
  "comOfV AID v = Send \<longleftrightarrow> isl v \<and> Iss.isPValS (projl v) \<and> Iss.PValS_tgtAPI (projl v) \<noteq> AID"
  "comOfV AID v = Recv \<longleftrightarrow> Not (isl v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (comOfV AID v = Send) = (isl v \<and> Iss.isPValS (projl v) \<and> Iss.PValS_tgtAPI (projl v) \<noteq> AID) &&& (comOfV AID v = Recv) = (\<not> isl v)
[PROOF STEP]
by (cases v rule: value_cases; auto)+


[STATEMENT]
lemma list_all_Not_isl_projectSrcV: "list_all (Not o isl) (Net.projectSrcV aid vlSrc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (Not \<circ> isl) (Net.projectSrcV aid vlSrc)
[PROOF STEP]
proof (induction vlSrc)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. list_all (Not \<circ> isl) (Net.projectSrcV aid [])
 2. \<And>a vlSrc. list_all (Not \<circ> isl) (Net.projectSrcV aid vlSrc) \<Longrightarrow> list_all (Not \<circ> isl) (Net.projectSrcV aid (a # vlSrc))
[PROOF STEP]
case (Cons vSrc vlSrc')
[PROOF STATE]
proof (state)
this:
list_all (Not \<circ> isl) (Net.projectSrcV aid vlSrc')

goal (2 subgoals):
 1. list_all (Not \<circ> isl) (Net.projectSrcV aid [])
 2. \<And>a vlSrc. list_all (Not \<circ> isl) (Net.projectSrcV aid vlSrc) \<Longrightarrow> list_all (Not \<circ> isl) (Net.projectSrcV aid (a # vlSrc))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_all (Not \<circ> isl) (Net.projectSrcV aid vlSrc')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
list_all (Not \<circ> isl) (Net.projectSrcV aid vlSrc')

goal (1 subgoal):
 1. list_all (Not \<circ> isl) (Net.projectSrcV aid (vSrc # vlSrc'))
[PROOF STEP]
by (cases vSrc rule: value_cases) auto
[PROOF STATE]
proof (state)
this:
list_all (Not \<circ> isl) (Net.projectSrcV aid (vSrc # vlSrc'))

goal (1 subgoal):
 1. list_all (Not \<circ> isl) (Net.projectSrcV aid [])
[PROOF STEP]
qed auto


[STATEMENT]
lemma Source_B_Sink_B_aux:
assumes "list_all isl vl"
and "list_all isl vl1"
and "map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl)) =
     map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl1))"
shows "length (map projr (Net.projectSrcV AID' vl)) = length (map projr (Net.projectSrcV AID' vl1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map projr (Net.projectSrcV AID' vl)) = length (map projr (Net.projectSrcV AID' vl1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_all isl vl
list_all isl vl1
map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl1))

goal (1 subgoal):
 1. length (map projr (Net.projectSrcV AID' vl)) = length (map projr (Net.projectSrcV AID' vl1))
[PROOF STEP]
proof (induction vl vl1 rule: list22_induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>list_all isl []; list_all isl []; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl [])) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl []))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' [])) = length (map projr (Net.projectSrcV AID' []))
 2. \<And>x xs. \<lbrakk>\<lbrakk>list_all isl xs; list_all isl []; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl xs)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl []))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' xs)) = length (map projr (Net.projectSrcV AID' [])); list_all isl (x # xs); list_all isl []; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (x # xs))) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl []))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (x # xs))) = length (map projr (Net.projectSrcV AID' []))
 3. \<And>y ys. \<lbrakk>\<lbrakk>list_all isl []; list_all isl ys; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl [])) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ys))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' [])) = length (map projr (Net.projectSrcV AID' ys)); list_all isl []; list_all isl (y # ys); map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl [])) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (y # ys)))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' [])) = length (map projr (Net.projectSrcV AID' (y # ys)))
 4. \<And>x xs y ys. \<lbrakk>\<lbrakk>list_all isl xs; list_all isl ys; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl xs)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ys))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' xs)) = length (map projr (Net.projectSrcV AID' ys)); \<And>ys'. \<lbrakk>length ys' \<le> Suc (length ys); list_all isl xs; list_all isl ys'; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl xs)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ys'))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' xs)) = length (map projr (Net.projectSrcV AID' ys')); \<And>xs'. \<lbrakk>length xs' \<le> Suc (length xs); list_all isl xs'; list_all isl ys; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl xs')) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ys))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' xs')) = length (map projr (Net.projectSrcV AID' ys)); list_all isl (x # xs); list_all isl (y # ys); map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (x # xs))) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (y # ys)))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (x # xs))) = length (map projr (Net.projectSrcV AID' (y # ys)))
[PROOF STEP]
case (ConsCons v vl v1 vl1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>list_all isl vl; list_all isl vl1; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl1))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' vl)) = length (map projr (Net.projectSrcV AID' vl1))
\<lbrakk>length ?ys'1 \<le> Suc (length vl1); list_all isl vl; list_all isl ?ys'1; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ?ys'1))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' vl)) = length (map projr (Net.projectSrcV AID' ?ys'1))
\<lbrakk>length ?xs'1 \<le> Suc (length vl); list_all isl ?xs'1; list_all isl vl1; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ?xs'1)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl1))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' ?xs'1)) = length (map projr (Net.projectSrcV AID' vl1))
list_all isl (v # vl)
list_all isl (v1 # vl1)
map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (v # vl))) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (v1 # vl1)))

goal (4 subgoals):
 1. \<lbrakk>list_all isl []; list_all isl []; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl [])) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl []))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' [])) = length (map projr (Net.projectSrcV AID' []))
 2. \<And>x xs. \<lbrakk>\<lbrakk>list_all isl xs; list_all isl []; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl xs)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl []))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' xs)) = length (map projr (Net.projectSrcV AID' [])); list_all isl (x # xs); list_all isl []; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (x # xs))) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl []))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (x # xs))) = length (map projr (Net.projectSrcV AID' []))
 3. \<And>y ys. \<lbrakk>\<lbrakk>list_all isl []; list_all isl ys; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl [])) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ys))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' [])) = length (map projr (Net.projectSrcV AID' ys)); list_all isl []; list_all isl (y # ys); map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl [])) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (y # ys)))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' [])) = length (map projr (Net.projectSrcV AID' (y # ys)))
 4. \<And>x xs y ys. \<lbrakk>\<lbrakk>list_all isl xs; list_all isl ys; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl xs)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ys))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' xs)) = length (map projr (Net.projectSrcV AID' ys)); \<And>ys'. \<lbrakk>length ys' \<le> Suc (length ys); list_all isl xs; list_all isl ys'; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl xs)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ys'))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' xs)) = length (map projr (Net.projectSrcV AID' ys')); \<And>xs'. \<lbrakk>length xs' \<le> Suc (length xs); list_all isl xs'; list_all isl ys; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl xs')) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ys))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' xs')) = length (map projr (Net.projectSrcV AID' ys)); list_all isl (x # xs); list_all isl (y # ys); map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (x # xs))) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (y # ys)))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (x # xs))) = length (map projr (Net.projectSrcV AID' (y # ys)))
[PROOF STEP]
consider (SendSend) aid pst pst1 where "v = Inl (Iss.PValS aid pst)" "v1 = Inl (Iss.PValS aid pst1)"
           | (Internal) "comOfV AID v = Internal" "\<not>Iss.isPValS (projl v)"
           | (Internal1) "comOfV AID v1 = Internal" "\<not>Iss.isPValS (projl v1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>aid pst pst1. \<lbrakk>v = Inl (Iss.PValS aid pst); v1 = Inl (Iss.PValS aid pst1)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>comOfV AID v = Internal; \<not> Iss.isPValS (projl v)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>comOfV AID v1 = Internal; \<not> Iss.isPValS (projl v1)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using ConsCons(4-6)
[PROOF STATE]
proof (prove)
using this:
list_all isl (v # vl)
list_all isl (v1 # vl1)
map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (v # vl))) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (v1 # vl1)))

goal (1 subgoal):
 1. \<lbrakk>\<And>aid pst pst1. \<lbrakk>v = Inl (Iss.PValS aid pst); v1 = Inl (Iss.PValS aid pst1)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>comOfV AID v = Internal; \<not> Iss.isPValS (projl v)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>comOfV AID v1 = Internal; \<not> Iss.isPValS (projl v1)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (cases v rule: value_cases; cases v1 rule: value_cases) auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>aid pst pst1. \<lbrakk>v = Inl (Iss.PValS aid pst); v1 = Inl (Iss.PValS aid pst1)\<rbrakk> \<Longrightarrow> ?thesis1; \<lbrakk>comOfV AID v = Internal; \<not> Iss.isPValS (projl v)\<rbrakk> \<Longrightarrow> ?thesis1; \<lbrakk>comOfV AID v1 = Internal; \<not> Iss.isPValS (projl v1)\<rbrakk> \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (4 subgoals):
 1. \<lbrakk>list_all isl []; list_all isl []; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl [])) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl []))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' [])) = length (map projr (Net.projectSrcV AID' []))
 2. \<And>x xs. \<lbrakk>\<lbrakk>list_all isl xs; list_all isl []; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl xs)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl []))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' xs)) = length (map projr (Net.projectSrcV AID' [])); list_all isl (x # xs); list_all isl []; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (x # xs))) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl []))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (x # xs))) = length (map projr (Net.projectSrcV AID' []))
 3. \<And>y ys. \<lbrakk>\<lbrakk>list_all isl []; list_all isl ys; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl [])) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ys))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' [])) = length (map projr (Net.projectSrcV AID' ys)); list_all isl []; list_all isl (y # ys); map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl [])) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (y # ys)))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' [])) = length (map projr (Net.projectSrcV AID' (y # ys)))
 4. \<And>x xs y ys. \<lbrakk>\<lbrakk>list_all isl xs; list_all isl ys; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl xs)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ys))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' xs)) = length (map projr (Net.projectSrcV AID' ys)); \<And>ys'. \<lbrakk>length ys' \<le> Suc (length ys); list_all isl xs; list_all isl ys'; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl xs)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ys'))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' xs)) = length (map projr (Net.projectSrcV AID' ys')); \<And>xs'. \<lbrakk>length xs' \<le> Suc (length xs); list_all isl xs'; list_all isl ys; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl xs')) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ys))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' xs')) = length (map projr (Net.projectSrcV AID' ys)); list_all isl (x # xs); list_all isl (y # ys); map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (x # xs))) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (y # ys)))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (x # xs))) = length (map projr (Net.projectSrcV AID' (y # ys)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>aid pst pst1. \<lbrakk>v = Inl (Iss.PValS aid pst); v1 = Inl (Iss.PValS aid pst1)\<rbrakk> \<Longrightarrow> ?thesis1; \<lbrakk>comOfV AID v = Internal; \<not> Iss.isPValS (projl v)\<rbrakk> \<Longrightarrow> ?thesis1; \<lbrakk>comOfV AID v1 = Internal; \<not> Iss.isPValS (projl v1)\<rbrakk> \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>aid pst pst1. \<lbrakk>v = Inl (Iss.PValS aid pst); v1 = Inl (Iss.PValS aid pst1)\<rbrakk> \<Longrightarrow> ?thesis1; \<lbrakk>comOfV AID v = Internal; \<not> Iss.isPValS (projl v)\<rbrakk> \<Longrightarrow> ?thesis1; \<lbrakk>comOfV AID v1 = Internal; \<not> Iss.isPValS (projl v1)\<rbrakk> \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (1 subgoal):
 1. length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>aid pst pst1. \<lbrakk>v = Inl (Iss.PValS aid pst); v1 = Inl (Iss.PValS aid pst1)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
 2. \<lbrakk>comOfV AID v = Internal; \<not> Iss.isPValS (projl v)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
 3. \<lbrakk>comOfV AID v1 = Internal; \<not> Iss.isPValS (projl v1)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
case (SendSend)
[PROOF STATE]
proof (state)
this:
v = Inl (Iss.PValS aid pst)
v1 = Inl (Iss.PValS aid pst1)

goal (3 subgoals):
 1. \<And>aid pst pst1. \<lbrakk>v = Inl (Iss.PValS aid pst); v1 = Inl (Iss.PValS aid pst1)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
 2. \<lbrakk>comOfV AID v = Internal; \<not> Iss.isPValS (projl v)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
 3. \<lbrakk>comOfV AID v1 = Internal; \<not> Iss.isPValS (projl v1)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v = Inl (Iss.PValS aid pst)
v1 = Inl (Iss.PValS aid pst1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v = Inl (Iss.PValS aid pst)
v1 = Inl (Iss.PValS aid pst1)

goal (1 subgoal):
 1. length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
using ConsCons.IH(1) ConsCons.prems
[PROOF STATE]
proof (prove)
using this:
v = Inl (Iss.PValS aid pst)
v1 = Inl (Iss.PValS aid pst1)
\<lbrakk>list_all isl vl; list_all isl vl1; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl1))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' vl)) = length (map projr (Net.projectSrcV AID' vl1))
list_all isl (v # vl)
list_all isl (v1 # vl1)
map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (v # vl))) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (v1 # vl1)))

goal (1 subgoal):
 1. length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))

goal (2 subgoals):
 1. \<lbrakk>comOfV AID v = Internal; \<not> Iss.isPValS (projl v)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
 2. \<lbrakk>comOfV AID v1 = Internal; \<not> Iss.isPValS (projl v1)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>comOfV AID v = Internal; \<not> Iss.isPValS (projl v)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
 2. \<lbrakk>comOfV AID v1 = Internal; \<not> Iss.isPValS (projl v1)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
case (Internal)
[PROOF STATE]
proof (state)
this:
comOfV AID v = Internal
\<not> Iss.isPValS (projl v)

goal (2 subgoals):
 1. \<lbrakk>comOfV AID v = Internal; \<not> Iss.isPValS (projl v)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
 2. \<lbrakk>comOfV AID v1 = Internal; \<not> Iss.isPValS (projl v1)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
comOfV AID v = Internal
\<not> Iss.isPValS (projl v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
comOfV AID v = Internal
\<not> Iss.isPValS (projl v)

goal (1 subgoal):
 1. length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
using ConsCons.IH(2)[of "v1 # vl1"] ConsCons.prems
[PROOF STATE]
proof (prove)
using this:
comOfV AID v = Internal
\<not> Iss.isPValS (projl v)
\<lbrakk>length (v1 # vl1) \<le> Suc (length vl1); list_all isl vl; list_all isl (v1 # vl1); map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (v1 # vl1)))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' vl)) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
list_all isl (v # vl)
list_all isl (v1 # vl1)
map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (v # vl))) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (v1 # vl1)))

goal (1 subgoal):
 1. length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))

goal (1 subgoal):
 1. \<lbrakk>comOfV AID v1 = Internal; \<not> Iss.isPValS (projl v1)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>comOfV AID v1 = Internal; \<not> Iss.isPValS (projl v1)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
case (Internal1)
[PROOF STATE]
proof (state)
this:
comOfV AID v1 = Internal
\<not> Iss.isPValS (projl v1)

goal (1 subgoal):
 1. \<lbrakk>comOfV AID v1 = Internal; \<not> Iss.isPValS (projl v1)\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
comOfV AID v1 = Internal
\<not> Iss.isPValS (projl v1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
comOfV AID v1 = Internal
\<not> Iss.isPValS (projl v1)

goal (1 subgoal):
 1. length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
using ConsCons.IH(3)[of "v # vl"] ConsCons.prems
[PROOF STATE]
proof (prove)
using this:
comOfV AID v1 = Internal
\<not> Iss.isPValS (projl v1)
\<lbrakk>length (v # vl) \<le> Suc (length vl); list_all isl (v # vl); list_all isl vl1; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (v # vl))) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl vl1))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' vl1))
list_all isl (v # vl)
list_all isl (v1 # vl1)
map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (v # vl))) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (v1 # vl1)))

goal (1 subgoal):
 1. length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (map projr (Net.projectSrcV AID' (v # vl))) = length (map projr (Net.projectSrcV AID' (v1 # vl1)))

goal (3 subgoals):
 1. \<lbrakk>list_all isl []; list_all isl []; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl [])) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl []))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' [])) = length (map projr (Net.projectSrcV AID' []))
 2. \<And>x xs. \<lbrakk>\<lbrakk>list_all isl xs; list_all isl []; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl xs)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl []))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' xs)) = length (map projr (Net.projectSrcV AID' [])); list_all isl (x # xs); list_all isl []; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (x # xs))) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl []))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' (x # xs))) = length (map projr (Net.projectSrcV AID' []))
 3. \<And>y ys. \<lbrakk>\<lbrakk>list_all isl []; list_all isl ys; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl [])) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ys))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' [])) = length (map projr (Net.projectSrcV AID' ys)); list_all isl []; list_all isl (y # ys); map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl [])) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl (y # ys)))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' [])) = length (map projr (Net.projectSrcV AID' (y # ys)))
[PROOF STEP]
qed (auto simp: comOfV_AID)


[STATEMENT]
lemma Source_B_Sink_B:
assumes "B AID vl vl1"
shows "Sink.B (map projr (Net.projectSrcV AID' vl)) (map projr (Net.projectSrcV AID' vl1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sink.B (map projr (Net.projectSrcV AID' vl)) (map projr (Net.projectSrcV AID' vl1))
[PROOF STEP]
using assms Source_B_Sink_B_aux
[PROOF STATE]
proof (prove)
using this:
B AID vl vl1
\<lbrakk>list_all isl ?vl; list_all isl ?vl1.0; map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ?vl)) = map Iss.PValS_tgtAPI (filter Iss.isPValS (map projl ?vl1.0))\<rbrakk> \<Longrightarrow> length (map projr (Net.projectSrcV AID' ?vl)) = length (map projr (Net.projectSrcV AID' ?vl1.0))

goal (1 subgoal):
 1. Sink.B (map projr (Net.projectSrcV AID' vl)) (map projr (Net.projectSrcV AID' vl1))
[PROOF STEP]
by (auto simp: Iss.B_def Sink.B_def)


[STATEMENT]
lemma map_projl_Inl: "map (projl o Inl) vl = vl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (projl \<circ> Inl) vl = vl
[PROOF STEP]
by (induction vl) auto


[STATEMENT]
lemma these_map_Inl_projl: "list_all isl vl \<Longrightarrow> these (map (Some o Inl o projl) vl) = vl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all isl vl \<Longrightarrow> these (map (Some \<circ> Inl \<circ> projl) vl) = vl
[PROOF STEP]
by (induction vl) auto


[STATEMENT]
lemma map_projr_Inr: "map (projr o Inr) vl = vl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (projr \<circ> Inr) vl = vl
[PROOF STEP]
by (induction vl) auto


[STATEMENT]
lemma these_map_Inr_projr: "list_all (Not o isl) vl \<Longrightarrow> these (map (Some o Inr o projr) vl) = vl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (Not \<circ> isl) vl \<Longrightarrow> these (map (Some \<circ> Inr \<circ> projr) vl) = vl
[PROOF STEP]
by (induction vl) auto


[STATEMENT]
theorem secure: "secure"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. secure
[PROOF STEP]
proof (intro preserve_source_secure ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (T nid))
[PROOF STEP]
fix aid
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (T nid))
[PROOF STEP]
assume aid: "aid \<in> AIDs - {AID}"
[PROOF STATE]
proof (state)
this:
aid \<in> nodes'

goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (T nid))
[PROOF STEP]
interpret Node: Post_RECEIVER "UIDs aid" PID AID
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (T nid))
[PROOF STEP]
interpret Node': BD_Security_TS_Trans
    istate System_Specification.validTrans srcOf tgtOf Node.\<phi> Node.f Node.\<gamma> Node.g Node.T Node.B
    istate System_Specification.validTrans srcOf tgtOf Node.\<phi> "\<lambda>trn. Inr (Node.f trn)" Node.\<gamma> Node.g Node.T "B aid"
    id id Some "Some o Inr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BD_Security_TS_Trans istate System_Specification.validTrans srcOf tgtOf Node.\<phi> Node.f Node.\<gamma> Node.g Node.T Node.B istate System_Specification.validTrans srcOf tgtOf Node.\<phi> (\<lambda>trn. Inr (Node.f trn)) Node.\<gamma> Node.g Node.T (B aid) id id Some (Some \<circ> Inr)
[PROOF STEP]
proof (unfold_locales, goal_cases)
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn)\<rbrakk> \<Longrightarrow> System_Specification.validTrans (id trn)
 2. \<And>trn' s. \<lbrakk>System_Specification.validTrans trn'; srcOf trn' = id s; System_Specification.reach s\<rbrakk> \<Longrightarrow> \<exists>trn. System_Specification.validTrans trn \<and> srcOf trn = s \<and> id trn = trn'
 3. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn)\<rbrakk> \<Longrightarrow> srcOf (id trn) = id (srcOf trn)
 4. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn)\<rbrakk> \<Longrightarrow> tgtOf (id trn) = id (tgtOf trn)
 5. istate = id istate
 6. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); Node.\<gamma> (id trn)\<rbrakk> \<Longrightarrow> Node.\<gamma> trn \<and> Some (Node.g trn) = Some (Node.g (id trn))
 7. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); Node.\<gamma> trn\<rbrakk> \<Longrightarrow> Node.\<gamma> (id trn) \<or> Some (Node.g trn) = None
 8. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); Node.\<phi> (id trn)\<rbrakk> \<Longrightarrow> Node.\<phi> trn \<and> (Some \<circ> Inr) (Node.f trn) = Some (Inr (Node.f (id trn)))
 9. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); Node.\<phi> trn\<rbrakk> \<Longrightarrow> Node.\<phi> (id trn) \<or> (Some \<circ> Inr) (Node.f trn) = None
 10. \<And>trn. \<lbrakk>Node.T trn; System_Specification.validTrans trn; System_Specification.reach (srcOf trn)\<rbrakk> \<Longrightarrow> Node.T (id trn)
A total of 11 subgoals...
[PROOF STEP]
case (11 vl' vl1' tr)
[PROOF STATE]
proof (state)
this:
B aid vl' vl1'
System_Specification.validFrom istate tr
BD_Security_IO.never Node.T tr
these (map (Some \<circ> Inr) (Node.V tr)) = vl'

goal (11 subgoals):
 1. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn)\<rbrakk> \<Longrightarrow> System_Specification.validTrans (id trn)
 2. \<And>trn' s. \<lbrakk>System_Specification.validTrans trn'; srcOf trn' = id s; System_Specification.reach s\<rbrakk> \<Longrightarrow> \<exists>trn. System_Specification.validTrans trn \<and> srcOf trn = s \<and> id trn = trn'
 3. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn)\<rbrakk> \<Longrightarrow> srcOf (id trn) = id (srcOf trn)
 4. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn)\<rbrakk> \<Longrightarrow> tgtOf (id trn) = id (tgtOf trn)
 5. istate = id istate
 6. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); Node.\<gamma> (id trn)\<rbrakk> \<Longrightarrow> Node.\<gamma> trn \<and> Some (Node.g trn) = Some (Node.g (id trn))
 7. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); Node.\<gamma> trn\<rbrakk> \<Longrightarrow> Node.\<gamma> (id trn) \<or> Some (Node.g trn) = None
 8. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); Node.\<phi> (id trn)\<rbrakk> \<Longrightarrow> Node.\<phi> trn \<and> (Some \<circ> Inr) (Node.f trn) = Some (Inr (Node.f (id trn)))
 9. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); Node.\<phi> trn\<rbrakk> \<Longrightarrow> Node.\<phi> (id trn) \<or> (Some \<circ> Inr) (Node.f trn) = None
 10. \<And>trn. \<lbrakk>Node.T trn; System_Specification.validTrans trn; System_Specification.reach (srcOf trn)\<rbrakk> \<Longrightarrow> Node.T (id trn)
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B aid vl' vl1'
System_Specification.validFrom istate tr
BD_Security_IO.never Node.T tr
these (map (Some \<circ> Inr) (Node.V tr)) = vl'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
B aid vl' vl1'
System_Specification.validFrom istate tr
BD_Security_IO.never Node.T tr
these (map (Some \<circ> Inr) (Node.V tr)) = vl'

goal (1 subgoal):
 1. \<exists>vl1. these (map (Some \<circ> Inr) vl1) = vl1' \<and> Node.B (Node.V tr) vl1
[PROOF STEP]
using aid
[PROOF STATE]
proof (prove)
using this:
B aid vl' vl1'
System_Specification.validFrom istate tr
BD_Security_IO.never Node.T tr
these (map (Some \<circ> Inr) (Node.V tr)) = vl'
aid \<in> nodes'

goal (1 subgoal):
 1. \<exists>vl1. these (map (Some \<circ> Inr) vl1) = vl1' \<and> Node.B (Node.V tr) vl1
[PROOF STEP]
by (intro exI[of _ "map projr vl1'"]) (auto simp: map_projr_Inr these_map_Inr_projr)
[PROOF STATE]
proof (state)
this:
\<exists>vl1. these (map (Some \<circ> Inr) vl1) = vl1' \<and> Node.B (Node.V tr) vl1

goal (10 subgoals):
 1. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn)\<rbrakk> \<Longrightarrow> System_Specification.validTrans (id trn)
 2. \<And>trn' s. \<lbrakk>System_Specification.validTrans trn'; srcOf trn' = id s; System_Specification.reach s\<rbrakk> \<Longrightarrow> \<exists>trn. System_Specification.validTrans trn \<and> srcOf trn = s \<and> id trn = trn'
 3. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn)\<rbrakk> \<Longrightarrow> srcOf (id trn) = id (srcOf trn)
 4. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn)\<rbrakk> \<Longrightarrow> tgtOf (id trn) = id (tgtOf trn)
 5. istate = id istate
 6. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); Node.\<gamma> (id trn)\<rbrakk> \<Longrightarrow> Node.\<gamma> trn \<and> Some (Node.g trn) = Some (Node.g (id trn))
 7. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); Node.\<gamma> trn\<rbrakk> \<Longrightarrow> Node.\<gamma> (id trn) \<or> Some (Node.g trn) = None
 8. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); Node.\<phi> (id trn)\<rbrakk> \<Longrightarrow> Node.\<phi> trn \<and> (Some \<circ> Inr) (Node.f trn) = Some (Inr (Node.f (id trn)))
 9. \<And>trn. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); Node.\<phi> trn\<rbrakk> \<Longrightarrow> Node.\<phi> (id trn) \<or> (Some \<circ> Inr) (Node.f trn) = None
 10. \<And>trn. \<lbrakk>Node.T trn; System_Specification.validTrans trn; System_Specification.reach (srcOf trn)\<rbrakk> \<Longrightarrow> Node.T (id trn)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (T nid))
[PROOF STEP]
show "Net.lsecure aid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV aid) (Net.lO aid) (B aid) (BD_Security_IO.never (T aid))
[PROOF STEP]
using aid Node.Post_secure Node'.translate_secure
[PROOF STATE]
proof (prove)
using this:
aid \<in> nodes'
Node.secure
Node.secure \<Longrightarrow> Node'.secure

goal (1 subgoal):
 1. Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV aid) (Net.lO aid) (B aid) (BD_Security_IO.never (T aid))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV aid) (Net.lO aid) (B aid) (BD_Security_IO.never (T aid))

goal:
No subgoals!
[PROOF STEP]
qed