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 = (