# Theory J1JVM

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

section ‹Correctness of Stage: From intermediate language to JVM›

theory J1JVM imports J1JVMBisim begin

context J1_JVM_heap_base begin

declare τmove1.simps [simp del] τmoves1.simps [simp del]

lemma bisim1_insync_Throw_exec:
assumes bisim2: "P,e2,h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, xcp)"
shows "τExec_movet_a P t (sync⇘V⇙ (e1) e2) h (stk, loc, Suc (Suc (Suc (length (compE2 e1) + pc))), xcp) ([Addr ad], loc, 6 + length (compE2 e1) + length (compE2 e2), None)"
proof -
from bisim2 have pc: "pc < length (compE2 e2)" and [simp]: "xs = loc" by(auto dest: bisim1_ThrowD)
let ?pc = "6 + length (compE2 e1) + length (compE2 e2)"
let ?stk = "Addr ad # drop (size stk - 0) stk"
from bisim2 have "xcp = ⌊ad⌋ ∨ xcp = None" by(auto dest: bisim1_ThrowD)
thus ?thesis
proof
have "τExec_movet_a P t (sync⇘V⇙ (e1) e2) h (stk, loc, Suc (Suc (Suc (length (compE2 e1) + pc))), ⌊ad⌋) (?stk, loc, ?pc, None)"
proof(rule τExect1step[unfolded exec_move_def, OF exec_catch])
from bisim1_xcp_Some_not_caught[OF bisim2[simplified], of "λC M Ts T. compMb2" "Suc (Suc (Suc (length (compE2 e1))))" 0]
have "match_ex_table (compP2 P) (cname_of h ad) (Suc (Suc (Suc (length (compE2 e1) + pc)))) (compxE2 e2 (Suc (Suc (Suc (length (compE2 e1))))) 0) = None"
thus "match_ex_table (compP2 P) (cname_of h ad) (Suc (Suc (Suc (length (compE2 e1) + pc)))) (compxE2 (sync⇘V⇙ (e1) e2) 0 0) = ⌊(6 + length (compE2 e1) + length (compE2 e2), 0)⌋"
using pc
by(auto simp add: compP2_def match_ex_table_append matches_ex_entry_def eval_nat_numeral
dest: match_ex_table_pc_length_compE2)
qed(insert pc, auto intro: τmove2xcp)
thus ?thesis by simp
next
assume [simp]: "xcp = None"
with bisim2 obtain pc'
by(auto dest: bisim1_Throw_τExec_movet)
hence "τExec_movet_a P t (sync⇘V⇙ (e1) e2) h (stk, loc, Suc (Suc (Suc (length (compE2 e1) + pc))), None) ([Addr ad], loc, Suc (Suc (Suc (length (compE2 e1) + pc'))), ⌊ad⌋)"
by-(rule Insync_τExectI)
from bisim' have pc': "pc' < length (compE2 e2)" by(auto dest: bisim1_ThrowD)
have "τExec_movet_a P t (sync⇘V⇙ (e1) e2) h ([Addr ad], loc, Suc (Suc (Suc (length (compE2 e1) + pc'))), ⌊ad⌋) (?stk, loc, ?pc, None)"
proof(rule τExect1step[unfolded exec_move_def, OF exec_catch])
from bisim1_xcp_Some_not_caught[OF bisim', of "λC M Ts T. compMb2" "Suc (Suc (Suc (length (compE2 e1))))" 0]
have "match_ex_table (compP2 P) (cname_of h ad) (Suc (Suc (Suc (length (compE2 e1) + pc')))) (compxE2 e2 (Suc (Suc (Suc (length (compE2 e1))))) 0) = None"
thus "match_ex_table (compP2 P) (cname_of h ad) (Suc (Suc (Suc (length (compE2 e1) + pc')))) (compxE2 (sync⇘V⇙ (e1) e2) 0 0) = ⌊(6 + length (compE2 e1) + length (compE2 e2), 0)⌋"
using pc'
by(auto simp add: compP2_def match_ex_table_append matches_ex_entry_def eval_nat_numeral
dest: match_ex_table_pc_length_compE2)
qed(insert pc', auto intro: τmove2xcp)
finally (tranclp_trans) show ?thesis by simp
qed
qed

end

primrec sim12_size :: "('a, 'b, 'addr) exp ⇒ nat"
and sim12_sizes :: "('a, 'b, 'addr) exp list ⇒ nat"
where
"sim12_size (new C) = 0"
| "sim12_size (newA T⌊e⌉) = Suc (sim12_size e)"
| "sim12_size (Cast T e) = Suc (sim12_size e)"
| "sim12_size (e instanceof T) = Suc (sim12_size e)"
| "sim12_size (e «bop» e') = Suc (sim12_size e + sim12_size e')"
| "sim12_size (Val v) = 0"
| "sim12_size (Var V) = 0"
| "sim12_size (V := e) = Suc (sim12_size e)"
| "sim12_size (a⌊i⌉) = Suc (sim12_size a + sim12_size i)"
| "sim12_size (a⌊i⌉ := e) = Suc (sim12_size a + sim12_size i + sim12_size e)"
| "sim12_size (a∙length) = Suc (sim12_size a)"
| "sim12_size (e∙F{D}) = Suc (sim12_size e)"
| "sim12_size (e∙F{D} := e') = Suc (sim12_size e + sim12_size e')"
| "sim12_size (e∙compareAndSwap(D∙F, e', e'')) = Suc (sim12_size e + sim12_size e' + sim12_size e'')"
| "sim12_size (e∙M(es)) = Suc (sim12_size e + sim12_sizes es)"
| "sim12_size ({V:T=vo; e}) = Suc (sim12_size e)"
| "sim12_size (sync⇘V⇙(e) e') = Suc (sim12_size e + sim12_size e')"
| "sim12_size (insync⇘V⇙(a) e) = Suc (sim12_size e)"
| "sim12_size (e;; e') = Suc (sim12_size e + sim12_size e')"
| "sim12_size (if (e) e1 else e2) = Suc (sim12_size e)"
| "sim12_size (while(b) c) = Suc (Suc (sim12_size b))"
| "sim12_size (throw e) = Suc (sim12_size e)"
| "sim12_size (try e catch(C V) e') = Suc (sim12_size e)"

| "sim12_sizes [] = 0"
| "sim12_sizes (e # es) = sim12_size e + sim12_sizes es"

lemma sim12_sizes_map_Val [simp]:
"sim12_sizes (map Val vs) = 0"
by(induct vs) simp_all

lemma sim12_sizes_append [simp]:
"sim12_sizes (es @ es') = sim12_sizes es + sim12_sizes es'"
by(induct es) simp_all

context JVM_heap_base begin

lemma τExec_mover_length_compE2_conv [simp]:
assumes pc: "pc ≥ length (compE2 e)"
shows "τExec_mover ci P t e h (stk, loc, pc, xcp) s ⟷ s = (stk, loc, pc, xcp)"
proof
assume "τExec_mover ci P t e h (stk, loc, pc, xcp) s"
thus "s = (stk, loc, pc, xcp)" using pc
qed auto

lemma τExec_movesr_length_compE2_conv [simp]:
assumes pc: "pc ≥ length (compEs2 es)"
shows "τExec_movesr ci P t es h (stk, loc, pc, xcp) s ⟷ s = (stk, loc, pc, xcp)"
proof
assume "τExec_movesr ci P t es h (stk, loc, pc, xcp) s"
thus "s = (stk, loc, pc, xcp)" using pc
qed auto

end

context J1_JVM_heap_base begin

lemma assumes wf: "wf_J1_prog P"
defines [simp]: "sim_move ≡ λe e'. if sim12_size e' < sim12_size e then τExec_mover_a else τExec_movet_a"
and [simp]: "sim_moves ≡ λes es'. if sim12_sizes es' < sim12_sizes es then τExec_movesr_a else τExec_movest_a"
shows exec_instr_simulates_red1:
"⟦ P, E, h ⊢ (e, xs) ↔ (stk, loc, pc, xcp); True,P,t ⊢1 ⟨e, (h, xs)⟩ -ta→ ⟨e', (h', xs')⟩; bsok E n ⟧
⟹ ∃pc'' stk'' loc'' xcp''. P, E, h' ⊢ (e', xs') ↔ (stk'', loc'', pc'', xcp'') ∧
(if τmove1 P h e
then h = h' ∧ sim_move e e' P t E h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')
else ∃pc' stk' loc' xcp'. τExec_mover_a P t E h (stk, loc, pc, xcp) (stk', loc', pc', xcp') ∧
exec_move_a P t E h (stk', loc', pc', xcp') (extTA2JVM (compP2 P) ta) h' (stk'', loc'', pc'', xcp'') ∧
¬ τmove2 (compP2 P) h stk' E pc' xcp' ∧
(call1 e = None ∨ no_call2 E pc ∨ pc' = pc ∧ stk' = stk ∧ loc' = loc ∧ xcp' = xcp))"
(is "⟦ _; _; _ ⟧
⟹ ∃pc'' stk'' loc'' xcp''. _ ∧ ?exec ta E e e' h stk loc pc xcp h' pc'' stk'' loc'' xcp''")

and exec_instr_simulates_reds1:
"⟦ P, Es, h ⊢ (es, xs) [↔] (stk, loc, pc, xcp); True,P,t ⊢1 ⟨es, (h, xs)⟩ [-ta→] ⟨es', (h', xs')⟩; bsoks Es n ⟧
⟹ ∃pc'' stk'' loc'' xcp''. P, Es, h' ⊢ (es', xs') [↔] (stk'', loc'', pc'', xcp'') ∧
(if τmoves1 P h es
then h = h' ∧ sim_moves es es' P t Es h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')
else ∃pc' stk' loc' xcp'. τExec_movesr_a P t Es h (stk, loc, pc, xcp) (stk', loc', pc', xcp') ∧
exec_moves_a P t Es h (stk', loc', pc', xcp') (extTA2JVM (compP2 P) ta) h' (stk'', loc'', pc'', xcp'') ∧
¬ τmoves2 (compP2 P) h stk' Es pc' xcp' ∧
(calls1 es = None ∨ no_calls2 Es pc ∨ pc' = pc ∧ stk' = stk ∧ loc' = loc ∧ xcp' = xcp))"
(is "⟦ _; _; _ ⟧
⟹ ∃pc'' stk'' loc'' xcp''. _ ∧ ?execs ta Es es es' h stk loc pc xcp h' pc'' stk'' loc'' xcp''")
proof(induction E n e xs stk loc pc xcp and Es n es xs stk loc pc xcp
arbitrary: e' h' xs' Env T Env' T' and es' h' xs' Env Ts Env' Ts' rule: bisim1_bisims1_inducts_split)
case (bisim1Call1 obj n obj' xs stk loc pc xcp ps M')
note IHobj = bisim1Call1.IH(2)
note IHparam = bisim1Call1.IH(4)
note bisim1 = ‹P,obj,h ⊢ (obj', xs) ↔ (stk, loc, pc, xcp)›
note bisim2 = ‹⋀xs. P,ps,h ⊢ (ps, xs) [↔] ([], xs, 0, None)›
note bsok = ‹bsok (obj∙M'(ps)) n›
note red = ‹True,P,t ⊢1 ⟨obj'∙M'(ps),(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩›
from red show ?case
proof(cases)
case (Call1Obj E')
note [simp] = ‹e' = E'∙M'(ps)›
and red = ‹True,P,t ⊢1 ⟨obj',(h, xs)⟩ -ta→ ⟨E',(h', xs')⟩›
from red have τ: "τmove1 P h obj' = τmove1 P h (obj'∙M'(ps))" by(auto simp add: τmove1.simps τmoves1.simps)
moreover from red have "call1 (obj'∙M'(ps)) = call1 obj'" by auto
moreover from IHobj[OF red] bsok
obtain pc'' stk'' loc'' xcp'' where bisim: "P,obj,h' ⊢ (E', xs') ↔ (stk'', loc'', pc'', xcp'')"
and redo: "?exec ta obj obj' E' h stk loc pc xcp h' pc'' stk'' loc'' xcp''" by auto
from bisim
have "P,obj∙M'(ps),h' ⊢ (E'∙M'(ps), xs') ↔ (stk'', loc'', pc'', xcp'')"
by(rule bisim1_bisims1.bisim1Call1)
moreover {
assume "no_call2 obj pc"
hence "no_call2 (obj∙M'(ps)) pc ∨ pc = length (compE2 obj)" by(auto simp add: no_call2_def) }
ultimately show ?thesis using redo
by(auto simp del: call1.simps calls1.simps split: if_split_asm split del: if_split)(blast intro: Call_τExecrI1 Call_τExectI1 exec_move_CallI1)+
next
case (Call1Params es v)
note [simp] = ‹obj' = Val v› ‹e' = Val v∙M'(es)›
and red = ‹True,P,t ⊢1 ⟨ps, (h, xs)⟩ [-ta→] ⟨es, (h', xs')⟩›
from red have τ: "τmove1 P h (obj'∙M'(ps)) = τmoves1 P h ps" by(auto simp add: τmove1.simps τmoves1.simps)
from bisim1 have s: "xcp = None" "xs = loc"
and execo: "τExec_mover_a P t obj h (stk, loc, pc, xcp) ([v], loc, length (compE2 obj), None)"
by(auto dest: bisim1Val2D1)
hence "τExec_mover_a P t (obj∙M'(ps)) h (stk, loc, pc, xcp) ([v], loc, length (compE2 obj), None)"
by-(rule Call_τExecrI1)
moreover from IHparam[OF red] bsok obtain pc'' stk'' loc'' xcp''
where bisim': "P,ps,h' ⊢ (es, xs') [↔] (stk'', loc'', pc'', xcp'')"
and exec': "?execs ta ps ps es h [] xs 0 None h' pc'' stk'' loc'' xcp''" by auto
have "?exec ta (obj∙M'(ps)) (obj'∙M'(ps)) (obj'∙M(es)) h [v] loc (length (compE2 obj)) None h' (length (compE2 obj) + pc'') (stk'' @ [v]) loc'' xcp''"
proof(cases "τmove1 P h (obj'∙M'(ps))")
case True
with exec' τ have [simp]: "h = h'"
and e: "sim_moves ps es P t ps h ([], xs, 0, None) (stk'', loc'', pc'', xcp'')" by auto
from e have "sim_move (obj'∙M'(ps)) (obj'∙M'(es)) P t (obj∙M'(ps)) h ([] @ [v], xs, length (compE2 obj) + 0, None) (stk'' @ [v], loc'', length (compE2 obj) + pc'', xcp'')"
by(fastforce dest: Call_τExecrI2 Call_τExectI2)
with s True show ?thesis by auto
next
case False
with exec' τ obtain pc' stk' loc' xcp'
where e: "τExec_movesr_a P t ps h ([], xs, 0, None) (stk', loc', pc', xcp')"
and e': "exec_moves_a P t ps h (stk', loc', pc', xcp') (extTA2JVM (compP2 P) ta) h' (stk'', loc'', pc'', xcp'')"
and τ': "¬ τmoves2 (compP2 P) h stk' ps pc' xcp'"
and call: "calls1 ps = None ∨ no_calls2 ps 0 ∨ pc' = 0 ∧ stk' = [] ∧ loc' = xs ∧ xcp' = None" by auto
from e have "τExec_mover_a P t (obj∙M'(ps)) h ([] @ [v], xs, length (compE2 obj) + 0, None) (stk' @ [v], loc', length (compE2 obj) + pc', xcp')" by(rule Call_τExecrI2)
moreover from e' have "exec_move_a P t (obj∙M'(ps)) h (stk' @ [v], loc', length (compE2 obj) + pc', xcp') (extTA2JVM (compP2 P) ta) h' (stk'' @ [v], loc'', length (compE2 obj) + pc'', xcp'')"
by(rule exec_move_CallI2)
moreover from τ' e' have "τmove2 (compP2 P) h (stk' @ [v]) (obj∙M'(ps)) (length (compE2 obj) + pc') xcp' ⟹ False"
by(fastforce simp add: τmove2_iff τmoves2_iff τinstr_stk_drop_exec_moves split: if_split_asm)
moreover from red have "call1 (obj'∙M'(ps)) = calls1 ps" by(auto simp add: is_vals_conv)
moreover have "no_calls2 ps 0 ⟹ no_call2 (obj∙M'(ps)) (length (compE2 obj)) ∨ ps = []" "calls1 [] = None"
ultimately show ?thesis using False s call
by(auto simp del: split_paired_Ex call1.simps calls1.simps) blast
qed
moreover from bisim'
have "P,obj∙M'(ps),h' ⊢ (Val v∙M'(es), xs') ↔ ((stk'' @ [v]), loc'', length (compE2 obj) + pc'', xcp'')"
by(rule bisim1_bisims1.bisim1CallParams)
moreover from bisim1 have "pc ≠ length (compE2 obj) ⟶ no_call2 (obj∙M'(ps)) pc"
by(auto simp add: no_call2_def dest: bisim_Val_pc_not_Invoke bisim1_pc_length_compE2)
ultimately show ?thesis using τ execo
apply(auto simp del: split_paired_Ex call1.simps calls1.simps split: if_split_asm split del: if_split)
apply(blast intro: τExec_mover_trans|fastforce elim!: τExec_mover_trans simp del: split_paired_Ex call1.simps calls1.simps)+
done
next
case (Call1ThrowObj a)
note [simp] = ‹obj' = Throw a› ‹ta = ε› ‹e' = Throw a› ‹h' = h› ‹xs' = xs›
have τ: "τmove1 P h (Throw a∙M'(ps))" by(rule τmove1CallThrowObj)
from bisim1 have "xcp = ⌊a⌋ ∨ xcp = None" by(auto dest: bisim1_ThrowD)
thus ?thesis
proof
assume [simp]: "xcp = ⌊a⌋"
with bisim1 have "P, obj∙M'(ps), h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"
by(auto intro: bisim1_bisims1.bisim1CallThrowObj)
thus ?thesis using τ by(fastforce)
next
assume [simp]: "xcp = None"
with bisim1 obtain pc'
where "τExec_mover_a P t obj h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
and bisim': "P, obj, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)" and [simp]: "xs = loc"
by(auto dest: bisim1_Throw_τExec_mover)
hence "τExec_mover_a P t (obj∙M'(ps)) h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
by-(rule Call_τExecrI1)
moreover from bisim' have "P, obj∙M'(ps), h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)"
by(rule bisim1CallThrowObj)
ultimately show ?thesis using τ by auto
qed
next
case (Call1ThrowParams vs a es' v)
note [simp] = ‹obj' = Val v› ‹ta = ε› ‹e' = Throw a› ‹h' = h› ‹xs' = xs›
and ps = ‹ps = map Val vs @ Throw a # es'›
from bisim1 have [simp]: "xcp = None" "xs = loc"
and "τExec_mover_a P t obj h (stk, loc, pc, xcp) ([v], loc, length (compE2 obj), None)"
by(auto dest: bisim1Val2D1)
hence "τExec_mover_a P t (obj∙M'(ps)) h (stk, loc, pc, xcp) ([v], loc, length (compE2 obj), None)"
by-(rule Call_τExecrI1)
also from bisims1_Throw_τExec_movest[OF bisim2[of xs, unfolded ps]]
obtain pc' where exec': "τExec_movest_a P t (map Val vs @ Throw a # es') h ([], xs, 0, None) (Addr a # rev vs, xs, pc', ⌊a⌋)"
and bisim': "P,map Val vs @ Throw a # es',h ⊢ (map Val vs @ Throw a # es', xs) [↔] (Addr a # rev vs, xs, pc', ⌊a⌋)"
by auto
from Call_τExectI2[OF exec', of "obj" M' v] ps
have "τExec_movet_a P t (obj∙M'(ps)) h ([v], loc, length (compE2 obj), None) (Addr a # rev vs @ [v], xs, length (compE2 obj) + pc', ⌊a⌋)" by simp
also from bisim1_bisims1.bisim1CallThrowParams[OF bisim', of obj M' v] ps
have bisim'': "P,obj∙M'(ps),h ⊢ (Throw a, xs) ↔ (Addr a # rev vs @ [v], xs, length (compE2 obj) + pc', ⌊a⌋)" by simp
moreover have "τmove1 P h (obj'∙M'(ps))" using ps by(auto intro: τmove1CallThrowParams)
ultimately show ?thesis by fastforce
next
case (Red1CallExternal a Ta Ts Tr D vs va H')
hence [simp]: "obj' = addr a" "ps = map Val vs"
"e' = extRet2J (addr a∙M'(map Val vs)) va" "H' = h'" "xs' = xs"
and Ta: "typeof_addr h a = ⌊Ta⌋"
and iec: "P ⊢ class_type_of Ta sees M': Ts→Tr = Native in D"
and redex: "P,t ⊢ ⟨a∙M'(vs),h⟩ -ta→ext ⟨va,h'⟩" by auto
from bisim1 have [simp]: "xs = loc" by(auto dest: bisim_Val_loc_eq_xcp_None)
have τ: "τmove1 P h (addr a∙M'(map Val vs)) ⟷  τmove2 (compP2 P) h (rev vs @ [Addr a]) (obj∙M'(ps)) (length (compE2 obj) + length (compEs2 ps)) None" using Ta iec
by(auto simp add: map_eq_append_conv τmove1.simps τmoves1.simps τmove2_iff compP2_def)
from bisim1 have s: "xcp = None" "lcl (h, xs) = loc"
and "τExec_mover_a P t obj h (stk, loc, pc, xcp) ([Addr a], loc, length (compE2 obj), None)"
by(auto dest: bisim1Val2D1)
hence "τExec_mover_a P t (obj∙M'(ps)) h (stk, loc, pc, xcp) ([Addr a], loc, length (compE2 obj), None)"
by-(rule Call_τExecrI1)
also have "τExec_movesr_a P t ps h ([], loc, 0, None) (rev vs, loc, length (compEs2 ps), None)"
unfolding ‹ps = map Val vs› by(rule τExec_movesr_map_Val)
from Call_τExecrI2[OF this, of obj M' "Addr a"]
have "τExec_mover_a P t (obj∙M'(ps)) h ([Addr a], loc, length (compE2 obj), None) (rev vs @ [Addr a], loc, length (compE2 obj) + length (compEs2 ps), None)" by simp
also (rtranclp_trans) from bisim1 have "pc ≤ length (compE2 obj)" by(rule bisim1_pc_length_compE2)
hence "no_call2 (obj∙M'(ps)) pc ∨ pc = length (compE2 obj) + length (compEs2 ps)"
using bisim1 by(fastforce simp add: no_call2_def neq_Nil_conv dest: bisim_Val_pc_not_Invoke)
moreover {
assume "pc = length (compE2 obj) + length (compEs2 ps)"
with ‹τExec_mover_a P t obj h (stk, loc, pc, xcp) ([Addr a], loc, length (compE2 obj), None)›
have "stk = rev vs @ [Addr a]" "xcp = None" by auto }
moreover
let ?ret = "extRet2JVM (length ps) h' (rev vs @ [Addr a]) loc undefined undefined (length (compE2 obj) + length (compEs2 ps)) [] va"
let ?stk' = "fst (hd (snd (snd ?ret)))"
let ?xcp' = "fst ?ret"
let ?pc' = "snd (snd (snd (snd (hd (snd (snd ?ret))))))"
from redex have redex': "(ta, va, h') ∈ red_external_aggr (compP2 P) t a M' vs h"
by -(rule red_external_imp_red_external_aggr, simp add: compP2_def)
with Ta iec redex'
have "exec_move_a P t (obj∙M'(ps)) h (rev vs @ [Addr a], loc, length (compE2 obj) + length (compEs2 ps), None) (extTA2JVM (compP2 P) ta) h' (?stk', loc, ?pc', ?xcp')"
unfolding exec_move_def
by-(rule exec_instr,cases va,(force simp add: compP2_def simp del: split_paired_Ex)+)
moreover have "P,obj∙M'(ps),h' ⊢ (extRet2J1 (addr a∙M'(map Val vs)) va, loc) ↔ (?stk', loc, ?pc', ?xcp')"
proof(cases va)
case (RetVal v)
have "P,obj∙M'(ps),h' ⊢ (Val v, loc) ↔ ([v], loc, length (compE2 (obj∙M'(ps))), None)"
by(rule bisim1Val2) simp
thus ?thesis unfolding RetVal by simp
next
case (RetExc ad) thus ?thesis by(auto intro: bisim1CallThrow)
next
case RetStaySame
from bisims1_map_Val_append[OF bisims1Nil, of "map Val vs" vs P h' loc]
have "P,map Val vs,h' ⊢ (map Val vs, loc) [↔] (rev vs, loc, length (compEs2 (map Val vs)), None)" by simp
hence "P,obj∙M'(map Val vs),h' ⊢ (addr a∙M'(map Val vs), loc) ↔ (rev vs @ [Addr a], loc, length (compE2 obj) + length (compEs2 (map Val vs)), None)"
by(rule bisim1CallParams)
thus ?thesis using RetStaySame by simp
qed
moreover from redex Ta iec
have "τmove1 P h (addr a∙M'(map Val vs)) ⟹ ta = ε ∧ h' = h"
by(fastforce simp add: τmove1.simps τmoves1.simps map_eq_append_conv τexternal'_def τexternal_def dest: τexternal'_red_external_heap_unchanged τexternal'_red_external_TA_empty sees_method_fun)
ultimately show ?thesis using τ
apply(auto simp del: split_paired_Ex simp add: compP2_def)
apply(blast intro: rtranclp.rtrancl_into_rtrancl rtranclp_into_tranclp1 τexec_moveI)+
done
next
case (Red1CallNull vs)
note [simp] = ‹h' = h› ‹xs' = xs› ‹ta = ε› ‹obj' = null› ‹ps = map Val vs› ‹e' = THROW NullPointer›
from bisim1 have s: "xcp = None" "xs = loc"
and "τExec_mover_a P t obj h (stk, loc, pc, xcp) ([Null], loc, length (compE2 obj), None)"
by(auto dest: bisim1Val2D1)
hence "τExec_mover_a P t (obj∙M'(map Val vs)) h (stk, loc, pc, xcp) ([Null], loc, length (compE2 obj), None)"
by-(rule Call_τExecrI1)
also have "τExec_movesr_a P t (map Val vs) h ([], loc, 0, None) (rev vs, loc, length (compEs2 (map Val vs)), None)"
proof(cases "vs")
case Nil thus ?thesis by(auto)
next
case Cons
with bisims1_refl[of P "h" "map Val vs" loc, simplified] show ?thesis
by -(drule bisims1_Val_τExec_moves, auto)
qed
from Call_τExecrI2[OF this, of obj M' Null]
have "τExec_mover_a P t (obj∙M'(map Val vs)) h ([Null], loc, length (compE2 obj), None) (rev vs @ [Null], loc, length (compE2 obj) + length (compEs2 (map Val vs)), None)" by simp
also (rtranclp_trans) {
have "τmove2 (compP2 P) h (rev vs @ [Null]) (obj∙M'(map Val vs)) (length (compE2 obj) + length (compEs2 (map Val vs))) None"
moreover have "exec_move_a P t (obj∙M'(map Val vs)) h (rev vs @ [Null], loc, length (compE2 obj) + length (compEs2 (map Val vs)), None) ε h (rev vs @ [Null], loc, length (compE2 obj) + length (compEs2 (map Val vs)), ⌊addr_of_sys_xcpt NullPointer⌋)"
unfolding exec_move_def by(cases vs)(auto intro: exec_instr)
ultimately have "τExec_movet_a P t (obj∙M'(map Val vs)) h  (rev vs @ [Null], loc, length (compE2 obj) + length (compEs2 (map Val vs)), None) (rev vs @ [Null], loc, length (compE2 obj) + length (compEs2 (map Val vs)), ⌊addr_of_sys_xcpt NullPointer⌋)"
by(auto intro: τexec_moveI simp add: compP2_def) }
also have "τmove1 P h (null∙M'(map Val vs))" by(auto simp add: τmove1.simps τmoves1.simps map_eq_append_conv)
moreover have "P,obj∙M'(map Val vs),h ⊢ (THROW NullPointer, loc) ↔ ((rev vs @ [Null]), loc, length (compE2 obj) + length (compEs2 (map Val vs)), ⌊addr_of_sys_xcpt NullPointer⌋)"
by(rule bisim1CallThrow) simp
ultimately show ?thesis using s by(auto simp del: split_paired_Ex)
qed
next
case bisim1Val2 thus ?case by fastforce
next
case (bisim1New C' n xs)
have τ: "¬ τmove1 P h (new C')" by(auto simp add: τmove1.simps τmoves1.simps)
from ‹True,P,t ⊢1 ⟨new C',(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩› show ?case
proof cases
case (Red1New a)
hence "exec_meth_a (compP2 P) [New C'] [] t h ([], xs, 0, None) ⦃NewHeapElem a (Class_type C')⦄ h' ([Addr a], xs, Suc 0, None)"
and [simp]: "e' = addr a" "xs' = xs" "ta = ⦃NewHeapElem a (Class_type C')⦄"
by (auto intro!: exec_instr simp add: compP2_def simp del: fun_upd_apply cong cong del: image_cong_simp)
moreover have "P, new C', h' ⊢ (addr a, xs) ↔ ([Addr a], xs, length (compE2 (new C')), None)"
by(rule bisim1Val2)(simp)
moreover have "¬ τmove2 (compP2 P) h [] (new C') 0 None" by(simp add: τmove2_iff)
ultimately show ?thesis using τ
next
case Red1NewFail
hence "exec_meth_a (compP2 P) [New C'] [] t h ([], xs, 0, None) ε h' ([], xs, 0, ⌊addr_of_sys_xcpt OutOfMemory⌋)"
and [simp]: "ta = ε" "xs' = xs" "e' = THROW OutOfMemory"
by(auto intro!:exec_instr simp add: compP2_def simp del: fun_upd_apply)
moreover have "P, new C', h' ⊢ (THROW OutOfMemory, xs) ↔ ([], xs, 0, ⌊addr_of_sys_xcpt OutOfMemory⌋)"
by(rule bisim1NewThrow)
moreover have "¬ τmove2 (compP2 P) h [] (new C') 0 None" by(simp add: τmove2_iff)
ultimately show ?thesis using τ by(fastforce simp add: exec_move_def)
qed
next
case bisim1NewThrow thus ?case by fastforce
next
case (bisim1NewArray E n e xs stk loc pc xcp U)
note IH = bisim1NewArray.IH(2)
note bisim = ‹P,E,h ⊢ (e, xs) ↔ (stk, loc, pc, xcp)›
note red = ‹True,P,t ⊢1 ⟨newA U⌊e⌉,(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩›
note bsok = ‹bsok (newA U⌊E⌉) n›
from red show ?case
proof cases
case (New1ArrayRed ee')
note [simp] = ‹e' = newA U⌊ee'⌉›
and red = ‹True,P,t ⊢1 ⟨e,(h, xs)⟩ -ta→ ⟨ee', (h', xs')⟩›
from red have "τmove1 P h (newA U⌊e⌉) = τmove1 P h e" by(auto simp add: τmove1.simps τmoves1.simps)
moreover from red have "call1 (newA U⌊e⌉) = call1 e" by auto
moreover from IH[OF red] bsok
obtain pc'' stk'' loc'' xcp'' where bisim: "P,E,h' ⊢ (ee', xs') ↔ (stk'', loc'', pc'', xcp'')"
and redo: "?exec ta E e ee' h stk loc pc xcp h' pc'' stk'' loc'' xcp''" by auto
from bisim
have "P,newA U⌊E⌉,h' ⊢ (newA U⌊ee'⌉, xs') ↔ (stk'', loc'', pc'', xcp'')"
by(rule bisim1_bisims1.bisim1NewArray)
moreover {
assume "no_call2 E pc"
hence "no_call2 (newA U⌊E⌉) pc" by(auto simp add: no_call2_def) }
ultimately show ?thesis using redo
by(auto simp del: call1.simps calls1.simps split: if_split_asm split del: if_split)(blast intro: NewArray_τExecrI NewArray_τExectI exec_move_newArrayI)+
next
case (Red1NewArray i a)
note [simp] = ‹e = Val (Intg i)› ‹ta = ⦃NewHeapElem a (Array_type U (nat (sint i)))⦄› ‹e' = addr a› ‹xs' = xs›
and new = ‹(h', a) ∈ allocate h (Array_type U (nat (sint i)))›
from bisim have s: "xcp = None" "xs = loc" by(auto dest: bisim_Val_loc_eq_xcp_None)
from bisim have "τExec_mover_a P t E h (stk, loc, pc, xcp) ([Intg i], loc, length (compE2 E), None)"
by(auto dest: bisim1Val2D1)
hence "τExec_mover_a P t (newA U⌊E⌉) h (stk, loc, pc, xcp) ([Intg i], loc, length (compE2 E), None)"
by(rule NewArray_τExecrI)
moreover from new ‹0 <=s i›
have "exec_move_a P t (newA U⌊E⌉) h ([Intg i], loc, length (compE2 E), None) ⦃NewHeapElem a (Array_type U (nat (sint i)))⦄ h' ([Addr a], loc, Suc (length (compE2 E)), None)"
by (auto intro!: exec_instr simp add: compP2_def exec_move_def cong del: image_cong_simp)
moreover have "τmove2 (compP2 P) h [Intg i] (newA U⌊E⌉) (length (compE2 E)) None ⟹ False" by(simp add: τmove2_iff)
moreover have "¬ τmove1 P h (newA U⌊Val (Intg i)⌉)" by(auto simp add: τmove1.simps τmoves1.simps)
moreover have "P, newA U⌊E⌉, h' ⊢ (addr a, loc) ↔ ([Addr a], loc, length (compE2 (newA U⌊E⌉)), None)"
by(rule bisim1Val2) simp
ultimately show ?thesis using s by(auto simp del: fun_upd_apply simp add: ta_upd_simps) blast
next
case (Red1NewArrayNegative i)
note [simp] = ‹e = Val (Intg i)› ‹e' = THROW NegativeArraySize› ‹h' = h› ‹xs' = xs› ‹ta = ε›
have "¬ τmove1 P h (newA U⌊Val (Intg i)⌉)" by(auto simp add: τmove1.simps τmoves1.simps)
moreover from bisim have s: "xcp = None" "xs = loc"
and "τExec_mover_a P t E h (stk, loc, pc, xcp) ([Intg i], loc, length (compE2 E), None)"
by(auto dest: bisim1Val2D1)
moreover from ‹i <s 0›
have "exec_meth_a (compP2 P) (compE2 (newA U⌊E⌉)) (compxE2 (newA U⌊E⌉) 0 0) t h ([Intg i], loc, length (compE2 E), None) ε h ([Intg i], loc, length (compE2 E), ⌊addr_of_sys_xcpt NegativeArraySize⌋)"
by -(rule exec_instr, auto simp add: compP2_def)
moreover have "τmove2 (compP2 P) h [Intg i] (newA U⌊E⌉) (length (compE2 E)) None ⟹ False" by(simp add: τmove2_iff)
moreover
have "P,newA U⌊E⌉,h ⊢ (THROW NegativeArraySize, loc) ↔ ([Intg i], loc, length (compE2 E), ⌊addr_of_sys_xcpt NegativeArraySize⌋)"
by(auto intro!: bisim1_bisims1.bisim1NewArrayFail)
ultimately show ?thesis using s
by(auto simp add: exec_move_def)(blast intro: NewArray_τExecrI)
next
case (Red1NewArrayFail i)
note [simp] = ‹e = Val (Intg i)› ‹e' = THROW OutOfMemory› ‹xs' = xs› ‹ta = ε› ‹h' = h›
and new = ‹allocate h (Array_type U (nat (sint i))) = {}›
have "¬ τmove1 P h (newA U⌊Val (Intg i)⌉)" by(auto simp add: τmove1.simps τmoves1.simps)
moreover from bisim have s: "xcp = None" "xs = loc"
and "τExec_mover_a P t E h (stk, loc, pc, xcp) ([Intg i], loc, length (compE2 E), None)"
by(auto dest: bisim1Val2D1)
moreover from ‹0 <=s i› new
have "exec_meth_a (compP2 P) (compE2 (newA U⌊E⌉)) (compxE2 (newA U⌊E⌉) 0 0) t h ([Intg i], loc, length (compE2 E), None) ε h' ([Intg i], loc, length (compE2 E), ⌊addr_of_sys_xcpt OutOfMemory⌋)"
by -(rule exec_instr, auto simp add: compP2_def)
moreover have "τmove2 (compP2 P) h [Intg i] (newA U⌊E⌉) (length (compE2 E)) None ⟹ False" by(simp add: τmove2_iff)
moreover
have "P,newA U⌊E⌉,h' ⊢ (THROW OutOfMemory, loc) ↔ ([Intg i], loc, length (compE2 E), ⌊addr_of_sys_xcpt OutOfMemory⌋)"
by(auto intro!: bisim1_bisims1.bisim1NewArrayFail)
ultimately show ?thesis using s by (auto simp add: exec_move_def)(blast intro: NewArray_τExecrI)
next
case (New1ArrayThrow a)
note [simp] = ‹e = Throw a› ‹h' = h› ‹xs' = xs› ‹ta = ε› ‹e' = Throw a›
have τ: "τmove1 P h (newA U⌊e⌉)" by(auto intro: τmove1NewArrayThrow)
from bisim have "xcp = ⌊a⌋ ∨ xcp = None" by(auto dest: bisim1_ThrowD)
thus ?thesis
proof
assume [simp]: "xcp = ⌊a⌋"
with bisim have "P,newA U⌊E⌉, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, xcp)"
by(auto intro: bisim1_bisims1.bisim1NewArrayThrow)
thus ?thesis using τ by(fastforce)
next
assume [simp]: "xcp = None"
with bisim obtain pc'
where "τExec_mover_a P t E h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
and bisim': "P, E, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)" and [simp]: "xs = loc"
by(auto dest: bisim1_Throw_τExec_mover)
hence "τExec_mover_a P t (newA U⌊E⌉) h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
by-(rule NewArray_τExecrI)
moreover from bisim' have "P, newA U⌊E⌉, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)"
by(rule bisim1_bisims1.bisim1NewArrayThrow)
ultimately show ?thesis using τ by auto
qed
qed
next
case bisim1NewArrayThrow thus ?case by auto
next
case bisim1NewArrayFail thus ?case by auto
next
case (bisim1Cast E n e xs stk loc pc xcp U)
note IH = bisim1Cast.IH(2)
note bisim = ‹P,E,h ⊢ (e, xs) ↔ (stk, loc, pc, xcp)›
note red = ‹True,P,t ⊢1 ⟨Cast U e,(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩›
note bsok = ‹bsok (Cast U E) n›
from red show ?case
proof cases
case (Cast1Red ee')
note [simp] = ‹e' = Cast U ee'›
and red = ‹True,P,t ⊢1 ⟨e,(h, xs)⟩ -ta→ ⟨ee', (h', xs')⟩›
from red have "τmove1 P h (Cast U e) = τmove1 P h e" by(auto simp add: τmove1.simps τmoves1.simps)
moreover from red have "call1 (Cast U e) = call1 e" by auto
moreover from IH[OF red] bsok
obtain pc'' stk'' loc'' xcp'' where bisim: "P,E,h' ⊢ (ee', xs') ↔ (stk'', loc'', pc'', xcp'')"
and redo: "?exec ta E e ee' h stk loc pc xcp h' pc'' stk'' loc'' xcp''" by auto
from bisim
have "P,Cast U E,h' ⊢ (Cast U ee', xs') ↔ (stk'', loc'', pc'', xcp'')"
by(rule bisim1_bisims1.bisim1Cast)
moreover {
assume "no_call2 E pc"
hence "no_call2 (Cast U E) pc" by(auto simp add: no_call2_def) }
ultimately show ?thesis using redo
by(auto simp del: call1.simps calls1.simps split: if_split_asm split del: if_split)(blast intro: Cast_τExecrI Cast_τExectI exec_move_CastI)+
next
case (Red1Cast c U')
hence [simp]: "e = Val c" "ta = ε" "e' = Val c" "h' = h" "xs' = xs"
and type: "typeof⇘h⇙ c = ⌊U'⌋" "P ⊢ U' ≤ U" by auto
from bisim have s: "xcp = None" "xs = loc" by(auto dest: bisim_Val_loc_eq_xcp_None)
from bisim have "τExec_mover_a P t E h (stk, loc, pc, xcp) ([c], loc, length (compE2 E), None)"
by(auto dest: bisim1Val2D1)
hence "τExec_mover_a P t (Cast U E) h (stk, loc, pc, xcp) ([c], loc, length (compE2 E), None)"
by(rule Cast_τExecrI)
moreover from type
have "exec_meth_a (compP2 P) (compE2 (Cast U E)) (compxE2 (Cast U E) 0 0) t h ([c], loc, length (compE2 E), None) ε h' ([c], loc, Suc (length (compE2 E)), None)"
by(auto intro!: exec_instr simp add: compP2_def)
moreover have "τmove2 (compP2 P) h [c] (Cast U E) (length (compE2 E)) None" by(simp add: τmove2_iff)
ultimately have "τExec_mover_a P t (Cast U E) h (stk, loc, pc, xcp) ([c], loc, Suc (length (compE2 E)), None)"
by(fastforce elim: rtranclp.rtrancl_into_rtrancl intro: τexec_moveI simp add: exec_move_def compP2_def)
moreover have "τmove1 P h (Cast U (Val c))" by(rule τmove1CastRed)
moreover
have "P, Cast U E, h' ⊢ (Val c, loc) ↔ ([c], loc, length (compE2 (Cast U E)), None)"
by(rule bisim1Val2) simp
ultimately show ?thesis using s by(auto simp add: exec_move_def)
next
case (Red1CastFail v U')
note [simp] = ‹e = Val v› ‹e' = THROW ClassCast› ‹h' = h› ‹xs' = xs› ‹ta = ε›
moreover from bisim have s: "xcp = None" "xs = loc"
and "τExec_mover_a P t E h (stk, loc, pc, xcp) ([v], loc, length (compE2 E), None)"
by(auto dest: bisim1Val2D1)
hence "τExec_mover_a P t (Cast U E) h (stk, loc, pc, xcp) ([v], loc, length (compE2 E), None)"
by(auto elim: Cast_τExecrI)
moreover from ‹typeof⇘hp (h, xs)⇙ v = ⌊U'⌋› ‹¬ P ⊢ U' ≤ U›
have "exec_meth_a (compP2 P) (compE2 (Cast U E)) (compxE2 (Cast U E) 0 0) t h ([v], loc, length (compE2 E), None) ε h ([v], loc, length (compE2 E), ⌊addr_of_sys_xcpt ClassCast⌋)"
by -(rule exec_instr, auto simp add: compP2_def)
moreover have "τmove2 (compP2 P) h [v] (Cast U E) (length (compE2 E)) None" by(simp add: τmove2_iff)
ultimately have "τExec_movet_a P t (Cast U E) h (stk, loc, pc, xcp) ([v], loc, length (compE2 E), ⌊addr_of_sys_xcpt ClassCast⌋)"
by(fastforce simp add: exec_move_def compP2_def intro: rtranclp_into_tranclp1 τexec_moveI)
moreover have "τmove1 P h (Cast U (Val v))" by(rule τmove1CastRed)
moreover
have "P,Cast U E,h ⊢ (THROW ClassCast, loc) ↔ ([v], loc, length (compE2 E), ⌊addr_of_sys_xcpt ClassCast⌋)"
by(auto intro!: bisim1_bisims1.bisim1CastFail)
ultimately show ?thesis using s by(auto simp add: exec_move_def)
next
case [simp]: (Cast1Throw a)
have τ: "τmove1 P h (Cast U e)" by(auto intro: τmove1CastThrow)
from bisim have "xcp = ⌊a⌋ ∨ xcp = None" by(auto dest: bisim1_ThrowD)
thus ?thesis
proof
assume [simp]: "xcp = ⌊a⌋"
with bisim have "P,Cast U E, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, xcp)"
by(auto intro: bisim1_bisims1.bisim1CastThrow)
thus ?thesis using τ by(fastforce)
next
assume [simp]: "xcp = None"
with bisim obtain pc'
where "τExec_mover_a P t E h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
and bisim': "P, E, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)" and [simp]: "xs = loc"
by(auto dest: bisim1_Throw_τExec_mover)
hence "τExec_mover_a P t (Cast U E) h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
by-(rule Cast_τExecrI)
moreover from bisim' have "P, Cast U E, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)"
by-(rule bisim1_bisims1.bisim1CastThrow, auto)
ultimately show ?thesis using τ by auto
qed
qed
next
case bisim1CastThrow thus ?case by auto
next
case bisim1CastFail thus ?case by auto
next
case (bisim1InstanceOf E n e xs stk loc pc xcp U)
note IH = bisim1InstanceOf(2)
note bisim = ‹P,E,h ⊢ (e, xs) ↔ (stk, loc, pc, xcp)›
note red = ‹True,P,t ⊢1 ⟨e instanceof U,(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩›
note bsok = ‹bsok (E instanceof U) n›
from red show ?case
proof cases
case (InstanceOf1Red ee')
note [simp] = ‹e' = ee' instanceof U›
and red = ‹True,P,t ⊢1 ⟨e,(h, xs)⟩ -ta→ ⟨ee', (h', xs')⟩›
from red have "τmove1 P h (e instanceof U) = τmove1 P h e" by(auto simp add: τmove1.simps τmoves1.simps)
moreover from red have "call1 (e instanceof U) = call1 e" by auto
moreover from IH[OF red] bsok
obtain pc'' stk'' loc'' xcp'' where bisim: "P,E,h' ⊢ (ee', xs') ↔ (stk'', loc'', pc'', xcp'')"
and redo: "?exec ta E e ee' h stk loc pc xcp h' pc'' stk'' loc'' xcp''" by auto
from bisim
have "P,E instanceof U,h' ⊢ (ee' instanceof U, xs') ↔ (stk'', loc'', pc'', xcp'')"
by(rule bisim1_bisims1.bisim1InstanceOf)
moreover {
assume "no_call2 E pc"
hence "no_call2 (E instanceof U) pc" by(auto simp add: no_call2_def) }
ultimately show ?thesis using redo
by(auto simp del: call1.simps calls1.simps split: if_split_asm split del: if_split)(blast intro: InstanceOf_τExecrI InstanceOf_τExectI exec_move_InstanceOfI)+
next
case (Red1InstanceOf c U' b)
hence [simp]: "e = Val c" "ta = ε" "e' = Val (Bool (c ≠ Null ∧ P ⊢ U' ≤ U))" "h' = h" "xs' = xs"
"b = (c ≠ Null ∧ P ⊢ U' ≤ U)"
and type: "typeof⇘h⇙ c = ⌊U'⌋" by auto
from bisim have s: "xcp = None" "xs = loc" by(auto dest: bisim_Val_loc_eq_xcp_None)
from bisim have "τExec_mover_a P t E h (stk, loc, pc, xcp) ([c], loc, length (compE2 E), None)"
by(auto dest: bisim1Val2D1)
hence "τExec_mover_a P t (E instanceof U) h (stk, loc, pc, xcp) ([c], loc, length (compE2 E), None)"
by(rule InstanceOf_τExecrI)
moreover from type
have "exec_meth_a (compP2 P) (compE2 (E instanceof U)) (compxE2 (E instanceof U) 0 0) t h ([c], loc, length (compE2 E), None) ε h' ([Bool b], loc, Suc (length (compE2 E)), None)"
by(auto intro!: exec_instr simp add: compP2_def)
moreover have "τmove2 (compP2 P) h [c] (E instanceof U) (length (compE2 E)) None" by(simp add: τmove2_iff)
ultimately have "τExec_mover_a P t (E instanceof U) h (stk, loc, pc, xcp) ([Bool b], loc, Suc (length (compE2 E)), None)"
by(fastforce elim: rtranclp.rtrancl_into_rtrancl intro: τexec_moveI simp add: exec_move_def compP2_def)
moreover have "τmove1 P h ((Val c) instanceof U)" by(rule τmove1InstanceOfRed)
moreover
have "P, E instanceof U, h' ⊢ (Val (Bool b), loc) ↔ ([Bool b], loc, length (compE2 (E instanceof U)), None)"
by(rule bisim1Val2) simp
ultimately show ?thesis using s by(auto simp add: exec_move_def)
next
case (InstanceOf1Throw a)
note [simp] = ‹e = Throw a› ‹h' = h› ‹xs' = xs› ‹ta = ε› ‹e' = Throw a›
have τ: "τmove1 P h (e instanceof U)" by(auto intro: τmove1InstanceOfThrow)
from bisim have "xcp = ⌊a⌋ ∨ xcp = None" by(auto dest: bisim1_ThrowD)
thus ?thesis
proof
assume [simp]: "xcp = ⌊a⌋"
with bisim have "P,E instanceof U, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, xcp)"
by(auto intro: bisim1_bisims1.bisim1InstanceOfThrow)
thus ?thesis using τ by(fastforce)
next
assume [simp]: "xcp = None"
with bisim obtain pc'
where "τExec_mover_a P t E h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
and bisim': "P, E, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)" and [simp]: "xs = loc"
by(auto dest: bisim1_Throw_τExec_mover)
hence "τExec_mover_a P t (E instanceof U) h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
by-(rule InstanceOf_τExecrI)
moreover from bisim' have "P, E instanceof U, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)"
by-(rule bisim1_bisims1.bisim1InstanceOfThrow, auto)
ultimately show ?thesis using τ by auto
qed
qed
next
case bisim1InstanceOfThrow thus ?case by auto
next
case bisim1Val thus ?case by fastforce
next
case (bisim1Var V n xs)
from ‹True,P,t ⊢1 ⟨Var V,(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩› show ?case
proof cases
case (Red1Var v)
hence "exec_meth_a (compP2 P) [Load V] [] t h ([], xs, 0, None) ε h ([v], xs, 1, None)"
and [simp]: "ta = ε" "h' = h" "xs' = xs" "e' = Val v"
by(auto intro: exec_instr)
moreover have "τmove2 (compP2 P) h [] (Var V) 0 None" by(simp add: τmove2_iff)
ultimately have "τExec_movet_a P t (Var V) h ([], xs, 0, None) ([v], xs, 1, None)"
by(auto intro: τExect1step simp add: exec_move_def compP2_def)
moreover have "P, Var V, h ⊢ (Val v, xs) ↔ ([v], xs, length (compE2 (Var V)), None)"
by(rule bisim1Val2) simp
moreover have "τmove1 P h (Var V)" by(rule τmove1Var)
ultimately show ?thesis by(fastforce)
qed
next
case (bisim1BinOp1 e1 n e1' xs stk loc pc xcp e2 bop)
note IH1 = bisim1BinOp1.IH(2)
note IH2 = bisim1BinOp1.IH(4)
note bisim1 = ‹P,e1,h ⊢ (e1', xs) ↔ (stk, loc, pc, xcp)›
note bisim2 = ‹⋀xs. P,e2,h ⊢ (e2, xs) ↔ ([], xs, 0, None)›
note bsok = ‹bsok (e1 «bop» e2) n›
from ‹True,P,t ⊢1 ⟨e1' «bop» e2,(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩› show ?case
proof cases
case (Bin1OpRed1 E')
note [simp] = ‹e' = E' «bop» e2›
and red = ‹True,P,t ⊢1 ⟨e1',(h, xs)⟩ -ta→ ⟨E',(h', xs')⟩›
from red have "τmove1 P h (e1' «bop» e2) = τmove1 P h e1'" by(auto simp add: τmove1.simps τmoves1.simps)
moreover from red have "call1 (e1' «bop» e2) = call1 e1'" by auto
moreover from IH1[OF red] bsok
obtain pc'' stk'' loc'' xcp'' where bisim: "P,e1,h' ⊢ (E', xs') ↔ (stk'', loc'', pc'', xcp'')"
and redo: "?exec ta e1 e1' E' h stk loc pc xcp h' pc'' stk'' loc'' xcp''" by auto
from bisim
have "P,e1«bop»e2,h' ⊢ (E'«bop»e2, xs') ↔ (stk'', loc'', pc'', xcp'')"
by(rule bisim1_bisims1.bisim1BinOp1)
moreover {
assume "no_call2 e1 pc"
hence "no_call2 (e1«bop»e2) pc ∨ pc = length (compE2 e1)" by(auto simp add: no_call2_def) }
ultimately show ?thesis using redo
by(auto simp del: call1.simps calls1.simps split: if_split_asm split del: if_split)(blast intro: BinOp_τExecrI1 BinOp_τExectI1 exec_move_BinOpI1)+
next
case (Bin1OpRed2 E' v)
note [simp] = ‹e1' = Val v› ‹e' = Val v «bop» E'›
and red = ‹True,P,t ⊢1 ⟨e2,(h, xs)⟩ -ta→ ⟨E',(h', xs')⟩›
from red have τ: "τmove1 P h (Val v «bop» e2) = τmove1 P h e2" by(auto simp add: τmove1.simps τmoves1.simps)
from bisim1 have s: "xcp = None" "xs = loc"
and exec1: "τExec_mover_a P t e1 h (stk, loc, pc, None) ([v], xs, length (compE2 e1), None)"
by(auto dest: bisim1Val2D1)
from exec1 have "τExec_mover_a P t (e1«bop»e2) h (stk, loc, pc, None) ([v], xs, length (compE2 e1), None)"
by(rule BinOp_τExecrI1)
moreover
from IH2[OF red] bsok obtain pc'' stk'' loc'' xcp''
where bisim': "P,e2,h' ⊢ (E', xs') ↔ (stk'', loc'', pc'', xcp'')"
and exec': "?exec ta e2 e2 E' h [] xs 0 None h' pc'' stk'' loc'' xcp''" by auto
have "?exec ta (e1«bop»e2) (Val v«bop»e2) (Val v«bop»E') h ([] @ [v]) xs (length (compE2 e1) + 0) None h' (length (compE2 e1) + pc'') (stk'' @ [v]) loc'' xcp''"
proof(cases "τmove1 P h (Val v «bop» e2)")
case True
with exec' τ have [simp]: "h = h'" and e: "sim_move e2 E' P t e2 h ([], xs, 0, None) (stk'', loc'', pc'', xcp'')" by auto
from e have "sim_move (Val v«bop»e2) (Val v«bop»E') P t (e1 «bop» e2) h ([] @ [v], xs, length (compE2 e1) + 0, None) (stk'' @ [v], loc'', length (compE2 e1) + pc'', xcp'')"
by(fastforce dest: BinOp_τExecrI2 BinOp_τExectI2)
with True show ?thesis by auto
next
case False
with exec' τ obtain pc' stk' loc' xcp'
where e: "τExec_mover_a P t e2 h ([], xs, 0, None) (stk', loc', pc', xcp')"
and e': "exec_move_a P t e2 h (stk', loc', pc', xcp') (extTA2JVM (compP2 P) ta) h' (stk'', loc'', pc'', xcp'')"
and τ': "¬ τmove2 (compP2 P) h stk' e2 pc' xcp'"
and call: "call1 e2 = None ∨ no_call2 e2 0 ∨ pc' = 0 ∧ stk' = [] ∧ loc' = xs ∧ xcp' = None" by auto
from e have "τExec_mover_a P t (e1 «bop» e2) h ([] @ [v], xs, length (compE2 e1) + 0, None) (stk' @ [v], loc', length (compE2 e1) + pc', xcp')" by(rule BinOp_τExecrI2)
moreover from e' have "exec_move_a P t (e1 «bop» e2) h (stk' @ [v], loc', length (compE2 e1) + pc', xcp') (extTA2JVM (compP2 P) ta) h' (stk'' @ [v], loc'', length (compE2 e1) + pc'', xcp'')"
by(rule exec_move_BinOpI2)
moreover from e' have "pc' < length (compE2 e2)" by auto
with τ' e' have "¬ τmove2 (compP2 P) h (stk' @ [v]) (e1 «bop» e2) (length (compE2 e1) + pc') xcp'"
moreover from red have "call1 (e1'«bop»e2) = call1 e2" by(auto)
moreover have "no_call2 e2 0 ⟹ no_call2 (e1«bop»e2) (length (compE2 e1))"
ultimately show ?thesis using False call
by(auto simp del: split_paired_Ex call1.simps calls1.simps) blast
qed
moreover from bisim'
have "P,e1«bop»e2,h' ⊢ (Val v«bop»E', xs') ↔ ((stk'' @ [v]), loc'', length (compE2 e1) + pc'', xcp'')"
by(rule bisim1_bisims1.bisim1BinOp2)
moreover from bisim1 have "pc ≠ length (compE2 e1) ⟶ no_call2 (e1«bop»e2) pc"
by(auto simp add: no_call2_def dest: bisim_Val_pc_not_Invoke bisim1_pc_length_compE2)
ultimately show ?thesis using τ exec1 s
apply(auto simp del: split_paired_Ex call1.simps calls1.simps split: if_split_asm split del: if_split)
apply(blast intro: τExec_mover_trans|fastforce elim!: τExec_mover_trans simp del: split_paired_Ex call1.simps calls1.simps)+
done
next
case (Red1BinOp v1 v2 v)
note [simp] = ‹e1' = Val v1› ‹e2 = Val v2› ‹ta = ε› ‹e' = Val v› ‹h' = h› ‹xs' = xs›
and binop = ‹binop bop v1 v2 = ⌊Inl v⌋›
have τ: "τmove1 P h (Val v1 «bop» Val v2)" by(rule τmove1BinOp)
from bisim1 have s: "xcp = None" "xs = loc"
and "τExec_mover_a P t e1 h (stk, loc, pc, xcp) ([v1], loc, length (compE2 e1), None)"
by(auto dest: bisim1Val2D1)
hence "τExec_mover_a P t (e1«bop»Val v2) h (stk, loc, pc, xcp) ([v1], loc, length (compE2 e1), None)"
by-(rule BinOp_τExecrI1)
also have "τmove2 (compP2 P) h [v1] (e1 «bop» Val v2) (length (compE2 e1) + 0) None"
by(rule τmove2BinOp2)(rule τmove2Val)
with binop have "τExec_mover_a P t (e1«bop»Val v2) h ([v1], loc, length (compE2 e1), None) ([v2, v1], loc, Suc (length (compE2 e1)), None)"
by-(rule τExecr1step, auto intro!: exec_instr simp add: exec_move_def compP2_def)
also (rtranclp_trans) from binop
have "exec_meth_a (compP2 P) (compE2 (e1«bop»Val v2)) (compxE2 (e1«bop»Val v2) 0 0) t
h ([v2, v1], loc, Suc (length (compE2 e1)), None) ε
h ([v], loc, Suc (Suc (length (compE2 e1))), None)"
by-(rule exec_instr, auto)
moreover have "τmove2 (compP2 P) h [v2, v1] (e1«bop»Val v2) (Suc (length (compE2 e1))) None" by(simp add: τmove2_iff)
ultimately have "τExec_mover_a P t (e1 «bop» Val v2) h (stk, loc, pc, xcp) ([v], loc, Suc (Suc (length (compE2 e1))), None)"
by(fastforce intro: rtranclp.rtrancl_into_rtrancl τexec_moveI simp add: exec_move_def compP2_def)
moreover
have "P, e1 «bop» Val v2, h ⊢ (Val v, loc) ↔ ([v], loc, length (compE2 (e1 «bop» Val v2)), None)"
by(rule bisim1Val2) simp
ultimately show ?thesis using s τ by auto
next
case (Red1BinOpFail v1 v2 a)
note [simp] = ‹e1' = Val v1› ‹e2 = Val v2› ‹ta = ε› ‹e' = Throw a› ‹h' = h› ‹xs' = xs›
and binop = ‹binop bop v1 v2 = ⌊Inr a⌋›
have τ: "τmove1 P h (Val v1 «bop» Val v2)" by(rule τmove1BinOp)
from bisim1 have s: "xcp = None" "xs = loc"
and "τExec_mover_a P t e1 h (stk, loc, pc, xcp) ([v1], loc, length (compE2 e1), None)"
by(auto dest: bisim1Val2D1)
hence "τExec_mover_a P t (e1«bop»Val v2) h (stk, loc, pc, xcp) ([v1], loc, length (compE2 e1), None)"
by-(rule BinOp_τExecrI1)
also have "τmove2 (compP2 P) h [v1] (e1 «bop» Val v2) (length (compE2 e1) + 0) None"
by(rule τmove2BinOp2)(rule τmove2Val)
with binop have "τExec_mover_a P t (e1«bop»Val v2) h ([v1], loc, length (compE2 e1), None) ([v2, v1], loc, Suc (length (compE2 e1)), None)"
by-(rule τExecr1step, auto intro!: exec_instr simp add: exec_move_def compP2_def)
also (rtranclp_trans) from binop
have "exec_meth_a (compP2 P) (compE2 (e1«bop»Val v2)) (compxE2 (e1«bop»Val v2) 0 0) t
h ([v2, v1], loc, Suc (length (compE2 e1)), None) ε
h ([v2, v1], loc, Suc (length (compE2 e1)), ⌊a⌋)"
by-(rule exec_instr, auto)
moreover have "τmove2 (compP2 P) h [v2, v1] (e1«bop»Val v2) (Suc (length (compE2 e1))) None" by(simp add: τmove2_iff)
ultimately have "τExec_movet_a P t (e1 «bop» Val v2) h (stk, loc, pc, xcp) ([v2, v1], loc, Suc (length (compE2 e1)), ⌊a⌋)"
by(fastforce intro: rtranclp_into_tranclp1 τexec_moveI simp add: exec_move_def compP2_def)
moreover
have "P, e1 «bop» Val v2, h ⊢ (Throw a, loc) ↔ ([v2, v1], loc, length (compE2 e1) + length (compE2 (Val v2)), ⌊a⌋)"
by(rule bisim1BinOpThrow)
ultimately show ?thesis using s τ by auto
next
case (Bin1OpThrow1 a)
note [simp] = ‹e1' = Throw a› ‹ta = ε› ‹e' = Throw a› ‹h' = h› ‹xs' = xs›
have τ: "τmove1 P h (Throw a «bop» e2)" by(rule τmove1BinOpThrow1)
from bisim1 have "xcp = ⌊a⌋ ∨ xcp = None" by(auto dest: bisim1_ThrowD)
thus ?thesis
proof
assume [simp]: "xcp = ⌊a⌋"
with bisim1 have "P, e1«bop»e2, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, xcp)"
by(auto intro: bisim1_bisims1.intros)
thus ?thesis using τ by(fastforce)
next
assume [simp]: "xcp = None"
with bisim1 obtain pc' where "τExec_mover_a P t e1 h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
and bisim': "P, e1, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)"
and [simp]: "xs = loc"
by(auto dest: bisim1_Throw_τExec_mover)
hence "τExec_mover_a P t (e1«bop»e2) h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
by-(rule BinOp_τExecrI1)
moreover from bisim'
have "P, e1«bop»e2, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)"
by(auto intro: bisim1_bisims1.bisim1BinOpThrow1)
ultimately show ?thesis using τ by auto
qed
next
case (Bin1OpThrow2 v a)
note [simp] = ‹e1' = Val v› ‹e2 = Throw a› ‹ta = ε› ‹e' = Throw a› ‹h' = h› ‹xs' = xs›
from bisim1 have s: "xcp = None" "xs = loc"
and "τExec_mover_a P t e1 h (stk, loc, pc, xcp) ([v], loc, length (compE2 e1), None)"
by(auto dest: bisim1Val2D1)
hence "τExec_mover_a P t (e1«bop»Throw a) h (stk, loc, pc, xcp) ([v], loc, length (compE2 e1), None)"
by-(rule BinOp_τExecrI1)
also have "τExec_mover_a P t (e1«bop»Throw a) h ([v], loc, length (compE2 e1), None) ([Addr a, v], loc, Suc (length (compE2 e1)), ⌊a⌋)"
by(rule τExecr2step)(auto simp add: exec_move_def exec_meth_instr τmove2_iff τmove1.simps τmoves1.simps)
also (rtranclp_trans)
have "P,e1«bop»Throw a,h ⊢ (Throw a, loc) ↔ ([Addr a] @ [v], loc, (length (compE2 e1) + length (compE2 (addr a))), ⌊a⌋)"
by(rule bisim1BinOpThrow2[OF bisim1Throw2])
moreover have "τmove1 P h (e1' «bop» e2)" by(auto intro: τmove1BinOpThrow2)
ultimately show ?thesis using s by auto
qed
next
case (bisim1BinOp2 e2 n e2' xs stk loc pc xcp e1 bop v1)
note IH2 = bisim1BinOp2.IH(2)
note bisim1 = ‹⋀xs. P,e1,h ⊢ (e1, xs) ↔ ([], xs, 0, None)›
note bisim2 = ‹P,e2,h ⊢ (e2', xs) ↔ (stk, loc, pc, xcp)›
note red = ‹True,P,t ⊢1 ⟨Val v1 «bop» e2',(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩›
note bsok = ‹bsok (e1 «bop» e2) n›
from red show ?case
proof cases
case (Bin1OpRed2 E')
note [simp] = ‹e' = Val v1 «bop» E'›
and red = ‹True,P,t ⊢1 ⟨e2',(h, xs)⟩ -ta→ ⟨E',(h', xs')⟩›
from IH2[OF red] bsok obtain pc'' stk'' loc'' xcp''
where bisim': "P,e2,h' ⊢ (E', xs') ↔ (stk'', loc'', pc'', xcp'')"
and exec': "?exec ta e2 e2' E' h stk loc pc xcp h' pc'' stk'' loc'' xcp''" by auto
from red have τ: "τmove1 P h (Val v1 «bop» e2') = τmove1 P h e2'" by(auto simp add: τmove1.simps τmoves1.simps)
have "no_call2 e2 pc ⟹ no_call2 (e1 «bop» e2) (length (compE2 e1) + pc)" by(auto simp add: no_call2_def)
hence "?exec ta (e1«bop»e2) (Val v1«bop»e2') (Val v1«bop»E') h (stk @ [v1]) loc (length (compE2 e1) + pc) xcp h' (length (compE2 e1) + pc'') (stk'' @ [v1]) loc'' xcp''"
using exec' τ
apply(cases "τmove1 P h (Val v1 «bop» e2')")
apply(auto)
apply(blast intro: BinOp_τExecrI2 BinOp_τExectI2 exec_move_BinOpI2)
apply(blast intro: BinOp_τExecrI2 BinOp_τExectI2 exec_move_BinOpI2)
apply(rule exI conjI BinOp_τExecrI2 exec_move_BinOpI2|assumption)+
apply(fastforce simp add: τinstr_stk_drop_exec_move τmove2_iff split: if_split_asm)
apply(rule exI conjI BinOp_τExecrI2 exec_move_BinOpI2|assumption)+
apply(fastforce simp add: τinstr_stk_drop_exec_move τmove2_iff split: if_split_asm)
apply(rule exI conjI BinOp_τExecrI2 exec_move_BinOpI2 rtranclp.rtrancl_refl|assumption)+
apply(fastforce simp add: τinstr_stk_drop_exec_move τmove2_iff split: if_split_asm)+
done
moreover from bisim'
have "P,e1«bop»e2,h' ⊢ (Val v1«bop»E', xs') ↔ (stk''@[v1], loc'', length (compE2 e1) + pc'', xcp'')"
by(rule bisim1_bisims1.bisim1BinOp2)
ultimately show ?thesis using τ by auto blast+
next
case (Red1BinOp v2 v)
note [simp] = ‹e2' = Val v2› ‹ta = ε› ‹e' = Val v› ‹h' = h› ‹xs' = xs›
and binop = ‹binop bop v1 v2 = ⌊Inl v⌋›
have τ: "τmove1 P h (Val v1 «bop» Val v2)" by(rule τmove1BinOp)
from bisim2 have s: "xcp = None" "xs = loc"
and "τExec_mover_a P t e2 h (stk, loc, pc, xcp) ([v2], loc, length (compE2 e2), None)"
by(auto dest: bisim1Val2D1)
hence "τExec_mover_a P t (e1«bop»e2) h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ([v2] @ [v1], loc, length (compE2 e1) + length (compE2 e2), None)"
by-(rule BinOp_τExecrI2)
moreover from binop
have "exec_move_a P t (e1«bop»e2) h ([v2, v1], loc, length (compE2 e1) + length (compE2 e2), None) ε
h ([v], loc, Suc (length (compE2 e1) + length (compE2 e2)), None)"
unfolding exec_move_def by-(rule exec_instr, auto)
moreover have "τmove2 (compP2 P) h [v2, v1] (e1«bop»e2) (length (compE2 e1) + length (compE2 e2)) None"
ultimately have "τExec_mover_a P t (e1 «bop» e2) h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ([v], loc, Suc (length (compE2 e1) + length (compE2 e2)), None)"
by(auto intro: rtranclp.rtrancl_into_rtrancl τexec_moveI simp add: compP2_def)
moreover
have "P, e1 «bop» e2, h ⊢ (Val v, loc) ↔ ([v], loc, length (compE2 (e1 «bop» e2)), None)"
by(rule bisim1Val2) simp
ultimately show ?thesis using s τ by(auto)
next
case (Red1BinOpFail v2 a)
note [simp] = ‹e2' = Val v2› ‹ta = ε› ‹e' = Throw a› ‹h' = h› ‹xs' = xs›
and binop = ‹binop bop v1 v2 = ⌊Inr a⌋›
have τ: "τmove1 P h (Val v1 «bop» Val v2)" by(rule τmove1BinOp)
from bisim2 have s: "xcp = None" "xs = loc"
and "τExec_mover_a P t e2 h (stk, loc, pc, xcp) ([v2], loc, length (compE2 e2), None)"
by(auto dest: bisim1Val2D1)
hence "τExec_mover_a P t (e1«bop»e2) h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ([v2] @ [v1], loc, length (compE2 e1) + length (compE2 e2), None)"
by-(rule BinOp_τExecrI2)
moreover from binop
have "exec_move_a P t (e1«bop»e2) h ([v2, v1], loc, length (compE2 e1) + length (compE2 e2), None) ε
h ([v2, v1], loc, length (compE2 e1) + length (compE2 e2), ⌊a⌋)"
unfolding exec_move_def by-(rule exec_instr, auto)
moreover have "τmove2 (compP2 P) h [v2, v1] (e1«bop»e2) (length (compE2 e1) + length (compE2 e2)) None"