[STATEMENT]
lemma append_exec_meth_xt:
  assumes exec: "exec_meth ci P ins xt t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  and jump: "jump_ok ins 0 n"
  and pcs: "pcs xt' \<subseteq> {0..<length ins'}"
  shows "exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, (length ins' + pc), xcp) ta h' (stk', loc', (length ins' + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
using exec
[PROOF STATE]
proof (prove)
using this:
exec_meth ci P ins xt t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
case (exec_catch xcp d)
[PROOF STATE]
proof (state)
this:
xcp = \<lfloor>xcp\<rfloor>
ta = \<lbrace>\<rbrace>
h' = h
stk' = Addr xcp # drop (length stk - d) stk
loc' = loc
xcp' = None
match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>
d \<le> length stk

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
from \<open>match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>\<close>
[PROOF STATE]
proof (chain)
picking this:
match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>
[PROOF STEP]
have "match_ex_table P (cname_of h xcp) (length ins' + pc) (shift (length ins') xt) = \<lfloor>(length ins' + pc', d)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>

goal (1 subgoal):
 1. match_ex_table P (cname_of h xcp) (length ins' + pc) (shift (length ins') xt) = \<lfloor>(length ins' + pc', d)\<rfloor>
[PROOF STEP]
by(simp add: match_ex_table_shift)
[PROOF STATE]
proof (state)
this:
match_ex_table P (cname_of h xcp) (length ins' + pc) (shift (length ins') xt) = \<lfloor>(length ins' + pc', d)\<rfloor>

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
match_ex_table P (cname_of h xcp) (length ins' + pc) (shift (length ins') xt) = \<lfloor>(length ins' + pc', d)\<rfloor>

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
from pcs
[PROOF STATE]
proof (chain)
picking this:
pcs xt' \<subseteq> {0..<length ins'}
[PROOF STEP]
have "length ins' + pc \<notin> pcs xt'"
[PROOF STATE]
proof (prove)
using this:
pcs xt' \<subseteq> {0..<length ins'}

goal (1 subgoal):
 1. length ins' + pc \<notin> pcs xt'
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
length ins' + pc \<notin> pcs xt'

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
match_ex_table P (cname_of h xcp) (length ins' + pc) (shift (length ins') xt) = \<lfloor>(length ins' + pc', d)\<rfloor>
length ins' + pc \<notin> pcs xt'
[PROOF STEP]
have "match_ex_table P (cname_of h xcp) (length ins' + pc) (xt' @ shift (length ins') xt) = \<lfloor>(length ins' + pc', d)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
match_ex_table P (cname_of h xcp) (length ins' + pc) (shift (length ins') xt) = \<lfloor>(length ins' + pc', d)\<rfloor>
length ins' + pc \<notin> pcs xt'

