Theory Correctness2

(*  Title:      JinjaDCI/Compiler/Correctness2.thy
    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   TUM 2003, UIUC 2019-20

    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 ⊳ []"
(*<*)by(simp add:before_def)(*>*)


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)"
(*<*)
by(subst add.commute)
  (fastforce simp add:before_def prefix_def drop_drop[symmetric])
(*>*)

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


lemma [simp]: "P,C,M,pc ▹ i ⟹ instrs_of P C M ! pc = i"
(*<*)by(clarsimp simp add:at_def strict_prefix_def nth_via_drop)(*>*)

lemma beforeM:
  "P ⊢ C sees M,b: Ts→T = body in D ⟹
  compP⇩2 P,D,M,0 ⊳ compE⇩2 body @ [Return]"
(*<*)by(drule sees_method_idemp) (simp add:before_def compMb⇩2_def)(*>*)

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)
qed (simp_all add:pcs_def)
(*>*)


lemma [simp]: "pcs [] = {}"
(*<*)by(simp add:pcs_def)(*>*)


lemma [simp]: "pcs (x#xt) = {fst x ..< fst(snd x)} ∪ pcs xt"
(*<*)by(auto simp add: pcs_def)(*>*)


lemma [simp]: "pcs(xt⇩1 @ xt⇩2) = pcs xt⇩1 ∪ pcs xt⇩2"
(*<*)by(simp add:pcs_def)(*>*)


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)"
    by(force simp add:matches_ex_entry_def pcs_def)
  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)"
    by(force simp add:matches_ex_entry_def pcs_def)
  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)"
(*<*)by(simp add:matches_ex_entry_def)(*>*)


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"
(*<*)by(auto simp add:beforex_def)(*>*)


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 nat_add_distrib[simp] caught_def[simp]
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)
   -jvm→ (None,h,(vs,ls,C⇩0,M,pc,Throwing Cs (addr_of_sys_xcpt NoClassDefFoundError))#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 ⊢