[STATEMENT]
lemma \<tau>Exec_movesr_trans:
  "\<lbrakk> \<tau>Exec_movesr ci P t es h s s'; \<tau>Exec_movesr ci P t es h s' s'' \<rbrakk> \<Longrightarrow> \<tau>Exec_movesr ci P t es h s s''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>Exec_movesr ci P t es h s s'; \<tau>Exec_movesr ci P t es h s' s''\<rbrakk> \<Longrightarrow> \<tau>Exec_movesr ci P t es h s s''
[PROOF STEP]
by(rule rtranclp_trans)


[STATEMENT]
lemma \<tau>Exec_movet_trans:
  "\<lbrakk> \<tau>Exec_movet ci P t e h s s'; \<tau>Exec_movet ci P t e h s' s'' \<rbrakk> \<Longrightarrow> \<tau>Exec_movet ci P t e h s s''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>Exec_movet ci P t e h s s'; \<tau>Exec_movet ci P t e h s' s''\<rbrakk> \<Longrightarrow> \<tau>Exec_movet ci P t e h s s''
[PROOF STEP]
by(rule tranclp_trans)


[STATEMENT]
lemma \<tau>Exec_movest_trans:
  "\<lbrakk> \<tau>Exec_movest ci P t es h s s'; \<tau>Exec_movest ci P t es h s' s'' \<rbrakk> \<Longrightarrow> \<tau>Exec_movest ci P t es h s s''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>Exec_movest ci P t es h s s'; \<tau>Exec_movest ci P t es h s' s''\<rbrakk> \<Longrightarrow> \<tau>Exec_movest ci P t es h s s''
[PROOF STEP]
by(rule tranclp_trans)


[STATEMENT]
lemma \<tau>exec_move_into_\<tau>exec_moves:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_moves ci P t (e # es) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_moves ci P t (e # es) h s s'
[PROOF STEP]
by(cases s)(auto elim!: \<tau>exec_moveE intro!: \<tau>exec_movesI simp add: exec_move_def exec_moves_def intro: \<tau>moves2Hd)


[STATEMENT]
lemma \<tau>Exec_mover_\<tau>Exec_movesr:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_movesr ci P t (e # es) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_movesr ci P t (e # es) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl \<tau>exec_move_into_\<tau>exec_moves)+


[STATEMENT]
lemma \<tau>Exec_movet_\<tau>Exec_movest:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movest ci P t (e # es) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movest ci P t (e # es) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl \<tau>exec_move_into_\<tau>exec_moves)+


[STATEMENT]
lemma exec_moves_append: "exec_moves ci P t es h s ta h' s' \<Longrightarrow> exec_moves ci P t (es @ es') h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_moves ci P t es h s ta h' s' \<Longrightarrow> exec_moves ci P t (es @ es') h s ta h' s'
[PROOF STEP]
by(auto simp add: exec_moves_def)


[STATEMENT]
lemma \<tau>exec_moves_append: "\<tau>exec_moves ci P t es h s s' \<Longrightarrow> \<tau>exec_moves ci P t (es @ es') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_moves ci P t es h s s' \<Longrightarrow> \<tau>exec_moves ci P t (es @ es') h s s'
[PROOF STEP]
by(cases s)(auto elim!: \<tau>exec_movesE intro!: \<tau>exec_movesI exec_moves_append)


[STATEMENT]
lemma \<tau>Exec_movesr_append [intro]:
  "\<tau>Exec_movesr ci P t es h s s' \<Longrightarrow> \<tau>Exec_movesr ci P t (es @ es') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movesr ci P t es h s s' \<Longrightarrow> \<tau>Exec_movesr ci P t (es @ es') h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl \<tau>exec_moves_append)+


[STATEMENT]
lemma \<tau>Exec_movest_append [intro]:
  "\<tau>Exec_movest ci P t es h s s' \<Longrightarrow> \<tau>Exec_movest ci P t (es @ es') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movest ci P t es h s s' \<Longrightarrow> \<tau>Exec_movest ci P t (es @ es') h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl \<tau>exec_moves_append)+


[STATEMENT]
lemma append_exec_moves:
  assumes len: "length vs = length es'"
  and exec: "exec_moves ci P t es h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_moves ci P t (es' @ es) h ((stk @ vs), loc, (length (compEs2 es') + pc), xcp) ta h' ((stk' @ vs), loc', (length (compEs2 es') + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_moves ci P t (es' @ es) h (stk @ vs, loc, length (compEs2 es') + pc, xcp) ta h' (stk' @ vs, loc', length (compEs2 es') + pc', xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_moves ci P t (es' @ es) h (stk @ vs, loc, length (compEs2 es') + pc, xcp) ta h' (stk' @ vs, loc', length (compEs2 es') + 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_moves ci P t (es' @ es) h (stk @ vs, loc, length (compEs2 es') + pc, xcp) ta h' (stk' @ vs, loc', length (compEs2 es') + pc', xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) (compEs2 es) (stack_xlift (length vs) (compxEs2 es 0 0)) t h ((stk @ vs), loc, pc, xcp) ta h' ((stk' @ vs), loc', pc', xcp')"
[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) (stack_xlift (length vs) (compxEs2 es 0 0)) t h (stk @ vs, loc, pc, xcp) ta h' (stk' @ vs, loc', pc', xcp')
[PROOF STEP]
by(rule exec_meth_stk_offer)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compEs2 es) (stack_xlift (length vs) (compxEs2 es 0 0)) t h (stk @ vs, loc, pc, xcp) ta h' (stk' @ vs, loc', pc', xcp')

goal (1 subgoal):
 1. exec_moves ci P t (es' @ es) h (stk @ vs, loc, length (compEs2 es') + pc, xcp) ta h' (stk' @ vs, loc', length (compEs2 es') + pc', xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) (compEs2 es' @ compEs2 es) (compxEs2 es' 0 0 @ shift (length (compEs2 es')) (stack_xlift (length (vs)) (compxEs2 es 0 0))) t h ((stk @ vs), loc, (length (compEs2 es') + pc), xcp) ta h' ((stk' @ vs), loc', (length (compEs2 es') + pc'), xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compEs2 es) (stack_xlift (length vs) (compxEs2 es 0 0)) t h (stk @ vs, loc, pc, xcp) ta h' (stk' @ vs, loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compEs2 es' @ compEs2 es) (compxEs2 es' 0 0 @ shift (length (compEs2 es')) (stack_xlift (length vs) (compxEs2 es 0 0))) t h (stk @ vs, loc, length (compEs2 es') + pc, xcp) ta h' (stk' @ vs, loc', length (compEs2 es') + pc', xcp')
[PROOF STEP]
by(rule append_exec_meth_xt) auto
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compEs2 es' @ compEs2 es) (compxEs2 es' 0 0 @ shift (length (compEs2 es')) (stack_xlift (length vs) (compxEs2 es 0 0))) t h (stk @ vs, loc, length (compEs2 es') + pc, xcp) ta h' (stk' @ vs, loc', length (compEs2 es') + pc', xcp')

goal (1 subgoal):
 1. exec_moves ci P t (es' @ es) h (stk @ vs, loc, length (compEs2 es') + pc, xcp) ta h' (stk' @ vs, loc', length (compEs2 es') + pc', xcp')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compEs2 es' @ compEs2 es) (compxEs2 es' 0 0 @ shift (length (compEs2 es')) (stack_xlift (length vs) (compxEs2 es 0 0))) t h (stk @ vs, loc, length (compEs2 es') + pc, xcp) ta h' (stk' @ vs, loc', length (compEs2 es') + pc', xcp')

goal (1 subgoal):
 1. exec_moves ci P t (es' @ es) h (stk @ vs, loc, length (compEs2 es') + pc, xcp) ta h' (stk' @ vs, loc', length (compEs2 es') + pc', xcp')