goal (1 subgoal):
 1. match_ex_table P (cname_of h xcp) (length ins' + pc) (xt' @ shift (length ins') xt) = \<lfloor>(length ins' + pc', d)\<rfloor>
[PROOF STEP]
by(simp add: match_ex_table_append_not_pcs)
[PROOF STATE]
proof (state)
this:
match_ex_table P (cname_of h xcp) (length ins' + pc) (xt' @ shift (length ins') xt) = \<lfloor>(length ins' + pc', d)\<rfloor>

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
with exec_catch
[PROOF STATE]
proof (chain)
picking this:
xcp = \<lfloor>xcp\<rfloor>
ta = \<lbrace>\<rbrace>
h' = h
stk' = Addr xcp # drop (length stk - d) stk
loc' = loc
xcp' = None
match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>
d \<le> length stk
match_ex_table P (cname_of h xcp) (length ins' + pc) (xt' @ shift (length ins') xt) = \<lfloor>(length ins' + pc', d)\<rfloor>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xcp = \<lfloor>xcp\<rfloor>
ta = \<lbrace>\<rbrace>
h' = h
stk' = Addr xcp # drop (length stk - d) stk
loc' = loc
xcp' = None
match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>
d \<le> length stk
match_ex_table P (cname_of h xcp) (length ins' + pc) (xt' @ shift (length ins') xt) = \<lfloor>(length ins' + pc', d)\<rfloor>

goal (1 subgoal):
 1. exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
by(auto dest: exec_meth.exec_catch)
[PROOF STATE]
proof (state)
this:
exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
case exec_instr
[PROOF STATE]
proof (state)
this:
xcp = None
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []
pc < length ins
ci_app ci (ins ! pc) P h stk loc undefined undefined pc []

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
note exec = \<open>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []\<close>
[PROOF STATE]
proof (state)
this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
hence "(ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []"
[PROOF STATE]
proof (prove)
using this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []

goal (1 subgoal):
 1. (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
[PROOF STEP]
proof(cases "ins ! pc")
[PROOF STATE]
proof (state)
goal (24 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 2. \<And>x2. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 3. \<And>x3. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 4. \<And>x4. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 5. \<And>x5. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 6. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 7. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 8. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
A total of 24 subgoals...
[PROOF STEP]
case (Goto i)
[PROOF STATE]
proof (state)
this:
ins ! pc = Goto i

goal (24 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 2. \<And>x2. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 3. \<And>x3. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 4. \<And>x4. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 5. \<And>x5. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 6. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 7. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 8. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
A total of 24 subgoals...
[PROOF STEP]
with jump \<open>pc < length ins\<close>
[PROOF STATE]
proof (chain)
picking this:
jump_ok ins 0 n
pc < length ins
ins ! pc = Goto i
[PROOF STEP]
have "- int pc  \<le> i" "i < int (length ins - pc + n)"
[PROOF STATE]
proof (prove)
using this:
jump_ok ins 0 n
pc < length ins
ins ! pc = Goto i

goal (1 subgoal):
 1. - int pc \<le> i &&& i < int (length ins - pc + n)
[PROOF STEP]
by(auto dest: jump_ok_GotoD)
[PROOF STATE]
proof (state)
this:
- int pc \<le> i
i < int (length ins - pc + n)

goal (24 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 2. \<And>x2. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 3. \<And>x3. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 4. \<And>x4. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 5. \<And>x5. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 6. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 7. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 8. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
A total of 24 subgoals...
[PROOF STEP]
with exec Goto
[PROOF STATE]
proof (chain)
picking this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []
ins ! pc = Goto i
- int pc \<le> i
i < int (length ins - pc + n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []
ins ! pc = Goto i
- int pc \<le> i
i < int (length ins - pc + n)

goal (1 subgoal):
 1. (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
(ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []

goal (23 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 2. \<And>x2. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 3. \<And>x3. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 4. \<And>x4. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 5. \<And>x5. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 6. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 7. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 8. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
A total of 23 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (23 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 2. \<And>x2. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 3. \<And>x3. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 4. \<And>x4. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 5. \<And>x5. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 6. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 7. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 8. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
A total of 23 subgoals...
[PROOF STEP]
case (IfFalse i)
[PROOF STATE]
proof (state)
this:
ins ! pc = IfFalse i

goal (23 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 2. \<And>x2. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 3. \<And>x3. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 4. \<And>x4. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 5. \<And>x5. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 6. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 7. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 8. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
A total of 23 subgoals...
[PROOF STEP]
with jump \<open>pc < length ins\<close>
[PROOF STATE]
proof (chain)
picking this:
jump_ok ins 0 n
pc < length ins
ins ! pc = IfFalse i
[PROOF STEP]
have "- int pc  \<le> i" "i < int (length ins - pc + n)"
[PROOF STATE]
proof (prove)
using this:
jump_ok ins 0 n
pc < length ins
ins ! pc = IfFalse i

goal (1 subgoal):
 1. - int pc \<le> i &&& i < int (length ins - pc + n)
[PROOF STEP]
by(auto dest: jump_ok_IfFalseD)
[PROOF STATE]
proof (state)
this:
- int pc \<le> i
i < int (length ins - pc + n)

goal (23 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 2. \<And>x2. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 3. \<And>x3. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 4. \<And>x4. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 5. \<And>x5. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 6. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 7. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 8. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
A total of 23 subgoals...
[PROOF STEP]
with exec IfFalse
[PROOF STATE]
proof (chain)
picking this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []
ins ! pc = IfFalse i
- int pc \<le> i
i < int (length ins - pc + n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []
ins ! pc = IfFalse i
- int pc \<le> i
i < int (length ins - pc + n)

goal (1 subgoal):
 1. (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
(ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []

goal (22 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 2. \<And>x2. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 3. \<And>x3. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 4. \<And>x4. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 5. \<And>x5. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 6. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 7. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 8. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
A total of 22 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (22 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 2. \<And>x2. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 3. \<And>x3. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 4. \<And>x4. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 5. \<And>x5. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 6. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 7. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 8. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
A total of 22 subgoals...
[PROOF STEP]
case (Invoke M n)
[PROOF STATE]
proof (state)
this:
ins ! pc = Invoke M n

goal (22 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 2. \<And>x2. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 3. \<And>x3. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 4. \<And>x4. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 5. \<And>x5. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 6. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 7. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 8. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
A total of 22 subgoals...
[PROOF STEP]
with exec
[PROOF STATE]
proof (chain)
picking this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []
ins ! pc = Invoke M n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []
ins ! pc = Invoke M n

goal (1 subgoal):
 1. (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
[PROOF STEP]
by(auto split: if_split_asm extCallRet.splits split del: if_split simp add: split_beta nth_append min_def extRet2JVM_def)
[PROOF STATE]
proof (state)
this:
(ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []

goal (21 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 2. \<And>x2. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 3. \<And>x3. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 4. \<And>x4. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 5. \<And>x5. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 6. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 7. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 8. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
A total of 21 subgoals...
[PROOF STEP]
qed(auto simp add: split_beta split: if_split_asm sum.split_asm)
[PROOF STATE]
proof (state)
this:
(ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
from \<open>ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<close>
[PROOF STATE]
proof (chain)
picking this:
ci_app ci (ins ! pc) P h stk loc undefined undefined pc []
[PROOF STEP]
have "ci_app ci (ins ! pc) P h stk loc undefined undefined (length ins' + pc) []"
[PROOF STATE]
proof (prove)
using this:
ci_app ci (ins ! pc) P h stk loc undefined undefined pc []

goal (1 subgoal):
 1. ci_app ci (ins ! pc) P h stk loc undefined undefined (length ins' + pc) []
[PROOF STEP]
by(rule wf_ciD3'_ci_app) simp
[PROOF STATE]
proof (state)
this:
ci_app ci (ins ! pc) P h stk loc undefined undefined (length ins' + pc) []

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
ci_app ci (ins ! pc) P h stk loc undefined undefined (length ins' + pc) []
[PROOF STEP]
have "exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, (length ins' + pc), None) ta h' (stk', loc', (length ins' + pc'), xcp')"
[PROOF STATE]
proof (prove)
using this:
(ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
ci_app ci (ins ! pc) P h stk loc undefined undefined (length ins' + pc) []

goal (1 subgoal):
 1. exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, None) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
using \<open>pc < length ins\<close>
[PROOF STATE]
proof (prove)
using this:
(ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []
ci_app ci (ins ! pc) P h stk loc undefined undefined (length ins' + pc) []
pc < length ins

goal (1 subgoal):
 1. exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, None) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
by -(rule exec_meth.exec_instr, simp_all)
[PROOF STATE]
proof (state)
this:
exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, None) ta h' (stk', loc', length ins' + pc', xcp')

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, None) ta h' (stk', loc', length ins' + pc', xcp')

goal (1 subgoal):
 1. exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
using exec_instr
[PROOF STATE]
proof (prove)
using this:
exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, None) ta h' (stk', loc', length ins' + pc', xcp')
xcp = None
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []
pc < length ins
ci_app ci (ins ! pc) P h stk loc undefined undefined pc []

goal (1 subgoal):
 1. exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma append_exec_meth:
  assumes exec: "exec_meth ci P ins xt t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  and jump: "jump_ok ins 0 n"
  shows "exec_meth ci P (ins' @ ins) (shift (length ins') xt) t h (stk, loc, (length ins' + pc), xcp) ta h' (stk', loc', (length ins' + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci P (ins' @ ins) (shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
exec_meth ci P ins xt t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
jump_ok ins 0 n

goal (1 subgoal):
 1. exec_meth ci P (ins' @ ins) (shift (length ins') xt) t h (stk, loc, length ins' + pc, xcp) ta h' (stk', loc', length ins' + pc', xcp')
[PROOF STEP]
by(rule append_exec_meth_xt [where xt'="[]", simplified])


[STATEMENT]
lemma exec_meth_take_xt':
  "\<lbrakk> exec_meth ci P (ins @ ins') (xt' @ xt) t h (stk, loc, pc, xcp) ta h' s';
    pc < length ins; pc \<notin> pcs xt \<rbrakk>
  \<Longrightarrow> exec_meth ci P ins xt' t h (stk, loc, pc, xcp) ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_meth ci P (ins @ ins') (xt' @ xt) t h (stk, loc, pc, xcp) ta h' s'; pc < length ins; pc \<notin> pcs xt\<rbrakk> \<Longrightarrow> exec_meth ci P ins xt' t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
apply(erule exec_meth.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>taa xcpa h'a stk' loc' pc' pca ha stka loca. \<lbrakk>pc < length ins; pc \<notin> pcs xt; h = ha; (stk, loc, pc, xcp) = (stka, loca, pca, None); ta = taa; h' = h'a; s' = (stk', loc', pc', xcpa); (taa, xcpa, h'a, [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! pca) P t ha stka loca undefined undefined pca []; pca < length (ins @ ins'); ci_app ci ((ins @ ins') ! pca) P ha stka loca undefined undefined pca []\<rbrakk> \<Longrightarrow> exec_meth ci P ins xt' t h (stk, loc, pc, xcp) ta h' s'
 2. \<And>ha xcpa pca pc' d stka loca. \<lbrakk>pc < length ins; pc \<notin> pcs xt; h = ha; (stk, loc, pc, xcp) = (stka, loca, pca, \<lfloor>xcpa\<rfloor>); ta = \<lbrace>\<rbrace>; h' = ha; s' = (Addr xcpa # drop (length stka - d) stka, loca, pc', None); match_ex_table P (cname_of ha xcpa) pca (xt' @ xt) = \<lfloor>(pc', d)\<rfloor>; d \<le> length stka\<rbrakk> \<Longrightarrow> exec_meth ci P ins xt' t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
apply(auto intro: exec_meth.intros simp add: match_ex_table_append nth_append dest: match_ex_table_pcsD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma exec_meth_take_xt:
  "\<lbrakk> exec_meth ci P (ins @ ins') (xt' @ shift (length ins) xt) t h (stk, loc, pc, xcp) ta h' s';
    pc < length ins \<rbrakk>
  \<Longrightarrow> exec_meth ci P ins xt' t h (stk, loc, pc, xcp) ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_meth ci P (ins @ ins') (xt' @ shift (length ins) xt) t h (stk, loc, pc, xcp) ta h' s'; pc < length ins\<rbrakk> \<Longrightarrow> exec_meth ci P ins xt' t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(auto intro: exec_meth_take_xt')


[STATEMENT]
lemma exec_meth_take:
  "\<lbrakk> exec_meth ci P (ins @ ins') xt t h (stk, loc, pc, xcp) ta h' s';
    pc < length ins \<rbrakk>
  \<Longrightarrow> exec_meth ci P ins xt t h (stk, loc, pc, xcp) ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_meth ci P (ins @ ins') xt t h (stk, loc, pc, xcp) ta h' s'; pc < length ins\<rbrakk> \<Longrightarrow> exec_meth ci P ins xt t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(auto intro: exec_meth_take_xt[where xt = "[]"])


[STATEMENT]
lemma exec_meth_drop_xt:
  assumes exec: "exec_meth ci P (ins @ ins') (xt @ shift (length ins) xt') t h (stk, loc, (length ins + pc), xcp) ta h' (stk', loc', pc', xcp')"
  and xt: "pcs xt \<subseteq> {..<length ins}"
  and jump: "jump_ok ins' 0 n"
  shows "exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', (pc' - length ins), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
using exec
[PROOF STATE]
proof (prove)
using this:
exec_meth ci P (ins @ ins') (xt @ shift (length ins) xt') t h (stk, loc, length ins + pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
proof(cases rule: exec_meth.cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; length ins + pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! (length ins + pc)) P h stk loc undefined undefined (length ins + pc) []\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
case exec_instr
[PROOF STATE]
proof (state)
this:
xcp = None
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []
length ins + pc < length (ins @ ins')
ci_app ci ((ins @ ins') ! (length ins + pc)) P h stk loc undefined undefined (length ins + pc) []

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; length ins + pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! (length ins + pc)) P h stk loc undefined undefined (length ins + pc) []\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
let ?PC = "length ins + pc"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; length ins + pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! (length ins + pc)) P h stk loc undefined undefined (length ins + pc) []\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
note [simp] = \<open>xcp = None\<close>
[PROOF STATE]
proof (state)
this:
xcp = None

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; length ins + pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! (length ins + pc)) P h stk loc undefined undefined (length ins + pc) []\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
from \<open>?PC < length (ins @ ins')\<close>
[PROOF STATE]
proof (chain)
picking this:
length ins + pc < length (ins @ ins')
[PROOF STEP]
have pc: "pc < length ins'"
[PROOF STATE]
proof (prove)
using this:
length ins + pc < length (ins @ ins')

goal (1 subgoal):
 1. pc < length ins'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pc < length ins'

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; length ins + pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! (length ins + pc)) P h stk loc undefined undefined (length ins + pc) []\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pc < length ins'

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; length ins + pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! (length ins + pc)) P h stk loc undefined undefined (length ins + pc) []\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
with \<open>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! ?PC) P t h stk loc undefined undefined ?PC []\<close>
[PROOF STATE]
proof (chain)
picking this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []
pc < length ins'
[PROOF STEP]
have "(ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []"
[PROOF STATE]
proof (prove)
using this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []
pc < length ins'

goal (1 subgoal):
 1. (ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []
[PROOF STEP]
apply(cases "ins' ! pc")
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; pc < length ins'; ins' ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []
 2. \<And>x2. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; pc < length ins'; ins' ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []
 3. \<And>x3. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; pc < length ins'; ins' ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []
 4. \<And>x4. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; pc < length ins'; ins' ! pc = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []
 5. \<And>x5. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; pc < length ins'; ins' ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []
 6. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; pc < length ins'; ins' ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []
 7. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; pc < length ins'; ins' ! pc = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []
 8. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; pc < length ins'; ins' ! pc = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; pc < length ins'; ins' ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; pc < length ins'; ins' ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []
A total of 24 subgoals...
[PROOF STEP]
apply(simp_all add: split_beta split: if_split_asm sum.split_asm split del: if_split)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x4. \<lbrakk>pc < length ins'; ins' ! pc = New x4; allocate h (Class_type x4) \<noteq> {}; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> (\<lambda>x. (\<lbrace>NewHeapElem (snd x) (Class_type x4)\<rbrace>, None, fst x, [(Addr (snd x) # stk, loc, undefined, undefined, Suc (length ins + pc))])) ` allocate h (Class_type x4)\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> (\<lambda>x. (\<lbrace>NewHeapElem (snd x) (Class_type x4)\<rbrace>, None, fst x, [(Addr (snd x) # stk, loc, undefined, undefined, Suc pc)])) ` allocate h (Class_type x4)
 2. \<And>x5. \<lbrakk>pc < length ins'; ins' ! pc = NewArray x5; \<not> the_Intg (hd stk) <s 0; allocate h (Array_type x5 (nat (sint (the_Intg (hd stk))))) \<noteq> {}; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> (\<lambda>x. (\<lbrace>NewHeapElem (snd x) (Array_type x5 (nat (sint (the_Intg (hd stk)))))\<rbrace>, None, fst x, [(Addr (snd x) # tl stk, loc, undefined, undefined, Suc (length ins + pc))])) ` allocate h (Array_type x5 (nat (sint (the_Intg (hd stk)))))\<rbrakk> \<Longrightarrow> (ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> (\<lambda>x. (\<lbrace>NewHeapElem (snd x) (Array_type x5 (nat (sint (the_Intg (hd stk)))))\<rbrace>, None, fst x, [(Addr (snd x) # tl stk, loc, undefined, undefined, Suc pc)])) ` allocate h (Array_type x5 (nat (sint (the_Intg (hd stk)))))
 3. \<lbrakk>pc < length ins'; ins' ! pc = ALoad; hd (tl stk) \<noteq> Null; \<not> the_Intg (hd stk) <s 0 \<and> \<not> int (alen_of_htype (the (typeof_addr h (the_Addr (hd (tl stk)))))) \<le> sint (the_Intg (hd stk)); \<exists>v. ta = \<lbrace>ReadMem (the_Addr (hd (tl stk))) (ACell (nat (sint (the_Intg (hd stk))))) v\<rbrace> \<and> xcp' = None \<and> h' = h \<and> stk' = v # tl (tl stk) \<and> loc' = loc \<and> pc' = Suc (length ins + pc) \<and> heap_read h (the_Addr (hd (tl stk))) (ACell (nat (sint (the_Intg (hd stk))))) v\<rbrakk> \<Longrightarrow> \<exists>v. ta = \<lbrace>ReadMem (the_Addr (hd (tl stk))) (ACell (nat (sint (the_Intg (hd stk))))) v\<rbrace> \<and> xcp' = None \<and> h' = h \<and> stk' = v # tl (tl stk) \<and> loc' = loc \<and> pc' - length ins = Suc pc \<and> heap_read h (the_Addr (hd (tl stk))) (ACell (nat (sint (the_Intg (hd stk))))) v
 4. \<And>x91 x92. \<lbrakk>pc < length ins'; ins' ! pc = Getfield x91 x92; hd stk \<noteq> Null; \<exists>v'. ta = \<lbrace>ReadMem (the_Addr (hd stk)) (CField x92 x91) v'\<rbrace> \<and> xcp' = None \<and> h' = h \<and> stk' = v' # tl stk \<and> loc' = loc \<and> pc' = Suc (length ins + pc) \<and> heap_read h (the_Addr (hd stk)) (CField x92 x91) v'\<rbrakk> \<Longrightarrow> \<exists>v'. ta = \<lbrace>ReadMem (the_Addr (hd stk)) (CField x92 x91) v'\<rbrace> \<and> xcp' = None \<and> h' = h \<and> stk' = v' # tl stk \<and> loc' = loc \<and> pc' - length ins = Suc pc \<and> heap_read h (the_Addr (hd stk)) (CField x92 x91) v'
 5. \<And>x111 x112. \<lbrakk>pc < length ins'; ins' ! pc = CAS x111 x112; hd (tl (tl stk)) \<noteq> Null; ta = \<lbrace>ReadMem (the_Addr (hd (tl (tl stk)))) (CField x112 x111) (hd (tl stk)), WriteMem (the_Addr (hd (tl (tl stk)))) (CField x112 x111) (hd stk)\<rbrace> \<and> xcp' = None \<and> stk' = Bool True # tl (tl (tl stk)) \<and> loc' = loc \<and> pc' = Suc (length ins + pc) \<and> heap_read h (the_Addr (hd (tl (tl stk)))) (CField x112 x111) (hd (tl stk)) \<and> heap_write h (the_Addr (hd (tl (tl stk)))) (CField x112 x111) (hd stk) h' \<or> (\<exists>v''. ta = \<lbrace>ReadMem (the_Addr (hd (tl (tl stk)))) (CField x112 x111) v''\<rbrace> \<and> xcp' = None \<and> h' = h \<and> stk' = Bool False # tl (tl (tl stk)) \<and> loc' = loc \<and> pc' = Suc (length ins + pc) \<and> heap_read h (the_Addr (hd (tl (tl stk)))) (CField x112 x111) v'' \<and> v'' \<noteq> hd (tl stk))\<rbrakk> \<Longrightarrow> ta = \<lbrace>ReadMem (the_Addr (hd (tl (tl stk)))) (CField x112 x111) (hd (tl stk)), WriteMem (the_Addr (hd (tl (tl stk)))) (CField x112 x111) (hd stk)\<rbrace> \<and> xcp' = None \<and> stk' = Bool True # tl (tl (tl stk)) \<and> loc' = loc \<and> pc' - length ins = Suc pc \<and> heap_read h (the_Addr (hd (tl (tl stk)))) (CField x112 x111) (hd (tl stk)) \<and> heap_write h (the_Addr (hd (tl (tl stk)))) (CField x112 x111) (hd stk) h' \<or> (\<exists>v''. ta = \<lbrace>ReadMem (the_Addr (hd (tl (tl stk)))) (CField x112 x111) v''\<rbrace> \<and> xcp' = None \<and> h' = h \<and> stk' = Bool False # tl (tl (tl stk)) \<and> loc' = loc \<and> pc' - length ins = Suc pc \<and> heap_read h (the_Addr (hd (tl (tl stk)))) (CField x112 x111) v'' \<and> v'' \<noteq> hd (tl stk))
 6. \<And>x141 x142. \<lbrakk>pc < length ins'; ins' ! pc = Invoke x141 x142; stk ! x142 \<noteq> Null; snd (snd (snd (method P (class_type_of (the (typeof_addr h (the_Addr (stk ! x142))))) x141))) = None; \<exists>a aa ab ac ad b. ta = (a, map (convert_new_thread_action (extNTA2JVM P)) aa, ab, ac, ad, b) \<and> (\<exists>va. (case va of RetVal v \<Rightarrow> xcp' = None \<and> [(stk', loc', undefined, undefined, pc')] = [(v # drop (Suc x142) stk, loc, undefined, undefined, length ins + pc + 1)] | RetExc a \<Rightarrow> xcp' = \<lfloor>a\<rfloor> \<and> [(stk', loc', undefined, undefined, pc')] = [(stk, loc, undefined, undefined, length ins + pc)] | RetStaySame \<Rightarrow> xcp' = None \<and> [(stk', loc', undefined, undefined, pc')] = [(stk, loc, undefined, undefined, length ins + pc)]) \<and> ((a, aa, ab, ac, ad, b), va, h') \<in> red_external_aggr P t (the_Addr (stk ! x142)) x141 (rev (take x142 stk)) h)\<rbrakk> \<Longrightarrow> \<exists>a aa ab ac ad b. ta = (a, map (convert_new_thread_action (extNTA2JVM P)) aa, ab, ac, ad, b) \<and> (\<exists>va. (case va of RetVal v \<Rightarrow> xcp' = None \<and> [(stk', loc', undefined, undefined, pc' - length ins)] = [(v # drop (Suc x142) stk, loc, undefined, undefined, pc + 1)] | RetExc a \<Rightarrow> xcp' = \<lfloor>a\<rfloor> \<and> [(stk', loc', undefined, undefined, pc' - length ins)] = [(stk, loc, undefined, undefined, pc)] | RetStaySame \<Rightarrow> xcp' = None \<and> [(stk', loc', undefined, undefined, pc' - length ins)] = [(stk, loc, undefined, undefined, pc)]) \<and> ((a, aa, ab, ac, ad, b), va, h') \<in> red_external_aggr P t (the_Addr (stk ! x142)) x141 (rev (take x142 stk)) h)
 7. \<lbrakk>pc < length ins'; ins' ! pc = MExit; hd stk \<noteq> Null; ta = \<lbrace>(Unlock, the_Addr (hd stk)), SyncUnlock (the_Addr (hd stk))\<rbrace> \<and> xcp' = None \<and> h' = h \<and> stk' = tl stk \<and> loc' = loc \<and> pc' = Suc (length ins + pc) \<or> ta = \<lbrace>(UnlockFail, the_Addr (hd stk))\<rbrace> \<and> xcp' = \<lfloor>addr_of_sys_xcpt IllegalMonitorState\<rfloor> \<and> h' = h \<and> stk' = stk \<and> loc' = loc \<and> pc' = length ins + pc\<rbrakk> \<Longrightarrow> ta = \<lbrace>(Unlock, the_Addr (hd stk)), SyncUnlock (the_Addr (hd stk))\<rbrace> \<and> xcp' = None \<and> h' = h \<and> stk' = tl stk \<and> loc' = loc \<and> pc' - length ins = Suc pc \<or> ta = \<lbrace>(UnlockFail, the_Addr (hd stk))\<rbrace> \<and> xcp' = \<lfloor>addr_of_sys_xcpt IllegalMonitorState\<rfloor> \<and> h' = h \<and> stk' = stk \<and> loc' = loc \<and> pc' - length ins = pc
[PROOF STEP]
apply(force split: extCallRet.splits simp add: min_def extRet2JVM_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; length ins + pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! (length ins + pc)) P h stk loc undefined undefined (length ins + pc) []\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; length ins + pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! (length ins + pc)) P h stk loc undefined undefined (length ins + pc) []\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
from \<open>ci_app ci ((ins @ ins') ! ?PC) P h stk loc undefined undefined ?PC []\<close> jump pc
[PROOF STATE]
proof (chain)
picking this:
ci_app ci ((ins @ ins') ! (length ins + pc)) P h stk loc undefined undefined (length ins + pc) []
jump_ok ins' 0 n
pc < length ins'
[PROOF STEP]
have "ci_app ci (ins' ! pc) P h stk loc undefined undefined pc []"
[PROOF STATE]
proof (prove)
using this:
ci_app ci ((ins @ ins') ! (length ins + pc)) P h stk loc undefined undefined (length ins + pc) []
jump_ok ins' 0 n
pc < length ins'

goal (1 subgoal):
 1. ci_app ci (ins' ! pc) P h stk loc undefined undefined pc []
[PROOF STEP]
by(fastforce elim: wf_ciD3_ci_app dest: jump_ok_ins_jump_ok)
[PROOF STATE]
proof (state)
this:
ci_app ci (ins' ! pc) P h stk loc undefined undefined pc []

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! (length ins + pc)) P t h stk loc undefined undefined (length ins + pc) []; length ins + pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! (length ins + pc)) P h stk loc undefined undefined (length ins + pc) []\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pc < length ins'
(ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []
ci_app ci (ins' ! pc) P h stk loc undefined undefined pc []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pc < length ins'
(ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) \<in> exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []
ci_app ci (ins' ! pc) P h stk loc undefined undefined pc []

goal (1 subgoal):
 1. exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
by(auto intro: exec_meth.intros)
[PROOF STATE]
proof (state)
this:
exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')

goal (1 subgoal):
 1. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
case (exec_catch XCP D)
[PROOF STATE]
proof (state)
this:
xcp = \<lfloor>XCP\<rfloor>
ta = \<lbrace>\<rbrace>
h' = h
stk' = Addr XCP # drop (length stk - D) stk
loc' = loc
xcp' = None
match_ex_table P (cname_of h XCP) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', D)\<rfloor>
D \<le> length stk

goal (1 subgoal):
 1. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
let ?PC = "length ins + pc"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
note [simp] = \<open>xcp = \<lfloor>XCP\<rfloor>\<close>
    \<open>ta = \<epsilon>\<close> \<open>h' = h\<close> \<open>stk' = Addr XCP # drop (length stk - D) stk\<close> \<open>loc' = loc\<close> \<open>xcp' = None\<close>
[PROOF STATE]
proof (state)
this:
xcp = \<lfloor>XCP\<rfloor>
ta = \<lbrace>\<rbrace>
h' = h
stk' = Addr XCP # drop (length stk - D) stk
loc' = loc
xcp' = None

goal (1 subgoal):
 1. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
from \<open>match_ex_table P (cname_of h XCP) ?PC (xt @ shift (length ins) xt') = \<lfloor>(pc', D)\<rfloor>\<close> xt
[PROOF STATE]
proof (chain)
picking this:
match_ex_table P (cname_of h XCP) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', D)\<rfloor>
pcs xt \<subseteq> {..<length ins}
[PROOF STEP]
have "match_ex_table P (cname_of h XCP) pc xt' = \<lfloor>(pc' - length ins, D)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
match_ex_table P (cname_of h XCP) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', D)\<rfloor>
pcs xt \<subseteq> {..<length ins}

goal (1 subgoal):
 1. match_ex_table P (cname_of h XCP) pc xt' = \<lfloor>(pc' - length ins, D)\<rfloor>
[PROOF STEP]
by(auto simp add: match_ex_table_append dest: match_ex_table_shift_pcD match_ex_table_pcsD)
[PROOF STATE]
proof (state)
this:
match_ex_table P (cname_of h XCP) pc xt' = \<lfloor>(pc' - length ins, D)\<rfloor>

goal (1 subgoal):
 1. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) (length ins + pc) (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
with \<open>D \<le> length stk\<close>
[PROOF STATE]
proof (chain)
picking this:
D \<le> length stk
match_ex_table P (cname_of h XCP) pc xt' = \<lfloor>(pc' - length ins, D)\<rfloor>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
D \<le> length stk
match_ex_table P (cname_of h XCP) pc xt' = \<lfloor>(pc' - length ins, D)\<rfloor>

goal (1 subgoal):
 1. exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
by(auto intro: exec_meth.intros)
[PROOF STATE]
proof (state)
this:
exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_meth_drop:
  "\<lbrakk> exec_meth ci P (ins @ ins') (shift (length ins) xt) t h (stk, loc, (length ins + pc), xcp) ta h' (stk', loc', pc', xcp');
     jump_ok ins' 0 b \<rbrakk>
   \<Longrightarrow> exec_meth ci P ins' xt t h (stk, loc, pc, xcp) ta h' (stk', loc', (pc' - length ins), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_meth ci P (ins @ ins') (shift (length ins) xt) t h (stk, loc, length ins + pc, xcp) ta h' (stk', loc', pc', xcp'); jump_ok ins' 0 b\<rbrakk> \<Longrightarrow> exec_meth ci P ins' xt t h (stk, loc, pc, xcp) ta h' (stk', loc', pc' - length ins, xcp')
[PROOF STEP]
by(auto intro: exec_meth_drop_xt[where xt = "[]"])