Theory JVMTau

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

section ‹Unobservable steps for the JVM›

theory JVMTau imports
  TypeComp
  "../JVM/JVMThreaded"
  "../Framework/FWLTS"
begin

declare nth_append [simp del]
declare Listn.lesub_list_impl_same_size[simp del]
declare listE_length [simp del]

declare match_ex_table_append_not_pcs[simp del]
  outside_pcs_not_matches_entry [simp del]
  outside_pcs_compxE2_not_matches_entry [simp del]
  outside_pcs_compxEs2_not_matches_entry [simp del]

context JVM_heap_base begin

primrec τinstr :: "'m prog ⇒ 'heap ⇒ 'addr val list ⇒ 'addr instr ⇒ bool"
where
  "τinstr P h stk (Load n) = True"
| "τinstr P h stk (Store n) = True"
| "τinstr P h stk (Push v) = True"
| "τinstr P h stk (New C) = False"
| "τinstr P h stk (NewArray T) = False"
| "τinstr P h stk ALoad = False"
| "τinstr P h stk AStore = False"
| "τinstr P h stk ALength = False"
| "τinstr P h stk (Getfield F D) = False"
| "τinstr P h stk (Putfield F D) = False"
| "τinstr P h stk (CAS F D) = False"
| "τinstr P h stk (Checkcast T) = True"
| "τinstr P h stk (Instanceof T) = True"
| "τinstr P h stk (Invoke M n) = 
   (n < length stk ∧ 
    (stk ! n = Null ∨ 
     (∀T Ts Tr D. typeof_addr h (the_Addr (stk ! n)) = ⌊T⌋ ⟶ P ⊢ class_type_of T sees M:Ts→Tr = Native in D ⟶ τexternal_defs D M)))"
| "τinstr P h stk Return = True"
| "τinstr P h stk Pop = True"
| "τinstr P h stk Dup = True"
| "τinstr P h stk Swap = True"
| "τinstr P h stk (BinOpInstr bop) = True"
| "τinstr P h stk (Goto i) = True"
| "τinstr P h stk (IfFalse i) = True" 
| "τinstr P h stk ThrowExc = True"
| "τinstr P h stk MEnter = False"
| "τinstr P h stk MExit = False"

inductive τmove2 :: "'m prog ⇒ 'heap ⇒ 'addr val list ⇒ 'addr expr1 ⇒ nat ⇒ 'addr option ⇒ bool"
  and τmoves2 :: "'m prog ⇒ 'heap ⇒ 'addr val list ⇒ 'addr expr1 list ⇒ nat ⇒ 'addr option ⇒ bool"
for P :: "'m prog" and h :: 'heap and stk :: "'addr val list"
where
  τmove2xcp: "pc < length (compE2 e) ⟹ τmove2 P h stk e pc ⌊xcp⌋"

| τmove2NewArray: "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (newA T⌊e⌉) pc xcp"

| τmove2Cast: "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (Cast T e) pc xcp"
| τmove2CastRed: "τmove2 P h stk (Cast T e) (length (compE2 e)) None"

| τmove2InstanceOf: "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (e instanceof T) pc xcp"
| τmove2InstanceOfRed: "τmove2 P h stk (e instanceof T) (length (compE2 e)) None"

| τmove2Val: "τmove2 P h stk (Val v) 0 None"

| τmove2BinOp1:
  "τmove2 P h stk e1 pc xcp ⟹ τmove2 P h stk (e1«bop»e2) pc xcp"
| τmove2BinOp2:
  "τmove2 P h stk e2 pc xcp ⟹ τmove2 P h stk (e1«bop»e2) (length (compE2 e1) + pc) xcp"
| τmove2BinOp:
  "τmove2 P h stk (e1«bop»e2) (length (compE2 e1) + length (compE2 e2)) None"

| τmove2Var:
  "τmove2 P h stk (Var V) 0 None"

| τmove2LAss:
  "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (V:=e) pc xcp"
| τmove2LAssRed1:
  "τmove2 P h stk (V:=e) (length (compE2 e)) None"
| τmove2LAssRed2:  "τmove2 P h stk (V:=e) (Suc (length (compE2 e))) None"

| τmove2AAcc1: "τmove2 P h stk a pc xcp ⟹ τmove2 P h stk (a⌊i⌉) pc xcp"
| τmove2AAcc2: "τmove2 P h stk i pc xcp ⟹ τmove2 P h stk (a⌊i⌉) (length (compE2 a) + pc) xcp"

| τmove2AAss1: "τmove2 P h stk a pc xcp ⟹ τmove2 P h stk (a⌊i⌉ := e) pc xcp"
| τmove2AAss2: "τmove2 P h stk i pc xcp ⟹ τmove2 P h stk (a⌊i⌉ := e) (length (compE2 a) + pc) xcp"
| τmove2AAss3: "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (a⌊i⌉ := e) (length (compE2 a) + length (compE2 i) + pc) xcp"
| τmove2AAssRed: "τmove2 P h stk (a⌊i⌉ := e) (Suc (length (compE2 a) + length (compE2 i) + length (compE2 e))) None"