[PROOF STEP]
by(simp add: exec_moves_def stack_xlift_compxEs2 shift_compxEs2 len)
[PROOF STATE]
proof (state)
this:
exec_moves ci P t (es' @ es) h (stk @ vs, loc, length (compEs2 es') + pc, xcp) ta h' (stk' @ vs, loc', length (compEs2 es') + pc', xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma append_\<tau>exec_moves:
  "\<lbrakk> length vs = length es';
    \<tau>exec_moves ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<rbrakk>
  \<Longrightarrow> \<tau>exec_moves ci P t (es' @ es) h ((stk @ vs), loc, (length (compEs2 es') + pc), xcp) ((stk' @ vs), loc', (length (compEs2 es') + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length vs = length es'; \<tau>exec_moves ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp')\<rbrakk> \<Longrightarrow> \<tau>exec_moves ci P t (es' @ es) h (stk @ vs, loc, length (compEs2 es') + pc, xcp) (stk' @ vs, loc', length (compEs2 es') + pc', xcp')
[PROOF STEP]
by(auto elim!: \<tau>exec_movesE intro: \<tau>exec_movesI append_exec_moves \<tau>moves2_stk_append append_\<tau>moves2)


[STATEMENT]
lemma append_\<tau>Exec_movesr:
  assumes len: "length vs = length es'"
  shows "\<tau>Exec_movesr ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movesr ci P t (es' @ es) h ((stk @ vs), loc, (length (compEs2 es') + pc), xcp) ((stk' @ vs), loc', (length (compEs2 es') + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movesr ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movesr ci P t (es' @ es) h (stk @ vs, loc, length (compEs2 es') + pc, xcp) (stk' @ vs, loc', length (compEs2 es') + pc', xcp')
[PROOF STEP]
by(induct rule: rtranclp_induct4)(blast intro: rtranclp.rtrancl_into_rtrancl append_\<tau>exec_moves[OF len])+


[STATEMENT]
lemma append_\<tau>Exec_movest:
  assumes len: "length vs = length es'"
  shows "\<tau>Exec_movest ci P t es h  (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movest ci P t (es' @ es) h ((stk @ vs), loc, (length (compEs2 es') + pc), xcp)  ((stk' @ vs), loc', (length (compEs2 es') + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movest ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movest ci P t (es' @ es) h (stk @ vs, loc, length (compEs2 es') + pc, xcp) (stk' @ vs, loc', length (compEs2 es') + pc', xcp')
[PROOF STEP]
by(induct rule: tranclp_induct4)(blast intro: tranclp.trancl_into_trancl append_\<tau>exec_moves[OF len])+


[STATEMENT]
lemma NewArray_\<tau>execI:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (newA T\<lfloor>e\<rceil>) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (newA T\<lfloor>e\<rceil>) h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_newArrayI)


[STATEMENT]
lemma Cast_\<tau>execI:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (Cast T e) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (Cast T e) h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_CastI)


[STATEMENT]
lemma InstanceOf_\<tau>execI:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e instanceof T) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e instanceof T) h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_InstanceOfI)


[STATEMENT]
lemma BinOp_\<tau>execI1:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e \<guillemotleft>bop\<guillemotright> e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e \<guillemotleft>bop\<guillemotright> e') h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_BinOpI1)


[STATEMENT]
lemma BinOp_\<tau>execI2:
  "\<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (e \<guillemotleft>bop\<guillemotright> e') h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (e \<guillemotleft>bop\<guillemotright> e') h (stk @ [v], loc, length (compE2 e) + pc, xcp) (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_BinOpI2 \<tau>move2_stk_append)


[STATEMENT]
lemma LAss_\<tau>execI:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (V := e) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (V:=e) h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_LAssI)


[STATEMENT]
lemma AAcc_\<tau>execI1:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<lfloor>i\<rceil>) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<lfloor>i\<rceil>) h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_AAccI1)


[STATEMENT]
lemma AAcc_\<tau>execI2:
  "\<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (e\<lfloor>e'\<rceil>) h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (e\<lfloor>e'\<rceil>) h (stk @ [v], loc, length (compE2 e) + pc, xcp) (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_AAccI2 \<tau>move2_stk_append)


[STATEMENT]
lemma AAss_\<tau>execI1:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<lfloor>i\<rceil> := e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<lfloor>i\<rceil> := e') h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_AAssI1)


[STATEMENT]
lemma AAss_\<tau>execI2:
  "\<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk @ [v], loc, length (compE2 e) + pc, xcp) (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_AAssI2 \<tau>move2_stk_append)


[STATEMENT]
lemma AAss_\<tau>execI3:
  "\<tau>exec_move ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h ((stk @ [v, v']), loc, (length (compE2 e) + length (compE2 e') + pc), xcp) ((stk' @ [v, v']), loc', (length (compE2 e) + length (compE2 e') + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (e\<lfloor>e'\<rceil> := e'') h (stk @ [v, v'], loc, length (compE2 e) + length (compE2 e') + pc, xcp) (stk' @ [v, v'], loc', length (compE2 e) + length (compE2 e') + pc', xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_AAssI3 \<tau>move2_stk_append)


[STATEMENT]
lemma ALength_\<tau>execI:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>length) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>length) h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_ALengthI)


[STATEMENT]
lemma FAcc_\<tau>execI:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>F{D}) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>F{D}) h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_FAccI)


[STATEMENT]
lemma FAss_\<tau>execI1:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>F{D} := e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>F{D} := e') h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_FAssI1)


[STATEMENT]
lemma FAss_\<tau>execI2:
  "\<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>F{D} := e') h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>F{D} := e') h (stk @ [v], loc, length (compE2 e) + pc, xcp) (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_FAssI2 \<tau>move2_stk_append)


[STATEMENT]
lemma CAS_\<tau>execI1:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_CASI1)


[STATEMENT]
lemma CAS_\<tau>execI2:
  "\<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk @ [v], loc, length (compE2 e) + pc, xcp) (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_CASI2 \<tau>move2_stk_append)


[STATEMENT]
lemma CAS_\<tau>execI3:
  "\<tau>exec_move ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h ((stk @ [v, v']), loc, (length (compE2 e) + length (compE2 e') + pc), xcp) ((stk' @ [v, v']), loc', (length (compE2 e) + length (compE2 e') + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk @ [v, v'], loc, length (compE2 e) + length (compE2 e') + pc, xcp) (stk' @ [v, v'], loc', length (compE2 e) + length (compE2 e') + pc', xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_CASI3 \<tau>move2_stk_append)


[STATEMENT]
lemma Call_\<tau>execI1:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>M(es)) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>M(es)) h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_CallI1)


[STATEMENT]
lemma Call_\<tau>execI2:
  "\<tau>exec_moves ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>M(es)) h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_moves ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (e\<bullet>M(es)) h (stk @ [v], loc, length (compE2 e) + pc, xcp) (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_movesE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_CallI2 \<tau>moves2_stk_append)


[STATEMENT]
lemma Block_\<tau>execI_Some:
  "\<tau>exec_move ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) (stk', loc', Suc (Suc pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) (stk', loc', Suc (Suc pc'), xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_BlockSomeI)


[STATEMENT]
lemma Block_\<tau>execI_None:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t {V:T=None; e} h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t {V:T=None; e} h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_BlockNoneI)


[STATEMENT]
lemma Sync_\<tau>execI:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_SyncI1)


[STATEMENT]
lemma Insync_\<tau>execI:
  "\<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, Suc (Suc (Suc (length (compE2 e) + pc))), xcp) (stk', loc', Suc (Suc (Suc (length (compE2 e) + pc'))), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, Suc (Suc (Suc (length (compE2 e) + pc))), xcp) (stk', loc', Suc (Suc (Suc (length (compE2 e) + pc'))), xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_SyncI2)


[STATEMENT]
lemma Seq_\<tau>execI1:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e;; e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (e;; e') h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_SeqI1)


[STATEMENT]
lemma Seq_\<tau>execI2:
  "\<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (e;; e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) (stk', loc', Suc (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (e;; e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_SeqI2)


[STATEMENT]
lemma Cond_\<tau>execI1:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (if (e) e' else e'') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (if (e) e' else e'') h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_CondI1)


