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