| τmove2ALength: "τmove2 P h stk a pc xcp ⟹ τmove2 P h stk (a∙length) pc xcp"

| τmove2FAcc: "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (e∙F{D}) pc xcp"

| τmove2FAss1: "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (e∙F{D} := e') pc xcp"
| τmove2FAss2: "τmove2 P h stk e' pc xcp ⟹ τmove2 P h stk (e∙F{D} := e') (length (compE2 e) + pc) xcp"
| τmove2FAssRed: "τmove2 P h stk (e∙F{D} := e') (Suc (length (compE2 e) + length (compE2 e'))) None"

| τmove2CAS1: "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (e∙compareAndSwap(D∙F, e', e'')) pc xcp"
| τmove2CAS2: "τmove2 P h stk e' pc xcp ⟹ τmove2 P h stk (e∙compareAndSwap(D∙F, e', e'')) (length (compE2 e) + pc) xcp"
| τmove2CAS3: "τmove2 P h stk e'' pc xcp ⟹ τmove2 P h stk (e∙compareAndSwap(D∙F, e', e'')) (length (compE2 e) + length (compE2 e') + pc) xcp"

| τmove2CallObj:
  "τmove2 P h stk obj pc xcp ⟹ τmove2 P h stk (obj∙M(ps)) pc xcp"
| τmove2CallParams:
  "τmoves2 P h stk ps pc xcp ⟹ τmove2 P h stk (obj∙M(ps)) (length (compE2 obj) + pc) xcp"
| τmove2Call:
  "⟦ length ps < length stk;
     stk ! length ps = Null ∨ 
     (∀T Ts Tr D. typeof_addr h (the_Addr (stk ! length ps)) = ⌊T⌋ ⟶ P ⊢ class_type_of T sees M:Ts→Tr = Native in D ⟶ τexternal_defs D M)⟧
  ⟹ τmove2 P h stk (obj∙M(ps)) (length (compE2 obj) + length (compEs2 ps)) None"

| τmove2BlockSome1:
  "τmove2 P h stk {V:T=⌊v⌋; e} 0 None"
| τmove2BlockSome2:
  "τmove2 P h stk {V:T=⌊v⌋; e} (Suc 0) None"
| τmove2BlockSome:
  "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk {V:T=⌊v⌋; e} (Suc (Suc pc)) xcp"
| τmove2BlockNone:
  "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk {V:T=None; e} pc xcp"

| τmove2Sync1:
  "τmove2 P h stk o' pc xcp ⟹ τmove2 P h stk (sync⇘V⇙ (o') e) pc xcp"
| τmove2Sync2:
  "τmove2 P h stk (sync⇘V⇙ (o') e) (length (compE2 o')) None"
| τmove2Sync3:
  "τmove2 P h stk (sync⇘V⇙ (o') e) (Suc (length (compE2 o'))) None"
| τmove2Sync4:
  "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (sync⇘V⇙ (o') e) (Suc (Suc (Suc (length (compE2 o') + pc)))) xcp"
| τmove2Sync5:
  "τmove2 P h stk (sync⇘V⇙ (o') e) (Suc (Suc (Suc (length (compE2 o') + length (compE2 e))))) None"
| τmove2Sync6:
  "τmove2 P h stk (sync⇘V⇙ (o') e) (5 + length (compE2 o') + length (compE2 e)) None"
| τmove2Sync7:
  "τmove2 P h stk (sync⇘V⇙ (o') e) (6 + length (compE2 o') + length (compE2 e)) None"
| τmove2Sync8:
  "τmove2 P h stk (sync⇘V⇙ (o') e) (8 + length (compE2 o') + length (compE2 e)) None"

(* This is only because compE2 produces @{term "Goto 1"} for insync expressions. *)
| τmove2InSync: "τmove2 P h stk (insync⇘V⇙ (a) e) 0 None"

| τmove2Seq1:
  "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (e;;e') pc xcp"
| τmove2SeqRed:
  "τmove2 P h stk (e;;e') (length (compE2 e)) None"
| τmove2Seq2:
  "τmove2 P h stk e' pc xcp ⟹ τmove2 P h stk (e;;e') (Suc (length (compE2 e) + pc)) xcp"

| τmove2Cond:
  "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (if (e) e1 else e2) pc xcp"
| τmove2CondRed:
  "τmove2 P h stk (if (e) e1 else e2) (length (compE2 e)) None"
| τmove2CondThen:
  "τmove2 P h stk e1 pc xcp
  ⟹ τmove2 P h stk (if (e) e1 else e2) (Suc (length (compE2 e) + pc)) xcp"
| τmove2CondThenExit:
  "τmove2 P h stk (if (e) e1 else e2) (Suc (length (compE2 e) + length (compE2 e1))) None "
