Theory J1JVMBisim

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

section ‹The delay bisimulation between intermediate language and JVM›

theory J1JVMBisim imports 
  Execs
  "../BV/BVNoTypeError"
  J1
begin

declare Listn.lesub_list_impl_same_size[simp del]

lemma (in JVM_heap_conf_base') τexec_1_τexec_1_d:
  "⟦ wf_jvm_prog⇘Φ⇙ P; τexec_1 P t σ σ'; Φ |- t:σ [ok] ⟧ ⟹ τexec_1_d P t σ σ'"
by(auto simp add: τexec_1_def τexec_1_d_def welltyped_commute[symmetric] elim: jvmd_NormalE)

context JVM_conf_read begin

lemma τExec_1r_preserves_correct_state:
  assumes wf: "wf_jvm_prog⇘Φ⇙ P"
  and exec: "τExec_1r P t σ σ'"
  shows "Φ |- t:σ [ok] ⟹ Φ |- t:σ' [ok]"
using exec
by(induct)(blast intro: BV_correct_1[OF wf])+

lemma τExec_1t_preserves_correct_state:
  assumes wf: "wf_jvm_prog⇘Φ⇙ P"
  and exec: "τExec_1t P t σ σ'"
  shows "Φ |- t:σ [ok] ⟹ Φ |- t:σ' [ok]"
using exec
by(induct)(blast intro: BV_correct_1[OF wf])+

lemma τExec_1r_τExec_1_dr:
  assumes wf: "wf_jvm_prog⇘Φ⇙ P"
  shows "⟦ τExec_1r P t σ σ'; Φ |- t:σ [ok] ⟧ ⟹ τExec_1_dr P t σ σ'"
apply(induct rule: rtranclp_induct)
apply(blast intro: rtranclp.rtrancl_into_rtrancl τexec_1_τexec_1_d[OF wf] τExec_1r_preserves_correct_state[OF wf])+
done

lemma τExec_1t_τExec_1_dt:
  assumes wf: "wf_jvm_prog⇘Φ⇙ P"
  shows "⟦ τExec_1t P t σ σ'; Φ |- t:σ [ok] ⟧ ⟹ τExec_1_dt P t σ σ'"
apply(induct rule: tranclp_induct)
apply(blast intro: tranclp.trancl_into_trancl τexec_1_τexec_1_d[OF wf] τExec_1t_preserves_correct_state[OF wf])+
done

lemma τExec_1_dr_preserves_correct_state:
  assumes wf: "wf_jvm_prog⇘Φ⇙ P"
  and exec: "τExec_1_dr P t σ σ'"
  shows "Φ |- t: σ [ok] ⟹ Φ |- t: σ' [ok]"
using exec
by(induct)(blast intro: BV_correct_1[OF wf])+

lemma τExec_1_dt_preserves_correct_state:
  assumes wf: "wf_jvm_prog⇘Φ⇙ P"
  and exec: "τExec_1_dt P t σ σ'"
  shows "Φ |- t:σ [ok] ⟹ Φ |- t:σ' [ok]"
using exec
by(induct)(blast intro: BV_correct_1[OF wf])+

end

locale J1_JVM_heap_base =
  J1_heap_base +
  JVM_heap_base +
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
  and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
  and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
  and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
begin

inductive bisim1 ::
  "'m prog ⇒ 'heap ⇒ 'addr expr1 ⇒ ('addr expr1 × 'addr locals1)
  ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"

  and bisims1 :: 
  "'m prog ⇒ 'heap ⇒ 'addr expr1 list ⇒ ('addr expr1 list × 'addr locals1)
  ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"
  
  and bisim1_syntax :: 
  "'m prog ⇒ 'addr expr1 ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1)
  ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"
  ("_,_,_ ⊢ _ ↔ _" [50, 0, 0, 0, 50] 100)

  and bisims1_syntax :: 
  "'m prog ⇒ 'addr expr1 list ⇒ 'heap ⇒ ('addr expr1 list × 'addr locals1)
  ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"
  ("_,_,_ ⊢ _ [↔] _" [50, 0, 0, 0, 50] 100)
  for P :: "'m prog" and  h :: 'heap
where
  "P, e, h ⊢ exs ↔ s ≡ bisim1 P h e exs s"
| "P, es, h ⊢ esxs [↔] s ≡ bisims1 P h es esxs s"

| bisim1Val2:
  "pc = length (compE2 e) ⟹ P, e, h ⊢ (Val v, xs) ↔ (v # [], xs, pc, None)"

| bisim1New:
  "P, new C, h ⊢ (new C, xs) ↔ ([], xs, 0, None)"

| bisim1NewThrow:
  "P, new C, h ⊢ (THROW OutOfMemory, xs) ↔ ([], xs, 0, ⌊addr_of_sys_xcpt OutOfMemory⌋)"


| bisim1NewArray:
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp) ⟹ P, newA T⌊e⌉, h ⊢ (newA T⌊e'⌉, xs) ↔ (stk, loc, pc, xcp)"

| bisim1NewArrayThrow:
  "P, e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋) ⟹ P, newA T⌊e⌉, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"

| bisim1NewArrayFail:
  "P, newA T⌊e⌉, h ⊢ (Throw a, xs) ↔ ([v], xs, length (compE2 e), ⌊a⌋)"


| bisim1Cast:
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp) ⟹ P, Cast T e, h ⊢ (Cast T e', xs) ↔ (stk, loc, pc, xcp)"

| bisim1CastThrow:
  "P, e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋) ⟹ P, Cast T e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"

| bisim1CastFail:
  "P, Cast T e, h ⊢ (THROW ClassCast, xs) ↔ ([v], xs, length (compE2 e), ⌊addr_of_sys_xcpt ClassCast⌋)"


| bisim1InstanceOf:
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp) ⟹ P, e instanceof T, h ⊢ (e' instanceof T, xs) ↔ (stk, loc, pc, xcp)"

| bisim1InstanceOfThrow:
  "P, e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋) ⟹ P, e instanceof T, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"


| bisim1Val: "P, Val v, h ⊢ (Val v, xs) ↔ ([], xs, 0, None)"

| bisim1Var: "P, Var V, h ⊢ (Var V, xs) ↔ ([], xs, 0, None)"


| bisim1BinOp1:
  "P, e1, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp) ⟹ P, e1«bop»e2, h ⊢ (e'«bop»e2, xs) ↔ (stk, loc, pc, xcp)"

| bisim1BinOp2:
  "P, e2, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, e1«bop»e2, h ⊢ (Val v1 «bop» e', xs) ↔ (stk @ [v1], loc, length (compE2 e1) + pc, xcp)"

| bisim1BinOpThrow1:
  "P, e1, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
  ⟹ P, e1«bop»e2, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"

| bisim1BinOpThrow2:
  "P, e2, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
  ⟹ P, e1«bop»e2, h ⊢ (Throw a, xs) ↔ (stk @ [v1], loc, length (compE2 e1) + pc, ⌊a⌋)"

| bisim1BinOpThrow:
  "P, e1«bop»e2, h ⊢ (Throw a, xs) ↔ ([v1, v2], xs, length (compE2 e1) + length (compE2 e2), ⌊a⌋)"

| bisim1LAss1:
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp) ⟹ P, V:=e, h ⊢ (V:=e', xs) ↔ (stk, loc, pc, xcp)"

| bisim1LAss2:
  "P, V:=e, h ⊢ (unit, xs) ↔ ([], xs, Suc (length (compE2 e)), None)"

| bisim1LAssThrow:
  "P, e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋) ⟹ P, V:=e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"

| bisim1AAcc1:
  "P, a, h ⊢ (a', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, a⌊i⌉, h ⊢ (a'⌊i⌉, xs) ↔ (stk, loc, pc, xcp)"

| bisim1AAcc2:
  "P, i, h ⊢ (i', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, a⌊i⌉, h ⊢ (Val v⌊i'⌉, xs) ↔ (stk @ [v], loc, length (compE2 a) + pc, xcp)"

| bisim1AAccThrow1:
  "P, a, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, a⌊i⌉, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)"

| bisim1AAccThrow2:
  "P, i, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, a⌊i⌉, h ⊢ (Throw ad, xs) ↔ (stk @ [v], loc, length (compE2 a) + pc, ⌊ad⌋)"

| bisim1AAccFail:
  "P, a⌊i⌉, h ⊢ (Throw ad, xs) ↔ ([v, v'], xs, length (compE2 a) + length (compE2 i), ⌊ad⌋)"


| bisim1AAss1:
  "P, a, h ⊢ (a', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, a⌊i⌉ := e, h ⊢ (a'⌊i⌉ := e, xs) ↔ (stk, loc, pc, xcp)"

| bisim1AAss2:
  "P, i, h ⊢ (i', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, a⌊i⌉ := e, h ⊢ (Val v⌊i'⌉ := e, xs) ↔ (stk @ [v], loc, length (compE2 a) + pc, xcp)"

| bisim1AAss3:
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, a⌊i⌉ := e, h ⊢ (Val v⌊Val v'⌉ := e', xs) ↔ (stk @ [v', v], loc, length (compE2 a) + length (compE2 i) + pc, xcp)"

| bisim1AAssThrow1:
  "P, a, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, a⌊i⌉ := e, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)"

| bisim1AAssThrow2:
  "P, i, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, a⌊i⌉ := e, h ⊢ (Throw ad, xs) ↔ (stk @ [v], loc, length (compE2 a) + pc, ⌊ad⌋)"

| bisim1AAssThrow3:
  "P, e, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, a⌊i⌉ := e, h ⊢ (Throw ad, xs) ↔ (stk @ [v', v], loc, length (compE2 a) + length (compE2 i) + pc, ⌊ad⌋)"

| bisim1AAssFail:
  "P, a⌊i⌉ := e, h ⊢ (Throw ad, xs) ↔ ([v', v, v''], xs, length (compE2 a) + length (compE2 i) + length (compE2 e), ⌊ad⌋)"

| bisim1AAss4:
  "P, a⌊i⌉ := e, h ⊢ (unit, xs) ↔ ([], xs, Suc (length (compE2 a) + length (compE2 i) + length (compE2 e)), None)"


| bisim1ALength: 
  "P, a, h ⊢ (a', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, a∙length, h ⊢ (a'∙length, xs) ↔ (stk, loc, pc, xcp)"

| bisim1ALengthThrow:
  "P, a, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, a∙length, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)"


| bisim1ALengthNull:
  "P, a∙length, h ⊢ (THROW NullPointer, xs) ↔ ([Null], xs, length (compE2 a), ⌊addr_of_sys_xcpt NullPointer⌋)"


| bisim1FAcc: 
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, e∙F{D}, h ⊢ (e'∙F{D}, xs) ↔ (stk, loc, pc, xcp)"

| bisim1FAccThrow:
  "P, e, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, e∙F{D}, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)"

| bisim1FAccNull:
  "P, e∙F{D}, h ⊢ (THROW NullPointer, xs) ↔ ([Null], xs, length (compE2 e), ⌊addr_of_sys_xcpt NullPointer⌋)"


| bisim1FAss1: 
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, e∙F{D} := e2, h ⊢ (e'∙F{D} := e2, xs) ↔ (stk, loc, pc, xcp)"

| bisim1FAss2: 
  "P, e2, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, e∙F{D} := e2, h ⊢ (Val v∙F{D} := e', xs) ↔ (stk @ [v], loc, length (compE2 e) + pc, xcp)"

| bisim1FAssThrow1:
  "P, e, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, e∙F{D} := e2, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)"

| bisim1FAssThrow2:
  "P, e2, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, e∙F{D} := e2, h ⊢ (Throw ad, xs) ↔ (stk @ [v], loc, length (compE2 e) + pc, ⌊ad⌋)"

| bisim1FAssNull:
  "P, e∙F{D} := e2, h ⊢ (THROW NullPointer, xs) ↔ ([v, Null], xs, length (compE2 e) + length (compE2 e2), ⌊addr_of_sys_xcpt NullPointer⌋)"

| bisim1FAss3:
  "P, e∙F{D} := e2, h ⊢ (unit, xs) ↔ ([], xs, Suc (length (compE2 e) + length (compE2 e2)), None)"


| bisim1CAS1:
  "P, e1, h ⊢ (e1', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, e1∙compareAndSwap(D∙F, e2, e3), h ⊢ (e1'∙compareAndSwap(D∙F, e2, e3), xs) ↔ (stk, loc, pc, xcp)"

| bisim1CAS2:
  "P, e2, h ⊢ (e2', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, e1∙compareAndSwap(D∙F, e2, e3), h ⊢ (Val v∙compareAndSwap(D∙F, e2', e3), xs) ↔ (stk @ [v], loc, length (compE2 e1) + pc, xcp)"

| bisim1CAS3:
  "P, e3, h ⊢ (e3', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, e1∙compareAndSwap(D∙F, e2, e3), h ⊢ (Val v∙compareAndSwap(D∙F, Val v', e3'), xs) ↔ (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp)"

| bisim1CASThrow1:
  "P, e1, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, e1∙compareAndSwap(D∙F, e2, e3), h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)"

| bisim1CASThrow2:
  "P, e2, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, e1∙compareAndSwap(D∙F, e2, e3), h ⊢ (Throw ad, xs) ↔ (stk @ [v], loc, length (compE2 e1) + pc, ⌊ad⌋)"

| bisim1CASThrow3:
  "P, e3, h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, e1∙compareAndSwap(D∙F, e2, e3), h ⊢ (Throw ad, xs) ↔ (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, ⌊ad⌋)"

| bisim1CASFail:
  "P, e1∙compareAndSwap(D∙F, e2, e3), h ⊢ (Throw ad, xs) ↔ ([v', v, v''], xs, length (compE2 e1) + length (compE2 e2) + length (compE2 e3), ⌊ad⌋)"


| bisim1Call1:
  "P, obj, h ⊢ (obj', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, obj∙M(ps), h ⊢ (obj'∙M(ps), xs) ↔ (stk, loc, pc, xcp)"

| bisim1CallParams:
  "P, ps, h ⊢ (ps', xs) [↔] (stk, loc, pc, xcp)
  ⟹ P, obj∙M(ps), h ⊢ (Val v∙M(ps'), xs) ↔ (stk @ [v], loc, length (compE2 obj) +  pc, xcp)"

| bisim1CallThrowObj:
  "P, obj, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
  ⟹ P, obj∙M(ps), h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"

| bisim1CallThrowParams:
  "P, ps, h ⊢ (map Val vs @ Throw a # ps', xs) [↔] (stk, loc, pc, ⌊a⌋)
  ⟹ P, obj∙M(ps), h ⊢ (Throw a, xs) ↔ (stk @ [v], loc, length (compE2 obj) + pc, ⌊a⌋)"

| bisim1CallThrow:
  "length ps = length vs
  ⟹ P, obj∙M(ps), h ⊢ (Throw a, xs) ↔ (vs @ [v], xs, length (compE2 obj) + length (compEs2 ps), ⌊a⌋)"

| bisim1BlockSome1:
  "P, {V:T=⌊v⌋; e}, h ⊢ ({V:T=⌊v⌋; e}, xs) ↔ ([], xs, 0, None)"

| bisim1BlockSome2:
  "P, {V:T=⌊v⌋; e}, h ⊢ ({V:T=⌊v⌋; e}, xs) ↔ ([v], xs, Suc 0, None)"

| bisim1BlockSome4:
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, {V:T=⌊v⌋; e}, h ⊢ ({V:T=None; e'}, xs) ↔ (stk, loc, Suc (Suc pc), xcp)"

| bisim1BlockThrowSome:
  "P, e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
  ⟹ P, {V:T=⌊v⌋; e}, h ⊢ (Throw a, xs) ↔ (stk, loc, Suc (Suc pc), ⌊a⌋)"

| bisim1BlockNone:
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, {V:T=None; e}, h ⊢ ({V:T=None; e'}, xs) ↔ (stk, loc, pc, xcp)"

| bisim1BlockThrowNone:
  "P, e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
   ⟹ P, {V:T=None; e}, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"


| bisim1Sync1:
  "P, e1, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, sync⇘V⇙ (e1) e2, h ⊢ (sync⇘V⇙ (e') e2, xs) ↔ (stk, loc, pc, xcp)"

| bisim1Sync2:
  "P, sync⇘V⇙ (e1) e2, h ⊢ (sync⇘V⇙ (Val v) e2, xs) ↔ ([v, v], xs, Suc (length (compE2 e1)), None)"

| bisim1Sync3:
  "P, sync⇘V⇙ (e1) e2, h ⊢ (sync⇘V⇙ (Val v) e2, xs) ↔ ([v], xs[V := v], Suc (Suc (length (compE2 e1))), None)"

| bisim1Sync4:
  "P, e2, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, sync⇘V⇙ (e1) e2, h ⊢ (insync⇘V⇙ (a) e', xs) ↔ (stk, loc, Suc (Suc (Suc (length (compE2 e1) + pc))), xcp)"

| bisim1Sync5:
  "P, sync⇘V⇙ (e1) e2, h ⊢ (insync⇘V⇙ (a) Val v, xs) ↔ ([xs ! V, v], xs, 4 + length (compE2 e1) + length (compE2 e2), None)"

| bisim1Sync6:
  "P, sync⇘V⇙ (e1) e2, h ⊢ (Val v, xs) ↔ ([v], xs, 5 + length (compE2 e1) + length (compE2 e2), None)"

| bisim1Sync7:
  "P, sync⇘V⇙ (e1) e2, h ⊢ (insync⇘V⇙ (a) Throw a', xs) ↔ ([Addr a'], xs, 6 + length (compE2 e1) + length (compE2 e2), None)"

| bisim1Sync8:
  "P, sync⇘V⇙ (e1) e2, h ⊢ (insync⇘V⇙ (a) Throw a', xs) ↔
                         ([xs ! V, Addr a'], xs, 7 + length (compE2 e1) + length (compE2 e2), None)"

| bisim1Sync9:
  "P, sync⇘V⇙ (e1) e2, h ⊢ (Throw a, xs) ↔ ([Addr a], xs, 8 + length (compE2 e1) + length (compE2 e2), None)"

| bisim1Sync10:
  "P, sync⇘V⇙ (e1) e2, h ⊢ (Throw a, xs) ↔ ([Addr a], xs, 8 + length (compE2 e1) + length (compE2 e2), ⌊a⌋)"

| bisim1Sync11:
  "P, sync⇘V⇙ (e1) e2, h ⊢ (THROW NullPointer, xs) ↔ ([Null], xs, Suc (Suc (length (compE2 e1))), ⌊addr_of_sys_xcpt NullPointer⌋)"

| bisim1Sync12:
  "P, sync⇘V⇙ (e1) e2, h ⊢ (Throw a, xs) ↔ ([v, v'], xs, 4 + length (compE2 e1) + length (compE2 e2), ⌊a⌋)"

| bisim1Sync14:
  "P, sync⇘V⇙ (e1) e2, h ⊢ (Throw a, xs) ↔
        ([v, Addr a'], xs, 7 + length (compE2 e1) + length (compE2 e2), ⌊a⌋)"

| bisim1SyncThrow:
  "P, e1, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
  ⟹ P, sync⇘V⇙ (e1) e2, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"


| bisim1InSync: ― ‹This rule only exists such that @{text "P,e,h ⊢ (e, xs) ↔ ([], xs, 0, None)"} holds for all @{text "e"}› 
  "P, insync⇘V⇙ (a) e, h ⊢ (insync⇘V⇙ (a) e, xs) ↔ ([], xs, 0, None)"


| bisim1Seq1:
  "P, e1, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp) ⟹ P, e1;;e2, h ⊢ (e';;e2, xs) ↔ (stk, loc, pc, xcp)"

| bisim1SeqThrow1:
  "P, e1, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋) ⟹ P, e1;;e2, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"

| bisim1Seq2:
  "P, e2, h ⊢ exs ↔ (stk, loc, pc, xcp)
  ⟹ P, e1;;e2, h ⊢ exs ↔ (stk, loc, Suc (length (compE2 e1) + pc), xcp)"


| bisim1Cond1:
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, if (e) e1 else e2, h ⊢ (if (e') e1 else e2, xs) ↔ (stk, loc, pc, xcp)"

| bisim1CondThen:
  "P, e1, h ⊢ exs ↔ (stk, loc, pc, xcp)
  ⟹ P, if (e) e1 else e2, h ⊢ exs ↔ (stk, loc, Suc (length (compE2 e) + pc), xcp)"

| bisim1CondElse:
  "P, e2, h ⊢ exs ↔ (stk, loc, pc, xcp)
  ⟹ P, if (e) e1 else e2, h ⊢ exs ↔ (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) +  pc)), xcp)"

| bisim1CondThrow:
  "P, e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
  ⟹ P, if (e) e1 else e2, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"


| bisim1While1:
  "P, while (c) e, h ⊢ (while (c) e, xs) ↔ ([], xs, 0, None)"

| bisim1While3:
  "P, c, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, while (c) e, h ⊢ (if (e') (e;; while (c) e) else unit, xs) ↔ (stk, loc, pc, xcp)"

| bisim1While4:
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, while (c) e, h  ⊢ (e';; while (c) e, xs) ↔ (stk, loc, Suc (length (compE2 c) + pc), xcp)"

| bisim1While6:
  "P, while (c) e, h ⊢ (while (c) e, xs) ↔ ([], xs, Suc (Suc (length (compE2 c) + length (compE2 e))), None)"

| bisim1While7:
  "P, while (c) e, h ⊢ (unit, xs) ↔ ([], xs, Suc (Suc (Suc (length (compE2 c) + length (compE2 e)))), None)"

| bisim1WhileThrow1:
  "P, c, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
  ⟹ P, while (c) e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"

| bisim1WhileThrow2:
  "P, e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
   ⟹ P, while (c) e, h ⊢ (Throw a, xs) ↔ (stk, loc, Suc (length (compE2 c) + pc), ⌊a⌋)"


| bisim1Throw1:
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp) ⟹ P, throw e, h ⊢ (throw e', xs) ↔ (stk, loc, pc, xcp)"

| bisim1Throw2:
  "P, throw e, h ⊢ (Throw a, xs) ↔ ([Addr a], xs, length (compE2 e), ⌊a⌋)"

| bisim1ThrowNull:
  "P, throw e, h ⊢ (THROW NullPointer, xs) ↔ ([Null], xs, length (compE2 e), ⌊addr_of_sys_xcpt NullPointer⌋)"

| bisim1ThrowThrow:
  "P, e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋) ⟹ P, throw e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"


| bisim1Try:
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
   ⟹ P, try e catch(C V) e2, h ⊢ (try e' catch(C V) e2, xs) ↔ (stk, loc, pc, xcp)"

| bisim1TryCatch1:
  "⟦ P, e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋); typeof_addr h a = ⌊Class_type C'⌋; P ⊢ C' ≼⇧* C ⟧
  ⟹ P, try e catch(C V) e2, h ⊢ ({V:Class C=None; e2}, xs[V := Addr a]) ↔ ([Addr a], loc, Suc (length (compE2 e)), None)"

| bisim1TryCatch2:
  "P, e2, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)
   ⟹ P, try e catch(C V) e2, h ⊢ ({V:Class C=None; e'}, xs) ↔ (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp)"

| bisim1TryFail:
  "⟦ P, e, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋); typeof_addr h a = ⌊Class_type C'⌋; ¬ P ⊢ C' ≼⇧* C ⟧ 
  ⟹ P, try e catch(C V) e2, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"

| bisim1TryCatchThrow:
  "P, e2, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
   ⟹ P, try e catch(C V) e2, h ⊢ (Throw a, xs) ↔ (stk, loc, Suc (Suc (length (compE2 e) + pc)), ⌊a⌋)"

| bisims1Nil: "P, [], h ⊢ ([], xs) [↔] ([], xs, 0, None)"

| bisims1List1:
  "P, e, h ⊢ (e', xs) ↔ (stk, loc, pc, xcp) ⟹ P, e#es, h ⊢ (e'#es, xs) [↔] (stk, loc, pc, xcp)"

| bisims1List2:
  "P, es, h ⊢ (es', xs) [↔] (stk, loc, pc, xcp)
  ⟹ P, e#es, h ⊢ (Val v # es', xs) [↔] (stk @ [v], loc, length (compE2 e) + pc, xcp)"


inductive_cases bisim1_cases:
  "P,e,h ⊢ (Val v, xs) ↔ (stk, loc, pc, xcp)"


lemma bisim1_refl: "P,e,h ⊢ (e, xs) ↔ ([], xs, 0, None)"
  and bisims1_refl: "P,es,h ⊢ (es, xs) [↔] ([], xs, 0, None)"
apply(induct e and es rule: call.induct calls.induct)
apply(auto intro: bisim1_bisims1.intros simp add: nat_fun_sum_eq_conv)
apply(rename_tac option a)
apply(case_tac option)
apply(auto intro: bisim1_bisims1.intros split: if_split_asm)
done

lemma bisims1_lengthD: "P, es, h ⊢ (es', xs) [↔] s ⟹ length es = length es'"
apply(induct es arbitrary: es' s)
apply(auto elim: bisims1.cases)
done

text ‹
  Derive an alternative induction rule for @{term bisim1} such that
  (i) induction hypothesis are generated for all subexpressions and
  (ii) the number of surrounding blocks is passed through.
›

inductive bisim1' :: 
  "'m prog ⇒ 'heap ⇒ 'addr expr1 ⇒ nat ⇒ ('addr expr1 × 'addr locals1) 
  ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"

  and bisims1' :: 
  "'m prog ⇒ 'heap ⇒ 'addr expr1 list ⇒ nat ⇒ ('addr expr1 list × 'addr locals1)
  ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"

  and bisim1'_syntax :: 
  "'m prog ⇒ 'addr expr1 ⇒ nat ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) 
  ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"
  ("_,_,_,_ ⊢'' _ ↔ _" [50, 0, 0, 0, 0, 50] 100)

  and bisims1'_syntax :: 
  "'m prog ⇒ 'addr expr1 list ⇒ nat ⇒ 'heap ⇒ ('addr expr1 list × 'addr val list) 
  ⇒ ('addr val list × 'addr val list × pc × 'addr option) ⇒ bool"
  ("_,_,_,_ ⊢'' _ [↔] _" [50, 0, 0, 0, 0, 50] 100)
  for P :: "'m prog" and  h :: 'heap
where
  "P, e, n, h ⊢' exs ↔ s ≡ bisim1' P h e n exs s"
| "P, es, n, h ⊢' esxs [↔] s ≡ bisims1' P h es n esxs s"

| bisim1Val2':
  "P, e, n, h ⊢' (Val v, xs) ↔ (v # [], xs, length (compE2 e), None)"

| bisim1New':
  "P, new C, n, h ⊢' (new C, xs) ↔ ([], xs, 0, None)"

| bisim1NewThrow':
  "P, new C, n, h ⊢' (THROW OutOfMemory, xs) ↔ ([], xs, 0, ⌊addr_of_sys_xcpt OutOfMemory⌋)"


| bisim1NewArray':
  "P, e, n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, newA T⌊e⌉, n, h ⊢' (newA T⌊e'⌉, xs) ↔ (stk, loc, pc, xcp)"

| bisim1NewArrayThrow':
  "P, e, n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
  ⟹ P, newA T⌊e⌉, n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"

| bisim1NewArrayFail':
  "(⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None))
  ⟹ P, newA T⌊e⌉, n, h ⊢' (Throw a, xs) ↔ ([v], xs, length (compE2 e), ⌊a⌋)"


| bisim1Cast':
  "P, e, n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, Cast T e, n, h ⊢' (Cast T e', xs) ↔ (stk, loc, pc, xcp)"

| bisim1CastThrow':
  "P, e, n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
  ⟹ P, Cast T e, n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"

| bisim1CastFail':
  "(⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None))
  ⟹ P, Cast T e, n, h ⊢' (THROW ClassCast, xs) ↔ ([v], xs, length (compE2 e), ⌊addr_of_sys_xcpt ClassCast⌋)"


| bisim1InstanceOf':
  "P, e, n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, e instanceof T, n, h ⊢' (e' instanceof T, xs) ↔ (stk, loc, pc, xcp)"

| bisim1InstanceOfThrow':
  "P, e, n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
  ⟹ P, e instanceof T, n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"


| bisim1Val': "P, Val v, n, h ⊢' (Val v, xs) ↔ ([], xs, 0, None)"

| bisim1Var': "P, Var V, n, h ⊢' (Var V, xs) ↔ ([], xs, 0, None)"


| bisim1BinOp1':
  "⟦ P, e1, n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp);
     ⋀xs. P, e2, n, h ⊢' (e2, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e1«bop»e2, n, h ⊢' (e'«bop»e2, xs) ↔ (stk, loc, pc, xcp)"

| bisim1BinOp2':
  "⟦ P, e2, n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp);
     ⋀xs. P, e1, n, h ⊢' (e1, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e1«bop»e2, n, h ⊢' (Val v1 «bop» e', xs) ↔ (stk @ [v1], loc, length (compE2 e1) + pc, xcp)"

| bisim1BinOpThrow1':
  "⟦ P, e1, n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋);
     ⋀xs. P, e2, n, h ⊢' (e2, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e1«bop»e2, n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"

| bisim1BinOpThrow2':
  "⟦ P, e2, n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋);
     ⋀xs. P, e1, n, h ⊢' (e1, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e1«bop»e2, n, h ⊢' (Throw a, xs) ↔ (stk @ [v1], loc, length (compE2 e1) + pc, ⌊a⌋)"

| bisim1BinOpThrow':
  "⟦ ⋀xs. P, e1, n, h ⊢' (e1, xs) ↔ ([], xs, 0, None); 
     ⋀xs. P, e2, n, h ⊢' (e2, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e1«bop»e2, n, h ⊢' (Throw a, xs) ↔ ([v1, v2], xs, length (compE2 e1) + length (compE2 e2), ⌊a⌋)"

| bisim1LAss1':
  "P, e, n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, V:=e, n, h ⊢' (V:=e', xs) ↔ (stk, loc, pc, xcp)"

| bisim1LAss2':
  "(⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None))
   ⟹ P, V:=e, n, h ⊢' (unit, xs) ↔ ([], xs, Suc (length (compE2 e)), None)"

| bisim1LAssThrow':
  "P, e, n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
  ⟹ P, V:=e, n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"


| bisim1AAcc1':
  "⟦ P, a, n, h ⊢' (a', xs) ↔ (stk, loc, pc, xcp); ⋀xs. P, i, n, h ⊢' (i, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, a⌊i⌉, n, h ⊢' (a'⌊i⌉, xs) ↔ (stk, loc, pc, xcp)"

| bisim1AAcc2':
  "⟦ P, i, n, h ⊢' (i', xs) ↔ (stk, loc, pc, xcp); ⋀xs. P, a, n, h ⊢' (a, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, a⌊i⌉, n, h ⊢' (Val v⌊i'⌉, xs) ↔ (stk @ [v], loc, length (compE2 a) + pc, xcp)"

| bisim1AAccThrow1':
  "⟦ P, a, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋);
     ⋀xs. P, i, n, h ⊢' (i, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, a⌊i⌉, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)"

| bisim1AAccThrow2':
  "⟦ P, i, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋);
     ⋀xs. P, a, n, h ⊢' (a, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, a⌊i⌉, n, h ⊢' (Throw ad, xs) ↔ (stk @ [v], loc, length (compE2 a) + pc, ⌊ad⌋)"

| bisim1AAccFail':
  "⟦ ⋀xs. P, a, n, h ⊢' (a, xs) ↔ ([], xs, 0, None); ⋀xs. P, i, n, h ⊢' (i, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, a⌊i⌉, n, h ⊢' (Throw ad, xs) ↔ ([v, v'], xs, length (compE2 a) + length (compE2 i), ⌊ad⌋)"


| bisim1AAss1':
  "⟦ P, a, n, h ⊢' (a', xs) ↔ (stk, loc, pc, xcp); 
     ⋀xs. P, i, n, h ⊢' (i, xs) ↔ ([], xs, 0, None);
     ⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, a⌊i⌉ := e, n, h ⊢' (a'⌊i⌉ := e, xs) ↔ (stk, loc, pc, xcp)"

| bisim1AAss2':
  "⟦ P, i, n, h ⊢' (i', xs) ↔ (stk, loc, pc, xcp);
     ⋀xs. P, a, n, h ⊢' (a, xs) ↔ ([], xs, 0, None);
     ⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, a⌊i⌉ := e, n, h ⊢' (Val v⌊i'⌉ := e, xs) ↔ (stk @ [v], loc, length (compE2 a) + pc, xcp)"

| bisim1AAss3':
  "⟦ P, e, n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp); 
     ⋀xs. P, a, n, h ⊢' (a, xs) ↔ ([], xs, 0, None);
     ⋀xs. P, i, n, h ⊢' (i, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, a⌊i⌉ := e, n, h ⊢' (Val v⌊Val v'⌉ := e', xs) ↔ (stk @ [v', v], loc, length (compE2 a) + length (compE2 i) + pc, xcp)"

| bisim1AAssThrow1':
  "⟦ P, a, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋);
     ⋀xs. P, i, n, h ⊢' (i, xs) ↔ ([], xs, 0, None); 
     ⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, a⌊i⌉ := e, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)"

| bisim1AAssThrow2':
  "⟦ P, i, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋); 
     ⋀xs. P, a, n, h ⊢' (a, xs) ↔ ([], xs, 0, None);
     ⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, a⌊i⌉ := e, n, h ⊢' (Throw ad, xs) ↔ (stk @ [v], loc, length (compE2 a) + pc, ⌊ad⌋)"

| bisim1AAssThrow3':
  "⟦ P, e, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋);
     ⋀xs. P, a, n, h ⊢' (a, xs) ↔ ([], xs, 0, None); 
     ⋀xs. P, i, n, h ⊢' (i, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, a⌊i⌉ := e, n, h ⊢' (Throw ad, xs) ↔ (stk @ [v', v], loc, length (compE2 a) + length (compE2 i) + pc, ⌊ad⌋)"

| bisim1AAssFail':
  "⟦ ⋀xs. P, a, n, h ⊢' (a, xs) ↔ ([], xs, 0, None);  
     ⋀xs. P, i, n, h ⊢' (i, xs) ↔ ([], xs, 0, None);
     ⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, a⌊i⌉ := e, n, h ⊢' (Throw ad, xs) ↔ ([v', v, v''], xs, length (compE2 a) + length (compE2 i) + length (compE2 e), ⌊ad⌋)"

| bisim1AAss4':
  "⟦ ⋀xs. P, a, n, h ⊢' (a, xs) ↔ ([], xs, 0, None);  
     ⋀xs. P, i, n, h ⊢' (i, xs) ↔ ([], xs, 0, None);
     ⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, a⌊i⌉ := e, n, h ⊢' (unit, xs) ↔ ([], xs, Suc (length (compE2 a) + length (compE2 i) + length (compE2 e)), None)"


| bisim1ALength': 
  "P, a, n, h ⊢' (a', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, a∙length, n, h ⊢' (a'∙length, xs) ↔ (stk, loc, pc, xcp)"

| bisim1ALengthThrow':
  "P, a, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, a∙length, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)"


| bisim1ALengthNull':
  "(⋀xs. P, a, n, h ⊢' (a, xs) ↔ ([], xs, 0, None))
  ⟹ P, a∙length, n, h ⊢' (THROW NullPointer, xs) ↔ ([Null], xs, length (compE2 a), ⌊addr_of_sys_xcpt NullPointer⌋)"


| bisim1FAcc': 
  "P, e, n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, e∙F{D}, n, h ⊢' (e'∙F{D}, xs) ↔ (stk, loc, pc, xcp)"

| bisim1FAccThrow':
  "P, e, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)
  ⟹ P, e∙F{D}, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)"

| bisim1FAccNull':
  "(⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None))
   ⟹ P, e∙F{D}, n, h ⊢' (THROW NullPointer, xs) ↔ ([Null], xs, length (compE2 e), ⌊addr_of_sys_xcpt NullPointer⌋)"


| bisim1FAss1': 
  "⟦ P, e, n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp); 
     ⋀xs. P, e2, n, h ⊢' (e2, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e∙F{D} := e2, n, h ⊢' (e'∙F{D} := e2, xs) ↔ (stk, loc, pc, xcp)"

| bisim1FAss2': 
  "⟦ P, e2, n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp);
     ⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e∙F{D} := e2, n, h ⊢' (Val v∙F{D} := e', xs) ↔ (stk @ [v], loc, length (compE2 e) + pc, xcp)"

| bisim1FAssThrow1':
  "⟦ P, e, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋);
     ⋀xs. P, e2, n, h ⊢' (e2, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e∙F{D} := e2, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)"

| bisim1FAssThrow2':
  "⟦ P, e2, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋);
     ⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e∙F{D} := e2, n, h ⊢' (Throw ad, xs) ↔ (stk @ [v], loc, length (compE2 e) + pc, ⌊ad⌋)"

| bisim1FAssNull':
  "⟦ ⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None);
     ⋀xs. P, e2, n, h ⊢' (e2, xs) ↔ ([], xs, 0, None) ⟧
   ⟹ P, e∙F{D} := e2, n, h ⊢' (THROW NullPointer, xs) ↔ ([v, Null], xs, length (compE2 e) + length (compE2 e2), ⌊addr_of_sys_xcpt NullPointer⌋)"

| bisim1FAss3':
  "⟦ ⋀xs. P, e, n, h ⊢' (e, xs) ↔ ([], xs, 0, None); 
     ⋀xs. P, e2, n, h ⊢' (e2, xs) ↔ ([], xs, 0, None) ⟧
   ⟹ P, e∙F{D} := e2, n, h ⊢' (unit, xs) ↔ ([], xs, Suc (length (compE2 e) + length (compE2 e2)), None)"


| bisim1CAS1':
  "⟦ P, e1, n, h ⊢' (e1', xs) ↔ (stk, loc, pc, xcp); 
    ⋀xs. P, e2, n, h ⊢' (e2, xs) ↔ ([], xs, 0, None);
    ⋀xs. P, e3, n, h ⊢' (e3, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e1∙compareAndSwap(D∙F, e2, e3), n, h ⊢' (e1'∙compareAndSwap(D∙F, e2, e3), xs) ↔ (stk, loc, pc, xcp)"

| bisim1CAS2':
  "⟦ P, e2, n, h ⊢' (e2', xs) ↔ (stk, loc, pc, xcp); 
    ⋀xs. P, e1, n, h ⊢' (e1, xs) ↔ ([], xs, 0, None);
    ⋀xs. P, e3, n, h ⊢' (e3, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e1∙compareAndSwap(D∙F, e2, e3), n, h ⊢' (Val v∙compareAndSwap(D∙F, e2', e3), xs) ↔ (stk @ [v], loc, length (compE2 e1) + pc, xcp)"

| bisim1CAS3':
  "⟦ P, e3, n, h ⊢' (e3', xs) ↔ (stk, loc, pc, xcp);
    ⋀xs. P, e1, n, h ⊢' (e1, xs) ↔ ([], xs, 0, None);
    ⋀xs. P, e2, n, h ⊢' (e2, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e1∙compareAndSwap(D∙F, e2, e3), n, h ⊢' (Val v∙compareAndSwap(D∙F, Val v', e3'), xs) ↔ (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, xcp)"

| bisim1CASThrow1':
  "⟦ P, e1, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋);
    ⋀xs. P, e2, n, h ⊢' (e2, xs) ↔ ([], xs, 0, None);
    ⋀xs. P, e3, n, h ⊢' (e3, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e1∙compareAndSwap(D∙F, e2, e3), n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋)"

| bisim1CASThrow2':
  "⟦ P, e2, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋);
    ⋀xs. P, e1, n, h ⊢' (e1, xs) ↔ ([], xs, 0, None);
    ⋀xs. P, e3, n, h ⊢' (e3, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e1∙compareAndSwap(D∙F, e2, e3), n, h ⊢' (Throw ad, xs) ↔ (stk @ [v], loc, length (compE2 e1) + pc, ⌊ad⌋)"

| bisim1CASThrow3':
  "⟦ P, e3, n, h ⊢' (Throw ad, xs) ↔ (stk, loc, pc, ⌊ad⌋);
    ⋀xs. P, e1, n, h ⊢' (e1, xs) ↔ ([], xs, 0, None);
    ⋀xs. P, e2, n, h ⊢' (e2, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e1∙compareAndSwap(D∙F, e2, e3), n, h ⊢' (Throw ad, xs) ↔ (stk @ [v', v], loc, length (compE2 e1) + length (compE2 e2) + pc, ⌊ad⌋)"

| bisim1CASFail':
  "⟦ ⋀xs. P, e1, n, h ⊢' (e1, xs) ↔ ([], xs, 0, None);
    ⋀xs. P, e2, n, h ⊢' (e2, xs) ↔ ([], xs, 0, None); 
    ⋀xs. P, e3, n, h ⊢' (e3, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, e1∙compareAndSwap(D∙F, e2, e3), n, h ⊢' (Throw ad, xs) ↔ ([v', v, v''], xs, length (compE2 e1) + length (compE2 e2) + length (compE2 e3), ⌊ad⌋)"


| bisim1Call1':
  "⟦ P, obj, n, h ⊢' (obj', xs) ↔ (stk, loc, pc, xcp);
     ⋀xs. P, ps, n, h ⊢' (ps, xs) [↔] ([], xs, 0, None) ⟧
  ⟹ P, obj∙M(ps), n, h ⊢' (obj'∙M(ps), xs) ↔ (stk, loc, pc, xcp)"

| bisim1CallParams':
  "⟦ P, ps, n, h ⊢' (ps', xs) [↔] (stk, loc, pc, xcp); ps ≠ [];
     ⋀xs. P, obj, n, h ⊢' (obj, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, obj∙M(ps), n, h ⊢' (Val v∙M(ps'), xs) ↔ (stk @ [v], loc, length (compE2 obj) +  pc, xcp)"

| bisim1CallThrowObj':
  "⟦ P, obj, n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋);
     ⋀xs. P, ps, n, h ⊢' (ps, xs) [↔] ([], xs, 0, None)⟧
  ⟹ P, obj∙M(ps), n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"

| bisim1CallThrowParams':
  "⟦ P, ps, n, h ⊢' (map Val vs @ Throw a # ps', xs) [↔] (stk, loc, pc, ⌊a⌋);
     ⋀xs. P, obj, n, h ⊢' (obj, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, obj∙M(ps), n, h ⊢' (Throw a, xs) ↔ (stk @ [v], loc, length (compE2 obj) + pc, ⌊a⌋)"

| bisim1CallThrow':
  "⟦ length ps = length vs;
     ⋀xs. P, obj, n, h ⊢' (obj, xs) ↔ ([], xs, 0, None); ⋀xs. P, ps, n, h ⊢' (ps, xs) [↔] ([], xs, 0, None) ⟧
  ⟹ P, obj∙M(ps), n, h ⊢' (Throw a, xs) ↔ (vs @ [v], xs, length (compE2 obj) + length (compEs2 ps), ⌊a⌋)"

| bisim1BlockSome1':
  "(⋀xs. P, e, Suc n, h ⊢' (e, xs) ↔ ([], xs, 0, None))
  ⟹ P, {V:T=⌊v⌋; e}, n, h ⊢' ({V:T=⌊v⌋; e}, xs) ↔ ([], xs, 0, None)"

| bisim1BlockSome2':
  "(⋀xs. P, e, Suc n, h ⊢' (e, xs) ↔ ([], xs, 0, None))
  ⟹ P, {V:T=⌊v⌋; e}, n, h ⊢' ({V:T=⌊v⌋; e}, xs) ↔ ([v], xs, Suc 0, None)"

| bisim1BlockSome4':
  "P, e, Suc n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, {V:T=⌊v⌋; e}, n, h ⊢' ({V:T=None; e'}, xs) ↔ (stk, loc, Suc (Suc pc), xcp)"

| bisim1BlockThrowSome':
  "P, e, Suc n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
  ⟹ P, {V:T=⌊v⌋; e}, n, h ⊢' (Throw a, xs) ↔ (stk, loc, Suc (Suc pc), ⌊a⌋)"

| bisim1BlockNone':
  "P, e, Suc n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp)
  ⟹ P, {V:T=None; e}, n, h ⊢' ({V:T=None; e'}, xs) ↔ (stk, loc, pc, xcp)"

| bisim1BlockThrowNone':
  "P, e, Suc n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)
  ⟹ P, {V:T=None; e}, n, h ⊢' (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"


| bisim1Sync1':
  "⟦ P, e1, n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp); 
     ⋀xs. P, e2, Suc n, h ⊢' (e2, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, sync⇘V⇙ (e1) e2, n, h ⊢' (sync⇘V⇙ (e') e2, xs) ↔ (stk, loc, pc, xcp)"

| bisim1Sync2':
  "⟦ ⋀xs. P, e1, n, h ⊢' (e1, xs) ↔ ([], xs, 0, None);
    ⋀xs. P, e2, Suc n, h ⊢' (e2, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, sync⇘V⇙ (e1) e2, n, h ⊢' (sync⇘V⇙ (Val v) e2, xs) ↔ ([v, v], xs, Suc (length (compE2 e1)), None)"

| bisim1Sync3':
  "⟦ ⋀xs. P, e1, n, h ⊢' (e1, xs) ↔ ([], xs, 0, None);
    ⋀xs. P, e2, Suc n, h ⊢' (e2, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, sync⇘V⇙ (e1) e2, n, h ⊢' (sync⇘V⇙ (Val v) e2, xs) ↔ ([v], xs[V := v], Suc (Suc (length (compE2 e1))), None)"

| bisim1Sync4':
  "⟦ P, e2, Suc n, h ⊢' (e', xs) ↔ (stk, loc, pc, xcp); 
     ⋀xs. P, e1, n, h ⊢' (e1, xs) ↔ ([], xs, 0, None) ⟧
  ⟹ P, sync⇘V⇙ (e1) e2, n, h ⊢' (insync⇘V⇙ (a) e', xs) ↔ (stk, loc, Suc (Suc (Suc (