Theory Execs

(*  Title:      JinjaThreads/Compiler/Execs.thy
    Author:     Andreas Lochbihler
*)

section ‹JVM Semantics for the delay bisimulation proof from intermediate language to byte code›

theory Execs imports JVMTau begin

declare match_ex_table_app [simp del]
  match_ex_table_eq_NoneI [simp del]
  compxE2_size_convs [simp del]
  compxE2_stack_xlift_convs [simp del]
  compxEs2_stack_xlift_convs [simp del]

type_synonym
  ('addr, 'heap) check_instr' = 
  "'addr instr ⇒ 'addr jvm_prog ⇒ 'heap ⇒ 'addr val list ⇒ 'addr val list ⇒ cname ⇒ mname ⇒ pc ⇒ 'addr frame list ⇒ bool"

primrec check_instr' :: "('addr, 'heap) check_instr'"
where 
check_instr'_Load:
  "check_instr' (Load n) P h stk loc C M⇩0 pc frs =
  True"

| check_instr'_Store:
  "check_instr' (Store n) P h stk loc C⇩0 M⇩0 pc frs =
  (0 < length stk)"

| check_instr'_Push:
  "check_instr' (Push v) P h stk loc C⇩0 M⇩0 pc frs =
  True"

| check_instr'_New:
  "check_instr' (New C) P h stk loc C⇩0 M⇩0 pc frs = 
  True"

| check_instr'_NewArray:
  "check_instr' (NewArray T) P h stk loc C0 M0 pc frs =
  (0 < length stk)"

| check_instr'_ALoad:
  "check_instr' ALoad P h stk loc C0 M0 pc frs =
  (1 < length stk)"

| check_instr'_AStore:
  "check_instr' AStore P h stk loc C0 M0 pc frs =
  (2 < length stk)"

| check_instr'_ALength:
  "check_instr' ALength P h stk loc C0 M0 pc frs =
  (0 < length stk)"

| check_instr'_Getfield:
  "check_instr' (Getfield F C) P h stk loc C⇩0 M⇩0 pc frs = 
  (0 < length stk)"

| check_instr'_Putfield:
  "check_instr' (Putfield F C) P h stk loc C⇩0 M⇩0 pc frs = 
  (1 < length stk)"

| check_instr'_CAS:
  "check_instr' (CAS F C) P h stk loc C⇩0 M⇩0 pc frs  =
  (2 < length stk)"

| check_instr'_Checkcast:
  "check_instr' (Checkcast T) P h stk loc C⇩0 M⇩0 pc frs =
  (0 < length stk)"

| check_instr'_Instanceof:
  "check_instr' (Instanceof T) P h stk loc C⇩0 M⇩0 pc frs =
  (0 < length stk)"

| check_instr'_Invoke:
  "check_instr' (Invoke M n) P h stk loc C⇩0 M⇩0 pc frs =
  (n < length stk)"

| check_instr'_Return:
  "check_instr' Return P h stk loc C⇩0 M⇩0 pc frs =
  (0 < length stk)"
 
| check_instr'_Pop:
  "check_instr' Pop P h stk loc C⇩0 M⇩0 pc frs = 
  (0 < length stk)"

| check_instr'_Dup:
  "check_instr' Dup P h stk loc C⇩0 M⇩0 pc frs = 
  (0 < length stk)"

| check_instr'_Swap:
  "check_instr' Swap P h stk loc C⇩0 M⇩0 pc frs = 
  (1 < length stk)"

| check_instr'_BinOpInstr:
  "check_instr' (BinOpInstr bop) P h stk loc C⇩0 M⇩0 pc frs =
  (1 < length stk)"

| check_instr'_IfFalse:
  "check_instr' (IfFalse b) P h stk loc C⇩0 M⇩0 pc frs =
  (0 < length stk ∧ 0 ≤ int pc+b)"

| check_instr'_Goto:
  "check_instr' (Goto b) P h stk loc C⇩0 M⇩0 pc frs =
  (0 ≤ int pc+b)"

| check_instr'_Throw:
  "check_instr' ThrowExc P h stk loc C⇩0 M⇩0 pc frs =
  (0 < length stk)"

| check_instr'_MEnter:
  "check_instr' MEnter P h stk loc C⇩0 M⇩0 pc frs =
   (0 < length stk)"

| check_instr'_MExit:
  "check_instr' MExit P h stk loc C⇩0 M⇩0 pc frs =
   (0 < length stk)"

definition ci_stk_offer :: "('addr, 'heap) check_instr' ⇒ bool"
where
  "ci_stk_offer ci =
  (∀ins P h stk stk' loc C M pc frs. ci ins P h stk loc C M pc frs ⟶ ci ins P h (stk @ stk') loc C M pc frs)"

lemma ci_stk_offerI:
  "(⋀ins P h stk stk' loc C M pc frs. ci ins P h stk loc C M pc frs ⟹ ci ins P h (stk @ stk') loc C M pc frs) ⟹ ci_stk_offer ci"
unfolding ci_stk_offer_def by blast

lemma ci_stk_offerD:
  "⟦ ci_stk_offer ci; ci ins P h stk loc C M pc frs ⟧ ⟹ ci ins P h (stk @ stk') loc C M pc frs"
unfolding ci_stk_offer_def by blast


lemma check_instr'_stk_offer:
  "ci_stk_offer check_instr'"
proof(rule ci_stk_offerI)
  fix ins P h stk stk' loc C M pc frs
  assume "check_instr' ins P h stk loc C M pc frs"
  thus "check_instr' ins P h (stk @ stk') loc C M pc frs"
    by(cases ins) auto
qed

context JVM_heap_base begin

lemma check_instr_imp_check_instr':
  "check_instr ins P h stk loc C M pc frs ⟹ check_instr' ins P h stk loc C M pc frs"
by(cases ins) auto

lemma check_instr_stk_offer:
  "ci_stk_offer check_instr"
proof(rule ci_stk_offerI)
  fix ins P h stk stk' loc C M pc frs
  assume "check_instr ins P h stk loc C M pc frs"
  thus "check_instr ins P h (stk @ stk') loc C M pc frs"
    by(cases ins)(auto simp add: nth_append hd_append neq_Nil_conv tl_append split: list.split)
qed

end