| τmove2CondElse:
  "τmove2 P h stk e2 pc xcp
  ⟹ τmove2 P h stk (if (e) e1 else e2) (Suc (Suc (length (compE2 e) + length (compE2 e1) + pc))) xcp "

| τmove2While1:
  "τmove2 P h stk c pc xcp ⟹ τmove2 P h stk (while (c) e) pc xcp"
| τmove2While2:
  "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (while (c) e) (Suc (length (compE2 c) + pc)) xcp"
| τmove2While3: ― ‹Jump back to condition›
  "τmove2 P h stk (while (c) e) (Suc (Suc (length (compE2 c) + length (compE2 e)))) None"
| τmove2While4: ― ‹last instruction: Push Unit›
  "τmove2 P h stk (while (c) e) (Suc (Suc (Suc (length (compE2 c) + length (compE2 e))))) None"
| τmove2While5: ― ‹IfFalse instruction›
  "τmove2 P h stk (while (c) e) (length (compE2 c)) None"
| τmove2While6: ― ‹Pop instruction›
  "τmove2 P h stk (while (c) e) (Suc (length (compE2 c) + length (compE2 e))) None"

| τmove2Throw1:
  "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (throw e) pc xcp"
| τmove2Throw2:
  "τmove2 P h stk (throw e) (length (compE2 e)) None"

| τmove2Try1:
  "τmove2 P h stk e pc xcp ⟹ τmove2 P h stk (try e catch(C V) e') pc xcp"
| τmove2TryJump:
  "τmove2 P h stk (try e catch(C V) e') (length (compE2 e)) None"
| τmove2TryCatch2:
  "τmove2 P h stk (try e catch(C V) e') (Suc (length (compE2 e))) None"
