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 ⊳ (is1 @ is2) = (P,C,M,pc ⊳ is1 ∧ P,C,M,pc + size is1 ⊳ is2)"
(*<*)
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 ⟹
  compP2 P,D,M,0 ⊳ compE2 body @ [Return]"
(*<*)by(drule sees_method_idemp) (simp add:before_def compMb2_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(compxE2 e pc d) ⊆ {pc..<pc+size(compE2 e)})"
and "(⋀pc d. pcs(compxEs2 es pc d) ⊆ {pc..<pc+size(compEs2 es)})"
(*<*)
proof(induct e and es rule: compxE2.induct compxEs2.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(xt1 @ xt2) = pcs xt1 ∪ pcs xt2"
(*<*)by(simp add:pcs_def)(*>*)


lemma [simp]: "pc < pc0 ∨ pc0+size(compE2 e) ≤ pc ⟹ pc ∉ pcs(compxE2 e pc0 d)"
(*<*)using pcs_subset by fastforce(*>*)


lemma [simp]: "pc < pc0 ∨ pc0+size(compEs2 es) ≤ pc ⟹ pc ∉ pcs(compxEs2 es pc0 d)"
(*<*)using pcs_subset by fastforce(*>*)


lemma [simp]: "pc1 + size(compE2 e1) ≤ pc2 ⟹ pcs(compxE2 e1 pc1 d1) ∩ pcs(compxE2 e2 pc2 d2) = {}"
(*<*)using pcs_subset by fastforce(*>*)


lemma [simp]: "pc1 + size(compE2 e) ≤ pc2 ⟹ pcs(compxE2 e pc1 d1) ∩ pcs(compxEs2 es pc2 d2) = {}"
(*<*)using pcs_subset by fastforce(*>*)


lemma [simp]:
 "pc ∉ pcs xt0 ⟹ match_ex_table P C pc (xt0 @ xt1) = match_ex_table P C pc xt1"
(*<*)by (induct xt0) (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(compxE2 e pc d)" and outside: "pc' < pc ∨ pc+size(compE2 e) ≤ pc'"
shows "¬ matches_ex_entry P C pc' xe"
(*<*)
proof
  assume "matches_ex_entry P C pc' xe"
  with xe have "pc' ∈ pcs(compxE2 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(compxEs2 es pc d)" and outside: "pc' < pc ∨ pc+size(compEs2 es) ≤ pc'"
shows "¬ matches_ex_entry P C pc' xe"
(*<*)
proof
  assume "matches_ex_entry P C pc' xe"
  with xe have "pc' ∈ pcs(compxEs2 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 xt1. ¬ matches_ex_entry P D pc xte ⟹
  match_ex_table P D pc (xt1 @ xt) = match_ex_table P D pc xt"
(*<*)by(induct xt1) 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 ⟷
  (∃xt0 xt1. ex_table_of P C M = xt0 @ xt @ xt1 ∧ pcs xt0 ∩ I = {} ∧ pcs xt ⊆ I ∧
    (∀pc ∈ I. ∀C pc' d'. match_ex_table P C pc xt1 = ⌊(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
"beforex0 P C M d I xt xt0 xt1
  ≡ ex_table_of P C M = xt0 @ xt @ xt1 ∧ pcs xt0 ∩ I = {}
      ∧ pcs xt ⊆ I ∧ (∀pc ∈ I. ∀C pc' d'. match_ex_table P C pc xt1 = ⌊(pc',d')⌋ ⟶ d' ≤ d)"

lemma beforex_beforex0_eq:
 "P,C,M ⊳ xt / I,d ≡ ∃xt0 xt1. beforex0 P C M d I xt xt0 xt1"
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 xt1 ∩ pcs xt2 = {} ⟹
  P,C,M ⊳ xt1 @ xt2/I,d =
  (P,C,M ⊳ xt1/I-pcs xt2,d  ∧  P,C,M ⊳ xt2/I-pcs xt1,d ∧ P,C,M ▹ xt1@xt2/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 = "xt1 @ xt2"
    let ?beforex = "beforex0 P C M d"
    obtain xt0 xt1' where beforex: "?beforex I ?xt xt0 xt1'"
      using hyp by(clarsimp simp: beforex_def)
    have "∃xt0 xt1'. ?beforex (I - pcs xt2) xt1 xt0 xt1'" ― ‹?P1›
      using pcs beforex by(rule_tac x=xt0 in exI) auto
    moreover have "∃xt0 xt1'. ?beforex (I - pcs xt1) xt2 xt0 xt1'"  ― ‹?P2›
      using pcs beforex by(rule_tac x="xt0@xt1" 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 ⊳ xt1 @ xt2 @ [(f,t,D,h,d)] / I,d"
  and pcs: "pcs xt1 ⊆ J" and JI: "J ⊆ I" and Jpcs: "J ∩ pcs xt2 = {}"
shows "P,C,M ⊳ xt1 / J,d"
(*<*)
proof -
  let ?beforex = "beforex0 P C M d"
  obtain xt0 xt1' where bx': "?beforex I (xt1 @ xt2 @ [(f,t,D,h,d)]) xt0 xt1'"
    using bx by(clarsimp simp:beforex_def)
  let ?xt0 = xt0 and ?xt1 = "xt2 @ (f, t, D, h, d) # xt1'"
  have "pcs xt0 ∩ J = {}" using bx' JI by blast
  moreover {
    fix pc C pc' d' assume pcJ: "pc∈J"
    then have "pc ∉ pcs xt2" using bx' Jpcs by blast
    then have "match_ex_table P C pc (xt2 @ (f, t, D, h, d) # xt1')
                   = ⌊(pc', d')⌋ ⟶ d' ≤ d"
      using bx' JI pcJ by (auto split:if_split_asm)
  }
  ultimately have "?beforex J xt1 ?xt0 ?xt1" using bx' pcs by simp
  then show ?thesis using beforex_def by blast
qed
(*>*)


lemma beforex_appendD2:
assumes bx: "P,C,M ⊳ xt1 @ xt2 @ [(f,t,D,h,d)] / I,d"
  and pcs: "pcs xt2 ⊆ J" and JI: "J ⊆ I" and Jpcs: "J ∩ pcs xt1 = {}"
shows "P,C,M ⊳ xt2 / J,d"
(*<*)
proof -
  let ?beforex = "beforex0 P C M d"
  obtain xt0 xt1' where bx': "?beforex I (xt1 @ xt2 @ [(f,t,D,h,d)]) xt0 xt1'"
    using bx by(clarsimp simp:beforex_def)
  then have "∃xt1''. beforex0 P C M d J xt2 (xt0 @ xt1) xt1''"
    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 ⟹ compP2 P,D,M ⊳ compxE2 body 0 0/{..<size(compE2 body)},0"
(*<*)
proof -
  assume cM: "P ⊢ C sees M,b: Ts→T = body in D"
  let ?xt0 = "[]"
  have "∃xt1. beforex0 (compP2 P) D M 0 ({..<size(compE2 body)}) (compxE2 body 0 0) ?xt0 xt1"
    using sees_method_compP[where f = compMb2, OF sees_method_idemp[OF cM]]
          pcs_subset by(fastforce simp add: compP2_def compMb2_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 xt0 xt1 where bx': "beforex0 P C M d I xt xt0 xt1"
    using bx by(clarsimp simp:beforex_def)
  then have "pc ∉ pcs xt0" 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 :: "J1_prog ⇒ ty list ⇒ cname ⇒ mname ⇒ val list ⇒ pc ⇒ init_call_status
   ⇒ nat set ⇒ heap ⇒ sheap ⇒ expr1 ⇒ bool" where
"Jcc_cond P E C M vs pc ics I h sh (INIT C0 (Cs,b) ← e')
  = ((∃T. P,E,h,sh ⊢1 INIT C0 (Cs,b) ← e' : T) ∧ unit = e' ∧ ics = No_ics)" |
"Jcc_cond P E C M vs pc ics I h sh (RI(C',e0);Cs ← e')
  = (((e0 = C'∙sclinit([]) ∧ (∃T. P,E,h,sh ⊢1 RI(C',e0);Cs ← e':T))
         ∨ ((∃a. e0 = 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 (compP2 P,C,M,pc ⊳ compE2 e ∧ compP2 P,C,M ⊳ compxE2 e pc (size vs)/I,size vs
                  ∧ {pc..<pc+size(compE2 e)} ⊆ I ∧ ¬sub_RI e ∧ ics = No_ics)
    )" |
"Jcc_cond P E C M vs pc ics I h sh e
  = (compP2 P,C,M,pc ⊳ compE2 e ∧ compP2 P,C,M ⊳ compxE2 e pc (size vs)/I,size vs
                  ∧ {pc..<pc+size(compE2 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 ⇒ expr1 ⇒ frame list" where
"Jcc_frames P C M vs ls pc ics frs (INIT C0 (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 C0 (Nil,b) ← e')
  = (vs,ls,C,M,pc,Called [])#frs" |
"Jcc_frames P C M vs ls pc ics frs (RI(C',e0);Cs ← e')
  = (case e0 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 :: "J1_prog ⇒ ty list ⇒ cname ⇒ mname ⇒ val list ⇒ val list ⇒ pc ⇒ init_call_status
  ⇒ frame list ⇒ heap ⇒ val list ⇒ sheap ⇒ val ⇒ expr1 ⇒ jvm_state" where
"Jcc_rhs P E C M vs ls pc ics frs h' ls' sh' v (INIT C0 (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',e0);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(compE2 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(compE2 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 ⇒ expr1
  ⇒ bool" where
"Jcc_err P C M h vs ls pc ics frs sh I h' ls' sh' xa (INIT C0 (Cs,b) ← e')
  = (∃vs'. P ⊢ (None,h,Jcc_frames P C M vs ls pc ics frs (INIT C0 (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',e0);Cs ← e')
  = (∃vs'. P ⊢ (None,h,Jcc_frames P C M vs ls pc ics frs (RI(C',e0);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 (∃pc1. pc ≤ pc1 ∧ pc1 < pc + size(compE2 e) ∧
               ¬ caught P pc1 h' xa (compxE2 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' pc1 ics frs sh'))
    )" |
"Jcc_err P C M h vs ls pc ics frs sh I h' ls' sh' xa e
  = (∃pc1. pc ≤ pc1 ∧ pc1 < pc + size(compE2 e) ∧
               ¬ caught P pc1 h' xa (compxE2 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' pc1 ics frs sh'))"

fun Jcc_pieces :: "J1_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 ⇒ expr1
  ⇒ 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 (compP2 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 (compP2 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 ≡ compP2 P1"
  and nsub: "¬sub_RI e"
shows "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh' v xa e 
  = (let cond = P,C,M,pc ⊳ compE2 e ∧ P,C,M ⊳ compxE2 e pc (size vs)/I,size vs
                  ∧ {pc..<pc+size(compE2 e)} ⊆ I ∧ ics = No_ics;
         frs' = (vs,ls,C,M,pc,ics)#frs;
         rhs = (None,h',(v#vs,ls',C,M,pc+size(compE2 e),ics)#frs,sh');
         err = (∃pc1. pc ≤ pc1 ∧ pc1 < pc + size(compE2 e) ∧
               ¬ caught P pc1 h' xa (compxE2 e pc (size vs)) ∧
               (∃vs'. P ⊢ (None,h,frs',sh) -jvm→ handle P C M xa h' (vs'@vs) ls' pc1 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 ≡ compP2 P1"
 and "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (Cast C' e)
   = (True, frs0, (xp',h',(v#vs',ls',C0,M',pc',ics')#frs',sh'), err)"
shows "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v' xa e
   = (True, frs0, (xp',h',(v'#vs',ls',C0,M',pc' - 1,ics')#frs',sh'),
        (∃pc1. pc ≤ pc1 ∧ pc1 < pc + size(compE2 e) ∧
               ¬ caught P pc1 h1 xa (compxE2 e pc (size vs)) ∧
               (∃vs'. P ⊢ (None,h0,frs0,sh0) -jvm→ handle P C M xa h1 (vs'@vs) ls1 pc1 ics frs sh1)))"
proof -
  have pc: "{pc..<pc + length (compE2 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 h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e «bop» e')
   = (True, frs0, (xp',h',(v#vs',ls',C0,M',pc',ics')#frs',sh'), err)"
shows "∃err. Jcc_pieces P E C M h0 vs ls0 pc ics frs sh0
 (I - pcs (compxE2 e' (pc + length (compE2 e)) (Suc (length vs')))) h1 ls1 sh1 v' xa e
   = (True, frs0, (xp',h1,(v'#vs',ls1,C0,M',pc' - size (compE2 e') - 1,ics')#frs',sh1), err)"
proof -
  have bef: "compP compMb2 P,C0,M' ⊳ compxE2 e pc (length vs) 
         / I - pcs (compxE2 e' (pc + length (compE2 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 ≡ compP2 P1"
 and "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e «bop» e')
   = (True, frs0, (xp',h',(v#vs',ls',C0,M',pc',ics')#frs',sh'), err)"
shows "∃err. Jcc_pieces P1 E C M h1 (v1#vs) ls1 (pc + size (compE2 e)) ics frs sh1
   (I - pcs (compxE2 e pc (length vs'))) h2 ls2 sh2 v' xa e'
   = (True, (v1#vs,ls1,C,M,pc + size (compE2 e),ics)#frs,
       (xp',h',(v'#v1#vs',ls',C0,M',pc' - 1,ics')#frs',sh'),
          (∃pc1. pc + size (compE2 e) ≤ pc1 ∧ pc1 < pc + size (compE2 e) + length (compE2 e') ∧
               ¬ caught P pc1 h2 xa (compxE2 e' (pc + size (compE2 e)) (Suc (length vs))) ∧
               (∃vs'. P ⊢ (None,h1,(v1#vs,ls1,C,M,pc + size (compE2 e),ics)#frs,sh1)
                       -jvm→ handle P C M xa h2 (vs'@v1#vs) ls2 pc1 ics frs sh2)))"
proof -
  have bef: "compP compMb2 P1,C0,M' ⊳ compxE2 e pc (length vs) 
         / I - pcs (compxE2 e' (pc + length (compE2 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 h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (e∙F{D})
   = (True, frs0, (xp',h',(v#vs',ls',C0,M',pc',ics')#frs',sh'), err)"
shows "∃err. Jcc_pieces P E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v' xa e
   = (True, frs0, (xp',h',(v'#vs',ls',C0,M',pc' - 1,ics')#frs',sh'), err)"
proof -
  have pc: "{pc..<pc + length (compE2 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 ≡ compP2 P1"
 and "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (i:=e)
   = (True, frs0, (xp',h',(v#vs',ls',C0,M',pc',ics')#frs',sh'), err)"
shows "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v' xa e
   = (True, frs0, (xp',h',(v'#vs',ls',C0,M',pc' - 2,ics')#frs',sh'),
        (∃pc1. pc ≤ pc1 ∧ pc1 < pc + size(compE2 e) ∧
               ¬ caught P pc1 h1 xa (compxE2 e pc (size vs)) ∧
               (∃vs'. P ⊢ (None,h0,frs0,sh0) -jvm→ handle P C M xa h1 (vs'@vs) ls1 pc1 ics frs sh1)))"
proof -
  have pc: "{pc..<pc + length (compE2 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 h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e∙F{D}:=e')
   = (True, frs0, (xp',h',(v#vs',ls',C0,M',pc',ics')#frs',sh'), err)"
shows "∃err. Jcc_pieces P E C M h0 vs ls0 pc ics frs sh0
 (I - pcs (compxE2 e' (pc + length (compE2 e)) (Suc (length vs')))) h1 ls1 sh1 v' xa e
   = (True, frs0, (xp',h1,(v'#vs',ls1,C0,M',pc' - size (compE2 e') - 2,ics')#frs',sh1), 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 h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e∙F{D}:=e')
   = (True, frs0, (xp',h',(v#vs',ls',C0,M',pc',ics')#frs',sh'), err)"
shows "Jcc_pieces P E C M h1 (v1#vs) ls1 (pc + size (compE2 e)) ics frs sh1
   (I - pcs (compxE2 e pc (length vs'))) h2 ls2 sh2 v' xa e'
   = (True, (v1#vs,ls1,C,M,pc + size (compE2 e),ics)#frs,
       (xp',h',(v'#v1#vs',ls',C0,M',pc' - 2,ics')#frs',sh'),
        (∃pc1. (pc + size (compE2 e)) ≤ pc1 ∧ pc1 < pc + size (compE2 e) + size(compE2 e') ∧
               ¬ caught (compP2 P) pc1 h2 xa (compxE2 e' (pc + size (compE2 e)) (size (v1#vs))) ∧
               (∃vs'. (compP2 P) ⊢ (None,h1,(v1#vs,ls1,C,M,pc + size (compE2 e),ics)#frs,sh1)
                                   -jvm→ handle (compP2 P) C M xa h2 (vs'@v1#vs) ls2 pc1 ics frs sh2)))"
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 h0 vs ls0 pc ics frs sh0 I h' ls' sh' v xa (C'∙sF{D}:=e)
   = (True, frs0, (xp',h',(v#vs',ls',C0,M',pc',ics')#frs',sh'), err)"
shows "∃err. Jcc_pieces P E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v' xa e
   = (True, frs0, (xp',h1,(v'#vs',ls1,C0,M',pc' - 2,ics')#frs',sh1), err)"
proof -
  have pc: "{pc..<pc + length (compE2 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 h0 vs ls0 pc ics frs sh0 I h3 ls3 sh3 v xa (e∙M0(es))
   = (True, frs0, (xp',h',(v#vs',ls',C',M',pc',ics')#frs',sh'), err)"
shows "∃err. Jcc_pieces P E C M h0 vs ls0 pc ics frs sh0
    (I - pcs (compxEs2 es (pc + length (compE2 e)) (Suc (length vs')))) h1 ls1 sh1 v' xa e
   = (True, frs0,
       (xp',h1,(v'#vs',ls1,C',M',pc' - size (compEs2 es) - 1,ics')#frs',sh1), err)"
proof -
  show ?thesis using assms nsub_RI_Jcc_pieces[where e=e] by clarsimp
qed

lemma Jcc_pieces_clinit:
assumes [simp]: "P ≡ compP2 P1"
  and cond: "Jcc_cond P1 E C M vs pc ics I h sh (C1∙sclinit([]))"
shows "Jcc_pieces P1 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 ≡ compP2 P1" and wf: "wf_J1_prog P1"
 and "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h3 ls2 sh3 v xa (C1∙sclinit([]))
         = (True, frs', rhs', err')"
 and method: "P1 ⊢ C1 sees clinit,Static: []→Void = body in D"
shows "Jcc_pieces P1 [] D clinit h2 [] (replicate (max_vars body) undefined) 0
          No_ics (tl frs') sh2 {..<length (compE2 body)} h3 ls3 sh3 v xa body
           = (True, frs', 
                (None,h3,([v],ls3,D,clinit,size(compE2 body), No_ics)#tl frs',sh3),
                    ∃pc1. 0 ≤ pc1 ∧ pc1 < size(compE2 body) ∧
                      ¬ caught P pc1 h3 xa (compxE2 body 0 0) ∧
                      (∃vs'. P ⊢ (None,h2,frs',sh2) -jvm→ handle P D clinit xa h3 vs' ls3 pc1
                            No_ics (tl frs') sh3))"
proof -
  have M_in_D: "P1 ⊢ D sees clinit,Static: []→Void = body in D"
    using method by(rule sees_method_idemp) 
  hence M_code: "compP2 P1,D,clinit,0 ⊳ compE2 body @ [Return]"
    and M_xtab: "compP2 P1,D,clinit ⊳ compxE2 body 0 0/{..<size(compE2 body)},0"
    by(rule beforeM, rule beforexM)
  have nsub: "¬sub_RI body" by(rule sees_wf1_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 ≡ compP2 P1"
 and "P,C,M,pc ⊳ compEs2 (e#es)" and "P,C,M ⊳ compxEs2 (e#es) pc (size vs)/I,size vs"
 and "{pc..<pc+size(compEs2 (e#es))} ⊆ I"
 and "ics = No_ics"
 and "¬sub_RIs (e#es)"
shows "Jcc_pieces P1 E C M h vs ls pc ics frs sh
  (I - pcs (compxEs2 es (pc + length (compE2 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 (compE2 e), ics) # frs, sh'),
          ∃pc1≥pc. pc1 < pc + length (compE2 e) ∧ ¬ caught P pc1 h' xa (compxE2 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' pc1 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 ≡ compP2 P1"
 and "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh' v xa (INIT C' (C0 # Cs,False) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
shows
 "Jcc_pieces P1 E C M h vs l pc ics frs (sh(C0 ↦ (sblank P C0, Prepared)))
     I h' l' sh' v xa (INIT C' (C0 # Cs,False) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'),
        ∃vs'. P ⊢ (None,h,frs',(sh(C0 ↦ (sblank P1 C0, Prepared))))
            -jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh')"
proof -
  have  "Jcc_cond P1 E C M vs pc ics I h sh (INIT C' (C0 # Cs,False) ← e)" using assms by simp
  then obtain T where "P1,E,h,sh ⊢1 INIT C' (C0 # Cs,False) ← unit : T" by fastforce
  then have "P1,E,h,sh(C0 ↦ (sblank P1 C0, Prepared)) ⊢1 INIT C' (C0 # Cs,False) ← unit : T"
    by(auto simp: fun_upd_apply)
  then have "Ex (WTrt21 P1 E h (sh(C0 ↦ (sblank P1 C0, Prepared))) (INIT C' (C0 # Cs,False) ← unit))"
    by(simp only: exI)
  then show ?thesis using assms by clarsimp
qed

lemma Jcc_pieces_InitDP:
assumes [simp]: "P ≡ compP2 P1"
 and "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh' v xa (INIT C' (C0 # Cs,False) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
shows
 "Jcc_pieces P1 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 P1 E C M vs pc ics I h sh (INIT C' (C0 # Cs,False) ← e)" using assms by simp
  then obtain T where "P1,E,h,sh ⊢1 INIT C' (C0 # Cs,False) ← unit : T" by fastforce
  then have "P1,E,h,sh ⊢1 INIT C' (Cs,True) ← unit : T"
    by (auto; metis list.sel(2) list.set_sel(2))
  then have wtrt: "Ex (WTrt21 P1 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 ≡ compP2 P1"
 and "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh' v xa (INIT C' (C0 # Cs,False) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
 and err: "sh C0 = Some(sfs,Error)"
shows
 "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh' v xa (RI (C0, 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 C0 clinit") clarsimp
  qed(clarsimp)
qed

lemma Jcc_pieces_InitObj:
assumes [simp]: "P ≡ compP2 P1"
 and "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' (sh(C0 ↦ (sfs,Processing))) v xa (INIT C' (C0 # Cs,False) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
shows
 "Jcc_pieces P1 E C M h vs l pc ics frs (sh(C0 ↦ (sfs,Processing))) I h' l' sh'' v xa (INIT C' (C0 # 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 P1 E C M vs pc ics I h sh (INIT C' (C0 # Cs,False) ← e)" using assms by simp
  then obtain T where "P1,E,h,sh ⊢1 INIT C' (C0 # Cs,False) ← unit : T" by fastforce
  then have "P1,E,h,sh(C0 ↦ (sfs,Processing)) ⊢1 INIT C' (C0 # Cs,True) ← unit : T"
    using assms by clarsimp (auto simp: fun_upd_apply)
  then have wtrt: "Ex (WTrt21 P1 E h (sh(C0 ↦ (sfs,Processing))) (INIT C' (C0 # Cs,True) ← unit))"
    by(simp only: exI)
  show ?thesis using assms wtrt by clarsimp
qed

lemma Jcc_pieces_InitNonObj:
assumes [simp]: "P ≡ compP2 P1"
 and "is_class P1 D" and "D ∉ set (C0#Cs)" and "∀C ∈ set (C0#Cs). P1 ⊢ C ≼* D"
 and pcs: "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' (sh(C0 ↦ (sfs,Processing))) v xa (INIT C' (C0 # Cs,False) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
shows
 "Jcc_pieces P1 E C M h vs l pc ics frs (sh(C0 ↦ (sfs,Processing))) I h' l' sh'' v xa (INIT C' (D # C0 # 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 P1 E C M vs pc ics I h sh (INIT C' (C0 # Cs,False) ← e)" using assms by simp
  then obtain T where "P1,E,h,sh ⊢1 INIT C' (C0 # Cs,False) ← unit : T" by fastforce
  then have "P1,E,h,sh(C0 ↦ (sfs,Processing)) ⊢1 INIT C' (D # C0 # Cs,False) ← unit : T"
    using assms by clarsimp (auto simp: fun_upd_apply)
  then have wtrt: "Ex (WTrt21 P1 E h (sh(C0 ↦ (sfs,Processing))) (INIT C' (D # C0 # Cs,False) ← unit))"
    by(simp only: exI)
  show ?thesis using assms wtrt by clarsimp
qed

lemma Jcc_pieces_InitRInit:
assumes [simp]: "P ≡ compP2 P1" and wf: "wf_J1_prog P1"
 and "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh' v xa (INIT C' (C0 # Cs,True) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
shows
 "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh' v xa (RI (C0,C0∙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 P1 E C M vs pc ics I h sh (INIT C' (C0 # Cs,True) ← e)" using assms by simp
  then have clinit: "∃T. P1,E,h,sh ⊢1 C0∙sclinit([]) : T" using wf
    by clarsimp (auto simp: is_class_def intro: wf1_types_clinit)
  then obtain T where cT: "P1,E,h,sh ⊢1 C0∙sclinit([]) : T" by blast
  obtain T where "P1,E,h,sh ⊢1 INIT C' (C0 # Cs,True) ← unit : T" using cond by fastforce
  then have "P1,E,h,sh ⊢1 RI (C0,C0∙sclinit([])) ; Cs ← unit : T"
    using assms by (auto intro: cT)
  then have wtrt: "Ex (WTrt21 P1 E h sh (RI (C0,C0∙sclinit([])) ; Cs ← unit))"
    by(simp only: exI)
  then show ?thesis using assms by simp
qed

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

lemma Jcc_pieces_RInit_Init:
assumes [simp]: "P ≡ compP2 P1" and wf: "wf_J1_prog P1"
 and proc: "∀C' ∈ set Cs. ∃sfs. sh'' C' = ⌊(sfs,Processing)⌋"
 and "Jcc_pieces P1 E C M h vs l pc ics frs sh I h1 l1 sh1 v xa (RI (C0,C0∙sclinit([]));Cs ← e)
    = (True, frs',
         (None, h1, (vs, l, C, M, pc, Called []) # frs, sh1), err)"
shows
 "Jcc_pieces P1 E C M h' vs l pc ics frs sh'' I h1 l1 sh1 v xa (INIT (last (C0#Cs)) (Cs,True) ← e)
    = (True, (vs, l, C, M, pc, Called Cs) # frs,
         (None, h1, (vs, l, C, M, pc, Called []) # frs, sh1),
             ∃vs'. P ⊢ (None,h',(vs, l, C, M, pc, Called Cs) # frs,sh'')
                        -jvm→ handle P C M xa h1 (vs'@vs) l pc ics frs sh1)"
proof -
  have "Jcc_cond P1 E C M vs pc ics I h sh (RI (C0,C0∙sclinit([]));Cs ← e)" using assms by simp
  then have "Ex (WTrt21 P1 E h sh (RI (C0,C0∙sclinit([])) ; Cs ← unit))" by simp
  then obtain T where riwt: "P1,E,h,sh ⊢1 RI (C0,C0∙sclinit([]));Cs ← unit : T" by meson
  then have "P1,E,h',sh'' ⊢1 INIT (last (C0#Cs)) (Cs,True) ← unit : T" using proc
  proof(cases Cs) qed(auto)
  then have wtrt: "Ex (WTrt21 P1 E h' sh'' (INIT (last (C0#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 ≡ compP2 P1"
 and "Jcc_pieces P1 E C M h vs l pc ics frs sh I h1 l1 sh1 v xa (RI (C0,e);D#Cs ← e')
    = (True, frs', rhs, err)"
 and hd: "hd frs' = (vs1,l1,C1,M1,pc1,ics1)"
shows
 "Jcc_pieces P1 E C M h' vs l pc ics frs sh'' I h1 l1 sh1 v xa (RI (D,Throw xa) ; Cs ← e')
    = (True, (vs1, l1, C1, M1, pc1, Throwing (D#Cs) xa) # tl frs',
         (None, h1, (vs, l, C, M, pc, Called []) # frs, sh1),
             ∃vs'. P ⊢ (None,h',(vs1, l1, C1, M1, pc1, Throwing (D#Cs) xa) # tl frs',sh'')
                        -jvm→ handle P C M xa h1 (vs'@vs) l pc ics frs sh1)"
using assms by(case_tac "method P D clinit", cases "e = C0∙sclinit([])") clarsimp+


subsubsection "JVM stepping lemmas"

lemma jvm_Invoke:
assumes [simp]: "P ≡ compP2 P1"
 and "P,C,M,pc ▹ Invoke M' (length Ts)"
 and ha: "h2 a = ⌊(Ca, fs)⌋" and method: "P1 ⊢ Ca sees M', NonStatic :  Ts→T = body in D"
 and len: "length pvs = length Ts" and "ls2' = Addr a # pvs @ replicate (max_vars body) undefined"
shows "P ⊢ (None, h2, (rev pvs @ Addr a # vs, ls2, C, M, pc, No_ics) # frs, sh2) -jvm→
    (None, h2, ([], ls2', D, M', 0, No_ics) # (rev pvs @ Addr a # vs, ls2, C, M, pc, No_ics) # frs, sh2)"
proof -
  have cname: "cname_of h2 (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 ≡ compP2 P1"
 and "P,C,M,pc ▹ Invokestatic C' M' (length Ts)"
 and sh: "sh2 D = Some(sfs,Done)"
 and method: "P1 ⊢ C' sees M', Static :  Ts→T = body in D"
 and len: "length pvs = length Ts" and "ls2' = pvs @ replicate (max_vars body) undefined"
shows "P ⊢ (None, h2, (rev pvs @ vs, ls2, C, M, pc, No_ics) # frs, sh2) -jvm→
    (None, h2, ([], ls2', D, M', 0, No_ics) # (rev pvs @ vs, ls2, C, M, pc, No_ics) # frs, sh2)"
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 ≡ compP2 P1"                       
 and "P,C,M,pc ▹ Invokestatic C' M' (length Ts)"
 and sh: "sh2 D = Some(sfs,i)"
 and method: "P1 ⊢ C' sees M', Static :  Ts→T = body in D"
 and len: "length pvs = length Ts" and "ls2' = pvs @ replicate (max_vars body) undefined"
shows "P ⊢ (None, h2, (rev pvs @ vs, ls2, C, M, pc, Called []) # frs, sh2) -jvm→
    (None, h2, ([], ls2', D, M', 0, No_ics) # (rev pvs @ vs, ls2, C, M, pc, No_ics) # frs, sh2)"
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 ⊳ compE2 body @ [Return]
  ⟹ P ⊢ (None, h, (vs, ls, D, clinit, size(compE2 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,C0,M,pc,Calling C Cs)#frs,sh)
   -jvm→ (None,h,(vs,ls,C0,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,C0,M,pc,Calling C Cs)#frs, sh) -jvm→
    (None, h, (vs,ls,C0,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,C0,M,pc,Calling C Cs)#frs, sh) -jvm→
    (None, h, (vs,ls,C0,M,pc,Calling D (C#Cs))#frs, sh')"
(is "⟦ ?P; ?Q; ?R; ?S ⟧ ⟹ P ⊢ ?s1 -jvm→ ?s2")
proof -
  assume assms: ?P ?Q ?R ?S
  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_RInit_throw:
 "P ⊢ (None,h,(vs,l,C,M,pc,Throwing [] xa) # frs,sh)
        -jvm→ handle P C M xa h vs l pc No_ics frs sh"
(is "P ⊢ ?s1 -jvm→ ?s2")
proof -
  have "exec (P, ?s1) = ⌊?s2⌋"
    by(simp add: handle_def split: bool.splits)
  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_RInit_throw':
 "P ⊢ (None,h,(vs,l,C,M,pc,Throwing [C'] xa) # frs,sh)
        -jvm→ handle P C M xa h vs l pc No_ics frs (sh(C':=Some(fst(the(sh C')), Error)))"
(is "P ⊢ ?s1 -jvm→ ?s2")
proof -
  let ?sy = "(None,h,(vs,l,C,M,pc,Throwing [] xa) # frs,sh(C':=Some(fst(the(sh C')), Error)))"
  have "exec (P, ?s1) = ⌊?sy⌋" by simp
  then have "(?s1, ?sy) ∈ (exec_1 P)*"
    by(rule exec_1I[THEN r_into_rtrancl])
  also have "(?sy, ?s2) ∈ (exec_1 P)*"
    using jvm_RInit_throw by(simp add: exec_all_def1)
  ultimately show ?thesis by(simp add: exec_all_def1)
qed

lemma jvm_Called:
 "P ⊢ (None, h, (vs, l, C, M, pc, Called (C0 # Cs)) # frs, sh) -jvm→
    (None, h, create_init_frame P C0 # (vs, l, C, M, pc, Called Cs) # frs, sh)"
 by(simp add: exec_all_def1 r_into_rtrancl exec_1I)

lemma jvm_Throwing:
 "P ⊢ (None, h, (vs, l, C, M, pc, Throwing (C0#Cs) xa') # frs, sh) -jvm→
    (None, h, (vs, l, C, M, pc, Throwing Cs xa') # frs, sh(C0 ↦ (fst (the (sh C0)), Error)))"
 by(simp add: exec_all_def1 r_into_rtrancl exec_1I)

subsubsection "Other lemmas for correctness proof"

lemma assumes wf:"wf_prog wf_md P"
 and ex: "class P C = Some a"
shows create_init_frame_wf_eq: "create_init_frame (compP2 P) C = (stk,loc,D,M,pc,ics) ⟹ D=C"
using wf_sees_clinit[OF wf ex] by(cases "method P C clinit", auto)

lemma beforex_try:
assumes pcI: "{pc..<pc+size(compE2(try e1 catch(Ci i) e2))} ⊆ I"
  and bx: "P,C,M ⊳ compxE2 (try e1 catch(Ci i) e2) pc (size vs) / I,size vs"
shows "P,C,M ⊳ compxE2 e1 pc (size vs) / {pc..<pc + length (compE2 e1)},size vs"
proof -
  obtain xt0 xt1 where
   "beforex0 P C M (size vs) I (compxE2 (try e1 catch(Ci i) e2) pc (size vs)) xt0 xt1"
    using bx by(clarsimp simp:beforex_def)
  then have "∃xt1. beforex0 P C M (size vs) {pc..<pc + length (compE2 e1)}
                   (compxE2 e1 pc (size vs)) xt0 xt1"
    using pcI pcs_subset(1) atLeastLessThan_iff by simp blast
  then show ?thesis using beforex_def by blast
qed

― ‹ Evaluation of initialization expressions ›

(* --needs J1 and EConform; version for eval found in Equivalence *)
lemma
shows eval1_init_return: "P ⊢1 ⟨e,s⟩ ⇒ ⟨e',s'⟩
  ⟹ iconf (shp1 s) e
  ⟹ (∃Cs b. e = INIT C' (Cs,b) ← unit) ∨ (∃C e0 Cs ei. e = RI(C,e0);Cs@[C'] ← unit)
     ∨ (∃e0. e = RI(C',e0);Nil ← unit)
  ⟹ (val_of e' = Some v ⟶ (∃sfs i. shp1 s' C' = ⌊(sfs,i)⌋ ∧ (i = Done ∨ i = Processing)))
   ∧ (throw_of e' = Some a ⟶ (∃sfs i. shp1 s' C' = ⌊(sfs,Error)⌋))"
and "P ⊢1 ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ True"
proof(induct rule: eval1_evals1.inducts)
  case (InitFinal1 e s e' s' C b) then show ?case
    by(auto simp: initPD_def dest: eval1_final_same)
next
  case (InitDone1 sh C sfs C' Cs e h l e' s')
  then have "final e'" using eval1_final by simp
  then show ?case
  proof(rule finalE)
    fix v assume e': "e' = Val v" then show ?thesis using InitDone1 initPD_def
    proof(cases Cs) qed(auto)
  next
    fix a assume e': "e' = throw a" then show ?thesis using InitDone1 initPD_def
    proof(cases Cs) qed(auto)
  qed
next
  case (InitProcessing1 sh C sfs C' Cs e h l e' s')
  then have "final e'" using eval1_final by simp
  then show ?case
  proof(rule finalE)
    fix v assume e': "e' = Val v" then show ?thesis using InitProcessing1 initPD_def
    proof(cases Cs) qed(auto)
  next
    fix a assume e': "e' = throw a" then show ?thesis using InitProcessing1 initPD_def
    proof(cases Cs) qed(auto)
  qed
next
  case (InitError1 sh C sfs Cs e h l e' s' C') show ?case
  proof(cases Cs)
    case Nil then show ?thesis using InitError1 by simp
  next
    case (Cons C2 list)
    then have "final e'" using InitError1 eval1_final by simp
    then show ?thesis
    proof(rule finalE)
      fix v assume e': "e' = Val v" show ?thesis
        using InitError1.hyps(2) e' rinit1_throwE by blast
    next
      fix a assume e': "e' = throw a"
      then show ?thesis using Cons InitError1 cons_to_append[of list] by clarsimp
    qed
  qed
next
  case (InitRInit1 C Cs h l sh e' s' C') show ?case
  proof(cases Cs)
    case Nil then show ?thesis using InitRInit1 by simp
  next
    case (Cons C' list) then show ?thesis
      using InitRInit1 Cons cons_to_append[of list] by clarsimp
  qed
next
  case (RInit1 e s v h' l' sh' C sfs i sh'' C' Cs e' e1 s1)
  then have final: "final e1" using eval1_final by simp
  then show ?case
  proof(cases Cs)
    case Nil show ?thesis using final
    proof(rule finalE)
      fix v assume e': "e1 = Val v" show ?thesis
      using RInit1 Nil by(clarsimp, meson fun_upd_same initPD_def)
    next
      fix a assume e': "e1 = throw a" show ?thesis
      using RInit1 Nil by(clarsimp, meson fun_upd_same initPD_def)
    qed
  next
    case (Cons a list) show ?thesis using final
    proof(rule finalE)
      fix v assume e': "e1 = Val v" then show ?thesis
      using RInit1 Cons by(clarsimp, metis last.simps last_appendR list.distinct(1))
    next
      fix a assume e': "e1 = throw a" then show ?thesis
      using RInit1 Cons by(clarsimp, metis last.simps last_appendR list.distinct(1))
    qed
  qed
next
  case (RInitInitFail1 e s a h' l' sh' C sfs i sh'' D Cs e' e1 s1)
  then have final: "final e1" using eval1_final by simp
  then show ?case
  proof(rule finalE)
    fix v assume e': "e1 = Val v" then show ?thesis
    using RInitInitFail1 by(clarsimp, meson exp.distinct(101) rinit1_throwE)
  next
    fix a' assume e': "e1 = Throw a'"
    then have "iconf (sh'(C ↦ (sfs, Error))) a"
      using RInitInitFail1.hyps(1) eval1_final by fastforce
    then show ?thesis using RInitInitFail1 e'
      by(clarsimp, meson Cons_eq_append_conv list.inject)
  qed
qed(auto simp: fun_upd_same)

lemma init1_Val_PD: "P ⊢1 ⟨INIT C' (Cs,b) ← unit,s⟩ ⇒ ⟨Val v,s'⟩
  ⟹ iconf (shp1 s) (INIT C' (Cs,b) ← unit)
  ⟹ ∃sfs i. shp1 s' C' = ⌊(sfs,i)⌋ ∧ (i = Done ∨ i = Processing)"
 by(drule_tac v = v in eval1_init_return, simp+)

lemma init1_throw_PD: "P ⊢1 ⟨INIT C' (Cs,b) ← unit,s⟩ ⇒ ⟨throw a,s'⟩
  ⟹ iconf (shp1 s) (INIT C' (Cs,b) ← unit)
  ⟹ ∃sfs i. shp1 s' C' = ⌊(sfs,Error)⌋"
 by(drule_tac a = a in eval1_init_return, simp+)

lemma rinit1_Val_PD:
assumes eval: "P ⊢1 ⟨RI(C,e0);Cs ← unit,s⟩ ⇒ ⟨Val v,s'⟩"
  and iconf: "iconf (shp1 s) (RI(C,e0);Cs ← unit)" and last: "last(C#Cs) = C'"
shows "∃sfs i. shp1 s' C' = ⌊(sfs,i)⌋ ∧ (i = Done ∨ i = Processing)"
proof(cases Cs)
  case Nil
  then show ?thesis using eval1_init_return[OF eval iconf] last by simp
next
  case (Cons a list)
  then have nNil: "Cs ≠ []" by simp
  then have "∃Cs'. Cs = Cs' @ [C']" using last append_butlast_last_id[OF nNil]
    by(rule_tac x="butlast Cs" in exI) simp
  then show ?thesis using eval1_init_return[OF eval iconf] by simp
qed

lemma rinit1_throw_PD:
assumes eval: "P ⊢1 ⟨RI(C,e0);Cs ← unit,s⟩ ⇒ ⟨throw a,s'⟩"
  and iconf: "iconf (shp1 s) (RI(C,e0);Cs ← unit)" and last: "last(C#Cs) = C'"
shows "∃sfs. shp1 s' C' = ⌊(sfs,Error)⌋"
proof(cases Cs)
  case Nil
  then show ?thesis using eval1_init_return[OF eval iconf] last by simp
next
  case (Cons a list)
  then have nNil: "Cs ≠ []" by simp
  then have "∃Cs'. Cs = Cs' @ [C']" using last append_butlast_last_id[OF nNil]
    by(rule_tac x="butlast Cs" in exI) simp
  then show ?thesis using eval1_init_return[OF eval iconf] by simp
qed

subsubsection "The proof"

lemma fixes P1 defines [simp]: "P ≡ compP2 P1"
assumes wf: "wf_J1_prog P1"
shows Jcc: "P1 ⊢1 ⟨e,(h0,ls0,sh0)⟩ ⇒ ⟨ef,(h1,ls1,sh1)⟩ ⟹
  (⋀E C M pc ics v xa vs frs I.
     ⟦ Jcc_cond P1 E C M vs pc ics I h0 sh0 e ⟧ ⟹
     (ef = Val v ⟶
         P ⊢ (None,h0,Jcc_frames P C M vs ls0 pc ics frs e,sh0)
                -jvm→ Jcc_rhs P1 E C M vs ls0 pc ics frs h1 ls1 sh1 v e)
     ∧
     (ef = Throw xa ⟶ Jcc_err P C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 xa e)
  )"
(*<*)
  (is "_ ⟹ (⋀E C M pc ics v xa vs frs I.
                  PROP ?P e h0 ls0 sh0 ef h1 ls1 sh1 E C M pc ics v xa vs frs I)")
(*>*)
and "P1 ⊢1 ⟨es,(h0,ls0,sh0)⟩ [⇒] ⟨fs,(h1,ls1,sh1)⟩ ⟹
    (⋀C M pc ics ws xa es' vs frs I.
      ⟦ P,C,M,pc ⊳ compEs2 es; P,C,M ⊳ compxEs2 es pc (size vs)/I,size vs;
       {pc..<pc+size(compEs2 es)} ⊆ I; ics = No_ics;
       ¬sub_RIs es ⟧ ⟹
      (fs = map Val ws ⟶
       P ⊢ (None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0) -jvm→
             (None,h1,(rev ws @ vs,ls1,C,M,pc+size(compEs2 es),ics)#frs,sh1))
      ∧
      (fs = map Val ws @ Throw xa # es' ⟶
       (∃pc1. pc ≤ pc1 ∧ pc1 < pc + size(compEs2 es) ∧
                ¬ caught P pc1 h1 xa (compxEs2 es pc (size vs)) ∧
                (∃vs'. P ⊢ (None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0)
                                     -jvm→ handle P C M xa h1 (vs'@vs) ls1 pc1 ics frs sh1))))"
(*<*)
  (is "_ ⟹ (⋀C M pc ics ws xa es' vs frs I.
                  PROP ?Ps es h0 ls0 sh0 fs h1 ls1 sh1 C M pc ics ws xa es' vs frs I)")
proof (induct rule:eval1_evals1_inducts)
  case New1 thus ?case by auto
next
  case (NewFail1 sh C' sfs h ls)
  let ?xa = "addr_of_sys_xcpt OutOfMemory"
  have "P ⊢ (None,h,(vs,ls,C,M,pc,ics)#frs,sh) -jvm→ handle P C M ?xa h vs ls pc ics frs sh"
    using NewFail1 by(clarsimp simp: handle_def)
  then show ?case by(auto intro!: exI[where x="[]"])
next
  case (NewInit1 sh C' h ls v' h' ls' sh' a FDTs h'')
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh' v xa (new C')
    = (True, frs', (None,h',(v#vs,ls',C,M,pc+size(compE2 (new C')),ics)#frs,sh'), err)"
    using NewInit1.prems(1) by clarsimp
  have "Ex (WTrt21 P1 E h sh (INIT C' ([C'],False) ← unit))"
    using has_fields_is_class[OF NewInit1.hyps(5)] by auto
  then obtain err' where pcs':
    "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh' v' xa (INIT C' ([C'],False) ← unit)
    = (True, (vs,ls,C,M,pc,Calling C' []) # frs, (None,h',(vs,ls,C,M,pc,Called [])#frs,sh'), err')"
    using NewInit1.prems(1) by auto
  have IH: "PROP ?P (INIT C' ([C'],False) ← unit) h ls sh (Val v')
             h' ls' sh' E C M pc ics v' xa vs frs I" by fact
  have ls: "ls = ls'" by(rule init1_same_loc[OF NewInit1.hyps(2)])
  obtain sfs i where sh': "sh' C' = Some(sfs,i)"
    using init1_Val_PD[OF NewInit1.hyps(2)] by clarsimp
  have "P ⊢ (None,h,(vs,ls,C,M,pc,ics)#frs,sh) -jvm→ (None,h,(vs,ls,C,M,pc,Calling C' [])#frs,sh)"
  proof(cases "sh C'")
    case None then show ?thesis using NewInit1.prems by(cases ics) auto
  next
    case (Some a)
    then obtain sfs i where "a = (sfs,i)" by(cases a)
    then show ?thesis using NewInit1.hyps(1) NewInit1.prems Some
      by(cases ics; case_tac i) auto
  qed
  also have "P ⊢ … -jvm→ (None, h', (vs, ls, C, M, pc, Called []) # frs, sh')"
    using IH pcs' by auto
  also have "P ⊢ … -jvm→ (None, h'', (Addr a#vs, ls, C, M, Suc pc, ics) # frs, sh')"
    using NewInit1.hyps(1,2,4-6) NewInit1.prems sh' by(cases ics) auto
  finally show ?case using pcs ls by clarsimp
next
  case (NewInitOOM1 sh C' h ls v' h' ls' sh')
  let ?xa = "addr_of_sys_xcpt OutOfMemory"
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh' v xa (new C')
    = (True, frs', (None,h',(v#vs,ls',C,M,pc+size(compE2 (new C')),ics)#frs,sh'), err)"
    using NewInitOOM1.prems(1) by clarsimp
  have "Ex (WTrt21 P1 E h sh (INIT C' ([C'],False) ← unit))" using NewInitOOM1.hyps(5) by auto
  then obtain err' where pcs':
    "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh' v' xa (INIT C' ([C'],False) ← unit)
    = (True, (vs,ls,C,M,pc,Calling C' []) # frs, (None,h',(vs,ls,C,M,pc,Called [])#frs,sh'), err')"
    using NewInitOOM1.prems(1) by auto
  have IH: "PROP ?P (INIT C' ([C'],False) ← unit) h ls sh (Val v')
             h' ls' sh' E C M pc ics v' xa vs frs I" by fact
  have ls: "ls = ls'" by(rule init1_same_loc[OF NewInitOOM1.hyps(2)])
  have "iconf (shp1 (h, ls, sh)) (INIT C' ([C'],False) ← unit)" by simp
  then obtain sfs i where sh': "sh' C' = Some(sfs,i)"
    using init1_Val_PD[OF NewInitOOM1.hyps(2)] by clarsimp
  have "P ⊢ (None,h,(vs,ls,C,M,pc,ics)#frs,sh) -jvm→ (None,h,(vs,ls,C,M,pc,Calling C' [])#frs,sh)"
  proof(cases "sh C'")
    case None then show ?thesis using NewInitOOM1.prems by(cases ics) auto
  next
    case (Some a)
    then obtain sfs i where "a = (sfs,i)" by(cases a)
    then show ?thesis using NewInitOOM1.hyps(1) NewInitOOM1.prems Some
      by(cases ics; case_tac i) auto
  qed
  also have "P ⊢ … -jvm→ (None, h', (vs, ls, C, M, pc, Called []) # frs, sh')"
    using IH pcs' by auto
  also have "P ⊢ … -jvm→ handle P C M ?xa h' vs ls pc ics frs sh'"
    using NewInitOOM1.hyps(1,2,4,5) NewInitOOM1.prems sh' by(auto simp: handle_def)
  finally show ?case using pcs ls by(simp, metis (no_types) append_Nil le_refl lessI)
next
  case (NewInitThrow1 sh C' h ls a h' ls' sh')
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh' v xa (new C')
    = (True, frs', (None,h',(v#vs,ls',C,M,pc+size(compE2 (new C')),ics)#frs,sh'), err)"
    using NewInitThrow1.prems(1) by clarsimp
  obtain a' where throw: "throw a = Throw a'" using eval1_final[OF NewInitThrow1.hyps(2)] by clarsimp
  have "Ex (WTrt21 P1 E h sh (INIT C' ([C'],False) ← unit))" using NewInitThrow1.hyps(4) by auto
  then obtain vs' where pcs':
    "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh' v a' (INIT C' ([C'],False) ← unit)
    = (True, (vs,ls,C,M,pc,Calling C' []) # frs, (None,h',(vs,ls,C,M,pc,Called [])#frs,sh'),
        P ⊢ (None,h,(vs,ls,C,M,pc,Calling C' []) # frs,sh)
               -jvm→ handle P C M a' h' (vs'@vs) ls pc ics frs sh')"
    using NewInitThrow1.prems(1) by simp blast
  have IH: "PROP ?P (INIT C' ([C'],False) ← unit) h ls sh (throw a)
             h' ls' sh' E C M pc ics v a' vs frs I" by fact
  have ls: "ls = ls'" by(rule init1_same_loc[OF NewInitThrow1.hyps(2)])
  then have "P ⊢ (None,h,(vs,ls,C,M,pc,ics)#frs,sh) -jvm→ (None,h,(vs,ls,C,M,pc,Calling C' []) # frs,sh)"
  proof(cases "sh C'")
    case None then show ?thesis using NewInitThrow1.prems by(cases ics) auto
  next
    case (Some a)
    then obtain sfs i where "a = (sfs,i)" by(cases a)
    then show ?thesis using NewInitThrow1.hyps(1) NewInitThrow1.prems Some
      by(cases ics; case_tac i) auto
  qed
  also have "P ⊢ … -jvm→ handle P C M a' h' (vs'@vs) ls pc ics frs sh'" using IH pcs' throw by auto
  finally show ?case using throw ls by auto
next
  case (Cast1 e h0 ls0 sh0 a h1 ls1 sh1 D fs C')
  let ?pc = "pc + length(compE2 e)"
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (Cast C' e)
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (Cast C' e)),ics)#frs,sh1), err)"
    using Cast1.prems(1) by auto
  have IH: "PROP ?P e h0 ls0 sh0 (addr a) h1 ls1 sh1 E C M pc ics (Addr a) xa vs frs I" by fact
  then have "P ⊢ (None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0) -jvm→
             (None,h1,(Addr a#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using Jcc_pieces_Cast[OF assms(1) pcs, of "Addr a"] Cast1.prems pcs by auto
  also have "P ⊢ … -jvm→ (None,h1,(Addr a#vs,ls1,C,M,?pc+1,ics)#frs,sh1)"
    using Cast1 by (auto simp add:cast_ok_def)
  finally show ?case by auto
next
  case (CastNull1 e h0 ls0 sh0 h1 ls1 sh1 C')
  let ?pc = "pc + length(compE2 e)"
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (Cast C' e)
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (Cast C' e)),ics)#frs,sh1), err)"
    using CastNull1.prems(1) by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 null h1 ls1 sh1 E C M pc ics Null xa vs frs I" by fact
  then have "P ⊢ (None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0) -jvm→
             (None,h1,(Null#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using Jcc_pieces_Cast[OF assms(1) pcs, of Null] CastNull1.prems pcs by auto
  also have "P ⊢ … -jvm→ (None,h1,(Null#vs,ls1,C,M,?pc+1,ics)#frs,sh1)"
    using CastNull1 by (auto simp add:cast_ok_def)
  finally show ?case by auto
next
  case (CastFail1 e h0 ls0 sh0 a h1 ls1 sh1 D fs C')
  let ?pc = "pc + length(compE2 e)"
  let ?xa = "addr_of_sys_xcpt ClassCast"
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (Cast C' e)
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (Cast C' e)),ics)#frs,sh1), err)"
    using CastFail1.prems(1) by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 (addr a) h1 ls1 sh1 E C M pc ics (Addr a) xa vs frs I" by fact
  then have "P ⊢ (None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0) -jvm→
             (None,h1,(Addr a#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using Jcc_pieces_Cast[OF assms(1) pcs, of "Addr a"] CastFail1.prems pcs by auto
  also have "P ⊢ … -jvm→ handle P C M ?xa h1 (Addr a#vs) ls1 ?pc ics frs sh1"
    using CastFail1 by (auto simp add:handle_def cast_ok_def)
  finally have exec: "P ⊢ (None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0) -jvm→ …".
  show ?case (is "?N ∧ (?eq ⟶ ?err)")
  proof
    show ?N by simp
  next
    { assume ?eq
      then have ?err using exec by (auto intro!: exI[where x="?pc"] exI[where x="[Addr a]"])
    }
    thus "?eq ⟶ ?err" by simp
  qed
next
  case (CastThrow1 e h0 ls0 sh0 e' h1 ls1 sh1 C')
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (Cast C' e)
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (Cast C' e)),ics)#frs,sh1), err)"
    using CastThrow1.prems(1) by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 (throw e') h1 ls1 sh1 E C M pc ics v xa vs frs I" by fact
  show ?case using IH Jcc_pieces_Cast[OF assms(1) pcs, of v] CastThrow1.prems pcs less_SucI
   by(simp, blast)
next
  case Val1 thus ?case by auto
next
  case Var1 thus ?case by auto
next
  case (BinOp1 e1 h0 ls0 sh0 v1 h1 ls1 sh1 e2 v2 h2 ls2 sh2 bop w)
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e1 «bop» e2)
    = (True, frs', (None,h2,(v#vs,ls2,C,M,pc+size(compE2 (e1 «bop» e2)),ics)#frs,sh2), err)"
    using BinOp1.prems(1) by clarsimp
  let ?pc1 = "pc + length(compE2 e1)"
  let ?pc2 = "?pc1 + length(compE2 e2)"
  have IH1: "PROP ?P e1 h0 ls0 sh0 (Val v1) h1 ls1 sh1 E C M pc ics v1 xa vs frs
                     (I - pcs (compxE2 e2 (pc + length (compE2 e1)) (Suc (length vs))))" by fact
  have IH2: "PROP ?P e2 h1 ls1 sh1 (Val v2) h2 ls2 sh2 E C M ?pc1 ics v2 xa (v1#vs) frs
                     (I - pcs(compxE2 e1 pc (size vs)))" by fact
  have "P ⊢ (None,h0,frs',sh0) -jvm→ (None,h1,(v1#vs,ls1,C,M,?pc1,ics)#frs,sh1)"
    using IH1 Jcc_pieces_BinOp1[OF pcs, of h1 ls1 sh1 v1] by simp
  also have "P ⊢ … -jvm→ (None,h2,(v2#v1#vs,ls2,C,M,?pc2,ics)#frs,sh2)"
    using IH2 Jcc_pieces_BinOp2[OF assms(1) pcs, of h1 v1 ls1 sh1 v2] by (simp add: add.assoc)
  also have "P ⊢ … -jvm→ (None,h2,(w#vs,ls2,C,M,?pc2+1,ics)#frs,sh2)"
    using BinOp1 by(cases bop) auto
  finally show ?case using pcs by (auto split: bop.splits simp:add.assoc)
next
  case (BinOpThrow11 e1 h0 ls0 sh0 e h1 ls1 sh1 bop e2)
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (e1 «bop» e2)
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (e1 «bop» e2)),ics)#frs,sh1), err)"
    using BinOpThrow11.prems(1) by clarsimp
  have IH1: "PROP ?P e1 h0 ls0 sh0 (throw e) h1 ls1 sh1 E C M pc ics v xa vs frs
                     (I - pcs (compxE2 e2 (pc + length (compE2 e1)) (Suc (length vs))))" by fact
  show ?case using IH1 Jcc_pieces_BinOp1[OF pcs, of h1 ls1 sh1 v] BinOpThrow11.prems nsub_RI_Jcc_pieces
    by auto
next
  case (BinOpThrow21 e1 h0 ls0 sh0 v1 h1 ls1 sh1 e2 e h2 ls2 sh2 bop)
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e1 «bop» e2)
    = (True, frs', (None,h2,(v#vs,ls2,C,M,pc+size(compE2 (e1 «bop» e2)),ics)#frs,sh2), err)"
    using BinOpThrow21.prems(1) by clarsimp
  let ?pc = "pc + length(compE2 e1)"
  have IH1: "PROP ?P e1 h0 ls0 sh0 (Val v1) h1 ls1 sh1 E C M pc ics v1 xa vs frs
                     (I - pcs (compxE2 e2 (pc + length (compE2 e1)) (Suc (length vs))))" by fact
  have IH2: "PROP ?P e2 h1 ls1 sh1 (throw e) h2 ls2 sh2 E C M ?pc ics v xa (v1#vs) frs
                     (I - pcs(compxE2 e1 pc (size vs)))" by fact
  let ?σ1 = "(None,h1,(v1#vs,ls1,C,M,?pc,ics)#frs,sh1)"
  have 1: "P ⊢ (None,h0,frs',sh0) -jvm→ ?σ1"
    using IH1 Jcc_pieces_BinOp1[OF pcs, of h1 ls1 sh1 v1] by simp
  have "(throw e = Val v ⟶  P ⊢ (None, h0, Jcc_frames P C M vs ls0 pc ics frs (e1 «bop» e2), sh0) -jvm→
     Jcc_rhs P1 E C M vs ls0 pc ics frs h2 ls2 sh2 v (e1 «bop» e2))
   ∧ (throw e = Throw xa ⟶ (∃pc1. pc ≤ pc1 ∧ pc1 < pc + size(compE2 (e1 «bop» e2)) ∧
               ¬ caught P pc1 h2 xa (compxE2 (e1 «bop» e2) pc (size vs)) ∧
               (∃vs'. P ⊢ (None,h0,frs',sh0) -jvm→ handle P C M xa h2 (vs'@vs) ls2 pc1 ics frs sh2)))"
   (is "?N ∧ (?eq ⟶ (∃pc2. ?H pc2))")
  proof
    show ?N by simp
  next
    { assume ?eq
      then obtain pc2 vs' where
        pc2: "?pc ≤ pc2 ∧ pc2 < ?pc + size(compE2 e2) ∧
              ¬ caught P pc2 h2 xa (compxE2 e2 ?pc (size vs + 1))" and
        2: "P ⊢ ?σ1 -jvm→ handle P C M xa h2 (vs'@v1#vs) ls2 pc2 ics frs sh2"
        using IH2 Jcc_pieces_BinOp2[OF assms(1) pcs, of h1 v1 ls1 sh1 v] BinOpThrow21.prems by clarsimp
      then have "?H pc2" using jvm_trans[OF 1 2] by(auto intro!: exI[where x="vs'@[v1]"])
      hence "∃pc2. ?H pc2" by iprover
    }
    thus "?eq ⟶ (∃pc2. ?H pc2)" by iprover
  qed
  then show ?case using pcs by simp blast
next
  case (FAcc1 e h0 ls0 sh0 a h1 ls1 sh1 C' fs F T D w)
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (e∙F{D})
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (e∙F{D})),ics)#frs,sh1), err)"
    using FAcc1.prems(1) by clarsimp
  have "P1 ⊢ D sees F,NonStatic:T in D" by(rule has_field_sees[OF has_field_idemp[OF FAcc1.hyps(4)]])
  then have field: "field P D F = (D,NonStatic,T)" by simp
  have IH: "PROP ?P e h0 ls0 sh0 (addr a) h1 ls1 sh1 E C M pc ics (Addr a) xa vs frs I" by fact
  let ?pc = "pc + length(compE2 e)"
  have "P ⊢ (None,h0,frs',sh0) -jvm→ (None,h1,(Addr a#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using IH Jcc_pieces_FAcc[OF pcs, of "Addr a"] pcs by simp
  also have "P ⊢ … -jvm→ (None,h1,(w#vs,ls1,C,M,?pc+1,ics)#frs,sh1)"
    using FAcc1 field by auto
  finally have "P ⊢ (None, h0, frs', sh0) -jvm→ (None,h1,(w#vs,ls1,C,M,?pc+1,ics)#frs,sh1)"
    by auto
  then show ?case using pcs by auto
next
  case (FAccNull1 e h0 ls0 sh0 h1 ls1 sh1 F D)
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (e∙F{D})
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (e∙F{D})),ics)#frs,sh1), err)"
    using FAccNull1.prems(1) by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 null h1 ls1 sh1 E C M pc ics Null xa vs frs I" by fact
  let ?pc = "pc + length(compE2 e)"
  let ?xa = "addr_of_sys_xcpt NullPointer"
  have "P ⊢ (None,h0,frs',sh0) -jvm→ (None,h1,(Null#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using IH Jcc_pieces_FAcc[OF pcs, of Null] by simp
  also have "P ⊢ … -jvm→ handle P C M ?xa h1 (Null#vs) ls1 ?pc ics frs sh1"
    using FAccNull1.prems
    by(fastforce simp:split_beta handle_def simp del: split_paired_Ex)
  finally show ?case using pcs by (auto intro!: exI[where x = ?pc] exI[where x="[Null]"])
next
  case (FAccThrow1 e h0 ls0 sh0 e' h1 ls1 sh1 F D)
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (e∙F{D})
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (e∙F{D})),ics)#frs,sh1), err)"
    using FAccThrow1.prems(1) by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 (throw e') h1 ls1 sh1 E C M pc ics v xa vs frs I" by fact
  show ?case using IH Jcc_pieces_FAcc[OF pcs, of v] FAccThrow1.prems nsub_RI_Jcc_pieces
    less_Suc_eq by auto
next
  case (FAccNone1 e h0 ls0 sh0 a h1 ls1 sh1 C fs F D)
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (e∙F{D})
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (e∙F{D})),ics)#frs,sh1), err)"
    using FAccNone1.prems(1) by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 (addr a) h1 ls1 sh1 E C M pc ics (Addr a) xa vs frs I" by fact
  let ?pc = "pc + length(compE2 e)"
  let ?xa = "addr_of_sys_xcpt NoSuchFieldError"
  have "P ⊢ (None,h0,frs',sh0) -jvm→ (None,h1,(Addr a#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using IH Jcc_pieces_FAcc[OF pcs, of "Addr a"] by simp
  also have "P ⊢ … -jvm→ handle P C M ?xa h1 (Addr a#vs) ls1 ?pc ics frs sh1"
    using FAccNone1
    by(cases ics; clarsimp simp:split_beta handle_def simp del: split_paired_Ex)
  finally show ?case using pcs by (auto intro!: exI[where x = ?pc] exI[where x="[Addr a]"])
next
  case (FAccStatic1 e h0 ls0 sh0 a h1 ls1 sh1 C' fs F T D)
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (e∙F{D})
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (e∙F{D})),ics)#frs,sh1), err)"
    using FAccStatic1.prems(1) by clarsimp
  have "P1 ⊢ D sees F,Static:T in D" by(rule has_field_sees[OF has_field_idemp[OF FAccStatic1.hyps(4)]])
  then have field: "field P D F = (D,Static,T)" by simp
  have IH: "PROP ?P e h0 ls0 sh0 (addr a) h1 ls1 sh1 E C M pc ics (Addr a) xa vs frs I" by fact
  let ?pc = "pc + length(compE2 e)"
  let ?xa = "addr_of_sys_xcpt IncompatibleClassChangeError"
  have "P ⊢ (None,h0,frs',sh0) -jvm→ (None,h1,(Addr a#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using IH Jcc_pieces_FAcc[OF pcs, of "Addr a"] by simp
  also have "P ⊢ … -jvm→ handle P C M ?xa h1 (Addr a#vs) ls1 ?pc ics frs sh1"
    using FAccStatic1 field by(fastforce simp:split_beta handle_def simp del: split_paired_Ex)
  finally show ?case using pcs by (auto intro!: exI[where x = ?pc] exI[where x="[Addr a]"])
next
  case (SFAcc1 C' F t D sh sfs v' h ls)
  have has: "P1 ⊢ D has F,Static:t in D" by(rule has_field_idemp[OF SFAcc1.hyps(1)])
  have "P1 ⊢ D sees F,Static:t in D" by(rule has_field_sees[OF has])
  then have field: "field P D F = (D,Static,t)" by simp
  then have "P ⊢ (None,h,Jcc_frames P C M vs ls pc ics frs (C'∙sF{D}),sh) -jvm→
             (None,h,(v'#vs,ls,C,M,Suc pc,ics)#frs,sh)"
    using SFAcc1 has by(cases ics) auto
  then show ?case by clarsimp
next
  case (SFAccInit1 C' F t D sh h ls v' h' ls' sh' sfs i v'')
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh' v xa (C'∙sF{D})
    = (True, frs', (None,h',(v#vs,ls',C,M,pc+size(compE2 (C'∙sF{D})),ics)#frs,sh'), err)"
    using SFAccInit1.prems(1) by clarsimp
  have "Ex (WTrt21 P1 E h sh (INIT D ([D],False) ← unit))"
    using has_field_is_class'[OF SFAccInit1.hyps(1)] by auto
  then obtain err' where pcs':
    "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh' v' xa (INIT D ([D],False) ← unit)
    = (True, (vs,ls,C,M,pc,Calling D []) # frs, (None,h',(vs,ls,C,M,pc,Called [])#frs,sh'), err')"
    using SFAccInit1.prems(1) by auto
  have IH: "PROP ?P (INIT D ([D],False) ← unit) h ls sh (Val v')
             h' ls' sh' E C M pc ics v' xa vs frs I" by fact
  have ls: "ls = ls'" by(rule init1_same_loc[OF SFAccInit1.hyps(3)])
  have has: "P1 ⊢ D has F,Static:t in D" by(rule has_field_idemp[OF SFAccInit1.hyps(1)])
  have "P1 ⊢ D sees F,Static:t in D" by(rule has_field_sees[OF has])
  then have field: "field P D F = (D,Static,t)" by simp
  have "P ⊢ (None,h,(vs,ls,C,M,pc,ics)#frs,sh) -jvm→ (None,h,(vs,ls,C,M,pc,Calling D [])#frs,sh)"
  proof(cases "sh D")
    case None then show ?thesis using SFAccInit1.hyps(1,2,5,6) SFAccInit1.prems field
      by(cases ics) auto
  next
    case (Some a)
    then obtain sfs i where "a = (sfs,i)" by(cases a)
    then show ?thesis using SFAccInit1.hyps(1,2,5,6) SFAccInit1.prems field Some
      by(cases ics; case_tac i) auto
  qed
  also have "P ⊢ ... -jvm→ (None, h', (vs, ls, C, M, pc, Called []) # frs, sh')"
    using IH pcs' by auto
  also have "P ⊢ ... -jvm→ (None, h', (v''#vs, ls, C, M, Suc pc, ics) # frs, sh')"
    using SFAccInit1.hyps(1,2,5,6) SFAccInit1.prems has field by(cases ics) auto
  finally show ?case using pcs ls by clarsimp
next
  case (SFAccInitThrow1 C' F t D sh h ls a h' ls' sh')
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh' v xa (C'∙sF{D})
    = (True, frs', (None,h',(v#vs,ls',C,M,pc+size(compE2 (C'∙sF{D})),ics)#frs,sh'), err)"
    using SFAccInitThrow1.prems(1) by clarsimp
  obtain a' where throw: "throw a = Throw a'" using eval1_final[OF SFAccInitThrow1.hyps(3)] by clarsimp
  have "Ex (WTrt21 P1 E h sh (INIT D ([D],False) ← unit))"
    using has_field_is_class'[OF SFAccInitThrow1.hyps(1)] by auto
  then obtain vs' where pcs':
    "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh' v a' (INIT D ([D],False) ← unit)
    = (True, (vs,ls,C,M,pc,Calling D []) # frs, (None,h',(vs,ls,C,M,pc,Called [])#frs,sh'),
        P ⊢ (None,h,(vs,ls,C,M,pc,Calling D []) # frs,sh)
               -jvm→ handle P C M a' h' (vs'@vs) ls pc ics frs sh')"
    using SFAccInitThrow1.prems(1) by simp blast
  have IH: "PROP ?P (INIT D ([D],False) ← unit) h ls sh (throw a)
             h' ls' sh' E C M pc ics v a' vs frs I" by fact
  have ls: "ls = ls'" by(rule init1_same_loc[OF SFAccInitThrow1.hyps(3)])
  have has: "P1 ⊢ D has F,Static:t in D" by(rule has_field_idemp[OF SFAccInitThrow1.hyps(1)])
  have "P1 ⊢ D sees F,Static:t in D" by(rule has_field_sees[OF has])
  then have field: "field P D F = (D,Static,t)" by simp
  then have "P ⊢ (None,h,(vs,ls,C,M,pc,ics)#frs,sh) -jvm→ (None,h,(vs,ls,C,M,pc,Calling D []) # frs,sh)"
  proof(cases "sh D")
    case None then show ?thesis using SFAccInitThrow1.hyps(1,2) SFAccInitThrow1.prems field
      by(cases ics) auto
  next
    case (Some a)
    then obtain sfs i where "a = (sfs,i)" by(cases a)
    then show ?thesis using SFAccInitThrow1.hyps(1,2) SFAccInitThrow1.prems field Some
      by(cases ics; case_tac i) auto
  qed
  also have "P ⊢ … -jvm→ handle P C M a' h' (vs'@vs) ls pc ics frs sh'"
    using IH pcs' throw by auto
  finally show ?case using throw ls by auto
next
  case (SFAccNone1 C' F D h1 ls1 sh1)
  then obtain frs' err where pcs:
   "Jcc_pieces P1 E C M h1 vs ls1 pc ics frs sh1 I h1 ls1 sh1 v xa (C'∙sF{D})
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (C'∙sF{D})),ics)#frs,sh1), err)"
    by clarsimp
  let ?xa = "addr_of_sys_xcpt NoSuchFieldError"
  have "P ⊢ (None,h1,frs',sh1) -jvm→ handle P C M ?xa h1 vs ls1 pc ics frs sh1"
    using SFAccNone1 pcs
    by(cases ics; clarsimp simp:split_beta handle_def simp del: split_paired_Ex)
  then show ?case using pcs by(auto intro!: exI[where x = pc] exI[where x="[]"])
next
  case (SFAccNonStatic1 C' F t D h1 ls1 sh1)
  let ?frs' = "(vs, ls1, C, M, pc, ics) # frs"
  let ?xa = "addr_of_sys_xcpt IncompatibleClassChangeError"
  have "P1 ⊢ D sees F,NonStatic:t in D"
    by(rule has_field_sees[OF has_field_idemp[OF SFAccNonStatic1.hyps(1)]])
  then have field: "field P D F = (D,NonStatic,t)" by simp
  have "P ⊢ (None,h1,?frs',sh1) -jvm→ handle P C M ?xa h1 vs ls1 pc ics frs sh1"
    using SFAccNonStatic1
    proof(cases ics)
      case No_ics
      then show ?thesis using SFAccNonStatic1 field
       by (auto simp:split_beta handle_def simp del: split_paired_Ex)
    qed(simp_all)
  then show ?case by (auto intro!: exI[where x = pc] exI[where x="[]"])
next
  case (LAss1 e h0 ls0 sh0 w h1 ls1 sh1 i ls2)
  let ?pc = "pc + length(compE2 e)"
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (i:=e)
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (i:=e)),ics)#frs,sh1), err)"
    using LAss1.prems(1) by auto
  have IH: "PROP ?P e h0 ls0 sh0 (Val w) h1 ls1 sh1 E C M pc ics w xa vs frs I" by fact
  then have "P ⊢ (None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0) -jvm→
             (None,h1,(w#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using Jcc_pieces_LAss[OF assms(1) pcs, of w] LAss1.prems pcs by auto
  also have "P ⊢ … -jvm→ (None,h1,(Unit#vs,ls2,C,M,?pc+2,ics)#frs,sh1)"
    using LAss1 by (auto simp add:cast_ok_def)
  finally show ?case by auto
next
  case (LAssThrow1 e h0 ls0 sh0 w h1 ls1 sh1 i)
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (i:=e)
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (i:=e)),ics)#frs,sh1), err)"
    using LAssThrow1.prems(1) by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 (throw w) h1 ls1 sh1 E C M pc ics v xa vs frs I" by fact
  show ?case using IH Jcc_pieces_LAss[OF assms(1) pcs, of v] LAssThrow1.prems pcs less_SucI
    by(simp, blast)
next
  case (FAss1 e1 h0 ls0 sh0 a h1 ls1 sh1 e2 w h2 ls2 sh2 C' fs F T D fs' h2')
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e1∙F{D} := e2)
    = (True, frs', (None,h2,(v#vs,ls2,C,M,pc+size(compE2 (e1∙F{D} := e2)),ics)#frs,sh2), err)"
    using FAss1.prems(1) by clarsimp
  have "P1 ⊢ D sees F,NonStatic:T in D" by(rule has_field_sees[OF has_field_idemp[OF FAss1.hyps(6)]])
  then have field: "field P D F = (D,NonStatic,T)" by simp
  let ?pc1 = "pc + length(compE2 e1)"
  let ?pc2 = "?pc1 + length(compE2 e2)"
  have IH1: "PROP ?P e1 h0 ls0 sh0 (addr a) h1 ls1 sh1 E C M pc ics (Addr a) xa vs frs
                     (I - pcs (compxE2 e2 (pc + length (compE2 e1)) (Suc (length vs))))" by fact
  have IH2: "PROP ?P e2 h1 ls1 sh1 (Val w) h2 ls2 sh2 E C M ?pc1 ics w xa (Addr a#vs) frs
                     (I - pcs(compxE2 e1 pc (size vs)))" by fact
  have "P ⊢ (None,h0,frs',sh0) -jvm→ (None,h1,(Addr a#vs,ls1,C,M,?pc1,ics)#frs,sh1)"
    using IH1 Jcc_pieces_FAss1[OF pcs, of h1 ls1 sh1 "Addr a"] by simp
  also have "P ⊢ … -jvm→ (None,h2,(w#Addr a#vs,ls2,C,M,?pc2,ics)#frs,sh2)"
    using IH2 Jcc_pieces_FAss2[OF pcs, of h1 "Addr a" ls1 sh1 w] by (simp add: add.assoc)
  also have "P ⊢ … -jvm→ (None,h2',(Unit#vs,ls2,C,M,?pc2+2,ics)#frs,sh2)"
    using FAss1 field by auto
  finally show ?case using pcs by (auto simp:add.assoc)
next
  case (FAssNull1 e1 h0 ls0 sh0 h1 ls1 sh1 e2 w h2 ls2 sh2 F D)
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e1∙F{D} := e2)
    = (True, frs', (None,h2,(v#vs,ls2,C,M,pc+size(compE2 (e1∙F{D} := e2)),ics)#frs,sh2), err)"
    using FAssNull1.prems(1) by clarsimp
  let ?pc1 = "pc + length(compE2 e1)"
  let ?pc2 = "?pc1 + length(compE2 e2)"
  let ?xa = "addr_of_sys_xcpt NullPointer"
  have IH1: "PROP ?P e1 h0 ls0 sh0 null h1 ls1 sh1 E C M pc ics Null xa vs frs
                     (I - pcs (compxE2 e2 (pc + length (compE2 e1)) (Suc (length vs))))" by fact
  have IH2: "PROP ?P e2 h1 ls1 sh1 (Val w) h2 ls2 sh2 E C M ?pc1 ics w xa (Null#vs) frs
                     (I - pcs(compxE2 e1 pc (size vs)))" by fact
  have "P ⊢ (None,h0,frs',sh0) -jvm→ (None,h1,(Null#vs,ls1,C,M,?pc1,ics)#frs,sh1)"
    using IH1 Jcc_pieces_FAss1[OF pcs, of h1 ls1 sh1 Null] by simp
  also have "P ⊢ … -jvm→ (None,h2,(w#Null#vs,ls2,C,M,?pc2,ics)#frs,sh2)"
    using IH2 Jcc_pieces_FAss2[OF pcs, of h1 Null ls1 sh1 w] by (simp add: add.assoc)
  also have "P ⊢ … -jvm→ handle P C M ?xa h2 (w#Null#vs) ls2 ?pc2 ics frs sh2"
    using FAssNull1 by(fastforce simp:split_beta handle_def simp del: split_paired_Ex)
  finally show ?case using pcs by (auto intro!: exI[where x = ?pc2] exI[where x="w#[Null]"])
next
  case (FAssThrow21 e1 h0 ls0 sh0 w h1 ls1 sh1 e2 e' h2 ls2 sh2 F D)
  let ?frs' = "(vs, ls0, C, M, pc, ics) # frs"
  obtain err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e1∙F{D} := e2)
    = (True, ?frs', (None,h2,(v#vs,ls2,C,M,pc+size(compE2 (e1∙F{D} := e2)),ics)#frs,sh2), err)"
    using FAssThrow21.prems(1) by clarsimp
  let ?pc1 = "pc + length(compE2 e1)"
  let ?σ1 = "(None,h1,(w#vs,ls1,C,M,?pc1,ics)#frs,sh1)"
  have IH1: "PROP ?P e1 h0 ls0 sh0 (Val w) h1 ls1 sh1 E C M pc ics w xa vs frs
                     (I - pcs (compxE2 e2 (pc + length (compE2 e1)) (Suc (length vs))))" by fact
  have IH2: "PROP ?P e2 h1 ls1 sh1 (throw e') h2 ls2 sh2 E C M ?pc1 ics v xa (w#vs) frs
                     (I - pcs(compxE2 e1 pc (size vs)))" by fact
  have 1: "P ⊢ (None,h0,?frs',sh0) -jvm→ ?σ1"
    using IH1 Jcc_pieces_FAss1[OF pcs, of h1 ls1 sh1 w] by simp
  show ?case (is "?N ∧ (?eq ⟶ ?err)")
  proof
    show ?N by simp
  next
    { assume ?eq
      moreover
      have "PROP ?P e2 h1 ls1 sh1 (throw e') h2 ls2 sh2 E C M ?pc1 ics v xa (w#vs) frs
                    (I - pcs (compxE2 e1 pc (length vs)))" by fact
      ultimately obtain pc2 vs' where
        pc2: "?pc1 ≤ pc2 ∧ pc2 < ?pc1 + size(compE2 e2) ∧
              ¬ caught P pc2 h2 xa (compxE2 e2 ?pc1 (size vs + 1))" and
        2: "P ⊢ ?σ1 -jvm→ handle P C M xa h2 (vs'@w#vs) ls2 pc2 ics frs sh2"
        using FAssThrow21.prems Jcc_pieces_FAss2[OF pcs, of h1 w ls1 sh1] by auto
      have ?err using Jcc_pieces_FAss2[OF pcs, of h1 w ls1 sh1] pc2 jvm_trans[OF 1 2]
        by(auto intro!: exI[where x=pc2] exI[where x="vs'@[w]"])
    }
    thus "?eq ⟶ ?err" by simp
  qed
next
  case (FAssThrow11 e1 h0 ls0 sh0 e' h1 ls1 sh1 F D e2)
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (e1∙F{D} := e2)
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (e1∙F{D} := e2)),ics)#frs,sh1), err)"
    using FAssThrow11.prems(1) by clarsimp
  have IH1: "PROP ?P e1 h0 ls0 sh0 (throw e') h1 ls1 sh1 E C M pc ics v xa vs frs
                     (I - pcs (compxE2 e2 (pc + length (compE2 e1)) (Suc (length vs))))" by fact
  show ?case using IH1 Jcc_pieces_FAss1[OF pcs, of h1 ls1 sh1 v] FAssThrow11.prems nsub_RI_Jcc_pieces
    by auto
next
  case (FAssNone1 e1 h0 ls0 sh0 a h1 ls1 sh1 e2 w h2 ls2 sh2 C' fs F D)
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e1∙F{D} := e2)
    = (True, frs', (None,h2,(v#vs,ls2,C,M,pc+size(compE2 (e1∙F{D} := e2)),ics)#frs,sh2), err)"
    using FAssNone1.prems(1) by clarsimp
  let ?pc1 = "pc + length(compE2 e1)"
  let ?pc2 = "?pc1 + length(compE2 e2)"
  let ?xa = "addr_of_sys_xcpt NoSuchFieldError"
  have IH1: "PROP ?P e1 h0 ls0 sh0 (addr a) h1 ls1 sh1 E C M pc ics (Addr a) xa vs frs
                     (I - pcs (compxE2 e2 (pc + length (compE2 e1)) (Suc (length vs))))" by fact
  have IH2: "PROP ?P e2 h1 ls1 sh1 (Val w) h2 ls2 sh2 E C M ?pc1 ics w xa (Addr a#vs) frs
                     (I - pcs(compxE2 e1 pc (size vs)))" by fact
  have "P ⊢ (None,h0,frs',sh0) -jvm→ (None,h1,(Addr a#vs,ls1,C,M,?pc1,ics)#frs,sh1)"
    using IH1 Jcc_pieces_FAss1[OF pcs, of h1 ls1 sh1 "Addr a"] by simp
  also have "P ⊢ … -jvm→ (None,h2,(w#Addr a#vs,ls2,C,M,?pc2,ics)#frs,sh2)"
    using IH2 Jcc_pieces_FAss2[OF pcs, of h1 "Addr a" ls1 sh1 w] by (simp add: add.assoc)
  also have "P ⊢ … -jvm→ handle P C M ?xa h2 (w#Addr a#vs) ls2 ?pc2 ics frs sh2"
    using FAssNone1 by(fastforce simp:split_beta handle_def simp del: split_paired_Ex)
  finally show ?case using pcs by (auto intro!: exI[where x = ?pc2] exI[where x="w#[Addr a]"])
next
  case (FAssStatic1 e1 h0 ls0 sh0 a h1 ls1 sh1 e2 w h2 ls2 sh2 C' fs F T D)
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e1∙F{D} := e2)
    = (True, frs', (None,h2,(v#vs,ls2,C,M,pc+size(compE2 (e1∙F{D} := e2)),ics)#frs,sh2), err)"
    using FAssStatic1.prems(1) by clarsimp
  have "P1 ⊢ D sees F,Static:T in D" by(rule has_field_sees[OF has_field_idemp[OF FAssStatic1.hyps(6)]])
  then have field: "field P D F = (D,Static,T)" by simp
  let ?pc1 = "pc + length(compE2 e1)"
  let ?pc2 = "?pc1 + length(compE2 e2)"
  let ?xa = "addr_of_sys_xcpt IncompatibleClassChangeError"
  have IH1: "PROP ?P e1 h0 ls0 sh0 (addr a) h1 ls1 sh1 E C M pc ics (Addr a) xa vs frs
                     (I - pcs (compxE2 e2 (pc + length (compE2 e1)) (Suc (length vs))))" by fact
  have IH2: "PROP ?P e2 h1 ls1 sh1 (Val w) h2 ls2 sh2 E C M ?pc1 ics w xa (Addr a#vs) frs
                     (I - pcs(compxE2 e1 pc (size vs)))" by fact
  have "P ⊢ (None,h0,frs',sh0) -jvm→ (None,h1,(Addr a#vs,ls1,C,M,?pc1,ics)#frs,sh1)"
    using IH1 Jcc_pieces_FAss1[OF pcs, of h1 ls1 sh1 "Addr a"] by simp
  also have "P ⊢ … -jvm→ (None,h2,(w#Addr a#vs,ls2,C,M,?pc2,ics)#frs,sh2)"
    using IH2 Jcc_pieces_FAss2[OF pcs, of h1 "Addr a" ls1 sh1 w] by (simp add: add.assoc)
  also have "P ⊢ … -jvm→ handle P C M ?xa h2 (w#Addr a#vs) ls2 ?pc2 ics frs sh2"
    using FAssStatic1 field by(fastforce simp:split_beta handle_def simp del: split_paired_Ex)
  finally show ?case using pcs by (auto intro!: exI[where x = ?pc2] exI[where x="w#[Addr a]"])
next
  case (SFAss1 e2 h0 ls0 sh0 w h1 ls1 sh1 C' F T D sfs sfs' sh1')
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (C'∙sF{D} := e2)
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (C'∙sF{D} := e2)),ics)#frs,sh1), err)"
    using SFAss1.prems(1) by clarsimp
  have "P1 ⊢ D sees F,Static:T in D" by(rule has_field_sees[OF has_field_idemp[OF SFAss1.hyps(3)]])
  then have field: "field P D F = (D,Static,T)" by simp
  have IH: "PROP ?P e2 h0 ls0 sh0 (Val w) h1 ls1 sh1 E C M pc ics w xa vs frs I" by fact
  let ?pc = "pc + length(compE2 e2)"
  have "P ⊢ (None,h0,frs',sh0) -jvm→ (None,h1,(w#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using IH Jcc_pieces_SFAss[OF pcs, where v'=w] pcs by simp
  also have "P ⊢ … -jvm→ (None,h1,(vs,ls1,C,M,?pc+1,ics)#frs,sh1')"
    using SFAss1.hyps(3-6) SFAss1.prems(1) field by auto
  also have "P ⊢ ... -jvm→ (None,h1,(Unit#vs,ls1,C,M,?pc+2,ics)#frs,sh1')"
    using SFAss1 by auto
  finally show ?case using pcs by auto
next
  case (SFAssInit1 e2 h ls sh w h1 ls1 sh1 C' F t D v' h' ls' sh' sfs i sfs' sh'')
  let ?pc = "pc + length(compE2 e2)"
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh'' v xa (C'∙sF{D}:=e2)
    = (True, frs', (None,h',(v#vs,ls',C,M,pc+size(compE2 (C'∙sF{D}:=e2)),ics)#frs,sh''), err)"
    using SFAssInit1.prems(1) by clarsimp
  have "Ex (WTrt21 P1 E h1 sh1 (INIT D ([D],False) ← unit))"
    using has_field_is_class'[OF SFAssInit1.hyps(3)] by auto
  then obtain err' where pcs':
    "Jcc_pieces P1 E C M h1 (w#vs) ls1 ?pc ics frs sh1 I h' ls' sh' v' xa (INIT D ([D],False) ← unit)
    = (True, (w#vs,ls1,C,M,?pc,Calling D []) # frs,
       (None,h',(w#vs,ls1,C,M,?pc,Called [])#frs,sh'), err')"
    using SFAssInit1.prems(1) by simp
  have ls: "ls1 = ls'" by(rule init1_same_loc[OF SFAssInit1.hyps(5)])
  have has: "P1 ⊢ D has F,Static:t in D" by(rule has_field_idemp[OF SFAssInit1.hyps(3)])
  have "P1 ⊢ D sees F,Static:t in D" by(rule has_field_sees[OF has])
  then have field: "field P D F = (D,Static,t)" by simp
  have IH: "PROP ?P e2 h ls sh (Val w) h1 ls1 sh1 E C M pc ics w xa vs frs I" by fact
  have IHI: "PROP ?P (INIT D ([D],False) ← unit) h1 ls1 sh1 (Val v')
             h' ls' sh' E C M ?pc ics v' xa (w#vs) frs I" by fact
  have "P ⊢ (None,h,frs',sh) -jvm→ (None,h1,(w#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using IH Jcc_pieces_SFAss[OF pcs, where v'=w] by simp
  also have "P ⊢ … -jvm→ (None,h1,(w#vs,ls1,C,M,?pc,Calling D [])#frs,sh1)"
  proof(cases "sh1 D")
    case None then show ?thesis using None SFAssInit1.hyps(1,3-5,7-9) SFAssInit1.prems field
      by(cases ics, auto)
  next
    case (Some a)
    then obtain sfs i where "a = (sfs,i)" by(cases a)
    then show ?thesis using SFAssInit1.hyps(1,3-5,7-9) SFAssInit1.prems field Some
      by(cases ics; case_tac i) auto
  qed
  also have "P ⊢ ... -jvm→ (None, h', (w#vs, ls1, C, M, ?pc, Called []) # frs, sh')"
    using IHI pcs' by clarsimp
  also have "P ⊢ ... -jvm→ (None, h', (vs, ls1, C, M, ?pc + 1, ics) # frs, sh'')"
    using SFAssInit1.hyps(1,3-5,7-9) SFAssInit1.prems has field by(cases ics) auto
  also have "P ⊢ ... -jvm→ (None, h', (Unit#vs, ls1, C, M, ?pc + 2, ics) # frs, sh'')"
    using SFAssInit1.hyps(1,3-5,7-9) SFAssInit1.prems has field by(cases ics) auto
  finally show ?case using pcs ls by simp blast
next
  case (SFAssInitThrow1 e2 h ls sh w h1 ls1 sh1 C' F t D a h' ls' sh')
  let ?pc = "pc + length(compE2 e2)"
  obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh' v xa (C'∙sF{D}:=e2)
    = (True, frs', (None,h',(v#vs,ls',C,M,pc+size(compE2 (C'∙sF{D}:=e2)),ics)#frs,sh'), err)"
    using SFAssInitThrow1.prems(1) by clarsimp
  obtain a' where throw: "throw a = Throw a'" using eval1_final[OF SFAssInitThrow1.hyps(5)] by clarsimp
  have "Ex (WTrt21 P1 E h1 sh1 (INIT D ([D],False) ← unit))"
    using has_field_is_class'[OF SFAssInitThrow1.hyps(3)] by auto
  then obtain vs' where pcs':
    "Jcc_pieces P1 E C M h1 (w#vs) ls1 ?pc ics frs sh1 I h' ls' sh' v a' (INIT D ([D],False) ← unit)
    = (True, (w#vs,ls1,C,M,?pc,Calling D []) # frs, (None,h',(w#vs,ls1,C,M,?pc,Called [])#frs,sh'),
         P ⊢ (None,h1,(w#vs,ls1,C,M,?pc,Calling D []) # frs,sh1)
               -jvm→ handle P C M a' h' (vs'@w#vs) ls1 ?pc ics frs sh')"
    using SFAssInitThrow1.prems(1) by simp blast
  have ls: "ls1 = ls'" by(rule init1_same_loc[OF SFAssInitThrow1.hyps(5)])
  have has: "P1 ⊢ D has F,Static:t in D" by(rule has_field_idemp[OF SFAssInitThrow1.hyps(3)])
  have "P1 ⊢ D sees F,Static:t in D" by(rule has_field_sees[OF has])
  then have field: "field P D F = (D,Static,t)" by simp
  have IH: "PROP ?P e2 h ls sh (Val w) h1 ls1 sh1 E C M pc ics w xa vs frs I" by fact
  have IHI: "PROP ?P (INIT D ([D],False) ← unit) h1 ls1 sh1 (throw a)
             h' ls' sh' E C M ?pc ics v a' (w#vs) frs I" by fact
  have "P ⊢ (None,h,(vs, ls, C, M, pc, ics) # frs,sh) -jvm→ (None,h1,(w#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using IH Jcc_pieces_SFAss[OF pcs, where v'=w] pcs by simp blast
  also have "P ⊢ … -jvm→ (None,h1,(w#vs,ls1,C,M,?pc,Calling D [])#frs,sh1)"
  proof(cases "sh1 D")
    case None then show ?thesis using SFAssInitThrow1.hyps(1,3,4,5) SFAssInitThrow1.prems field
      by(cases ics) auto
  next
    case (Some a)
    then obtain sfs i where "a = (sfs,i)" by(cases a)
    then show ?thesis using SFAssInitThrow1.hyps(1,3,4,5) SFAssInitThrow1.prems field Some
      by(cases ics; case_tac i) auto
  qed
  also have "P ⊢ ... -jvm→ handle P C M a' h' (vs'@w#vs) ls1 ?pc ics frs sh'"
    using IHI pcs' throw by auto
  finally show ?case using throw ls by(auto intro!: exI[where x = ?pc] exI[where x="vs'@[w]"])
next
  case (SFAssThrow1 e2 h0 ls0 sh0 e' h1 ls1 sh1 C' F D)
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (C'∙sF{D} := e2)
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (C'∙sF{D} := e2)),ics)#frs,sh1), err)"
    using SFAssThrow1.prems(1) by clarsimp
  have IH: "PROP ?P e2 h0 ls0 sh0 (throw e') h1 ls1 sh1 E C M pc ics v xa vs frs I" by fact
  show ?case using IH Jcc_pieces_SFAss[OF pcs, where v'=v] SFAssThrow1.prems nsub_RI_Jcc_pieces
    less_Suc_eq by auto
next
  case (SFAssNone1 e2 h0 ls0 sh0 w h1 ls1 sh1 C' F D)
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (C'∙sF{D} := e2)
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (C'∙sF{D} := e2)),ics)#frs,sh1), err)"
    using SFAssNone1.prems(1) by clarsimp
  have IH: "PROP ?P e2 h0 ls0 sh0 (Val w) h1 ls1 sh1 E C M pc ics w xa vs frs I" by fact
  let ?pc = "pc + length(compE2 e2)"
  let ?xa = "addr_of_sys_xcpt NoSuchFieldError"
  have "P ⊢ (None,h0,frs',sh0) -jvm→ (None,h1,(w#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using IH Jcc_pieces_SFAss[OF pcs, where v'=w] pcs by simp
  also have "P ⊢ … -jvm→ handle P C M ?xa h1 (w#vs) ls1 ?pc ics frs sh1"
    using SFAssNone1 by(cases ics; clarsimp simp add: handle_def)
  finally show ?case using pcs by (auto intro!: exI[where x = ?pc] exI[where x="[w]"])
next
  case (SFAssNonStatic1 e2 h0 ls0 sh0 w h1 ls1 sh1 C' F T D)
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h1 ls1 sh1 v xa (C'∙sF{D} := e2)
    = (True, frs', (None,h1,(v#vs,ls1,C,M,pc+size(compE2 (C'∙sF{D} := e2)),ics)#frs,sh1), err)"
    using SFAssNonStatic1.prems(1) by clarsimp
  have IH: "PROP ?P e2 h0 ls0 sh0 (Val w) h1 ls1 sh1 E C M pc ics w xa vs frs I" by fact
  let ?pc = "pc + length(compE2 e2)"
  let ?xa = "addr_of_sys_xcpt IncompatibleClassChangeError"
  have "P1 ⊢ D sees F,NonStatic:T in D"
    by(rule has_field_sees[OF has_field_idemp[OF SFAssNonStatic1.hyps(3)]])
  then have field: "field P D F = (D,NonStatic,T)" by simp
  have "P ⊢ (None,h0,frs',sh0) -jvm→ (None,h1,(w#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using IH Jcc_pieces_SFAss[OF pcs, where v'=w] pcs by simp
  also have "P ⊢ … -jvm→ handle P C M ?xa h1 (w#vs) ls1 ?pc ics frs sh1"
    using SFAssNonStatic1
    proof(cases ics)
      case No_ics
      then show ?thesis using SFAssNonStatic1 field
       by (auto simp:split_beta handle_def simp del: split_paired_Ex)
    qed(simp_all)
  finally show ?case using pcs by (auto intro!: exI[where x = ?pc] exI[where x="[w]"])
next
  case (Call1 e h0 ls0 sh0 a h1 ls1 sh1 es pvs h2 ls2 sh2 Ca fs M' Ts T body D ls2' f h3 ls3 sh3)
  let ?frs0 = "(vs, ls0, C,M,pc,ics)#frs"
  let ?σ0 = "(None,h0,?frs0,sh0)"
  let ?pc1 = "pc + length(compE2 e)"
  let ?σ1 = "(None,h1,(Addr a#vs, ls1, C,M,?pc1,ics)#frs,sh1)"
  let ?pc2 = "?pc1 + length(compEs2 es)"
  let ?frs2 = "(rev pvs @ Addr a # vs, ls2, C,M,?pc2,ics)#frs"
  let ?σ2 = "(None,h2,?frs2,sh2)"
  let ?frs2' = "([], ls2', D,M',0,No_ics) # ?frs2"
  let ?σ2' = "(None, h2, ?frs2', sh2)"
  have nclinit: "M' ≠ clinit" using wf_sees_clinit1[OF wf] visible_method_exists[OF Call1.hyps(6)]
    sees_method_idemp[OF Call1.hyps(6)] by fastforce
  have "P1 ⊢1 ⟨es,(h1, ls1, sh1)⟩ [⇒] ⟨map Val pvs,(h2, ls2, sh2)⟩" by fact
  hence [simp]: "length es = length pvs" by(auto dest:evals1_preserves_elen)
  have invoke: "P,C,M,?pc2 ▹ Invoke M' (length Ts)"
    using Call1.hyps(7) Call1.prems(1) by clarsimp
  have nsub: "¬ sub_RI body" by(rule sees_wf1_nsub_RI[OF wf Call1.hyps(6)])
  obtain err where pcs:
    "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h3 ls2 sh3 v xa (e∙M'(es)) =
    (True, ?frs0, (None, h3, (v#vs, ls2, C,M,?pc2+1,ics)#frs,sh3), err)"
   using Call1.prems(1) by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 (addr a) h1 ls1 sh1 E C M pc ics (Addr a) xa vs frs
    (I - pcs (compxEs2 es (pc + length (compE2 e)) (Suc (length vs))))" by fact
  have IH_es: "PROP ?Ps es h1 ls1 sh1 (map Val pvs) h2 ls2 sh2 C M ?pc1 ics pvs xa
                    (map Val pvs) (Addr a#vs) frs (I - pcs(compxE2 e pc (size vs)))" by fact
  have "P ⊢ ?σ0 -jvm→ ?σ1" using Jcc_pieces_Call1[OF pcs] IH by clarsimp
  also have "P ⊢ … -jvm→ ?σ2" using IH_es Call1.prems by fastforce
  also have "P ⊢ … -jvm→ ?σ2'"
    using jvm_Invoke[OF assms(1) invoke _ Call1.hyps(6-8)] Call1.hyps(5) Call1.prems(1) by simp
  finally have 1: "P ⊢ ?σ0 -jvm→ ?σ2'".
  have "P1 ⊢ Ca sees M',NonStatic: Ts→T = body in D" by fact
  then have M'_in_D: "P1 ⊢ D sees M',NonStatic: Ts→T = body in D"
    by(rule sees_method_idemp) 
  have M'_code: "compP2 P1,D,M',0 ⊳ compE2 body @ [Return]" using beforeM M'_in_D by simp
  have M'_xtab: "compP2 P1,D,M' ⊳ compxE2 body 0 0/{..<size(compE2 body)},0"
    using M'_in_D by(rule beforexM)
  have IH_body: "PROP ?P body h2 ls2' sh2 f h3 ls3 sh3 (Class D # Ts) D M' 0 No_ics v xa [] ?frs2
    ({..<size(compE2 body)})" by fact
  have cond: "Jcc_cond P1 (Class D # Ts) D M' [] 0 No_ics {..<length (compE2 body)} h2 sh2 body"
    using nsub_RI_Jcc_pieces[OF assms(1) nsub] M'_code M'_xtab by clarsimp
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val ⟶ ?trans")
    proof
      assume val: ?val
      note 1
      also have "P ⊢ ?σ2' -jvm→ (None,h3,([v],ls3,D,M',size(compE2 body),No_ics)#?frs2,sh3)"
        using val IH_body Call1.prems M'_code cond nsub_RI_Jcc_pieces nsub by auto
      also have "P ⊢ … -jvm→ (None, h3, (v#vs, ls2, C,M,?pc2+1,ics)#frs,sh3)"
        using Call1.hyps(7) M'_code M'_in_D nclinit by(cases T, auto)
      finally show ?trans by(simp add:add.assoc)
    qed
  next
    show ?Err (is "?throw ⟶ ?err")
    proof
      assume throw: ?throw
      with IH_body obtain pc2 vs' where
        pc2: "0 ≤ pc2 ∧ pc2 < size(compE2 body) ∧
              ¬ caught P pc2 h3 xa (compxE2 body 0 0)" and
        2: "P ⊢ ?σ2' -jvm→ handle P D M' xa h3 vs' ls3 pc2 No_ics ?frs2 sh3"
        using Call1.prems M'_code M'_xtab cond nsub_RI_Jcc_pieces nsub
         by (auto simp del:split_paired_Ex)
      have "handle P D M' xa h3 vs' ls3 pc2 No_ics ?frs2 sh3 =
            handle P C M xa h3 (rev pvs @ Addr a # vs) ls2 ?pc2 ics frs sh3"
        using pc2 M'_in_D nclinit by(auto simp add:handle_def)
      then show "?err" using pc2 jvm_trans[OF 1 2]
       by(auto intro!:exI[where x="?pc2"] exI[where x="rev pvs@[Addr a]"])
    qed
  qed
next
  case (CallParamsThrow1 e h0 ls0 sh0 w h1 ls1 sh1 es es' h2 ls2 sh2 pvs ex es'' M')
  let ?frs0 = "(vs, ls0, C,M,pc,ics)#frs"
  let ?σ0 = "(None,h0,(vs, ls0, C,M,pc,ics)#frs,sh0)"
  let ?pc1 = "pc + length(compE2 e)"
  let ?σ1 = "(None,h1,(w # vs, ls1, C,M,?pc1,ics)#frs,sh1)"
  let ?pc2 = "?pc1 + length(compEs2 es)"
  obtain err where pcs:
    "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e∙M'(es)) =
    (True, ?frs0, (None, h2, (v#vs, ls2, C,M,?pc2+1,ics)#frs,sh2), err)"
   using CallParamsThrow1.prems(1) by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 (Val w) h1 ls1 sh1 E C M pc ics w xa vs frs
    (I - pcs (compxEs2 es (pc + length (compE2 e)) (Suc (length vs))))" by fact
  have 1: "P ⊢ ?σ0 -jvm→ ?σ1" using Jcc_pieces_Call1[OF pcs] IH by clarsimp
  have Isubs: "{?pc1..<?pc2} ⊆ I - pcs (compxE2 e pc (length vs))"
    using CallParamsThrow1.prems by clarsimp
  show ?case (is "?N ∧ (?eq ⟶ ?err)")
  proof
    show ?N by simp
  next
    { assume ?eq
      moreover
      have "PROP ?Ps es h1 ls1 sh1 es' h2 ls2 sh2 C M ?pc1 ics pvs xa es'' (w#vs) frs
        (I - pcs (compxE2 e pc (length vs)))" by fact
      ultimately obtain vs' where "∃pc2.
        (?pc1 ≤ pc2 ∧ pc2 < ?pc1 + size(compEs2 es) ∧
         ¬ caught P pc2 h2 xa (compxEs2 es ?pc1 (size vs + 1))) ∧
        P ⊢ ?σ1 -jvm→ handle P C M xa h2 (vs'@w#vs) ls2 pc2 ics frs sh2"
        (is "∃pc2. ?PC pc2 ∧ ?Exec pc2")
        using CallParamsThrow1 Isubs by auto
      then obtain pc2 where pc2: "?PC pc2" and 2: "?Exec pc2" by iprover
      then have "?err" using pc2 jvm_trans[OF 1 2]
       by(auto intro!: exI[where x="pc2"] exI[where x="vs'@[w]"])
    }
    thus "?eq ⟶ ?err" by simp
  qed
next
  case (CallNull1 e h0 ls0 sh0 h1 ls1 sh1 es pvs h2 ls2 sh2 M')
  have "P1 ⊢1 ⟨es,(h1, ls1, sh1)⟩ [⇒] ⟨map Val pvs,(h2, ls2, sh2)⟩" by fact
  hence [simp]: "length es = length pvs" by(auto dest:evals1_preserves_elen)
  let ?frs0 = "(vs, ls0, C,M,pc,ics)#frs"
  let ?pc1 = "pc + length(compE2 e)"
  let ?pc2 = "?pc1 + length(compEs2 es)"
  let ?xa = "addr_of_sys_xcpt NullPointer"
  obtain err where pcs:
    "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e∙M'(es)) =
    (True, ?frs0, (None, h2, (v#vs, ls2, C,M,?pc2+1,ics)#frs,sh2), err)"
   using CallNull1.prems(1) by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 null h1 ls1 sh1 E C M pc ics Null xa vs frs
    (I - pcs (compxEs2 es (pc + length (compE2 e)) (Suc (length vs))))" by fact
  have IH_es: "PROP ?Ps es h1 ls1 sh1 (map Val pvs) h2 ls2 sh2 C M ?pc1 ics pvs xa
                    (map Val pvs) (Null#vs) frs (I - pcs(compxE2 e pc (size vs)))" by fact
  have Isubs: "{pc + length (compE2 e)..<pc + length (compE2 e) + length (compEs2 es)}
     ⊆ I - pcs (compxE2 e pc (length vs))" using CallNull1.prems by clarsimp
  have "P ⊢ (None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0) -jvm→
             (None,h1,(Null#vs,ls1,C,M,?pc1,ics)#frs,sh1)"
    using Jcc_pieces_Call1[OF pcs] IH by clarsimp
  also have "P ⊢ … -jvm→ (None,h2,(rev pvs@Null#vs,ls2,C,M,?pc2,ics)#frs,sh2)"
    using CallNull1 IH_es Isubs by auto
  also have "P ⊢ … -jvm→ handle P C M ?xa h2 (rev pvs@Null#vs) ls2 ?pc2 ics frs sh2"
    using CallNull1.prems
    by(auto simp:split_beta handle_def nth_append simp del: split_paired_Ex)
  finally show ?case by (auto intro!: exI[where x = ?pc2] exI[where x="rev pvs@[Null]"])
next
  case (CallObjThrow1 e h ls sh e' h' ls' sh' M' es)
  obtain err where pcs:
    "Jcc_pieces P1 E C M h vs ls pc ics frs sh I h' ls' sh' v xa (e∙M'(es)) =
    (True, (vs, ls, C,M,pc,ics)#frs,
       (None, h', (v#vs, ls', C,M,pc+size(compE2 (e∙M'(es))),ics)#frs,sh'), err)"
   using CallObjThrow1.prems(1) by clarsimp
  obtain a' where throw: "throw e' = Throw a'"
    using eval1_final[OF CallObjThrow1.hyps(1)] by clarsimp
  have IH: "PROP ?P e h ls sh (throw e') h' ls' sh' E C M pc ics v a' vs frs
    (I - pcs (compxEs2 es (pc + length (compE2 e)) (Suc (length vs))))" by fact
  show ?case using IH Jcc_pieces_Call1[OF pcs] throw CallObjThrow1.prems nsub_RI_Jcc_pieces
    by auto
next
  case (CallNone1 e h0 ls0 sh0 a h1 ls1 sh1 es pvs h2 ls2 sh2 C' fs M')
  let ?frs0 = "(vs, ls0, C,M,pc,ics)#frs"
  let ?σ0 = "(None,h0,?frs0,sh0)"
  let ?pc1 = "pc + length(compE2 e)"
  let ?σ1 = "(None,h1,(Addr a#vs, ls1, C,M,?pc1,ics)#frs,sh1)"
  let ?pc2 = "?pc1 + length(compEs2 es)"
  let ?frs2 = "(rev pvs @ Addr a # vs, ls2, C,M,?pc2,ics)#frs"
  let ?σ2 = "(None,h2,?frs2,sh2)"
  let ?xa = "addr_of_sys_xcpt NoSuchMethodError"
  have "P1 ⊢1 ⟨es,(h1, ls1, sh1)⟩ [⇒] ⟨map Val pvs,(h2, ls2, sh2)⟩" by fact
  hence [simp]: "length es = length pvs" by(auto dest:evals1_preserves_elen)
  have aux: "(rev pvs @ Addr a # vs) ! length pvs = Addr a"
    by (metis length_rev nth_append_length)
  have nmeth: "¬(∃b Ts T body D. P ⊢ C' sees M', b :  Ts→T = body in D)"
    using sees_method_compPD CallNone1.hyps(6) by fastforce
  obtain err where pcs:
    "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e∙M'(es)) =
    (True, ?frs0, (None, h2, (v#vs, ls2, C,M,?pc2+1,ics)#frs,sh2), err)"
   using CallNone1.prems(1) by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 (addr a) h1 ls1 sh1 E C M pc ics (Addr a) xa vs frs
    (I - pcs (compxEs2 es (pc + length (compE2 e)) (Suc (length vs))))" by fact
  have IH_es: "PROP ?Ps es h1 ls1 sh1 (map Val pvs) h2 ls2 sh2 C M ?pc1 ics pvs xa
                    (map Val pvs) (Addr a#vs) frs (I - pcs(compxE2 e pc (size vs)))" by fact
  have "P ⊢ ?σ0 -jvm→ ?σ1" using Jcc_pieces_Call1[OF pcs] IH by clarsimp
  also have "P ⊢ … -jvm→ ?σ2" using IH_es CallNone1.prems by fastforce
  also have "P ⊢ … -jvm→ handle P C M ?xa h2 (rev pvs@Addr a#vs) ls2 ?pc2 ics frs sh2"
    using CallNone1.hyps(5) CallNone1.prems aux nmeth
     by(cases "method P C' M'", cases "find_handler P ?xa h2 frs sh2", auto simp: handle_def)
  finally show ?case using pcs by (auto intro!: exI[where x = ?pc2] exI[where x="rev pvs@[Addr a]"])
next
  case (CallStatic1 e h0 ls0 sh0 a h1 ls1 sh1 es pvs h2 ls2 sh2 C' fs M' Ts T body D)
  let ?frs0 = "(vs, ls0, C,M,pc,ics)#frs"
  let ?σ0 = "(None,h0,?frs0,sh0)"
  let ?pc1 = "pc + length(compE2 e)"
  let ?σ1 = "(None,h1,(Addr a#vs, ls1, C,M,?pc1,ics)#frs,sh1)"
  let ?pc2 = "?pc1 + length(compEs2 es)"
  let ?frs2 = "(rev pvs @ Addr a # vs, ls2, C,M,?pc2,ics)#frs"
  let ?σ2 = "(None,h2,?frs2,sh2)"
  let ?xa = "addr_of_sys_xcpt IncompatibleClassChangeError"
  have "P1 ⊢1 ⟨es,(h1, ls1, sh1)⟩ [⇒] ⟨map Val pvs,(h2, ls2, sh2)⟩" by fact
  hence [simp]: "length es = length pvs" by(auto dest:evals1_preserves_elen)
  have aux: "(rev pvs @ Addr a # vs) ! length pvs = Addr a"
    by (metis length_rev nth_append_length)
  obtain body' where method: "P ⊢ C' sees M', Static :  Ts→T = body' in D"
    by (metis CallStatic1.hyps(6) P_def compP2_def sees_method_compP)
  obtain err where pcs:
    "Jcc_pieces P1 E C M h0 vs ls0 pc ics frs sh0 I h2 ls2 sh2 v xa (e∙M'(es)) =
    (True, ?frs0, (None, h2, (v#vs, ls2, C,M,?pc2+1,ics)#frs,sh2), err)"
   using CallStatic1.prems(1) by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 (addr a) h1 ls1 sh1 E C M pc ics (Addr a) xa vs frs
    (I - pcs (compxEs2 es (pc + length (compE2 e)) (Suc (length vs))))" by fact
  have IH_es: "PROP ?Ps es h1 ls1 sh1 (map Val pvs) h2 ls2 sh2 C M ?pc1 ics pvs xa
                    (map Val pvs) (Addr a#vs) frs (I - pcs(compxE2 e pc (size vs)))" by fact
  have "P ⊢ ?σ0 -jvm→ ?σ1" using Jcc_pieces_Call1[OF pcs] IH by clarsimp
  also have "P ⊢ … -jvm→ ?σ2" using IH_es CallStatic1.prems by fastforce
  also have "P ⊢ … -jvm→ handle P C M ?xa h2 (rev pvs@Addr a#vs) ls2 ?pc2 ics frs sh2"
    using CallStatic1.hyps(5) CallStatic1.prems aux method
     by(cases "method P C' M'", cases "find_handler P ?xa h2 frs sh2")
       (auto simp: handle_def; meson frames_of.cases)
  finally show ?case using pcs by (auto intro!: exI[where x = ?pc2] exI[where x="rev pvs@[Addr a]"])
next
  case (SCallParamsThrow1 es h1 ls1 sh1 es' h2 ls2 sh2 pvs ex es'' C' M')
  show ?case
  proof(cases "M' = clinit ∧ es = []")
    case clinit: True then show ?thesis
      using SCallParamsThrow1.hyps(1,3) evals1_cases(1) by fastforce
  next
    case nclinit: False
    let ?σ1 = "(None,h1,(vs, ls1, C,M,pc,ics)#frs,sh1)"
    let ?pc2 = "pc + length(compEs2 es)"
    have Isubs: "{pc..<pc + length (compEs2 es)} ⊆ I" using SCallParamsThrow1.prems nclinit by clarsimp
    show ?thesis (is "?N ∧ (?eq ⟶ ?err)")
    proof
      show ?N by simp
    next
      { assume ?eq
        moreover
        have "PROP ?Ps es h1 ls1 sh1 es' h2 ls2 sh2 C M pc ics pvs xa es'' vs frs I" by fact
        ultimately have "∃pc2.
          (pc ≤ pc2 ∧ pc2 < pc + size(compEs2 es) ∧
           ¬ caught P pc2 h2 xa (compxEs2 es pc (size vs))) ∧
          (∃vs'. P ⊢ ?σ1 -jvm→ handle P C M xa h2 (vs'@vs) ls2 pc2 ics frs sh2)"
          (is "∃pc2. ?PC pc2 ∧ ?Exec pc2")
          using SCallParamsThrow1 Isubs nclinit by auto
        then obtain pc2 where pc2: "?PC pc2" and 2: "?Exec pc2" by iprover
        then have "?err" using pc2 2 by(auto intro: exI[where x="pc2"])
      }
      thus "?eq ⟶ ?err" by iprover
    qed
  qed
next
  case (SCallNone1 es h1 ls1 sh1 pvs h2 ls2 sh2 C' M')
  show ?case
  proof(cases "M' = clinit ∧ es = []")
    case clinit: True then show ?thesis using SCallNone1.hyps(3) SCallNone1.prems by auto
  next
    case nclinit: False
    let ?σ1 = "(None,h1,(vs, ls1, C,M,pc,ics)#frs,sh1)"
    let ?pc2 = "pc + length(compEs2 es)"
    let ?frs2 = "(rev pvs @ vs, ls2, C,M,?pc2,ics)#frs"
    let ?σ2 = "(None,h2,?frs2,sh2)"
    let ?xa = "addr_of_sys_xcpt NoSuchMethodError"
    have "P1 ⊢1 ⟨es,(h1, ls1, sh1)⟩ [⇒] ⟨map Val pvs,(h2, ls2, sh2)⟩" by fact
    hence [simp]: "length es = length pvs" by(auto dest:evals1_preserves_elen)
    have nmeth: "¬(∃b Ts T body D. P ⊢ C' sees M', b :  Ts→T = body in D)"
      using sees_method_compPD SCallNone1.hyps(3) by fastforce
    have IH_es: "PROP ?Ps es h1 ls1 sh1 (map Val pvs) h2 ls2 sh2 C M pc ics pvs xa
                      (map Val pvs) vs frs I" by fact
    have "P ⊢ ?σ1 -jvm→ ?σ2" using IH_es SCallNone1.prems nclinit by auto fastforce+
    also have "P ⊢ … -jvm→ handle P C M ?xa h2 (rev pvs@vs) ls2 ?pc2 ics frs sh2"
      using SCallNone1.prems nmeth nclinit
       by(cases "method P C' M'", cases "find_handler P ?xa h2 frs sh2", auto simp: handle_def)
    finally show ?thesis using nclinit by (auto intro: exI[where x = ?pc2])
  qed
next
  case (SCallNonStatic1 es h1 ls1 sh1 pvs h2 ls2 sh2 C' M' Ts T body D)
  show ?case
  proof(cases "M' = clinit ∧ es = []")
    case clinit: True then show ?thesis
      using SCallNonStatic1.hyps(3) SCallNonStatic1.prems sees_method_fun by fastforce
  next
    case nclinit: False
    let ?σ1 = "(None,h1,(vs, ls1, C,M,pc,ics)#frs,sh1)"
    let ?pc2 = "pc + length(compEs2 es)"
    let ?frs2 = "(rev pvs @ vs, ls2, C,M,?pc2,ics)#frs"
    let ?σ2 = "(None,h2,?frs2,sh2)"
    let ?xa = "addr_of_sys_xcpt IncompatibleClassChangeError"
    have "P1 ⊢1 ⟨es,(h1, ls1, sh1)⟩ [⇒] ⟨map Val pvs,(h2, ls2, sh2)⟩" by fact
    hence [simp]: "length es = length pvs" by(auto dest:evals1_preserves_elen)
    obtain body' where method: "P ⊢ C' sees M', NonStatic :  Ts→T = body' in D"
      by (metis SCallNonStatic1.hyps(3) P_def compP2_def sees_method_compP)
    have IH_es: "PROP ?Ps es h1 ls1 sh1 (map Val pvs) h2 ls2 sh2 C M pc ics pvs xa
                      (map Val pvs) vs frs I" by fact
    have "P ⊢ ?σ1 -jvm→ ?σ2" using IH_es SCallNonStatic1.prems nclinit by auto fastforce+
    also have "P ⊢ … -jvm→ handle P C M ?xa h2 (rev pvs@vs) ls2 ?pc2 ics frs sh2"
      using SCallNonStatic1.prems method nclinit
       by(cases "method P C' M'", cases "find_handler P ?xa h2 frs sh2")
         (auto simp: handle_def; meson frames_of.cases)
    finally show ?thesis using nclinit by (auto intro: exI[where x = ?pc2])
  qed
next
  case (SCallInitThrow1 es h0 ls0 sh0 pvs h1 ls1 sh1 C' M' Ts T body D a h2 ls2 sh2)
  show ?case
  proof(cases "M' = clinit ∧ es = []")
    case clinit: True then show ?thesis using SCallInitThrow1 by simp
  next
    case nclinit: False
    let ?σ0 = "(None,h0,(vs, ls0, C,M,pc,ics)#frs,sh0)"
    let ?pc1 = "pc + length(compEs2 es)"
    let ?frs1 = "(rev pvs @ vs, ls1, C,M,?pc1,ics)#frs"
    let ?σ1 = "(None,h1,?frs1,sh1)"
    let ?frs1' = "(rev pvs@vs,ls1,C,M,?pc1,Calling D [])#frs"
    let ?σ1' = "(None,h1,?frs1',sh1)"
    let ?frs2 = "(rev pvs@vs,ls1,C,M,?pc1,Called [])#frs"
    let ?σ2 = "(None,h2,?frs2,sh2)"
    have ls: "ls1 = ls2" by(rule init1_same_loc[OF SCallInitThrow1.hyps(6)])
    have method: "∃m'. P ⊢ C' sees M',Static:Ts→T = m' in D" using SCallInitThrow1.hyps(3)
      by (metis P_def compP2_def sees_method_compP)
    obtain a' where throw: "throw a = Throw a'" using eval1_final[OF SCallInitThrow1.hyps(6)] by clarsimp
    have "Ex (WTrt21 P1 E h1 sh1 (INIT D ([D],False) ← unit))"
      using sees_method_is_class'[OF SCallInitThrow1.hyps(3)] by auto
    then obtain err' where pcs':
      "Jcc_pieces P1 E C M h1 (rev pvs@vs) ls1 ?pc1 ics frs sh1 I h2 ls2 sh2 v xa (INIT D ([D],False) ← unit)
      = (True, ?frs1', (None,h2,?frs2,sh2), err')"
      using SCallInitThrow1.prems(1) nclinit by auto
    have IHI: "PROP ?P (INIT D ([D],False) ← unit) h1 ls1 sh1 (throw a)
               h2 ls2 sh2 E C M ?pc1 ics v a' (rev pvs@vs) frs I" by fact
    have IH_es: "PROP ?Ps es h0 ls0 sh0 (map Val pvs) h1 ls1 sh1 C M pc ics pvs xa
                      (map Val pvs) vs frs I" by fact
    have "P ⊢ ?σ0 -jvm→ ?σ1" using IH_es SCallInitThrow1.prems nclinit by auto fastforce+
    also have "P ⊢ … -jvm→ ?σ1'"
    proof(cases "sh1 D")
      case None then show ?thesis using SCallInitThrow1.hyps(1,3-6) SCallInitThrow1.prems method
        by(cases ics) auto
    next
      case (Some a)
      then obtain sfs i where "a = (sfs,i)" by(cases a)
      then show ?thesis using SCallInitThrow1.hyps(1,3-6) SCallInitThrow1.prems method Some
        by(cases ics; case_tac i, auto)
    qed
    also obtain vs' where "P ⊢ … -jvm→ handle P C M a' h2 (vs'@rev pvs@vs) ls1 ?pc1 ics frs sh2"
      using IHI pcs' throw by auto
    finally show ?thesis using nclinit throw ls
     by(auto intro!: exI[where x="?pc1"] exI[where x="vs'@rev pvs"])
  qed
next
  case (SCallInit1 es h0 ls0 sh0 pvs h1 ls1 sh1 C' M' Ts T body D v' h2 ls2 sh2 ls2' e' h3 ls3 sh3)
  show ?case
  proof(cases "M' = clinit ∧ es = []")
    case clinit: True then show ?thesis using SCallInit1 by simp
  next
    case nclinit: False
    let ?σ0 = "(None,h0,(vs, ls0, C,M,pc,ics)#frs,sh0)"
    let ?pc1 = "pc + length(compEs2 es)"
    let ?frs1 = "(rev pvs @ vs, ls1, C,M,?pc1,ics)#frs"
    let ?σ1 = "(None,h1,?frs1,sh1)"
    let ?frs1' = "(rev pvs@vs,ls1,C,M,?pc1,Calling D [])#frs"
    let ?σ1' = "(None,h1,?frs1',sh1)"
    let ?frs2 = "(rev pvs@vs,ls1,C,M,?pc1,Called [])#frs"
    let ?σ2 = "(None,h2,?frs2,sh2)"
    let ?frs2' = "([], ls2', D,M',0,No_ics) # ?frs1"
    let ?σ2' = "(None, h2, ?frs2', sh2)"
    have nclinit': "M' ≠ clinit" by fact
    have ics: "ics = No_ics" using SCallInit1.hyps(5) SCallInit1.prems by simp
    have "P1 ⊢1 ⟨es,(h0, ls0, sh0)⟩ [⇒] ⟨map Val pvs,(h1, ls1, sh1)⟩" by fact
    hence [simp]: "length es = length pvs" by(auto dest:evals1_preserves_elen)
    have invoke: "P,C,M,?pc1 ▹ Invokestatic C' M' (length Ts)"
      using SCallInit1.hyps(8) SCallInit1.prems nclinit by(auto simp: add.assoc)
    have nsub: "¬ sub_RI body" by(rule sees_wf1_nsub_RI[OF wf SCallInit1.hyps(3)])
    have ls: "ls1 = ls2" by(rule init1_same_loc[OF SCallInit1.hyps(6)])
    obtain sfs i where sh2: "sh2 D = Some(sfs,i)"
      using init1_Val_PD[OF SCallInit1.hyps(6)] by clarsimp
    have method: "∃m'. P ⊢ C' sees M',Static:Ts→T = m' in D" using SCallInit1.hyps(3)
      by (metis P_def compP2_def sees_method_compP)
    have "Ex (WTrt21 P1 E h1 sh1 (INIT D ([D],False) ← unit))"
      using sees_method_is_class'[OF SCallInit1.hyps(3)] by auto
    then obtain err' where pcs':
      "Jcc_pieces P1 E C M h1 (rev pvs@vs) ls1 ?pc1 ics frs sh1 I h2 ls2 sh2 v' xa (INIT D ([D],False) ← unit)
      = (True, ?frs1', (None,h2,?frs2,sh2), err')"
      using SCallInit1.prems(1) nclinit by auto
    have IHI: "PROP ?P (INIT D ([D],False) ← unit) h1 ls1 sh1 (Val v')
               h2 ls2 sh2 E C M ?pc1 ics v' xa (rev pvs@vs) frs I" by fact
    have IH_es: "PROP ?Ps es h0 ls0 sh0 (map Val pvs) h1 ls1 sh1 C M pc ics pvs xa
                      (map Val pvs) vs frs I" by fact
    have "P ⊢ ?σ0 -jvm→ ?σ1" using IH_es SCallInit1.prems nclinit by auto fastforce+
    also have "P ⊢ … -jvm→ ?σ1'"
    proof(cases "sh1 D")
      case None then show ?thesis using SCallInit1.hyps(1,3-6,8-10) SCallInit1.prems method
        by(cases ics) auto
    next
      case (Some a)
      then obtain sfs i where "a = (sfs,i)" by(cases a)
      then show ?thesis using SCallInit1.hyps(1,3-6,8-10) SCallInit1.prems method Some
        by(cases ics; case_tac i, auto)
    qed
    also have "P ⊢ … -jvm→ ?σ2" using IHI pcs' by auto
    also have "P ⊢ … -jvm→ ?σ2'"
      using jvm_Invokestatic_Called[OF assms(1) invoke _ SCallInit1.hyps(3,8,9)] sh2 ics by auto
    finally have 1: "P ⊢ ?σ0 -jvm→ ?σ2'".
    have "P1 ⊢ C' sees M',Static: Ts→T = body in D" by fact
    then have M'_in_D: "P1 ⊢ D sees M',Static: Ts→T = body in D"
      by(rule sees_method_idemp) 
    have M'_code: "compP2 P1,D,M',0 ⊳ compE2 body @ [Return]" using beforeM M'_in_D by simp
    have M'_xtab: "compP2 P1,D,M' ⊳ compxE2 body 0 0/{..<size(compE2 body)},0"
      using M'_in_D by(rule beforexM)
    have IH_body: "PROP ?P body h2 ls2' sh2 e' h3 ls3 sh3 (Class D # Ts) D M' 0 No_ics v xa [] ?frs1
      ({..<size(compE2 body)})" by fact
    have cond: "Jcc_cond P1 (Class D # Ts) D M' [] 0 No_ics {..<length (compE2 body)} h2 sh2 body"
      using nsub_RI_Jcc_pieces[OF assms(1) nsub] M'_code M'_xtab by clarsimp
    show ?thesis (is "?Norm ∧ ?Err")
    proof
      show ?Norm (is "?val ⟶ ?trans")
      proof
        assume val: ?val
        note 1
        also have "P ⊢ ?σ2' -jvm→ (None,h3,([v],ls3,D,M',size(compE2 body),No_ics)#?frs1,sh3)"
          using val IH_body SCallInit1.prems M'_code cond nsub_RI_Jcc_pieces nsub by auto
        also have "P ⊢ … -jvm→ (None, h3, (v#vs, ls2, C,M,?pc1+1,ics)#frs,sh3)"
          using SCallInit1.hyps(8) M'_code M'_in_D ls nclinit' by(cases T, auto)
        finally show ?trans using nclinit by(auto simp:add.assoc)
      qed
    next
      show ?Err (is "?throw ⟶ ?err")
      proof
        assume throw: ?throw
        with IH_body obtain pc2 vs' where
          pc2: "0 ≤ pc2 ∧ pc2 < size(compE2 body) ∧
                ¬ caught P pc2 h3 xa (compxE2 body 0 0)" and
          2: "P ⊢ ?σ2' -jvm→ handle P D M' xa h3 vs' ls3 pc2 No_ics ?frs1 sh3"
          using SCallInit1.prems M'_code M'_xtab cond nsub_RI_Jcc_pieces nsub
           by (auto simp del:split_paired_Ex)
        have "handle P D M' xa h3 vs' ls3 pc2 No_ics ?frs1 sh3 =
              handle P C M xa h3 (rev pvs @ vs) ls2 ?pc1 ics frs sh3"
          using pc2 M'_in_D ls nclinit' by(auto simp add:handle_def)
        then show "?err" using pc2 jvm_trans[OF 1 2] nclinit
         by(auto intro!:exI[where x="?pc1"] exI[where x="rev pvs"])
      qed
    qed
  qed
next
  case (SCall1 es h1 ls1 sh1 pvs h2 ls2 sh2 C' M' Ts T body D sfs ls2' e' h3 ls3 sh3)
  show ?case
  proof(cases "M' = clinit ∧ es = []")
    case clinit: True
    then have s1: "pvs = []" "h1 = h2" "ls1 = ls2" "sh1 = sh2"
      using SCall1.hyps(1) evals1_cases(1) by blast+
    then have ls2': "ls2' = replicate (max_vars body) undefined" using SCall1.hyps(6) clinit by simp
    let ?frs = "create_init_frame P C' # (vs, ls1, C,M,pc,ics)#frs"
    let ?σ1 = "(None,h1,?frs,sh1)"
    have method: "P1 ⊢ C' sees clinit,Static: []→Void = body in C'"
      using SCall1.hyps(3) clinit s1(1) wf_sees_clinit[OF wf]
        by (metis is_class_def option.collapse sees_method_fun sees_method_is_class)
    then have M_code: "compP2 P1,C',clinit,0 ⊳ compE2 body @ [Return]" by(rule beforeM)
    have pcs: "Jcc_pieces P1 E C M h1 vs ls1 pc ics frs sh1 I h3 ls2 sh3 v xa (C'∙sclinit([]))
         = (True, ?frs, (None, h3, tl ?frs, sh3(C'↦(fst(the(sh3 C')),Done))),
        P ⊢ (None, h1, ?frs, sh1) -jvm→
        (case ics of
     Called Cs ⇒ (None, h3, (vs, ls1, C, M, pc, Throwing Cs xa) # frs, sh3(C' ↦ (fst (the (sh3 C')), Error)))))"
      using Jcc_pieces_clinit[OF assms(1),of E C M vs pc ics I h1 sh1 C' ls1 frs h3 ls2 sh3 v xa]
         SCall1.prems(1) clinit s1(1) by clarsimp
    have IH_body: "PROP ?P body h2 ls2' sh2 e' h3 ls3 sh3 [] C' clinit 0 No_ics v xa [] (tl ?frs)
     ({..<size(compE2 body)})" by fact
    show ?thesis (is "?Norm ∧ ?Err")
    proof
      show ?Norm (is "?val ⟶ ?trans")
      proof
        assume val: ?val
        then have "P ⊢ ?σ1
           -jvm→ (None, h3, ([v], ls3, C', clinit, size(compE2 body), No_ics) # tl ?frs,sh3)"
          using IH_body Jcc_pieces_SCall_clinit_body[OF assms(1) wf pcs method] s1 ls2' by clarsimp
        also have "P ⊢ … -jvm→ (None, h3, tl ?frs, sh3(C'↦(fst(the(sh3 C')),Done)))"
          using jvm_Return_Init[OF M_code] by simp
        finally show ?trans using pcs s1 clinit by simp
      qed
    next
      show ?Err (is "?throw ⟶ ?err")
      proof
        assume throw: ?throw
        with IH_body obtain pc2 vs2 where
          pc2: "0 ≤ pc2 ∧ pc2 < size(compE2 body) ∧
                ¬ caught P pc2 h3 xa (compxE2 body 0 0)" and
          2: "P ⊢ ?σ1 -jvm→ handle P C' clinit xa h3 vs2 ls3 pc2 No_ics (tl ?frs) sh3"
          using SCall1.prems Jcc_pieces_SCall_clinit_body[OF assms(1) wf pcs method] s1 ls2' by clarsimp
        show ?err using SCall1.prems(1) clinit
        proof(cases ics)
          case (Called Cs)
          note 2
          also have "handle P C' clinit xa h3 vs2 ls3 pc2 No_ics (tl ?frs) sh3
             = (None, h3, (vs, ls1, C, M, pc, Throwing (C'#Cs) xa) # frs, sh3)"
            using Called pc2 method by(simp add: handle_def)
          also have "P ⊢ … -jvm→ (None, h3, (vs, ls1, C, M, pc, Throwing Cs xa) # frs,
             sh3(C' ↦ (fst (the (sh3 C')), Error)))" using Called jvm_Throwing by simp
          finally show ?thesis using pcs clinit Called by(clarsimp intro!: exI[where x="[]"])
        qed(auto)
      qed
    qed
  next
    case nclinit: False
    let ?σ1 = "(None,h1,(vs, ls1, C,M,pc,ics)#frs,sh1)"
    let ?pc2 = "pc + length(compEs2 es)"
    let ?frs2 = "(rev pvs @ vs, ls2, C,M,?pc2,ics)#frs"
    let ?σ2 = "(None,h2,?frs2,sh2)"
    let ?frs2' = "([], ls2', D,M',0,No_ics) # ?frs2"
    let ?σ2' = "(None, h2, ?frs2', sh2)"
    have nclinit': "M' ≠ clinit"
     using wf_sees_clinit1[OF wf] visible_method_exists[OF SCall1.hyps(3)]
       sees_method_idemp[OF SCall1.hyps(3)] nclinit SCall1.hyps(5)
       evals1_preserves_elen[OF SCall1.hyps(1)] by fastforce
    have "P1 ⊢1 ⟨es,(h1, ls1, sh1)⟩ [⇒] ⟨map Val pvs,(h2, ls2, sh2)⟩" by fact
    hence [simp]: "length es = length pvs" by(auto dest:evals1_preserves_elen)
    have invoke: "P,C,M,?pc2 ▹ Invokestatic C' M' (length Ts)"
      using SCall1.hyps(5) SCall1.prems nclinit by(auto simp: add.assoc)
    have nsub: "¬ sub_RI body" by(rule sees_wf1_nsub_RI[OF wf SCall1.hyps(3)])
    have IH_es: "PROP ?Ps es h1 ls1 sh1 (map Val pvs) h2 ls2 sh2 C M pc ics pvs xa
                      (map Val pvs) vs frs I" by fact
    have "P ⊢ ?σ1 -jvm→ ?σ2" using IH_es SCall1.prems nclinit by auto fastforce+
    also have "P ⊢ … -jvm→ ?σ2'" using jvm_Invokestatic[OF assms(1) invoke _ SCall1.hyps(3,5,6)]
         SCall1.hyps(4) SCall1.prems nclinit by auto
    finally have 1: "P ⊢ ?σ1 -jvm→ ?σ2'".
    have "P1 ⊢ C' sees M',Static: Ts→T = body in D" by fact
    then have M'_in_D: "P1 ⊢ D sees M',Static: Ts→T = body in D"
      by(rule sees_method_idemp) 
    have M'_code: "compP2 P1,D,M',0 ⊳ compE2 body @ [Return]" using beforeM M'_in_D by simp
    have M'_xtab: "compP2 P1,D,M' ⊳ compxE2 body 0 0/{..<size(compE2 body)},0"
      using M'_in_D by(rule beforexM)
    have IH_body: "PROP ?P body h2 ls2' sh2 e' h3 ls3 sh3 (Class D # Ts) D M' 0 No_ics v xa [] ?frs2
      ({..<size(compE2 body)})" by fact
    have cond: "Jcc_cond P1 (Class D # Ts) D M' [] 0 No_ics {..<length (compE2 body)} h2 sh2 body"
      using nsub_RI_Jcc_pieces[OF assms(1) nsub] M'_code M'_xtab by clarsimp
    show ?thesis (is "?Norm ∧ ?Err")
    proof
      show ?Norm (is "?val ⟶ ?trans")
      proof
        assume val: ?val
        note 1
        also have "P ⊢ ?σ2' -jvm→ (None,h3,([v],ls3,D,M',size(compE2 body),No_ics)#?frs2,sh3)"
          using val IH_body SCall1.prems M'_code cond nsub_RI_Jcc_pieces nsub by auto
        also have "P ⊢ … -jvm→ (None, h3, (v#vs, ls2, C,M,?pc2+1,ics)#frs,sh3)"
          using SCall1.hyps(5) M'_code M'_in_D nclinit' by(cases T, auto)
        finally show ?trans using nclinit by(auto simp:add.assoc)
      qed
    next
      show ?Err (is "?throw ⟶ ?err")
      proof
        assume throw: ?throw
        with IH_body obtain pc2 vs' where
          pc2: "0 ≤ pc2 ∧ pc2 < size(compE2 body) ∧
                ¬ caught P pc2 h3 xa (compxE2 body 0 0)" and
          2: "P ⊢ ?σ2' -jvm→ handle P D M' xa h3 vs' ls3 pc2 No_ics ?frs2 sh3"
          using SCall1.prems M'_code M'_xtab cond nsub_RI_Jcc_pieces nsub
           by (auto simp del:split_paired_Ex)
        have "handle P D M' xa h3 vs' ls3 pc2 No_ics ?frs2 sh3 =
              handle P C M xa h3 (rev pvs @ vs) ls2 ?pc2 ics frs sh3"
          using pc2 M'_in_D nclinit' by(auto simp add:handle_def)
        then show "?err" using pc2 jvm_trans[OF 1 2] nclinit by(auto intro:exI[where x="?pc2"])
      qed
    qed
  qed
next
  case Block1 then show ?case using nsub_RI_Jcc_pieces by auto
next
  case (Seq1 e1 h0 ls0 sh0 w h1 ls1 sh1 e2 e2' h2 ls2 sh2)
  let ?pc1 = "pc + length(compE2 e1)"
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0)"
  let ?σ1 = "(None,h1,(vs,ls1,C,M,?pc1+1,ics)#frs,sh1)"
  let ?I = "I - pcs (compxE2 e2 (Suc ?pc1) (length vs))"
  have Isub: "{pc..<pc + length (compE2 e1)} ⊆ ?I" using Seq1.prems by clarsimp
  have IH: "PROP ?P e1 h0 ls0 sh0 (Val w) h1 ls1 sh1 E C M pc ics w xa vs frs ?I" by fact
  have "P ⊢ ?σ0 -jvm→ (None,h1,(w#vs,ls1,C,M,?pc1,ics)#frs,sh1)"
    using Seq1.prems nsub_RI_Jcc_pieces IH Isub by auto
  also have "P ⊢ … -jvm→ ?σ1" using Seq1 by auto
  finally have eval1: "P ⊢ ?σ0 -jvm→ ?σ1".
  let ?pc2 = "?pc1 + 1 + length(compE2 e2)"
  let ?I' = "I - pcs(compxE2 e1 pc (size vs))"
  have IH2: "PROP ?P e2 h1 ls1 sh1 e2' h2 ls2 sh2 E C M (?pc1+1) ics v xa vs frs
                     ?I'" by fact
  have Isub2: "{Suc (pc + length (compE2 e1))..<Suc (pc + length (compE2 e1) + length (compE2 e2))}
     ⊆ ?I'" using Seq1.prems by clarsimp
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val ⟶ ?trans")
    proof
      assume val: ?val
      note eval1
      also have "P ⊢ ?σ1 -jvm→ (None,h2,(v#vs,ls2,C,M,?pc2,ics)#frs,sh2)"
        using val Seq1.prems nsub_RI_Jcc_pieces IH2 Isub2 by auto
      finally show ?trans by(simp add:add.assoc)
    qed
  next
    show ?Err (is "?throw ⟶ ?err")
    proof
      assume throw: ?throw
      then obtain pc2 vs' where
        pc2: "?pc1+1 ≤ pc2 ∧ pc2 < ?pc2 ∧
              ¬ caught P pc2 h2 xa (compxE2 e2 (?pc1+1) (size vs))" and
        eval2: "P ⊢ ?σ1 -jvm→ handle P C M xa h2 (vs'@vs) ls2 pc2 ics frs sh2"
        using IH2 Seq1.prems nsub_RI_Jcc_pieces Isub2 by auto
      show "?err" using pc2 jvm_trans[OF eval1 eval2] by(auto intro: exI[where x=pc2])
    qed
  qed
next
  case (SeqThrow1 e0 h0 ls0 sh0 e h1 ls1 sh1 e1)
  let ?I = "I - pcs (compxE2 e1 (Suc (pc + length (compE2 e0))) (length vs))"
  obtain a' where throw: "throw e = Throw a'" using eval1_final[OF SeqThrow1.hyps(1)] by clarsimp
  have Isub: "{pc..<pc + length (compE2 e0)} ⊆ ?I" using SeqThrow1.prems by clarsimp
  have "PROP ?P e0 h0 ls0 sh0 (throw e) h1 ls1 sh1 E C M pc ics v a' vs frs ?I" by fact
  then show ?case using SeqThrow1.prems throw nsub_RI_Jcc_pieces Isub by auto
next
  case (CondT1 e h0 ls0 sh0 h1 ls1 sh1 e1 e' h2 ls2 sh2 e2)
  let ?pc1 = "pc + length(compE2 e)"
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0)"
  let ?σ1 = "(None,h1,(vs,ls1,C,M,?pc1+1,ics)#frs,sh1)"
  let ?d = "size vs"
  let ?xt1 = "compxE2 e1 (pc+size(compE2 e)+1) ?d"
  let ?xt2 = "compxE2 e2 (pc+size(compE2 e)+size(compE2 e1)+2) ?d"
  let ?I = "I - (pcs ?xt1 ∪ pcs ?xt2)"
  have Isub: "{pc..<pc + length (compE2 e)} ⊆ ?I" using CondT1.prems by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 true h1 ls1 sh1 E C M pc ics (Bool True) xa vs frs ?I" by fact
  have "P ⊢ ?σ0 -jvm→ (None,h1,(Bool(True)#vs,ls1,C,M,?pc1,ics)#frs,sh1)"
    using CondT1.prems nsub_RI_Jcc_pieces IH Isub by(auto simp: Int_Un_distrib)
  also have "P ⊢ … -jvm→ ?σ1" using CondT1 by auto
  finally have eval1: "P ⊢ ?σ0 -jvm→ ?σ1".
  let ?pc1' = "?pc1 + 1 + length(compE2 e1)"
  let ?pc2' = "?pc1' + 1 + length(compE2 e2)"
  let ?I' = "I - pcs(compxE2 e pc ?d) - pcs(compxE2 e2 (?pc1'+1) ?d)"
  have IH2: "PROP ?P e1 h1 ls1 sh1 e' h2 ls2 sh2 E C M (?pc1+1) ics v xa vs frs ?I'" by fact
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val ⟶ ?trans")
    proof
      assume val: ?val
      note eval1
      also have "P ⊢ ?σ1 -jvm→ (None,h2,(v#vs,ls2,C,M,?pc1',ics)#frs,sh2)"
        using val CondT1.prems nsub_RI_Jcc_pieces IH2 by(fastforce simp:Int_Un_distrib)
      also have "P ⊢ … -jvm→ (None,h2,(v#vs,ls2,C,M,?pc2',ics)#frs,sh2)"
        using CondT1 nsub_RI_Jcc_pieces by(auto simp:add.assoc)
      finally show ?trans by(simp add:add.assoc)
    qed
  next
    show ?Err (is "?throw ⟶ ?err")
    proof
      assume throw: ?throw
      moreover
      note IH2
      ultimately obtain pc2 vs' where
        pc2: "?pc1+1 ≤ pc2 ∧ pc2 < ?pc1' ∧
              ¬ caught P pc2 h2 xa (compxE2 e1 (?pc1+1) (size vs))" and
        eval2: "P ⊢ ?σ1 -jvm→ handle P C M xa h2 (vs'@vs) ls2 pc2 ics frs sh2"
        using CondT1.prems nsub_RI_Jcc_pieces by (fastforce simp:Int_Un_distrib)
      show "?err" using pc2 jvm_trans[OF eval1 eval2] by(auto intro: exI[where x=pc2])
    qed
  qed
next
  case (CondF1 e h0 ls0 sh0 h1 ls1 sh1 e2 e' h2 ls2 sh2 e1)
  let ?pc1 = "pc + length(compE2 e)"
  let ?pc2 = "?pc1 + 1 + length(compE2 e1)+ 1"
  let ?pc2' = "?pc2 + length(compE2 e2)"
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0)"
  let ?σ1 = "(None,h1,(vs,ls1,C,M,?pc2,ics)#frs,sh1)"
  let ?d = "size vs"
  let ?xt1 = "compxE2 e1 (pc+size(compE2 e)+1) ?d"
  let ?xt2 = "compxE2 e2 (pc+size(compE2 e)+size(compE2 e1)+2) ?d"
  let ?I = "I - (pcs ?xt1 ∪ pcs ?xt2)"
  let ?I' = "I - pcs(compxE2 e pc ?d) - pcs(compxE2 e1 (?pc1+1) ?d)"
  have pcs: "pcs(compxE2 e pc ?d) ∩ pcs(?xt1 @ ?xt2) = {}"
    using CondF1.prems by (simp add:Int_Un_distrib)
  have Isub: "{pc..<pc + length (compE2 e)} ⊆ ?I" using CondF1.prems by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 false h1 ls1 sh1 E C M pc ics (Bool False) xa vs frs ?I" by fact
  have IH2: "PROP ?P e2 h1 ls1 sh1 e' h2 ls2 sh2 E C M ?pc2 ics v xa vs frs ?I'" by fact
  have "P ⊢ ?σ0 -jvm→ (None,h1,(Bool(False)#vs,ls1,C,M,?pc1,ics)#frs,sh1)"
    using CondF1.prems nsub_RI_Jcc_pieces IH Isub pcs by auto
  also have "P ⊢ … -jvm→ ?σ1" using CondF1 by auto
  finally have eval1: "P ⊢ ?σ0 -jvm→ ?σ1".
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val ⟶ ?trans")
    proof
      assume val: ?val
      note eval1
      also have "P ⊢ ?σ1 -jvm→ (None,h2,(v#vs,ls2,C,M,?pc2',ics)#frs,sh2)"
        using val CondF1.prems nsub_RI_Jcc_pieces IH2 by(fastforce simp:Int_Un_distrib)
      finally show ?trans by(simp add:add.assoc)
    qed
  next
    show ?Err (is "?throw ⟶ ?err")
    proof
      let ?I' = "I - pcs(compxE2 e pc ?d) - pcs(compxE2 e1 (?pc1+1) ?d)"
      assume throw: ?throw
      then obtain pc2 vs' where
        pc2: "?pc2 ≤ pc2 ∧ pc2 < ?pc2' ∧
              ¬ caught P pc2 h2 xa (compxE2 e2 ?pc2 ?d)" and
        eval2: "P ⊢ ?σ1 -jvm→ handle P C M xa h2 (vs'@vs) ls2 pc2 ics frs sh2"
        using CondF1.prems nsub_RI_Jcc_pieces IH2 by(fastforce simp:Int_Un_distrib)
      show "?err" using pc2 jvm_trans[OF eval1 eval2] by(auto intro: exI[where x=pc2])
    qed
  qed
next
  case (CondThrow1 e h0 ls0 sh0 f h1 ls1 sh1 e1 e2)
  let ?d = "size vs"
  let ?xt1 = "compxE2 e1 (pc+size(compE2 e)+1) ?d"
  let ?xt2 = "compxE2 e2 (pc+size(compE2 e)+size(compE2 e1)+2) ?d"
  let ?I = "I - (pcs ?xt1 ∪ pcs ?xt2)"
  have Isub: "{pc..<pc + length (compE2 e)} ⊆ ?I" using CondThrow1.prems by clarsimp
  have "pcs(compxE2 e pc ?d) ∩ pcs(?xt1 @ ?xt2) = {}"
    using CondThrow1.prems by (simp add:Int_Un_distrib)
  moreover have "PROP ?P e h0 ls0 sh0 (throw f) h1 ls1 sh1 E C M pc ics v xa vs frs ?I" by fact
  ultimately show ?case using CondThrow1.prems nsub_RI_Jcc_pieces Isub by auto
next
  case (WhileF1 e h0 ls0 sh0 h1 ls1 sh1 c)
  let ?pc = "pc + length(compE2 e)"
  let ?pc' = "?pc + length(compE2 c) + 3"
  have Isub: "{pc..<pc + length (compE2 e)} ⊆ I - pcs (compxE2 c (Suc (pc + length (compE2 e))) (length vs))"
    using WhileF1.prems by clarsimp
  have Isub2: "{Suc (pc + length (compE2 e))..<Suc (pc + length (compE2 e) + length (compE2 c))}
     ⊆ I - pcs (compxE2 e pc (length vs))" using WhileF1.prems by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 false h1 ls1 sh1 E C M pc ics (Bool False) xa vs frs
    (I - pcs (compxE2 c (Suc (pc + length (compE2 e))) (length vs)))" by fact
  have "P ⊢ (None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0) -jvm→
            (None,h1,(Bool False#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using WhileF1.prems nsub_RI_Jcc_pieces IH Isub by auto
  also have "P ⊢ … -jvm→ (None,h1,(vs,ls1,C,M,?pc',ics)#frs,sh1)"
    using WhileF1 by (auto simp:add.assoc)
  also have "P ⊢ … -jvm→ (None,h1,(Unit#vs,ls1,C,M,?pc'+1,ics)#frs,sh1)"
    using WhileF1.prems by (auto simp:eval_nat_numeral)
  finally show ?case by (simp add:add.assoc eval_nat_numeral)
next
  case (WhileT1 e h0 ls0 sh0 h1 ls1 sh1 c v1 h2 ls2 sh2 e3 h3 ls3 sh3)
  let ?pc = "pc + length(compE2 e)"
  let ?pc' = "?pc + length(compE2 c) + 1"
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0)"
  let ?σ2 = "(None,h2,(vs,ls2,C,M,pc,ics)#frs,sh2)"
  have Isub: "{pc..<pc + length (compE2 e)} ⊆ I - pcs (compxE2 c (Suc (pc + length (compE2 e))) (length vs))"
    using WhileT1.prems by clarsimp
  have Isub2: "{Suc (pc + length (compE2 e))..<Suc (pc + length (compE2 e) + length (compE2 c))}
     ⊆ I - pcs (compxE2 e pc (length vs))" using WhileT1.prems by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 true h1 ls1 sh1 E C M pc ics (Bool True) xa vs frs
    (I - pcs (compxE2 c (Suc (pc + length (compE2 e))) (length vs)))" by fact
  have IH2: "PROP ?P c h1 ls1 sh1 (Val v1) h2 ls2 sh2 E C M (Suc ?pc) ics v1 xa vs frs
    (I - pcs (compxE2 e pc (length vs)))" by fact
  have "P ⊢ ?σ0 -jvm→ (None,h1,(Bool True#vs,ls1,C,M,?pc,ics)#frs,sh1)"
    using WhileT1.prems nsub_RI_Jcc_pieces IH Isub by auto
  also have "P ⊢ … -jvm→ (None,h1,(vs,ls1,C,M,?pc+1,ics)#frs,sh1)"
    using WhileT1.prems by auto
  also have "P ⊢ … -jvm→ (None,h2,(v1#vs,ls2,C,M,?pc',ics)#frs,sh2)"
    using WhileT1.prems nsub_RI_Jcc_pieces IH2 Isub2 by auto
  also have "P ⊢ … -jvm→ ?σ2" using WhileT1.prems by auto
  finally have 1: "P ⊢ ?σ0 -jvm→ ?σ2".
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val ⟶ ?trans")
    proof
      assume val: ?val
      note 1
      also have "P ⊢ ?σ2 -jvm→ (None,h3,(v#vs,ls3,C,M,?pc'+3,ics)#frs,sh3)"
        using val WhileT1 by (auto simp add:add.assoc eval_nat_numeral)
      finally show ?trans by(simp add:add.assoc eval_nat_numeral)
    qed
  next
    show ?Err (is "?throw ⟶ ?err")
    proof
      assume throw: ?throw
      moreover
      have "PROP ?P (while (e) c) h2 ls2 sh2 e3 h3 ls3 sh3 E C M pc ics v xa vs frs I" by fact
      ultimately obtain pc2 vs' where
        pc2: "pc ≤ pc2 ∧ pc2 < ?pc'+3 ∧
              ¬ caught P pc2 h3 xa (compxE2 (while (e) c) pc (size vs))" and
        2: "P ⊢ ?σ2 -jvm→ handle P C M xa h3 (vs'@vs) ls3 pc2 ics frs sh3"
        using WhileT1.prems by (auto simp:add.assoc eval_nat_numeral)
      show "?err" using pc2 jvm_trans[OF 1 2] by(auto intro: exI[where x=pc2])
    qed
  qed
next
  case (WhileCondThrow1 e h ls sh e' h' ls' sh' c)
  let ?I = "I - pcs (compxE2 c (Suc (pc + length (compE2 e))) (length vs))"
  obtain a' where throw: "throw e' = Throw a'" using eval1_final[OF WhileCondThrow1.hyps(1)] by clarsimp
  have Isub: "{pc..<pc + length (compE2 e)} ⊆ ?I" using WhileCondThrow1.prems by clarsimp
  have "PROP ?P e h ls sh (throw e') h' ls' sh' E C M pc ics v a' vs frs ?I" by fact
  then show ?case using WhileCondThrow1.prems throw nsub_RI_Jcc_pieces Isub by auto
next
  case (WhileBodyThrow1 e h0 ls0 sh0 h1 ls1 sh1 c e' h2 ls2 sh2)
  let ?pc1 = "pc + length(compE2 e)"
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0)"
  let ?σ1 = "(None,h1,(vs,ls1,C,M,?pc1+1,ics)#frs,sh1)"
  let ?I = "I - pcs (compxE2 c (Suc (pc + length (compE2 e))) (length vs))"
  have Isub: "{pc..<pc + length (compE2 e)} ⊆ ?I"
    using WhileBodyThrow1.prems by clarsimp
  have IH: "PROP ?P e h0 ls0 sh0 true h1 ls1 sh1 E C M pc ics (Bool True) xa vs frs ?I" by fact
  then have "P ⊢ ?σ0 -jvm→ (None,h1,(Bool(True)#vs,ls1,C,M,?pc1,ics)#frs,sh1)"
    using WhileBodyThrow1.prems nsub_RI_Jcc_pieces Isub by auto
  also have "P ⊢ … -jvm→ ?σ1" using  WhileBodyThrow1 by auto
  finally have eval1: "P ⊢ ?σ0 -jvm→ ?σ1".
  let ?pc1' = "?pc1 + 1 + length(compE2 c)"
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm by simp
  next
    show ?Err (is "?throw ⟶ ?err")
    proof
      assume throw: ?throw
      moreover
      have "PROP ?P c h1 ls1 sh1 (throw e') h2 ls2 sh2 E C M (?pc1+1) ics v xa vs frs
                    (I - pcs (compxE2 e pc (size vs)))" by fact
      ultimately obtain pc2 vs' where
        pc2: "?pc1+1 ≤ pc2 ∧ pc2 < ?pc1' ∧
              ¬ caught P pc2 h2 xa (compxE2 c (?pc1+1) (size vs))" and
        eval2: "P ⊢ ?σ1 -jvm→ handle P C M xa h2 (vs'@vs) ls2 pc2 ics frs sh2"
        using WhileBodyThrow1.prems nsub_RI_Jcc_pieces by (fastforce simp:Int_Un_distrib)
      show "?err" using pc2 jvm_trans[OF eval1 eval2] by(auto intro: exI[where x=pc2])
    qed
  qed
next
  case (Throw1 e h0 ls0 sh0 a h1 ls1 sh1)
  let ?pc = "pc + size(compE2 e)"
  have Isub: "{pc..<pc + length (compE2 e)} ⊆ I" using Throw1.prems by clarsimp
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm by simp
  next
    show ?Err (is "?throw ⟶ ?err")
    proof
      assume throw:?throw
      have "PROP ?P e h0 ls0 sh0 (addr a) h1 ls1 sh1 E C M pc ics (Addr a) a vs frs I" by fact
      then have "P ⊢ (None, h0, (vs, ls0, C, M, pc, ics) # frs, sh0) -jvm→
                 (None, h1, (Addr xa#vs, ls1, C, M, ?pc, ics) # frs, sh1)"
        using Throw1 nsub_RI_Jcc_pieces Isub throw by auto
      also have "P ⊢ … -jvm→ handle P C M xa h1 (Addr xa#vs) ls1 ?pc ics frs sh1"
        using Throw1.prems by(auto simp add:handle_def)
      finally show "?err" by(auto intro!: exI[where x="?pc"] exI[where x="[Addr xa]"])
    qed
  qed
next
  case (ThrowNull1 e h0 ls0 sh0 h1 ls1 sh1)
  let ?pc = "pc + size(compE2 e)"
  let ?xa = "addr_of_sys_xcpt NullPointer"
  have Isub: "{pc..<pc + length (compE2 e)} ⊆ I" using ThrowNull1.prems by clarsimp
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm by simp
  next
    show ?Err (is "?throw ⟶ ?err")
    proof
      assume throw: ?throw
      have "PROP ?P e h0 ls0 sh0 null h1 ls1 sh1 E C M pc ics Null xa vs frs I" by fact
      then have "P ⊢ (None, h0, (vs, ls0, C, M, pc, ics) # frs, sh0) -jvm→
                 (None, h1, (Null#vs, ls1, C, M, ?pc, ics) # frs, sh1)"
        using ThrowNull1.prems nsub_RI_Jcc_pieces Isub by auto
      also have "P ⊢ … -jvm→  handle P C M ?xa h1 (Null#vs) ls1 ?pc ics frs sh1"
        using ThrowNull1.prems by(auto simp add:handle_def)
      finally show "?err" using throw by(auto intro!: exI[where x="?pc"] exI[where x="[Null]"])
    qed
  qed
next
  case (ThrowThrow1 e h ls sh e' h' ls' sh')
  obtain a' where throw: "throw e' = Throw a'" using eval1_final[OF ThrowThrow1.hyps(1)] by clarsimp
  have Isub: "{pc..<pc + length (compE2 e)} ⊆ I" using ThrowThrow1.prems by clarsimp
  have "PROP ?P e h ls sh (throw e') h' ls' sh' E C M pc ics v a' vs frs I" by fact
  then show ?case using ThrowThrow1.prems throw nsub_RI_Jcc_pieces Isub by auto
next
  case (Try1 e1 h0 ls0 sh0 v1 h1 ls1 sh1 Ci i e2)
  let ?pc1 = "pc + length(compE2 e1)"
  let ?pc1' = "?pc1 + 2 + length(compE2 e2)"
  have "{pc..<pc+size(compE2 (try e1 catch(Ci i) e2))} ⊆ I" using Try1.prems by simp
  also have "P,C,M ⊳ compxE2 (try e1 catch(Ci i) e2) pc (size vs) / I,size vs"
    using Try1.prems by simp
  ultimately have "P,C,M ⊳ compxE2 e1 pc (size vs) / {pc..<pc + length (compE2 e1)},size vs"
    by(rule beforex_try)
  hence "P ⊢ (None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0) -jvm→
             (None,h1,(v1#vs,ls1,C,M,?pc1,ics)#frs,sh1)"
    using Try1 nsub_RI_Jcc_pieces by auto blast
  also have "P ⊢ … -jvm→ (None,h1,(v1#vs,ls1,C,M,?pc1',ics)#frs,sh1)"
    using Try1.prems by auto
  finally show ?case by (auto simp:add.assoc)
next
  case (TryCatch1 e1 h0 ls0 sh0 a h1 ls1 sh1 D fs Ci i e2 e2' h2 ls2 sh2)
  let ?e = "try e1 catch(Ci i) e2"
  let ?xt = "compxE2 ?e pc (size vs)"
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0)"
  let ?ls1 = "ls1[i := Addr a]"
  let ?pc1 = "pc + length(compE2 e1)"
  let ?pc1' = "?pc1 + 2"
  let ?σ1 = "(None,h1,(vs,?ls1,C,M, ?pc1',ics) # frs,sh1)"
  have I: "{pc..<pc + length (compE2 (try e1 catch(Ci i) e2))} ⊆ I"
   and beforex: "P,C,M ⊳ ?xt/I,size vs" using TryCatch1.prems by simp+
  have "P ⊢ ?σ0 -jvm→ (None,h1,((Addr a)#vs,ls1,C,M, ?pc1+1,ics) # frs,sh1)"
  proof -
    have ics: "ics = No_ics" using TryCatch1.prems by auto
    have "PROP ?P e1 h0 ls0 sh0 (Throw a) h1 ls1 sh1 E C M pc ics v a vs frs {pc..<pc + length (compE2 e1)}"
      by fact
    moreover have "P,C,M ⊳ compxE2 e1 pc (size vs)/{pc..<?pc1},size vs"
      using beforex I pcs_subset by(force elim!: beforex_appendD1)
    ultimately have
      "∃pc1. pc ≤ pc1 ∧ pc1 < ?pc1 ∧
             ¬ caught P pc1 h1 a (compxE2 e1 pc (size vs)) ∧
             (∃vs'. P ⊢ ?σ0 -jvm→ handle P C M a h1 (vs'@vs) ls1 pc1 ics frs sh1)"
      using  TryCatch1.prems nsub_RI_Jcc_pieces by auto
    then obtain pc1 vs' where
      pc1_in_e1: "pc ≤ pc1" "pc1 < ?pc1" and
      pc1_not_caught: "¬ caught P pc1 h1 a (compxE2 e1 pc (size vs))" and
      0: "P ⊢ ?σ0 -jvm→ handle P C M a h1 (vs'@vs) ls1 pc1 ics frs sh1" by iprover
    from beforex obtain xt0 xt1
      where ex_tab: "ex_table_of P C M = xt0 @ ?xt @ xt1"
      and disj: "pcs xt0 ∩ I = {}" by(auto simp:beforex_def)
    have hp: "h1 a = Some (D, fs)" "P1 ⊢ D ≼* Ci" by fact+
    have "pc1 ∉ pcs xt0" using pc1_in_e1 I disj by auto
    with pc1_in_e1 pc1_not_caught hp
    show ?thesis using ex_tab 0 ics by(simp add:handle_def matches_ex_entry_def)
  qed
  also have "P ⊢ … -jvm→ ?σ1" using TryCatch1 by auto
  finally have 1: "P ⊢ ?σ0 -jvm→ ?σ1" .
  let ?pc2 = "?pc1' + length(compE2 e2)"
  let ?I2 = "{?pc1' ..< ?pc2}"
  have "P,C,M ⊳ compxE2 ?e pc (size vs) / I,size vs" by fact
  hence beforex2: "P,C,M ⊳ compxE2 e2 ?pc1' (size vs) / ?I2, size vs"
    using I pcs_subset[of _ ?pc1'] by(auto elim!:beforex_appendD2)
  have IH2: "PROP ?P e2 h1 ?ls1 sh1 e2' h2 ls2 sh2 E C M ?pc1' ics v xa vs frs ?I2" by fact
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val ⟶ ?trans")
    proof
      assume val: ?val
      note 1 also have "P ⊢ ?σ1 -jvm→ (None,h2,(v#vs,ls2,C,M,?pc2,ics)#frs,sh2)"
        using val beforex2 IH2 TryCatch1.prems nsub_RI_Jcc_pieces by auto
      finally show ?trans by(simp add:add.assoc)
    qed
  next
    show ?Err (is "?throw ⟶ ?err")
    proof
      assume throw: ?throw
      then obtain pc2 vs' where
        pc2: "?pc1+2 ≤ pc2 ∧ pc2 < ?pc2 ∧
              ¬ caught P pc2 h2 xa (compxE2 e2 ?pc1' (size vs))" and
        2: "P ⊢ ?σ1 -jvm→ handle P C M xa h2 (vs'@vs) ls2 pc2 ics frs sh2"
        using IH2 beforex2 TryCatch1.prems nsub_RI_Jcc_pieces by auto
      show ?err using pc2 jvm_trans[OF 1 2]
       by (simp add:match_ex_entry) (auto intro: exI[where x=pc2])
    qed
  qed
next
  case (TryThrow1 e1 h0 ls0 sh0 a h1 ls1 sh1 D fs Ci i e2)
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0)"
  let ?pc1 = "pc + length(compE2 e1)"
  let ?e = "try e1 catch(Ci i) e2"
  let ?xt = "compxE2 ?e pc (size vs)"
  have I: "{pc..<pc + length (compE2 (try e1 catch(Ci i) e2))} ⊆ I"
   and beforex: "P,C,M ⊳ ?xt/I,size vs" using TryThrow1.prems by simp+
  have "PROP ?P e1 h0 ls0 sh0 (Throw a) h1 ls1 sh1 E C M pc ics v a vs frs 
   {pc..<pc + length (compE2 e1)}" by fact
  moreover have "P,C,M ⊳ compxE2 e1 pc (size vs)/{pc..<?pc1},size vs"
    using beforex I pcs_subset by(force elim!: beforex_appendD1)
    ultimately have
      "∃pc1. pc ≤ pc1 ∧ pc1 < ?pc1 ∧
             ¬ caught P pc1 h1 a (compxE2 e1 pc (size vs)) ∧
             (∃vs'. P ⊢ ?σ0 -jvm→ handle P C M a h1 (vs'@vs) ls1 pc1 ics frs sh1)"
      using TryThrow1.prems nsub_RI_Jcc_pieces by auto
    then obtain pc1 vs' where
      pc1_in_e1: "pc ≤ pc1" "pc1 < ?pc1" and
      pc1_not_caught: "¬ caught P pc1 h1 a (compxE2 e1 pc (size vs))" and
      0: "P ⊢ ?σ0 -jvm→ handle P C M a h1 (vs'@vs) ls1 pc1 ics frs sh1" by iprover
  show ?case (is "?N ∧ (?eq ⟶ ?err)")
  proof
    show ?N by simp
  next
    { assume ?eq
      with TryThrow1 pc1_in_e1 pc1_not_caught 0
      have "?err" by (simp add:match_ex_entry) auto
    }
    thus "?eq ⟶ ?err" by iprover
  qed
next
  case Nil1 thus ?case by simp
next
  case (Cons1 e h0 ls0 sh0 v h1 ls1 sh1 es fs h2 ls2 sh2)
  let ?pc1 = "pc + length(compE2 e)"
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc,ics)#frs,sh0)"
  let ?σ1 = "(None,h1,(v#vs,ls1,C,M,?pc1,ics)#frs,sh1)"
  have IH: "PROP ?P e h0 ls0 sh0 (Val v) h1 ls1 sh1 [] C M pc ics v xa vs frs
    (I - pcs (compxEs2 es ?pc1 (Suc (length vs))))" by fact
  then have 1: "P ⊢ ?σ0 -jvm→ ?σ1" using Jcc_pieces_Cons[OF _ Cons1.prems(1-5)] by auto
  let ?pc2 = "?pc1 + length(compEs2 es)"
  have IHs: "PROP ?Ps es h1 ls1 sh1 fs h2 ls2 sh2 C M ?pc1 ics (tl ws) xa es' (v#vs) frs
    (I - pcs (compxE2 e pc (length vs)))" by fact
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val ⟶ ?trans")
    proof
      assume val: ?val
      note 1
      also have "P ⊢ ?σ1 -jvm→ (None,h2,(rev(ws) @ vs,ls2,C,M,?pc2,ics)#frs,sh2)"
        using val IHs Cons1.prems by fastforce
      finally show ?trans by(simp add:add.assoc)
    qed
  next
    show ?Err (is "?throw ⟶ (∃pc2. ?H pc2)")
    proof
      assume throw: ?throw
      then obtain pc2 vs' where
        pc2: "?pc1 ≤ pc2 ∧ pc2 < ?pc2 ∧
              ¬ caught P pc2 h2 xa (compxEs2 es ?pc1 (size vs + 1))" and
        2: "P ⊢ ?σ1 -jvm→ handle P C M xa h2 (vs'@v#vs) ls2 pc2 ics frs sh2"
        using IHs Cons1.prems by(fastforce simp:Cons_eq_append_conv neq_Nil_conv)
      have "?H pc2" using Cons1.prems pc2 jvm_trans[OF 1 2] by(auto intro!: exI[where x="vs'@[v]"])
      thus "∃pc2. ?H pc2" by iprover
    qed
  qed
next
  case (ConsThrow1 e h0 ls0 sh0 a h1 ls1 sh1 es)
  then show ?case using Jcc_pieces_Cons[OF _ ConsThrow1.prems(1-5)]
    by (fastforce simp:Cons_eq_append_conv)
next
  case InitFinal1 then show ?case using eval1_final_same[OF InitFinal1.hyps(1)] by clarsimp
next
  case (InitNone1 sh C0 C' Cs e h l e' h' l' sh')
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh' v xa
     (INIT C' (C0 # Cs,False) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
    using InitNone1.prems(1) by clarsimp
  let ?sh = "(sh(C0 ↦ (sblank P1 C0, Prepared)))"
  obtain ics: "ics_of(hd frs') = Calling C0 Cs"
     and frs1: "frs' ≠ Nil" using pcs by clarsimp
  then have 1: "P ⊢ (None,h,frs',sh) -jvm→ (None,h,frs',?sh)"
    using InitNone1 jvm_InitNone[where P = P] by(cases frs', simp+)
  show ?case (is "(?e1 ⟶ ?jvm1) ∧ (?e2 ⟶ ?err)")
  proof(rule conjI)
    { assume val: ?e1
      note 1
      also have "P ⊢ (None,h,frs',?sh) -jvm→ (None,h',(vs,l,C,M,pc,Called [])#frs,sh')"
        using InitNone1.hyps(3)[of E] Jcc_pieces_InitNone[OF assms(1) pcs] InitNone1.prems val
         by clarsimp
      finally have ?jvm1 using pcs by simp
    }
    thus "?e1 ⟶ ?jvm1" by simp
  next
    { assume throw: ?e2
      note 1
      also obtain vs' where "P ⊢ (None,h,frs',?sh)
                     -jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh'"
        using InitNone1.hyps(3)[of E] Jcc_pieces_InitNone[OF assms(1) pcs] throw
         by clarsimp presburger
      finally have ?err using pcs by auto
    }
    thus "?e2 ⟶ ?err" by simp
  qed
next
  case (InitDone1 sh C0 sfs C' Cs e h l e' h' l' sh')
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh' v xa
     (INIT C' (C0 # Cs,False) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
    using InitDone1.prems(1) by clarsimp
  let ?frs' = "(calling_to_scalled (hd frs'))#(tl frs')"
  have IH: "PROP ?P (INIT C' (Cs,True) ← e) h l sh e' h' l' sh' E C M pc ics v xa vs frs I"
    by fact
  obtain ics: "ics_of(hd frs') = Calling C0 Cs"
     and frs1: "frs' ≠ Nil" using pcs by clarsimp
  then have 1: "P ⊢ (None,h,frs',sh) -jvm→ (None,h,?frs',sh)"
    using InitDone1 jvm_InitDP[where P = P] by(cases frs', simp+)
  show ?case (is "(?e1 ⟶ ?jvm1) ∧ (?e2 ⟶ ?err)")
  proof(rule conjI)
    { assume val: ?e1
      note 1
      also have "P ⊢ (None,h,?frs',sh) -jvm→ (None,h',(vs,l,C,M,pc,Called [])#frs,sh')"
        using IH Jcc_pieces_InitDP[OF assms(1) pcs] InitDone1.prems val by clarsimp
      finally have ?jvm1 using pcs by simp
    }
    thus "?e1 ⟶ ?jvm1" by simp
  next
    { assume throw: ?e2
      note 1
      also obtain vs' where "P ⊢ (None,h,?frs',sh)
                     -jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh'"
        using IH Jcc_pieces_InitDP[OF assms(1) pcs] InitDone1.prems throw by clarsimp
      finally have ?err using pcs by auto
    }
    thus "?e2 ⟶ ?err" by simp
  qed
next
  case (InitProcessing1 sh C0 sfs C' Cs e h l e' h' l' sh')
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh' v xa
     (INIT C' (C0 # Cs,False) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
    using InitProcessing1.prems(1) by clarsimp
  let ?frs' = "(calling_to_scalled (hd frs'))#(tl frs')"
  have IH: "PROP ?P (INIT C' (Cs,True) ← e) h l sh e' h' l' sh' E C M pc ics v xa vs frs I"
    by fact
  obtain ics: "ics_of(hd frs') = Calling C0 Cs"
     and frs1: "frs' ≠ Nil" using pcs by clarsimp
  then have 1: "P ⊢ (None,h,frs',sh) -jvm→ (None,h,?frs',sh)"
    using InitProcessing1 jvm_InitDP[where P = P] by(cases frs', simp+)
  show ?case (is "(?e1 ⟶ ?jvm1) ∧ (?e2 ⟶ ?err)")
  proof(rule conjI)
    { assume val: ?e1
      note 1
      also have "P ⊢ (None,h,?frs',sh) -jvm→ (None,h',(vs,l,C,M,pc,Called [])#frs,sh')"
        using IH Jcc_pieces_InitDP[OF assms(1) pcs] InitProcessing1.prems val by clarsimp
      finally have ?jvm1 using pcs by simp
    }
    thus "?e1 ⟶ ?jvm1" by simp
  next
    { assume throw: ?e2
      note 1
      also obtain vs' where "P ⊢ (None,h,?frs',sh)
                     -jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh'"
        using IH Jcc_pieces_InitDP[OF assms(1) pcs] InitProcessing1.prems throw by clarsimp
      finally have ?err using pcs by auto
    }
    thus "?e2 ⟶ ?err" by simp
  qed
next
  case (InitError1 sh C0 sfs Cs e h l e' h' l' sh' C')
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh' v xa
     (INIT C' (C0 # Cs,False) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
    using InitError1.prems(1) by clarsimp
  let ?e0 = "THROW NoClassDefFoundError"
  let ?frs' = "(calling_to_sthrowing (hd frs') (addr_of_sys_xcpt NoClassDefFoundError))#(tl frs')"
  have IH: "PROP ?P (RI (C0,?e0) ; Cs ← e) h l sh e' h' l' sh' E C M pc ics v xa vs frs I" by fact
  obtain ics: "ics_of(hd frs') = Calling C0 Cs"
     and frs1: "frs' ≠ Nil"
     and tl: "tl frs' = frs" using pcs by clarsimp
  then have 1: "P ⊢ (None,h,frs',sh) -jvm→ (None,h,?frs',sh)"
  proof(cases frs')
    case (Cons a list)
    obtain vs' l' C' M' pc' ics' where a: "a = (vs',l',C',M',pc',ics')" by(cases a)
    then have "ics' = Calling C0 Cs" using Cons ics by simp
    then show ?thesis
     using Cons a IH InitError1.prems jvm_InitError[where P = P] InitError1.hyps(1) by simp
  qed(simp)
  show ?case (is "(?e1 ⟶ ?jvm1) ∧ (?e2 ⟶ ?err)")
  proof(rule conjI)
    { assume val: ?e1
      then have False using val rinit1_throw[OF InitError1.hyps(2)] by blast
      then have ?jvm1 using pcs by simp
    }
    thus "?e1 ⟶ ?jvm1" by simp
  next
    { assume throw: ?e2
      let ?frs = "(calling_to_throwing (hd frs') (addr_of_sys_xcpt NoClassDefFoundError))#(tl frs')"
      have exec: "exec (P, (None,h,?frs,sh)) = Some (None,h,?frs',sh)"
        using exec_ErrorThrowing[where sh=sh, OF InitError1.hyps(1)] ics by(cases "hd frs'", simp)
      obtain vs' where 2: "P ⊢ (None,h,?frs,sh) -jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh'"
        using IH Jcc_pieces_InitError[OF assms(1) pcs InitError1.hyps(1)] throw by clarsimp
      have neq: "(None, h, ?frs, sh) ≠ handle P C M xa h' (vs' @ vs) l pc ics frs sh'"
        using tl ics by(cases "hd frs'", simp add: handle_frs_tl_neq)

      note 1
      also have "P ⊢ (None,h,?frs',sh) -jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh'"
        using exec_1_exec_all_conf[OF exec 2] neq by simp
      finally have ?err using pcs by auto
    }
    thus "?e2 ⟶ ?err" by simp
  qed
next
  case (InitObject1 sh C0 sfs sh' C' Cs e h l e' h' l' sh'')
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l'
    (sh(C0 ↦ (sfs, Processing))) v xa (INIT C' (C0 # Cs,False) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
    using InitObject1.prems(1) by clarsimp
  let ?frs' = "(calling_to_called (hd frs'))#(tl frs')"
  have IH: "PROP ?P (INIT C' (C0#Cs,True) ← e) h l sh' e' h' l' sh'' E C M pc ics v xa vs frs I"
    by fact
  obtain ics: "ics_of(hd frs') = Calling C0 Cs"
     and frs1: "frs' ≠ Nil" using pcs by clarsimp
  then have 1: "P ⊢ (None,h,frs',sh) -jvm→ (None,h,?frs',sh')"
  proof(cases frs')
    case (Cons a list)
    obtain vs' l' C' M' pc' ics' where a: "a = (vs',l',C',M',pc',ics')" by(cases a)
    then have "ics' = Calling C0 Cs" using Cons ics by simp
    then show ?thesis
     using Cons Nil a IH InitObject1 jvm_InitObj[where P = P] by simp
  qed(simp)
  show ?case (is "(?e1 ⟶ ?jvm1) ∧ (?e2 ⟶ ?err)")
  proof(rule conjI)
    { assume val: ?e1
      note 1
      also have "P ⊢ (None,h,?frs',sh') -jvm→ (None,h',(vs,l,C,M,pc,Called [])#frs,sh'')"
        using IH Jcc_pieces_InitObj[OF assms(1) pcs] InitObject1 val by simp
      finally have ?jvm1 using pcs by simp
    }
    thus "?e1 ⟶ ?jvm1" by simp
  next
    { assume throw: ?e2
      note 1
      also obtain vs' where "P ⊢ (None,h,?frs',sh')
                     -jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh''"
        using IH Jcc_pieces_InitObj[OF assms(1) pcs] InitObject1 throw by clarsimp
      finally have ?err using pcs by auto
    }
    thus "?e2 ⟶ ?err" by simp
  qed
next
  case (InitNonObject1 sh C0 sfs D a b sh' C' Cs e h l e' h' l' sh'')
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l'
    (sh(C0 ↦ (sfs,Processing))) v xa (INIT C' (C0 # Cs,False) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
    using InitNonObject1.prems(1) by clarsimp
  let ?frs' = "(calling_to_calling (hd frs') D)#(tl frs')"
  have cls1: "is_class P1 D" using InitNonObject1.hyps(2,3) class_wf wf wf_cdecl_supD by blast
  have cls_aux: "distinct (C0#Cs) ∧ supercls_lst P1 (C0#Cs)" using InitNonObject1.prems(1) by auto
  then have cls2: "D ∉ set (C0 # Cs)"
  proof -
    have "distinct (D # C0 # Cs)"
      using InitNonObject1.hyps(2,3) cls_aux wf wf_supercls_distinct_app by blast
    then show "D ∉ set (C0 # Cs)"
      by (metis distinct.simps(2))
  qed
  have cls3: "∀C∈set (C0 # Cs). P1 ⊢ C ≼* D" using InitNonObject1.hyps(2,3) cls_aux
    by (metis r_into_rtrancl rtrancl_into_rtrancl set_ConsD subcls1.subcls1I supercls_lst.simps(1))
  have IH: "PROP ?P (INIT C' (D # C0 # Cs,False) ← e) h l sh' e' h' l' sh'' E C M pc ics v xa vs frs I"
    by fact
  obtain r where cls: "class P C0 = ⌊(D, r)⌋" using InitNonObject1.hyps(3)
    by (metis assms class_compP compP2_def)
  obtain ics: "ics_of(hd frs') = Calling C0 Cs"
     and frs1: "frs' ≠ Nil" using pcs by clarsimp
  then have 1: "P ⊢ (None,h,frs',sh) -jvm→ (None,h,?frs',sh')"
  proof(cases frs')
    case (Cons a list)
    obtain vs' l' C' M' pc' ics' where a: "a = (vs',l',C',M',pc',ics')" by(cases a)
    then have "ics' = Calling C0 Cs" using Cons ics by simp
    then show ?thesis
     using Cons a IH InitNonObject1 jvm_InitNonObj[OF _ _ cls] by simp
  qed(simp)
  show ?case (is "(?e1 ⟶ ?jvm1) ∧ (?e2 ⟶ ?err)")
  proof(rule conjI)
    { assume val: ?e1
      note 1
      also have "P ⊢ (None,h,?frs',sh') -jvm→ (None,h',(vs,l,C,M,pc,Called [])#frs,sh'')"
        using IH Jcc_pieces_InitNonObj[OF assms(1) cls1 cls2 cls3 pcs] InitNonObject1 val by simp
      finally have ?jvm1 using pcs by simp
    }
    thus "?e1 ⟶ ?jvm1" by simp
  next
    { assume throw: ?e2
      note 1
      also obtain vs' where "P ⊢ (None,h,?frs',sh')
                     -jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh''"
        using IH Jcc_pieces_InitNonObj[OF assms(1) cls1 cls2 cls3 pcs] InitNonObject1 throw by clarsimp
      finally have ?err using pcs by auto
    }
    thus "?e2 ⟶ ?err" by simp
  qed
next
  case (InitRInit1 C0 Cs e h l sh e' h' l' sh' C')
  then obtain frs' err where pcs: "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh' v xa
     (INIT C' (C0 # Cs,True) ← e)
    = (True, frs', (None, h', (vs, l, C, M, pc, Called []) # frs, sh'), err)"
    using InitRInit1.prems(1) by clarsimp
  have IH: "PROP ?P (RI (C0,C0∙sclinit([])) ; Cs ← e) h l sh e' h' l' sh' E C M pc ics v xa vs frs I"
    by fact
  show ?case (is "(?e1 ⟶ ?jvm1) ∧ (?e2 ⟶ ?err)")
  proof(rule conjI)
    { assume val: ?e1
      have "P ⊢ (None,h,frs',sh) -jvm→ (None,h',(vs,l,C,M,pc,Called [])#frs,sh')"
        using IH Jcc_pieces_InitRInit[OF assms(1,2) pcs] InitRInit1.prems val by simp
      then have ?jvm1 using pcs by simp
    }
    thus "?e1 ⟶ ?jvm1" by simp
  next
    { assume throw: ?e2
      obtain vs' where "P ⊢ (None,h,frs',sh)
                     -jvm→ handle P C M xa h' (vs'@vs) l pc ics frs sh'"
        using IH Jcc_pieces_InitRInit[OF assms(1,2) pcs] InitRInit1 throw by clarsimp
      then have ?err using pcs by auto
    }
    thus "?e2 ⟶ ?err" by simp
  qed
next
  case (RInit1 e h l sh v1 h' l' sh' C0 sfs i sh'' C' Cs e' e1 h1 l1 sh1)
  let ?frs = "(vs,l,C,M,pc,Called (C0#Cs)) # frs"
  let ?frs' = "(vs,l,C,M,pc,Called Cs) # frs"
  have clinit: "e = C0∙sclinit([])" using RInit1
    by (metis Jcc_cond.simps(2) eval1_final_same exp.distinct(101) final_def)
  then obtain err where pcs: "Jcc_pieces P1 E C M h vs l pc ics frs sh I h1 l1 sh1 v xa
     (RI (C0,C0∙sclinit([])) ; Cs ← e')
    = (True, ?frs, (None, h1, (vs, l, C, M, pc, Called []) # frs, sh1), err)"
    using RInit1.prems(1) by simp
  have shC: "∀C'∈set Cs. ∃sfs. sh C' = ⌊(sfs, Processing)⌋" using RInit1.prems(1) clinit by clarsimp
  then have shC'': "∀C'∈set Cs. ∃sfs. sh'' C' = ⌊(sfs, Processing)⌋"
    using clinit1_proc_pres[OF wf] RInit1.hyps(1) clinit RInit1.hyps(4) RInit1.prems(1)
      by (auto simp: fun_upd_apply)
  have loc: "l = l'" using clinit1_loc_pres RInit1.hyps(1) clinit by simp
  have IH: "PROP ?P e h l sh (Val v1) h' l' sh' E C M pc (Called Cs) v1 xa vs (tl ?frs') I" by fact
  then have IH':
   "PROP ?P (C0∙sclinit([])) h l sh (Val v1) h' l' sh' E C M pc (Called Cs) v1 xa vs (tl ?frs') I"
    using clinit by simp
  have IH2: "PROP ?P (INIT C' (Cs,True) ← e') h' l' sh'' e1 h1 l1 sh1 E C M
    pc ics v xa vs frs I" by fact
  have "P ⊢ (None,h,?frs,sh) -jvm→ (None,h,create_init_frame P C0 # ?frs',sh)" by(rule jvm_Called)
  also have "P ⊢ … -jvm→ (None,h',?frs',sh'')"
     using IH' Jcc_pieces_RInit_clinit[OF assms(1-2) pcs,of h' l' sh'] RInit1.hyps(3,4) by simp
  finally have jvm1: "P ⊢ (None,h,?frs,sh) -jvm→ (None,h',?frs',sh'')" .
  show ?case (is "(?e1 ⟶ ?jvm1) ∧ (?e2 ⟶ ?err)")
  proof(rule conjI)
    { assume val: ?e1
      note jvm1
      also have "P ⊢ (None,h',?frs',sh'') -jvm→ (None,h1,(vs,l,C,M,pc,Called [])#frs,sh1)"
        using IH2 Jcc_pieces_RInit_Init[OF assms(1-2) shC'' pcs,of h'] RInit1.hyps(5) loc val by auto
      finally have ?jvm1 using pcs clinit by simp
    }
    thus "?e1 ⟶ ?jvm1" by simp
  next
    { assume throw: ?e2
      note jvm1
      also obtain vs' where "P ⊢ (None,h',?frs',sh'')
                     -jvm→ handle P C M xa h1 (vs'@vs) l pc ics frs sh1"
        using IH2 Jcc_pieces_RInit_Init[OF assms(1-2) shC'' pcs,of h'] RInit1.hyps(5) loc throw by auto
      finally have ?err using pcs clinit by auto
    }
    thus "?e2 ⟶ ?err" by simp
  qed
next
  case (RInitInitFail1 e h l sh a h' l' sh' C0 sfs i sh'' D Cs e' e1 h1 l1 sh1)
  let ?frs = "(vs,l,C,M,pc,Called (C0#D#Cs)) # frs"
  let ?frs' = "(vs,l,C,M,pc,Called (D#Cs)) # frs"
  let "?frsT" = "λxa1. (vs,l,C,M,pc,Throwing (C0#D#Cs) xa1) # frs"
  let "?frsT'" = "λxa1. (vs,l,C,M,pc,Throwing (D#Cs) xa1) # frs"
  obtain xa' where xa': "throw a = Throw xa'"
    by (metis RInitInitFail1.hyps(1) eval1_final exp.distinct(101) final_def)
  have e1: "e1 = Throw xa'" using xa' rinit1_throw RInitInitFail1.hyps(5) by simp
  show ?case
  proof(cases "e = C0∙sclinit([])")
    case clinit: True
    then obtain err where pcs: "Jcc_pieces P1 E C M h vs l pc ics frs sh I h1 l1 sh1 v xa'
       (RI (C0,C0∙sclinit([])) ; D # Cs ← e')
      = (True, ?frs, (None, h1, (vs, l, C, M, pc, Called []) # frs, sh1), err)"
      using RInitInitFail1.prems(1) by simp
    have loc: "l = l'" using clinit1_loc_pres RInitInitFail1.hyps(1) clinit by simp
    have IH: "PROP ?P e h l sh (throw a) h' l' sh' E C M pc (Called (D#Cs)) v xa' vs frs I"
     by fact
    then have IH':
     "PROP ?P (C0∙sclinit([])) h l sh (Throw xa') h' l' sh' E C M pc (Called (D#Cs)) v xa' vs
       frs I"  using clinit xa' by simp
    have IH2: "PROP ?P (RI (D,throw a) ; Cs ← e') h' l' sh'' e1 h1 l1 sh1 E C M
      pc ics v xa' vs frs I" by fact
    have "P ⊢ (None,h,?frs,sh) -jvm→ (None,h,create_init_frame P C0 # ?frs',sh)" by(rule jvm_Called)
    also have "P ⊢ … -jvm→ (None,h',(vs, l, C, M, pc, Throwing (D#Cs) xa') # frs,sh'')"
      using IH' Jcc_pieces_RInit_clinit[OF assms(1-2) pcs,of h' l' sh'] RInitInitFail1.hyps(3,4)
        by simp
    also obtain vs'' where "P ⊢ … -jvm→ handle P C M xa' h1 (vs''@vs) l pc ics frs sh1"
      using IH2 pcs Jcc_pieces_RInit_RInit[OF assms(1) pcs] RInitInitFail1.hyps(3,4)
        xa' loc e1 xa' by clarsimp
    finally show ?thesis using pcs e1 clinit by auto
  next
    case throw: False
    then have eT: "e = Throw xa'" "h = h'" "l = l'" "sh = sh'" using xa' RInitInitFail1.prems(1)
      eval1_final_same[OF RInitInitFail1.hyps(1)] by clarsimp+
    obtain a' where "class P1 C0 = ⌊a'⌋" using RInitInitFail1.prems by(auto simp: is_class_def)
    then obtain stk' loc' M' pc' ics' where "create_init_frame P C0 = (stk',loc',C0,M',pc',ics')"
      using create_init_frame_wf_eq[OF wf] by(cases "create_init_frame P C0", simp)
    then obtain rhs err where pcs: "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh'' v xa'
       (RI (C0,e) ; D#Cs ← e') = (True, ?frsT xa', rhs, err)"
      using RInitInitFail1.prems(1) eT by clarsimp
    have IH2: "PROP ?P (RI (D,throw a) ; Cs ← e') h' l' sh'' e1 h1 l1 sh1 E C M
      pc ics v xa' vs frs I" by fact
    have "P ⊢ (None,h,?frsT xa',sh') -jvm→ (None,h,?frsT' xa',sh'(C0 ↦ (fst (the (sh' C0)), Error)))"
      by(rule jvm_Throwing)
    also obtain vs' where "P ⊢ ... -jvm→ handle P C M xa' h1 (vs'@vs) l pc ics frs sh1"
      using IH2 Jcc_pieces_RInit_RInit[OF assms(1) pcs] RInitInitFail1.hyps(3,4)
       eT e1 xa' by clarsimp
    finally show ?thesis using pcs e1 throw eT by auto
  qed
next
  case (RInitFailFinal1 e h l sh a h' l' sh' C0 sfs i sh'' e'')
  let ?frs = "(vs,l,C,M,pc,Called [C0]) # frs"
  let ?frs' = "(vs,l,C,M,pc,Called []) # frs"
  let "?frsT" = "λxa1. (vs,l,C,M,pc,Throwing [C0] xa1) # frs"
  let "?frsT'" = "λxa1. (vs,l,C,M,pc,Throwing [] xa1) # frs"
  obtain xa' where xa': "throw a = Throw xa'"
    by (metis RInitFailFinal1.hyps(1) eval1_final exp.distinct(101) final_def)
  show ?case
  proof(cases "e = C0∙sclinit([])")
    case clinit: True
    then obtain err where pcs: "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh'' v xa'
       (RI (C0,C0∙sclinit([])) ; [] ← unit) = (True, ?frs, (None, h', ?frs', sh''), err)"
      using RInitFailFinal1.prems(1) by clarsimp
    have IH: "PROP ?P e h l sh (throw a) h' l' sh' E C M pc (Called []) v xa' vs frs I" by fact
    then have IH':
     "PROP ?P (C0∙sclinit([])) h l sh (throw a) h' l' sh' E C M pc (Called []) v xa' vs frs I"
      using clinit by simp
    have "P ⊢ (None,h,?frs,sh) -jvm→ (None,h,create_init_frame P C0 # ?frs',sh)"
      by(rule jvm_Called)
    also have "P ⊢ … -jvm→ (None,h',?frsT' xa',sh'')"
      using IH' Jcc_pieces_RInit_clinit[OF assms(1-2) pcs,of h' l' sh'] xa'
        RInitFailFinal1.hyps(3,4) by simp
    also have
       "P ⊢ … -jvm→ handle (compP compMb2 P1) C M xa' h' vs l pc No_ics frs sh''"
      using RInitFailFinal1.hyps(3,4) jvm_RInit_throw[where h=h' and sh=sh''] by simp
    finally show ?thesis using xa' pcs clinit by(clarsimp intro!: exI[where x="[]"])
  next
    case throw: False
    then have eT: "e = Throw xa'" "h = h'" "sh = sh'" using xa' RInitFailFinal1.prems(1)
      eval1_final_same[OF RInitFailFinal1.hyps(1)] by clarsimp+
    obtain a where "class P1 C0 = ⌊a⌋" using RInitFailFinal1.prems by(auto simp: is_class_def)
    then obtain stk' loc' M' pc' ics' where "create_init_frame P C0 = (stk',loc',C0,M',pc',ics')"
      using create_init_frame_wf_eq[OF wf] by(cases "create_init_frame P C0", simp)
    then obtain rhs err where pcs: "Jcc_pieces P1 E C M h vs l pc ics frs sh I h' l' sh'' v xa'
       (RI (C0,e) ; [] ← unit) = (True, ?frsT xa', rhs, err)"
      using RInitFailFinal1.prems(1) eT by clarsimp
    have "P ⊢ (None,h,?frsT xa',sh) -jvm→ (None,h,?frsT' xa',sh(C0 ↦ (fst (the (sh C0)), Error)))"
      by(rule jvm_Throwing)
    also have "P ⊢ … -jvm→ handle P C M xa' h' vs l pc No_ics frs sh''"
      using RInitFailFinal1.hyps(3,4) jvm_RInit_throw[where h=h and sh=sh''] eT by simp
    finally show ?thesis using pcs xa' by(clarsimp intro!: exI[where x="[]"])
  qed
qed
(*>*)

(*FIXME move! *)
lemma atLeast0AtMost[simp]: "{0::nat..n} = {..n}"
by auto

lemma atLeast0LessThan[simp]: "{0::nat..<n} = {..<n}"
by auto

fun exception :: "'a exp ⇒ addr option" where
  "exception (Throw a) = Some a"
| "exception e = None"

lemma comp2_correct:
assumes wf: "wf_J1_prog P1"
    and "method": "P1 ⊢ C sees M,b:Ts→T = body in C"
    and eval:   "P1 ⊢1 ⟨body,(h,ls,sh)⟩ ⇒ ⟨e',(h',ls',sh')⟩"
    and nclinit: "M ≠ clinit"
shows "compP2 P1 ⊢ (None,h,[([],ls,C,M,0,No_ics)],sh) -jvm→ (exception e',h',[],sh')"
(*<*)
      (is "_ ⊢ ?σ0 -jvm→ ?σ1")
proof -
  let ?P = "compP2 P1"
  let ?E = "case b of Static ⇒ Ts | NonStatic ⇒ Class C#Ts"
  have nsub: "¬sub_RI body" using sees_wf1_nsub_RI[OF wf method] by simp
  have code: "?P,C,M,0 ⊳ compE2 body" using beforeM[OF "method"] by auto
  have xtab: "?P,C,M ⊳ compxE2 body 0 (size[])/{..<size(compE2 body)},size[]"
    using beforexM[OF "method"] by auto
  have cond: "Jcc_cond P1 ?E C M [] 0 No_ics {..<size(compE2 body)} h sh body"
    using nsub_RI_Jcc_pieces nsub code xtab by auto
  ― ‹Distinguish if e' is a value or an exception›
  { fix v assume [simp]: "e' = Val v"
    have "?P ⊢ ?σ0 -jvm→ (None,h',[([v],ls',C,M,size(compE2 body),No_ics)],sh')"
      using Jcc[OF wf eval cond] nsub_RI_Jcc_pieces[OF _ nsub] by auto
    also have "?P ⊢ … -jvm→ ?σ1" using beforeM[OF "method"] nclinit by auto
    finally have ?thesis .
  }
  moreover
  { fix a assume [simp]: "e' = Throw a"
    obtain pc vs' where pc: "0 ≤ pc ∧ pc < size(compE2 body) ∧
          ¬ caught ?P pc h' a (compxE2 body 0 0)"
    and 1: "?P ⊢ ?σ0 -jvm→ handle ?P C M a h' vs' ls' pc No_ics [] sh'"
      using Jcc[OF wf eval cond] nsub_RI_Jcc_pieces[OF _ nsub] by auto meson
    from pc have "handle ?P C M a h' vs' ls' pc No_ics [] sh' = ?σ1" using xtab "method" nclinit
      by(auto simp:handle_def compMb2_def)
    with 1 have ?thesis by simp
  } 
  ultimately show ?thesis using eval1_final[OF eval] by(auto simp:final_def)
qed
(*>*)

end