[STATEMENT]
lemma exec_meth_drop_xt_pc:
  assumes exec: "exec_meth ci P (ins @ ins') (xt @ shift (length ins) xt') t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  and pc: "pc \<ge> length ins"
  and pcs: "pcs xt \<subseteq> {..<length ins}"
  and jump: "jump_ok ins' 0 n'"
  shows "pc' \<ge> length ins"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ins \<le> pc'
[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, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. length ins \<le> pc'
[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') ! pc) P t h stk loc undefined undefined pc []; pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 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 @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> length ins \<le> pc'
[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') ! pc) P t h stk loc undefined undefined pc []
pc < length (ins @ ins')
ci_app ci ((ins @ 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') ! pc) P t h stk loc undefined undefined pc []; pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 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 @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> length ins \<le> pc'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xcp = None
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! pc) P t h stk loc undefined undefined pc []
pc < length (ins @ ins')
ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []

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

goal (1 subgoal):
 1. length ins \<le> pc'
[PROOF STEP]
apply(cases "ins' ! (pc - length ins)")
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>x1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! pc) P t h stk loc undefined undefined pc []; pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = Load x1\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 2. \<And>x2. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! pc) P t h stk loc undefined undefined pc []; pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = Store x2\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 3. \<And>x3. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! pc) P t h stk loc undefined undefined pc []; pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = Push x3\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 4. \<And>x4. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! pc) P t h stk loc undefined undefined pc []; pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = New x4\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 5. \<And>x5. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! pc) P t h stk loc undefined undefined pc []; pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = NewArray x5\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 6. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! pc) P t h stk loc undefined undefined pc []; pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = ALoad\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 7. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! pc) P t h stk loc undefined undefined pc []; pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = AStore\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 8. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! pc) P t h stk loc undefined undefined pc []; pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = ALength\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 9. \<And>x91 x92. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! pc) P t h stk loc undefined undefined pc []; pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = Getfield x91 x92\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 10. \<And>x101 x102. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! pc) P t h stk loc undefined undefined pc []; pc < length (ins @ ins'); ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = Putfield x101 x102\<rbrakk> \<Longrightarrow> length ins \<le> pc'
A total of 24 subgoals...
[PROOF STEP]
apply(simp_all add: split_beta nth_append split: if_split_asm sum.split_asm)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>x4. \<lbrakk>pc < length ins + length ins'; ci_app ci (New x4) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = New x4; xcp = None; 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 pc)])) ` allocate h (Class_type x4)\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 2. \<And>x5. \<lbrakk>pc < length ins + length ins'; ci_app ci (NewArray x5) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = NewArray x5; xcp = None; \<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 pc)])) ` allocate h (Array_type x5 (nat (sint (the_Intg (hd stk)))))\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 3. \<lbrakk>pc < length ins + length ins'; ci_app ci ALoad P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = ALoad; xcp = None; 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 pc \<and> heap_read h (the_Addr (hd (tl stk))) (ACell (nat (sint (the_Intg (hd stk))))) v\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 4. \<And>x91 x92. \<lbrakk>pc < length ins + length ins'; ci_app ci (Getfield x91 x92) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = Getfield x91 x92; xcp = None; 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 pc \<and> heap_read h (the_Addr (hd stk)) (CField x92 x91) v'\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 5. \<And>x111 x112. \<lbrakk>pc < length ins + length ins'; ci_app ci (CAS x111 x112) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = CAS x111 x112; xcp = None; 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 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 pc \<and> heap_read h (the_Addr (hd (tl (tl stk)))) (CField x112 x111) v'' \<and> v'' \<noteq> hd (tl stk))\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 6. \<And>x141 x142. \<lbrakk>pc < length ins + length ins'; ci_app ci (Invoke x141 x142) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = Invoke x141 x142; xcp = None; 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, pc + 1)] | RetExc a \<Rightarrow> xcp' = \<lfloor>a\<rfloor> \<and> [(stk', loc', undefined, undefined, pc')] = [(stk, loc, undefined, undefined, pc)] | RetStaySame \<Rightarrow> xcp' = None \<and> [(stk', loc', undefined, undefined, pc')] = [(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)\<rbrakk> \<Longrightarrow> length ins \<le> pc'
 7. \<And>x20. \<lbrakk>xcp = None; ta = \<lbrace>\<rbrace> \<and> xcp' = None \<and> h' = h \<and> stk' = stk \<and> loc' = loc \<and> pc' = nat (int pc + x20); pc < length ins + length ins'; ci_app ci (Goto x20) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = Goto x20\<rbrakk> \<Longrightarrow> length ins \<le> nat (int pc + x20)
 8. \<And>x21. \<lbrakk>pc < length ins + length ins'; ci_app ci (IfFalse x21) P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = IfFalse x21; xcp = None; hd stk = Bool False; ta = \<lbrace>\<rbrace> \<and> xcp' = None \<and> h' = h \<and> stk' = tl stk \<and> loc' = loc \<and> pc' = nat (int pc + x21)\<rbrakk> \<Longrightarrow> length ins \<le> nat (int pc + x21)
 9. \<lbrakk>pc < length ins + length ins'; ci_app ci MExit P h stk loc undefined undefined pc []; jump_ok ins' 0 n'; length ins \<le> pc; ins' ! (pc - length ins) = MExit; xcp = None; 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 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' = pc\<rbrakk> \<Longrightarrow> length ins \<le> pc'
[PROOF STEP]
apply(force split: extCallRet.splits simp add: min_def extRet2JVM_def dest: jump_ok_GotoD jump_ok_IfFalseD)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
length ins \<le> pc'

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) pc (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> length ins \<le> pc'
[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) pc (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> length ins \<le> pc'
[PROOF STEP]
case exec_catch
[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 @ 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) pc (xt @ shift (length ins) xt') = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> length ins \<le> pc'
[PROOF STEP]
thus ?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 @ shift (length ins) xt') = \<lfloor>(pc', d_)\<rfloor>
d_ \<le> length stk

goal (1 subgoal):
 1. length ins \<le> pc'
[PROOF STEP]
using pcs pc
[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 @ shift (length ins) xt') = \<lfloor>(pc', d_)\<rfloor>
d_ \<le> length stk
pcs xt \<subseteq> {..<length ins}
length ins \<le> pc

goal (1 subgoal):
 1. length ins \<le> pc'
[PROOF STEP]
by(auto dest: match_ex_table_pcsD match_ex_table_shift_pcD simp add: match_ex_table_append)
[PROOF STATE]
proof (state)
this:
length ins \<le> pc'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_newArrayI:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (newA T\<lfloor>e\<rceil>) h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (newA T\<lfloor>e\<rceil>) h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (newA T\<lfloor>e\<rceil>)) (compxE2 (newA T\<lfloor>e\<rceil>) 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_newArray:
  "pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (newA T\<lfloor>e\<rceil>) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (newA T\<lfloor>e\<rceil>) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (newA T\<lfloor>e\<rceil>)) (compxE2 (newA T\<lfloor>e\<rceil>) 0 0) t h (stk, loc, pc, xcp) = exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp)
[PROOF STEP]
by(auto intro!: ext intro: exec_meth_take)


[STATEMENT]
lemma exec_move_CastI:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (Cast T e) h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (Cast T e) h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (Cast T e)) (compxE2 (Cast T e) 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_Cast:
  "pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (Cast T e) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (Cast T e) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (Cast T e)) (compxE2 (Cast T e) 0 0) t h (stk, loc, pc, xcp) = exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp)
[PROOF STEP]
by(auto intro!: ext intro: exec_meth_take)


[STATEMENT]
lemma exec_move_InstanceOfI:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e instanceof T) h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e instanceof T) h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e instanceof T)) (compxE2 (e instanceof T) 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_InstanceOf:
  "pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e instanceof T) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e instanceof T) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e instanceof T)) (compxE2 (e instanceof T) 0 0) t h (stk, loc, pc, xcp) = exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp)
[PROOF STEP]
by(auto intro!: ext intro: exec_meth_take)


[STATEMENT]
lemma exec_move_BinOpI1:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e \<guillemotleft>bop\<guillemotright> e') h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e \<guillemotleft>bop\<guillemotright> e') h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e \<guillemotleft>bop\<guillemotright> e')) (compxE2 (e \<guillemotleft>bop\<guillemotright> e') 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_BinOp1:
  "pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e \<guillemotleft>bop\<guillemotright> e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e \<guillemotleft>bop\<guillemotright> e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e \<guillemotleft>bop\<guillemotright> e')) (compxE2 (e \<guillemotleft>bop\<guillemotright> e') 0 0) t h (stk, loc, pc, xcp) = exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp)
[PROOF STEP]
by(auto intro!: ext intro: exec_meth_take_xt simp add: compxE2_size_convs)


[STATEMENT]
lemma exec_move_BinOpI2:
  assumes exec: "exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1 \<guillemotleft>bop\<guillemotright> e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (e1 \<guillemotleft>bop\<guillemotright> e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (e1 \<guillemotleft>bop\<guillemotright> e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1 \<guillemotleft>bop\<guillemotright> e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
from exec_meth_stk_offer[OF this, where stk''="[v]"]
[PROOF STATE]
proof (chain)
picking this:
exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v]) (compxE2 e2 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v]) (compxE2 e2 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1 \<guillemotleft>bop\<guillemotright> e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
by(fastforce split: bop.splits intro: append_exec_meth_xt simp add: exec_move_def compxE2_size_convs compxE2_stack_xlift_convs)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e1 \<guillemotleft>bop\<guillemotright> e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_LAssI:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (V := e) h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (V:=e) h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (V:=e)) (compxE2 (V:=e) 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_LAss:
  "pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (V := e) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (V:=e) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (V:=e)) (compxE2 (V:=e) 0 0) t h (stk, loc, pc, xcp) = exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp)
[PROOF STEP]
by(auto intro!: ext intro: exec_meth_take)


[STATEMENT]
lemma exec_move_AAccI1:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<lfloor>e'\<rceil>) h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<lfloor>e'\<rceil>) h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e\<lfloor>e'\<rceil>)) (compxE2 (e\<lfloor>e'\<rceil>) 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_AAcc1:
  "pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e\<lfloor>e'\<rceil>) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e\<lfloor>e'\<rceil>) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e\<lfloor>e'\<rceil>)) (compxE2 (e\<lfloor>e'\<rceil>) 0 0) t h (stk, loc, pc, xcp) = exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp)
[PROOF STEP]
by(auto intro!: ext intro: exec_meth_take_xt simp add: compxE2_size_convs)


[STATEMENT]
lemma exec_move_AAccI2:
  assumes exec: "exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1\<lfloor>e2\<rceil>) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil>) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil>) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil>) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
from exec_meth_stk_offer[OF this, where stk''="[v]"]
[PROOF STATE]
proof (chain)
picking this:
exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v]) (compxE2 e2 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v]) (compxE2 e2 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil>) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
by(fastforce intro: append_exec_meth_xt simp add: exec_move_def compxE2_size_convs compxE2_stack_xlift_convs)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e1\<lfloor>e2\<rceil>) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_AAssI1:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e\<lfloor>e'\<rceil> := e'')) (compxE2 (e\<lfloor>e'\<rceil> := e'') 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_AAss1:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
proof(rule ext iffI)+
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
fix ta h' s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
assume "?rhs ta h' s'"
[PROOF STATE]
proof (state)
this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'

goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
thus "?lhs ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(rule exec_move_AAssI1)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
fix ta h' s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
assume "?lhs ta h' s'"
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
hence "exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [AStore, Push Unit])
     (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t
     h (stk, loc, pc, xcp) ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [AStore, Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(simp add: exec_move_def shift_compxE2 ac_simps)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [AStore, Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
thus "?rhs ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [AStore, Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [AStore, Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
using pc
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [AStore, Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t h (stk, loc, pc, xcp) ta h' s'
pc < length (compE2 e)

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(rule exec_meth_take_xt)
[PROOF STATE]
proof (state)
this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_AAssI2:
  assumes exec: "exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
from exec_meth_stk_offer[OF this, where stk''="[v]", simplified stack_xlift_compxE2, simplified]
[PROOF STATE]
proof (chain)
picking this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 (Suc 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e2 @ compE2 e3 @ [AStore, Push Unit]) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 (Suc 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2 @ compE2 e3 @ [AStore, Push Unit]) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')
[PROOF STEP]
by(rule exec_meth_append_xt)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e2 @ compE2 e3 @ [AStore, Push Unit]) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2 @ compE2 e3 @ [AStore, Push Unit]) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0))))) t h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e2 @ compE2 e3 @ [AStore, Push Unit]) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2 @ compE2 e3 @ [AStore, Push Unit]) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0))))) t h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
by(rule append_exec_meth_xt) auto
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2 @ compE2 e3 @ [AStore, Push Unit]) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0))))) t h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2 @ compE2 e3 @ [AStore, Push Unit]) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0))))) t h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
by(auto simp add: exec_move_def shift_compxE2 ac_simps)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_AAssI3:
  assumes exec: "exec_move ci P t e3 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e3 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e3 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')
[PROOF STEP]
from exec_meth_stk_offer[OF this, where stk''="[v', v]", simplified stack_xlift_compxE2, simplified]
[PROOF STATE]
proof (chain)
picking this:
exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e3 @ [AStore, Push Unit]) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e3 @ [AStore, Push Unit]) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')
[PROOF STEP]
by(rule exec_meth_append)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e3 @ [AStore, Push Unit]) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ compE2 e3 @ [AStore, Push Unit])
                   ((compxE2 e1 0 0 @ compxE2 e2 (length (compE2 e1)) (Suc 0)) @ shift (length (compE2 e1 @ compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v', v], loc, length (compE2 e1 @ compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1 @ compE2 e2) + pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e3 @ [AStore, Push Unit]) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ compE2 e3 @ [AStore, Push Unit]) ((compxE2 e1 0 0 @ compxE2 e2 (length (compE2 e1)) (Suc 0)) @ shift (length (compE2 e1 @ compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v', v], loc, length (compE2 e1 @ compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1 @ compE2 e2) + pc', xcp')
[PROOF STEP]
by(rule append_exec_meth_xt) auto
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ compE2 e3 @ [AStore, Push Unit]) ((compxE2 e1 0 0 @ compxE2 e2 (length (compE2 e1)) (Suc 0)) @ shift (length (compE2 e1 @ compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v', v], loc, length (compE2 e1 @ compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1 @ compE2 e2) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ compE2 e3 @ [AStore, Push Unit]) ((compxE2 e1 0 0 @ compxE2 e2 (length (compE2 e1)) (Suc 0)) @ shift (length (compE2 e1 @ compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v', v], loc, length (compE2 e1 @ compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1 @ compE2 e2) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')
[PROOF STEP]
by(auto simp add: exec_move_def shift_compxE2 ac_simps)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e1\<lfloor>e2\<rceil> := e3) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_ALengthI:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<bullet>length) h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<bullet>length) h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e\<bullet>length)) (compxE2 (e\<bullet>length) 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_ALength:
  "pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e\<bullet>length) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e\<bullet>length) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e\<bullet>length)) (compxE2 (e\<bullet>length) 0 0) t h (stk, loc, pc, xcp) = exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp)
[PROOF STEP]
by(auto intro!: ext intro: exec_meth_take)


[STATEMENT]
lemma exec_move_FAccI:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<bullet>F{D}) h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<bullet>F{D}) h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e\<bullet>F{D})) (compxE2 (e\<bullet>F{D}) 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_FAcc:
  "pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e\<bullet>F{D}) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e\<bullet>F{D}) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e\<bullet>F{D})) (compxE2 (e\<bullet>F{D}) 0 0) t h (stk, loc, pc, xcp) = exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp)
[PROOF STEP]
by(auto intro!: ext intro: exec_meth_take)


[STATEMENT]
lemma exec_move_FAssI1:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<bullet>F{D} := e') h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<bullet>F{D} := e') h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e\<bullet>F{D} := e')) (compxE2 (e\<bullet>F{D} := e') 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_FAss1:
  "pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e\<bullet>F{D} := e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e\<bullet>F{D} := e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e\<bullet>F{D} := e')) (compxE2 (e\<bullet>F{D} := e') 0 0) t h (stk, loc, pc, xcp) = exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp)
[PROOF STEP]
by(auto intro!: ext intro: exec_meth_take_xt simp add: compxE2_size_convs)


[STATEMENT]
lemma exec_move_FAssI2:
  assumes exec: "exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1\<bullet>F{D} := e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>F{D} := e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>F{D} := e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>F{D} := e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
from exec_meth_stk_offer[OF this, where stk''="[v]"]
[PROOF STATE]
proof (chain)
picking this:
exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v]) (compxE2 e2 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v]) (compxE2 e2 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>F{D} := e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
by(fastforce intro: append_exec_meth_xt simp add: exec_move_def compxE2_size_convs compxE2_stack_xlift_convs)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e1\<bullet>F{D} := e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_CASI1:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e\<bullet>compareAndSwap(D\<bullet>F, e', e''))) (compxE2 (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_CAS1:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
proof(rule ext iffI)+
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
fix ta h' s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
assume "?rhs ta h' s'"
[PROOF STATE]
proof (state)
this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'

goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
thus "?lhs ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(rule exec_move_CASI1)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
fix ta h' s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
assume "?lhs ta h' s'"
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
hence "exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [CAS F D])
     (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t
     h (stk, loc, pc, xcp) ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [CAS F D]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(simp add: exec_move_def shift_compxE2 ac_simps)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [CAS F D]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
thus "?rhs ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [CAS F D]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [CAS F D]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
using pc
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [CAS F D]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t h (stk, loc, pc, xcp) ta h' s'
pc < length (compE2 e)

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(rule exec_meth_take_xt)
[PROOF STATE]
proof (state)
this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_CASI2:
  assumes exec: "exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
from exec_meth_stk_offer[OF this, where stk''="[v]", simplified stack_xlift_compxE2, simplified]
[PROOF STATE]
proof (chain)
picking this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 (Suc 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e2 @ compE2 e3 @ [CAS F D]) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 (Suc 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2 @ compE2 e3 @ [CAS F D]) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')
[PROOF STEP]
by(rule exec_meth_append_xt)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e2 @ compE2 e3 @ [CAS F D]) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2 @ compE2 e3 @ [CAS F D]) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0))))) t h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e2 @ compE2 e3 @ [CAS F D]) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2 @ compE2 e3 @ [CAS F D]) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0))))) t h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
by(rule append_exec_meth_xt) auto
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2 @ compE2 e3 @ [CAS F D]) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0))))) t h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2 @ compE2 e3 @ [CAS F D]) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0))))) t h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')
[PROOF STEP]
by(auto simp add: exec_move_def shift_compxE2 ac_simps)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_CASI3:
  assumes exec: "exec_move ci P t e3 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e3 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e3 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')
[PROOF STEP]
from exec_meth_stk_offer[OF this, where stk''="[v', v]", simplified stack_xlift_compxE2, simplified]
[PROOF STATE]
proof (chain)
picking this:
exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e3 @ [CAS F D]) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e3 @ [CAS F D]) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')
[PROOF STEP]
by(rule exec_meth_append)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e3 @ [CAS F D]) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ compE2 e3 @ [CAS F D])
                   ((compxE2 e1 0 0 @ compxE2 e2 (length (compE2 e1)) (Suc 0)) @ shift (length (compE2 e1 @ compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v', v], loc, length (compE2 e1 @ compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1 @ compE2 e2) + pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e3 @ [CAS F D]) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ compE2 e3 @ [CAS F D]) ((compxE2 e1 0 0 @ compxE2 e2 (length (compE2 e1)) (Suc 0)) @ shift (length (compE2 e1 @ compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v', v], loc, length (compE2 e1 @ compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1 @ compE2 e2) + pc', xcp')
[PROOF STEP]
by(rule append_exec_meth_xt) auto
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ compE2 e3 @ [CAS F D]) ((compxE2 e1 0 0 @ compxE2 e2 (length (compE2 e1)) (Suc 0)) @ shift (length (compE2 e1 @ compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v', v], loc, length (compE2 e1 @ compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1 @ compE2 e2) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ compE2 e3 @ [CAS F D]) ((compxE2 e1 0 0 @ compxE2 e2 (length (compE2 e1)) (Suc 0)) @ shift (length (compE2 e1 @ compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v', v], loc, length (compE2 e1 @ compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1 @ compE2 e2) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')
[PROOF STEP]
by(auto simp add: exec_move_def shift_compxE2 ac_simps)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e1\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_CallI1:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<bullet>M(es)) h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e\<bullet>M(es)) h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e\<bullet>M(es))) (compxE2 (e\<bullet>M(es)) 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_Call1:
  "pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e\<bullet>M(es)) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (e\<bullet>M(es)) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e\<bullet>M(es))) (compxE2 (e\<bullet>M(es)) 0 0) t h (stk, loc, pc, xcp) = exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp)
[PROOF STEP]
by(auto intro!: ext intro: exec_meth_take_xt simp add: compxEs2_size_convs)


[STATEMENT]
lemma exec_move_CallI2:
  assumes exec: "exec_moves ci P t es h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e\<bullet>M(es)) h (stk @ [v], loc, length (compE2 e) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e) + pc', xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (e\<bullet>M(es)) h (stk @ [v], loc, length (compE2 e) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (e\<bullet>M(es)) h (stk @ [v], loc, length (compE2 e) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_moves ci P t es h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_moves ci P t es h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
unfolding exec_moves_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e\<bullet>M(es)) h (stk @ [v], loc, length (compE2 e) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
from exec_meth_stk_offer[OF this, where stk''="[v]"]
[PROOF STATE]
proof (chain)
picking this:
exec_meth ci (compP2 P) (compEs2 es) (stack_xlift (length [v]) (compxEs2 es 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compEs2 es) (stack_xlift (length [v]) (compxEs2 es 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e\<bullet>M(es)) h (stk @ [v], loc, length (compE2 e) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
by(fastforce intro: append_exec_meth_xt simp add: exec_move_def compxEs2_size_convs compxEs2_stack_xlift_convs)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e\<bullet>M(es)) h (stk @ [v], loc, length (compE2 e) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e) + pc', xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_BlockNoneI:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t {V:T=None; e} h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t {V:T=None; e} h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 {V:T=None; e}) (compxE2 {V:T=None; e} 0 0) t h s ta h' s'
[PROOF STEP]
by simp


[STATEMENT]
lemma exec_move_BlockNone:
  "exec_move ci P t {V:T=None; e} = exec_move ci P t e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t {V:T=None; e} = exec_move ci P t e
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 {V:T=None; e}) (compxE2 {V:T=None; e} 0 0) t = exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t
[PROOF STEP]
by(simp)


[STATEMENT]
lemma exec_move_BlockSomeI:
  assumes exec: "exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')
[PROOF STEP]
let ?ins = "[Push v, Store V]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by(simp add: exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) (?ins @ compE2 e) (shift (length ?ins) (compxE2 e 0 0)) t h (stk, loc, length ?ins + pc, xcp) ta h' (stk', loc', length ?ins + pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) ([Push v, Store V] @ compE2 e) (shift (length [Push v, Store V]) (compxE2 e 0 0)) t h (stk, loc, length [Push v, Store V] + pc, xcp) ta h' (stk', loc', length [Push v, Store V] + pc', xcp')
[PROOF STEP]
by(rule append_exec_meth) auto
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) ([Push v, Store V] @ compE2 e) (shift (length [Push v, Store V]) (compxE2 e 0 0)) t h (stk, loc, length [Push v, Store V] + pc, xcp) ta h' (stk', loc', length [Push v, Store V] + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) ([Push v, Store V] @ compE2 e) (shift (length [Push v, Store V]) (compxE2 e 0 0)) t h (stk, loc, length [Push v, Store V] + pc, xcp) ta h' (stk', loc', length [Push v, Store V] + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')
[PROOF STEP]
by(simp add: exec_move_def shift_compxE2)
[PROOF STATE]
proof (state)
this:
exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_BlockSome:
  "exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp') =
   exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp') = exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp') \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (2 subgoals):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp') \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')
[PROOF STEP]
thus ?lhs
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')
[PROOF STEP]
by(rule exec_move_BlockSomeI)
[PROOF STATE]
proof (state)
this:
exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')

goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp') \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp') \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
let ?ins = "[Push v, Store V]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp') \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')

goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp') \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) (?ins @ compE2 e) (shift (length ?ins) (compxE2 e 0 0)) t h (stk, loc, length ?ins + pc, xcp) ta h' (stk', loc', length ?ins + pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) ([Push v, Store V] @ compE2 e) (shift (length [Push v, Store V]) (compxE2 e 0 0)) t h (stk, loc, length [Push v, Store V] + pc, xcp) ta h' (stk', loc', length [Push v, Store V] + pc', xcp')
[PROOF STEP]
by(simp add: exec_move_def shift_compxE2)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) ([Push v, Store V] @ compE2 e) (shift (length [Push v, Store V]) (compxE2 e 0 0)) t h (stk, loc, length [Push v, Store V] + pc, xcp) ta h' (stk', loc', length [Push v, Store V] + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp') \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', length ?ins + pc' - length ?ins, xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) ([Push v, Store V] @ compE2 e) (shift (length [Push v, Store V]) (compxE2 e 0 0)) t h (stk, loc, length [Push v, Store V] + pc, xcp) ta h' (stk', loc', length [Push v, Store V] + pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', length [Push v, Store V] + pc' - length [Push v, Store V], xcp')
[PROOF STEP]
by(rule exec_meth_drop) auto
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', length [Push v, Store V] + pc' - length [Push v, Store V], xcp')

goal (1 subgoal):
 1. exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp') \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', length [Push v, Store V] + pc' - length [Push v, Store V], xcp')

goal (1 subgoal):
 1. exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by(simp add: exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_SyncI1:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (sync\<^bsub>V\<^esub> (e) e')) (compxE2 (sync\<^bsub>V\<^esub> (e) e') 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_Sync1:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
proof(rule ext iffI)+
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
fix ta h' s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
assume "?lhs ta h' s'"
[PROOF STATE]
proof (state)
this:
exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, pc, xcp) ta h' s'

goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
hence "exec_meth ci (compP2 P) (compE2 e @ Dup # Store V # MEnter # compE2 e' @ [Load V, MExit, Goto 4, Load V, MExit, ThrowExc])
                   (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 3 0 @ [(3, 3 + length (compE2 e'), None, 6 + length (compE2 e'), 0)]))
                   t h (stk, loc, pc, xcp) ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e @ Dup # Store V # MEnter # compE2 e' @ [Load V, MExit, Goto 4, Load V, MExit, ThrowExc]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 3 0 @ [(3, 3 + length (compE2 e'), Any, 6 + length (compE2 e'), 0)])) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(simp add: shift_compxE2 ac_simps exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e @ Dup # Store V # MEnter # compE2 e' @ [Load V, MExit, Goto 4, Load V, MExit, ThrowExc]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 3 0 @ [(3, 3 + length (compE2 e'), Any, 6 + length (compE2 e'), 0)])) t h (stk, loc, pc, xcp) ta h' s'

goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
thus "?rhs ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ Dup # Store V # MEnter # compE2 e' @ [Load V, MExit, Goto 4, Load V, MExit, ThrowExc]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 3 0 @ [(3, 3 + length (compE2 e'), Any, 6 + length (compE2 e'), 0)])) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ Dup # Store V # MEnter # compE2 e' @ [Load V, MExit, Goto 4, Load V, MExit, ThrowExc]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 3 0 @ [(3, 3 + length (compE2 e'), Any, 6 + length (compE2 e'), 0)])) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
using pc
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ Dup # Store V # MEnter # compE2 e' @ [Load V, MExit, Goto 4, Load V, MExit, ThrowExc]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 3 0 @ [(3, 3 + length (compE2 e'), Any, 6 + length (compE2 e'), 0)])) t h (stk, loc, pc, xcp) ta h' s'
pc < length (compE2 e)

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(rule exec_meth_take_xt)
[PROOF STATE]
proof (state)
this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
qed(rule exec_move_SyncI1)


[STATEMENT]
lemma exec_move_SyncI2:
  assumes exec: "exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (sync\<^bsub>V\<^esub> (o') e) h (stk, loc, (Suc (Suc (Suc (length (compE2 o') + pc)))), xcp) ta h' (stk', loc', (Suc (Suc (Suc (length (compE2 o') + pc')))), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (sync\<^bsub>V\<^esub> (o') e) h (stk, loc, Suc (Suc (Suc (length (compE2 o') + pc))), xcp) ta h' (stk', loc', Suc (Suc (Suc (length (compE2 o') + pc'))), xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (sync\<^bsub>V\<^esub> (o') e) h (stk, loc, Suc (Suc (Suc (length (compE2 o') + pc))), xcp) ta h' (stk', loc', Suc (Suc (Suc (length (compE2 o') + pc'))), xcp')
[PROOF STEP]
let ?e = "compE2 o' @ [Dup, Store V, MEnter]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (sync\<^bsub>V\<^esub> (o') e) h (stk, loc, Suc (Suc (Suc (length (compE2 o') + pc))), xcp) ta h' (stk', loc', Suc (Suc (Suc (length (compE2 o') + pc'))), xcp')
[PROOF STEP]
let ?e' = "[Load V, MExit, Goto 4, Load V, MExit, ThrowExc]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (sync\<^bsub>V\<^esub> (o') e) h (stk, loc, Suc (Suc (Suc (length (compE2 o') + pc))), xcp) ta h' (stk', loc', Suc (Suc (Suc (length (compE2 o') + pc'))), xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by(simp add: exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (sync\<^bsub>V\<^esub> (o') e) h (stk, loc, Suc (Suc (Suc (length (compE2 o') + pc))), xcp) ta h' (stk', loc', Suc (Suc (Suc (length (compE2 o') + pc'))), xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) ((?e @ compE2 e) @ ?e') ((compxE2 o' 0 0 @ shift (length ?e) (compxE2 e 0 0)) @ [(length ?e, length ?e + length (compE2 e), None, length ?e + length (compE2 e) + 3, 0)]) t h (stk, loc, (length ?e + pc), xcp) ta h' (stk', loc', (length ?e + pc'), xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (((compE2 o' @ [Dup, Store V, MEnter]) @ compE2 e) @ [Load V, MExit, Goto 4, Load V, MExit, ThrowExc]) ((compxE2 o' 0 0 @ shift (length (compE2 o' @ [Dup, Store V, MEnter])) (compxE2 e 0 0)) @ [(length (compE2 o' @ [Dup, Store V, MEnter]), length (compE2 o' @ [Dup, Store V, MEnter]) + length (compE2 e), Any, length (compE2 o' @ [Dup, Store V, MEnter]) + length (compE2 e) + 3, 0)]) t h (stk, loc, length (compE2 o' @ [Dup, Store V, MEnter]) + pc, xcp) ta h' (stk', loc', length (compE2 o' @ [Dup, Store V, MEnter]) + pc', xcp')
[PROOF STEP]
by(rule exec_meth_append_xt[OF append_exec_meth_xt]) auto
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (((compE2 o' @ [Dup, Store V, MEnter]) @ compE2 e) @ [Load V, MExit, Goto 4, Load V, MExit, ThrowExc]) ((compxE2 o' 0 0 @ shift (length (compE2 o' @ [Dup, Store V, MEnter])) (compxE2 e 0 0)) @ [(length (compE2 o' @ [Dup, Store V, MEnter]), length (compE2 o' @ [Dup, Store V, MEnter]) + length (compE2 e), Any, length (compE2 o' @ [Dup, Store V, MEnter]) + length (compE2 e) + 3, 0)]) t h (stk, loc, length (compE2 o' @ [Dup, Store V, MEnter]) + pc, xcp) ta h' (stk', loc', length (compE2 o' @ [Dup, Store V, MEnter]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (sync\<^bsub>V\<^esub> (o') e) h (stk, loc, Suc (Suc (Suc (length (compE2 o') + pc))), xcp) ta h' (stk', loc', Suc (Suc (Suc (length (compE2 o') + pc'))), xcp')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (((compE2 o' @ [Dup, Store V, MEnter]) @ compE2 e) @ [Load V, MExit, Goto 4, Load V, MExit, ThrowExc]) ((compxE2 o' 0 0 @ shift (length (compE2 o' @ [Dup, Store V, MEnter])) (compxE2 e 0 0)) @ [(length (compE2 o' @ [Dup, Store V, MEnter]), length (compE2 o' @ [Dup, Store V, MEnter]) + length (compE2 e), Any, length (compE2 o' @ [Dup, Store V, MEnter]) + length (compE2 e) + 3, 0)]) t h (stk, loc, length (compE2 o' @ [Dup, Store V, MEnter]) + pc, xcp) ta h' (stk', loc', length (compE2 o' @ [Dup, Store V, MEnter]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (sync\<^bsub>V\<^esub> (o') e) h (stk, loc, Suc (Suc (Suc (length (compE2 o') + pc))), xcp) ta h' (stk', loc', Suc (Suc (Suc (length (compE2 o') + pc'))), xcp')
[PROOF STEP]
by(simp add: eval_nat_numeral shift_compxE2 exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (sync\<^bsub>V\<^esub> (o') e) h (stk, loc, Suc (Suc (Suc (length (compE2 o') + pc))), xcp) ta h' (stk', loc', Suc (Suc (Suc (length (compE2 o') + pc'))), xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_SeqI1:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e;;e') h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (e;; e') h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (e;; e')) (compxE2 (e;; e') 0 0) t h s ta h' s'
[PROOF STEP]
by auto