| τmove2Try2:
  "τmove2 P h stk {V:T=None; e'} pc xcp
  ⟹ τmove2 P h stk (try e catch(C V) e') (Suc (Suc (length (compE2 e) + pc))) xcp"

| τmoves2Hd:
  "τmove2 P h stk e pc xcp ⟹ τmoves2 P h stk (e # es) pc xcp"
| τmoves2Tl:
  "τmoves2 P h stk es pc xcp ⟹ τmoves2 P h stk (e # es) (length (compE2 e) + pc) xcp"

inductive_cases τmove2_cases:
  "τmove2 P h stk (new C) pc xcp"
  "τmove2 P h stk (newA T⌊e⌉) pc xcp"
  "τmove2 P h stk (Cast T e) pc xcp"
  "τmove2 P h stk (e instanceof T) pc xcp"
  "τmove2 P h stk (Val v) pc xcp"
  "τmove2 P h stk (Var V) pc xcp"
  "τmove2 P h stk (e1«bop»e2) pc xcp"
  "τmove2 P h stk (V := e) pc xcp"
  "τmove2 P h stk (e1⌊e2⌉) pc xcp"
  "τmove2 P h stk (e1⌊e2⌉ := e3) pc xcp"
  "τmove2 P h stk (e1∙length) pc xcp"
  "τmove2 P h stk (e1∙F{D}) pc xcp"
  "τmove2 P h stk (e1∙F{D} := e3) pc xcp"
  "τmove2 P h stk (e1∙compareAndSwap(D∙F, e2, e3)) pc xcp"
  "τmove2 P h stk (e∙M(ps)) pc xcp"
  "τmove2 P h stk {V:T=vo; e} pc xcp"
  "τmove2 P h stk (sync⇘V⇙ (e1) e2) pc xcp"
  "τmove2 P h stk (e1;;e2) pc xcp"
  "τmove2 P h stk (if (e1) e2 else e3) pc xcp"
  "τmove2 P h stk (while (e1) e2) pc xcp"
  "τmove2 P h stk (try e1 catch(C V) e2) pc xcp"
  "τmove2 P h stk (throw e) pc xcp"

lemma τmoves2xcp: "pc < length (compEs2 es) ⟹ τmoves2 P h stk es pc ⌊xcp⌋"
proof(induct es arbitrary: pc)
  case Nil thus ?case by simp
next
  case (Cons e es)
  note IH = ‹⋀pc. pc < length (compEs2 es) ⟹ τmoves2 P h stk es pc ⌊xcp⌋›
  note pc = ‹pc < length (compEs2 (e # es))›
  show ?case
  proof(cases "pc < length (compE2 e)")
    case True
    thus ?thesis by(auto intro: τmoves2Hd τmove2xcp)
  next
    case False
    with pc IH[of "pc - length (compE2 e)"]
    have "τmoves2 P h stk es (pc - length (compE2 e)) ⌊xcp⌋" by(simp)
    hence "τmoves2 P h stk (e # es) (length (compE2 e) + (pc - length (compE2 e))) ⌊xcp⌋"
      by(rule τmoves2Tl)
    with False show ?thesis by simp
  qed
qed

lemma τmove2_intros':
  shows τmove2CastRed': "pc = length (compE2 e) ⟹ τmove2 P h stk (Cast T e) pc None"
  and τmove2InstanceOfRed': "pc = length (compE2 e) ⟹ τmove2 P h stk (e instanceof T) pc None"
  and τmove2BinOp2': "⟦ τmove2 P h stk e2 pc xcp; pc' = length (compE2 e1) + pc ⟧ ⟹ τmove2 P h stk (e1«bop»e2) pc' xcp"
  and τmove2BinOp': "pc = length (compE2 e1) + length (compE2 e2) ⟹ τmove2 P h stk (e1«bop»e2) pc None"
  and τmove2LAssRed1': "pc = length (compE2 e) ⟹ τmove2 P h stk (V:=e) pc None"
  and τmove2LAssRed2': "pc = Suc (length (compE2 e)) ⟹ τmove2 P h stk (V:=e) pc None"
  and τmove2AAcc2': "⟦ τmove2 P h stk i pc xcp; pc' = length (compE2 a) + pc ⟧ ⟹ τmove2 P h stk (a⌊i⌉) pc' xcp"
  and τmove2AAss2': "⟦ τmove2 P h stk i pc xcp; pc' = length (compE2 a) + pc ⟧ ⟹ τmove2 P h stk (a⌊i⌉ := e) pc' xcp"
  and τmove2AAss3': "⟦ τmove2 P h stk e pc xcp; pc' = length (compE2 a) + length (compE2 i) + pc ⟧ ⟹ τmove2 P h stk (a⌊i⌉ := e) pc' xcp"
  and τmove2AAssRed': "pc = Suc (length (compE2 a) + length (compE2 i) + length (compE2 e)) ⟹ τmove2 P h stk (a⌊i⌉ := e) pc None"
  and τmove2FAss2': "⟦ τmove2 P h stk e' pc xcp; pc' = length (compE2 e) + pc ⟧ ⟹ τmove2 P h stk (e∙F{D} := e') pc' xcp"
  and τmove2FAssRed': "pc = Suc (length (compE2 e) + length (compE2 e')) ⟹ τmove2 P h stk (e∙F{D} := e') pc None"
  and τmove2CAS2': "⟦ τmove2 P h stk e2 pc xcp; pc' = length (compE2 e1) + pc ⟧ ⟹ τmove2 P h stk (e1∙compareAndSwap(D∙F, e2, e3)) pc' xcp"
  and τmove2CAS3': "⟦ τmove2 P h stk e3 pc xcp; pc' = length (compE2 e1) + length (compE2 e2) + pc ⟧ ⟹ τmove2 P h stk (e1∙compareAndSwap(D∙F, e2, e3)) pc' xcp"
  and τmove2CallParams': "⟦ τmoves2 P h stk ps pc xcp; pc' = length (compE2 obj) + pc ⟧ ⟹ τmove2 P h stk (obj∙M(ps)) pc' xcp"
  and τmove2Call': "⟦ pc = length (compE2 obj) + length (compEs2 ps); length ps < length stk; 
                     stk ! length ps = Null ∨ 
                     (∀T Ts Tr D. typeof_addr h (the_Addr (stk ! length ps)) = ⌊T⌋ ⟶ P ⊢ class_type_of T sees M:Ts→Tr = Native in D ⟶ τexternal_defs D M) ⟧
                   ⟹ τmove2 P h stk (obj∙M(ps)) pc None"
  and τmove2BlockSome2: "pc = Suc 0 ⟹ τmove2 P h stk {V:T=⌊v⌋; e} pc None"
  and τmove2BlockSome': "⟦ τmove2 P h stk e pc xcp; pc' = Suc (Suc pc) ⟧ ⟹ τmove2 P h stk {V:T=⌊v⌋; e} pc' xcp"
  and τmove2Sync2': "pc = length (compE2 o') ⟹ τmove2 P h stk (sync⇘V⇙ (o') e) pc None"
  and τmove2Sync3': "pc = Suc (length (compE2 o')) ⟹ τmove2 P h stk (sync⇘V⇙ (o') e) pc None"
  and τmove2Sync4': "⟦ τmove2 P h stk e pc xcp; pc' = Suc (Suc (Suc (length (compE2 o') + pc))) ⟧ ⟹ τmove2 P h stk (sync⇘V⇙ (o') e) pc' xcp"
  and τmove2Sync5': "pc = Suc (Suc (Suc (length (compE2 o') + length (compE2 e)))) ⟹ τmove2 P h stk (sync⇘V⇙ (o') e) pc None"
  and τmove2Sync6': "pc = 5 + length (compE2 o') + length (compE2 e) ⟹ τmove2 P h stk (sync⇘V⇙ (o') e) pc None"
  and τmove2Sync7': "pc = 6 + length (compE2 o') + length (compE2 e) ⟹ τmove2 P h stk (sync⇘V⇙ (o') e) pc None"
  and τmove2Sync8': "pc = 8 + length (compE2 o') + length (compE2 e) ⟹ τmove2 P h stk (sync⇘V⇙ (o') e) pc None"
  and τmove2SeqRed': "pc = length (compE2 e) ⟹ τmove2 P h stk (e;;e') pc None"
  and τmove2Seq2': "⟦ τmove2 P h stk e' pc xcp; pc' = Suc (length (compE2 e) + pc) ⟧ ⟹ τmove2 P h stk (e;;e') pc' xcp"
  and τmove2CondRed': "pc = length (compE2 e) ⟹ τmove2 P h stk (if (e) e1 else e2) pc None"
  and τmove2CondThen': "⟦ τmove2 P h stk e1 pc xcp; pc' = Suc (length (compE2 e) + pc) ⟧ ⟹ τmove2 P h stk (if (e) e1 else e2) pc' xcp"
  and τmove2CondThenExit': "pc = Suc (length (compE2 e) + length (compE2 e1)) ⟹ τmove2 P h stk (if (e) e1 else e2) pc None"
  and τmove2CondElse': "⟦ τmove2 P h stk e2 pc xcp; pc' = Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)) ⟧ 
                        ⟹ τmove2 P h stk (if (e) e1 else e2) pc' xcp"
  and τmove2While2': "⟦ τmove2 P h stk e pc xcp; pc' = Suc (length (compE2 c) + pc) ⟧ ⟹ τmove2 P h stk (while (c) e) pc' xcp"
  and τmove2While3': "pc = Suc (Suc (length (compE2 c) + length (compE2 e))) ⟹ τmove2 P h stk (while (c) e) pc None"
  and τmove2While4': "pc = Suc (Suc (Suc (length (compE2 c) + length (compE2 e)))) ⟹ τmove2 P h stk (while (c) e) pc None"
  and τmove2While5': "pc = length (compE2 c) ⟹ τmove2 P h stk (while (c) e) pc None"
  and τmove2While6': "pc = Suc (length (compE2 c) + length (compE2 e)) ⟹ τmove2 P h stk (while (c) e) pc None"
  and τmove2Throw2': "pc = length (compE2 e) ⟹ τmove2 P h stk (throw e) pc None"
  and τmove2TryJump': "pc = length (compE2 e) ⟹ τmove2 P h stk (try e catch(C V) e') pc None"
  and τmove2TryCatch2': "pc = Suc (length (compE2 e)) ⟹ τmove2 P h stk (try e catch(C V) e') pc None"
  and τmove2Try2': "⟦ τmove2 P h stk {V:T=None; e'} pc xcp; pc' = Suc (Suc (length (compE2 e) + pc)) ⟧
                    ⟹ τmove2 P h stk (try e catch(C V) e') pc' xcp"
  and τmoves2Tl': "⟦ τmoves2 P h stk es pc xcp; pc' = length (compE2 e) + pc ⟧ ⟹ τmoves2 P h stk (e # es) pc' xcp"
apply(blast intro: τmove2_τmoves2.intros)+
done

lemma τmove2_iff: "τmove2 P h stk e pc xcp ⟷ pc < length (compE2 e) ∧ (xcp = None ⟶ τinstr P h stk (compE2 e ! pc))" (is "?lhs1 ⟷ ?rhs1")
  and τmoves2_iff: "τmoves2 P h stk es pc xcp ⟷ pc < length (compEs2 es) ∧ (xcp = None ⟶ τinstr P h stk (compEs2 es ! pc))" (is "?lhs2 ⟷ ?rhs2")
proof -
  have rhs1lhs1: "⟦ τinstr P h stk (compE2 e ! pc); pc < length (compE2 e) ⟧ ⟹ τmove2 P h stk e pc None"
    and rhs2lhs2: "⟦ τinstr P h stk (compEs2 es ! pc); pc < length (compEs2 es) ⟧ ⟹ τmoves2 P h stk es pc None"
    apply(induct e and es arbitrary: pc and pc rule: compE2.induct compEs2.induct)
    apply(force intro: τmove2_τmoves2.intros τmove2_intros' simp add: nth_append nth_Cons' not_less_eq split: if_split_asm)+
    done

  { assume "pc < length (compE2 e)" "xcp ≠ None"
    hence "τmove2 P h stk e pc xcp" by(auto intro: τmove2xcp) }
  with rhs1lhs1 have "?rhs1 ⟹ ?lhs1" by(cases xcp) auto
  moreover {
    assume "pc < length (compEs2 es)" "xcp ≠ None"
    hence "τmoves2 P h stk es pc xcp" by(auto intro: τmoves2xcp) }
  with rhs2lhs2 have "?rhs2 ⟹ ?lhs2" by(cases xcp) auto
  moreover have "?lhs1 ⟹ ?rhs1" and "?lhs2 ⟹ ?rhs2"
    by(induct rule: τmove2_τmoves2.inducts)(fastforce simp add: nth_append eval_nat_numeral)+
  ultimately show "?lhs1 ⟷ ?rhs1" "?lhs2 ⟷ ?rhs2" by blast+
qed

lemma τmove2_pc_length_compE2: "τmove2 P h stk e pc xcp ⟹ pc < length (compE2 e)"
  and τmoves2_pc_length_compEs2: "τmoves2 P h stk es pc xcp ⟹ pc < length (compEs2 es)"
by(simp_all add: τmove2_iff τmoves2_iff)

lemma τmove2_pc_length_compE2_conv: "pc ≥ length (compE2 e) ⟹ ¬ τmove2 P h stk e pc xcp"
by(auto dest: τmove2_pc_length_compE2)

lemma τmoves2_pc_length_compEs2_conv: "pc ≥ length (compEs2 es) ⟹ ¬ τmoves2 P h stk es pc xcp"
by(auto dest: τmoves2_pc_length_compEs2)

lemma τmoves2_append [elim]:
  "τmoves2 P h stk es pc xcp ⟹ τmoves2 P h stk (es @ es') pc xcp"
by(auto simp add: τmoves2_iff nth_append)

lemma append_τmoves2:
  "τmoves2 P h stk es pc xcp ⟹ τmoves2 P h stk (es' @ es) (length (compEs2 es') + pc) xcp"
by(simp add: τmoves2_iff)

lemma [dest]:
  shows τmove2_NewArrayD: "⟦ τmove2 P h stk (newA T⌊e⌉) pc xcp; pc < length (compE2 e) ⟧ ⟹ τmove2 P h stk e pc xcp"
  and τmove2_CastD: "⟦ τmove2 P h stk (Cast T e) pc xcp; pc < length (compE2 e) ⟧ ⟹ τmove2 P h stk e pc xcp"
  and τmove2_InstanceOfD: "⟦ τmove2 P h stk (e instanceof T) pc xcp; pc < length (compE2 e) ⟧ ⟹ τmove2 P h stk e pc xcp"
  and τmove2_BinOp1D: "⟦ τmove2 P h stk (e1 «bop» e2) pc' xcp'; pc' < length (compE2 e1) ⟧ ⟹ τmove2 P h stk e1 pc' xcp'"
  and τmove2_BinOp2D:
  "⟦ τmove2 P h stk (e1 «bop» e2) (length (compE2 e1) + pc') xcp'; pc' < length (compE2 e2) ⟧ ⟹ τmove2 P h stk e2 pc' xcp'"
  and τmove2_LAssD: "⟦ τmove2 P h stk (V := e) pc xcp; pc < length (compE2 e) ⟧ ⟹ τmove2 P h stk e pc xcp"
  and τmove2_AAccD1: "⟦ τmove2 P h stk (a⌊i⌉) pc xcp; pc < length (compE2 a) ⟧ ⟹ τmove2 P h stk a pc xcp"
  and τmove2_AAccD2: "⟦ τmove2 P h stk (a⌊i⌉) (length (compE2 a) + pc) xcp; pc < length (compE2 i) ⟧ ⟹ τmove2 P h stk i pc xcp"
  and τmove2_AAssD1: "⟦ τmove2 P h stk (a⌊i⌉ := e) pc xcp; pc < length (compE2 a) ⟧ ⟹ τmove2 P h stk a pc xcp"
  and τmove2_AAssD2: "⟦ τmove2 P h stk (a⌊i⌉ := e) (length (compE2 a) + pc) xcp; pc < length (compE2 i) ⟧ ⟹ τmove2 P h stk i pc xcp"
  and τmove2_AAssD3:
  "⟦ τmove2 P h stk (a⌊i⌉ := e) (length (compE2 a) + length (compE2 i) + pc) xcp; pc < length (compE2 e) ⟧ ⟹ τmove2 P h stk e pc xcp"
  and τmove2_ALengthD: "⟦ τmove2 P h stk (a∙length) pc xcp; pc < length (compE2 a) ⟧ ⟹ τmove2 P h stk a pc xcp"
  and τmove2_FAccD: "⟦ τmove2 P h stk (e∙F{D}) pc xcp; pc < length (compE2 e) ⟧ ⟹ τmove2 P h stk e pc xcp"
  and τmove2_FAssD1: "⟦ τmove2 P h stk (e∙F{D} := e') pc xcp; pc < length (compE2 e) ⟧ ⟹ τmove2 P h stk e pc xcp"
  and τmove2_FAssD2: "⟦ τmove2 P h stk (e∙F{D} := e') (length (compE2 e) + pc) xcp; pc < length (compE2 e') ⟧ ⟹ τmove2 P h stk e' pc xcp"
  and τmove2_CASD1: "⟦ τmove2 P h stk (e1∙compareAndSwap(D∙F, e2, e3)) pc xcp; pc < length (compE2 e1) ⟧ ⟹ τmove2 P h stk e1 pc xcp"
  and τmove2_CASD2: "⟦ τmove2 P h stk (e1∙compareAndSwap(D∙F, e2, e3)) (length (compE2 e1) + pc) xcp; pc < length (compE2 e2) ⟧ ⟹ τmove2 P h stk e2 pc xcp"
  and τmove2_CASD3:
  "⟦ τmove2 P h stk (e1∙compareAndSwap(D∙F, e2, e3)) (length (compE2 e1) + length (compE2 e2) + pc) xcp; pc < length (compE2 e3) ⟧ ⟹ τmove2 P h stk e3 pc xcp"
  and τmove2_CallObjD: "⟦ τmove2 P h stk (e∙M(es)) pc xcp; pc < length (compE2 e) ⟧ ⟹ τmove2 P h stk e pc xcp"
  and τmove2_BlockNoneD: "τmove2 P h stk {V:T=None; e} pc xcp ⟹ τmove2 P h stk e pc xcp"
  and τmove2_BlockSomeD: "τmove2 P h stk {V:T=⌊v⌋; e} (Suc (Suc pc)) xcp ⟹ τmove2 P h stk e pc xcp"
  and τmove2_sync1D: "⟦ τmove2 P h stk (sync⇘V⇙ (o') e) pc xcp; pc < length (compE2 o') ⟧ ⟹ τmove2 P h stk o' pc xcp"
  and τmove2_sync2D:
  "⟦ τmove2 P h stk (sync⇘V⇙ (o') e) (Suc (Suc (Suc (length (compE2 o') + pc)))) xcp; pc < length (compE2 e) ⟧ ⟹ τmove2 P h stk e pc xcp"
  and τmove2_Seq1D: "⟦ τmove2 P h stk (e1;; e2) pc xcp; pc < length (compE2 e1) ⟧ ⟹ τmove2 P h stk e1 pc xcp"
  and τmove2_Seq2D: "τmove2 P h stk (e1;; e2) (Suc (length (compE2 e1) + pc')) xcp' ⟹ τmove2 P h stk e2 pc' xcp'"
  and τmove2_IfCondD: "⟦ τmove2 P h stk (if (e) e1 else e2) pc xcp; pc < length (compE2 e) ⟧ ⟹ τmove2 P h stk e pc xcp"
  and τmove2_IfThenD:
  "⟦ τmove2 P h stk (if (e) e1 else e2) (Suc (length (compE2 e) + pc')) xcp'; pc' < length (compE2 e1) ⟧ ⟹ τmove2 P h stk e1 pc' xcp'"
  and τmove2_IfElseD:
  "τmove2 P h stk (if (e) e1 else e2) (Suc (Suc (length (compE2 e) + length (compE2 e1) + pc'))) xcp' ⟹ τmove2 P h stk e2 pc' xcp'"
  and τmove2_WhileCondD: "⟦ τmove2 P h stk (while (c) b) pc xcp; pc < length (compE2 c) ⟧ ⟹ τmove2 P h stk c pc xcp"
  and τmove2_ThrowD: "⟦ τmove2 P h stk (throw e) pc xcp; pc < length (compE2 e) ⟧ ⟹ τmove2 P h stk e pc xcp"
  and τmove2_Try1D: "⟦ τmove2 P h stk (try e1 catch(C' V) e2) pc xcp; pc < length (compE2 e1) ⟧ ⟹ τmove2 P h stk e1 pc xcp"
apply(auto elim!: τmove2_cases intro: τmove2xcp dest: τmove2_pc_length_compE2)
done

lemma τmove2_Invoke:
  "⟦τmove2 P h stk e pc None; compE2 e ! pc = Invoke M n ⟧
  ⟹ n < length stk ∧ (stk ! n = Null ∨ (∀T Ts Tr D. typeof_addr h (the_Addr (stk ! n)) = ⌊T⌋ ⟶ P ⊢ class_type_of T sees M:Ts→Tr = Native in D ⟶ τexternal_defs D M))"

  and τmoves2_Invoke: 
  "⟦τmoves2 P h stk es pc None; compEs2 es ! pc = Invoke M n ⟧ 
  ⟹ n < length stk ∧ (stk ! n = Null ∨ (∀T C Ts Tr D. typeof_addr h (the_Addr (stk ! n)) = ⌊T⌋ ⟶ P ⊢ class_type_of T sees M:Ts→Tr = Native in D ⟶ τexternal_defs D M))"
by(simp_all add: τmove2_iff τmoves2_iff split_beta)

lemmas τmove2_compE2_not_Invoke = τmove2_Invoke
lemmas τmoves2_compEs2_not_Invoke = τmoves2_Invoke

lemma τmove2_blocks1 [simp]:
  "τmove2 P h stk (blocks1 n Ts body) pc' xcp' = τmove2 P h stk body pc' xcp'"
by(simp add: τmove2_iff)

lemma τinstr_stk_append:
  "τinstr P h stk i ⟹ τinstr P h (stk @ vs) i"
by(cases i)(auto simp add: nth_append)

lemma τmove2_stk_append:
  "τmove2 P h stk e pc xcp ⟹ τmove2 P h (stk @ vs) e pc xcp"
by(simp add: τmove2_iff τinstr_stk_append)

lemma τmoves2_stk_append:
  "τmoves2 P h stk es pc xcp ⟹ τmoves2 P h (stk @ vs) es pc xcp"
by(simp add: τmoves2_iff τinstr_stk_append)

fun τMove2 :: "'addr jvm_prog ⇒ ('addr, 'heap) jvm_state ⇒ bool"
where 
  "τMove2 P (xcp, h, []) = False"
| "τMove2 P (xcp, h, (stk, loc, C, M, pc) # frs) =
       (let (_,_,_,meth) = method P C M; (_,_,ins,xt) = the meth
        in (pc < length ins ∧ (xcp = None ⟶ τinstr P h stk (ins ! pc))))"

lemma τMove2_iff:
  "τMove2 P σ = (let (xcp, h, frs) = σ
                 in case frs of [] ⇒ False
     | (stk, loc, C, M, pc) # frs' ⇒ 
       (let (_,_,_,meth) = method P C M; (_,_,ins,xt) = the meth
        in (pc < length ins ∧ (xcp = None ⟶ τinstr P h stk (ins ! pc)))))"
by(cases σ)(clarsimp split: list.splits simp add: fun_eq_iff split_beta)

lemma τinstr_compP [simp]: "τinstr (compP f P) h stk i ⟷ τinstr P h stk i"
by(cases i) auto

lemma [simp]: fixes e :: "'addr expr1" and es :: "'addr expr1 list"
  shows τmove2_compP: "τmove2 (compP f P) h stk e = τmove2 P h stk e"
  and τmoves2_compP: "τmoves2 (compP f P) h stk es = τmoves2 P h stk es"
by(auto simp add: τmove2_iff τmoves2_iff fun_eq_iff)

lemma τMove2_compP2:
  "P ⊢ C sees M:Ts→T=⌊body⌋ in D ⟹ 
   τMove2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs) =
   (case xcp of None ⇒ τmove2 P h stk body pc xcp ∨ pc = length (compE2 body) | Some a ⇒ pc < Suc (length (compE2 body)))"