(* TODO: Combine ins_jump_ok and jump_ok *)
primrec jump_ok :: "'addr instr list ⇒ nat ⇒ nat ⇒ bool"
where "jump_ok [] n n' = True"
| "jump_ok (x # xs) n n' = (jump_ok xs (Suc n) n' ∧ 
                           (case x of IfFalse m ⇒ - int n ≤ m ∧ m ≤ int (n' + length xs)
                                       | Goto m ⇒ - int n ≤ m ∧ m ≤ int (n' + length xs)
                                            | _ ⇒ True))"

lemma jump_ok_append [simp]:
  "jump_ok (xs @ xs') n n' ⟷ jump_ok xs n (n' + length xs') ∧ jump_ok xs' (n + length xs) n'"
apply(induct xs arbitrary: n)
 apply(simp)
apply(auto split: instr.split)
done

lemma jump_ok_GotoD:
  "⟦ jump_ok ins n n'; ins ! pc = Goto m; pc < length ins ⟧ ⟹ - int (pc + n) ≤ m ∧ m < int (length ins - pc + n')"
apply(induct ins arbitrary: n n' pc)
 apply(simp)
apply(clarsimp)
apply(case_tac pc)
apply(fastforce)+
done

lemma jump_ok_IfFalseD:
  "⟦ jump_ok ins n n'; ins ! pc = IfFalse m; pc < length ins ⟧ ⟹ - int (pc + n) ≤ m ∧ m < int (length ins - pc + n')"
apply(induct ins arbitrary: n n' pc)
 apply(simp)
apply(clarsimp)
apply(case_tac pc)
apply(fastforce)+
done

lemma fixes e :: "'addr expr1" and es :: "'addr expr1 list"
  shows compE2_jump_ok [intro!]: "jump_ok (compE2 e) n (Suc n')"
  and compEs2_jump_ok [intro!]: "jump_ok (compEs2 es) n (Suc n')"
apply(induct e and es arbitrary: n n' and n n' rule: compE2.induct compEs2.induct)
apply(auto split: bop.split)
done

lemma fixes e :: "'addr expr1" and es :: "'addr expr1 list"
  shows compE1_Goto_not_same: "⟦ compE2 e ! pc = Goto i; pc < length (compE2 e) ⟧ ⟹ nat (int pc + i) ≠ pc"
  and compEs2_Goto_not_same: "⟦ compEs2 es ! pc = Goto i; pc < length (compEs2 es) ⟧ ⟹ nat (int pc + i) ≠ pc"
apply(induct e and es arbitrary: pc i and pc i rule: compE2.induct compEs2.induct)
apply(auto simp add: nth_Cons nth_append split: if_split_asm bop.split_asm nat.splits)
apply fastforce+
done

fun ins_jump_ok :: "'addr instr ⇒ nat ⇒ bool"
where
  "ins_jump_ok (Goto m) l = (- (int l) ≤ m)"
| "ins_jump_ok (IfFalse m) l = (- (int l) ≤ m)"
| "ins_jump_ok _ _ = True"

definition wf_ci :: "('addr, 'heap) check_instr' ⇒ bool"
where
  "wf_ci ci ⟷
   ci_stk_offer ci ∧ ci ≤ check_instr' ∧
   (∀ins P h stk loc C M pc pc' frs. ci ins P h stk loc C M pc frs ⟶ ins_jump_ok ins pc' ⟶ ci ins P h stk loc C M pc' frs)"

lemma wf_ciI:
  "⟦ ci_stk_offer ci;
    ⋀ins P h stk loc C M pc frs. ci ins P h stk loc C M pc frs ⟹ check_instr' ins P h stk loc C M pc frs;
    ⋀ins P h stk loc C M pc pc' frs. ⟦ ci ins P h stk loc C M pc frs; ins_jump_ok ins pc' ⟧ ⟹ ci ins P h stk loc C M pc' frs ⟧
  ⟹ wf_ci ci"
unfolding wf_ci_def le_fun_def le_bool_def
by blast

lemma check_instr'_pc:
  "⟦ check_instr' ins P h stk loc C M pc frs; ins_jump_ok ins pc' ⟧ ⟹ check_instr' ins P h stk loc C M pc' frs"
by(cases ins) auto

lemma wf_ci_check_instr' [iff]:
  "wf_ci check_instr'"
apply(rule wf_ciI)
  apply(rule check_instr'_stk_offer)
 apply(assumption)
apply(erule (1) check_instr'_pc)
done

lemma jump_ok_ins_jump_ok:
  "⟦ jump_ok ins n n'; pc < length ins ⟧ ⟹ ins_jump_ok (ins ! pc) (pc + n)"
apply(induct ins arbitrary: n n' pc)
apply(fastforce simp add: nth_Cons' gr0_conv_Suc split: instr.split_asm)+
done

context JVM_heap_base begin

lemma check_instr_pc:
  "⟦ check_instr ins P h stk loc C M pc frs; ins_jump_ok ins pc' ⟧ ⟹ check_instr ins P h stk loc C M pc' frs"
by(cases ins) auto

lemma wf_ci_check_instr [iff]:
  "wf_ci check_instr"
apply(rule wf_ciI)
  apply(rule check_instr_stk_offer)
 apply(erule check_instr_imp_check_instr')
apply(erule (1) check_instr_pc)
done

end

lemma wf_ciD1: "wf_ci ci ⟹ ci_stk_offer ci"
unfolding wf_ci_def by blast

lemma wf_ciD2: "⟦ wf_ci ci; ci ins P h stk loc C M pc frs ⟧ ⟹ check_instr' ins P h stk loc C M pc frs"
unfolding wf_ci_def le_fun_def le_bool_def
by blast

lemma wf_ciD3: "⟦ wf_ci ci; ci ins P h stk loc C M pc frs; ins_jump_ok ins pc' ⟧ ⟹ ci ins P h stk loc C M pc' frs"
unfolding wf_ci_def by blast

lemma check_instr'_ins_jump_ok: "check_instr' ins P h stk loc C M pc frs ⟹ ins_jump_ok ins pc"
by(cases ins) auto
lemma wf_ci_ins_jump_ok:
  assumes wf: "wf_ci ci"
  and ci: "ci ins P h stk loc C M pc frs"
  and pc': "pc ≤ pc'"
  shows "ins_jump_ok ins pc'"
proof -
  from wf ci have "check_instr' ins P h stk loc C M pc frs" by(rule wf_ciD2)
  with pc' have "check_instr' ins P h stk loc C M pc' frs" by(cases ins) auto
  thus ?thesis by(rule check_instr'_ins_jump_ok)
qed

lemma wf_ciD3': "⟦ wf_ci ci; ci ins P h stk loc C M pc frs; pc ≤ pc' ⟧ ⟹ ci ins P h stk loc C M pc' frs"
apply(frule (2) wf_ci_ins_jump_ok)
apply(erule (2) wf_ciD3)
done

typedef ('addr, 'heap) check_instr = "Collect wf_ci :: ('addr, 'heap) check_instr' set"
  morphisms ci_app Abs_check_instr
by auto

lemma ci_app_check_instr' [simp]: "ci_app (Abs_check_instr check_instr') = check_instr'"
by(simp add: Abs_check_instr_inverse)

lemma (in JVM_heap_base) ci_app_check_instr [simp]: "ci_app (Abs_check_instr check_instr) = check_instr"
by(simp add: Abs_check_instr_inverse)

lemma wf_ci_stk_offerD:
  "ci_app ci ins P h stk loc C M pc frs ⟹ ci_app ci ins P h (stk @ stk') loc C M pc frs"
apply(rule ci_stk_offerD[OF wf_ciD1]) back
by(rule ci_app [simplified])

lemma wf_ciD2_ci_app:
  "ci_app ci ins P h stk loc C M pc frs ⟹ check_instr' ins P h stk loc C M pc frs"
apply(cases ci)
apply(simp add: Abs_check_instr_inverse)
apply(erule (1) wf_ciD2)
done

lemma wf_ciD3_ci_app:
  "⟦ ci_app ci ins P h stk loc C M pc frs; ins_jump_ok ins pc' ⟧ ⟹ ci_app ci ins P h stk loc C M pc' frs"
apply(cases ci)
apply(simp add: Abs_check_instr_inverse)
apply(erule (2) wf_ciD3)
done

lemma wf_ciD3'_ci_app: "⟦ ci_app ci ins P h stk loc C M pc frs; pc ≤ pc' ⟧ ⟹ ci_app ci ins P h stk loc C M pc' frs"
apply(cases ci)
apply(simp add: Abs_check_instr_inverse)
apply(erule (2) wf_ciD3')
done

context JVM_heap_base begin

inductive exec_meth ::
  "('addr, 'heap) check_instr ⇒ 'addr jvm_prog ⇒ 'addr instr list ⇒ ex_table ⇒ 'thread_id
  ⇒ 'heap ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ ('addr, 'thread_id, 'heap) jvm_thread_action
  ⇒ 'heap ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"
for ci :: "('addr, 'heap) check_instr" and P :: "'addr jvm_prog" 
and ins :: "'addr instr list" and xt :: "ex_table" and t :: 'thread_id
where
  exec_instr: 
  "⟦ (ta, xcp, h', [(stk', loc', undefined, undefined, pc')]) ∈ exec_instr (ins ! pc) P t h stk loc undefined undefined pc [];
     pc < length ins;
     ci_app ci (ins ! pc) P h stk loc undefined undefined pc [] ⟧
  ⟹ exec_meth ci P ins xt t h (stk, loc, pc, None) ta h' (stk', loc', pc', xcp)"

| exec_catch:
  "⟦ match_ex_table P (cname_of h xcp) pc xt = ⌊(pc', d)⌋; d ≤ length stk ⟧
  ⟹ exec_meth ci P ins xt t h (stk, loc, pc, ⌊xcp⌋) ε h (Addr xcp # drop (size stk - d) stk, loc, pc', None)"

lemma exec_meth_instr:
  "exec_meth ci P ins xt t h (stk, loc, pc, None) ta h' (stk', loc', pc', xcp) ⟷
   (ta, xcp, h', [(stk', loc', undefined, undefined, pc')]) ∈ exec_instr (ins ! pc) P t h stk loc undefined undefined pc [] ∧ pc < length ins ∧ ci_app ci (ins ! pc) P h stk loc undefined undefined pc []"
by(auto elim: exec_meth.cases intro: exec_instr)

lemma exec_meth_xcpt:
  "exec_meth ci P ins xt t h (stk, loc, pc, ⌊xcp⌋) ta h (stk', loc', pc', xcp') ⟷
   (∃d. match_ex_table P (cname_of h xcp) pc xt = ⌊(pc', d)⌋ ∧ ta = ε ∧ stk' = (Addr xcp # drop (size stk - d) stk) ∧ loc' = loc ∧ xcp' = None ∧ d ≤ length stk)"
by(auto elim: exec_meth.cases intro: exec_catch)

abbreviation exec_meth_a
where "exec_meth_a ≡ exec_meth (Abs_check_instr check_instr')"

abbreviation exec_meth_d
where "exec_meth_d ≡ exec_meth (Abs_check_instr check_instr)"

lemma exec_meth_length_compE2D [dest]:
  "exec_meth ci P (compE2 e) (compxE2 e 0 d) t h (stk, loc, pc, xcp) ta h' s' ⟹ pc < length (compE2 e)"
apply(erule exec_meth.cases)
apply(auto dest: match_ex_table_pc_length_compE2)
done

lemma exec_meth_length_compEs2D [dest]:
  "exec_meth ci P (compEs2 es) (compxEs2 es 0 0) t h (stk, loc, pc, xcp) ta h' s' ⟹ pc < length (compEs2 es)"
apply(erule exec_meth.cases)
apply(auto dest: match_ex_table_pc_length_compEs2)
done

lemma exec_instr_stk_offer:
  assumes check: "check_instr' (ins ! pc) P h stk loc C M pc frs"
  and exec: "(ta', xcp', h', (stk', loc', C, M, pc') # frs) ∈ exec_instr (ins ! pc) P t h stk loc C M pc frs"
  shows "(ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) ∈ exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs"
using assms
proof(cases "ins ! pc")
  case (Invoke M n)
  thus ?thesis using exec check
    by(auto split: if_split_asm extCallRet.splits split del: if_split simp add: split_beta nth_append min_def extRet2JVM_def)
qed(force simp add: nth_append is_Ref_def has_method_def nth_Cons split_beta hd_append tl_append neq_Nil_conv split: list.split if_split_asm nat.splits sum.split_asm)+

lemma exec_meth_stk_offer:
  assumes exec: "exec_meth ci P ins xt t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')"
using exec
proof(cases)
  case (exec_catch xcp d)
  from ‹match_ex_table P (cname_of h xcp) pc xt = ⌊(pc', d)⌋›
  have "match_ex_table P (cname_of h xcp) pc (stack_xlift (length stk'') xt) = ⌊(pc', length stk'' + d)⌋"
    by(simp add: match_ex_table_stack_xlift)
  moreover have "length stk'' + d ≤ length (stk @ stk'')" using ‹d ≤ length stk› by simp
  ultimately have "exec_meth ci P ins (stack_xlift (length stk'') xt) t h ((stk @ stk''), loc, pc, ⌊xcp⌋) ε h ((Addr xcp # drop (length (stk @ stk'') - (length stk'' + d)) (stk @ stk'')), loc, pc', None)"
    by(rule exec_meth.exec_catch)
  with exec_catch show ?thesis by(simp)
next
  case exec_instr
  note ciins = ‹ci_app ci (ins ! pc) P h stk loc undefined undefined pc []›
  hence "ci_app ci (ins ! pc) P h (stk @ stk'') loc undefined undefined pc []"
    by(rule wf_ci_stk_offerD)
  moreover from ciins
  have "check_instr' (ins ! pc) P h stk loc undefined undefined  pc []"
    by(rule wf_ciD2_ci_app)
  hence "(ta, xcp', h', [(stk' @ stk'', loc', undefined, undefined, pc')]) ∈ exec_instr (ins ! pc) P t h (stk @ stk'') loc undefined undefined pc []"
    using ‹(ta, xcp', h', [(stk', loc', undefined,undefined , pc')]) ∈ exec_instr (ins ! pc) P t h stk loc undefined undefined pc []›
    by(rule exec_instr_stk_offer)
  ultimately show ?thesis using exec_instr by(auto intro: exec_meth.exec_instr)
qed
  
lemma exec_meth_append_xt [intro]:
  "exec_meth ci P ins xt t h s ta h' s'
  ⟹ exec_meth ci P (ins @ ins') (xt @ xt') t h s ta h' s'"
apply(erule exec_meth.cases)
 apply(auto)
 apply(rule exec_instr)
   apply(clarsimp simp add: nth_append)
  apply(simp)
 apply(simp add: nth_append)
apply(rule exec_catch)
by(simp)

lemma exec_meth_append [intro]:
  "exec_meth ci P ins xt t h s ta h' s' ⟹ exec_meth ci P (ins @ ins') xt t h s ta h' s'"
by(rule exec_meth_append_xt[where xt'="[]", simplified])

lemma append_exec_meth_xt:
  assumes exec: "exec_meth ci P ins xt t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  and jump: "jump_ok ins 0 n"
  and pcs: "pcs xt' ⊆ {0..<length ins'}"
  shows "exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, (length ins' + pc), xcp) ta h' (stk', loc', (length ins' + pc'), xcp')"
using exec
proof(cases)
  case (exec_catch xcp d)
  from ‹match_ex_table P (cname_of h xcp) pc xt = ⌊(pc', d)⌋›
  have "match_ex_table P (cname_of h xcp) (length ins' + pc) (shift (length ins') xt) = ⌊(length ins' + pc', d)⌋"
    by(simp add: match_ex_table_shift)
  moreover from pcs have "length ins' + pc ∉ pcs xt'" by(auto)
  ultimately have "match_ex_table P (cname_of h xcp) (length ins' + pc) (xt' @ shift (length ins') xt) = ⌊(length ins' + pc', d)⌋"
    by(simp add: match_ex_table_append_not_pcs)
  with exec_catch show ?thesis by(auto dest: exec_meth.exec_catch)
next
  case exec_instr
  note exec = ‹(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) ∈ exec_instr (ins ! pc) P t h stk loc undefined undefined pc []›
  hence "(ta, xcp', h', [(stk', loc', undefined, undefined, length ins' + pc')]) ∈ exec_instr (ins ! pc) P t h stk loc undefined undefined (length ins' + pc) []"
  proof(cases "ins ! pc")
    case (Goto i)
    with jump ‹pc < length ins› have "- int pc  ≤ i" "i < int (length ins - pc + n)"
      by(auto dest: jump_ok_GotoD)
    with exec Goto show ?thesis by(auto)
  next
    case (IfFalse i)
    with jump ‹pc < length ins› have "- int pc  ≤ i" "i < int (length ins - pc + n)"
      by(auto dest: jump_ok_IfFalseD)
    with exec IfFalse show ?thesis by(auto)
  next
    case (Invoke M n)
    with exec show ?thesis 
      by(auto split: if_split_asm extCallRet.splits split del: if_split simp add: split_beta nth_append min_def extRet2JVM_def)
  qed(auto simp add: split_beta split: if_split_asm sum.split_asm)
  moreover from ‹ci_app ci (ins ! pc) P h stk loc undefined undefined pc []›
  have "ci_app ci (ins ! pc) P h stk loc undefined undefined (length ins' + pc) []"
    by(rule wf_ciD3'_ci_app) simp
  ultimately have "exec_meth ci P (ins' @ ins) (xt' @ shift (length ins') xt) t h (stk, loc, (length ins' + pc), None) ta h' (stk', loc', (length ins' + pc'), xcp')"
    using ‹pc < length ins› by -(rule exec_meth.exec_instr, simp_all)
  thus ?thesis using exec_instr by(auto)
qed

lemma append_exec_meth:
  assumes exec: "exec_meth ci P ins xt t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  and jump: "jump_ok ins 0 n"
  shows "exec_meth ci P (ins' @ ins) (shift (length ins') xt) t h (stk, loc, (length ins' + pc), xcp) ta h' (stk', loc', (length ins' + pc'), xcp')"
using assms by(rule append_exec_meth_xt [where xt'="[]", simplified])

lemma exec_meth_take_xt':
  "⟦ exec_meth ci P (ins @ ins') (xt' @ xt) t h (stk, loc, pc, xcp) ta h' s';
    pc < length ins; pc ∉ pcs xt ⟧
  ⟹ exec_meth ci P ins xt' t h (stk, loc, pc, xcp) ta h' s'"
apply(erule exec_meth.cases)
apply(auto intro: exec_meth.intros simp add: match_ex_table_append nth_append dest: match_ex_table_pcsD)
done

lemma exec_meth_take_xt:
  "⟦ exec_meth ci P (ins @ ins') (xt' @ shift (length ins) xt) t h (stk, loc, pc, xcp) ta h' s';
    pc < length ins ⟧
  ⟹ exec_meth ci P ins xt' t h (stk, loc, pc, xcp) ta h' s'"
by(auto intro: exec_meth_take_xt')

lemma exec_meth_take:
  "⟦ exec_meth ci P (ins @ ins') xt t h (stk, loc, pc, xcp) ta h' s';
    pc < length ins ⟧
  ⟹ exec_meth ci P ins xt t h (stk, loc, pc, xcp) ta h' s'"
by(auto intro: exec_meth_take_xt[where xt = "[]"])


lemma exec_meth_drop_xt:
  assumes exec: "exec_meth ci P (ins @ ins') (xt @ shift (length ins) xt') t h (stk, loc, (length ins + pc), xcp) ta h' (stk', loc', pc', xcp')"
  and xt: "pcs xt ⊆ {..<length ins}"
  and jump: "jump_ok ins' 0 n"
  shows "exec_meth ci P ins' xt' t h (stk, loc, pc, xcp) ta h' (stk', loc', (pc' - length ins), xcp')"
using exec
proof(cases rule: exec_meth.cases)
  case exec_instr
  let ?PC = "length ins + pc"
  note [simp] = ‹xcp = None›
  from ‹?PC < length (ins @ ins')› have pc: "pc < length ins'" by simp
  moreover with ‹(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) ∈ exec_instr ((ins @ ins') ! ?PC) P t h stk loc undefined undefined ?PC []›
  have "(ta, xcp', h', [(stk', loc', undefined, undefined, pc' - length ins)]) ∈ exec_instr (ins' ! pc) P t h stk loc undefined undefined pc []"
    apply(cases "ins' ! pc")
    apply(simp_all add: split_beta split: if_split_asm sum.split_asm split del: if_split)
    apply(force split: extCallRet.splits simp add: min_def extRet2JVM_def)+
    done
  moreover from ‹ci_app ci ((ins @ ins') ! ?PC) P h stk loc undefined undefined ?PC []› jump pc
  have "ci_app ci (ins' ! pc) P h stk loc undefined undefined pc []"
    by(fastforce elim: wf_ciD3_ci_app dest: jump_ok_ins_jump_ok)
  ultimately show ?thesis by(auto intro: exec_meth.intros)
next
  case (exec_catch XCP D)
  let ?PC = "length ins + pc"
  note [simp] = ‹xcp = ⌊XCP⌋›
    ‹ta = ε› ‹h' = h› ‹stk' = Addr XCP # drop (length stk - D) stk› ‹loc' = loc› ‹xcp' = None›
  from ‹match_ex_table P (cname_of h XCP) ?PC (xt @ shift (length ins) xt') = ⌊(pc', D)⌋› xt
  have "match_ex_table P (cname_of h XCP) pc xt' = ⌊(pc' - length ins, D)⌋"
    by(auto simp add: match_ex_table_append dest: match_ex_table_shift_pcD match_ex_table_pcsD)
  with ‹D ≤ length stk› show ?thesis by(auto intro: exec_meth.intros)
qed

lemma exec_meth_drop:
  "⟦ exec_meth ci P (ins @ ins') (shift (length ins) xt) t h (stk, loc, (length ins + pc), xcp) ta h' (stk', loc', pc', xcp');
     jump_ok ins' 0 b ⟧
   ⟹ exec_meth ci P ins' xt t h (stk, loc, pc, xcp) ta h' (stk', loc', (pc' - length ins), xcp')"
by(auto intro: exec_meth_drop_xt[where xt = "[]"])

lemma exec_meth_drop_xt_pc:
  assumes exec: "exec_meth ci P (ins @ ins') (xt @ shift (length ins) xt') t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  and pc: "pc ≥ length ins"
  and pcs: "pcs xt ⊆ {..<length ins}"
  and jump: "jump_ok ins' 0 n'"
  shows "pc' ≥ length ins"
using exec
proof(cases rule: exec_meth.cases)
  case exec_instr thus ?thesis using jump pc
    apply(cases "ins' ! (pc - length ins)")
    apply(simp_all add: split_beta nth_append split: if_split_asm sum.split_asm)
    apply(force split: extCallRet.splits simp add: min_def extRet2JVM_def dest: jump_ok_GotoD jump_ok_IfFalseD)+
    done
next
  case exec_catch thus ?thesis using pcs pc
    by(auto dest: match_ex_table_pcsD match_ex_table_shift_pcD simp add: match_ex_table_append)
qed

lemmas exec_meth_drop_pc = exec_meth_drop_xt_pc[where xt="[]", simplified]

definition exec_move ::
  "('addr, 'heap) check_instr ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'addr expr1
  ⇒ 'heap  ⇒ ('addr val list × 'addr val list × pc × 'addr option)
  ⇒ ('addr, 'thread_id, 'heap) jvm_thread_action
  ⇒ 'heap ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"
where "exec_move ci P t e ≡ exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t"

definition exec_moves :: 
  "('addr, 'heap) check_instr ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'addr expr1 list
  ⇒ 'heap ⇒ ('addr val list × 'addr val list × pc × 'addr option)
  ⇒ ('addr, 'thread_id, 'heap) jvm_thread_action
  ⇒ 'heap ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"
where "exec_moves ci P t es ≡ exec_meth ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t"

abbreviation exec_move_a
where "exec_move_a ≡ exec_move (Abs_check_instr check_instr')"

abbreviation exec_move_d
where "exec_move_d ≡ exec_move (Abs_check_instr check_instr)"

abbreviation exec_moves_a
where "exec_moves_a ≡ exec_moves (Abs_check_instr check_instr')"

abbreviation exec_moves_d
where "exec_moves_d ≡ exec_moves (Abs_check_instr check_instr)"

lemma exec_move_newArrayI:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (newA T⌊e⌉) h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_newArray:
  "pc < length (compE2 e) ⟹ exec_move ci P t (newA T⌊e⌉) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
unfolding exec_move_def by(auto intro!: ext intro: exec_meth_take)

lemma exec_move_CastI:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (Cast T e) h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_Cast:
  "pc < length (compE2 e) ⟹ exec_move ci P t (Cast T e) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
unfolding exec_move_def by(auto intro!: ext intro: exec_meth_take)

lemma exec_move_InstanceOfI:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (e instanceof T) h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_InstanceOf:
  "pc < length (compE2 e) ⟹ exec_move ci P t (e instanceof T) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
unfolding exec_move_def by(auto intro!: ext intro: exec_meth_take)

lemma exec_move_BinOpI1:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (e «bop» e') h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_BinOp1:
  "pc < length (compE2 e) ⟹ exec_move ci P t (e «bop» e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
unfolding exec_move_def
by(auto intro!: ext intro: exec_meth_take_xt simp add: compxE2_size_convs)

lemma exec_move_BinOpI2:
  assumes exec: "exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1 «bop» e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
proof -
  from exec have "exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    unfolding exec_move_def .
  from exec_meth_stk_offer[OF this, where stk''="[v]"] show ?thesis
    by(fastforce split: bop.splits intro: append_exec_meth_xt simp add: exec_move_def compxE2_size_convs compxE2_stack_xlift_convs)
qed

lemma exec_move_LAssI:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (V := e) h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_LAss:
  "pc < length (compE2 e) ⟹ exec_move ci P t (V := e) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
unfolding exec_move_def by(auto intro!: ext intro: exec_meth_take)

lemma exec_move_AAccI1:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (e⌊e'⌉) h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_AAcc1:
  "pc < length (compE2 e) ⟹ exec_move ci P t (e⌊e'⌉) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
unfolding exec_move_def
by(auto intro!: ext intro: exec_meth_take_xt simp add: compxE2_size_convs)

lemma exec_move_AAccI2:
  assumes exec: "exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1⌊e2⌉) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
proof -
  from exec have "exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    unfolding exec_move_def .
  from exec_meth_stk_offer[OF this, where stk''="[v]"] show ?thesis
    by(fastforce intro: append_exec_meth_xt simp add: exec_move_def compxE2_size_convs compxE2_stack_xlift_convs)
qed

lemma exec_move_AAssI1:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (e⌊e'⌉ := e'') h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_AAss1:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (e⌊e'⌉ := e'') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
  (is "?lhs = ?rhs")
proof(rule ext iffI)+
  fix ta h' s' assume "?rhs ta h' s'"
  thus "?lhs ta h' s'" by(rule exec_move_AAssI1)
next
  fix ta h' s' assume "?lhs ta h' s'"
  hence "exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [AStore, Push Unit])
     (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t
     h (stk, loc, pc, xcp) ta h' s'" by(simp add: exec_move_def shift_compxE2 ac_simps)
  thus "?rhs ta h' s'" unfolding exec_move_def using pc by(rule exec_meth_take_xt)
qed

lemma exec_move_AAssI2:
  assumes exec: "exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1⌊e2⌉ := e3) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
proof -
  from exec have "exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    unfolding exec_move_def .
  from exec_meth_stk_offer[OF this, where stk''="[v]", simplified stack_xlift_compxE2, simplified]
  have "exec_meth ci (compP2 P) (compE2 e2 @ compE2 e3 @ [AStore, Push Unit]) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')"
    by(rule exec_meth_append_xt)
  hence "exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2 @ compE2 e3 @ [AStore, Push Unit]) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0))))) t h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
    by(rule append_exec_meth_xt) auto
  thus ?thesis by(auto simp add: exec_move_def shift_compxE2 ac_simps)
qed

lemma exec_move_AAssI3:
  assumes exec: "exec_move ci P t e3 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1⌊e2⌉ := e3) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')"
proof -
  from exec have "exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    unfolding exec_move_def .
  from exec_meth_stk_offer[OF this, where stk''="[v', v]", simplified stack_xlift_compxE2, simplified]
  have "exec_meth ci (compP2 P) (compE2 e3 @ [AStore, Push Unit]) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')"
    by(rule exec_meth_append)
  hence "exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ compE2 e3 @ [AStore, Push Unit]) 
                   ((compxE2 e1 0 0 @ compxE2 e2 (length (compE2 e1)) (Suc 0)) @ shift (length (compE2 e1 @ compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v', v], loc, length (compE2 e1 @ compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1 @ compE2 e2) + pc', xcp')"
    by(rule append_exec_meth_xt) auto
  thus ?thesis by(auto simp add: exec_move_def shift_compxE2 ac_simps)
qed

lemma exec_move_ALengthI:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (e∙length) h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_ALength:
  "pc < length (compE2 e) ⟹ exec_move ci P t (e∙length) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
unfolding exec_move_def by(auto intro!: ext intro: exec_meth_take)

lemma exec_move_FAccI:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (e∙F{D}) h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_FAcc:
  "pc < length (compE2 e) ⟹ exec_move ci P t (e∙F{D}) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
unfolding exec_move_def by(auto intro!: ext intro: exec_meth_take)

lemma exec_move_FAssI1:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (e∙F{D} := e') h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_FAss1:
  "pc < length (compE2 e) ⟹ exec_move ci P t (e∙F{D} := e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
unfolding exec_move_def
by(auto intro!: ext intro: exec_meth_take_xt simp add: compxE2_size_convs)

lemma exec_move_FAssI2:
  assumes exec: "exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1∙F{D} := e2) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
proof -
  from exec have "exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    unfolding exec_move_def .
  from exec_meth_stk_offer[OF this, where stk''="[v]"] show ?thesis
    by(fastforce intro: append_exec_meth_xt simp add: exec_move_def compxE2_size_convs compxE2_stack_xlift_convs)
qed

lemma exec_move_CASI1:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (e∙compareAndSwap(D∙F, e', e'')) h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_CAS1:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (e∙compareAndSwap(D∙F, e', e'')) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
  (is "?lhs = ?rhs")
proof(rule ext iffI)+
  fix ta h' s' assume "?rhs ta h' s'"
  thus "?lhs ta h' s'" by(rule exec_move_CASI1)
next
  fix ta h' s' assume "?lhs ta h' s'"
  hence "exec_meth ci (compP2 P) (compE2 e @ compE2 e' @ compE2 e'' @ [CAS F D])
     (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 0 (Suc 0) @ compxE2 e'' (length (compE2 e')) (Suc (Suc 0)))) t
     h (stk, loc, pc, xcp) ta h' s'" by(simp add: exec_move_def shift_compxE2 ac_simps)
  thus "?rhs ta h' s'" unfolding exec_move_def using pc by(rule exec_meth_take_xt)
qed

lemma exec_move_CASI2:
  assumes exec: "exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1∙compareAndSwap(D∙F, e2, e3)) h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
proof -
  from exec have "exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    unfolding exec_move_def .
  from exec_meth_stk_offer[OF this, where stk''="[v]", simplified stack_xlift_compxE2, simplified]
  have "exec_meth ci (compP2 P) (compE2 e2 @ compE2 e3 @ [CAS F D]) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v], loc, pc, xcp) ta h' (stk' @ [v], loc', pc', xcp')"
    by(rule exec_meth_append_xt)
  hence "exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2 @ compE2 e3 @ [CAS F D]) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 0 (Suc 0) @ shift (length (compE2 e2)) (compxE2 e3 0 (Suc (Suc 0))))) t h (stk @ [v], loc, length (compE2 e1) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e1) + pc', xcp')"
    by(rule append_exec_meth_xt) auto
  thus ?thesis by(auto simp add: exec_move_def shift_compxE2 ac_simps)
qed

lemma exec_move_CASI3:
  assumes exec: "exec_move ci P t e3 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e1∙compareAndSwap(D∙F, e2, e3)) h (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1) + length (compE2 e2) + pc', xcp')"
proof -
  from exec have "exec_meth ci (compP2 P) (compE2 e3) (compxE2 e3 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    unfolding exec_move_def .
  from exec_meth_stk_offer[OF this, where stk''="[v', v]", simplified stack_xlift_compxE2, simplified]
  have "exec_meth ci (compP2 P) (compE2 e3 @ [CAS F D]) (compxE2 e3 0 (Suc (Suc 0))) t h (stk @ [v', v], loc, pc, xcp) ta h' (stk' @ [v', v], loc', pc', xcp')"
    by(rule exec_meth_append)
  hence "exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ compE2 e3 @ [CAS F D]) 
                   ((compxE2 e1 0 0 @ compxE2 e2 (length (compE2 e1)) (Suc 0)) @ shift (length (compE2 e1 @ compE2 e2)) (compxE2 e3 0 (Suc (Suc 0)))) t h (stk @ [v', v], loc, length (compE2 e1 @ compE2 e2) + pc, xcp) ta h' (stk' @ [v', v], loc', length (compE2 e1 @ compE2 e2) + pc', xcp')"
    by(rule append_exec_meth_xt) auto
  thus ?thesis by(auto simp add: exec_move_def shift_compxE2 ac_simps)
qed

lemma exec_move_CallI1:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (e∙M(es)) h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_Call1:
  "pc < length (compE2 e) ⟹ exec_move ci P t (e∙M(es)) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
unfolding exec_move_def
by(auto intro!: ext intro: exec_meth_take_xt simp add: compxEs2_size_convs)

lemma exec_move_CallI2:
  assumes exec: "exec_moves ci P t es h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (e∙M(es)) h (stk @ [v], loc, length (compE2 e) + pc, xcp) ta h' (stk' @ [v], loc', length (compE2 e) + pc', xcp')"
proof -
  from exec have "exec_meth ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    unfolding exec_moves_def .
  from exec_meth_stk_offer[OF this, where stk''="[v]"] show ?thesis
    by(fastforce intro: append_exec_meth_xt simp add: exec_move_def compxEs2_size_convs compxEs2_stack_xlift_convs)
qed

lemma exec_move_BlockNoneI:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t {V:T=None; e} h s ta h' s'"
unfolding exec_move_def by simp

lemma exec_move_BlockNone:
  "exec_move ci P t {V:T=None; e} = exec_move ci P t e"
unfolding exec_move_def by(simp)

lemma exec_move_BlockSomeI:
  assumes exec: "exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t {V:T=⌊v⌋; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp')"
proof -
  let ?ins = "[Push v, Store V]"
  from exec have "exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    by(simp add: exec_move_def)
  hence "exec_meth ci (compP2 P) (?ins @ compE2 e) (shift (length ?ins) (compxE2 e 0 0)) t h (stk, loc, length ?ins + pc, xcp) ta h' (stk', loc', length ?ins + pc', xcp')"
    by(rule append_exec_meth) auto
  thus ?thesis by(simp add: exec_move_def shift_compxE2)
qed

lemma exec_move_BlockSome:
  "exec_move ci P t {V:T=⌊v⌋; e} h (stk, loc, Suc (Suc pc), xcp) ta h' (stk', loc', Suc (Suc pc'), xcp') =
   exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')" (is "?lhs = ?rhs")
proof
  assume ?rhs thus ?lhs by(rule exec_move_BlockSomeI)
next
  let ?ins = "[Push v, Store V]"
  assume ?lhs
  hence "exec_meth ci (compP2 P) (?ins @ compE2 e) (shift (length ?ins) (compxE2 e 0 0)) t h (stk, loc, length ?ins + pc, xcp) ta h' (stk', loc', length ?ins + pc', xcp')"
    by(simp add: exec_move_def shift_compxE2)
  hence "exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', length ?ins + pc' - length ?ins, xcp')"
    by(rule exec_meth_drop) auto
  thus ?rhs by(simp add: exec_move_def)
qed

lemma exec_move_SyncI1:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (sync⇘V⇙ (e) e') h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_Sync1:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (sync⇘V⇙ (e) e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
  (is "?lhs = ?rhs")
proof(rule ext iffI)+
  fix ta h' s'
  assume "?lhs ta h' s'"
  hence "exec_meth ci (compP2 P) (compE2 e @ Dup # Store V # MEnter # compE2 e' @ [Load V, MExit, Goto 4, Load V, MExit, ThrowExc])
                   (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' 3 0 @ [(3, 3 + length (compE2 e'), None, 6 + length (compE2 e'), 0)]))
                   t h (stk, loc, pc, xcp) ta h' s'"
    by(simp add: shift_compxE2 ac_simps exec_move_def)
  thus "?rhs ta h' s'" unfolding exec_move_def using pc by(rule exec_meth_take_xt)
qed(rule exec_move_SyncI1)

lemma exec_move_SyncI2:
  assumes exec: "exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (sync⇘V⇙ (o') e) h (stk, loc, (Suc (Suc (Suc (length (compE2 o') + pc)))), xcp) ta h' (stk', loc', (Suc (Suc (Suc (length (compE2 o') + pc')))), xcp')"
proof -
  let ?e = "compE2 o' @ [Dup, Store V, MEnter]"
  let ?e' = "[Load V, MExit, Goto 4, Load V, MExit, ThrowExc]"
  from exec have "exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    by(simp add: exec_move_def)
  hence "exec_meth ci (compP2 P) ((?e @ compE2 e) @ ?e') ((compxE2 o' 0 0 @ shift (length ?e) (compxE2 e 0 0)) @ [(length ?e, length ?e + length (compE2 e), None, length ?e + length (compE2 e) + 3, 0)]) t h (stk, loc, (length ?e + pc), xcp) ta h' (stk', loc', (length ?e + pc'), xcp')"
    by(rule exec_meth_append_xt[OF append_exec_meth_xt]) auto
  thus ?thesis by(simp add: eval_nat_numeral shift_compxE2 exec_move_def)
qed

lemma exec_move_SeqI1:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (e;;e') h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_Seq1:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (e;;e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
  (is "?lhs = ?rhs")
proof(rule ext iffI)+
  fix ta h' s'
  assume "?lhs ta h' s'"
  hence "exec_meth ci (compP2 P) (compE2 e @ Pop # compE2 e') (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' (Suc 0) 0)) t h (stk, loc, pc, xcp) ta h' s'"
    by(simp add: exec_move_def shift_compxE2)
  thus "?rhs ta h' s'" unfolding exec_move_def using pc by(rule exec_meth_take_xt)
qed(rule exec_move_SeqI1)

lemma exec_move_SeqI2:
  assumes exec: "exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc' ,xcp')"
  shows "exec_move ci P t (e';;e) h (stk, loc, (Suc (length (compE2 e') + pc)), xcp) ta h' (stk', loc', (Suc (length (compE2 e') + pc')), xcp')"
proof -
  from exec have "exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    by(simp add: exec_move_def)
  hence "exec_meth ci (compP2 P) ((compE2 e' @ [Pop]) @ compE2 e) (compxE2 e' 0 0 @ shift (length (compE2 e' @ [Pop])) (compxE2 e 0 0)) t h (stk, loc, (length ((compE2 e') @ [Pop]) + pc), xcp) ta h' (stk', loc', (length ((compE2 e') @ [Pop]) + pc'), xcp')"
    by(rule append_exec_meth_xt) auto
  thus ?thesis by(simp add: shift_compxE2 exec_move_def)
qed

lemma exec_move_Seq2:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (e';;e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta
                                h' (stk', loc', Suc (length (compE2 e') + pc'), xcp') =
         exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  (is "?lhs = ?rhs")
proof
  let ?E = "compE2 e' @ [Pop]"
  assume ?lhs
  hence "exec_meth ci (compP2 P) (?E @ compE2 e) (compxE2 e' 0 0 @ shift (length ?E) (compxE2 e 0 0)) t h (stk, loc, length ?E + pc, xcp) ta h' (stk', loc', length ?E + pc', xcp')"
    by(simp add: exec_move_def shift_compxE2)
  from exec_meth_drop_xt[OF this] show ?rhs unfolding exec_move_def by fastforce
qed(rule exec_move_SeqI2)

lemma exec_move_CondI1:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (if (e) e1 else e2) h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_Cond1:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
  (is "?lhs = ?rhs")
proof(rule ext iffI)+
  let ?E = "IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ Goto (1 + int (length (compE2 e2))) # compE2 e2"
  let ?xt = "compxE2 e1 (Suc 0) 0 @ compxE2 e2 (Suc (Suc (length (compE2 e1)))) 0"
  fix ta h' s'
  assume "?lhs ta h' s'"
  hence "exec_meth ci (compP2 P) (compE2 e @ ?E) (compxE2 e 0 0 @ shift (length (compE2 e)) ?xt) t h (stk, loc, pc, xcp) ta h' s'"
    by(simp add: exec_move_def shift_compxE2 ac_simps)
  thus "?rhs ta h' s'" unfolding exec_move_def using pc by(rule exec_meth_take_xt)
qed(rule exec_move_CondI1)

lemma exec_move_CondI2:
  assumes exec: "exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (if (e) e1 else e2) h (stk, loc, (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', (Suc (length (compE2 e) + pc')), xcp')"
proof -
  from exec have "exec_meth ci (compP2 P) (compE2 e1) (compxE2 e1 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    by(simp add: exec_move_def)
  hence "exec_meth ci (compP2 P) (((compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) @ compE2 e1) @ Goto (1 + int (length (compE2 e2))) # compE2 e2) ((compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))])) (compxE2 e1 0 0)) @ (compxE2 e2 (Suc (Suc (length (compE2 e) + length (compE2 e1)))) 0)) t h (stk, loc, (length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc), xcp) ta h' (stk', loc', (length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc'), xcp')"
    by -(rule exec_meth_append_xt, rule append_exec_meth_xt, auto)
  thus ?thesis by(simp add: shift_compxE2 exec_move_def)
qed

lemma exec_move_Cond2:
  assumes pc: "pc < length (compE2 e1)"
  shows "exec_move ci P t (if (e) e1 else e2) h (stk, loc, (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', (Suc (length (compE2 e) + pc')), xcp') = exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  (is "?lhs = ?rhs")
proof
  let ?E1 = "compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]"
  let ?E2 = "Goto (1 + int (length (compE2 e2))) # compE2 e2"
  assume ?lhs
  hence "exec_meth ci (compP2 P) (?E1 @ compE2 e1 @ ?E2) (compxE2 e 0 0 @ shift (length ?E1) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 (Suc 0) 0))) t h (stk, loc, length ?E1 + pc, xcp) ta h' (stk', loc', length ?E1 + pc', xcp')"
    by(simp add: exec_move_def shift_compxE2 ac_simps)
  thus ?rhs unfolding exec_move_def
    by -(rule exec_meth_take_xt,drule exec_meth_drop_xt,auto simp add: pc)
qed(rule exec_move_CondI2)

lemma exec_move_CondI3:
  assumes exec: "exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')"
proof -
  let ?E = "compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]"
  let ?xt = "compxE2 e 0 0 @ compxE2 e1 (Suc (length (compE2 e))) 0"
  from exec have "exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    by(simp add: exec_move_def)
  hence "exec_meth ci (compP2 P) (?E @ compE2 e2) (?xt @ shift (length ?E) (compxE2 e2 0 0)) t h (stk, loc, length ?E + pc, xcp) ta h' (stk', loc', length ?E + pc', xcp')"
    by(rule append_exec_meth_xt) auto
  thus ?thesis by(simp add: shift_compxE2 exec_move_def)
qed

lemma exec_move_Cond3:
  "exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta
                                      h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp') =
   exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  (is "?lhs = ?rhs")
proof
  let ?E = "compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]"
  let ?xt = "compxE2 e 0 0 @ compxE2 e1 (Suc (length (compE2 e))) 0"
  assume ?lhs
  hence "exec_meth ci (compP2 P) (?E @ compE2 e2) (?xt @ shift (length ?E) (compxE2 e2 0 0)) t h (stk, loc, length ?E + pc, xcp) ta h' (stk', loc', length ?E + pc', xcp')"
    by(simp add: shift_compxE2 exec_move_def)
  thus ?rhs unfolding exec_move_def by -(drule exec_meth_drop_xt, auto)
qed(rule exec_move_CondI3)

lemma exec_move_WhileI1:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (while (e) e') h s ta h' s'"
unfolding exec_move_def by auto

lemma (in ab_group_add) uminus_minus_left_commute:
  "- a - (b + c) = - b - (a + c)"
  by (simp add: algebra_simps)

lemma exec_move_While1:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
  (is "?lhs = ?rhs")
proof(rule ext iffI)+
  let ?E = "IfFalse (3 + int (length (compE2 e'))) # compE2 e' @ [Pop, Goto (- int (length (compE2 e)) + (-2 - int (length (compE2 e')))), Push Unit]"
  let ?xt = "compxE2 e' (Suc 0) 0"
  fix ta h' s'
  assume "?lhs ta h' s'"
  then have "exec_meth ci (compP2 P) (compE2 e @ ?E) (compxE2 e 0 0 @ shift (length (compE2 e)) ?xt) t h (stk, loc, pc, xcp) ta h' s'"
    by (simp add: exec_move_def shift_compxE2 algebra_simps uminus_minus_left_commute)
  thus "?rhs ta h' s'" unfolding exec_move_def using pc by(rule exec_meth_take_xt)
qed(rule exec_move_WhileI1)

lemma exec_move_WhileI2:
  assumes exec: "exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (while (e) e1) h (stk, loc, (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', (Suc (length (compE2 e) + pc')), xcp')"
proof -
  let ?E = "compE2 e @ [IfFalse (3 + int (length (compE2 e1)))]"
  let ?E' = "[Pop, Goto (- int (length (compE2 e)) + (-2 - int (length (compE2 e1)))), Push Unit]"
  from exec have "exec_meth ci (compP2 P) (compE2 e1) (compxE2 e1 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    by(simp add: exec_move_def)
  hence "exec_meth ci (compP2 P) ((?E @ compE2 e1) @ ?E') (compxE2 e 0 0 @ shift (length ?E) (compxE2 e1 0 0)) t h (stk, loc, length ?E + pc, xcp) ta h' (stk', loc', length ?E + pc', xcp')"
    by -(rule exec_meth_append, rule append_exec_meth_xt, auto)
  thus ?thesis by (simp add: shift_compxE2 exec_move_def algebra_simps uminus_minus_left_commute)
qed

lemma exec_move_While2:
  assumes pc: "pc < length (compE2 e')"
  shows "exec_move ci P t (while (e) e') h (stk, loc, (Suc (length (compE2 e) + pc)), xcp) ta
                                    h' (stk', loc', (Suc (length (compE2 e) + pc')), xcp') =
         exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  (is "?lhs = ?rhs")
proof
  let ?E = "compE2 e @ [IfFalse (3 + int (length (compE2 e')))]"
  let ?E' = "[Pop, Goto (- int (length (compE2 e)) + (-2 - int (length (compE2 e')))), Push Unit]"
  assume ?lhs
  hence "exec_meth ci (compP2 P) ((?E @ compE2 e') @ ?E') (compxE2 e 0 0 @ shift (length ?E) (compxE2 e' 0 0)) t h (stk, loc, length ?E + pc, xcp) ta h' (stk', loc', length ?E + pc', xcp')"
    by(simp add: exec_move_def shift_compxE2 algebra_simps uminus_minus_left_commute)
  thus ?rhs unfolding exec_move_def using pc
    by -(drule exec_meth_take, simp, drule exec_meth_drop_xt, auto)
qed(rule exec_move_WhileI2)

lemma exec_move_ThrowI:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (throw e) h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_Throw:
  "pc < length (compE2 e) ⟹ exec_move ci P t (throw e) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
unfolding exec_move_def by(auto intro!: ext intro: exec_meth_take)

lemma exec_move_TryI1:
  "exec_move ci P t e h s ta h' s' ⟹ exec_move ci P t (try e catch(C V) e') h s ta h' s'"
unfolding exec_move_def by auto

lemma exec_move_TryI2:
  assumes exec: "exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (try e' catch(C V) e) h (stk, loc, Suc (Suc (length (compE2 e') + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e') + pc')), xcp')"
proof -
  let ?e = "compE2 e' @ [Goto (int(size (compE2 e))+2), Store V]"
  from exec have "exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    by(simp add: exec_move_def)
  hence "exec_meth ci (compP2 P) ((?e @ compE2 e) @ []) ((compxE2 e' 0 0 @ shift (length ?e) (compxE2 e 0 0)) @ [(0, length (compE2 e'), ⌊C⌋, Suc (length (compE2 e')), 0)]) t h (stk, loc, (length ?e + pc), xcp) ta h' (stk', loc', (length ?e + pc'), xcp')"
    by(rule exec_meth_append_xt[OF append_exec_meth_xt]) auto
  thus ?thesis by(simp add: eval_nat_numeral shift_compxE2 exec_move_def)
qed

lemma exec_move_Try2:
  "exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta
                                     h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp') =
   exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  (is "?lhs = ?rhs")
proof
  let ?E = "compE2 e @ [Goto (int(size (compE2 e'))+2), Store V]"
  let ?xt = "[(0, length (compE2 e), ⌊C⌋, Suc (length (compE2 e)), 0)]"
  assume lhs: ?lhs
  hence pc: "pc < length (compE2 e')"
    by(fastforce elim!: exec_meth.cases simp add: exec_move_def match_ex_table_append match_ex_entry dest: match_ex_table_pcsD)
  from lhs have "exec_meth ci (compP2 P) ((?E @ compE2 e') @ []) ((compxE2 e 0 0 @ shift (length ?E) (compxE2 e' 0 0)) @ ?xt) t h (stk, loc, length ?E + pc, xcp) ta h' (stk', loc', length ?E + pc', xcp')"
    by(simp add: exec_move_def shift_compxE2 ac_simps)
  thus ?rhs unfolding exec_move_def using pc
    by-(drule exec_meth_drop_xt[OF exec_meth_take_xt'], auto)
qed(rule exec_move_TryI2)

lemma exec_move_raise_xcp_pcD:
  "exec_move ci P t E h (stk, loc, pc, None) ta h' (stk', loc', pc', Some a) ⟹ pc' = pc"
apply(cases "compE2 E ! pc")
apply(auto simp add: exec_move_def elim!: exec_meth.cases split: if_split_asm sum.split_asm)
apply(auto split: extCallRet.split_asm simp add: split_beta)
done


definition τexec_meth :: 
  "('addr, 'heap) check_instr ⇒ 'addr jvm_prog ⇒ 'addr instr list ⇒ ex_table ⇒ 'thread_id ⇒ 'heap
  ⇒ ('addr val list × 'addr val list × pc × 'addr option)
  ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"
where
  "τexec_meth ci P ins xt t h s s' ⟷ 
  exec_meth ci P ins xt t h s ε h s' ∧ (snd (snd (snd s)) = None ⟶ τinstr P h (fst s) (ins ! fst (snd (snd s))))"

abbreviation τexec_meth_a
where "τexec_meth_a ≡ τexec_meth (Abs_check_instr check_instr')"

abbreviation τexec_meth_d
where "τexec_meth_d ≡ τexec_meth (Abs_check_instr check_instr)"

lemma τexec_methI [intro]:
  "⟦ exec_meth ci P ins xt t h (stk, loc, pc, xcp) ε h s'; xcp = None ⟹ τinstr P h stk (ins ! pc) ⟧
   ⟹ τexec_meth ci P ins xt t h (stk, loc, pc, xcp) s'"
by(simp add: τexec_meth_def)

lemma τexec_methE [elim]:
  assumes "τexec_meth ci P ins xt t h s s'"
  obtains stk loc pc xcp
  where "s = (stk, loc, pc, xcp)"
  and "exec_meth ci P ins xt t h (stk, loc, pc, xcp) ε h s'"
  and "xcp = None ⟹ τinstr P h stk (ins ! pc)"
using assms
by(cases s)(auto simp add: τexec_meth_def)

abbreviation τExec_methr :: 
  "('addr, 'heap) check_instr ⇒ 'addr jvm_prog ⇒ 'addr instr list ⇒ ex_table ⇒ 'thread_id ⇒ 'heap 
  ⇒ ('addr val list × 'addr val list × pc × 'addr option)
  ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"
where
  "τExec_methr ci P ins xt t h == (τexec_meth ci P ins xt t h)^**"

abbreviation τExec_metht :: 
  "('addr, 'heap) check_instr ⇒ 'addr jvm_prog ⇒ 'addr instr list ⇒ ex_table ⇒ 'thread_id ⇒ 'heap
  ⇒ ('addr val list × 'addr val list × pc × 'addr option)
  ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"
where
  "τExec_metht ci P ins xt t h == (τexec_meth ci P ins xt t h)^++"

abbreviation τExec_methr_a
where "τExec_methr_a ≡ τExec_methr (Abs_check_instr check_instr')"

abbreviation τExec_methr_d
where "τExec_methr_d ≡ τExec_methr (Abs_check_instr check_instr)"

abbreviation τExec_metht_a
where "τExec_metht_a ≡ τExec_metht (Abs_check_instr check_instr')"

abbreviation τExec_metht_d
where "τExec_metht_d ≡ τExec_metht (Abs_check_instr check_instr)"

lemma τExec_methr_refl: "τExec_methr ci P ins xt t h s s" ..

lemma τExec_methr_step':
  "⟦ τExec_methr ci P ins xt t h s (stk', loc', pc', xcp');
     τexec_meth ci P ins xt t h (stk', loc', pc', xcp') s' ⟧
  ⟹ τExec_methr ci P ins xt t h s s'"
by(rule rtranclp.rtrancl_into_rtrancl)

lemma τExec_methr_step:
  "⟦ τExec_methr ci P ins xt t h s (stk', loc', pc', xcp');
     exec_meth ci P ins xt t h (stk', loc', pc', xcp') ε h s';
     xcp' = None ⟹ τinstr P h stk' (ins ! pc') ⟧
  ⟹ τExec_methr ci P ins xt t h s s'"
by(erule τExec_methr_step')(rule τexec_methI)

lemmas τExec_methr_intros = τExec_methr_refl τExec_methr_step
lemmas τExec_methr1step = τExec_methr_step[OF τExec_methr_refl]
lemmas τExec_methr2step = τExec_methr_step[OF τExec_methr_step, OF τExec_methr_refl]
lemmas τExec_methr3step = τExec_methr_step[OF τExec_methr_step, OF τExec_methr_step, OF τExec_methr_refl]

lemma τExec_methr_cases [consumes 1, case_names refl step]:
  assumes "τExec_methr ci P ins xt t h s s'"
  obtains "s = s'"
  | stk' loc' pc' xcp'
    where "τExec_methr ci P ins xt t h s (stk', loc', pc', xcp')"
       "exec_meth ci P ins xt t h (stk', loc', pc', xcp') ε h s'"
       "xcp' = None ⟹ τinstr P h stk' (ins ! pc')"
using assms
by(rule rtranclp.cases)(auto elim!: τexec_methE)

lemma τExec_methr_induct [consumes 1, case_names refl step]:
  "⟦ τExec_methr ci P ins xt t h s s';
     Q s;
     ⋀stk loc pc xcp s'. ⟦ τExec_methr ci P ins xt t h s (stk, loc, pc, xcp); exec_meth ci P ins xt t h (stk, loc, pc, xcp) ε h s';
                          xcp = None ⟹ τinstr P h stk (ins ! pc); Q (stk, loc, pc, xcp) ⟧ ⟹ Q s' ⟧
  ⟹ Q s'"
by(erule (1) rtranclp_induct)(blast elim: τexec_methE)

lemma τExec_methr_trans: 
  "⟦ τExec_methr ci P ins xt t h s s'; τExec_methr ci P ins xt t h s' s'' ⟧ ⟹ τExec_methr ci P ins xt t h s s''"
by(rule rtranclp_trans)

lemmas τExec_meth_induct_split = τExec_methr_induct[split_format (complete), consumes 1, case_names τExec_refl τExec_step]

lemma τExec_methr_converse_cases [consumes 1, case_names refl step]:
  assumes "τExec_methr ci P ins xt t h s s'"
  obtains "s = s'"
  | stk loc pc xcp s''
    where "s = (stk, loc, pc, xcp)"
       "exec_meth ci P ins xt t h (stk, loc, pc, xcp) ε h s''"
       "xcp = None ⟹ τinstr P h stk (ins ! pc)"
       "τExec_methr ci P ins xt t h s'' s'"
using assms
by(erule converse_rtranclpE)(blast elim: τexec_methE)

definition τexec_move :: 
  "('addr, 'heap) check_instr ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'addr expr1 ⇒ 'heap
  ⇒ ('addr val list × 'addr val list × pc × 'addr option)
  ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"
where
  "τexec_move ci P t e h =
  (λ(stk, loc, pc, xcp) s'. exec_move ci P t e h (stk, loc, pc, xcp) ε h s' ∧ τmove2 P h stk e pc xcp)"

definition τexec_moves :: 
  "('addr, 'heap) check_instr ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'addr expr1 list ⇒ 'heap
  ⇒ ('addr val list × 'addr val list × pc × 'addr option)
  ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"
where
  "τexec_moves ci P t es h =
   (λ(stk, loc, pc, xcp) s'. exec_moves ci P t es h (stk, loc, pc, xcp) ε h s' ∧ τmoves2 P h stk es pc xcp)"

lemma τexec_moveI:
  "⟦ exec_move ci P t e h (stk, loc, pc, xcp) ε h s'; τmove2 P h stk e pc xcp ⟧ 
  ⟹ τexec_move ci P t e h (stk, loc, pc, xcp) s'"
by(simp add: τexec_move_def)

lemma τexec_moveE:
  assumes "τexec_move ci P t e h (stk, loc, pc, xcp) s'"
  obtains "exec_move ci P t e h (stk, loc, pc, xcp) ε h s'" "τmove2 P h stk e pc xcp"
using assms by(simp add: τexec_move_def)

lemma τexec_movesI:
  "⟦ exec_moves ci P t es h (stk, loc, pc, xcp) ε h s'; τmoves2 P h stk es pc xcp ⟧ 
  ⟹ τexec_moves ci P t es h (stk, loc, pc, xcp) s'"
by(simp add: τexec_moves_def)

lemma τexec_movesE:
  assumes "τexec_moves ci P t es h (stk, loc, pc, xcp) s'"
  obtains "exec_moves ci P t es h (stk, loc, pc, xcp) ε h s'" "τmoves2 P h stk es pc xcp"
using assms by(simp add: τexec_moves_def)

lemma τexec_move_conv_τexec_meth:
  "τexec_move ci P t e = τexec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t"
by(auto simp add: τexec_move_def exec_move_def τmove2_iff compP2_def intro!: ext τexec_methI elim!: τexec_methE)

lemma τexec_moves_conv_τexec_meth:
  "τexec_moves ci P t es = τexec_meth ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t"
by(auto simp add: τexec_moves_def exec_moves_def τmoves2_iff compP2_def intro!: ext τexec_methI elim!: τexec_methE)

abbreviation τExec_mover
where "τExec_mover ci P t e h == (τexec_move ci P t e h)^**"

abbreviation τExec_movet
where "τExec_movet ci P t e h == (τexec_move ci P t e h)^++"

abbreviation τExec_mover_a
where "τExec_mover_a ≡ τExec_mover (Abs_check_instr check_instr')"

abbreviation τExec_mover_d
where "τExec_mover_d ≡ τExec_mover (Abs_check_instr check_instr)"

abbreviation τExec_movet_a
where "τExec_movet_a ≡ τExec_movet (Abs_check_instr check_instr')"

abbreviation τExec_movet_d
where "τExec_movet_d ≡ τExec_movet (Abs_check_instr check_instr)"

abbreviation τExec_movesr
where "τExec_movesr ci P t e h == (τexec_moves ci P t e h)^**"

abbreviation τExec_movest
where "τExec_movest ci P t e h == (τexec_moves ci P t e h)^++"

abbreviation τExec_movesr_a
where "τExec_movesr_a ≡ τExec_movesr (Abs_check_instr check_instr')"

abbreviation τExec_movesr_d
where "τExec_movesr_d ≡ τExec_movesr (Abs_check_instr check_instr)"

abbreviation τExec_movest_a
where "τExec_movest_a ≡ τExec_movest (Abs_check_instr check_instr')"

abbreviation τExec_movest_d
where "τExec_movest_d ≡ τExec_movest (Abs_check_instr check_instr)"

lemma τExecr_refl: "τExec_mover ci P t e h s s"
by(rule rtranclp.rtrancl_refl)

lemma τExecsr_refl: "τExec_movesr ci P t e h s s"
by(rule rtranclp.rtrancl_refl)

lemma τExecr_step: 
  "⟦ τExec_mover ci P t e h s (stk', loc', pc', xcp');
     exec_move ci P t e h (stk', loc', pc', xcp') ε h s';
     τmove2 P h stk' e pc' xcp' ⟧
  ⟹ τExec_mover ci P t e h s s'"
by(rule rtranclp.rtrancl_into_rtrancl)(auto elim: τexec_moveI)

lemma τExecsr_step: 
  "⟦ τExec_movesr ci P t es h s (stk', loc', pc', xcp');
     exec_moves ci P t es h (stk', loc', pc', xcp') ε h s';
     τmoves2 P h stk' es pc' xcp' ⟧
  ⟹ τExec_movesr ci P t es h s s'"
by(rule rtranclp.rtrancl_into_rtrancl)(auto elim: τexec_movesI)

lemma τExect_step:
  "⟦ τExec_movet ci P t e h s (stk', loc', pc', xcp');
     exec_move ci P t e h (stk', loc', pc', xcp') ε h s';
     τmove2 P h stk' e pc' xcp' ⟧
  ⟹ τExec_movet ci P t e h s s'"
by(rule tranclp.trancl_into_trancl)(auto intro: τexec_moveI)

lemma τExecst_step:
  "⟦ τExec_movest ci P t es h s (stk', loc', pc', xcp');
     exec_moves ci P t es h (stk', loc', pc', xcp') ε h s';
     τmoves2 P h stk' es pc' xcp' ⟧
  ⟹ τExec_movest ci P t es h s s'"
by(rule tranclp.trancl_into_trancl)(auto intro: τexec_movesI)

lemmas τExecr1step = τExecr_step[OF τExecr_refl]
lemmas τExecr2step = τExecr_step[OF τExecr_step, OF τExecr_refl]
lemmas τExecr3step = τExecr_step[OF τExecr_step, OF τExecr_step, OF τExecr_refl]

lemmas τExecsr1step = τExecsr_step[OF τExecsr_refl]
lemmas τExecsr2step = τExecsr_step[OF τExecsr_step, OF τExecsr_refl]
lemmas τExecsr3step = τExecsr_step[OF τExecsr_step, OF τExecsr_step, OF τExecsr_refl]

lemma τExect1step:
  "⟦ exec_move ci P t e h s ε h s';
     τmove2 P h (fst s) e (fst (snd (snd s))) (snd (snd (snd s))) ⟧
  ⟹ τExec_movet ci P t e h s s'"
by(rule tranclp.r_into_trancl)(cases s, auto intro: τexec_moveI)

lemmas τExect2step = τExect_step[OF τExect1step]
lemmas τExect3step = τExect_step[OF τExect_step, OF τExect1step]

lemma τExecst1step:
  "⟦ exec_moves ci P t es h s ε h s';
     τmoves2 P h (fst s) es (fst (snd (snd s))) (snd (snd (snd s))) ⟧
  ⟹ τExec_movest ci P t es h s s'"
by(rule tranclp.r_into_trancl)(cases s, auto intro: τexec_movesI)

lemmas τExecst2step = τExecst_step[OF τExecst1step]
lemmas τExecst3step = τExecst_step[OF τExecst_step, OF τExecst1step]

lemma τExecr_induct [consumes 1, case_names refl step]:
  assumes major: "τExec_mover ci P t e h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')"
  and refl: "Q stk loc pc xcp"
  and step: "⋀stk' loc' pc' xcp' stk'' loc'' pc'' xcp''.
             ⟦ τExec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp');
               τexec_move ci P t e h (stk', loc', pc', xcp') (stk'', loc'', pc'', xcp''); Q stk' loc' pc' xcp' ⟧
             ⟹ Q stk'' loc'' pc'' xcp''"
  shows "Q stk'' loc'' pc'' xcp''"
using major refl
by(rule rtranclp_induct4)(rule step)

lemma τExecsr_induct [consumes 1, case_names refl step]:
  assumes major: "τExec_movesr ci P t es h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')"
  and refl: "Q stk loc pc xcp"
  and step: "⋀stk' loc' pc' xcp' stk'' loc'' pc'' xcp''.
             ⟦ τExec_movesr ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp');
               τexec_moves ci P t es h (stk', loc', pc', xcp') (stk'', loc'', pc'', xcp''); Q stk' loc' pc' xcp' ⟧
             ⟹ Q stk'' loc'' pc'' xcp''"
  shows "Q stk'' loc'' pc'' xcp''"
using major refl
by(rule rtranclp_induct4)(rule step)

lemma τExect_induct [consumes 1, case_names base step]:
  assumes major: "τExec_movet ci P t e h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')"
  and base: "⋀stk' loc' pc' xcp'. τexec_move ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp') ⟹ Q stk' loc' pc' xcp'"
  and step: "⋀stk' loc' pc' xcp' stk'' loc'' pc'' xcp''.
             ⟦ τExec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp');
               τexec_move ci P t e h (stk', loc', pc', xcp') (stk'', loc'', pc'', xcp''); Q stk' loc' pc' xcp' ⟧
             ⟹ Q stk'' loc'' pc'' xcp''"
  shows "Q stk'' loc'' pc'' xcp''"
using major
by(rule tranclp_induct4)(erule base step)+

lemma τExecst_induct [consumes 1, case_names base step]:
  assumes major: "τExec_movest ci P t es h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')"
  and base: "⋀stk' loc' pc' xcp'. τexec_moves ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp') ⟹ Q stk' loc' pc' xcp'"
  and step: "⋀stk' loc' pc' xcp' stk'' loc'' pc'' xcp''.
             ⟦ τExec_movest ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp');
               τexec_moves ci P t es h (stk', loc', pc', xcp') (stk'', loc'', pc'', xcp''); Q stk' loc' pc' xcp' ⟧
             ⟹ Q stk'' loc'' pc'' xcp''"
  shows "Q stk'' loc'' pc'' xcp''"
using major
by(rule tranclp_induct4)(erule base step)+

lemma τExec_mover_τExec_methr:
  "τExec_mover ci P t e = τExec_methr ci (compP2 P) (compE2 e) (compxE2 e 0 0) t"
by(simp only: τexec_move_conv_τexec_meth)

lemma τExec_movesr_τExec_methr:
  "τExec_movesr ci P t es = τExec_methr ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t"
by(simp only: τexec_moves_conv_τexec_meth)

lemma τExec_movet_τExec_metht:
  "τExec_movet ci P t e = τExec_metht ci (compP2 P) (compE2 e) (compxE2 e 0 0) t"
by(simp only: τexec_move_conv_τexec_meth)

lemma τExec_movest_τExec_metht:
  "τExec_movest ci P t es = τExec_metht ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t"
by(simp only: τexec_moves_conv_τexec_meth)

lemma τExec_mover_trans: 
  "⟦ τExec_mover ci P t e h s s'; τExec_mover ci P t e h s' s'' ⟧ ⟹ τExec_mover ci P t e h s s''"
by(rule rtranclp_trans)

lemma τExec_movesr_trans: 
  "⟦ τExec_movesr ci P t es h s s'; τExec_movesr ci P t es h s' s'' ⟧ ⟹ τExec_movesr ci P t es h s s''"
by(rule rtranclp_trans)

lemma τExec_movet_trans: 
  "⟦ τExec_movet ci P t e h s s'; τExec_movet ci P t e h s' s'' ⟧ ⟹ τExec_movet ci P t e h s s''"
by(rule tranclp_trans)

lemma τExec_movest_trans: 
  "⟦ τExec_movest ci P t es h s s'; τExec_movest ci P t es h s' s'' ⟧ ⟹ τExec_movest ci P t es h s s''"
by(rule tranclp_trans)

lemma τexec_move_into_τexec_moves:
  "τexec_move ci P t e h s s' ⟹ τexec_moves ci P t (e # es) h s s'"
by(cases s)(auto elim!: τexec_moveE intro!: τexec_movesI simp add: exec_move_def exec_moves_def intro: τmoves2Hd)

lemma τExec_mover_τExec_movesr:
  "τExec_mover ci P t e h s s' ⟹ τExec_movesr ci P t (e # es) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl τexec_move_into_τexec_moves)+

lemma τExec_movet_τExec_movest:
  "τExec_movet ci P t e h s s' ⟹ τExec_movest ci P t (e # es) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl τexec_move_into_τexec_moves)+

lemma exec_moves_append: "exec_moves ci P t es h s ta h' s' ⟹ exec_moves ci P t (es @ es') h s ta h' s'"
by(auto simp add: exec_moves_def)

lemma τexec_moves_append: "τexec_moves ci P t es h s s' ⟹ τexec_moves ci P t (es @ es') h s s'"
by(cases s)(auto elim!: τexec_movesE intro!: τexec_movesI exec_moves_append)

lemma τExec_movesr_append [intro]:
  "τExec_movesr ci P t es h s s' ⟹ τExec_movesr ci P t (es @ es') h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl τexec_moves_append)+

lemma τExec_movest_append [intro]:
  "τExec_movest ci P t es h s s' ⟹ τExec_movest ci P t (es @ es') h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl τexec_moves_append)+

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 -
  from exec have "exec_meth ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
    unfolding exec_moves_def .
  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')" by(rule exec_meth_stk_offer)
  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')"
    by(rule append_exec_meth_xt) auto
  thus ?thesis by(simp add: exec_moves_def stack_xlift_compxEs2 shift_compxEs2 len)
qed


lemma append_τexec_moves:
  "⟦ length vs = length es';
    τexec_moves ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp') ⟧
  ⟹ τexec_moves ci P t (es' @ es) h ((stk @ vs), loc, (length (compEs2 es') + pc), xcp) ((stk' @ vs), loc', (length (compEs2 es') + pc'), xcp')"
by(auto elim!: τexec_movesE intro: τexec_movesI append_exec_moves τmoves2_stk_append append_τmoves2)

lemma append_τExec_movesr:
  assumes len: "length vs = length es'"
  shows "τExec_movesr ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_movesr ci P t (es' @ es) h ((stk @ vs), loc, (length (compEs2 es') + pc), xcp) ((stk' @ vs), loc', (length (compEs2 es') + pc'), xcp')"
by(induct rule: rtranclp_induct4)(blast intro: rtranclp.rtrancl_into_rtrancl append_τexec_moves[OF len])+

lemma append_τExec_movest:
  assumes len: "length vs = length es'"
  shows "τExec_movest ci P t es h  (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_movest ci P t (es' @ es) h ((stk @ vs), loc, (length (compEs2 es') + pc), xcp)  ((stk' @ vs), loc', (length (compEs2 es') + pc'), xcp')"
by(induct rule: tranclp_induct4)(blast intro: tranclp.trancl_into_trancl append_τexec_moves[OF len])+


lemma NewArray_τexecI:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (newA T⌊e⌉) h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_newArrayI)

lemma Cast_τexecI:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (Cast T e) h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_CastI)

lemma InstanceOf_τexecI:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (e instanceof T) h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_InstanceOfI)

lemma BinOp_τexecI1:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (e «bop» e') h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_BinOpI1)

lemma BinOp_τexecI2:
  "τexec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τexec_move ci P t (e «bop» e') h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_BinOpI2 τmove2_stk_append)

lemma LAss_τexecI:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (V := e) h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_LAssI)

lemma AAcc_τexecI1:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (e⌊i⌉) h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_AAccI1)

lemma AAcc_τexecI2:
  "τexec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τexec_move ci P t (e⌊e'⌉) h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_AAccI2 τmove2_stk_append)

lemma AAss_τexecI1:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (e⌊i⌉ := e') h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_AAssI1)

lemma AAss_τexecI2:
  "τexec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τexec_move ci P t (e⌊e'⌉ := e'') h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_AAssI2 τmove2_stk_append)

lemma AAss_τexecI3:
  "τexec_move ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τexec_move ci P t (e⌊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')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_AAssI3 τmove2_stk_append)

lemma ALength_τexecI:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (e∙length) h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_ALengthI)

lemma FAcc_τexecI:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (e∙F{D}) h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_FAccI)

lemma FAss_τexecI1:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (e∙F{D} := e') h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_FAssI1)

lemma FAss_τexecI2:
  "τexec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τexec_move ci P t (e∙F{D} := e') h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_FAssI2 τmove2_stk_append)

lemma CAS_τexecI1:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (e∙compareAndSwap(D∙F, e', e'')) h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_CASI1)

lemma CAS_τexecI2:
  "τexec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τexec_move ci P t (e∙compareAndSwap(D∙F, e', e'')) h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_CASI2 τmove2_stk_append)

lemma CAS_τexecI3:
  "τexec_move ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τexec_move ci P t (e∙compareAndSwap(D∙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')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_CASI3 τmove2_stk_append)

lemma Call_τexecI1:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (e∙M(es)) h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_CallI1)

lemma Call_τexecI2:
  "τexec_moves ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τexec_move ci P t (e∙M(es)) h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
by(blast elim: τexec_movesE intro: τexec_moveI τmove2_τmoves2.intros exec_move_CallI2 τmoves2_stk_append)

lemma Block_τexecI_Some:
  "τexec_move ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τexec_move ci P t {V:T=⌊v⌋; e} h (stk, loc, Suc (Suc pc), xcp) (stk', loc', Suc (Suc pc'), xcp')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_BlockSomeI)

lemma Block_τexecI_None:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t {V:T=None; e} h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_BlockNoneI)

lemma Sync_τexecI:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (sync⇘V⇙ (e) e') h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_SyncI1)

lemma Insync_τexecI:
  "τexec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τexec_move ci P t (sync⇘V⇙ (e) e') h (stk, loc, Suc (Suc (Suc (length (compE2 e) + pc))), xcp) (stk', loc', Suc (Suc (Suc (length (compE2 e) + pc'))), xcp')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_SyncI2)

lemma Seq_τexecI1:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (e;; e') h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_SeqI1)

lemma Seq_τexecI2:
  "τexec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τexec_move ci P t (e;; e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) (stk', loc', Suc (length (compE2 e) + pc'), xcp')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_SeqI2)

lemma Cond_τexecI1:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (if (e) e' else e'') h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_CondI1)

lemma Cond_τexecI2:
  "τexec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τ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')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_CondI2)

lemma Cond_τexecI3:
  "τexec_move ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τ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')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_CondI3)

lemma While_τexecI1:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (while (e) e') h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_WhileI1)

lemma While_τexecI2:
  "τexec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τexec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) (stk', loc', Suc (length (compE2 e) + pc'), xcp')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_WhileI2)

lemma Throw_τexecI:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (throw e) h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_ThrowI)

lemma Try_τexecI1:
  "τexec_move ci P t e h s s' ⟹ τexec_move ci P t (try e catch(C V) e') h s s'"
by(cases s)(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_TryI1)

lemma Try_τexecI2:
  "τexec_move ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τ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')"
by(blast elim: τexec_moveE intro: τexec_moveI τmove2_τmoves2.intros exec_move_TryI2)



lemma NewArray_τExecrI:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (newA T⌊e⌉) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl NewArray_τexecI)+

lemma Cast_τExecrI:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (Cast T e) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Cast_τexecI)+

lemma InstanceOf_τExecrI:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (e instanceof T) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl InstanceOf_τexecI)+

lemma BinOp_τExecrI1:
  "τExec_mover ci P t e1 h s s' ⟹ τExec_mover ci P t (e1 «bop» e2) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl BinOp_τexecI1)+

lemma BinOp_τExecrI2:
  "τExec_mover ci P t e2 h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_mover ci P t (e «bop» e2)  h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl BinOp_τexecI2)+

lemma LAss_τExecrI:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (V := e) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl LAss_τexecI)+

lemma AAcc_τExecrI1:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (e⌊i⌉) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl AAcc_τexecI1)+

lemma AAcc_τExecrI2:
  "τExec_mover ci P t i h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_mover ci P t (a⌊i⌉) h ((stk @ [v]), loc, (length (compE2 a) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 a) + pc'), xcp')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl AAcc_τexecI2)+

lemma AAss_τExecrI1:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (e⌊i⌉ := e') h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl AAss_τexecI1)+

lemma AAss_τExecrI2:
  "τExec_mover ci P t i h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_mover ci P t (a⌊i⌉ := e) h ((stk @ [v]), loc, (length (compE2 a) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 a) + pc'), xcp')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl AAss_τexecI2)+

lemma AAss_τExecrI3:
  "τExec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_mover ci P t (a⌊i⌉ := 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')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl AAss_τexecI3)+

lemma ALength_τExecrI:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (e∙length) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl ALength_τexecI)+

lemma FAcc_τExecrI:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (e∙F{D}) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl FAcc_τexecI)+

lemma FAss_τExecrI1:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (e∙F{D} := e') h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl FAss_τexecI1)+

lemma FAss_τExecrI2:
  "τExec_mover ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_mover ci P t (e∙F{D} := e') h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl FAss_τexecI2)+

lemma CAS_τExecrI1:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (e∙compareAndSwap(D∙F, e', e'')) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl CAS_τexecI1)+

lemma CAS_τExecrI2:
  "τExec_mover ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_mover ci P t (e∙compareAndSwap(D∙F, e', e'')) h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl CAS_τexecI2)+

lemma CAS_τExecrI3:
  "τExec_mover ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_mover ci P t (e∙compareAndSwap(D∙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')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl CAS_τexecI3)+

lemma Call_τExecrI1:
  "τExec_mover ci P t obj h s s' ⟹ τExec_mover ci P t (obj∙M'(es)) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Call_τexecI1)+

lemma Call_τExecrI2:
  "τExec_movesr ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_mover ci P t (obj∙M'(es)) h ((stk @ [v]), loc, (length (compE2 obj) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 obj) + pc'), xcp')"
by(induct rule: τExecsr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Call_τexecI2)+

lemma Block_τExecrI_Some:
  "τExec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_mover ci P t {V:T=⌊v⌋; e} h (stk, loc, (Suc (Suc pc)), xcp) (stk', loc', (Suc (Suc pc')), xcp')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Block_τexecI_Some)+

lemma Block_τExecrI_None:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t {V:T=None; e} h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Block_τexecI_None)+

lemma Sync_τExecrI:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (sync⇘V⇙ (e) e') h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Sync_τexecI)+

lemma Insync_τExecrI:
  "τExec_mover ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_mover ci P t (sync⇘V⇙ (e) e')  h (stk, loc, (Suc (Suc (Suc (length (compE2 e) + pc)))), xcp) (stk', loc', (Suc (Suc (Suc (length (compE2 e) + pc')))), xcp')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Insync_τexecI)+

lemma Seq_τExecrI1:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (e;;e') h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Seq_τexecI1)+

lemma Seq_τExecrI2:
  "τExec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc' ,xcp') ⟹
   τExec_mover ci P t (e';;e) h (stk, loc, (Suc (length (compE2 e') + pc)), xcp) (stk', loc', (Suc (length (compE2 e') + pc')), xcp')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Seq_τexecI2)+

lemma Cond_τExecrI1:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (if (e) e1 else e2) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Cond_τexecI1)+

lemma Cond_τExecrI2:
  "τExec_mover ci P t e1  h (stk, loc, pc, xcp) (stk', loc', pc', xcp') ⟹
   τ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')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Cond_τexecI2)+

lemma Cond_τExecrI3:
  "τExec_mover ci P t e2  h (stk, loc ,pc, xcp) (stk', loc', pc', xcp') ⟹
   τ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')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Cond_τexecI3)+

lemma While_τExecrI1:
  "τExec_mover ci P t c h s s' ⟹ τExec_mover ci P t (while (c) e) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl While_τexecI1)+

lemma While_τExecrI2:
  "τExec_mover ci P t E h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τ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')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl While_τexecI2)+

lemma Throw_τExecrI:
  "τExec_mover ci P t e h s s' ⟹ τExec_mover ci P t (throw e) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Throw_τexecI)+

lemma Try_τExecrI1:
  "τExec_mover ci P t E h s s' ⟹ τExec_mover ci P t (try E catch(C' V) e) h s s'"
by(induct rule: rtranclp_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Try_τexecI1)+

lemma Try_τExecrI2:
  "τExec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τ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')"
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl Try_τexecI2)+


lemma NewArray_τExectI:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (newA T⌊e⌉) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl NewArray_τexecI)+

lemma Cast_τExectI:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (Cast T e) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Cast_τexecI)+

lemma InstanceOf_τExectI:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (e instanceof T) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl InstanceOf_τexecI)+

lemma BinOp_τExectI1:
  "τExec_movet ci P t e1 h s s' ⟹ τExec_movet ci P t (e1 «bop» e2) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl BinOp_τexecI1)+

lemma BinOp_τExectI2:
  "τExec_movet ci P t e2 h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_movet ci P t (e «bop» e2)  h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl BinOp_τexecI2)+

lemma LAss_τExectI:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (V := e) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl LAss_τexecI)+

lemma AAcc_τExectI1:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (e⌊i⌉) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl AAcc_τexecI1)+

lemma AAcc_τExectI2:
  "τExec_movet ci P t i h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_movet ci P t (a⌊i⌉) h ((stk @ [v]), loc, (length (compE2 a) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 a) + pc'), xcp')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl AAcc_τexecI2)+

lemma AAss_τExectI1:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (e⌊i⌉ := e') h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl AAss_τexecI1)+

lemma AAss_τExectI2:
  "τExec_movet ci P t i h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_movet ci P t (a⌊i⌉ := e) h ((stk @ [v]), loc, (length (compE2 a) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 a) + pc'), xcp')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl AAss_τexecI2)+

lemma AAss_τExectI3:
  "τExec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_movet ci P t (a⌊i⌉ := 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')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl AAss_τexecI3)+

lemma ALength_τExectI:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (e∙length) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl ALength_τexecI)+

lemma FAcc_τExectI:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (e∙F{D}) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl FAcc_τexecI)+

lemma FAss_τExectI1:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (e∙F{D} := e') h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl FAss_τexecI1)+

lemma FAss_τExectI2:
  "τExec_movet ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_movet ci P t (e∙F{D} := e') h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl FAss_τexecI2)+

lemma CAS_τExectI1:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (e∙compareAndSwap(D∙F, e', e'')) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl CAS_τexecI1)+

lemma CAS_τExectI2:
  "τExec_movet ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_movet ci P t (e∙compareAndSwap(D∙F, e', e'')) h ((stk @ [v]), loc, (length (compE2 e) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 e) + pc'), xcp')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl CAS_τexecI2)+

lemma CAS_τExectI3:
  "τExec_movet ci P t e'' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_movet ci P t (e∙compareAndSwap(D∙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')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl CAS_τexecI3)+

lemma Call_τExectI1:
  "τExec_movet ci P t obj h s s' ⟹ τExec_movet ci P t (obj∙M'(es)) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Call_τexecI1)+

lemma Call_τExectI2:
  "τExec_movest ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_movet ci P t (obj∙M'(es)) h ((stk @ [v]), loc, (length (compE2 obj) + pc), xcp) ((stk' @ [v]), loc', (length (compE2 obj) + pc'), xcp')"
by(induct rule: τExecst_induct)(blast intro: tranclp.trancl_into_trancl Call_τexecI2)+

lemma Block_τExectI_Some:
  "τExec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_movet ci P t {V:T=⌊v⌋; e} h (stk, loc, (Suc (Suc pc)), xcp) (stk', loc', (Suc (Suc pc')), xcp')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl Block_τexecI_Some)+

lemma Block_τExectI_None:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t {V:T=None; e} h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Block_τexecI_None)+

lemma Sync_τExectI:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (sync⇘V⇙ (e) e') h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Sync_τexecI)+

lemma Insync_τExectI:
  "τExec_movet ci P t e' h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τExec_movet ci P t (sync⇘V⇙ (e) e')  h (stk, loc, (Suc (Suc (Suc (length (compE2 e) + pc)))), xcp) (stk', loc', (Suc (Suc (Suc (length (compE2 e) + pc')))), xcp')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl Insync_τexecI)+

lemma Seq_τExectI1:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (e;;e') h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Seq_τexecI1)+

lemma Seq_τExectI2:
  "τExec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc' ,xcp') ⟹
   τExec_movet ci P t (e';;e) h (stk, loc, (Suc (length (compE2 e') + pc)), xcp) (stk', loc', (Suc (length (compE2 e') + pc')), xcp')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl Seq_τexecI2)+

lemma Cond_τExectI1:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (if (e) e1 else e2) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Cond_τexecI1)+

lemma Cond_τExectI2:
  "τExec_movet ci P t e1  h (stk, loc, pc, xcp) (stk', loc', pc', xcp') ⟹
   τ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')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl Cond_τexecI2)+

lemma Cond_τExectI3:
  "τExec_movet ci P t e2  h (stk, loc ,pc, xcp) (stk', loc', pc', xcp') ⟹
   τ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')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl Cond_τexecI3)+

lemma While_τExectI1:
  "τExec_movet ci P t c h s s' ⟹ τExec_movet ci P t (while (c) e) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl While_τexecI1)+

lemma While_τExectI2:
  "τExec_movet ci P t E h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τ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')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl While_τexecI2)+

lemma Throw_τExectI:
  "τExec_movet ci P t e h s s' ⟹ τExec_movet ci P t (throw e) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Throw_τexecI)+

lemma Try_τExectI1:
  "τExec_movet ci P t E h s s' ⟹ τExec_movet ci P t (try E catch(C' V) e) h s s'"
by(induct rule: tranclp_induct)(blast intro: tranclp.trancl_into_trancl Try_τexecI1)+

lemma Try_τExectI2:
  "τExec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
  ⟹ τ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')"
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl Try_τexecI2)+

lemma τExec_movesr_map_Val:
  "τExec_movesr_a P t (map Val vs) h ([], xs, 0, None) ((rev vs), xs, (length (compEs2 (map Val vs))), None)"
proof(induct vs arbitrary: pc stk Ts rule: rev_induct)
  case Nil thus ?case by(auto)
next
  case (snoc v vs')
  let ?E = "compEs2 (map Val vs')"
  from snoc have "τExec_movesr_a P t (map Val (vs' @ [v])) h ([], xs, 0, None) ((rev vs'), xs, (length ?E), None)"
    by auto
  also {
    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) ε h ((v # rev vs'), xs, (length ?E + Suc 0), None)"
      by -(rule append_exec_meth_xt, auto simp add: exec_meth_instr)
    moreover have "τmoves2 (compP2 P) h (rev vs') (map Val vs' @ [Val v]) (length (compEs2 (map Val vs')) + 0) None"
      by(rule append_τmoves2 τmoves2Hd τmove2Val)+
    ultimately have "τ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)"
      by -(rule τExecsr1step, auto simp add: exec_moves_def compP2_def) }
  finally show ?case .
qed

lemma τExec_mover_blocks1 [simp]:
  "τExec_mover ci P t (blocks1 n Ts body) h s s' = τExec_mover ci P t body h s s'"
by(simp add: τexec_move_conv_τexec_meth)

lemma τExec_movet_blocks1 [simp]:
  "τExec_movet ci P t (blocks1 n Ts body) h s s' = τExec_movet ci P t body h s s'"
by(simp add: τexec_move_conv_τexec_meth)


definition τexec_1 :: "'addr jvm_prog ⇒ 'thread_id ⇒ ('addr, 'heap) jvm_state ⇒ ('addr, 'heap) jvm_state ⇒ bool"
  where "τexec_1 P t σ σ' ⟷ exec_1 P t σ ε σ' ∧ τMove2 P σ"

lemma τexec_1I [intro]:
  "⟦ exec_1 P t σ ε σ'; τMove2 P σ ⟧ ⟹ τexec_1 P t σ σ'"
by(simp add: τexec_1_def)

lemma τexec_1E [elim]:
  assumes "τexec_1 P t σ σ'"
  obtains "exec_1 P t σ ε σ'" "τMove2 P σ"
using assms by(auto simp add: τexec_1_def)

abbreviation τExec_1r :: "'addr jvm_prog ⇒ 'thread_id ⇒ ('addr, 'heap) jvm_state ⇒ ('addr, 'heap) jvm_state ⇒ bool"
where "τExec_1r P t == (τexec_1 P t)^**"

abbreviation τExec_1t :: "'addr jvm_prog ⇒ 'thread_id ⇒ ('addr, 'heap) jvm_state ⇒ ('addr, 'heap) jvm_state ⇒ bool"
where "τExec_1t P t == (τexec_1 P t)^++"

definition τexec_1_d :: "'addr jvm_prog ⇒ 'thread_id ⇒ ('addr, 'heap) jvm_state ⇒ ('addr, 'heap) jvm_state ⇒ bool"
where "τexec_1_d P t σ σ' ⟷ exec_1 P t σ ε σ' ∧ τMove2 P σ ∧ check P σ"

lemma τexec_1_dI [intro]:
  "⟦ exec_1 P t σ ε σ'; check P σ; τMove2 P σ ⟧ ⟹ τexec_1_d P t σ σ'"
by(simp add: τexec_1_d_def)

lemma τexec_1_dE [elim]:
  assumes "τexec_1_d P t σ σ'"
  obtains "exec_1 P t σ ε σ'" "check P σ" "τMove2 P σ"
using assms by(auto simp add: τexec_1_d_def)

abbreviation τExec_1_dr :: "'addr jvm_prog ⇒ 'thread_id ⇒ ('addr, 'heap) jvm_state ⇒ ('addr, 'heap) jvm_state ⇒ bool"
where "τExec_1_dr P t == (τexec_1_d P t)^**"

abbreviation τExec_1_dt :: "'addr jvm_prog ⇒ 'thread_id ⇒ ('addr, 'heap) jvm_state ⇒ ('addr, 'heap) jvm_state ⇒ bool"
where "τExec_1_dt P t == (τexec_1_d P t)^++"

declare compxE2_size_convs[simp del] compxEs2_size_convs[simp del]
declare compxE2_stack_xlift_convs[simp del] compxEs2_stack_xlift_convs[simp del]

lemma exec_instr_frs_offer:
  "(ta, xcp', h', (stk', loc', C, M, pc') # frs) ∈ exec_instr ins P t h stk loc C M pc frs
  ⟹ (ta, xcp', h', (stk', loc', C, M, pc') # frs @ frs') ∈ exec_instr ins P t h stk loc C M pc (frs @ frs')"
apply(cases ins)
apply(simp_all add: nth_append split_beta split: if_split_asm sum.split_asm)
apply(force split: extCallRet.split_asm simp add: extRet2JVM_def)+
done

lemma check_instr_frs_offer:
  "⟦ check_instr ins P h stk loc C M pc frs; ins ≠ Return ⟧
  ⟹ check_instr ins P h stk loc C M pc (frs @ frs')"
by(cases ins)(simp_all split: if_split_asm)

lemma exec_instr_CM_change:
  "(ta, xcp', h', (stk', loc', C, M, pc') # frs) ∈ exec_instr ins P t h stk loc C M pc frs
  ⟹ (ta, xcp', h', (stk', loc', C', M', pc') # frs) ∈ exec_instr ins P t h stk loc C' M' pc frs"
apply(cases ins)
apply(simp_all add: nth_append split_beta neq_Nil_conv split: if_split_asm sum.split_asm)
apply(force split: extCallRet.split_asm simp add: extRet2JVM_def)+
done

lemma check_instr_CM_change:
  "⟦ check_instr ins P h stk loc C M pc frs; ins ≠ Return ⟧
  ⟹ check_instr ins P h stk loc C' M' pc frs"
by(cases ins)(simp_all split: if_split_asm)

lemma exec_move_exec_1:
  assumes exec: "exec_move ci P t body h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  and sees: "P ⊢ C sees M : Ts→T = ⌊body⌋ in D"
  shows "exec_1 (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs) ta (xcp', h', (stk', loc', C, M, pc') # frs)"
using exec unfolding exec_move_def
proof(cases)
  case exec_instr
  note [simp] = ‹xcp = None›
    and exec = ‹(ta, xcp', h', [(stk', loc', undefined, undefined, pc')])
                ∈ exec_instr (compE2 body ! pc) (compP2 P) t h stk loc undefined undefined pc []›
  from exec have "(ta, xcp', h', [(stk', loc', C, M, pc')])
                ∈ exec_instr (compE2 body ! pc) (compP2 P) t h stk loc C M pc []"
    by(rule exec_instr_CM_change)
  from exec_instr_frs_offer[OF this, of frs]
  have "(ta, xcp', h', (stk', loc', C, M, pc') # frs)
        ∈ exec_instr (compE2 body ! pc) (compP2 P) t h stk loc C M pc frs" by simp
  with sees ‹pc < length (compE2 body)› show ?thesis
    by(simp add: exec_1_iff compP2_def compMb2_def nth_append)
next
  case exec_catch
  thus ?thesis using sees_method_compP[OF sees, of "λC M Ts T. compMb2"]
    by(simp add: exec_1_iff compMb2_def compP2_def)
qed

lemma τexec_move_τexec_1:
  assumes exec: "τexec_move ci P t body h (stk, loc, pc, xcp) (stk', loc', pc', xcp')"
  and sees: "P ⊢ C sees M : Ts→T = ⌊body⌋ in D"
  shows "τexec_1 (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs) (xcp', h, (stk', loc', C, M, pc') # frs)"
proof(rule τexec_1I)
  from exec obtain exec': "exec_move ci P t body h (stk, loc, pc, xcp) ε h (stk', loc', pc', xcp')"
    and τ: "τmove2 P h stk body pc xcp" by(rule τexec_moveE)
  have "exec_1 (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs) ε (xcp', h, (stk', loc', C, M, pc') # frs)"
    using exec' sees by(rule exec_move_exec_1)
  thus "compP2 P,t ⊢ (xcp, h, (stk, loc, C, M, pc) # frs) -ε-jvm→ (xcp', h, (stk', loc', C, M, pc') # frs)" by auto
  { fix a
    assume [simp]: "xcp = ⌊a⌋" 
    from sees_method_compP[OF sees, of "λC M Ts T. compMb2"]
    have "ex_table_of (compP2 P) C M = compxE2 body 0 0" by(simp add: compP2_def compMb2_def)
    hence "match_ex_table (compP2 P) (cname_of h a) pc (ex_table_of (compP2 P) C M) ≠ None" "pc < length (compE2 body)"
      using exec' sees by(auto simp add: exec_move_def elim: exec_meth.cases) }
  with τ sees sees_method_compP[OF sees, of "λC M Ts T. compMb2"]
  show "τMove2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)" 
    unfolding τMove2_compP2[OF sees] by(fastforce simp add: compP2_def compMb2_def)
qed

lemma τExec_mover_τExec_1r:
  assumes move: "τExec_mover ci P t body h (stk, loc, pc, xcp) (stk', loc', pc', xcp')"
  and sees: "P ⊢ C sees M : Ts→T = ⌊body⌋ in D"
  shows "τExec_1r (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs') (xcp', h, (stk', loc', C, M, pc') # frs')"
using move
by(induct rule: τExecr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl τexec_move_τexec_1[OF _ sees])+

lemma τExec_movet_τExec_1t:
  assumes move: "τExec_movet ci P t body h (stk, loc, pc, xcp) (stk', loc', pc', xcp')"
  and sees: "P ⊢ C sees M : Ts→T = ⌊body⌋ in D"
  shows "τExec_1t (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs') (xcp', h, (stk', loc', C, M, pc') # frs')"
using move
by(induct rule: τExect_induct)(blast intro: tranclp.trancl_into_trancl τexec_move_τexec_1[OF _ sees])+

lemma τExec_1r_rtranclpD:
  "τExec_1r P t (xcp, h, frs) (xcp', h', frs')
  ⟹ (λ((xcp, frs), h) ((xcp', frs'), h'). exec_1 P t (xcp, h, frs) ε (xcp', h', frs') ∧ τMove2 P (xcp, h, frs))^** ((xcp, frs), h) ((xcp', frs'), h')"
by(induct rule: rtranclp_induct3)(fastforce intro: rtranclp.rtrancl_into_rtrancl)+

lemma τExec_1t_rtranclpD:
  "τExec_1t P t (xcp, h, frs) (xcp', h', frs')
  ⟹ (λ((xcp, frs), h) ((xcp', frs'), h'). exec_1 P t (xcp, h, frs) ε (xcp', h', frs') ∧ τMove2 P (xcp, h, frs))^++ ((xcp, frs), h) ((xcp', frs'), h')"
by(induct rule: tranclp_induct3)(fastforce intro: tranclp.trancl_into_trancl)+

lemma exec_meth_length_compE2_stack_xliftD:
  "exec_meth ci P (compE2 e) (stack_xlift d (compxE2 e 0 0)) t h (stk, loc, pc, xcp) ta h' s'
  ⟹ pc < length (compE2 e)"
by(cases s')(auto simp add: stack_xlift_compxE2)

lemma exec_meth_length_pc_xt_Nil:
  "exec_meth ci P ins [] t h (stk, loc, pc, xcp) ta h' s' ⟹ pc < length ins"
apply(erule exec_meth.cases)
apply(auto dest: match_ex_table_pc_length_compE2)
done

lemma BinOp_exec2D:
  assumes exec: "exec_meth ci (compP2 P) (compE2 (e1 «bop» e2)) (compxE2 (e1 «bop» e2) 0 0) t h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')"
  and pc: "pc < length (compE2 e2)"
  shows "exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v1]) (compxE2 e2 0 0)) t h (stk @ [v1], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 e1), xcp') ∧ pc' ≥ length (compE2 e1)"
proof
  from exec have "exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ [BinOpInstr bop])
     (compxE2 e1 0 0 @ shift (length (compE2 e1)) (stack_xlift (length [v1]) (compxE2 e2 0 0))) t h
     (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')"
    by(simp add: compxE2_size_convs compxE2_stack_xlift_convs)
  hence exec': "exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (stack_xlift (length [v1]) (compxE2 e2 0 0))) t h
     (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')"
    by(rule exec_meth_take) (simp add: pc)
  thus "exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v1]) (compxE2 e2 0 0)) t h
     (stk @ [v1], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 e1), xcp')"
    by(rule exec_meth_drop_xt) auto
  from exec' show "pc' ≥ length (compE2 e1)"
   by(rule exec_meth_drop_xt_pc)(auto)
qed

lemma Call_execParamD:
  assumes exec: "exec_meth ci (compP2 P) (compE2 (obj∙M'(ps))) (compxE2 (obj∙M'(ps)) 0 0) t h (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')"
  and pc: "pc < length (compEs2 ps)"
  shows "exec_meth ci (compP2 P) (compEs2 ps) (stack_xlift (length [v]) (compxEs2 ps 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 obj), xcp') ∧ pc' ≥ length (compE2 obj)"
proof
  from exec have "exec_meth ci (compP2 P) ((compE2 obj @ compEs2 ps) @ [Invoke M' (length ps)])
     (compxE2 obj 0 0 @ shift (length (compE2 obj)) (stack_xlift (length [v]) (compxEs2 ps 0 0))) t h
     (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')"
    by(simp add: compxEs2_size_convs compxEs2_stack_xlift_convs)
  hence exec': "exec_meth ci (compP2 P) (compE2 obj @ compEs2 ps) (compxE2 obj 0 0 @ shift (length (compE2 obj)) (stack_xlift (length [v]) (compxEs2 ps 0 0))) t h
     (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')"
    by(rule exec_meth_take)(simp add: pc)
  thus "exec_meth ci (compP2 P) (compEs2 ps) (stack_xlift (length [v]) (compxEs2 ps 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 obj), xcp')"
    by(rule exec_meth_drop_xt) auto
  from exec' show "pc' ≥ length (compE2 obj)"
   by(rule exec_meth_drop_xt_pc)(auto)
qed

lemma exec_move_length_compE2D [dest]:
  "exec_move ci P t e h (stk, loc, pc, xcp) ta h' s' ⟹ pc < length (compE2 e)"
by(cases s')(auto simp add: exec_move_def)

lemma exec_moves_length_compEs2D [dest]:
  "exec_moves ci P t es h (stk, loc, pc, xcp) ta h' s' ⟹ pc < length (compEs2 es)"
by(cases s')(auto simp add: exec_moves_def)

lemma exec_meth_ci_appD:
  "⟦ exec_meth ci P ins xt t h (stk, loc, pc, None) ta h' fr' ⟧
  ⟹  ci_app ci (ins ! pc) P h stk loc undefined undefined pc []"
by(cases fr')(simp add: exec_meth_instr)

lemma exec_move_ci_appD:
  "exec_move ci P t E h (stk, loc, pc, None) ta h' fr'
  ⟹ ci_app ci (compE2 E ! pc) (compP2 P) h stk loc undefined undefined pc []"
unfolding exec_move_def by(rule exec_meth_ci_appD)

lemma exec_moves_ci_appD:
  "exec_moves ci P t Es h (stk, loc, pc, None) ta h' fr'
  ⟹ ci_app ci (compEs2 Es ! pc) (compP2 P) h stk loc undefined undefined pc []"
unfolding exec_moves_def by(rule exec_meth_ci_appD)

lemma τinstr_stk_append_check:
  "check_instr' i P h stk loc C M pc frs ⟹ τinstr P h (stk @ vs) i = τinstr P h stk i"
by(cases i)(simp_all add: nth_append)

lemma τinstr_stk_drop_exec_move:
  "exec_move ci P t e h (stk, loc, pc, None) ta h' fr'
  ⟹ τinstr (compP2 P) h (stk @ vs) (compE2 e ! pc) = τinstr (compP2 P) h stk (compE2 e ! pc)"
apply(drule exec_move_ci_appD)
apply(drule wf_ciD2_ci_app)
apply(erule τinstr_stk_append_check)
done

lemma τinstr_stk_drop_exec_moves:
  "exec_moves ci P t es h (stk, loc, pc, None) ta h' fr'
  ⟹ τinstr (compP2 P) h (stk @ vs) (compEs2 es ! pc) = τinstr (compP2 P) h stk (compEs2 es ! pc)"
apply(drule exec_moves_ci_appD)
apply(drule wf_ciD2_ci_app)
apply(erule τinstr_stk_append_check)
done

end

end