[STATEMENT]
lemma Cond_\<tau>execI2:
  "\<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (if (e) e' else e'') h (stk, loc, Suc (length (compE2 e) + pc), xcp) (stk', loc', Suc (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (if (e) e' else e'') h (stk, loc, Suc (length (compE2 e) + pc), xcp) (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_CondI2)


[STATEMENT]
lemma Cond_\<tau>execI3:
  "\<tau>exec_move ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (if (e) e' else e'') h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e') + pc)), xcp) (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e') + pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (if (e) e' else e'') h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e') + pc)), xcp) (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e') + pc')), xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_CondI3)


[STATEMENT]
lemma While_\<tau>execI1:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (while (e) e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (while (e) e') h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_WhileI1)


[STATEMENT]
lemma Throw_\<tau>execI:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (throw e) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (throw e) h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_ThrowI)


[STATEMENT]
lemma Try_\<tau>execI1:
  "\<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (try e catch(C V) e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e h s s' \<Longrightarrow> \<tau>exec_move ci P t (try e catch(C V) e') h s s'
[PROOF STEP]
by(cases s)(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_TryI1)


[STATEMENT]
lemma Try_\<tau>execI2:
  "\<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp')
[PROOF STEP]
by(blast elim: \<tau>exec_moveE intro: \<tau>exec_moveI \<tau>move2_\<tau>moves2.intros exec_move_TryI2)


[STATEMENT]
lemma NewArray_\<tau>ExecrI:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (newA T\<lfloor>e\<rceil>) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (newA T\<lfloor>e\<rceil>) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl NewArray_\<tau>execI)+


[STATEMENT]
lemma Cast_\<tau>ExecrI:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (Cast T e) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (Cast T e) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Cast_\<tau>execI)+


[STATEMENT]
lemma InstanceOf_\<tau>ExecrI:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e instanceof T) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e instanceof T) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl InstanceOf_\<tau>execI)+


[STATEMENT]
lemma BinOp_\<tau>ExecrI1:
  "\<tau>Exec_mover ci P t e1 h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e1 \<guillemotleft>bop\<guillemotright> e2) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e1 h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e1 \<guillemotleft>bop\<guillemotright> e2) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl BinOp_\<tau>execI1)+


[STATEMENT]
lemma BinOp_\<tau>ExecrI2:
  "\<tau>Exec_mover ci P t e2 h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_mover ci P t (e \<guillemotleft>bop\<guillemotright> e2)  h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e2 h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (e \<guillemotleft>bop\<guillemotright> e2) h (stk @ [v], loc, length (compE2 e) + pc, xcp) (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl BinOp_\<tau>execI2)+


[STATEMENT]
lemma LAss_\<tau>ExecrI:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (V := e) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (V:=e) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl LAss_\<tau>execI)+


[STATEMENT]
lemma AAcc_\<tau>ExecrI1:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e\<lfloor>i\<rceil>) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e\<lfloor>i\<rceil>) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl AAcc_\<tau>execI1)+


[STATEMENT]
lemma AAcc_\<tau>ExecrI2:
  "\<tau>Exec_mover ci P t i h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_mover ci P t (a\<lfloor>i\<rceil>) h ((stk @ [v]), loc, (length (compE2 a) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 a) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t i h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (a\<lfloor>i\<rceil>) h (stk @ [v], loc, length (compE2 a) + pc, xcp) (stk' @ [v], loc', length (compE2 a) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl AAcc_\<tau>execI2)+


[STATEMENT]
lemma AAss_\<tau>ExecrI1:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e\<lfloor>i\<rceil> := e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e\<lfloor>i\<rceil> := e') h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl AAss_\<tau>execI1)+


[STATEMENT]
lemma AAss_\<tau>ExecrI2:
  "\<tau>Exec_mover ci P t i h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_mover ci P t (a\<lfloor>i\<rceil> := e) h ((stk @ [v]), loc, (length (compE2 a) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 a) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t i h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (a\<lfloor>i\<rceil> := e) h (stk @ [v], loc, length (compE2 a) + pc, xcp) (stk' @ [v], loc', length (compE2 a) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl AAss_\<tau>execI2)+


[STATEMENT]
lemma AAss_\<tau>ExecrI3:
  "\<tau>Exec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_mover ci P t (a\<lfloor>i\<rceil> := e) h ((stk @ [v, v']), loc, (length (compE2 a) + length (compE2 i) + pc), xcp) ((stk' @ [v, v']), loc', (length (compE2 a) + length (compE2 i) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (a\<lfloor>i\<rceil> := e) h (stk @ [v, v'], loc, length (compE2 a) + length (compE2 i) + pc, xcp) (stk' @ [v, v'], loc', length (compE2 a) + length (compE2 i) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl AAss_\<tau>execI3)+


[STATEMENT]
lemma ALength_\<tau>ExecrI:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>length) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>length) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl ALength_\<tau>execI)+


[STATEMENT]
lemma FAcc_\<tau>ExecrI:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>F{D}) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>F{D}) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl FAcc_\<tau>execI)+


[STATEMENT]
lemma FAss_\<tau>ExecrI1:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>F{D} := e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>F{D} := e') h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl FAss_\<tau>execI1)+


[STATEMENT]
lemma FAss_\<tau>ExecrI2:
  "\<tau>Exec_mover ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>F{D} := e') h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>F{D} := e') h (stk @ [v], loc, length (compE2 e) + pc, xcp) (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl FAss_\<tau>execI2)+


[STATEMENT]
lemma CAS_\<tau>ExecrI1:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl CAS_\<tau>execI1)+


[STATEMENT]
lemma CAS_\<tau>ExecrI2:
  "\<tau>Exec_mover ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk @ [v], loc, length (compE2 e) + pc, xcp) (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl CAS_\<tau>execI2)+


[STATEMENT]
lemma CAS_\<tau>ExecrI3:
  "\<tau>Exec_mover ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h ((stk @ [v, v']), loc, (length (compE2 e) + length (compE2 e') + pc), xcp) ((stk' @ [v, v']), loc', (length (compE2 e) + length (compE2 e') + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk @ [v, v'], loc, length (compE2 e) + length (compE2 e') + pc, xcp) (stk' @ [v, v'], loc', length (compE2 e) + length (compE2 e') + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl CAS_\<tau>execI3)+


[STATEMENT]
lemma Call_\<tau>ExecrI1:
  "\<tau>Exec_mover ci P t obj h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (obj\<bullet>M'(es)) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t obj h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (obj\<bullet>M'(es)) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Call_\<tau>execI1)+


[STATEMENT]
lemma Call_\<tau>ExecrI2:
  "\<tau>Exec_movesr ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_mover ci P t (obj\<bullet>M'(es)) h ((stk @ [v]), loc, (length (compE2 obj) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 obj) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movesr ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (obj\<bullet>M'(es)) h (stk @ [v], loc, length (compE2 obj) + pc, xcp) (stk' @ [v], loc', length (compE2 obj) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Execsr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Call_\<tau>execI2)+


[STATEMENT]
lemma Block_\<tau>ExecrI_Some:
  "\<tau>Exec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_mover ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, (Suc (Suc pc)), xcp) (stk', loc', (Suc (Suc pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) (stk', loc', Suc (Suc pc'), xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Block_\<tau>execI_Some)+


[STATEMENT]
lemma Block_\<tau>ExecrI_None:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t {V:T=None; e} h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t {V:T=None; e} h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Block_\<tau>execI_None)+