by(clarsimp simp add: τmove2_iff compP2_def compMb2_def nth_append nth_Cons' split: option.splits if_split_asm)

abbreviation τMOVE2 ::
  "'addr jvm_prog ⇒ (('addr option × 'addr frame list) × 'heap, ('addr, 'thread_id, 'heap) jvm_thread_action) trsys"
where "τMOVE2 P ≡ λ((xcp, frs), h) ta s. τMove2 P (xcp, h, frs) ∧ ta = ε"

lemma τjvmd_heap_unchanged: 
  "⟦ P,t ⊢ Normal (xcp, h, frs) -ε-jvmd→ Normal (xcp', h', frs'); τMove2 P (xcp, h, frs) ⟧
  ⟹ h = h'"
apply(erule jvmd_NormalE)
apply(clarsimp)
apply(cases xcp)
 apply(rename_tac stk loc C M pc FRS M' Ts T meth mxs mxl ins xt)
 apply(case_tac "ins ! pc")
 prefer 19 ― ‹BinOpInstr›
 apply(rename_tac bop)
 apply(case_tac "the (binop bop (hd (tl stk)) (hd stk))")
 apply(auto simp add: split_beta τexternal_def split: if_split_asm)
apply(fastforce simp add: check_def has_method_def τexternal_def dest: τexternal_red_external_aggr_heap_unchanged)
done

lemma mexecd_τmthr_wf:
  "τmultithreaded_wf JVM_final (mexecd P) (τMOVE2 P)"
proof
  fix t x h ta x' h'
  assume "mexecd P t (x, h) ta (x', h')"
    and "τMOVE2 P (x, h) ta (x', h')"
  thus "h = h'"
    by(cases x)(cases x', auto dest: τjvmd_heap_unchanged)
next
  fix s ta s'
  assume "τMOVE2 P s ta s'" thus "ta = ε" by(simp add: split_beta)
qed

end

sublocale JVM_heap_base < execd_mthr: 
  τmultithreaded_wf 
    JVM_final
    "mexecd P"
    convert_RA
    "τMOVE2 P"
  for P
by(rule mexecd_τmthr_wf)

context JVM_heap_base begin

lemma τexec_1_taD:
  assumes exec: "exec_1_d P t (Normal (xcp, h, frs)) ta (Normal (xcp', h', frs'))"
  and τ: "τMove2 P (xcp, h, frs)"
  shows "ta = ε"
using assms
apply(auto elim!: jvmd_NormalE simp add: split_beta)
apply(cases xcp)
apply auto
apply(rename_tac stk loc C M pc FRS)
apply(case_tac "instrs_of P C M ! pc")
apply(simp_all split: if_split_asm)
apply(auto simp add: check_def has_method_def τexternal_def dest!: τexternal_red_external_aggr_TA_empty)
done

end

end