[STATEMENT]
lemma OK_None_states [iff]: "OK None \<in> states P mxs mxl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK None \<in> states P mxs mxl
[PROOF STEP]
by(simp add: JVM_states_unfold)


[STATEMENT]
lemma after_in_states:
 "\<lbrakk> P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; size ST + max_stack e \<le> mxs \<rbrakk>
 \<Longrightarrow> OK (after E A ST e) \<in> states P mxs mxl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs\<rbrakk> \<Longrightarrow> OK (after E A ST e) \<in> states P mxs mxl
[PROOF STEP]
apply(subgoal_tac "size ST + 1 \<le> mxs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs; length ST + 1 \<le> mxs\<rbrakk> \<Longrightarrow> OK (after E A ST e) \<in> states P mxs mxl
 2. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs\<rbrakk> \<Longrightarrow> length ST + 1 \<le> mxs
[PROOF STEP]
apply(simp add:after_def ty\<^sub>i'_def JVM_states_unfold ty\<^sub>l_in_types)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs; Suc (length ST) \<le> mxs\<rbrakk> \<Longrightarrow> (\<exists>x2. A \<squnion> \<A> e = \<lfloor>x2\<rfloor>) \<longrightarrow> (\<exists>x. (\<exists>n. x = list n (types P) \<and> n \<le> mxs) \<and> T # ST \<in> x)
 2. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs\<rbrakk> \<Longrightarrow> length ST + 1 \<le> mxs
[PROOF STEP]
apply(clarify intro!: exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs; Suc (length ST) \<le> mxs; A \<squnion> \<A> e = \<lfloor>x2\<rfloor>\<rbrakk> \<Longrightarrow> (\<exists>n. ?x7 = list n (types P) \<and> n \<le> mxs) \<and> T # ST \<in> ?x7
 2. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs\<rbrakk> \<Longrightarrow> length ST + 1 \<le> mxs
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs; Suc (length ST) \<le> mxs; A \<squnion> \<A> e = \<lfloor>x2\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>n. ?x7 = list n (types P) \<and> n \<le> mxs
 2. \<And>x2. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs; Suc (length ST) \<le> mxs; A \<squnion> \<A> e = \<lfloor>x2\<rfloor>\<rbrakk> \<Longrightarrow> T # ST \<in> ?x7
 3. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs\<rbrakk> \<Longrightarrow> length ST + 1 \<le> mxs
[PROOF STEP]
apply(rule exI[where x="length ST + 1"], fastforce)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs; Suc (length ST) \<le> mxs; A \<squnion> \<A> e = \<lfloor>x2\<rfloor>\<rbrakk> \<Longrightarrow> T # ST \<in> list (Suc (length ST)) (types P)
 2. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs\<rbrakk> \<Longrightarrow> length ST + 1 \<le> mxs
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs; Suc (length ST) \<le> mxs; A \<squnion> \<A> e = \<lfloor>x2\<rfloor>\<rbrakk> \<Longrightarrow> is_type P T \<and> ST \<in> list (length ST) (types P)
 2. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs\<rbrakk> \<Longrightarrow> length ST + 1 \<le> mxs
[PROOF STEP]
apply(rule conjI[OF WT1_is_type[OF wf_prog]], auto intro: listI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs\<rbrakk> \<Longrightarrow> Suc (length ST) \<le> mxs
[PROOF STEP]
using max_stack1[of e]
[PROOF STATE]
proof (prove)
using this:
1 \<le> max_stack e

goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P; length ST + max_stack e \<le> mxs\<rbrakk> \<Longrightarrow> Suc (length ST) \<le> mxs
[PROOF STEP]
by simp


[STATEMENT]
lemma OK_ty\<^sub>i'_in_statesI [simp]:
  "\<lbrakk> set E \<subseteq> types P; set ST \<subseteq> types P; size ST \<le> mxs \<rbrakk>
  \<Longrightarrow> OK (ty\<^sub>i' ST E A) \<in> states P mxs mxl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set E \<subseteq> types P; set ST \<subseteq> types P; length ST \<le> mxs\<rbrakk> \<Longrightarrow> OK (ty\<^sub>i' ST E A) \<in> states P mxs mxl
[PROOF STEP]
apply(simp add:ty\<^sub>i'_def JVM_states_unfold ty\<^sub>l_in_types)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set E \<subseteq> types P; set ST \<subseteq> types P; length ST \<le> mxs\<rbrakk> \<Longrightarrow> (\<exists>x2. A = \<lfloor>x2\<rfloor>) \<longrightarrow> (\<exists>x. (\<exists>n. x = list n (types P) \<and> n \<le> mxs) \<and> ST \<in> x)
[PROOF STEP]
apply(blast intro!:listI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_class_type_aux: "is_class P C \<Longrightarrow> is_type P (Class C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_class P C \<Longrightarrow> is_type P (Class C)
[PROOF STEP]
by(simp)


[STATEMENT]
lemma wt_instrs_Nil [simp]: "\<tau>s \<noteq> [] \<Longrightarrow> \<turnstile> [],[] [::] \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>s \<noteq> [] \<Longrightarrow> \<turnstile> [], [] [::] \<tau>s
[PROOF STEP]
by(simp add:wt_defs)


[STATEMENT]
lemma eff_None [simp]: "eff i P pc et None = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eff i P pc et None = []
[PROOF STEP]
by (simp add: Effect.eff_def)


[STATEMENT]
lemma wt_instr_appR:
 "\<lbrakk> P,T,m,mpc,xt \<turnstile> is!pc,pc :: \<tau>s;
    pc < size is; size is < size \<tau>s; mpc \<le> size \<tau>s; mpc \<le> mpc' \<rbrakk>
  \<Longrightarrow> P,T,m,mpc',xt \<turnstile> is!pc,pc :: \<tau>s@\<tau>s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,T,m,mpc,xt \<turnstile> is ! pc,pc :: \<tau>s; pc < length is; length is < length \<tau>s; mpc \<le> length \<tau>s; mpc \<le> mpc'\<rbrakk> \<Longrightarrow> P,T,m,mpc',xt \<turnstile> is ! pc,pc :: \<tau>s @ \<tau>s'
[PROOF STEP]
by (fastforce simp:wt_instr_def app_def)


[STATEMENT]
lemma relevant_entries_shift [simp]:
  "relevant_entries P i (pc+n) (shift n xt) = shift n (relevant_entries P i pc xt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relevant_entries P i (pc + n) (shift n xt) = shift n (relevant_entries P i pc xt)
[PROOF STEP]
apply (induct xt)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. relevant_entries P i (pc + n) (shift n []) = shift n (relevant_entries P i pc [])
 2. \<And>a xt. relevant_entries P i (pc + n) (shift n xt) = shift n (relevant_entries P i pc xt) \<Longrightarrow> relevant_entries P i (pc + n) (shift n (a # xt)) = shift n (relevant_entries P i pc (a # xt))
[PROOF STEP]
apply (unfold relevant_entries_def shift_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. filter (is_relevant_entry P i (pc + n)) (map (\<lambda>(from, to, C, handler, depth). (n + from, n + to, C, n + handler, depth)) []) = map (\<lambda>(from, to, C, handler, depth). (n + from, n + to, C, n + handler, depth)) (filter (is_relevant_entry P i pc) [])
 2. \<And>a xt. filter (is_relevant_entry P i (pc + n)) (map (\<lambda>(from, to, C, handler, depth). (n + from, n + to, C, n + handler, depth)) xt) = map (\<lambda>(from, to, C, handler, depth). (n + from, n + to, C, n + handler, depth)) (filter (is_relevant_entry P i pc) xt) \<Longrightarrow> filter (is_relevant_entry P i (pc + n)) (map (\<lambda>(from, to, C, handler, depth). (n + from, n + to, C, n + handler, depth)) (a # xt)) = map (\<lambda>(from, to, C, handler, depth). (n + from, n + to, C, n + handler, depth)) (filter (is_relevant_entry P i pc) (a # xt))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xt. filter (is_relevant_entry P i (pc + n)) (map (\<lambda>(from, to, C, handler, depth). (n + from, n + to, C, n + handler, depth)) xt) = map (\<lambda>(from, to, C, handler, depth). (n + from, n + to, C, n + handler, depth)) (filter (is_relevant_entry P i pc) xt) \<Longrightarrow> filter (is_relevant_entry P i (pc + n)) (map (\<lambda>(from, to, C, handler, depth). (n + from, n + to, C, n + handler, depth)) (a # xt)) = map (\<lambda>(from, to, C, handler, depth). (n + from, n + to, C, n + handler, depth)) (filter (is_relevant_entry P i pc) (a # xt))
[PROOF STEP]
apply (auto simp add: is_relevant_entry_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma xcpt_eff_shift [simp]:
  "xcpt_eff i P (pc+n) \<tau> (shift n xt) =
   map (\<lambda>(pc,\<tau>). (pc + n, \<tau>)) (xcpt_eff i P pc \<tau> xt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xcpt_eff i P (pc + n) \<tau> (shift n xt) = map (\<lambda>(pc, \<tau>). (pc + n, \<tau>)) (xcpt_eff i P pc \<tau> xt)
[PROOF STEP]
apply(simp add: xcpt_eff_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case \<tau> of (ST, LT) \<Rightarrow> map (\<lambda>(f, t, C, h, d). (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length ST - d) ST, LT)\<rfloor>)) (shift n (relevant_entries P i pc xt))) = map (\<lambda>(pc, \<tau>). (pc + n, \<tau>)) (case \<tau> of (ST, LT) \<Rightarrow> map (\<lambda>(f, t, C, h, d). (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length ST - d) ST, LT)\<rfloor>)) (relevant_entries P i pc xt))
[PROOF STEP]
apply(cases \<tau>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<tau> = (a, b) \<Longrightarrow> (case \<tau> of (ST, LT) \<Rightarrow> map (\<lambda>(f, t, C, h, d). (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length ST - d) ST, LT)\<rfloor>)) (shift n (relevant_entries P i pc xt))) = map (\<lambda>(pc, \<tau>). (pc + n, \<tau>)) (case \<tau> of (ST, LT) \<Rightarrow> map (\<lambda>(f, t, C, h, d). (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length ST - d) ST, LT)\<rfloor>)) (relevant_entries P i pc xt))
[PROOF STEP]
apply(auto simp add: shift_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma  eff_shift [simp]:
  "app\<^sub>i (i, P, pc, m, T, \<tau>) \<Longrightarrow>
   eff i P (pc+n) (shift n xt) (Some \<tau>) =
   map (\<lambda>(pc,\<tau>). (pc+n,\<tau>)) (eff i P pc xt (Some \<tau>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, m, T, \<tau>) \<Longrightarrow> eff i P (pc + n) (shift n xt) \<lfloor>\<tau>\<rfloor> = map (\<lambda>(pc, \<tau>). (pc + n, \<tau>)) (eff i P pc xt \<lfloor>\<tau>\<rfloor>)
[PROOF STEP]
apply(simp add:eff_def norm_eff_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, m, T, \<tau>) \<Longrightarrow> map (\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, \<tau>)\<rfloor>)) (succs i \<tau> (pc + n)) = map ((\<lambda>(pc, y). (pc + n, y)) \<circ> (\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, \<tau>)\<rfloor>))) (succs i \<tau> pc)
[PROOF STEP]
apply(cases "i",auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma xcpt_app_shift [simp]:
  "xcpt_app i P (pc+n) m (shift n xt) \<tau> = xcpt_app i P pc m xt \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xcpt_app i P (pc + n) m (shift n xt) \<tau> = xcpt_app i P pc m xt \<tau>
[PROOF STEP]
by (simp add: xcpt_app_def) (auto simp add: shift_def)


[STATEMENT]
lemma wt_instr_appL:
  "\<lbrakk> P,T,m,mpc,xt \<turnstile> i,pc :: \<tau>s; pc < size \<tau>s; mpc \<le> size \<tau>s \<rbrakk>
  \<Longrightarrow> P,T,m,mpc + size \<tau>s',shift (size \<tau>s') xt \<turnstile> i,pc+size \<tau>s' :: \<tau>s'@\<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,T,m,mpc,xt \<turnstile> i,pc :: \<tau>s; pc < length \<tau>s; mpc \<le> length \<tau>s\<rbrakk> \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
apply(clarsimp simp add: wt_instr_def app_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>pc < length \<tau>s; mpc \<le> length \<tau>s; \<tau>s ! pc = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (i, P, pc, m, T, aa, ba); xcpt_app i P pc m xt (aa, ba); \<forall>x\<in>set (eff i P pc xt \<lfloor>(aa, ba)\<rfloor>). case x of (pc', \<tau>') \<Rightarrow> pc' < mpc; \<forall>x\<in>set (eff i P pc xt \<lfloor>(aa, ba)\<rfloor>). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' \<tau>s ! pc'\<rbrakk> \<Longrightarrow> app\<^sub>i (i, P, pc + length \<tau>s', m, T, aa, ba) \<and> (\<forall>x\<in>set (eff i P pc xt \<lfloor>(aa, ba)\<rfloor>). case case x of (pc, x) \<Rightarrow> (pc + length \<tau>s', x) of (pc', \<tau>') \<Rightarrow> pc' < mpc + length \<tau>s') \<and> (\<forall>x\<in>set (eff i P pc xt \<lfloor>(aa, ba)\<rfloor>). case case x of (pc, x) \<Rightarrow> (pc + length \<tau>s', x) of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s' then \<tau>s' ! pc' else \<tau>s ! (pc' - length \<tau>s')))
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>pc < length \<tau>s; mpc \<le> length \<tau>s; \<tau>s ! pc = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (i, P, pc, m, T, aa, ba); xcpt_app i P pc m xt (aa, ba); \<forall>x\<in>set (eff i P pc xt \<lfloor>(aa, ba)\<rfloor>). case x of (pc', \<tau>') \<Rightarrow> pc' < mpc; \<forall>x\<in>set (eff i P pc xt \<lfloor>(aa, ba)\<rfloor>). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' \<tau>s ! pc'\<rbrakk> \<Longrightarrow> app\<^sub>i (i, P, pc + length \<tau>s', m, T, aa, ba)
[PROOF STEP]
apply(cases "i", auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wt_instr_Cons:
  "\<lbrakk> P,T,m,mpc - 1,[] \<turnstile> i,pc - 1 :: \<tau>s;
     0 < pc; 0 < mpc; pc < size \<tau>s + 1; mpc \<le> size \<tau>s + 1 \<rbrakk>
  \<Longrightarrow> P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>#\<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,T,m,mpc - 1,[] \<turnstile> i,pc - 1 :: \<tau>s; 0 < pc; 0 < mpc; pc < length \<tau>s + 1; mpc \<le> length \<tau>s + 1\<rbrakk> \<Longrightarrow> P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s
[PROOF STEP]
apply(drule wt_instr_appL[where \<tau>s' = "[\<tau>]"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < pc; 0 < mpc; pc < length \<tau>s + 1; mpc \<le> length \<tau>s + 1\<rbrakk> \<Longrightarrow> pc - 1 < length \<tau>s
 2. \<lbrakk>0 < pc; 0 < mpc; pc < length \<tau>s + 1; mpc \<le> length \<tau>s + 1\<rbrakk> \<Longrightarrow> mpc - 1 \<le> length \<tau>s
 3. \<lbrakk>0 < pc; 0 < mpc; pc < length \<tau>s + 1; mpc \<le> length \<tau>s + 1; P,T,m,mpc - 1 + length [\<tau>],shift (length [\<tau>]) [] \<turnstile> i,pc - 1 + length [\<tau>] :: [\<tau>] @ \<tau>s\<rbrakk> \<Longrightarrow> P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < pc; 0 < mpc; pc < length \<tau>s + 1; mpc \<le> length \<tau>s + 1\<rbrakk> \<Longrightarrow> mpc - 1 \<le> length \<tau>s
 2. \<lbrakk>0 < pc; 0 < mpc; pc < length \<tau>s + 1; mpc \<le> length \<tau>s + 1; P,T,m,mpc - 1 + length [\<tau>],shift (length [\<tau>]) [] \<turnstile> i,pc - 1 + length [\<tau>] :: [\<tau>] @ \<tau>s\<rbrakk> \<Longrightarrow> P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < pc; 0 < mpc; pc < length \<tau>s + 1; mpc \<le> length \<tau>s + 1; P,T,m,mpc - 1 + length [\<tau>],shift (length [\<tau>]) [] \<turnstile> i,pc - 1 + length [\<tau>] :: [\<tau>] @ \<tau>s\<rbrakk> \<Longrightarrow> P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s
[PROOF STEP]
apply (simp split:nat_diff_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wt_instr_append:
  "\<lbrakk> P,T,m,mpc - size \<tau>s',[] \<turnstile> i,pc - size \<tau>s' :: \<tau>s;
     size \<tau>s' \<le> pc; size \<tau>s' \<le> mpc; pc < size \<tau>s + size \<tau>s'; mpc \<le> size \<tau>s + size \<tau>s' \<rbrakk>
  \<Longrightarrow> P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s'@\<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,T,m,mpc - length \<tau>s',[] \<turnstile> i,pc - length \<tau>s' :: \<tau>s; length \<tau>s' \<le> pc; length \<tau>s' \<le> mpc; pc < length \<tau>s + length \<tau>s'; mpc \<le> length \<tau>s + length \<tau>s'\<rbrakk> \<Longrightarrow> P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
apply(drule wt_instr_appL[where \<tau>s' = \<tau>s'])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length \<tau>s' \<le> pc; length \<tau>s' \<le> mpc; pc < length \<tau>s + length \<tau>s'; mpc \<le> length \<tau>s + length \<tau>s'\<rbrakk> \<Longrightarrow> pc - length \<tau>s' < length \<tau>s
 2. \<lbrakk>length \<tau>s' \<le> pc; length \<tau>s' \<le> mpc; pc < length \<tau>s + length \<tau>s'; mpc \<le> length \<tau>s + length \<tau>s'\<rbrakk> \<Longrightarrow> mpc - length \<tau>s' \<le> length \<tau>s
 3. \<lbrakk>length \<tau>s' \<le> pc; length \<tau>s' \<le> mpc; pc < length \<tau>s + length \<tau>s'; mpc \<le> length \<tau>s + length \<tau>s'; P,T,m,mpc - length \<tau>s' + length \<tau>s',shift (length \<tau>s') [] \<turnstile> i,pc - length \<tau>s' + length \<tau>s' :: \<tau>s' @ \<tau>s\<rbrakk> \<Longrightarrow> P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length \<tau>s' \<le> pc; length \<tau>s' \<le> mpc; pc < length \<tau>s + length \<tau>s'; mpc \<le> length \<tau>s + length \<tau>s'\<rbrakk> \<Longrightarrow> mpc - length \<tau>s' \<le> length \<tau>s
 2. \<lbrakk>length \<tau>s' \<le> pc; length \<tau>s' \<le> mpc; pc < length \<tau>s + length \<tau>s'; mpc \<le> length \<tau>s + length \<tau>s'; P,T,m,mpc - length \<tau>s' + length \<tau>s',shift (length \<tau>s') [] \<turnstile> i,pc - length \<tau>s' + length \<tau>s' :: \<tau>s' @ \<tau>s\<rbrakk> \<Longrightarrow> P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length \<tau>s' \<le> pc; length \<tau>s' \<le> mpc; pc < length \<tau>s + length \<tau>s'; mpc \<le> length \<tau>s + length \<tau>s'; P,T,m,mpc - length \<tau>s' + length \<tau>s',shift (length \<tau>s') [] \<turnstile> i,pc - length \<tau>s' + length \<tau>s' :: \<tau>s' @ \<tau>s\<rbrakk> \<Longrightarrow> P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
apply (simp split:nat_diff_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma xcpt_app_pcs:
  "pc \<notin> pcs xt \<Longrightarrow> xcpt_app i P pc mxs xt \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc \<notin> pcs xt \<Longrightarrow> xcpt_app i P pc mxs xt \<tau>
[PROOF STEP]
by (auto simp add: xcpt_app_def relevant_entries_def is_relevant_entry_def pcs_def)


[STATEMENT]
lemma xcpt_eff_pcs:
  "pc \<notin> pcs xt \<Longrightarrow> xcpt_eff i P pc \<tau> xt = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc \<notin> pcs xt \<Longrightarrow> xcpt_eff i P pc \<tau> xt = []
[PROOF STEP]
by (cases \<tau>)
   (auto simp add: is_relevant_entry_def xcpt_eff_def relevant_entries_def pcs_def
           intro!: filter_False)


[STATEMENT]
lemma pcs_shift:
  "pc < n \<Longrightarrow> pc \<notin> pcs (shift n xt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < n \<Longrightarrow> pc \<notin> pcs (shift n xt)
[PROOF STEP]
by (auto simp add: shift_def pcs_def)


[STATEMENT]
lemma xcpt_eff_shift_pc_ge_n: assumes "x \<in> set (xcpt_eff i P pc \<tau> (shift n xt))"
  shows "n \<le> pc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> pc
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<le> pc
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<le> pc
[PROOF STEP]
assume "pc < n"
[PROOF STATE]
proof (state)
this:
pc < n

goal (1 subgoal):
 1. n \<le> pc
[PROOF STEP]
hence "pc \<notin> pcs (shift n xt)"
[PROOF STATE]
proof (prove)
using this:
pc < n

goal (1 subgoal):
 1. pc \<notin> pcs (shift n xt)
[PROOF STEP]
by(rule pcs_shift)
[PROOF STATE]
proof (state)
this:
pc \<notin> pcs (shift n xt)

goal (1 subgoal):
 1. n \<le> pc
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (xcpt_eff i P pc \<tau> (shift n xt))
pc \<notin> pcs (shift n xt)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
x \<in> set (xcpt_eff i P pc \<tau> (shift n xt))
pc \<notin> pcs (shift n xt)

goal (1 subgoal):
 1. False
[PROOF STEP]
by(auto simp add: pcs_def xcpt_eff_def is_relevant_entry_def relevant_entries_def split_beta cong: filter_cong)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. n \<le> pc
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
pc < n \<Longrightarrow> False

goal (1 subgoal):
 1. n \<le> pc
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
pc < n \<Longrightarrow> False

goal (1 subgoal):
 1. n \<le> pc
[PROOF STEP]
by(cases "n \<le> pc")(auto)
[PROOF STATE]
proof (state)
this:
n \<le> pc

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wt_instr_appRx:
  "\<lbrakk> P,T,m,mpc,xt \<turnstile> is!pc,pc :: \<tau>s; pc < size is; size is < size \<tau>s; mpc \<le> size \<tau>s \<rbrakk>
  \<Longrightarrow> P,T,m,mpc,xt @ shift (size is) xt' \<turnstile> is!pc,pc :: \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,T,m,mpc,xt \<turnstile> is ! pc,pc :: \<tau>s; pc < length is; length is < length \<tau>s; mpc \<le> length \<tau>s\<rbrakk> \<Longrightarrow> P,T,m,mpc,xt @ shift (length is) xt' \<turnstile> is ! pc,pc :: \<tau>s
[PROOF STEP]
apply(clarsimp simp:wt_instr_def eff_def app_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>pc < length is; length is < length \<tau>s; mpc \<le> length \<tau>s; \<tau>s ! pc = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (is ! pc, P, pc, m, T, aa, ba); xcpt_app (is ! pc) P pc m xt (aa, ba); \<forall>x\<in>set (norm_eff (is ! pc) P pc (aa, ba)) \<union> set (xcpt_eff (is ! pc) P pc (aa, ba) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < mpc; \<forall>a b. ((a, b) \<in> set (norm_eff (is ! pc) P pc (aa, ba)) \<longrightarrow> P \<turnstile> b \<le>' \<tau>s ! a) \<and> ((a, b) \<in> set (xcpt_eff (is ! pc) P pc (aa, ba) xt) \<longrightarrow> P \<turnstile> b \<le>' \<tau>s ! a)\<rbrakk> \<Longrightarrow> xcpt_app (is ! pc) P pc m (shift (length is) xt') (aa, ba) \<and> (\<forall>x\<in>set (norm_eff (is ! pc) P pc (aa, ba)) \<union> (set (xcpt_eff (is ! pc) P pc (aa, ba) xt) \<union> set (xcpt_eff (is ! pc) P pc (aa, ba) (shift (length is) xt'))). case x of (pc', \<tau>') \<Rightarrow> pc' < mpc) \<and> (\<forall>a b. (a, b) \<in> set (xcpt_eff (is ! pc) P pc (aa, ba) (shift (length is) xt')) \<longrightarrow> P \<turnstile> b \<le>' \<tau>s ! a)
[PROOF STEP]
apply(fastforce dest: xcpt_eff_shift_pc_ge_n intro!: xcpt_app_pcs[OF pcs_shift])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wt_instr_appLx:
  "\<lbrakk> P,T,m,mpc,xt \<turnstile> i,pc :: \<tau>s; pc \<notin> pcs xt' \<rbrakk>
  \<Longrightarrow> P,T,m,mpc,xt'@xt \<turnstile> i,pc :: \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,T,m,mpc,xt \<turnstile> i,pc :: \<tau>s; pc \<notin> pcs xt'\<rbrakk> \<Longrightarrow> P,T,m,mpc,xt' @ xt \<turnstile> i,pc :: \<tau>s
[PROOF STEP]
by (auto simp:wt_instr_def app_def eff_def xcpt_app_pcs xcpt_eff_pcs)


[STATEMENT]
lemma wt_instrs_extR:
  "\<turnstile> is,xt [::] \<tau>s \<Longrightarrow> \<turnstile> is,xt [::] \<tau>s @ \<tau>s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s \<Longrightarrow> \<turnstile> is, xt [::] \<tau>s @ \<tau>s'
[PROOF STEP]
by(auto simp add:wt_instrs_def wt_instr_appR)


[STATEMENT]
lemma wt_instrs_ext:
  "\<lbrakk> \<turnstile> is\<^sub>1,xt\<^sub>1 [::] \<tau>s\<^sub>1@\<tau>s\<^sub>2; \<turnstile> is\<^sub>2,xt\<^sub>2 [::] \<tau>s\<^sub>2; size \<tau>s\<^sub>1 = size is\<^sub>1 \<rbrakk>
  \<Longrightarrow> \<turnstile> is\<^sub>1@is\<^sub>2, xt\<^sub>1 @ shift (size is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1@\<tau>s\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<turnstile> is\<^sub>1, xt\<^sub>1 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2; \<turnstile> is\<^sub>2, xt\<^sub>2 [::] \<tau>s\<^sub>2; length \<tau>s\<^sub>1 = length is\<^sub>1\<rbrakk> \<Longrightarrow> \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
apply(clarsimp simp:wt_instrs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; \<forall>pc<length is\<^sub>1. P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 \<turnstile> is\<^sub>1 ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<forall>pc<length is\<^sub>2. P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! pc,pc :: \<tau>s\<^sub>2\<rbrakk> \<Longrightarrow> pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1 + length is\<^sub>2} \<and> (+) (length is\<^sub>1) ` pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>1 + length is\<^sub>2} \<and> (\<forall>pc. (pc < length is\<^sub>1 \<longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>1 ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2) \<and> (\<not> pc < length is\<^sub>1 \<longrightarrow> pc < length is\<^sub>1 + length is\<^sub>2 \<longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2))
[PROOF STEP]
apply(rule conjI, fastforce)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; \<forall>pc<length is\<^sub>1. P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 \<turnstile> is\<^sub>1 ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<forall>pc<length is\<^sub>2. P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! pc,pc :: \<tau>s\<^sub>2\<rbrakk> \<Longrightarrow> (+) (length is\<^sub>1) ` pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>1 + length is\<^sub>2} \<and> (\<forall>pc. (pc < length is\<^sub>1 \<longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>1 ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2) \<and> (\<not> pc < length is\<^sub>1 \<longrightarrow> pc < length is\<^sub>1 + length is\<^sub>2 \<longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2))
[PROOF STEP]
apply(rule conjI, fastforce simp add: pcs_shift_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; \<forall>pc<length is\<^sub>1. P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 \<turnstile> is\<^sub>1 ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<forall>pc<length is\<^sub>2. P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! pc,pc :: \<tau>s\<^sub>2\<rbrakk> \<Longrightarrow> \<forall>pc. (pc < length is\<^sub>1 \<longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>1 ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2) \<and> (\<not> pc < length is\<^sub>1 \<longrightarrow> pc < length is\<^sub>1 + length is\<^sub>2 \<longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; \<forall>pc<length is\<^sub>1. P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 \<turnstile> is\<^sub>1 ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<forall>pc<length is\<^sub>2. P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! pc,pc :: \<tau>s\<^sub>2\<rbrakk> \<Longrightarrow> (pc < length is\<^sub>1 \<longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>1 ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2) \<and> (\<not> pc < length is\<^sub>1 \<longrightarrow> pc < length is\<^sub>1 + length is\<^sub>2 \<longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2)
[PROOF STEP]
apply(rule conjI, fastforce simp:wt_instr_appRx)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; \<forall>pc<length is\<^sub>1. P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 \<turnstile> is\<^sub>1 ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<forall>pc<length is\<^sub>2. P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! pc,pc :: \<tau>s\<^sub>2\<rbrakk> \<Longrightarrow> \<not> pc < length is\<^sub>1 \<longrightarrow> pc < length is\<^sub>1 + length is\<^sub>2 \<longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; \<forall>pc<length is\<^sub>1. P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 \<turnstile> is\<^sub>1 ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<forall>pc<length is\<^sub>2. P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! pc,pc :: \<tau>s\<^sub>2; \<not> pc < length is\<^sub>1; pc < length is\<^sub>1 + length is\<^sub>2\<rbrakk> \<Longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
apply(erule_tac x = "pc - size is\<^sub>1" in allE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<not> pc < length is\<^sub>1; pc < length is\<^sub>1 + length is\<^sub>2; pc - length is\<^sub>1 < length is\<^sub>1 \<longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 \<turnstile> is\<^sub>1 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2; pc - length is\<^sub>1 < length is\<^sub>2 \<longrightarrow> P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 :: \<tau>s\<^sub>2\<rbrakk> \<Longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
apply(thin_tac "P \<longrightarrow> Q" for P Q)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<not> pc < length is\<^sub>1; pc < length is\<^sub>1 + length is\<^sub>2; pc - length is\<^sub>1 < length is\<^sub>2 \<longrightarrow> P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 :: \<tau>s\<^sub>2\<rbrakk> \<Longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
apply(erule impE, arith)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<not> pc < length is\<^sub>1; pc < length is\<^sub>1 + length is\<^sub>2; P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 :: \<tau>s\<^sub>2\<rbrakk> \<Longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
apply(drule_tac \<tau>s' = "\<tau>s\<^sub>1" in wt_instr_appL)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>pc. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<not> pc < length is\<^sub>1; pc < length is\<^sub>1 + length is\<^sub>2\<rbrakk> \<Longrightarrow> pc - length is\<^sub>1 < length \<tau>s\<^sub>2
 2. \<And>pc. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<not> pc < length is\<^sub>1; pc < length is\<^sub>1 + length is\<^sub>2\<rbrakk> \<Longrightarrow> length \<tau>s\<^sub>2 \<le> length \<tau>s\<^sub>2
 3. \<And>pc. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<not> pc < length is\<^sub>1; pc < length is\<^sub>1 + length is\<^sub>2; P,T\<^sub>r,mxs,length \<tau>s\<^sub>2 + length \<tau>s\<^sub>1,shift (length \<tau>s\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 + length \<tau>s\<^sub>1 :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2\<rbrakk> \<Longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<not> pc < length is\<^sub>1; pc < length is\<^sub>1 + length is\<^sub>2\<rbrakk> \<Longrightarrow> length \<tau>s\<^sub>2 \<le> length \<tau>s\<^sub>2
 2. \<And>pc. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<not> pc < length is\<^sub>1; pc < length is\<^sub>1 + length is\<^sub>2; P,T\<^sub>r,mxs,length \<tau>s\<^sub>2 + length \<tau>s\<^sub>1,shift (length \<tau>s\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 + length \<tau>s\<^sub>1 :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2\<rbrakk> \<Longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>length \<tau>s\<^sub>1 = length is\<^sub>1; \<tau>s\<^sub>2 \<noteq> []; length is\<^sub>2 < length \<tau>s\<^sub>2; pcs xt\<^sub>1 \<subseteq> {0..<length is\<^sub>1}; pcs xt\<^sub>2 \<subseteq> {0..<length is\<^sub>2}; \<not> pc < length is\<^sub>1; pc < length is\<^sub>1 + length is\<^sub>2; P,T\<^sub>r,mxs,length \<tau>s\<^sub>2 + length \<tau>s\<^sub>1,shift (length \<tau>s\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 + length \<tau>s\<^sub>1 :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2\<rbrakk> \<Longrightarrow> P,T\<^sub>r,mxs,length is\<^sub>1 + length \<tau>s\<^sub>2,xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
apply(fastforce simp add:add.commute intro!: wt_instr_appLx)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wt_instrs_last_incr[trans]:
  "\<lbrakk> \<turnstile> is,xt [::] \<tau>s@[\<tau>]; P \<turnstile> \<tau> \<le>' \<tau>' \<rbrakk> \<Longrightarrow> \<turnstile> is,xt [::] \<tau>s@[\<tau>']"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<turnstile> is, xt [::] \<tau>s @ [\<tau>]; P \<turnstile> \<tau> \<le>' \<tau>'\<rbrakk> \<Longrightarrow> \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
apply(clarsimp simp add:wt_instrs_def wt_instr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc a b. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; \<forall>pc<length is. app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc) \<and> (\<forall>x\<in>set (eff (is ! pc) P pc xt (\<tau>s ! pc)). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s then \<tau>s ! pc' else [\<tau>] ! (pc' - length \<tau>s))); pc < length is; (a, b) \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc))\<rbrakk> \<Longrightarrow> (a < length \<tau>s \<longrightarrow> P \<turnstile> b \<le>' \<tau>s ! a) \<and> (\<not> a < length \<tau>s \<longrightarrow> P \<turnstile> b \<le>' [\<tau>'] ! (a - length \<tau>s))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc a b. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; \<forall>pc<length is. app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc) \<and> (\<forall>x\<in>set (eff (is ! pc) P pc xt (\<tau>s ! pc)). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s then \<tau>s ! pc' else [\<tau>] ! (pc' - length \<tau>s))); pc < length is; (a, b) \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc))\<rbrakk> \<Longrightarrow> a < length \<tau>s \<longrightarrow> P \<turnstile> b \<le>' \<tau>s ! a
 2. \<And>pc a b. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; \<forall>pc<length is. app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc) \<and> (\<forall>x\<in>set (eff (is ! pc) P pc xt (\<tau>s ! pc)). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s then \<tau>s ! pc' else [\<tau>] ! (pc' - length \<tau>s))); pc < length is; (a, b) \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc))\<rbrakk> \<Longrightarrow> \<not> a < length \<tau>s \<longrightarrow> P \<turnstile> b \<le>' [\<tau>'] ! (a - length \<tau>s)
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc a b. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; \<forall>pc<length is. app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc) \<and> (\<forall>x\<in>set (eff (is ! pc) P pc xt (\<tau>s ! pc)). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s then \<tau>s ! pc' else [\<tau>] ! (pc' - length \<tau>s))); pc < length is; (a, b) \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc))\<rbrakk> \<Longrightarrow> \<not> a < length \<tau>s \<longrightarrow> P \<turnstile> b \<le>' [\<tau>'] ! (a - length \<tau>s)
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc a b. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; \<forall>pc<length is. app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc) \<and> (\<forall>x\<in>set (eff (is ! pc) P pc xt (\<tau>s ! pc)). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s then \<tau>s ! pc' else [\<tau>] ! (pc' - length \<tau>s))); pc < length is; (a, b) \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc)); \<not> a < length \<tau>s\<rbrakk> \<Longrightarrow> P \<turnstile> b \<le>' [\<tau>'] ! (a - length \<tau>s)
[PROOF STEP]
apply(rename_tac pc' tau')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc pc' tau'. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; \<forall>pc<length is. app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc) \<and> (\<forall>x\<in>set (eff (is ! pc) P pc xt (\<tau>s ! pc)). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s then \<tau>s ! pc' else [\<tau>] ! (pc' - length \<tau>s))); pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc)); \<not> pc' < length \<tau>s\<rbrakk> \<Longrightarrow> P \<turnstile> tau' \<le>' [\<tau>'] ! (pc' - length \<tau>s)
[PROOF STEP]
apply(erule allE, erule (1) impE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc pc' tau'. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc)); \<not> pc' < length \<tau>s; app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc) \<and> (\<forall>x\<in>set (eff (is ! pc) P pc xt (\<tau>s ! pc)). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s then \<tau>s ! pc' else [\<tau>] ! (pc' - length \<tau>s)))\<rbrakk> \<Longrightarrow> P \<turnstile> tau' \<le>' [\<tau>'] ! (pc' - length \<tau>s)
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc pc' tau'. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc)); \<not> pc' < length \<tau>s; app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc); \<forall>x\<in>set (eff (is ! pc) P pc xt (\<tau>s ! pc)). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s then \<tau>s ! pc' else [\<tau>] ! (pc' - length \<tau>s))\<rbrakk> \<Longrightarrow> P \<turnstile> tau' \<le>' [\<tau>'] ! (pc' - length \<tau>s)
[PROOF STEP]
apply(drule (1) bspec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc pc' tau'. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc)); \<not> pc' < length \<tau>s; app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc); case (pc', tau') of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s then \<tau>s ! pc' else [\<tau>] ! (pc' - length \<tau>s))\<rbrakk> \<Longrightarrow> P \<turnstile> tau' \<le>' [\<tau>'] ! (pc' - length \<tau>s)
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc pc' tau'. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc)); \<not> pc' < length \<tau>s; app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc); P \<turnstile> tau' \<le>' [\<tau>] ! (pc' - length \<tau>s)\<rbrakk> \<Longrightarrow> P \<turnstile> tau' \<le>' [\<tau>'] ! (pc' - length \<tau>s)
[PROOF STEP]
apply(subgoal_tac "pc' = size \<tau>s")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc pc' tau'. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc)); \<not> pc' < length \<tau>s; app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc); P \<turnstile> tau' \<le>' [\<tau>] ! (pc' - length \<tau>s); pc' = length \<tau>s\<rbrakk> \<Longrightarrow> P \<turnstile> tau' \<le>' [\<tau>'] ! (pc' - length \<tau>s)
 2. \<And>pc pc' tau'. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc)); \<not> pc' < length \<tau>s; app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc); P \<turnstile> tau' \<le>' [\<tau>] ! (pc' - length \<tau>s)\<rbrakk> \<Longrightarrow> pc' = length \<tau>s
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc pc' tau'. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc)); \<not> pc' < length \<tau>s; app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc); P \<turnstile> tau' \<le>' [\<tau>] ! (pc' - length \<tau>s)\<rbrakk> \<Longrightarrow> pc' = length \<tau>s
 2. \<And>pc pc' tau'. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc)); \<not> pc' < length \<tau>s; app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc); P \<turnstile> tau' \<le>' [\<tau>] ! (pc' - length \<tau>s); pc' = length \<tau>s\<rbrakk> \<Longrightarrow> P \<turnstile> tau' \<le>' [\<tau>'] ! (pc' - length \<tau>s)
[PROOF STEP]
apply(clarsimp simp:app_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc pc' tau' a b. \<lbrakk>P \<turnstile> tau' \<le>' [\<tau>] ! (pc' - length \<tau>s); P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt \<lfloor>(a, b)\<rfloor>); \<not> pc' < length \<tau>s; \<tau>s ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app (is ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (eff (is ! pc) P pc xt \<lfloor>(a, b)\<rfloor>). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s)\<rbrakk> \<Longrightarrow> pc' = length \<tau>s
 2. \<And>pc pc' tau'. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc)); \<not> pc' < length \<tau>s; app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc); P \<turnstile> tau' \<le>' [\<tau>] ! (pc' - length \<tau>s); pc' = length \<tau>s\<rbrakk> \<Longrightarrow> P \<turnstile> tau' \<le>' [\<tau>'] ! (pc' - length \<tau>s)
[PROOF STEP]
apply(drule (1) bspec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc pc' tau' a b. \<lbrakk>P \<turnstile> tau' \<le>' [\<tau>] ! (pc' - length \<tau>s); P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt \<lfloor>(a, b)\<rfloor>); \<not> pc' < length \<tau>s; \<tau>s ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app (is ! pc) P pc mxs xt (a, b); case (pc', tau') of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s)\<rbrakk> \<Longrightarrow> pc' = length \<tau>s
 2. \<And>pc pc' tau'. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc)); \<not> pc' < length \<tau>s; app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc); P \<turnstile> tau' \<le>' [\<tau>] ! (pc' - length \<tau>s); pc' = length \<tau>s\<rbrakk> \<Longrightarrow> P \<turnstile> tau' \<le>' [\<tau>'] ! (pc' - length \<tau>s)
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc pc' tau'. \<lbrakk>P \<turnstile> \<tau> \<le>' \<tau>'; length is < Suc (length \<tau>s); pcs xt \<subseteq> {0..<length is}; pc < length is; (pc', tau') \<in> set (eff (is ! pc) P pc xt (\<tau>s ! pc)); \<not> pc' < length \<tau>s; app (is ! pc) P mxs T\<^sub>r pc (Suc (length \<tau>s)) xt (\<tau>s ! pc); P \<turnstile> tau' \<le>' [\<tau>] ! (pc' - length \<tau>s); pc' = length \<tau>s\<rbrakk> \<Longrightarrow> P \<turnstile> tau' \<le>' [\<tau>'] ! (pc' - length \<tau>s)
[PROOF STEP]
apply(auto elim!:sup_state_opt_trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [iff]: "xcpt_app i P pc mxs [] \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xcpt_app i P pc mxs [] \<tau>
[PROOF STEP]
by (simp add: xcpt_app_def relevant_entries_def)


[STATEMENT]
lemma [simp]: "xcpt_eff i P pc \<tau> [] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xcpt_eff i P pc \<tau> [] = []
[PROOF STEP]
by (simp add: xcpt_eff_def relevant_entries_def)


[STATEMENT]
lemma wt_New:
  "\<lbrakk> is_class P C; size ST < mxs \<rbrakk> \<Longrightarrow>
   \<turnstile> [New C],[] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (Class C#ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_class P C; length ST < mxs\<rbrakk> \<Longrightarrow> \<turnstile> [New C], [] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (Class C # ST) E A]
[PROOF STEP]
by(simp add:wt_defs ty\<^sub>i'_def)


[STATEMENT]
lemma wt_Cast:
  "is_type P T \<Longrightarrow>
   \<turnstile> [Checkcast T],[] [::] [ty\<^sub>i' (U # ST) E A, ty\<^sub>i' (T # ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_type P T \<Longrightarrow> \<turnstile> [Checkcast T], [] [::] [ty\<^sub>i' (U # ST) E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
by(simp add: ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma wt_Instanceof:
  "\<lbrakk> is_type P T; is_refT U \<rbrakk> \<Longrightarrow>
   \<turnstile> [Instanceof T],[] [::] [ty\<^sub>i' (U # ST) E A, ty\<^sub>i' (Boolean # ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_type P T; is_refT U\<rbrakk> \<Longrightarrow> \<turnstile> [Instanceof T], [] [::] [ty\<^sub>i' (U # ST) E A, ty\<^sub>i' (Boolean # ST) E A]
[PROOF STEP]
by(simp add: ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma wt_Push:
  "\<lbrakk> size ST < mxs; typeof v = Some T \<rbrakk>
  \<Longrightarrow> \<turnstile> [Push v],[] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (T#ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ST < mxs; typeof v = \<lfloor>T\<rfloor>\<rbrakk> \<Longrightarrow> \<turnstile> [Push v], [] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
by(simp add: ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma wt_Pop:
 "\<turnstile> [Pop],[] [::] (ty\<^sub>i' (T#ST) E A # ty\<^sub>i' ST E A # \<tau>s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> [Pop], [] [::] ty\<^sub>i' (T # ST) E A # ty\<^sub>i' ST E A # \<tau>s
[PROOF STEP]
by(simp add: ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma wt_BinOpInstr:
  "P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T \<Longrightarrow> \<turnstile> [BinOpInstr bop],[] [::] [ty\<^sub>i' (T2 # T1 # ST) E A, ty\<^sub>i' (T # ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T \<Longrightarrow> \<turnstile> [BinOpInstr bop], [] [::] [ty\<^sub>i' (T2 # T1 # ST) E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
by(auto simp:ty\<^sub>i'_def wt_defs dest: WT_binop_WTrt_binop intro: list_all2_refl)


[STATEMENT]
lemma wt_Load:
  "\<lbrakk> size ST < mxs; size E \<le> mxl; i \<in>\<in> A; i < size E \<rbrakk>
  \<Longrightarrow> \<turnstile> [Load i],[] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (E!i # ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ST < mxs; length E \<le> mxl; i \<in>\<in> A; i < length E\<rbrakk> \<Longrightarrow> \<turnstile> [Load i], [] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (E ! i # ST) E A]
[PROOF STEP]
by(auto simp add:ty\<^sub>i'_def wt_defs ty\<^sub>l_def hyperset_defs intro: widens_refl)


[STATEMENT]
lemma wt_Store:
 "\<lbrakk> P \<turnstile> T \<le> E!i; i < size E; size E \<le> mxl \<rbrakk> \<Longrightarrow>
  \<turnstile> [Store i],[] [::] [ty\<^sub>i' (T#ST) E A, ty\<^sub>i' ST E (\<lfloor>{i}\<rfloor> \<squnion> A)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> T \<le> E ! i; i < length E; length E \<le> mxl\<rbrakk> \<Longrightarrow> \<turnstile> [Store i], [] [::] [ty\<^sub>i' (T # ST) E A, ty\<^sub>i' ST E (\<lfloor>{i}\<rfloor> \<squnion> A)]
[PROOF STEP]
by(auto simp:hyperset_defs nth_list_update ty\<^sub>i'_def wt_defs ty\<^sub>l_def
        intro:list_all2_all_nthI)


[STATEMENT]
lemma wt_Get:
 "\<lbrakk> P \<turnstile> C sees F:T (fm) in D; class_type_of' U = \<lfloor>C\<rfloor> \<rbrakk> \<Longrightarrow>
  \<turnstile> [Getfield F D],[] [::] [ty\<^sub>i' (U # ST) E A, ty\<^sub>i' (T # ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> C sees F:T (fm) in D; class_type_of' U = \<lfloor>C\<rfloor>\<rbrakk> \<Longrightarrow> \<turnstile> [Getfield F D], [] [::] [ty\<^sub>i' (U # ST) E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
by(cases U)(auto simp: ty\<^sub>i'_def wt_defs dest: sees_field_idemp sees_field_decl_above intro: widens_refl widen_trans widen_array_object)


[STATEMENT]
lemma wt_Put:
  "\<lbrakk> P \<turnstile> C sees F:T (fm) in D; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> T' \<le> T \<rbrakk> \<Longrightarrow>
  \<turnstile> [Putfield F D],[] [::] [ty\<^sub>i' (T' # U # ST) E A, ty\<^sub>i' ST E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> C sees F:T (fm) in D; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> T' \<le> T\<rbrakk> \<Longrightarrow> \<turnstile> [Putfield F D], [] [::] [ty\<^sub>i' (T' # U # ST) E A, ty\<^sub>i' ST E A]
[PROOF STEP]
by(cases U)(auto 4 3 intro: sees_field_idemp widen_trans widen_array_object dest: sees_field_decl_above simp: ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma wt_CAS:
  "\<lbrakk> P \<turnstile> C sees F:T (fm) in D; class_type_of' U' = \<lfloor>C\<rfloor>; volatile fm; P \<turnstile> T2 \<le> T; P \<turnstile> T3 \<le> T \<rbrakk> \<Longrightarrow>
  \<turnstile> [CAS F D],[] [::] [ty\<^sub>i' (T3 # T2 # U' # ST) E A, ty\<^sub>i' (Boolean # ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> C sees F:T (fm) in D; class_type_of' U' = \<lfloor>C\<rfloor>; volatile fm; P \<turnstile> T2 \<le> T; P \<turnstile> T3 \<le> T\<rbrakk> \<Longrightarrow> \<turnstile> [CAS F D], [] [::] [ty\<^sub>i' (T3 # T2 # U' # ST) E A, ty\<^sub>i' (Boolean # ST) E A]
[PROOF STEP]
by(cases U')(auto 4 4 simp add: ty\<^sub>i'_def wt_defs intro: sees_field_idemp widen_trans widen_array_object dest: sees_field_decl_above)


[STATEMENT]
lemma wt_Throw:
  "P \<turnstile> C \<preceq>\<^sup>* Throwable \<Longrightarrow> \<turnstile> [ThrowExc],[] [::] [ty\<^sub>i' (Class C # ST) E A, \<tau>']"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> C \<preceq>\<^sup>* Throwable \<Longrightarrow> \<turnstile> [ThrowExc], [] [::] [ty\<^sub>i' (Class C # ST) E A, \<tau>']
[PROOF STEP]
by(simp add: ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma wt_IfFalse:
  "\<lbrakk> 2 \<le> i; nat i < size \<tau>s + 2; P \<turnstile> ty\<^sub>i' ST E A \<le>' \<tau>s ! nat(i - 2) \<rbrakk>
  \<Longrightarrow> \<turnstile> [IfFalse i],[] [::] ty\<^sub>i' (Boolean # ST) E A # ty\<^sub>i' ST E A # \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 \<le> i; nat i < length \<tau>s + 2; P \<turnstile> ty\<^sub>i' ST E A \<le>' \<tau>s ! nat (i - 2)\<rbrakk> \<Longrightarrow> \<turnstile> [IfFalse i], [] [::] ty\<^sub>i' (Boolean # ST) E A # ty\<^sub>i' ST E A # \<tau>s
[PROOF STEP]
by(auto simp add: ty\<^sub>i'_def wt_defs eval_nat_numeral nat_diff_distrib)


[STATEMENT]
lemma wt_Goto:
 "\<lbrakk> 0 \<le> int pc + i; nat (int pc + i) < size \<tau>s; size \<tau>s \<le> mpc;
    P \<turnstile> \<tau>s!pc \<le>' \<tau>s ! nat (int pc + i) \<rbrakk>
 \<Longrightarrow> P,T,mxs,mpc,[] \<turnstile> Goto i,pc :: \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> int pc + i; nat (int pc + i) < length \<tau>s; length \<tau>s \<le> mpc; P \<turnstile> \<tau>s ! pc \<le>' \<tau>s ! nat (int pc + i)\<rbrakk> \<Longrightarrow> P,T,mxs,mpc,[] \<turnstile> Goto i,pc :: \<tau>s
[PROOF STEP]
by(clarsimp simp add: wt_defs)


[STATEMENT]
lemma wt_Invoke:
  "\<lbrakk> size es = size Ts'; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts \<rbrakk>
  \<Longrightarrow> \<turnstile> [Invoke M (size es)],[] [::] [ty\<^sub>i' (rev Ts' @ U # ST) E A, ty\<^sub>i' (T#ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size es = length Ts'; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts\<rbrakk> \<Longrightarrow> \<turnstile> [Invoke M (size es)], [] [::] [ty\<^sub>i' (rev Ts' @ U # ST) E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
apply(clarsimp simp add: ty\<^sub>i'_def wt_defs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2 a. \<lbrakk>size es = length Ts'; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts; A = \<lfloor>x2\<rfloor>\<rbrakk> \<Longrightarrow> (a ! length Ts' = NT \<longrightarrow> rev Ts' @ U # ST = a \<longrightarrow> length Ts' < length a \<and> (\<forall>aa b. (\<exists>ab. ab ! length Ts' \<noteq> NT \<and> (ab ! length Ts' \<noteq> NT \<longrightarrow> ab = a \<and> aa = Suc 0 \<and> b = \<lfloor>(fst (snd (snd (method P (the (class_type_of' (ab ! length Ts'))) M))) # drop (Suc (length Ts')) ab, ty\<^sub>l E x2)\<rfloor>)) \<longrightarrow> P \<turnstile> b \<le>' [\<lfloor>(a, ty\<^sub>l E x2)\<rfloor>, \<lfloor>(T # ST, ty\<^sub>l E x2)\<rfloor>] ! aa)) \<and> (a ! length Ts' \<noteq> NT \<longrightarrow> rev Ts' @ U # ST = a \<longrightarrow> length Ts' < length a \<and> (\<exists>C. class_type_of' (a ! length Ts') = \<lfloor>C\<rfloor> \<and> (\<exists>D Ts. (\<exists>T m. P \<turnstile> C sees M: Ts\<rightarrow>T = m in D) \<and> P \<turnstile> rev (take (length Ts') a) [\<le>] Ts)) \<and> (\<forall>aa b. (\<exists>ab. ab ! length Ts' \<noteq> NT \<and> (ab ! length Ts' \<noteq> NT \<longrightarrow> ab = a \<and> aa = Suc 0 \<and> b = \<lfloor>(fst (snd (snd (method P (the (class_type_of' (ab ! length Ts'))) M))) # drop (Suc (length Ts')) ab, ty\<^sub>l E x2)\<rfloor>)) \<longrightarrow> P \<turnstile> b \<le>' [\<lfloor>(a, ty\<^sub>l E x2)\<rfloor>, \<lfloor>(T # ST, ty\<^sub>l E x2)\<rfloor>] ! aa))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2 a. \<lbrakk>size es = length Ts'; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts; A = \<lfloor>x2\<rfloor>; (rev Ts' @ U # ST) ! length Ts' = NT\<rbrakk> \<Longrightarrow> length Ts' < length (rev Ts' @ U # ST)
 2. \<And>x2 a. \<lbrakk>size es = length Ts'; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts; A = \<lfloor>x2\<rfloor>; (rev Ts' @ U # ST) ! length Ts' \<noteq> NT\<rbrakk> \<Longrightarrow> length Ts' < length (rev Ts' @ U # ST)
 3. \<And>x2 a. \<lbrakk>size es = length Ts'; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts; A = \<lfloor>x2\<rfloor>; (rev Ts' @ U # ST) ! length Ts' \<noteq> NT\<rbrakk> \<Longrightarrow> \<exists>C. class_type_of' ((rev Ts' @ U # ST) ! length Ts') = \<lfloor>C\<rfloor> \<and> (\<exists>D Ts. (\<exists>T m. P \<turnstile> C sees M: Ts\<rightarrow>T = m in D) \<and> P \<turnstile> rev (take (length Ts') (rev Ts' @ U # ST)) [\<le>] Ts)
 4. \<And>x2 a aa b ab. \<lbrakk>size es = length Ts'; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts; A = \<lfloor>x2\<rfloor>; (rev Ts' @ U # ST) ! length Ts' \<noteq> NT; (rev Ts' @ U # ST) ! length Ts' \<noteq> NT\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(fst (snd (snd (method P (the (class_type_of' ((rev Ts' @ U # ST) ! length Ts'))) M))) # drop (Suc (length Ts')) (rev Ts' @ U # ST), ty\<^sub>l E x2)\<rfloor> \<le>' [\<lfloor>(rev Ts' @ U # ST, ty\<^sub>l E x2)\<rfloor>, \<lfloor>(T # ST, ty\<^sub>l E x2)\<rfloor>] ! Suc 0
[PROOF STEP]
apply(simp_all (no_asm_use))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>size es = length Ts'; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts; A = \<lfloor>x2\<rfloor>; U \<noteq> NT\<rbrakk> \<Longrightarrow> \<exists>C. class_type_of' U = \<lfloor>C\<rfloor> \<and> (\<exists>D Ts. (\<exists>T m. P \<turnstile> C sees M: Ts\<rightarrow>T = m in D) \<and> P \<turnstile> Ts' [\<le>] Ts)
 2. \<And>x2. \<lbrakk>size es = length Ts'; class_type_of' U = \<lfloor>C\<rfloor>; P \<turnstile> C sees M: Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts; A = \<lfloor>x2\<rfloor>; U \<noteq> NT; U \<noteq> NT\<rbrakk> \<Longrightarrow> P \<turnstile> fst (snd (snd (method P (the (class_type_of' U)) M))) \<le> T \<and> P \<turnstile> ST [\<le>] ST
[PROOF STEP]
apply(auto simp add: intro: widens_refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done