[STATEMENT]
lemma Sync_\<tau>ExecrI:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (sync\<^bsub>V\<^esub> (e) e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (sync\<^bsub>V\<^esub> (e) e') h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Sync_\<tau>execI)+


[STATEMENT]
lemma Insync_\<tau>ExecrI:
  "\<tau>Exec_mover ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_mover ci P t (sync\<^bsub>V\<^esub> (e) e')  h (stk, loc, (Suc (Suc (Suc (length (compE2 e) + pc)))), xcp) (stk', loc', (Suc (Suc (Suc (length (compE2 e) + pc')))), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, Suc (Suc (Suc (length (compE2 e) + pc))), xcp) (stk', loc', Suc (Suc (Suc (length (compE2 e) + pc'))), xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Insync_\<tau>execI)+


[STATEMENT]
lemma Seq_\<tau>ExecrI1:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e;;e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (e;; e') h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Seq_\<tau>execI1)+


[STATEMENT]
lemma Seq_\<tau>ExecrI2:
  "\<tau>Exec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc' ,xcp') \<Longrightarrow>
   \<tau>Exec_mover ci P t (e';;e) h (stk, loc, (Suc (length (compE2 e') + pc)), xcp) (stk', loc', (Suc (length (compE2 e') + pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) (stk', loc', Suc (length (compE2 e') + pc'), xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Seq_\<tau>execI2)+


[STATEMENT]
lemma Cond_\<tau>ExecrI1:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (if (e) e1 else e2) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (if (e) e1 else e2) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Cond_\<tau>execI1)+


[STATEMENT]
lemma Cond_\<tau>ExecrI2:
  "\<tau>Exec_mover ci P t e1  h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow>
   \<tau>Exec_mover ci P t (if (e) e1 else e2)  h (stk, loc, (Suc (length (compE2 e) + pc)), xcp) (stk', loc', (Suc (length (compE2 e) + pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e1 h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Cond_\<tau>execI2)+


[STATEMENT]
lemma Cond_\<tau>ExecrI3:
  "\<tau>Exec_mover ci P t e2  h (stk, loc ,pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow>
   \<tau>Exec_mover ci P t (if (e) e1 else e2)  h (stk, loc, (Suc (Suc (length (compE2 e) + length (compE2 e1) + pc))), xcp)  (stk', loc', (Suc (Suc (length (compE2 e) + length (compE2 e1) + pc'))), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e2 h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Cond_\<tau>execI3)+


[STATEMENT]
lemma While_\<tau>ExecrI1:
  "\<tau>Exec_mover ci P t c h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (while (c) e) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t c h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (while (c) e) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl While_\<tau>execI1)+


[STATEMENT]
lemma While_\<tau>ExecrI2:
  "\<tau>Exec_mover ci P t E h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_mover ci P t (while (c) E)  h (stk, loc ,(Suc (length (compE2 c) + pc)), xcp) (stk', loc', (Suc (length (compE2 c) + pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t E h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (while (c) E) h (stk, loc, Suc (length (compE2 c) + pc), xcp) (stk', loc', Suc (length (compE2 c) + pc'), xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl While_\<tau>execI2)+


[STATEMENT]
lemma Throw_\<tau>ExecrI:
  "\<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (throw e) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (throw e) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Throw_\<tau>execI)+


[STATEMENT]
lemma Try_\<tau>ExecrI1:
  "\<tau>Exec_mover ci P t E h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (try E catch(C' V) e) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t E h s s' \<Longrightarrow> \<tau>Exec_mover ci P t (try E catch(C' V) e) h s s'
[PROOF STEP]
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Try_\<tau>execI1)+


[STATEMENT]
lemma Try_\<tau>ExecrI2:
  "\<tau>Exec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_mover ci P t (try E catch(C' V) e)  h (stk, loc, (Suc (Suc (length (compE2 E) + pc))), xcp)  (stk', loc', (Suc (Suc (length (compE2 E) + pc'))), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_mover ci P t (try E catch(C' V) e) h (stk, loc, Suc (Suc (length (compE2 E) + pc)), xcp) (stk', loc', Suc (Suc (length (compE2 E) + pc')), xcp')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Try_\<tau>execI2)+


[STATEMENT]
lemma NewArray_\<tau>ExectI:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (newA T\<lfloor>e\<rceil>) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (newA T\<lfloor>e\<rceil>) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl NewArray_\<tau>execI)+


[STATEMENT]
lemma Cast_\<tau>ExectI:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (Cast T e) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (Cast T e) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Cast_\<tau>execI)+


[STATEMENT]
lemma InstanceOf_\<tau>ExectI:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e instanceof T) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e instanceof T) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl InstanceOf_\<tau>execI)+


[STATEMENT]
lemma BinOp_\<tau>ExectI1:
  "\<tau>Exec_movet ci P t e1 h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e1 \<guillemotleft>bop\<guillemotright> e2) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e1 h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e1 \<guillemotleft>bop\<guillemotright> e2) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl BinOp_\<tau>execI1)+


[STATEMENT]
lemma BinOp_\<tau>ExectI2:
  "\<tau>Exec_movet ci P t e2 h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movet ci P t (e \<guillemotleft>bop\<guillemotright> e2)  h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e2 h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (e \<guillemotleft>bop\<guillemotright> e2) h (stk @ [v], loc, length (compE2 e) + pc, xcp) (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl BinOp_\<tau>execI2)+


[STATEMENT]
lemma LAss_\<tau>ExectI:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (V := e) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (V:=e) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl LAss_\<tau>execI)+


[STATEMENT]
lemma AAcc_\<tau>ExectI1:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e\<lfloor>i\<rceil>) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e\<lfloor>i\<rceil>) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl AAcc_\<tau>execI1)+


[STATEMENT]
lemma AAcc_\<tau>ExectI2:
  "\<tau>Exec_movet ci P t i h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movet ci P t (a\<lfloor>i\<rceil>) h ((stk @ [v]), loc, (length (compE2 a) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 a) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t i h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (a\<lfloor>i\<rceil>) h (stk @ [v], loc, length (compE2 a) + pc, xcp) (stk' @ [v], loc', length (compE2 a) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl AAcc_\<tau>execI2)+


[STATEMENT]
lemma AAss_\<tau>ExectI1:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e\<lfloor>i\<rceil> := e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e\<lfloor>i\<rceil> := e') h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl AAss_\<tau>execI1)+


[STATEMENT]
lemma AAss_\<tau>ExectI2:
  "\<tau>Exec_movet ci P t i h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movet ci P t (a\<lfloor>i\<rceil> := e) h ((stk @ [v]), loc, (length (compE2 a) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 a) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t i h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (a\<lfloor>i\<rceil> := e) h (stk @ [v], loc, length (compE2 a) + pc, xcp) (stk' @ [v], loc', length (compE2 a) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl AAss_\<tau>execI2)+


[STATEMENT]
lemma AAss_\<tau>ExectI3:
  "\<tau>Exec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movet ci P t (a\<lfloor>i\<rceil> := e) h ((stk @ [v, v']), loc, (length (compE2 a) + length (compE2 i) + pc), xcp) ((stk' @ [v, v']), loc', (length (compE2 a) + length (compE2 i) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (a\<lfloor>i\<rceil> := e) h (stk @ [v, v'], loc, length (compE2 a) + length (compE2 i) + pc, xcp) (stk' @ [v, v'], loc', length (compE2 a) + length (compE2 i) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl AAss_\<tau>execI3)+


[STATEMENT]
lemma ALength_\<tau>ExectI:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>length) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>length) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl ALength_\<tau>execI)+


[STATEMENT]
lemma FAcc_\<tau>ExectI:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>F{D}) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>F{D}) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl FAcc_\<tau>execI)+


[STATEMENT]
lemma FAss_\<tau>ExectI1:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>F{D} := e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>F{D} := e') h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl FAss_\<tau>execI1)+


[STATEMENT]
lemma FAss_\<tau>ExectI2:
  "\<tau>Exec_movet ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>F{D} := e') h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>F{D} := e') h (stk @ [v], loc, length (compE2 e) + pc, xcp) (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl FAss_\<tau>execI2)+


[STATEMENT]
lemma CAS_\<tau>ExectI1:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl CAS_\<tau>execI1)+


[STATEMENT]
lemma CAS_\<tau>ExectI2:
  "\<tau>Exec_movet ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk @ [v], loc, length (compE2 e) + pc, xcp) (stk' @ [v], loc', length (compE2 e) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl CAS_\<tau>execI2)+


[STATEMENT]
lemma CAS_\<tau>ExectI3:
  "\<tau>Exec_movet ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h ((stk @ [v, v']), loc, (length (compE2 e) + length (compE2 e') + pc), xcp) ((stk' @ [v, v']), loc', (length (compE2 e) + length (compE2 e') + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (e\<bullet>compareAndSwap(D\<bullet>F, e', e'')) h (stk @ [v, v'], loc, length (compE2 e) + length (compE2 e') + pc, xcp) (stk' @ [v, v'], loc', length (compE2 e) + length (compE2 e') + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl CAS_\<tau>execI3)+


