# Theory Correctness2

```(*  Title:      JinjaDCI/Compiler/Correctness2.thy
Author:     Tobias Nipkow, Susannah Mansky

Based on the Jinja theory Compiler/Correctness2.thy by Tobias Nipkow
*)

section ‹ Correctness of Stage 2 ›

theory Correctness2
imports "HOL-Library.Sublist" Compiler2 J1WellForm "../J/EConform"
begin

(*<*)hide_const (open) Throw(*>*)

subsection‹ Instruction sequences ›

text‹ How to select individual instructions and subsequences of
instructions from a program given the class, method and program
counter. ›

definition before :: "jvm_prog ⇒ cname ⇒ mname ⇒ nat ⇒ instr list ⇒ bool"
("(_,_,_,_/ ⊳ _)" [51,0,0,0,51] 50) where
"P,C,M,pc ⊳ is ⟷ prefix is (drop pc (instrs_of P C M))"

definition at :: "jvm_prog ⇒ cname ⇒ mname ⇒ nat ⇒ instr ⇒ bool"
("(_,_,_,_/ ▹ _)" [51,0,0,0,51] 50) where
"P,C,M,pc ▹ i ⟷ (∃is. drop pc (instrs_of P C M) = i#is)"

lemma [simp]: "P,C,M,pc ⊳ []"

lemma [simp]: "P,C,M,pc ⊳ (i#is) = (P,C,M,pc ▹ i ∧ P,C,M,pc + 1 ⊳ is)"
(*<*)by(fastforce simp add:before_def at_def prefix_def drop_Suc drop_tl)(*>*)

(*<*)
declare drop_drop[simp del]
(*>*)

lemma [simp]: "P,C,M,pc ⊳ (is⇩1 @ is⇩2) = (P,C,M,pc ⊳ is⇩1 ∧ P,C,M,pc + size is⇩1 ⊳ is⇩2)"
(*<*)
(*>*)

(*<*)
declare drop_drop[simp]
(*>*)

lemma [simp]: "P,C,M,pc ▹ i ⟹ instrs_of P C M ! pc = i"

lemma beforeM:
"P ⊢ C sees M,b: Ts→T = body in D ⟹
compP⇩2 P,D,M,0 ⊳ compE⇩2 body @ [Return]"

text‹ This lemma executes a single instruction by rewriting: ›

lemma [simp]:
"P,C,M,pc ▹ instr ⟹
(P ⊢ (None, h, (vs,ls,C,M,pc,ics) # frs, sh) -jvm→ σ') =
((None, h, (vs,ls,C,M,pc,ics) # frs, sh) = σ' ∨
(∃σ. exec(P,(None, h, (vs,ls,C,M,pc,ics) # frs, sh)) = Some σ ∧ P ⊢ σ -jvm→ σ'))"
(*<*)
by(simp only: exec_all_def)
(blast intro: converse_rtranclE converse_rtrancl_into_rtrancl)
(*>*)

subsection‹ Exception tables ›

definition pcs :: "ex_table ⇒ nat set"
where
"pcs xt  ≡  ⋃(f,t,C,h,d) ∈ set xt. {f ..< t}"

lemma pcs_subset:
shows "(⋀pc d. pcs(compxE⇩2 e pc d) ⊆ {pc..<pc+size(compE⇩2 e)})"
and "(⋀pc d. pcs(compxEs⇩2 es pc d) ⊆ {pc..<pc+size(compEs⇩2 es)})"
(*<*)
proof(induct e and es rule: compxE⇩2.induct compxEs⇩2.induct)
case Cast then show ?case by (fastforce simp:pcs_def)
next
case BinOp then show ?case by (fastforce simp:pcs_def split:bop.splits)
next
case LAss then show ?case by (fastforce simp: pcs_def)
next
case FAcc then show ?case by (fastforce simp: pcs_def)
next
case FAss then show ?case by (fastforce simp: pcs_def)
next
case SFAss then show ?case by (fastforce simp: pcs_def)
next
case Call then show ?case by (fastforce simp: pcs_def)
next
case SCall then show ?case by (fastforce simp: pcs_def)
next
case Seq then show ?case by (fastforce simp: pcs_def)
next
case Cond then show ?case by (fastforce simp: pcs_def)
next
case While then show ?case by (fastforce simp: pcs_def)
next
case throw then show ?case by (fastforce simp: pcs_def)
next
case TryCatch then show ?case by (fastforce simp: pcs_def)
next
case Cons_exp then show ?case by (fastforce simp: pcs_def)
(*>*)

lemma [simp]: "pcs [] = {}"

lemma [simp]: "pcs (x#xt) = {fst x ..< fst(snd x)} ∪ pcs xt"

lemma [simp]: "pcs(xt⇩1 @ xt⇩2) = pcs xt⇩1 ∪ pcs xt⇩2"

lemma [simp]: "pc < pc⇩0 ∨ pc⇩0+size(compE⇩2 e) ≤ pc ⟹ pc ∉ pcs(compxE⇩2 e pc⇩0 d)"
(*<*)using pcs_subset by fastforce(*>*)

lemma [simp]: "pc < pc⇩0 ∨ pc⇩0+size(compEs⇩2 es) ≤ pc ⟹ pc ∉ pcs(compxEs⇩2 es pc⇩0 d)"
(*<*)using pcs_subset by fastforce(*>*)

lemma [simp]: "pc⇩1 + size(compE⇩2 e⇩1) ≤ pc⇩2 ⟹ pcs(compxE⇩2 e⇩1 pc⇩1 d⇩1) ∩ pcs(compxE⇩2 e⇩2 pc⇩2 d⇩2) = {}"
(*<*)using pcs_subset by fastforce(*>*)

lemma [simp]: "pc⇩1 + size(compE⇩2 e) ≤ pc⇩2 ⟹ pcs(compxE⇩2 e pc⇩1 d⇩1) ∩ pcs(compxEs⇩2 es pc⇩2 d⇩2) = {}"
(*<*)using pcs_subset by fastforce(*>*)

lemma [simp]:
"pc ∉ pcs xt⇩0 ⟹ match_ex_table P C pc (xt⇩0 @ xt⇩1) = match_ex_table P C pc xt⇩1"
(*<*)by (induct xt⇩0) (auto simp: matches_ex_entry_def)(*>*)

lemma [simp]: "⟦ x ∈ set xt; pc ∉ pcs xt ⟧ ⟹ ¬ matches_ex_entry P D pc x"
(*<*)by(auto simp:matches_ex_entry_def pcs_def)(*>*)

lemma [simp]:
assumes xe: "xe ∈ set(compxE⇩2 e pc d)" and outside: "pc' < pc ∨ pc+size(compE⇩2 e) ≤ pc'"
shows "¬ matches_ex_entry P C pc' xe"
(*<*)
proof
assume "matches_ex_entry P C pc' xe"
with xe have "pc' ∈ pcs(compxE⇩2 e pc d)"
with outside show False by simp
qed
(*>*)

lemma [simp]:
assumes xe: "xe ∈ set(compxEs⇩2 es pc d)" and outside: "pc' < pc ∨ pc+size(compEs⇩2 es) ≤ pc'"
shows "¬ matches_ex_entry P C pc' xe"
(*<*)
proof
assume "matches_ex_entry P C pc' xe"
with xe have "pc' ∈ pcs(compxEs⇩2 es pc d)"
with outside show False by simp
qed
(*>*)

lemma match_ex_table_app[simp]:
"∀xte ∈ set xt⇩1. ¬ matches_ex_entry P D pc xte ⟹
match_ex_table P D pc (xt⇩1 @ xt) = match_ex_table P D pc xt"
(*<*)by(induct xt⇩1) simp_all(*>*)

lemma [simp]:
"∀x ∈ set xtab. ¬ matches_ex_entry P C pc x ⟹
match_ex_table P C pc xtab = None"
(*<*)using match_ex_table_app[where ?xt = "[]"] by fastforce(*>*)

lemma match_ex_entry:
"matches_ex_entry P C pc (start, end, catch_type, handler) =
(start ≤ pc ∧ pc < end ∧  P ⊢ C ≼⇧* catch_type)"

definition caught :: "jvm_prog ⇒ pc ⇒ heap ⇒ addr ⇒ ex_table ⇒ bool" where
"caught P pc h a xt ⟷
(∃entry ∈ set xt. matches_ex_entry P (cname_of h a) pc entry)"

definition beforex :: "jvm_prog ⇒ cname ⇒ mname ⇒ ex_table ⇒ nat set ⇒ nat ⇒ bool"
("(2_,/_,/_ ⊳/ _ /'/ _,/_)" [51,0,0,0,0,51] 50) where
"P,C,M ⊳ xt / I,d ⟷
(∃xt⇩0 xt⇩1. ex_table_of P C M = xt⇩0 @ xt @ xt⇩1 ∧ pcs xt⇩0 ∩ I = {} ∧ pcs xt ⊆ I ∧
(∀pc ∈ I. ∀C pc' d'. match_ex_table P C pc xt⇩1 = ⌊(pc',d')⌋ ⟶ d' ≤ d))"

definition dummyx :: "jvm_prog ⇒ cname ⇒ mname ⇒ ex_table ⇒ nat set ⇒ nat ⇒ bool"  ("(2_,_,_ ▹/ _ '/_,_)" [51,0,0,0,0,51] 50) where
"P,C,M ▹ xt/I,d ⟷ P,C,M ⊳ xt/I,d"

abbreviation
"beforex⇩0 P C M d I xt xt⇩0 xt⇩1
≡ ex_table_of P C M = xt⇩0 @ xt @ xt⇩1 ∧ pcs xt⇩0 ∩ I = {}
∧ pcs xt ⊆ I ∧ (∀pc ∈ I. ∀C pc' d'. match_ex_table P C pc xt⇩1 = ⌊(pc',d')⌋ ⟶ d' ≤ d)"

lemma beforex_beforex⇩0_eq:
"P,C,M ⊳ xt / I,d ≡ ∃xt⇩0 xt⇩1. beforex⇩0 P C M d I xt xt⇩0 xt⇩1"
using beforex_def by auto

lemma beforexD1: "P,C,M ⊳ xt / I,d ⟹ pcs xt ⊆ I"

lemma beforex_mono: "⟦ P,C,M ⊳ xt/I,d'; d' ≤ d ⟧ ⟹ P,C,M ⊳ xt/I,d"
(*<*)by(fastforce simp:beforex_def)(*>*)

lemma [simp]: "P,C,M ⊳ xt/I,d ⟹ P,C,M ⊳ xt/I,Suc d"
(*<*)by(fastforce intro:beforex_mono)(*>*)

lemma beforex_append[simp]:
"pcs xt⇩1 ∩ pcs xt⇩2 = {} ⟹
P,C,M ⊳ xt⇩1 @ xt⇩2/I,d =
(P,C,M ⊳ xt⇩1/I-pcs xt⇩2,d  ∧  P,C,M ⊳ xt⇩2/I-pcs xt⇩1,d ∧ P,C,M ▹ xt⇩1@xt⇩2/I,d)"
(*<*)(is "?Q ⟹ ?P = (?P1 ∧ ?P2 ∧ ?P3)" is "?Q ⟹ ?P = ?P123")
proof -
assume pcs: ?Q
show ?thesis proof(rule iffI)
assume "?P123" then show ?P by(simp add:dummyx_def)
next
assume hyp: ?P
let ?xt = "xt⇩1 @ xt⇩2"
let ?beforex = "beforex⇩0 P C M d"
obtain xt⇩0 xt⇩1' where beforex: "?beforex I ?xt xt⇩0 xt⇩1'"
using hyp by(clarsimp simp: beforex_def)
have "∃xt⇩0 xt⇩1'. ?beforex (I - pcs xt⇩2) xt⇩1 xt⇩0 xt⇩1'" ― ‹?P1›
using pcs beforex by(rule_tac x=xt⇩0 in exI) auto
moreover have "∃xt⇩0 xt⇩1'. ?beforex (I - pcs xt⇩1) xt⇩2 xt⇩0 xt⇩1'"  ― ‹?P2›
using pcs beforex by(rule_tac x="xt⇩0@xt⇩1" in exI) auto
moreover have ?P3 using hyp by(simp add: dummyx_def)
ultimately show ?P123 by (simp add: beforex_def)
qed
qed
(*>*)

lemma beforex_appendD1:
assumes bx: "P,C,M ⊳ xt⇩1 @ xt⇩2 @ [(f,t,D,h,d)] / I,d"
and pcs: "pcs xt⇩1 ⊆ J" and JI: "J ⊆ I" and Jpcs: "J ∩ pcs xt⇩2 = {}"
shows "P,C,M ⊳ xt⇩1 / J,d"
(*<*)
proof -
let ?beforex = "beforex⇩0 P C M d"
obtain xt⇩0 xt⇩1' where bx': "?beforex I (xt⇩1 @ xt⇩2 @ [(f,t,D,h,d)]) xt⇩0 xt⇩1'"
using bx by(clarsimp simp:beforex_def)
let ?xt0 = xt⇩0 and ?xt1 = "xt⇩2 @ (f, t, D, h, d) # xt⇩1'"
have "pcs xt⇩0 ∩ J = {}" using bx' JI by blast
moreover {
fix pc C pc' d' assume pcJ: "pc∈J"
then have "pc ∉ pcs xt⇩2" using bx' Jpcs by blast
then have "match_ex_table P C pc (xt⇩2 @ (f, t, D, h, d) # xt⇩1')
= ⌊(pc', d')⌋ ⟶ d' ≤ d"
using bx' JI pcJ by (auto split:if_split_asm)
}
ultimately have "?beforex J xt⇩1 ?xt0 ?xt1" using bx' pcs by simp
then show ?thesis using beforex_def by blast
qed
(*>*)

lemma beforex_appendD2:
assumes bx: "P,C,M ⊳ xt⇩1 @ xt⇩2 @ [(f,t,D,h,d)] / I,d"
and pcs: "pcs xt⇩2 ⊆ J" and JI: "J ⊆ I" and Jpcs: "J ∩ pcs xt⇩1 = {}"
shows "P,C,M ⊳ xt⇩2 / J,d"
(*<*)
proof -
let ?beforex = "beforex⇩0 P C M d"
obtain xt⇩0 xt⇩1' where bx': "?beforex I (xt⇩1 @ xt⇩2 @ [(f,t,D,h,d)]) xt⇩0 xt⇩1'"
using bx by(clarsimp simp:beforex_def)
then have "∃xt⇩1''. beforex⇩0 P C M d J xt⇩2 (xt⇩0 @ xt⇩1) xt⇩1''"
using assms by fastforce
then show ?thesis using beforex_def by blast
qed
(*>*)

lemma beforexM:
"P ⊢ C sees M,b: Ts→T = body in D ⟹ compP⇩2 P,D,M ⊳ compxE⇩2 body 0 0/{..<size(compE⇩2 body)},0"
(*<*)
proof -
assume cM: "P ⊢ C sees M,b: Ts→T = body in D"
let ?xt0 = "[]"
have "∃xt1. beforex⇩0 (compP⇩2 P) D M 0 ({..<size(compE⇩2 body)}) (compxE⇩2 body 0 0) ?xt0 xt1"
using sees_method_compP[where f = compMb⇩2, OF sees_method_idemp[OF cM]]
pcs_subset by(fastforce simp add: compP⇩2_def compMb⇩2_def)
then show ?thesis using beforex_def by blast
qed
(*>*)

lemma match_ex_table_SomeD2:
assumes met: "match_ex_table P D pc (ex_table_of P C M) = ⌊(pc',d')⌋"
and bx: "P,C,M ⊳ xt/I,d"
and nmet: "∀x ∈ set xt. ¬ matches_ex_entry P D pc x" and pcI: "pc ∈ I"
shows "d' ≤ d"
(*<*)
proof -
obtain xt⇩0 xt⇩1 where bx': "beforex⇩0 P C M d I xt xt⇩0 xt⇩1"
using bx by(clarsimp simp:beforex_def)
then have "pc ∉ pcs xt⇩0" using pcI by blast
then show ?thesis using bx' met nmet pcI by simp
qed
(*>*)

lemma match_ex_table_SomeD1:
"⟦ match_ex_table P D pc (ex_table_of P C M) = ⌊(pc',d')⌋;
P,C,M ⊳ xt / I,d; pc ∈ I; pc ∉ pcs xt ⟧ ⟹ d' ≤ d"
(*<*)by(auto elim: match_ex_table_SomeD2)(*>*)

subsection‹ The correctness proof ›

(*<*)
declare fun_upd_apply[simp del]
(*>*)

definition
handle :: "jvm_prog ⇒ cname ⇒ mname ⇒ addr ⇒ heap ⇒ val list ⇒ val list ⇒ nat ⇒ init_call_status ⇒ frame list ⇒ sheap
⇒ jvm_state" where
"handle P C M a h vs ls pc ics frs sh = find_handler P a h ((vs,ls,C,M,pc,ics) # frs) sh"

lemma aux_isin[simp]: "⟦ B ⊆ A; a ∈ B ⟧ ⟹ a ∈ A"
(*<*)by blast(*>*)

lemma handle_frs_tl_neq:
"ics_of f ≠ No_ics
⟹ (xp, h, f#frs, sh) ≠ handle P C M xa h' vs l pc ics frs sh'"
by(simp add: handle_def find_handler_frs_tl_neq del: find_handler.simps)

subsubsection "Correctness proof inductive hypothesis"

― ‹ frame definitions for use by correctness proof inductive hypothesis ›
fun calling_to_called :: "frame ⇒ frame" where
"calling_to_called (stk,loc,D,M,pc,ics) = (stk,loc,D,M,pc,case ics of Calling C Cs ⇒ Called (C#Cs))"

fun calling_to_scalled :: "frame ⇒ frame" where
"calling_to_scalled (stk,loc,D,M,pc,ics) = (stk,loc,D,M,pc,case ics of Calling C Cs ⇒ Called Cs)"

fun calling_to_calling :: "frame ⇒ cname ⇒ frame" where
"calling_to_calling (stk,loc,D,M,pc,ics) C' = (stk,loc,D,M,pc,case ics of Calling C Cs ⇒ Calling C' (C#Cs))"

fun calling_to_throwing :: "frame ⇒ addr ⇒ frame" where
"calling_to_throwing (stk,loc,D,M,pc,ics) a = (stk,loc,D,M,pc,case ics of Calling C Cs ⇒ Throwing (C#Cs) a)"

fun calling_to_sthrowing :: "frame ⇒ addr ⇒ frame" where
"calling_to_sthrowing (stk,loc,D,M,pc,ics) a = (stk,loc,D,M,pc,case ics of Calling C Cs ⇒ Throwing Cs a)"

― ‹ pieces of the correctness proof's inductive hypothesis, which depend on the
expression being compiled) ›

fun Jcc_cond :: "J⇩1_prog ⇒ ty list ⇒ cname ⇒ mname ⇒ val list ⇒ pc ⇒ init_call_status
⇒ nat set ⇒ heap ⇒ sheap ⇒ expr⇩1 ⇒ bool" where
"Jcc_cond P E C M vs pc ics I h sh (INIT C⇩0 (Cs,b) ← e')
= ((∃T. P,E,h,sh ⊢⇩1 INIT C⇩0 (Cs,b) ← e' : T) ∧ unit = e' ∧ ics = No_ics)" |
"Jcc_cond P E C M vs pc ics I h sh (RI(C',e⇩0);Cs ← e')
= (((e⇩0 = C'∙⇩sclinit([]) ∧ (∃T. P,E,h,sh ⊢⇩1 RI(C',e⇩0);Cs ← e':T))
∨ ((∃a. e⇩0 = Throw a) ∧ (∀C ∈ set(C'#Cs). is_class P C)))
∧ unit = e' ∧ ics = No_ics)" |
"Jcc_cond P E C M vs pc ics I h sh (C'∙⇩sM'(es))
= (let e = (C'∙⇩sM'(es))
in if M' = clinit ∧ es = [] then (∃T. P,E,h,sh ⊢⇩1 e:T) ∧ (∃Cs. ics = Called Cs)
else (compP⇩2 P,C,M,pc ⊳ compE⇩2 e ∧ compP⇩2 P,C,M ⊳ compxE⇩2 e pc (size vs)/I,size vs
∧ {pc..<pc+size(compE⇩2 e)} ⊆ I ∧ ¬sub_RI e ∧ ics = No_ics)
)" |
"Jcc_cond P E C M vs pc ics I h sh e
= (compP⇩2 P,C,M,pc ⊳ compE⇩2 e ∧ compP⇩2 P,C,M ⊳ compxE⇩2 e pc (size vs)/I,size vs
∧ {pc..<pc+size(compE⇩2 e)} ⊆ I ∧ ¬sub_RI e ∧ ics = No_ics)"

fun Jcc_frames :: "jvm_prog ⇒ cname ⇒ mname ⇒ val list ⇒ val list ⇒ pc ⇒ init_call_status
⇒ frame list ⇒ expr⇩1 ⇒ frame list" where
"Jcc_frames P C M vs ls pc ics frs (INIT C⇩0 (C'#Cs,b) ← e')
= (case b of False ⇒ (vs,ls,C,M,pc,Calling C' Cs) # frs
| True ⇒ (vs,ls,C,M,pc,Called (C'#Cs)) # frs
)" |
"Jcc_frames P C M vs ls pc ics frs (INIT C⇩0 (Nil,b) ← e')
= (vs,ls,C,M,pc,Called [])#frs" |
"Jcc_frames P C M vs ls pc ics frs (RI(C',e⇩0);Cs ← e')
= (case e⇩0 of Throw a ⇒ (vs,ls,C,M,pc,Throwing (C'#Cs) a) # frs
| _ ⇒ (vs,ls,C,M,pc,Called (C'#Cs)) # frs )" |
"Jcc_frames P C M vs ls pc ics frs (C'∙⇩sM'(es))
= (if M' = clinit ∧ es = []
then create_init_frame P C'#(vs,ls,C,M,pc,ics)#frs
else (vs,ls,C,M,pc,ics)#frs
)" |
"Jcc_frames P C M vs ls pc ics frs e
= (vs,ls,C,M,pc,ics)#frs"

fun Jcc_rhs :: "J⇩1_prog ⇒ ty list ⇒ cname ⇒ mname ⇒ val list ⇒ val list ⇒ pc ⇒ init_call_status
⇒ frame list ⇒ heap ⇒ val list ⇒ sheap ⇒ val ⇒ expr⇩1 ⇒ jvm_state" where
"Jcc_rhs P E C M vs ls pc ics frs h' ls' sh' v (INIT C⇩0 (Cs,b) ← e')
= (None,h',(vs,ls,C,M,pc,Called [])#frs,sh')" |
"Jcc_rhs P E C M vs ls pc ics frs h' ls' sh' v (RI(C',e⇩0);Cs ← e')
= (None,h',(vs,ls,C,M,pc,Called [])#frs,sh')" |
"Jcc_rhs P E C M vs ls pc ics frs h' ls' sh' v (C'∙⇩sM'(es))
= (let e = (C'∙⇩sM'(es))
in if M' = clinit ∧ es = []
then (None,h',(vs,ls,C,M,pc,ics)#frs,sh'(C'↦(fst(the(sh' C')),Done)))
else (None,h',(v#vs,ls',C,M,pc+size(compE⇩2 e),ics)#frs,sh')
)" |
"Jcc_rhs P E C M vs ls pc ics frs h' ls' sh' v e
= (None,h',(v#vs,ls',C,M,pc+size(compE⇩2 e),ics)#frs,sh')"

fun Jcc_err :: "jvm_prog ⇒ cname ⇒ mname ⇒ heap ⇒ val list ⇒ val list ⇒ pc ⇒ init_call_status
⇒ frame list ⇒ sheap ⇒ nat set ⇒ heap ⇒ val list ⇒ sheap ⇒ addr ⇒ expr⇩1
⇒ bool" where
"Jcc_err P C M h vs ls pc ics frs sh I h' ls' sh' xa (INIT C⇩0 (Cs,b) ← e')
= (∃vs'. P ⊢ (None,h,Jcc_frames P C M vs ls pc ics frs (INIT C⇩0 (Cs,b) ← e'),sh)
-jvm→ handle P C M xa h' (vs'@vs) ls pc ics frs sh')" |
"Jcc_err P C M h vs ls pc ics frs sh I h' ls' sh' xa (RI(C',e⇩0);Cs ← e')
= (∃vs'. P ⊢ (None,h,Jcc_frames P C M vs ls pc ics frs (RI(C',e⇩0);Cs ← e'),sh)
-jvm→ handle P C M xa h' (vs'@vs) ls pc ics frs sh')" |
"Jcc_err P C M h vs ls pc ics frs sh I h' ls' sh' xa (C'∙⇩sM'(es))
= (let e = (C'∙⇩sM'(es))
in if M' = clinit ∧ es = []
then case ics of
Called Cs ⇒ P ⊢ (None,h,Jcc_frames P C M vs ls pc ics frs e,sh)
-jvm→ (None,h',(vs,ls,C,M,pc,Throwing Cs xa)#frs,(sh'(C' ↦ (fst(the(sh' C')),Error))))
else (∃pc⇩1. pc ≤ pc⇩1 ∧ pc⇩1 < pc + size(compE⇩2 e) ∧
¬ caught P pc⇩1 h' xa (compxE⇩2 e pc (size vs)) ∧
(∃vs'. P ⊢ (None,h,Jcc_frames P C M vs ls pc ics frs e,sh)
-jvm→ handle P C M xa h' (vs'@vs) ls' pc⇩1 ics frs sh'))
)" |
"Jcc_err P C M h vs ls pc ics frs sh I h' ls' sh' xa e
= (∃pc⇩1. pc ≤ pc⇩1 ∧ pc⇩1 < pc + size(compE⇩2 e) ∧
¬ caught P pc⇩1 h' xa (compxE⇩2 e pc (size vs)) ∧
(∃vs'. P ⊢ (None,h,Jcc_frames P C M vs ls pc ics frs e,sh)
-jvm→ handle P C M xa h' (vs'@vs) ls' pc⇩1 ics frs sh'))"

fun Jcc_pieces :: "J⇩1_prog ⇒ ty list ⇒ cname ⇒ mname ⇒ heap ⇒ val list ⇒ val list ⇒ pc ⇒ init_call_status
⇒ frame list ⇒ sheap ⇒ nat set ⇒ heap ⇒ val list ⇒ sheap ⇒ val ⇒ addr ⇒ expr⇩1
⇒ bool × frame list × jvm_state × bool" where
"Jcc_pieces P E C M h vs ls pc ics frs sh I h' ls' sh' v xa e
= (Jcc_cond P E C M vs pc ics I h sh e, Jcc_frames (compP⇩2 P) C M vs ls pc ics frs e,
Jcc_rhs P E C M vs ls pc ics frs h' ls' sh' v e,
Jcc_err (compP⇩2 P) C M h vs ls pc ics frs sh I h' ls' sh' xa e)"

― ‹ @{text Jcc_pieces} lemmas ›

lemma nsub_RI_Jcc_pieces:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and nsub: "¬sub_RI e"
shows "Jcc_pieces P⇩1 E C M h vs ls pc ics frs sh I h' ls' sh' v xa e
= (let cond = P,C,M,pc ⊳ compE⇩2 e ∧ P,C,M ⊳ compxE⇩2 e pc (size vs)/I,size vs
∧ {pc..<pc+size(compE⇩2 e)} ⊆ I ∧ ics = No_ics;
frs' = (vs,ls,C,M,pc,ics)#frs;
rhs = (None,h',(v#vs,ls',C,M,pc+size(compE⇩2 e),ics)#frs,sh');
err = (∃pc⇩1. pc ≤ pc⇩1 ∧ pc⇩1 < pc + size(compE⇩2 e) ∧
¬ caught P pc⇩1 h' xa (compxE⇩2 e pc (size vs)) ∧
(∃vs'. P ⊢ (None,h,frs',sh) -jvm→ handle P C M xa h' (vs'@vs) ls' pc⇩1 ics frs sh'))
in (cond, frs',rhs, err)
)"
proof -
have NC: "∀C'. e ≠ C'∙⇩sclinit([])" using assms(2) proof(cases e) qed(simp_all)
then show ?thesis using assms
proof(cases e)
case (SCall C M es)
then have "M ≠ clinit" using nsub by simp
then show ?thesis using SCall nsub proof(cases es) qed(simp_all)
qed(simp_all)
qed

lemma Jcc_pieces_Cast:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and "Jcc_pieces P⇩1 E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h⇩1 ls⇩1 sh⇩1 v xa (Cast C' e)
= (True, frs⇩0, (xp',h',(v#vs',ls',C⇩0,M',pc',ics')#frs',sh'), err)"
shows "Jcc_pieces P⇩1 E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h⇩1 ls⇩1 sh⇩1 v' xa e
= (True, frs⇩0, (xp',h',(v'#vs',ls',C⇩0,M',pc' - 1,ics')#frs',sh'),
(∃pc⇩1. pc ≤ pc⇩1 ∧ pc⇩1 < pc + size(compE⇩2 e) ∧
¬ caught P pc⇩1 h⇩1 xa (compxE⇩2 e pc (size vs)) ∧
(∃vs'. P ⊢ (None,h⇩0,frs⇩0,sh⇩0) -jvm→ handle P C M xa h⇩1 (vs'@vs) ls⇩1 pc⇩1 ics frs sh⇩1)))"
proof -
have pc: "{pc..<pc + length (compE⇩2 e)} ⊆ I" using assms by clarsimp
show ?thesis using assms nsub_RI_Jcc_pieces[where e=e] pc by clarsimp
qed

lemma Jcc_pieces_BinOp1:
assumes
"Jcc_pieces P E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h⇩2 ls⇩2 sh⇩2 v xa (e «bop» e')
= (True, frs⇩0, (xp',h',(v#vs',ls',C⇩0,M',pc',ics')#frs',sh'), err)"
shows "∃err. Jcc_pieces P E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0
(I - pcs (compxE⇩2 e' (pc + length (compE⇩2 e)) (Suc (length vs')))) h⇩1 ls⇩1 sh⇩1 v' xa e
= (True, frs⇩0, (xp',h⇩1,(v'#vs',ls⇩1,C⇩0,M',pc' - size (compE⇩2 e') - 1,ics')#frs',sh⇩1), err)"
proof -
have bef: "compP compMb⇩2 P,C⇩0,M' ⊳ compxE⇩2 e pc (length vs)
/ I - pcs (compxE⇩2 e' (pc + length (compE⇩2 e)) (Suc (length vs'))),length vs"
using assms by clarsimp
have vs: "vs = vs'" using assms by simp
show ?thesis using assms nsub_RI_Jcc_pieces[where e=e] bef vs by clarsimp
qed

lemma Jcc_pieces_BinOp2:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and "Jcc_pieces P⇩1 E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h⇩2 ls⇩2 sh⇩2 v xa (e «bop» e')
= (True, frs⇩0, (xp',h',(v#vs',ls',C⇩0,M',pc',ics')#frs',sh'), err)"
shows "∃err. Jcc_pieces P⇩1 E C M h⇩1 (v⇩1#vs) ls⇩1 (pc + size (compE⇩2 e)) ics frs sh⇩1
(I - pcs (compxE⇩2 e pc (length vs'))) h⇩2 ls⇩2 sh⇩2 v' xa e'
= (True, (v⇩1#vs,ls⇩1,C,M,pc + size (compE⇩2 e),ics)#frs,
(xp',h',(v'#v⇩1#vs',ls',C⇩0,M',pc' - 1,ics')#frs',sh'),
(∃pc⇩1. pc + size (compE⇩2 e) ≤ pc⇩1 ∧ pc⇩1 < pc + size (compE⇩2 e) + length (compE⇩2 e') ∧
¬ caught P pc⇩1 h⇩2 xa (compxE⇩2 e' (pc + size (compE⇩2 e)) (Suc (length vs))) ∧
(∃vs'. P ⊢ (None,h⇩1,(v⇩1#vs,ls⇩1,C,M,pc + size (compE⇩2 e),ics)#frs,sh⇩1)
-jvm→ handle P C M xa h⇩2 (vs'@v⇩1#vs) ls⇩2 pc⇩1 ics frs sh⇩2)))"
proof -
have bef: "compP compMb⇩2 P⇩1,C⇩0,M' ⊳ compxE⇩2 e pc (length vs)
/ I - pcs (compxE⇩2 e' (pc + length (compE⇩2 e)) (Suc (length vs'))),length vs"
using assms by clarsimp
have vs: "vs = vs'" using assms by simp
show ?thesis using assms nsub_RI_Jcc_pieces[where e=e'] bef vs by clarsimp
qed

lemma Jcc_pieces_FAcc:
assumes
"Jcc_pieces P E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h⇩1 ls⇩1 sh⇩1 v xa (e∙F{D})
= (True, frs⇩0, (xp',h',(v#vs',ls',C⇩0,M',pc',ics')#frs',sh'), err)"
shows "∃err. Jcc_pieces P E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h⇩1 ls⇩1 sh⇩1 v' xa e
= (True, frs⇩0, (xp',h',(v'#vs',ls',C⇩0,M',pc' - 1,ics')#frs',sh'), err)"
proof -
have pc: "{pc..<pc + length (compE⇩2 e)} ⊆ I" using assms by clarsimp
then show ?thesis using assms nsub_RI_Jcc_pieces[where e=e] by clarsimp
qed

lemma Jcc_pieces_LAss:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and "Jcc_pieces P⇩1 E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h⇩1 ls⇩1 sh⇩1 v xa (i:=e)
= (True, frs⇩0, (xp',h',(v#vs',ls',C⇩0,M',pc',ics')#frs',sh'), err)"
shows "Jcc_pieces P⇩1 E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h⇩1 ls⇩1 sh⇩1 v' xa e
= (True, frs⇩0, (xp',h',(v'#vs',ls',C⇩0,M',pc' - 2,ics')#frs',sh'),
(∃pc⇩1. pc ≤ pc⇩1 ∧ pc⇩1 < pc + size(compE⇩2 e) ∧
¬ caught P pc⇩1 h⇩1 xa (compxE⇩2 e pc (size vs)) ∧
(∃vs'. P ⊢ (None,h⇩0,frs⇩0,sh⇩0) -jvm→ handle P C M xa h⇩1 (vs'@vs) ls⇩1 pc⇩1 ics frs sh⇩1)))"
proof -
have pc: "{pc..<pc + length (compE⇩2 e)} ⊆ I" using assms by clarsimp
show ?thesis using assms nsub_RI_Jcc_pieces[where e=e] pc by clarsimp
qed

lemma Jcc_pieces_FAss1:
assumes
"Jcc_pieces P E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h⇩2 ls⇩2 sh⇩2 v xa (e∙F{D}:=e')
= (True, frs⇩0, (xp',h',(v#vs',ls',C⇩0,M',pc',ics')#frs',sh'), err)"
shows "∃err. Jcc_pieces P E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0
(I - pcs (compxE⇩2 e' (pc + length (compE⇩2 e)) (Suc (length vs')))) h⇩1 ls⇩1 sh⇩1 v' xa e
= (True, frs⇩0, (xp',h⇩1,(v'#vs',ls⇩1,C⇩0,M',pc' - size (compE⇩2 e') - 2,ics')#frs',sh⇩1), err)"
proof -
show ?thesis using assms nsub_RI_Jcc_pieces[where e=e] by clarsimp
qed

lemma Jcc_pieces_FAss2:
assumes
"Jcc_pieces P E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h⇩2 ls⇩2 sh⇩2 v xa (e∙F{D}:=e')
= (True, frs⇩0, (xp',h',(v#vs',ls',C⇩0,M',pc',ics')#frs',sh'), err)"
shows "Jcc_pieces P E C M h⇩1 (v⇩1#vs) ls⇩1 (pc + size (compE⇩2 e)) ics frs sh⇩1
(I - pcs (compxE⇩2 e pc (length vs'))) h⇩2 ls⇩2 sh⇩2 v' xa e'
= (True, (v⇩1#vs,ls⇩1,C,M,pc + size (compE⇩2 e),ics)#frs,
(xp',h',(v'#v⇩1#vs',ls',C⇩0,M',pc' - 2,ics')#frs',sh'),
(∃pc⇩1. (pc + size (compE⇩2 e)) ≤ pc⇩1 ∧ pc⇩1 < pc + size (compE⇩2 e) + size(compE⇩2 e') ∧
¬ caught (compP⇩2 P) pc⇩1 h⇩2 xa (compxE⇩2 e' (pc + size (compE⇩2 e)) (size (v⇩1#vs))) ∧
(∃vs'. (compP⇩2 P) ⊢ (None,h⇩1,(v⇩1#vs,ls⇩1,C,M,pc + size (compE⇩2 e),ics)#frs,sh⇩1)
-jvm→ handle (compP⇩2 P) C M xa h⇩2 (vs'@v⇩1#vs) ls⇩2 pc⇩1 ics frs sh⇩2)))"
proof -
show ?thesis using assms nsub_RI_Jcc_pieces[where e=e'] by clarsimp
qed

lemma Jcc_pieces_SFAss:
assumes
"Jcc_pieces P E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h' ls' sh' v xa (C'∙⇩sF{D}:=e)
= (True, frs⇩0, (xp',h',(v#vs',ls',C⇩0,M',pc',ics')#frs',sh'), err)"
shows "∃err. Jcc_pieces P E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h⇩1 ls⇩1 sh⇩1 v' xa e
= (True, frs⇩0, (xp',h⇩1,(v'#vs',ls⇩1,C⇩0,M',pc' - 2,ics')#frs',sh⇩1), err)"
proof -
have pc: "{pc..<pc + length (compE⇩2 e)} ⊆ I" using assms by clarsimp
show ?thesis using assms nsub_RI_Jcc_pieces[where e=e] pc by clarsimp
qed

lemma Jcc_pieces_Call1:
assumes
"Jcc_pieces P E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h⇩3 ls⇩3 sh⇩3 v xa (e∙M⇩0(es))
= (True, frs⇩0, (xp',h',(v#vs',ls',C',M',pc',ics')#frs',sh'), err)"
shows "∃err. Jcc_pieces P E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0
(I - pcs (compxEs⇩2 es (pc + length (compE⇩2 e)) (Suc (length vs')))) h⇩1 ls⇩1 sh⇩1 v' xa e
= (True, frs⇩0,
(xp',h⇩1,(v'#vs',ls⇩1,C',M',pc' - size (compEs⇩2 es) - 1,ics')#frs',sh⇩1), err)"
proof -
show ?thesis using assms nsub_RI_Jcc_pieces[where e=e] by clarsimp
qed

lemma Jcc_pieces_clinit:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and cond: "Jcc_cond P⇩1 E C M vs pc ics I h sh (C1∙⇩sclinit([]))"
shows "Jcc_pieces P⇩1 E C M h vs ls pc ics frs sh I h' ls' sh' v xa (C1∙⇩sclinit([]))
= (True, create_init_frame P C1 # (vs,ls,C,M,pc,ics)#frs,
(None, h', (vs,ls,C,M,pc,ics)#frs, sh'(C1↦(fst(the(sh' C1)),Done))),
P ⊢ (None,h,create_init_frame P C1 # (vs,ls,C,M,pc,ics)#frs,sh) -jvm→
(case ics of Called Cs ⇒ (None,h',(vs,ls,C,M,pc,Throwing Cs xa)#frs,(sh'(C1 ↦ (fst(the(sh' C1)),Error))))))"
using assms by(auto split: init_call_status.splits list.splits bool.splits)

lemma Jcc_pieces_SCall_clinit_body:
assumes [simp]: "P ≡ compP⇩2 P⇩1" and wf: "wf_J⇩1_prog P⇩1"
and "Jcc_pieces P⇩1 E C M h⇩0 vs ls⇩0 pc ics frs sh⇩0 I h⇩3 ls⇩2 sh⇩3 v xa (C1∙⇩sclinit([]))
= (True, frs', rhs', err')"
and method: "P⇩1 ⊢ C1 sees clinit,Static: []→Void = body in D"
shows "Jcc_pieces P⇩1 [] D clinit h⇩2 [] (replicate (max_vars body) undefined) 0
No_ics (tl frs') sh⇩2 {..<length (compE⇩2 body)} h⇩3 ls⇩3 sh⇩3 v xa body
= (True, frs',
(None,h⇩3,([v],ls⇩3,D,clinit,size(compE⇩2 body), No_ics)#tl frs',sh⇩3),
∃pc⇩1. 0 ≤ pc⇩1 ∧ pc⇩1 < size(compE⇩2 body) ∧
¬ caught P pc⇩1 h⇩3 xa (compxE⇩2 body 0 0) ∧
(∃vs'. P ⊢ (None,h⇩2,frs',sh⇩2) -jvm→ handle P D clinit xa h⇩3 vs' ls⇩3 pc⇩1
No_ics (tl frs') sh⇩3))"
proof -
have M_in_D: "P⇩1 ⊢ D sees clinit,Static: []→Void = body in D"
using method by(rule sees_method_idemp)
hence M_code: "compP⇩2 P⇩1,D,clinit,0 ⊳ compE⇩2 body @ [Return]"
and M_xtab: "compP⇩2 P⇩1,D,clinit ⊳ compxE⇩2 body 0 0/{..<size(compE⇩2 body)},0"
by(rule beforeM, rule beforexM)
have nsub: "¬sub_RI body" by(rule sees_wf⇩1_nsub_RI[OF wf method])
then show ?thesis using assms nsub_RI_Jcc_pieces M_code M_xtab by clarsimp
qed

lemma Jcc_pieces_Cons:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and "P,C,M,pc ⊳ compEs⇩2 (e#es)" and "P,C,M ⊳ compxEs⇩2 (e#es) pc (size vs)/I,size vs"
and "{pc..<pc+size(compEs⇩2 (e#es))} ⊆ I"
and "ics = No_ics"
and "¬sub_RIs (e#es)"
shows "Jcc_pieces P⇩1 E C M h vs ls pc ics frs sh
(I - pcs (compxEs⇩2 es (pc + length (compE⇩2 e)) (Suc (length vs)))) h' ls' sh' v xa e
= (True, (vs, ls, C, M, pc, ics) # frs,
(None, h', (v#vs, ls', C, M, pc + length (compE⇩2 e), ics) # frs, sh'),
∃pc⇩1≥pc. pc⇩1 < pc + length (compE⇩2 e) ∧ ¬ caught P pc⇩1 h' xa (compxE⇩2 e pc (length vs))
∧ (∃vs'. P ⊢ (None, h, (vs, ls, C, M, pc, ics) # frs, sh)
-jvm→ handle P C M xa h' (vs'@vs) ls' pc⇩1 ics frs sh'))"
proof -
show ?thesis using assms nsub_RI_Jcc_pieces[where e=e] by auto
qed

lemma Jcc_pieces_InitNone:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and "Jcc_pieces P⇩1 E C M h vs l pc ics frs sh I h' l' sh' v xa (INIT C' (C⇩0 # Cs,False) ← e)
= (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
shows
"Jcc_pieces P⇩1 E C M h vs l pc ics frs (sh(C⇩0 ↦ (sblank P C⇩0, Prepared)))
I h' l' sh' v xa (INIT C' (C⇩0 # Cs,False) ← e)
= (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'),
∃vs'. P ⊢ (None,h,frs',(sh(C⇩0 ↦ (sblank P⇩1 C⇩0, Prepared))))
-jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh')"
proof -
have  "Jcc_cond P⇩1 E C M vs pc ics I h sh (INIT C' (C⇩0 # Cs,False) ← e)" using assms by simp
then obtain T where "P⇩1,E,h,sh ⊢⇩1 INIT C' (C⇩0 # Cs,False) ← unit : T" by fastforce
then have "P⇩1,E,h,sh(C⇩0 ↦ (sblank P⇩1 C⇩0, Prepared)) ⊢⇩1 INIT C' (C⇩0 # Cs,False) ← unit : T"
by(auto simp: fun_upd_apply)
then have "Ex (WTrt2⇩1 P⇩1 E h (sh(C⇩0 ↦ (sblank P⇩1 C⇩0, Prepared))) (INIT C' (C⇩0 # Cs,False) ← unit))"
by(simp only: exI)
then show ?thesis using assms by clarsimp
qed

lemma Jcc_pieces_InitDP:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and "Jcc_pieces P⇩1 E C M h vs l pc ics frs sh I h' l' sh' v xa (INIT C' (C⇩0 # Cs,False) ← e)
= (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
shows
"Jcc_pieces P⇩1 E C M h vs l pc ics frs sh I h' l' sh' v xa (INIT C' (Cs,True) ← e)
= (True, (calling_to_scalled (hd frs'))#(tl frs'),
(None, h', (vs, l, C, M, pc, Called []) # frs, sh'),
∃vs'. P ⊢ (None,h,calling_to_scalled (hd frs')#(tl frs'),sh)
-jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh')"
proof -
have "Jcc_cond P⇩1 E C M vs pc ics I h sh (INIT C' (C⇩0 # Cs,False) ← e)" using assms by simp
then obtain T where "P⇩1,E,h,sh ⊢⇩1 INIT C' (C⇩0 # Cs,False) ← unit : T" by fastforce
then have "P⇩1,E,h,sh ⊢⇩1 INIT C' (Cs,True) ← unit : T"
by (auto; metis list.sel(2) list.set_sel(2))
then have wtrt: "Ex (WTrt2⇩1 P⇩1 E h sh (INIT C' (Cs,True) ← unit))" by(simp only: exI)
show ?thesis using assms wtrt
proof(cases Cs)
case (Cons C1 Cs1)
then show ?thesis using assms wtrt
by(case_tac "method P C1 clinit") clarsimp
qed(clarsimp)
qed

lemma Jcc_pieces_InitError:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and "Jcc_pieces P⇩1 E C M h vs l pc ics frs sh I h' l' sh' v xa (INIT C' (C⇩0 # Cs,False) ← e)
= (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
and err: "sh C⇩0 = Some(sfs,Error)"
shows
"Jcc_pieces P⇩1 E C M h vs l pc ics frs sh I h' l' sh' v xa (RI (C⇩0, THROW NoClassDefFoundError);Cs ← e)
= (True, (calling_to_throwing (hd frs') (addr_of_sys_xcpt NoClassDefFoundError))#(tl frs'),
(None, h', (vs, l, C, M, pc, Called []) # frs, sh'),
∃vs'. P ⊢ (None,h, (calling_to_throwing (hd frs') (addr_of_sys_xcpt NoClassDefFoundError))#(tl frs'),sh)
-jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh')"
proof -
show ?thesis using assms
proof(cases Cs)
case (Cons C1 Cs1)
then show ?thesis using assms
by(case_tac "method P C1 clinit", case_tac "method P C⇩0 clinit") clarsimp
qed(clarsimp)
qed

lemma Jcc_pieces_InitObj:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and "Jcc_pieces P⇩1 E C M h vs l pc ics frs sh I h' l' (sh(C⇩0 ↦ (sfs,Processing))) v xa (INIT C' (C⇩0 # Cs,False) ← e)
= (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
shows
"Jcc_pieces P⇩1 E C M h vs l pc ics frs (sh(C⇩0 ↦ (sfs,Processing))) I h' l' sh'' v xa (INIT C' (C⇩0 # Cs,True) ← e)
= (True, calling_to_called (hd frs')#(tl frs'),
(None, h', (vs, l, C, M, pc, Called []) # frs, sh''),
∃vs'. P ⊢ (None,h,calling_to_called (hd frs')#(tl frs'),sh')
-jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh'')"
proof -
have "Jcc_cond P⇩1 E C M vs pc ics I h sh (INIT C' (C⇩0 # Cs,False) ← e)" using assms by simp
then obtain T where "P⇩1,E,h,sh ⊢⇩1 INIT C' (C⇩0 # Cs,False) ← unit : T" by fastforce
then have "P⇩1,E,h,sh(C⇩0 ↦ (sfs,Processing)) ⊢⇩1 INIT C' (C⇩0 # Cs,True) ← unit : T"
using assms by clarsimp (auto simp: fun_upd_apply)
then have wtrt: "Ex (WTrt2⇩1 P⇩1 E h (sh(C⇩0 ↦ (sfs,Processing))) (INIT C' (C⇩0 # Cs,True) ← unit))"
by(simp only: exI)
show ?thesis using assms wtrt by clarsimp
qed

lemma Jcc_pieces_InitNonObj:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and "is_class P⇩1 D" and "D ∉ set (C⇩0#Cs)" and "∀C ∈ set (C⇩0#Cs). P⇩1 ⊢ C ≼⇧* D"
and pcs: "Jcc_pieces P⇩1 E C M h vs l pc ics frs sh I h' l' (sh(C⇩0 ↦ (sfs,Processing))) v xa (INIT C' (C⇩0 # Cs,False) ← e)
= (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
shows
"Jcc_pieces P⇩1 E C M h vs l pc ics frs (sh(C⇩0 ↦ (sfs,Processing))) I h' l' sh'' v xa (INIT C' (D # C⇩0 # Cs,False) ← e)
= (True, calling_to_calling (hd frs') D#(tl frs'),
(None, h', (vs, l, C, M, pc, Called []) # frs, sh''),
∃vs'. P ⊢ (None,h,calling_to_calling (hd frs') D#(tl frs'),sh')
-jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh'')"
proof -
have "Jcc_cond P⇩1 E C M vs pc ics I h sh (INIT C' (C⇩0 # Cs,False) ← e)" using assms by simp
then obtain T where "P⇩1,E,h,sh ⊢⇩1 INIT C' (C⇩0 # Cs,False) ← unit : T" by fastforce
then have "P⇩1,E,h,sh(C⇩0 ↦ (sfs,Processing)) ⊢⇩1 INIT C' (D # C⇩0 # Cs,False) ← unit : T"
using assms by clarsimp (auto simp: fun_upd_apply)
then have wtrt: "Ex (WTrt2⇩1 P⇩1 E h (sh(C⇩0 ↦ (sfs,Processing))) (INIT C' (D # C⇩0 # Cs,False) ← unit))"
by(simp only: exI)
show ?thesis using assms wtrt by clarsimp
qed

lemma Jcc_pieces_InitRInit:
assumes [simp]: "P ≡ compP⇩2 P⇩1" and wf: "wf_J⇩1_prog P⇩1"
and "Jcc_pieces P⇩1 E C M h vs l pc ics frs sh I h' l' sh' v xa (INIT C' (C⇩0 # Cs,True) ← e)
= (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
shows
"Jcc_pieces P⇩1 E C M h vs l pc ics frs sh I h' l' sh' v xa (RI (C⇩0,C⇩0∙⇩sclinit([])) ; Cs ← e)
= (True, frs',
(None, h', (vs, l, C, M, pc, Called []) # frs, sh'),
∃vs'. P ⊢ (None,h,frs',sh)
-jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh')"
proof -
have cond: "Jcc_cond P⇩1 E C M vs pc ics I h sh (INIT C' (C⇩0 # Cs,True) ← e)" using assms by simp
then have clinit: "∃T. P⇩1,E,h,sh ⊢⇩1 C⇩0∙⇩sclinit([]) : T" using wf
by clarsimp (auto simp: is_class_def intro: wf⇩1_types_clinit)
then obtain T where cT: "P⇩1,E,h,sh ⊢⇩1 C⇩0∙⇩sclinit([]) : T" by blast
obtain T where "P⇩1,E,h,sh ⊢⇩1 INIT C' (C⇩0 # Cs,True) ← unit : T" using cond by fastforce
then have "P⇩1,E,h,sh ⊢⇩1 RI (C⇩0,C⇩0∙⇩sclinit([])) ; Cs ← unit : T"
using assms by (auto intro: cT)
then have wtrt: "Ex (WTrt2⇩1 P⇩1 E h sh (RI (C⇩0,C⇩0∙⇩sclinit([])) ; Cs ← unit))"
by(simp only: exI)
then show ?thesis using assms by simp
qed

lemma Jcc_pieces_RInit_clinit:
assumes [simp]: "P ≡ compP⇩2 P⇩1" and wf: "wf_J⇩1_prog P⇩1"
and "Jcc_pieces P⇩1 E C M h vs l pc ics frs sh I h⇩1 l⇩1 sh⇩1 v xa (RI (C⇩0,C⇩0∙⇩sclinit([]));Cs ← e)
= (True, frs',
(None, h⇩1, (vs, l, C, M, pc, Called []) # frs, sh⇩1), err)"
shows
"Jcc_pieces P⇩1 E C M h vs l pc (Called Cs) (tl frs') sh I h' l' sh' v xa (C⇩0∙⇩sclinit([]))
= (True, create_init_frame P C⇩0#(vs,l,C,M,pc,Called Cs)#tl frs',
(None, h', (vs,l,C,M,pc,Called Cs)#tl frs', sh'(C⇩0↦(fst(the(sh' C⇩0)),Done))),
P ⊢ (None,h,create_init_frame P C⇩0#(vs,l,C,M,pc,Called Cs)#tl frs',sh)
-jvm→ (None,h',(vs, l, C, M, pc, Throwing Cs xa) # tl frs',sh'(C⇩0 ↦ (fst(the(sh' C⇩0)),Error))))"
proof -
have cond: "Jcc_cond P⇩1 E C M vs pc ics I h sh (RI (C⇩0,C⇩0∙⇩sclinit([]));Cs ← e)" using assms by simp
then have wtrt: "∃T. P⇩1,E,h,sh ⊢⇩1 C⇩0∙⇩sclinit([]) : T" using wf
by clarsimp (auto simp: is_class_def intro: wf⇩1_types_clinit)
then show ?thesis using assms by clarsimp
qed

lemma Jcc_pieces_RInit_Init:
assumes [simp]: "P ≡ compP⇩2 P⇩1" and wf: "wf_J⇩1_prog P⇩1"
and proc: "∀C' ∈ set Cs. ∃sfs. sh'' C' = ⌊(sfs,Processing)⌋"
and "Jcc_pieces P⇩1 E C M h vs l pc ics frs sh I h⇩1 l⇩1 sh⇩1 v xa (RI (C⇩0,C⇩0∙⇩sclinit([]));Cs ← e)
= (True, frs',
(None, h⇩1, (vs, l, C, M, pc, Called []) # frs, sh⇩1), err)"
shows
"Jcc_pieces P⇩1 E C M h' vs l pc ics frs sh'' I h⇩1 l⇩1 sh⇩1 v xa (INIT (last (C⇩0#Cs)) (Cs,True) ← e)
= (True, (vs, l, C, M, pc, Called Cs) # frs,
(None, h⇩1, (vs, l, C, M, pc, Called []) # frs, sh⇩1),
∃vs'. P ⊢ (None,h',(vs, l, C, M, pc, Called Cs) # frs,sh'')
-jvm→ handle P C M xa h⇩1 (vs'@vs) l pc ics frs sh⇩1)"
proof -
have "Jcc_cond P⇩1 E C M vs pc ics I h sh (RI (C⇩0,C⇩0∙⇩sclinit([]));Cs ← e)" using assms by simp
then have "Ex (WTrt2⇩1 P⇩1 E h sh (RI (C⇩0,C⇩0∙⇩sclinit([])) ; Cs ← unit))" by simp
then obtain T where riwt: "P⇩1,E,h,sh ⊢⇩1 RI (C⇩0,C⇩0∙⇩sclinit([]));Cs ← unit : T" by meson
then have "P⇩1,E,h',sh'' ⊢⇩1 INIT (last (C⇩0#Cs)) (Cs,True) ← unit : T" using proc
proof(cases Cs) qed(auto)
then have wtrt: "Ex (WTrt2⇩1 P⇩1 E h' sh'' (INIT (last (C⇩0#Cs)) (Cs,True) ← unit))" by(simp only: exI)
show ?thesis using assms wtrt
proof(cases Cs)
case (Cons C1 Cs1)
then show ?thesis using assms wtrt
by(case_tac "method P C1 clinit") clarsimp
qed(clarsimp)
qed

lemma Jcc_pieces_RInit_RInit:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and "Jcc_pieces P⇩1 E C M h vs l pc ics frs sh I h⇩1 l⇩1 sh⇩1 v xa (RI (C⇩0,e);D#Cs ← e')
= (True, frs', rhs, err)"
and hd: "hd frs' = (vs1,l1,C1,M1,pc1,ics1)"
shows
"Jcc_pieces P⇩1 E C M h' vs l pc ics frs sh'' I h⇩1 l⇩1 sh⇩1 v xa (RI (D,Throw xa) ; Cs ← e')
= (True, (vs1, l1, C1, M1, pc1, Throwing (D#Cs) xa) # tl frs',
(None, h⇩1, (vs, l, C, M, pc, Called []) # frs, sh⇩1),
∃vs'. P ⊢ (None,h',(vs1, l1, C1, M1, pc1, Throwing (D#Cs) xa) # tl frs',sh'')
-jvm→ handle P C M xa h⇩1 (vs'@vs) l pc ics frs sh⇩1)"
using assms by(case_tac "method P D clinit", cases "e = C⇩0∙⇩sclinit([])") clarsimp+

subsubsection "JVM stepping lemmas"

lemma jvm_Invoke:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and "P,C,M,pc ▹ Invoke M' (length Ts)"
and ha: "h⇩2 a = ⌊(Ca, fs)⌋" and method: "P⇩1 ⊢ Ca sees M', NonStatic :  Ts→T = body in D"
and len: "length pvs = length Ts" and "ls⇩2' = Addr a # pvs @ replicate (max_vars body) undefined"
shows "P ⊢ (None, h⇩2, (rev pvs @ Addr a # vs, ls⇩2, C, M, pc, No_ics) # frs, sh⇩2) -jvm→
(None, h⇩2, ([], ls⇩2', D, M', 0, No_ics) # (rev pvs @ Addr a # vs, ls⇩2, C, M, pc, No_ics) # frs, sh⇩2)"
proof -
have cname: "cname_of h⇩2 (the_Addr ((rev pvs @ Addr a # vs) ! length Ts)) = Ca"
using ha method len by(auto simp: nth_append)
have r: "(rev pvs @ Addr a # vs) ! (length Ts) = Addr a" using len by(auto simp: nth_append)
have exm: "∃Ts T m D b. P ⊢ Ca sees M',b:Ts → T = m in D"
using sees_method_compP[OF method] by fastforce
show ?thesis using assms cname r exm by simp
qed

lemma jvm_Invokestatic:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and "P,C,M,pc ▹ Invokestatic C' M' (length Ts)"
and sh: "sh⇩2 D = Some(sfs,Done)"
and method: "P⇩1 ⊢ C' sees M', Static :  Ts→T = body in D"
and len: "length pvs = length Ts" and "ls⇩2' = pvs @ replicate (max_vars body) undefined"
shows "P ⊢ (None, h⇩2, (rev pvs @ vs, ls⇩2, C, M, pc, No_ics) # frs, sh⇩2) -jvm→
(None, h⇩2, ([], ls⇩2', D, M', 0, No_ics) # (rev pvs @ vs, ls⇩2, C, M, pc, No_ics) # frs, sh⇩2)"
proof -
have exm: "∃Ts T m D b. P ⊢ C' sees M',b:Ts → T = m in D"
using sees_method_compP[OF method] by fastforce
show ?thesis using assms exm by simp
qed

lemma jvm_Invokestatic_Called:
assumes [simp]: "P ≡ compP⇩2 P⇩1"
and "P,C,M,pc ▹ Invokestatic C' M' (length Ts)"
and sh: "sh⇩2 D = Some(sfs,i)"
and method: "P⇩1 ⊢ C' sees M', Static :  Ts→T = body in D"
and len: "length pvs = length Ts" and "ls⇩2' = pvs @ replicate (max_vars body) undefined"
shows "P ⊢ (None, h⇩2, (rev pvs @ vs, ls⇩2, C, M, pc, Called []) # frs, sh⇩2) -jvm→
(None, h⇩2, ([], ls⇩2', D, M', 0, No_ics) # (rev pvs @ vs, ls⇩2, C, M, pc, No_ics) # frs, sh⇩2)"
proof -
have exm: "∃Ts T m D b. P ⊢ C' sees M',b:Ts → T = m in D"
using sees_method_compP[OF method] by fastforce
show ?thesis using assms exm by simp
qed

lemma jvm_Return_Init:
"P,D,clinit,0 ⊳ compE⇩2 body @ [Return]
⟹ P ⊢ (None, h, (vs, ls, D, clinit, size(compE⇩2 body), No_ics) # frs, sh)
-jvm→ (None, h, frs, sh(D↦(fst(the(sh D)),Done)))"
(is "?P ⟹ P ⊢ ?s1 -jvm→ ?s2")
proof -
assume ?P
then have "exec (P, ?s1) = ⌊?s2⌋" by(cases frs) auto
then have "(?s1, ?s2) ∈ (exec_1 P)⇧*"
by(rule exec_1I[THEN r_into_rtrancl])
then show ?thesis by(simp add: exec_all_def1)
qed

lemma jvm_InitNone:
"⟦ ics_of f = Calling C Cs;
sh C = None ⟧
⟹ P ⊢ (None,h,f#frs,sh) -jvm→ (None,h,f#frs,sh(C ↦ (sblank P C, Prepared)))"
(is "⟦ ?P; ?Q ⟧ ⟹ P ⊢ ?s1 -jvm→ ?s2")
proof -
assume assms: ?P ?Q
then obtain stk1 loc1 C1 M1 pc1 ics1 where "f = (stk1,loc1,C1,M1,pc1,ics1)"
by(cases f) simp
then have "exec (P, ?s1) = ⌊?s2⌋" using assms
by(case_tac ics1) simp_all
then have "(?s1, ?s2) ∈ (exec_1 P)⇧*"
by(rule exec_1I[THEN r_into_rtrancl])
then show ?thesis by(simp add: exec_all_def1)
qed

lemma jvm_InitDP:
"⟦ ics_of f = Calling C Cs;
sh C = ⌊(sfs,i)⌋; i = Done ∨ i = Processing ⟧
⟹ P ⊢ (None,h,f#frs,sh) -jvm→ (None,h,(calling_to_scalled f)#frs,sh)"
(is "⟦ ?P; ?Q; ?R ⟧ ⟹ P ⊢ ?s1 -jvm→ ?s2")
proof -
assume assms: ?P ?Q ?R
then obtain stk1 loc1 C1 M1 pc1 ics1 where "f = (stk1,loc1,C1,M1,pc1,ics1)"
by(cases f) simp
then have "exec (P, ?s1) = ⌊?s2⌋" using assms
by(case_tac i) simp_all
then have "(?s1, ?s2) ∈ (exec_1 P)⇧*"
by(rule exec_1I[THEN r_into_rtrancl])
then show ?thesis by(simp add: exec_all_def1)
qed

lemma jvm_InitError:
"sh C = ⌊(sfs,Error)⌋
⟹ P ⊢ (None,h,(vs,ls,C⇩0,M,pc,Calling C Cs)#frs,sh)
by(clarsimp simp: exec_all_def1 intro!: r_into_rtrancl exec_1I)

lemma exec_ErrorThrowing:
"sh C = ⌊(sfs,Error)⌋
⟹ exec (P, (None,h,calling_to_throwing (stk,loc,D,M,pc,Calling C Cs) a#frs,sh))
= Some (None,h,calling_to_sthrowing (stk,loc,D,M,pc,Calling C Cs) a #frs,sh)"
by(clarsimp simp: exec_all_def1 fun_upd_idem_iff intro!: r_into_rtrancl exec_1I)

lemma jvm_InitObj:
"⟦ sh C = Some(sfs,Prepared);
C = Object;
sh' = sh(C ↦ (sfs,Processing)) ⟧
⟹ P ⊢ (None, h, (vs,ls,C⇩0,M,pc,Calling C Cs)#frs, sh) -jvm→
(None, h, (vs,ls,C⇩0,M,pc,Called (C#Cs))#frs,sh')"
(is "⟦ ?P; ?Q; ?R ⟧ ⟹ P ⊢ ?s1 -jvm→ ?s2")
proof -
assume assms: ?P ?Q ?R
then have "exec (P, ?s1) = ⌊?s2⌋"
by(case_tac "method P C clinit") simp
then have "(?s1, ?s2) ∈ (exec_1 P)⇧*"
by(rule exec_1I[THEN r_into_rtrancl])
then show ?thesis by(simp add: exec_all_def1)
qed

lemma jvm_InitNonObj:
"⟦ sh C = Some(sfs,Prepared);
C ≠ Object;
class P C = Some (D,r);
sh' = sh(C ↦ (sfs,Processing)) ⟧
⟹ P ⊢ (None, h, (vs,ls,C⇩0,M,pc,Calling C Cs)#frs, sh) -jvm→
(None, h, (vs,ls,C⇩0,M,pc,Calling D (C#Cs))#frs, sh')"
(is "⟦ ?P; ?Q; ?R; ?S ⟧ ⟹ P ⊢ ```