[STATEMENT]
lemma Call_\<tau>ExectI1:
  "\<tau>Exec_movet ci P t obj h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (obj\<bullet>M'(es)) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t obj h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (obj\<bullet>M'(es)) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Call_\<tau>execI1)+


[STATEMENT]
lemma Call_\<tau>ExectI2:
  "\<tau>Exec_movest ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movet ci P t (obj\<bullet>M'(es)) h ((stk @ [v]), loc, (length (compE2 obj) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 obj) + pc'), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movest ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (obj\<bullet>M'(es)) h (stk @ [v], loc, length (compE2 obj) + pc, xcp) (stk' @ [v], loc', length (compE2 obj) + pc', xcp')
[PROOF STEP]
by(induct rule: \<tau>Execst_induct)(blast intro: tranclp.trancl_into_trancl Call_\<tau>execI2)+


[STATEMENT]
lemma Block_\<tau>ExectI_Some:
  "\<tau>Exec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movet ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, (Suc (Suc pc)), xcp) (stk', loc', (Suc (Suc pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t {V:T=\<lfloor>v\<rfloor>; e} h (stk, loc, Suc (Suc pc), xcp) (stk', loc', Suc (Suc pc'), xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl Block_\<tau>execI_Some)+


[STATEMENT]
lemma Block_\<tau>ExectI_None:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t {V:T=None; e} h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t {V:T=None; e} h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Block_\<tau>execI_None)+


[STATEMENT]
lemma Sync_\<tau>ExectI:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (sync\<^bsub>V\<^esub> (e) e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (sync\<^bsub>V\<^esub> (e) e') h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Sync_\<tau>execI)+


[STATEMENT]
lemma Insync_\<tau>ExectI:
  "\<tau>Exec_movet ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movet ci P t (sync\<^bsub>V\<^esub> (e) e')  h (stk, loc, (Suc (Suc (Suc (length (compE2 e) + pc)))), xcp) (stk', loc', (Suc (Suc (Suc (length (compE2 e) + pc')))), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (sync\<^bsub>V\<^esub> (e) e') h (stk, loc, Suc (Suc (Suc (length (compE2 e) + pc))), xcp) (stk', loc', Suc (Suc (Suc (length (compE2 e) + pc'))), xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl Insync_\<tau>execI)+


[STATEMENT]
lemma Seq_\<tau>ExectI1:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e;;e') h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (e;; e') h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Seq_\<tau>execI1)+


[STATEMENT]
lemma Seq_\<tau>ExectI2:
  "\<tau>Exec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc' ,xcp') \<Longrightarrow>
   \<tau>Exec_movet ci P t (e';;e) h (stk, loc, (Suc (length (compE2 e') + pc)), xcp) (stk', loc', (Suc (length (compE2 e') + pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) (stk', loc', Suc (length (compE2 e') + pc'), xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl Seq_\<tau>execI2)+


[STATEMENT]
lemma Cond_\<tau>ExectI1:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (if (e) e1 else e2) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (if (e) e1 else e2) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Cond_\<tau>execI1)+


[STATEMENT]
lemma Cond_\<tau>ExectI2:
  "\<tau>Exec_movet ci P t e1  h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow>
   \<tau>Exec_movet ci P t (if (e) e1 else e2)  h (stk, loc, (Suc (length (compE2 e) + pc)), xcp) (stk', loc', (Suc (length (compE2 e) + pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e1 h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl Cond_\<tau>execI2)+


[STATEMENT]
lemma Cond_\<tau>ExectI3:
  "\<tau>Exec_movet ci P t e2  h (stk, loc ,pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow>
   \<tau>Exec_movet ci P t (if (e) e1 else e2)  h (stk, loc, (Suc (Suc (length (compE2 e) + length (compE2 e1) + pc))), xcp)  (stk', loc', (Suc (Suc (length (compE2 e) + length (compE2 e1) + pc'))), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e2 h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl Cond_\<tau>execI3)+


[STATEMENT]
lemma While_\<tau>ExectI1:
  "\<tau>Exec_movet ci P t c h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (while (c) e) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t c h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (while (c) e) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl While_\<tau>execI1)+


[STATEMENT]
lemma While_\<tau>ExectI2:
  "\<tau>Exec_movet ci P t E h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movet ci P t (while (c) E)  h (stk, loc ,(Suc (length (compE2 c) + pc)), xcp) (stk', loc', (Suc (length (compE2 c) + pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t E h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (while (c) E) h (stk, loc, Suc (length (compE2 c) + pc), xcp) (stk', loc', Suc (length (compE2 c) + pc'), xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl While_\<tau>execI2)+


[STATEMENT]
lemma Throw_\<tau>ExectI:
  "\<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (throw e) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (throw e) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Throw_\<tau>execI)+


[STATEMENT]
lemma Try_\<tau>ExectI1:
  "\<tau>Exec_movet ci P t E h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (try E catch(C' V) e) h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t E h s s' \<Longrightarrow> \<tau>Exec_movet ci P t (try E catch(C' V) e) h s s'
[PROOF STEP]
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Try_\<tau>execI1)+


[STATEMENT]
lemma Try_\<tau>ExectI2:
  "\<tau>Exec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  \<Longrightarrow> \<tau>Exec_movet ci P t (try E catch(C' V) e)  h (stk, loc, (Suc (Suc (length (compE2 E) + pc))), xcp)  (stk', loc', (Suc (Suc (length (compE2 E) + pc'))), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> \<tau>Exec_movet ci P t (try E catch(C' V) e) h (stk, loc, Suc (Suc (length (compE2 E) + pc)), xcp) (stk', loc', Suc (Suc (length (compE2 E) + pc')), xcp')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl Try_\<tau>execI2)+


[STATEMENT]
lemma \<tau>Exec_movesr_map_Val:
  "\<tau>Exec_movesr_a P t (map Val vs) h ([], xs, 0, None) ((rev vs), xs, (length (compEs2 (map Val vs))), None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movesr_a P t (map Val vs) h ([], xs, 0, None) (rev vs, xs, length (compEs2 (map Val vs)), None)
[PROOF STEP]
proof(induct vs arbitrary: pc stk Ts rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<tau>Exec_movesr_a P t (map Val []) h ([], xs, 0, None) (rev [], xs, length (compEs2 (map Val [])), None)
 2. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<tau>Exec_movesr_a P t (map Val []) h ([], xs, 0, None) (rev [], xs, length (compEs2 (map Val [])), None)
 2. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movesr_a P t (map Val []) h ([], xs, 0, None) (rev [], xs, length (compEs2 (map Val [])), None)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<tau>Exec_movesr_a P t (map Val []) h ([], xs, 0, None) (rev [], xs, length (compEs2 (map Val [])), None)

goal (1 subgoal):
 1. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
case (snoc v vs')
[PROOF STATE]
proof (state)
this:
\<tau>Exec_movesr_a P t (map Val vs') h ([], xs, 0, None) (rev vs', xs, length (compEs2 (map Val vs')), None)

goal (1 subgoal):
 1. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
let ?E = "compEs2 (map Val vs')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
from snoc
[PROOF STATE]
proof (chain)
picking this:
\<tau>Exec_movesr_a P t (map Val vs') h ([], xs, 0, None) (rev vs', xs, length (compEs2 (map Val vs')), None)
[PROOF STEP]
have "\<tau>Exec_movesr_a P t (map Val (vs' @ [v])) h ([], xs, 0, None) ((rev vs'), xs, (length ?E), None)"
[PROOF STATE]
proof (prove)
using this:
\<tau>Exec_movesr_a P t (map Val vs') h ([], xs, 0, None) (rev vs', xs, length (compEs2 (map Val vs')), None)

goal (1 subgoal):
 1. \<tau>Exec_movesr_a P t (map Val (vs' @ [v])) h ([], xs, 0, None) (rev vs', xs, length (compEs2 (map Val vs')), None)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau>Exec_movesr_a P t (map Val (vs' @ [v])) h ([], xs, 0, None) (rev vs', xs, length (compEs2 (map Val vs')), None)

goal (1 subgoal):
 1. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<tau>Exec_movesr_a P t (map Val (vs' @ [v])) h ([], xs, 0, None) (rev vs', xs, length (compEs2 (map Val vs')), None)

goal (1 subgoal):
 1. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<tau>Exec_movesr_a P t (map Val (vs' @ [v])) h ([], xs, 0, None) (rev vs', xs, length (compEs2 (map Val vs')), None)

goal (1 subgoal):
 1. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
have "exec_meth_a (compP2 P) (?E @ [Push v]) (compxEs2 (map Val vs') 0 0 @ shift (length ?E) []) t h ((rev vs'), xs, (length ?E + 0), None) \<epsilon> h ((v # rev vs'), xs, (length ?E + Suc 0), None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth_a (compP2 P) (compEs2 (map Val vs') @ [Push v]) (compxEs2 (map Val vs') 0 0 @ shift (length (compEs2 (map Val vs'))) []) t h (rev vs', xs, length (compEs2 (map Val vs')) + 0, None) \<lbrace>\<rbrace> h (v # rev vs', xs, length (compEs2 (map Val vs')) + Suc 0, None)
[PROOF STEP]
by -(rule append_exec_meth_xt, auto simp add: exec_meth_instr)
[PROOF STATE]
proof (state)
this:
exec_meth_a (compP2 P) (compEs2 (map Val vs') @ [Push v]) (compxEs2 (map Val vs') 0 0 @ shift (length (compEs2 (map Val vs'))) []) t h (rev vs', xs, length (compEs2 (map Val vs')) + 0, None) \<lbrace>\<rbrace> h (v # rev vs', xs, length (compEs2 (map Val vs')) + Suc 0, None)

goal (1 subgoal):
 1. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
exec_meth_a (compP2 P) (compEs2 (map Val vs') @ [Push v]) (compxEs2 (map Val vs') 0 0 @ shift (length (compEs2 (map Val vs'))) []) t h (rev vs', xs, length (compEs2 (map Val vs')) + 0, None) \<lbrace>\<rbrace> h (v # rev vs', xs, length (compEs2 (map Val vs')) + Suc 0, None)

goal (1 subgoal):
 1. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
have "\<tau>moves2 (compP2 P) h (rev vs') (map Val vs' @ [Val v]) (length (compEs2 (map Val vs')) + 0) None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>moves2 (compP2 P) h (rev vs') (map Val vs' @ [Val v]) (length (compEs2 (map Val vs')) + 0) None
[PROOF STEP]
by(rule append_\<tau>moves2 \<tau>moves2Hd \<tau>move2Val)+
[PROOF STATE]
proof (state)
this:
\<tau>moves2 (compP2 P) h (rev vs') (map Val vs' @ [Val v]) (length (compEs2 (map Val vs')) + 0) None

goal (1 subgoal):
 1. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
exec_meth_a (compP2 P) (compEs2 (map Val vs') @ [Push v]) (compxEs2 (map Val vs') 0 0 @ shift (length (compEs2 (map Val vs'))) []) t h (rev vs', xs, length (compEs2 (map Val vs')) + 0, None) \<lbrace>\<rbrace> h (v # rev vs', xs, length (compEs2 (map Val vs')) + Suc 0, None)
\<tau>moves2 (compP2 P) h (rev vs') (map Val vs' @ [Val v]) (length (compEs2 (map Val vs')) + 0) None
[PROOF STEP]
have "\<tau>Exec_movesr_a P t (map Val (vs' @ [v])) h ((rev vs'), xs, (length ?E), None) ((rev (vs' @ [v])), xs, (length (compEs2 (map Val (vs' @ [v])))), None)"
[PROOF STATE]
proof (prove)
using this:
exec_meth_a (compP2 P) (compEs2 (map Val vs') @ [Push v]) (compxEs2 (map Val vs') 0 0 @ shift (length (compEs2 (map Val vs'))) []) t h (rev vs', xs, length (compEs2 (map Val vs')) + 0, None) \<lbrace>\<rbrace> h (v # rev vs', xs, length (compEs2 (map Val vs')) + Suc 0, None)
\<tau>moves2 (compP2 P) h (rev vs') (map Val vs' @ [Val v]) (length (compEs2 (map Val vs')) + 0) None

goal (1 subgoal):
 1. \<tau>Exec_movesr_a P t (map Val (vs' @ [v])) h (rev vs', xs, length (compEs2 (map Val vs')), None) (rev (vs' @ [v]), xs, length (compEs2 (map Val (vs' @ [v]))), None)
[PROOF STEP]
by -(rule \<tau>Execsr1step, auto simp add: exec_moves_def compP2_def)
[PROOF STATE]
proof (state)
this:
\<tau>Exec_movesr_a P t (map Val (vs' @ [v])) h (rev vs', xs, length (compEs2 (map Val vs')), None) (rev (vs' @ [v]), xs, length (compEs2 (map Val (vs' @ [v]))), None)

goal (1 subgoal):
 1. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<tau>Exec_movesr_a P t (map Val (vs' @ [v])) h (rev vs', xs, length (compEs2 (map Val vs')), None) (rev (vs' @ [v]), xs, length (compEs2 (map Val (vs' @ [v]))), None)

goal (1 subgoal):
 1. \<And>x xsa. \<tau>Exec_movesr_a P t (map Val xsa) h ([], xs, 0, None) (rev xsa, xs, length (compEs2 (map Val xsa)), None) \<Longrightarrow> \<tau>Exec_movesr_a P t (map Val (xsa @ [x])) h ([], xs, 0, None) (rev (xsa @ [x]), xs, length (compEs2 (map Val (xsa @ [x]))), None)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<tau>Exec_movesr_a P t (map Val (vs' @ [v])) h ([], xs, 0, None) (rev (vs' @ [v]), xs, length (compEs2 (map Val (vs' @ [v]))), None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<tau>Exec_movesr_a P t (map Val (vs' @ [v])) h ([], xs, 0, None) (rev (vs' @ [v]), xs, length (compEs2 (map Val (vs' @ [v]))), None)

goal (1 subgoal):
 1. \<tau>Exec_movesr_a P t (map Val (vs' @ [v])) h ([], xs, 0, None) (rev (vs' @ [v]), xs, length (compEs2 (map Val (vs' @ [v]))), None)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<tau>Exec_movesr_a P t (map Val (vs' @ [v])) h ([], xs, 0, None) (rev (vs' @ [v]), xs, length (compEs2 (map Val (vs' @ [v]))), None)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<tau>Exec_mover_blocks1 [simp]:
  "\<tau>Exec_mover ci P t (blocks1 n Ts body) h s s' = \<tau>Exec_mover ci P t body h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t (blocks1 n Ts body) h s s' = \<tau>Exec_mover ci P t body h s s'
[PROOF STEP]
by(simp add: \<tau>exec_move_conv_\<tau>exec_meth)


[STATEMENT]
lemma \<tau>Exec_movet_blocks1 [simp]:
  "\<tau>Exec_movet ci P t (blocks1 n Ts body) h s s' = \<tau>Exec_movet ci P t body h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t (blocks1 n Ts body) h s s' = \<tau>Exec_movet ci P t body h s s'
[PROOF STEP]
by(simp add: \<tau>exec_move_conv_\<tau>exec_meth)


[STATEMENT]
lemma \<tau>exec_1I [intro]:
  "\<lbrakk> exec_1 P t \<sigma> \<epsilon> \<sigma>'; \<tau>Move2 P \<sigma> \<rbrakk> \<Longrightarrow> \<tau>exec_1 P t \<sigma> \<sigma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,t \<turnstile> \<sigma> -\<lbrace>\<rbrace>-jvm\<rightarrow> \<sigma>'; \<tau>Move2 P \<sigma>\<rbrakk> \<Longrightarrow> \<tau>exec_1 P t \<sigma> \<sigma>'
[PROOF STEP]
by(simp add: \<tau>exec_1_def)


[STATEMENT]
lemma \<tau>exec_1E [elim]:
  assumes "\<tau>exec_1 P t \<sigma> \<sigma>'"
  obtains "exec_1 P t \<sigma> \<epsilon> \<sigma>'" "\<tau>Move2 P \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>P,t \<turnstile> \<sigma> -\<lbrace>\<rbrace>-jvm\<rightarrow> \<sigma>'; \<tau>Move2 P \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<tau>exec_1 P t \<sigma> \<sigma>'

goal (1 subgoal):
 1. (\<lbrakk>P,t \<turnstile> \<sigma> -\<lbrace>\<rbrace>-jvm\<rightarrow> \<sigma>'; \<tau>Move2 P \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: \<tau>exec_1_def)


[STATEMENT]
lemma \<tau>exec_1_dI [intro]:
  "\<lbrakk> exec_1 P t \<sigma> \<epsilon> \<sigma>'; check P \<sigma>; \<tau>Move2 P \<sigma> \<rbrakk> \<Longrightarrow> \<tau>exec_1_d P t \<sigma> \<sigma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,t \<turnstile> \<sigma> -\<lbrace>\<rbrace>-jvm\<rightarrow> \<sigma>'; check P \<sigma>; \<tau>Move2 P \<sigma>\<rbrakk> \<Longrightarrow> \<tau>exec_1_d P t \<sigma> \<sigma>'
[PROOF STEP]
by(simp add: \<tau>exec_1_d_def)


[STATEMENT]
lemma \<tau>exec_1_dE [elim]:
  assumes "\<tau>exec_1_d P t \<sigma> \<sigma>'"
  obtains "exec_1 P t \<sigma> \<epsilon> \<sigma>'" "check P \<sigma>" "\<tau>Move2 P \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>P,t \<turnstile> \<sigma> -\<lbrace>\<rbrace>-jvm\<rightarrow> \<sigma>'; check P \<sigma>; \<tau>Move2 P \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<tau>exec_1_d P t \<sigma> \<sigma>'

goal (1 subgoal):
 1. (\<lbrakk>P,t \<turnstile> \<sigma> -\<lbrace>\<rbrace>-jvm\<rightarrow> \<sigma>'; check P \<sigma>; \<tau>Move2 P \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: \<tau>exec_1_d_def)


[STATEMENT]
lemma exec_instr_frs_offer:
  "(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs
  \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<in> exec_instr ins P t h stk loc C M pc (frs @ frs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<in> exec_instr ins P t h stk loc C M pc (frs @ frs')
[PROOF STEP]
apply(cases ins)
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<in> exec_instr ins P t h stk loc C M pc (frs @ frs')
 2. \<And>x2. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<in> exec_instr ins P t h stk loc C M pc (frs @ frs')
 3. \<And>x3. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<in> exec_instr ins P t h stk loc C M pc (frs @ frs')
 4. \<And>x4. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<in> exec_instr ins P t h stk loc C M pc (frs @ frs')
 5. \<And>x5. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<in> exec_instr ins P t h stk loc C M pc (frs @ frs')
 6. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<in> exec_instr ins P t h stk loc C M pc (frs @ frs')
 7. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<in> exec_instr ins P t h stk loc C M pc (frs @ frs')
 8. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<in> exec_instr ins P t h stk loc C M pc (frs @ frs')
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<in> exec_instr ins P t h stk loc C M pc (frs @ frs')
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<in> exec_instr ins P t h stk loc C M pc (frs @ frs')
A total of 24 subgoals...
[PROOF STEP]
apply(simp_all add: nth_append split_beta split: if_split_asm sum.split_asm)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x4. \<lbrakk>ins = New x4; allocate h (Class_type x4) \<noteq> {}; (ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> (\<lambda>x. (\<lbrace>NewHeapElem (snd x) (Class_type x4)\<rbrace>, None, fst x, (Addr (snd x) # stk, loc, C, M, Suc pc) # frs)) ` allocate h (Class_type x4)\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<in> (\<lambda>x. (\<lbrace>NewHeapElem (snd x) (Class_type x4)\<rbrace>, None, fst x, (Addr (snd x) # stk, loc, C, M, Suc pc) # frs @ frs')) ` allocate h (Class_type x4)
 2. \<And>x5. \<lbrakk>ins = NewArray x5; \<not> the_Intg (hd stk) <s 0; allocate h (Array_type x5 (nat (sint (the_Intg (hd stk))))) \<noteq> {}; (ta, xcp', h', (stk', loc', C, M, pc') # frs) \<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, C, M, Suc pc) # frs)) ` allocate h (Array_type x5 (nat (sint (the_Intg (hd stk)))))\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') \<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, C, M, Suc pc) # frs @ frs')) ` allocate h (Array_type x5 (nat (sint (the_Intg (hd stk)))))
 3. \<lbrakk>ins = AStore; hd (tl (tl stk)) \<noteq> Null; the_Intg (hd (tl stk)) <s 0 \<or> int (alen_of_htype (the (typeof_addr h (the_Addr (hd (tl (tl stk))))))) \<le> sint (the_Intg (hd (tl stk))); ta = \<lbrace>\<rbrace> \<and> xcp' = \<lfloor>addr_of_sys_xcpt ArrayIndexOutOfBounds\<rfloor> \<and> h' = h \<and> stk' = stk \<and> loc' = loc \<and> pc' = pc\<rbrakk> \<Longrightarrow> \<not> P \<turnstile> the (typeof\<^bsub>h\<^esub> (hd stk)) \<le> the_Array (ty_of_htype (the (typeof_addr h (the_Addr (hd (tl (tl stk))))))) \<longrightarrow> \<not> the_Intg (hd (tl stk)) <s 0 \<and> \<not> int (alen_of_htype (the (typeof_addr h (the_Addr (hd (tl (tl stk))))))) \<le> sint (the_Intg (hd (tl stk))) \<longrightarrow> addr_of_sys_xcpt ArrayIndexOutOfBounds = addr_of_sys_xcpt ArrayStore
 4. \<And>x141 x142. \<lbrakk>ins = Invoke x141 x142; stk ! x142 \<noteq> Null; snd (snd (snd (method P (class_type_of (the (typeof_addr h (the_Addr (stk ! x142))))) x141))) = None; \<exists>a aa ab ac ad b. ta = (a, map (convert_new_thread_action (extNTA2JVM P)) aa, ab, ac, ad, b) \<and> (\<exists>va. (case va of RetVal v \<Rightarrow> xcp' = None \<and> (stk', loc', C, M, pc') # frs = (v # drop (Suc x142) stk, loc, C, M, pc + 1) # frs | RetExc a \<Rightarrow> xcp' = \<lfloor>a\<rfloor> \<and> (stk', loc', C, M, pc') # frs = (stk, loc, C, M, pc) # frs | RetStaySame \<Rightarrow> xcp' = None \<and> (stk', loc', C, M, pc') # frs = (stk, loc, C, M, pc) # frs) \<and> ((a, aa, ab, ac, ad, b), va, h') \<in> red_external_aggr P t (the_Addr (stk ! x142)) x141 (rev (take x142 stk)) h)\<rbrakk> \<Longrightarrow> \<exists>a aa ab ac ad b. ta = (a, map (convert_new_thread_action (extNTA2JVM P)) aa, ab, ac, ad, b) \<and> (\<exists>va. (case va of RetVal v \<Rightarrow> xcp' = None \<and> (stk', loc', C, M, pc') # frs @ frs' = (v # drop (Suc x142) stk, loc, C, M, pc + 1) # frs @ frs' | RetExc a \<Rightarrow> xcp' = \<lfloor>a\<rfloor> \<and> (stk', loc', C, M, pc') # frs @ frs' = (stk, loc, C, M, pc) # frs @ frs' | RetStaySame \<Rightarrow> xcp' = None \<and> (stk', loc', C, M, pc') # frs @ frs' = (stk, loc, C, M, pc) # frs @ frs') \<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)
[PROOF STEP]
apply(force split: extCallRet.split_asm simp add: extRet2JVM_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma check_instr_frs_offer:
  "\<lbrakk> check_instr ins P h stk loc C M pc frs; ins \<noteq> Return \<rbrakk>
  \<Longrightarrow> check_instr ins P h stk loc C M pc (frs @ frs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>check_instr ins P h stk loc C M pc frs; ins \<noteq> Return\<rbrakk> \<Longrightarrow> check_instr ins P h stk loc C M pc (frs @ frs')
[PROOF STEP]
by(cases ins)(simp_all split: if_split_asm)


[STATEMENT]
lemma exec_instr_CM_change:
  "(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs
  \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<in> exec_instr ins P t h stk loc C' M' pc frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<in> exec_instr ins P t h stk loc C' M' pc frs
[PROOF STEP]
apply(cases ins)
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>x1. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = Load x1\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<in> exec_instr ins P t h stk loc C' M' pc frs
 2. \<And>x2. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = Store x2\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<in> exec_instr ins P t h stk loc C' M' pc frs
 3. \<And>x3. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = Push x3\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<in> exec_instr ins P t h stk loc C' M' pc frs
 4. \<And>x4. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = New x4\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<in> exec_instr ins P t h stk loc C' M' pc frs
 5. \<And>x5. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = NewArray x5\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<in> exec_instr ins P t h stk loc C' M' pc frs
 6. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = ALoad\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<in> exec_instr ins P t h stk loc C' M' pc frs
 7. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = AStore\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<in> exec_instr ins P t h stk loc C' M' pc frs
 8. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = ALength\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<in> exec_instr ins P t h stk loc C' M' pc frs
 9. \<And>x91 x92. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<in> exec_instr ins P t h stk loc C' M' pc frs
 10. \<And>x101 x102. \<lbrakk>(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr ins P t h stk loc C M pc frs; ins = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<in> exec_instr ins P t h stk loc C' M' pc frs
A total of 24 subgoals...
[PROOF STEP]
apply(simp_all add: nth_append split_beta neq_Nil_conv split: if_split_asm sum.split_asm)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x4. \<lbrakk>ins = New x4; allocate h (Class_type x4) \<noteq> {}; (ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> (\<lambda>x. (\<lbrace>NewHeapElem (snd x) (Class_type x4)\<rbrace>, None, fst x, (Addr (snd x) # stk, loc, C, M, Suc pc) # frs)) ` allocate h (Class_type x4)\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<in> (\<lambda>x. (\<lbrace>NewHeapElem (snd x) (Class_type x4)\<rbrace>, None, fst x, (Addr (snd x) # stk, loc, C', M', Suc pc) # frs)) ` allocate h (Class_type x4)
 2. \<And>x5. \<lbrakk>ins = NewArray x5; \<not> the_Intg (hd stk) <s 0; allocate h (Array_type x5 (nat (sint (the_Intg (hd stk))))) \<noteq> {}; (ta, xcp', h', (stk', loc', C, M, pc') # frs) \<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, C, M, Suc pc) # frs)) ` allocate h (Array_type x5 (nat (sint (the_Intg (hd stk)))))\<rbrakk> \<Longrightarrow> (ta, xcp', h', (stk', loc', C', M', pc') # frs) \<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, C', M', Suc pc) # frs)) ` allocate h (Array_type x5 (nat (sint (the_Intg (hd stk)))))
 3. \<lbrakk>ins = AStore; hd (tl (tl stk)) \<noteq> Null; the_Intg (hd (tl stk)) <s 0 \<or> int (alen_of_htype (the (typeof_addr h (the_Addr (hd (tl (tl stk))))))) \<le> sint (the_Intg (hd (tl stk))); ta = \<lbrace>\<rbrace> \<and> xcp' = \<lfloor>addr_of_sys_xcpt ArrayIndexOutOfBounds\<rfloor> \<and> h' = h \<and> stk' = stk \<and> loc' = loc \<and> pc' = pc\<rbrakk> \<Longrightarrow> \<not> P \<turnstile> the (typeof\<^bsub>h\<^esub> (hd stk)) \<le> the_Array (ty_of_htype (the (typeof_addr h (the_Addr (hd (tl (tl stk))))))) \<longrightarrow> \<not> the_Intg (hd (tl stk)) <s 0 \<and> \<not> int (alen_of_htype (the (typeof_addr h (the_Addr (hd (tl (tl stk))))))) \<le> sint (the_Intg (hd (tl stk))) \<longrightarrow> addr_of_sys_xcpt ArrayIndexOutOfBounds = addr_of_sys_xcpt ArrayStore
 4. \<And>x141 x142. \<lbrakk>ins = Invoke x141 x142; stk ! x142 \<noteq> Null; snd (snd (snd (method P (class_type_of (the (typeof_addr h (the_Addr (stk ! x142))))) x141))) = None; \<exists>a aa ab ac ad b. ta = (a, map (convert_new_thread_action (extNTA2JVM P)) aa, ab, ac, ad, b) \<and> (\<exists>va. (case va of RetVal v \<Rightarrow> xcp' = None \<and> (stk', loc', C, M, pc') # frs = (v # drop (Suc x142) stk, loc, C, M, pc + 1) # frs | RetExc a \<Rightarrow> xcp' = \<lfloor>a\<rfloor> \<and> (stk', loc', C, M, pc') # frs = (stk, loc, C, M, pc) # frs | RetStaySame \<Rightarrow> xcp' = None \<and> (stk', loc', C, M, pc') # frs = (stk, loc, C, M, pc) # frs) \<and> ((a, aa, ab, ac, ad, b), va, h') \<in> red_external_aggr P t (the_Addr (stk ! x142)) x141 (rev (take x142 stk)) h)\<rbrakk> \<Longrightarrow> \<exists>a aa ab ac ad b. ta = (a, map (convert_new_thread_action (extNTA2JVM P)) aa, ab, ac, ad, b) \<and> (\<exists>va. (case va of RetVal v \<Rightarrow> xcp' = None \<and> (stk', loc', C', M', pc') # frs = (v # drop (Suc x142) stk, loc, C', M', pc + 1) # frs | RetExc a \<Rightarrow> xcp' = \<lfloor>a\<rfloor> \<and> (stk', loc', C', M', pc') # frs = (stk, loc, C', M', pc) # frs | RetStaySame \<Rightarrow> xcp' = None \<and> (stk', loc', C', M', pc') # frs = (stk, loc, C', M', pc) # frs) \<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)
 5. \<lbrakk>ins = Return; \<exists>a aa ab ac b ys. frs = (a, aa, ab, ac, b) # ys; ta = \<lbrace>\<rbrace> \<and> xcp' = None \<and> h' = h \<and> stk' = hd stk # drop (Suc (length (fst (snd (method P C M))))) (fst (hd frs)) \<and> loc' = fst (snd (hd frs)) \<and> C = fst (snd (snd (hd frs))) \<and> M = fst (snd (snd (snd (hd frs)))) \<and> pc' = Suc (snd (snd (snd (snd (hd frs))))) \<and> frs = tl frs\<rbrakk> \<Longrightarrow> drop (Suc (length (fst (snd (method P (fst (snd (snd (hd frs)))) (fst (snd (snd (snd (hd frs)))))))))) (fst (hd frs)) = drop (Suc (length (fst (snd (method P C' M'))))) (fst (hd frs)) \<and> C' = fst (snd (snd (hd frs))) \<and> M' = fst (snd (snd (snd (hd frs))))
[PROOF STEP]
apply(force split: extCallRet.split_asm simp add: extRet2JVM_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma check_instr_CM_change:
  "\<lbrakk> check_instr ins P h stk loc C M pc frs; ins \<noteq> Return \<rbrakk>
  \<Longrightarrow> check_instr ins P h stk loc C' M' pc frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>check_instr ins P h stk loc C M pc frs; ins \<noteq> Return\<rbrakk> \<Longrightarrow> check_instr ins P h stk loc C' M' pc frs
[PROOF STEP]
by(cases ins)(simp_all split: if_split_asm)