Theory Correctness2

(*  Title:      Jinja/Compiler/Correctness2.thy
    Author:     Tobias Nipkow
    Copyright   TUM 2003
*)

section ‹Correctness of Stage 2›

theory Correctness2
imports "HOL-Library.Sublist" Compiler2
begin

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

subsection‹Instruction sequences›

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

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

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

lemma [simp]: "P,C,M,pc ⊳ []"
(*<*)by(simp add:before_def)(*>*)


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

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


lemma [simp]: "P,C,M,pc ⊳ (is⇩1 @ is⇩2) = (P,C,M,pc ⊳ is⇩1 ∧ P,C,M,pc + size is⇩1 ⊳ is⇩2)"
(*<*)
by(subst add.commute)
  (fastforce simp add:before_def prefix_def drop_drop[symmetric])
(*>*)

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


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


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

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

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


subsection‹Exception tables›

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

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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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

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

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

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

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


lemma beforexD1: "P,C,M ⊳ xt / I,d ⟹ pcs xt ⊆ I"
(*<*)by(auto simp add:beforex_def)(*>*)


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


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


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


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


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


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


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


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


subsection‹The correctness proof›

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


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

lemma handle_Cons:
 "⟦ P,C,M ⊳ xt/I,d; d ≤ size vs; pc ∈ I;
    ∀x ∈ set xt. ¬ matches_ex_entry P (cname_of h xa) pc x ⟧ ⟹
  handle P C M xa h (v # vs) ls pc frs = handle P C M xa h vs ls pc frs"
(*<*)by(auto simp:handle_def Suc_diff_le dest: match_ex_table_SomeD2)(*>*)

lemma handle_append:
assumes bx: "P,C,M ⊳ xt/I,d" and d: "d ≤ size vs"
  and pcI: "pc ∈ I" and pc_not: "pc ∉ pcs xt"
shows "handle P C M xa h (ws @ vs) ls pc frs = handle P C M xa h vs ls pc frs"
(*<*)
proof -
  { fix pc' d'
    assume "match_ex_table P (cname_of h xa) pc (ex_table_of P C M) = ⌊(pc', d')⌋"
    then have "length ws ≤ length ws + length vs - d'"
      using assms by(fastforce dest:match_ex_table_SomeD2 split:nat_diff_split)
  }
  then show ?thesis by(simp add: handle_def)
qed
(*>*)


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


lemma fixes P⇩1 defines [simp]: "P ≡ compP⇩2 P⇩1"
shows Jcc:
  "P⇩1 ⊢⇩1 ⟨e,(h⇩0,ls⇩0)⟩ ⇒ ⟨ef,(h⇩1,ls⇩1)⟩ ⟹
  (⋀C M pc v xa vs frs I.
     ⟦ P,C,M,pc ⊳ compE⇩2 e; P,C,M ⊳ compxE⇩2 e pc (size vs)/I,size vs;
       {pc..<pc+size(compE⇩2 e)} ⊆ I ⟧ ⟹
     (ef = Val v ⟶
      P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
            (None,h⇩1,(v#vs,ls⇩1,C,M,pc+size(compE⇩2 e))#frs))
     ∧
     (ef = Throw xa ⟶
      (∃pc⇩1. pc ≤ pc⇩1 ∧ pc⇩1 < pc + size(compE⇩2 e) ∧
               ¬ caught P pc⇩1 h⇩1 xa (compxE⇩2 e pc (size vs)) ∧
               P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→ handle P C M xa h⇩1 vs ls⇩1 pc⇩1 frs)))"
(*<*)
  (is "_ ⟹ (⋀C M pc v xa vs frs I.
                  PROP ?P e h⇩0 ls⇩0 ef h⇩1 ls⇩1 C M pc v xa vs frs I)")
(*>*)

and "P⇩1 ⊢⇩1 ⟨es,(h⇩0,ls⇩0)⟩ [⇒] ⟨fs,(h⇩1,ls⇩1)⟩ ⟹
    (⋀C M pc ws xa es' vs frs I.
      ⟦ P,C,M,pc ⊳ compEs⇩2 es; P,C,M ⊳ compxEs⇩2 es pc (size vs)/I,size vs;
       {pc..<pc+size(compEs⇩2 es)} ⊆ I ⟧ ⟹
      (fs = map Val ws ⟶
       P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
             (None,h⇩1,(rev ws @ vs,ls⇩1,C,M,pc+size(compEs⇩2 es))#frs))
      ∧
      (fs = map Val ws @ Throw xa # es' ⟶
       (∃pc⇩1. pc ≤ pc⇩1 ∧ pc⇩1 < pc + size(compEs⇩2 es) ∧
                ¬ caught P pc⇩1 h⇩1 xa (compxEs⇩2 es pc (size vs)) ∧
                P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→ handle P C M xa h⇩1 vs ls⇩1 pc⇩1 frs)))"
(*<*)
  (is "_ ⟹ (⋀C M pc ws xa es' vs frs I.
                  PROP ?Ps es h⇩0 ls⇩0 fs h⇩1 ls⇩1 C M pc ws xa es' vs frs I)")
proof (induct rule:eval⇩1_evals⇩1_inducts)
  case New⇩1 thus ?case by (clarsimp simp add:blank_def fun_eq_iff)
next
  case NewFail⇩1 thus ?case by(auto simp: handle_def pcs_def)
next
  case (Cast⇩1 e h⇩0 ls⇩0 a h⇩1 ls⇩1 D fs C')
  let ?pc = "pc + length(compE⇩2 e)"
  have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
             (None,h⇩1,(Addr a#vs,ls⇩1,C,M,?pc)#frs)" using Cast⇩1 by fastforce
  also have "P ⊢ … -jvm→ (None,h⇩1,(Addr a#vs,ls⇩1,C,M,?pc+1)#frs)"
    using Cast⇩1 by (auto simp add:cast_ok_def)
  finally show ?case by auto
next
  case (CastNull⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 C')
  let ?pc = "pc + length(compE⇩2 e)"
  have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
            (None,h⇩1,(Null#vs,ls⇩1,C,M,?pc)#frs)"
    using CastNull⇩1 by fastforce
  also have "P ⊢ … -jvm→ (None,h⇩1,(Null#vs,ls⇩1,C,M,?pc+1)#frs)"
    using CastNull⇩1 by (auto simp add:cast_ok_def)
  finally show ?case by auto
next
  case (CastFail⇩1 e h⇩0 ls⇩0 a h⇩1 ls⇩1 D fs C')
  let ?pc = "pc + length(compE⇩2 e)"
  let ?xa = "addr_of_sys_xcpt ClassCast"
  have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
             (None,h⇩1,(Addr a#vs,ls⇩1,C,M,?pc)#frs)"
    using CastFail⇩1 by fastforce
  also have "P ⊢ … -jvm→ handle P C M ?xa h⇩1 (Addr a#vs) ls⇩1 ?pc frs"
    using CastFail⇩1 by (auto simp add:handle_def cast_ok_def)
  also have "handle P C M ?xa h⇩1 (Addr a#vs) ls⇩1 ?pc frs =
             handle P C M ?xa h⇩1 vs ls⇩1 ?pc frs"
    using CastFail⇩1.prems by(auto simp:handle_Cons)
  finally have exec: "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→ …".
  show ?case (is "?N ∧ (?eq ⟶ (∃pc⇩1. ?H pc⇩1))")
  proof
    show ?N by simp
  next
    have "?eq ⟶ ?H ?pc" using exec by auto
    thus "?eq ⟶ (∃pc⇩1. ?H pc⇩1)" by blast
  qed
next
  case CastThrow⇩1 thus ?case by fastforce
next
  case Val⇩1 thus ?case by simp
next
  case Var⇩1 thus ?case by auto
next
  case (BinOp⇩1 e⇩1 h⇩0 ls⇩0 v⇩1 h⇩1 ls⇩1 e⇩2 v⇩2 h⇩2 ls⇩2 bop w)
  let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
  let ?pc⇩2 = "?pc⇩1 + length(compE⇩2 e⇩2)"
  have IH⇩2: "PROP ?P e⇩2 h⇩1 ls⇩1 (Val v⇩2) h⇩2 ls⇩2 C M ?pc⇩1 v⇩2 xa (v⇩1#vs) frs
                     (I - pcs(compxE⇩2 e⇩1 pc (size vs)))" by fact
  have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
             (None,h⇩1,(v⇩1#vs,ls⇩1,C,M,?pc⇩1)#frs)" using BinOp⇩1 by fastforce
  also have "P ⊢ … -jvm→ (None,h⇩2,(v⇩2#v⇩1#vs,ls⇩2,C,M,?pc⇩2)#frs)"
    using BinOp⇩1.prems IH⇩2 by fastforce
  also have "P ⊢ … -jvm→ (None,h⇩2,(w#vs,ls⇩2,C,M,?pc⇩2+1)#frs)"
    using BinOp⇩1 by(cases bop) auto
  finally show ?case by (auto split: bop.splits simp:add.assoc)
next
  case BinOpThrow⇩1⇩1 thus ?case by(fastforce)
next
  case (BinOpThrow⇩2⇩1 e⇩1 h⇩0 ls⇩0 v⇩1 h⇩1 ls⇩1 e⇩2 e h⇩2 ls⇩2 bop)
  let ?pc = "pc + length(compE⇩2 e⇩1)"
  let ?σ⇩1 = "(None,h⇩1,(v⇩1#vs,ls⇩1,C,M,?pc)#frs)"
  have 1: "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→ ?σ⇩1"
    using BinOpThrow⇩2⇩1 by fastforce
  show ?case (is "?N ∧ (?eq ⟶ (∃pc⇩2. ?H pc⇩2))")
  proof
    show ?N by simp
  next
    { assume ?eq
      moreover
      have "PROP ?P e⇩2 h⇩1 ls⇩1 (throw e) h⇩2 ls⇩2 C M ?pc v xa (v⇩1#vs) frs
                     (I - pcs(compxE⇩2 e⇩1 pc (size vs)))" by fact
      ultimately obtain pc⇩2 where
        pc⇩2: "?pc ≤ pc⇩2 ∧ pc⇩2 < ?pc + size(compE⇩2 e⇩2) ∧
              ¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 e⇩2 ?pc (size vs + 1))" and
        2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 (v⇩1#vs) ls⇩2 pc⇩2 frs"
        using BinOpThrow⇩2⇩1.prems by fastforce
      have 3: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
        using 2 BinOpThrow⇩2⇩1.prems pc⇩2 by(auto simp:handle_Cons)
      have "?H pc⇩2" using pc⇩2 jvm_trans[OF 1 3] by auto
      hence "∃pc⇩2. ?H pc⇩2" by iprover
    }
    thus "?eq ⟶ (∃pc⇩2. ?H pc⇩2)" by iprover
  qed
next
  case (FAcc⇩1 e h⇩0 ls⇩0 a h⇩1 ls⇩1 C fs F D w)
  let ?pc = "pc + length(compE⇩2 e)"
  have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
             (None,h⇩1,(Addr a#vs,ls⇩1,C,M,?pc)#frs)" using FAcc⇩1 by fastforce
  also have "P ⊢ … -jvm→ (None,h⇩1,(w#vs,ls⇩1,C,M,?pc+1)#frs)"
    using FAcc⇩1 by auto
  finally show ?case by auto
next
  case (FAccNull⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 F D)
  let ?pc = "pc + length(compE⇩2 e)"
  let ?xa = "addr_of_sys_xcpt NullPointer"
  have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
             (None,h⇩1,(Null#vs,ls⇩1,C,M,?pc)#frs)" using FAccNull⇩1 by fastforce
  also have "P ⊢ … -jvm→ handle P C M ?xa h⇩1 (Null#vs) ls⇩1 ?pc frs"
    using FAccNull⇩1.prems
    by(fastforce simp:split_beta handle_def simp del: split_paired_Ex)
  also have "handle P C M ?xa h⇩1 (Null#vs) ls⇩1 ?pc frs =
             handle P C M ?xa h⇩1 vs ls⇩1 ?pc frs"
    using FAccNull⇩1.prems by(auto simp add:handle_Cons)
  finally show ?case by (auto intro: exI[where x = ?pc])
next
  case FAccThrow⇩1 thus ?case by fastforce
next
  case (LAss⇩1 e h⇩0 ls⇩0 w h⇩1 ls⇩1 i ls⇩2)
  let ?pc = "pc + length(compE⇩2 e)"
  have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
             (None,h⇩1,(w#vs,ls⇩1,C,M,?pc)#frs)" using LAss⇩1 by fastforce
  also have "P ⊢ … -jvm→ (None,h⇩1,(Unit#vs,ls⇩2,C,M,?pc+2)#frs)"
    using LAss⇩1 by auto
  finally show ?case using LAss⇩1 by auto
next
  case LAssThrow⇩1 thus ?case by fastforce
next
  case (FAss⇩1 e⇩1 h⇩0 ls⇩0 a h⇩1 ls⇩1 e⇩2 w h⇩2 ls⇩2 C fs fs' F D h⇩2')
  let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
  let ?pc⇩2 = "?pc⇩1 + length(compE⇩2 e⇩2)"
  have IH⇩2: "PROP ?P e⇩2 h⇩1 ls⇩1 (Val w) h⇩2 ls⇩2 C M ?pc⇩1 w xa (Addr a#vs) frs
                     (I - pcs(compxE⇩2 e⇩1 pc (size vs)))" by fact
  have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
             (None,h⇩1,(Addr a#vs,ls⇩1,C,M,?pc⇩1)#frs)" using FAss⇩1 by fastforce
  also have "P ⊢ … -jvm→ (None,h⇩2,(w#Addr a#vs,ls⇩2,C,M,?pc⇩2)#frs)"
    using FAss⇩1.prems IH⇩2 by fastforce
  also have "P ⊢ … -jvm→ (None,h⇩2',(Unit#vs,ls⇩2,C,M,?pc⇩2+2)#frs)"
    using FAss⇩1 by auto
  finally show ?case using FAss⇩1 by (auto simp:add.assoc)
next
  case (FAssNull⇩1 e⇩1 h⇩0 ls⇩0 h⇩1 ls⇩1 e⇩2 w h⇩2 ls⇩2 F D)
  let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
  let ?pc⇩2 = "?pc⇩1 + length(compE⇩2 e⇩2)"
  let ?xa = "addr_of_sys_xcpt NullPointer"
  have IH⇩2: "PROP ?P e⇩2 h⇩1 ls⇩1 (Val w) h⇩2 ls⇩2 C M ?pc⇩1 w xa (Null#vs) frs
                     (I - pcs(compxE⇩2 e⇩1 pc (size vs)))" by fact
  have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
             (None,h⇩1,(Null#vs,ls⇩1,C,M,?pc⇩1)#frs)" using FAssNull⇩1 by fastforce
  also have "P ⊢ … -jvm→ (None,h⇩2,(w#Null#vs,ls⇩2,C,M,?pc⇩2)#frs)"
    using FAssNull⇩1.prems IH⇩2 by fastforce
  also have "P ⊢ … -jvm→ handle P C M ?xa h⇩2 (w#Null#vs) ls⇩2 ?pc⇩2 frs"
    using FAssNull⇩1.prems
    by(fastforce simp:split_beta handle_def simp del: split_paired_Ex)
  also have "handle P C M ?xa h⇩2 (w#Null#vs) ls⇩2 ?pc⇩2 frs =
             handle P C M ?xa h⇩2 vs ls⇩2 ?pc⇩2 frs"
    using FAssNull⇩1.prems by(auto simp add:handle_Cons)
  finally show ?case by (auto intro: exI[where x = ?pc⇩2])
next
  case (FAssThrow⇩2⇩1 e⇩1 h⇩0 ls⇩0 w h⇩1 ls⇩1 e⇩2 e' h⇩2 ls⇩2 F D)
  let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
  let ?σ⇩1 = "(None,h⇩1,(w#vs,ls⇩1,C,M,?pc⇩1)#frs)"
  have 1: "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→ ?σ⇩1"
    using FAssThrow⇩2⇩1 by fastforce
  show ?case (is "?N ∧ (?eq ⟶ (∃pc⇩2. ?H pc⇩2))")
  proof
    show ?N by simp
  next
    { assume ?eq
      moreover
      have "PROP ?P e⇩2 h⇩1 ls⇩1 (throw e') h⇩2 ls⇩2 C M ?pc⇩1 v xa (w#vs) frs
                    (I - pcs (compxE⇩2 e⇩1 pc (length vs)))" by fact
      ultimately obtain pc⇩2 where
        pc⇩2: "?pc⇩1 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩1 + size(compE⇩2 e⇩2) ∧
              ¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 e⇩2 ?pc⇩1 (size vs + 1))" and
        2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 (w#vs) ls⇩2 pc⇩2 frs"
        using FAssThrow⇩2⇩1.prems by fastforce
      have 3: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
        using 2 FAssThrow⇩2⇩1.prems pc⇩2 by(auto simp:handle_Cons)
      have "?H pc⇩2" using pc⇩2 jvm_trans[OF 1 3] by auto
      hence "∃pc⇩2. ?H pc⇩2" by iprover
    }
    thus "?eq ⟶ (∃pc⇩2. ?H pc⇩2)" by iprover
  qed
next
  case FAssThrow⇩1⇩1 thus ?case by fastforce
next
  case (Call⇩1 e h⇩0 ls⇩0 a h⇩1 ls⇩1 es pvs h⇩2 ls⇩2 Ca fs M' Ts T body D ls⇩2' f h⇩3 ls⇩3)
  have "P⇩1 ⊢⇩1 ⟨es,(h⇩1, ls⇩1)⟩ [⇒] ⟨map Val pvs,(h⇩2, ls⇩2)⟩" by fact
  hence [simp]: "length es = length pvs" by(auto dest:evals⇩1_preserves_elen)
  let ?σ⇩0 = "(None,h⇩0,(vs, ls⇩0, C,M,pc)#frs)"
  let ?pc⇩1 = "pc + length(compE⇩2 e)"
  let ?σ⇩1 = "(None,h⇩1,(Addr a # vs, ls⇩1, C,M,?pc⇩1)#frs)"
  let ?pc⇩2 = "?pc⇩1 + length(compEs⇩2 es)"
  let ?frs⇩2 = "(rev pvs @ Addr a # vs, ls⇩2, C,M,?pc⇩2)#frs"
  let ?σ⇩2 = "(None,h⇩2,?frs⇩2)"
  let ?frs⇩2' = "([], ls⇩2', D,M',0) # ?frs⇩2"
  let ?σ⇩2' = "(None, h⇩2, ?frs⇩2')"
  have IH_es: "PROP ?Ps es h⇩1 ls⇩1 (map Val pvs) h⇩2 ls⇩2 C M ?pc⇩1 pvs xa
                    (map Val pvs) (Addr a # vs) frs (I - pcs(compxE⇩2 e pc (size vs)))" by fact
  have "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1" using Call⇩1 by fastforce
  also have "P ⊢ … -jvm→ ?σ⇩2" using IH_es Call⇩1.prems by fastforce
  also have "P ⊢ … -jvm→ ?σ⇩2'"
    using Call⇩1 by(auto simp add: nth_append compMb⇩2_def)
  finally have 1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩2'".
  have "P⇩1 ⊢ Ca sees M': Ts→T = body in D" by fact
  then have M'_in_D: "P⇩1 ⊢ D sees M': Ts→T = body in D"
    by(rule sees_method_idemp) 
  hence M'_code: "compP⇩2 P⇩1,D,M',0 ⊳ compE⇩2 body @ [Return]"
    and M'_xtab: "compP⇩2 P⇩1,D,M' ⊳ compxE⇩2 body 0 0/{..<size(compE⇩2 body)},0"
    by(rule beforeM, rule beforexM)
  have IH_body: "PROP ?P body h⇩2 ls⇩2' f h⇩3 ls⇩3 D M' 0 v xa [] ?frs⇩2 ({..<size(compE⇩2 body)})" by fact
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val ⟶ ?trans")
    proof
      assume val: ?val
      note 1
      also have "P ⊢ ?σ⇩2' -jvm→
                     (None,h⇩3,([v],ls⇩3,D,M',size(compE⇩2 body))#?frs⇩2)"
        using val IH_body Call⇩1.prems M'_code M'_xtab
        by (fastforce simp del:split_paired_Ex)
      also have "P ⊢ … -jvm→ (None, h⇩3, (v # vs, ls⇩2, C,M,?pc⇩2+1)#frs)"
        using Call⇩1 M'_code M'_in_D by(auto simp: nth_append compMb⇩2_def)
      finally show ?trans by(simp add:add.assoc)
    qed
  next
    show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
    proof
      assume throw: ?throw
      with IH_body obtain pc⇩2 where
        pc⇩2: "0 ≤ pc⇩2 ∧ pc⇩2 < size(compE⇩2 body) ∧
              ¬ caught P pc⇩2 h⇩3 xa (compxE⇩2 body 0 0)" and
        2: "P ⊢ ?σ⇩2' -jvm→ handle P D M' xa h⇩3 [] ls⇩3 pc⇩2 ?frs⇩2"
        using Call⇩1.prems M'_code M'_xtab
        by (fastforce simp del:split_paired_Ex)
      have "handle P D M' xa h⇩3 [] ls⇩3 pc⇩2 ?frs⇩2 =
            handle P C M xa h⇩3 (rev pvs @ Addr a # vs) ls⇩2 ?pc⇩2 frs"
        using pc⇩2 M'_in_D by(auto simp add:handle_def)
      also have "… = handle P C M xa h⇩3 vs ls⇩2 ?pc⇩2 frs"
        using Call⇩1.prems by(auto simp add:handle_append handle_Cons)
      finally have "?H ?pc⇩2" using pc⇩2 jvm_trans[OF 1 2] by auto
      thus "∃pc⇩2. ?H pc⇩2" by iprover
    qed
  qed
next
  case (CallParamsThrow⇩1 e h⇩0 ls⇩0 w h⇩1 ls⇩1 es es' h⇩2 ls⇩2 pvs ex es'' M')
  let ?σ⇩0 = "(None,h⇩0,(vs, ls⇩0, C,M,pc)#frs)"
  let ?pc⇩1 = "pc + length(compE⇩2 e)"
  let ?σ⇩1 = "(None,h⇩1,(w # vs, ls⇩1, C,M,?pc⇩1)#frs)"
  let ?pc⇩2 = "?pc⇩1 + length(compEs⇩2 es)"
  have 1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1" using CallParamsThrow⇩1 by fastforce
  show ?case (is "?N ∧ (?eq ⟶ (∃pc⇩2. ?H pc⇩2))")
  proof
    show ?N by simp
  next
    { assume ?eq
      moreover
      have "PROP ?Ps es h⇩1 ls⇩1 es' h⇩2 ls⇩2 C M ?pc⇩1 pvs xa es'' (w#vs) frs
        (I - pcs (compxE⇩2 e pc (length vs)))" by fact
      ultimately have "∃pc⇩2.
        (?pc⇩1 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩1 + size(compEs⇩2 es) ∧
         ¬ caught P pc⇩2 h⇩2 xa (compxEs⇩2 es ?pc⇩1 (size vs + 1))) ∧
        P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 (w#vs) ls⇩2 pc⇩2 frs"
        (is "∃pc⇩2. ?PC pc⇩2 ∧ ?Exec pc⇩2")
        using CallParamsThrow⇩1 by force
      then obtain pc⇩2 where pc⇩2: "?PC pc⇩2" and 2: "?Exec pc⇩2" by iprover
      have "?H pc⇩2" using pc⇩2 jvm_trans[OF 1 2] CallParamsThrow⇩1
        by(auto simp:handle_Cons)
      hence "∃pc⇩2. ?H pc⇩2" by iprover
    }
    thus "?eq ⟶ (∃pc⇩2. ?H pc⇩2)" by iprover
  qed
next
  case (CallNull⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 es pvs h⇩2 ls⇩2 M')
  have "P⇩1 ⊢⇩1 ⟨es,(h⇩1, ls⇩1)⟩ [⇒] ⟨map Val pvs,(h⇩2, ls⇩2)⟩" by fact
  hence [simp]: "length es = length pvs" by(auto dest:evals⇩1_preserves_elen)
  let ?pc⇩1 = "pc + length(compE⇩2 e)"
  let ?pc⇩2 = "?pc⇩1 + length(compEs⇩2 es)"
  let ?xa = "addr_of_sys_xcpt NullPointer"
  have IH_es: "PROP ?Ps es h⇩1 ls⇩1 (map Val pvs) h⇩2 ls⇩2 C M ?pc⇩1 pvs xa
                    (map Val pvs) (Null#vs) frs (I - pcs(compxE⇩2 e pc (size vs)))" by fact
  have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
             (None,h⇩1,(Null#vs,ls⇩1,C,M,?pc⇩1)#frs)" using CallNull⇩1 by fastforce
  also have "P ⊢ … -jvm→ (None,h⇩2,(rev pvs@Null#vs,ls⇩2,C,M,?pc⇩2)#frs)"
    using CallNull⇩1 IH_es by fastforce
  also have "P ⊢ … -jvm→ handle P C M ?xa h⇩2 (rev pvs@Null#vs) ls⇩2 ?pc⇩2 frs"
    using CallNull⇩1.prems
    by(auto simp:split_beta handle_def nth_append simp del: split_paired_Ex)
  also have "handle P C M ?xa h⇩2 (rev pvs@Null#vs) ls⇩2 ?pc⇩2 frs =
             handle P C M ?xa h⇩2 vs ls⇩2 ?pc⇩2 frs"
    using CallNull⇩1.prems by(auto simp:handle_Cons handle_append)
  finally show ?case by (auto intro: exI[where x = ?pc⇩2])
next
  case CallObjThrow⇩1 thus ?case by fastforce
next
  case Block⇩1 thus ?case by auto
next
  case (Seq⇩1 e⇩1 h⇩0 ls⇩0 w h⇩1 ls⇩1 e⇩2 e⇩2' h⇩2 ls⇩2)
  let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
  let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
  let ?σ⇩1 = "(None,h⇩1,(vs,ls⇩1,C,M,?pc⇩1+1)#frs)"
  have "P ⊢ ?σ⇩0 -jvm→ (None,h⇩1,(w#vs,ls⇩1,C,M,?pc⇩1)#frs)"
    using Seq⇩1 by fastforce
  also have "P ⊢ … -jvm→ ?σ⇩1" using Seq⇩1 by auto
  finally have eval⇩1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1".
  let ?pc⇩2 = "?pc⇩1 + 1 + length(compE⇩2 e⇩2)"
  have IH⇩2: "PROP ?P e⇩2 h⇩1 ls⇩1 e⇩2' h⇩2 ls⇩2 C M (?pc⇩1+1) v xa vs frs
                     (I - pcs(compxE⇩2 e⇩1 pc (size vs)))" by fact
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val ⟶ ?trans")
    proof
      assume val: ?val
      note eval⇩1
      also have "P ⊢ ?σ⇩1 -jvm→ (None,h⇩2,(v#vs,ls⇩2,C,M,?pc⇩2)#frs)"
        using val Seq⇩1.prems IH⇩2 by fastforce
      finally show ?trans by(simp add:add.assoc)
    qed
  next
    show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
    proof
      assume throw: ?throw
      then obtain pc⇩2 where
        pc⇩2: "?pc⇩1+1 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩2 ∧
              ¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 e⇩2 (?pc⇩1+1) (size vs))" and
        eval⇩2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
        using IH⇩2 Seq⇩1.prems by fastforce
      have "?H pc⇩2" using pc⇩2 jvm_trans[OF eval⇩1 eval⇩2] by auto
      thus "∃pc⇩2. ?H pc⇩2" by iprover
    qed
  qed
next
  case SeqThrow⇩1 thus ?case by fastforce
next
  case (CondT⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 e⇩1 e' h⇩2 ls⇩2 e⇩2)
  let ?pc⇩1 = "pc + length(compE⇩2 e)"
  let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
  let ?σ⇩1 = "(None,h⇩1,(vs,ls⇩1,C,M,?pc⇩1+1)#frs)"
  have "P ⊢ ?σ⇩0 -jvm→ (None,h⇩1,(Bool(True)#vs,ls⇩1,C,M,?pc⇩1)#frs)"
    using CondT⇩1 by (fastforce simp add: Int_Un_distrib)
  also have "P ⊢ … -jvm→ ?σ⇩1" using CondT⇩1 by auto
  finally have eval⇩1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1".
  let ?pc⇩1' = "?pc⇩1 + 1 + length(compE⇩2 e⇩1)"
  let ?pc⇩2' = "?pc⇩1' + 1 + length(compE⇩2 e⇩2)"
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val ⟶ ?trans")
    proof
      assume val: ?val
      note eval⇩1
      also have "P ⊢ ?σ⇩1 -jvm→ (None,h⇩2,(v#vs,ls⇩2,C,M,?pc⇩1')#frs)"
        using val CondT⇩1 by(fastforce simp:Int_Un_distrib)
      also have "P ⊢ … -jvm→ (None,h⇩2,(v#vs,ls⇩2,C,M,?pc⇩2')#frs)"
        using CondT⇩1 by(auto simp:add.assoc)
      finally show ?trans by(simp add:add.assoc)
    qed
  next
    show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
    proof
      let ?d = "size vs"
      let ?I = "I - pcs(compxE⇩2 e pc ?d) - pcs(compxE⇩2 e⇩2 (?pc⇩1'+1) ?d)"
      assume throw: ?throw
      moreover
      have "PROP ?P e⇩1 h⇩1 ls⇩1 e' h⇩2 ls⇩2 C M (?pc⇩1+1) v xa vs frs ?I" by fact
      ultimately obtain pc⇩2 where
        pc⇩2: "?pc⇩1+1 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩1' ∧
              ¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 e⇩1 (?pc⇩1+1) (size vs))" and
        eval⇩2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
        using CondT⇩1.prems by (fastforce simp:Int_Un_distrib)
      have "?H pc⇩2" using pc⇩2 jvm_trans[OF eval⇩1 eval⇩2] by auto
      thus "∃pc⇩2. ?H pc⇩2" by iprover
    qed
  qed
next
  case (CondF⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 e⇩2 e' h⇩2 ls⇩2 e⇩1)
  let ?pc⇩1 = "pc + length(compE⇩2 e)"
  let ?pc⇩2 = "?pc⇩1 + 1 + length(compE⇩2 e⇩1)+ 1"
  let ?pc⇩2' = "?pc⇩2 + length(compE⇩2 e⇩2)"
  let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
  let ?σ⇩1 = "(None,h⇩1,(vs,ls⇩1,C,M,?pc⇩2)#frs)"
  have "P ⊢ ?σ⇩0 -jvm→ (None,h⇩1,(Bool(False)#vs,ls⇩1,C,M,?pc⇩1)#frs)"
    using CondF⇩1 by (fastforce simp add: Int_Un_distrib)
  also have "P ⊢ … -jvm→ ?σ⇩1" using CondF⇩1 by auto
  finally have eval⇩1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1".
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val ⟶ ?trans")
    proof
      assume val: ?val
      note eval⇩1
      also have "P ⊢ ?σ⇩1 -jvm→ (None,h⇩2,(v#vs,ls⇩2,C,M,?pc⇩2')#frs)"
        using val CondF⇩1 by(fastforce simp:Int_Un_distrib)
      finally show ?trans by(simp add:add.assoc)
    qed
  next
    show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
    proof
      let ?d = "size vs"
      let ?I = "I - pcs(compxE⇩2 e pc ?d) - pcs(compxE⇩2 e⇩1 (?pc⇩1+1) ?d)"
      assume throw: ?throw
      moreover
      have "PROP ?P e⇩2 h⇩1 ls⇩1 e' h⇩2 ls⇩2 C M ?pc⇩2 v xa vs frs ?I" by fact
      ultimately obtain pc⇩2 where
        pc⇩2: "?pc⇩2 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩2' ∧
              ¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 e⇩2 ?pc⇩2 ?d)" and
        eval⇩2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
        using CondF⇩1.prems by(fastforce simp:Int_Un_distrib)
      have "?H pc⇩2" using pc⇩2 jvm_trans[OF eval⇩1 eval⇩2] by auto
      thus "∃pc⇩2. ?H pc⇩2" by iprover
    qed
  qed
next
  case (CondThrow⇩1 e h⇩0 ls⇩0 f h⇩1 ls⇩1 e⇩1 e⇩2)
  let ?d = "size vs"
  let ?xt⇩1 = "compxE⇩2 e⇩1 (pc+size(compE⇩2 e)+1) ?d"
  let ?xt⇩2 = "compxE⇩2 e⇩2 (pc+size(compE⇩2 e)+size(compE⇩2 e⇩1)+2) ?d"
  let ?I = "I - (pcs ?xt⇩1 ∪ pcs ?xt⇩2)"
  have "pcs(compxE⇩2 e pc ?d) ∩ pcs(?xt⇩1 @ ?xt⇩2) = {}"
    using CondThrow⇩1.prems by (simp add:Int_Un_distrib)
  moreover have "PROP ?P e h⇩0 ls⇩0 (throw f) h⇩1 ls⇩1 C M pc v xa vs frs ?I" by fact
  ultimately show ?case using CondThrow⇩1.prems by fastforce
next
  case (WhileF⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 c)
  let ?pc = "pc + length(compE⇩2 e)"
  let ?pc' = "?pc + length(compE⇩2 c) + 3"
  have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
            (None,h⇩1,(Bool False#vs,ls⇩1,C,M,?pc)#frs)"
    using WhileF⇩1 by fastforce
  also have "P ⊢ … -jvm→ (None,h⇩1,(vs,ls⇩1,C,M,?pc')#frs)"
    using WhileF⇩1 by (auto simp:add.assoc)
  also have "P ⊢ … -jvm→ (None,h⇩1,(Unit#vs,ls⇩1,C,M,?pc'+1)#frs)"
    using WhileF⇩1.prems by (auto simp:eval_nat_numeral)
  finally show ?case by (simp add:add.assoc eval_nat_numeral)
next
  case (WhileT⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 c v⇩1 h⇩2 ls⇩2 e⇩3 h⇩3 ls⇩3)
  let ?pc = "pc + length(compE⇩2 e)"
  let ?pc' = "?pc + length(compE⇩2 c) + 1"
  let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
  let ?σ⇩2 = "(None,h⇩2,(vs,ls⇩2,C,M,pc)#frs)"
  have "P ⊢ ?σ⇩0 -jvm→ (None,h⇩1,(Bool True#vs,ls⇩1,C,M,?pc)#frs)"
    using WhileT⇩1 by fastforce
  also have "P ⊢ … -jvm→ (None,h⇩1,(vs,ls⇩1,C,M,?pc+1)#frs)"
    using WhileT⇩1.prems by auto
  also have "P ⊢ … -jvm→ (None,h⇩2,(v⇩1#vs,ls⇩2,C,M,?pc')#frs)"
    using WhileT⇩1 by(fastforce)
  also have "P ⊢ … -jvm→ ?σ⇩2" using WhileT⇩1.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,h⇩3,(v#vs,ls⇩3,C,M,?pc'+3)#frs)"
        using val WhileT⇩1 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 ⟶ (∃pc⇩2. ?H pc⇩2)")
    proof
      assume throw: ?throw
      moreover
      have "PROP ?P (while (e) c) h⇩2 ls⇩2 e⇩3 h⇩3 ls⇩3 C M pc v xa vs frs I" by fact
      ultimately obtain pc⇩2 where
        pc⇩2: "pc ≤ pc⇩2 ∧ pc⇩2 < ?pc'+3 ∧
              ¬ caught P pc⇩2 h⇩3 xa (compxE⇩2 (while (e) c) pc (size vs))" and
        2: "P ⊢ ?σ⇩2 -jvm→ handle P C M xa h⇩3 vs ls⇩3 pc⇩2 frs"
        using WhileT⇩1.prems by (auto simp:add.assoc eval_nat_numeral)
      have "?H pc⇩2" using pc⇩2 jvm_trans[OF 1 2] by auto
      thus "∃pc⇩2. ?H pc⇩2" by iprover
    qed
  qed
next
  case WhileCondThrow⇩1 thus ?case by fastforce
next
  case (WhileBodyThrow⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 c e' h⇩2 ls⇩2)
  let ?pc⇩1 = "pc + length(compE⇩2 e)"
  let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
  let ?σ⇩1 = "(None,h⇩1,(vs,ls⇩1,C,M,?pc⇩1+1)#frs)"
  have "P ⊢ ?σ⇩0 -jvm→ (None,h⇩1,(Bool(True)#vs,ls⇩1,C,M,?pc⇩1)#frs)"
    using WhileBodyThrow⇩1 by (fastforce simp add: Int_Un_distrib)
  also have "P ⊢ … -jvm→ ?σ⇩1" using  WhileBodyThrow⇩1 by auto
  finally have eval⇩1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1".
  let ?pc⇩1' = "?pc⇩1 + 1 + length(compE⇩2 c)"
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm by simp
  next
    show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
    proof
      assume throw: ?throw
      moreover
      have "PROP ?P c h⇩1 ls⇩1 (throw e') h⇩2 ls⇩2 C M (?pc⇩1+1) v xa vs frs
                    (I - pcs (compxE⇩2 e pc (size vs)))" by fact
      ultimately obtain pc⇩2 where
        pc⇩2: "?pc⇩1+1 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩1' ∧
              ¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 c (?pc⇩1+1) (size vs))" and
        eval⇩2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
        using WhileBodyThrow⇩1.prems by (fastforce simp:Int_Un_distrib)
      have "?H pc⇩2" using pc⇩2 jvm_trans[OF eval⇩1 eval⇩2] by auto
      thus "∃pc⇩2. ?H pc⇩2" by iprover
    qed
  qed
next
  case (Throw⇩1 e h⇩0 ls⇩0 a h⇩1 ls⇩1)
  let ?pc = "pc + size(compE⇩2 e)"
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm by simp
  next
    show ?Err (is "?throw ⟶ (∃pc⇩1. ?H pc⇩1)")
    proof
      assume ?throw
      hence "P ⊢ (None, h⇩0, (vs, ls⇩0, C, M, pc) # frs) -jvm→
                 (None, h⇩1, (Addr xa#vs, ls⇩1, C, M, ?pc) # frs)"
        using Throw⇩1 by fastforce
      also have "P ⊢ … -jvm→ handle P C M xa h⇩1 (Addr xa#vs) ls⇩1 ?pc frs"
        using Throw⇩1.prems by(auto simp add:handle_def)
      also have "handle P C M xa h⇩1 (Addr xa#vs) ls⇩1 ?pc frs =
                 handle P C M xa h⇩1 vs ls⇩1 ?pc frs"
        using Throw⇩1.prems by(auto simp add:handle_Cons)
      finally have "?H ?pc" by simp
      thus "∃pc⇩1. ?H pc⇩1" by iprover
    qed
  qed
next
  case (ThrowNull⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1)
  let ?pc = "pc + size(compE⇩2 e)"
  let ?xa = "addr_of_sys_xcpt NullPointer"
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm by simp
  next
    show ?Err (is "?throw ⟶ (∃pc⇩1. ?H pc⇩1)")
    proof
      assume throw: ?throw
      have "P ⊢ (None, h⇩0, (vs, ls⇩0, C, M, pc) # frs) -jvm→
                 (None, h⇩1, (Null#vs, ls⇩1, C, M, ?pc) # frs)"
        using ThrowNull⇩1 by fastforce
      also have "P ⊢ … -jvm→  handle P C M ?xa h⇩1 (Null#vs) ls⇩1 ?pc frs"
        using ThrowNull⇩1.prems by(auto simp add:handle_def)
      also have "handle P C M ?xa h⇩1 (Null#vs) ls⇩1 ?pc frs =
                 handle P C M ?xa h⇩1 vs ls⇩1 ?pc frs"
        using ThrowNull⇩1.prems by(auto simp add:handle_Cons)
      finally have "?H ?pc" using throw by simp
      thus "∃pc⇩1. ?H pc⇩1" by iprover
    qed
  qed
next
  case ThrowThrow⇩1 thus ?case by fastforce
next
  case (Try⇩1 e⇩1 h⇩0 ls⇩0 v⇩1 h⇩1 ls⇩1 Ci i e⇩2)
  let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
  let ?pc⇩1' = "?pc⇩1 + 2 + length(compE⇩2 e⇩2)"
  have "P,C,M ⊳ compxE⇩2 (try e⇩1 catch(Ci i) e⇩2) pc (size vs) / I,size vs" by fact
  hence "P,C,M ⊳ compxE⇩2 e⇩1 pc (size vs) /
                 {pc..<pc + length (compE⇩2 e⇩1)},size vs"
    using Try⇩1.prems by (fastforce simp:beforex_def split:if_split_asm)
  hence "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
             (None,h⇩1,(v⇩1#vs,ls⇩1,C,M,?pc⇩1)#frs)" using Try⇩1 by auto
  also have "P ⊢ … -jvm→ (None,h⇩1,(v⇩1#vs,ls⇩1,C,M,?pc⇩1')#frs)"
    using Try⇩1.prems by auto
  finally show ?case by (auto simp:add.assoc)
next
  case (TryCatch⇩1 e⇩1 h⇩0 ls⇩0 a h⇩1 ls⇩1 D fs Ci i e⇩2 e⇩2' h⇩2 ls⇩2)
  let ?e = "try e⇩1 catch(Ci i) e⇩2"
  let ?xt = "compxE⇩2 ?e pc (size vs)"
  let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
  let ?ls⇩1 = "ls⇩1[i := Addr a]"
  let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
  let ?pc⇩1' = "?pc⇩1 + 2"
  let ?σ⇩1 = "(None,h⇩1,(vs,?ls⇩1,C,M, ?pc⇩1') # frs)"
  have I: "{pc..<pc + length (compE⇩2 (try e⇩1 catch(Ci i) e⇩2))} ⊆ I"
   and beforex: "P,C,M ⊳ ?xt/I,size vs" by fact+
  have "P ⊢ ?σ⇩0 -jvm→ (None,h⇩1,((Addr a)#vs,ls⇩1,C,M, ?pc⇩1+1) # frs)"
  proof -
    have "PROP ?P e⇩1 h⇩0 ls⇩0 (Throw a) h⇩1 ls⇩1 C M pc w a vs frs {pc..<pc + length (compE⇩2 e⇩1)}"
      by fact
    moreover have "P,C,M ⊳ compxE⇩2 e⇩1 pc (size vs)/{pc..<?pc⇩1},size vs"
      using beforex I pcs_subset by(force elim!: beforex_appendD1)
    ultimately have
      "∃pc⇩1. pc ≤ pc⇩1 ∧ pc⇩1 < ?pc⇩1 ∧
             ¬ caught P pc⇩1 h⇩1 a (compxE⇩2 e⇩1 pc (size vs)) ∧
             P ⊢ ?σ⇩0 -jvm→ handle P C M a h⇩1 vs ls⇩1 pc⇩1 frs"
      using  TryCatch⇩1.prems by auto
    then obtain pc⇩1 where
      pc⇩1_in_e⇩1: "pc ≤ pc⇩1" "pc⇩1 < ?pc⇩1" and
      pc⇩1_not_caught: "¬ caught P pc⇩1 h⇩1 a (compxE⇩2 e⇩1 pc (size vs))" and
      0: "P ⊢ ?σ⇩0 -jvm→ handle P C M a h⇩1 vs ls⇩1 pc⇩1 frs" by iprover
    from beforex obtain xt⇩0 xt⇩1
      where ex_tab: "ex_table_of P C M = xt⇩0 @ ?xt @ xt⇩1"
      and disj: "pcs xt⇩0 ∩ I = {}" by(auto simp:beforex_def)
    have hp: "h⇩1 a = Some (D, fs)" "P⇩1 ⊢ D ≼⇧* Ci" by fact+
    have "pc⇩1 ∉ pcs xt⇩0" using pc⇩1_in_e⇩1 I disj by auto
    with pc⇩1_in_e⇩1 pc⇩1_not_caught hp
    show ?thesis using ex_tab 0 by(simp add:handle_def matches_ex_entry_def)
  qed
  also have "P ⊢ … -jvm→ ?σ⇩1" using TryCatch⇩1 by auto
  finally have 1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1" .
  let ?pc⇩2 = "?pc⇩1' + length(compE⇩2 e⇩2)"
  let ?I⇩2 = "{?pc⇩1' ..< ?pc⇩2}"
  have "P,C,M ⊳ compxE⇩2 ?e pc (size vs) / I,size vs" by fact
  hence beforex⇩2: "P,C,M ⊳ compxE⇩2 e⇩2 ?pc⇩1' (size vs) / ?I⇩2, size vs"
    using I pcs_subset[of _ ?pc⇩1'] by(auto elim!:beforex_appendD2)
  have IH⇩2: "PROP ?P e⇩2 h⇩1 ?ls⇩1 e⇩2' h⇩2 ls⇩2 C M ?pc⇩1' v xa vs frs ?I⇩2" 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,h⇩2,(v#vs,ls⇩2,C,M,?pc⇩2)#frs)"
        using val beforex⇩2 IH⇩2 TryCatch⇩1.prems by auto
      finally show ?trans by(simp add:add.assoc)
    qed
  next
    show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
    proof
      assume throw: ?throw
      then obtain pc⇩2 where
        pc⇩2: "?pc⇩1+2 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩2 ∧
              ¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 e⇩2 ?pc⇩1' (size vs))" and
        2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
        using IH⇩2 beforex⇩2 TryCatch⇩1.prems by auto
      have "?H pc⇩2" using pc⇩2 jvm_trans[OF 1 2]
        by (simp add:match_ex_entry) (fastforce)
      thus "∃pc⇩2. ?H pc⇩2" by iprover
    qed
  qed
next
  case (TryThrow⇩1 e⇩1 h⇩0 ls⇩0 a h⇩1 ls⇩1 D fs Ci i e⇩2)
  let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
  let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
  let ?e = "try e⇩1 catch(Ci i) e⇩2"
  let ?xt = "compxE⇩2 ?e pc (size vs)"
  have I: "{pc..<pc + length (compE⇩2 (try e⇩1 catch(Ci i) e⇩2))} ⊆ I"
   and beforex: "P,C,M ⊳ ?xt/I,size vs" by fact+
  have "PROP ?P e⇩1 h⇩0 ls⇩0 (Throw a) h⇩1 ls⇩1 C M pc w a vs frs {pc..<pc + length (compE⇩2 e⇩1)}" by fact
  moreover have "P,C,M ⊳ compxE⇩2 e⇩1 pc (size vs)/{pc..<?pc⇩1},size vs"
    using beforex I pcs_subset by(force elim!: beforex_appendD1)
    ultimately have
      "∃pc⇩1. pc ≤ pc⇩1 ∧ pc⇩1 < ?pc⇩1 ∧
             ¬ caught P pc⇩1 h⇩1 a (compxE⇩2 e⇩1 pc (size vs)) ∧
             P ⊢ ?σ⇩0 -jvm→ handle P C M a h⇩1 vs ls⇩1 pc⇩1 frs"
      using TryThrow⇩1.prems by auto
    then obtain pc⇩1 where
      pc⇩1_in_e⇩1: "pc ≤ pc⇩1" "pc⇩1 < ?pc⇩1" and
      pc⇩1_not_caught: "¬ caught P pc⇩1 h⇩1 a (compxE⇩2 e⇩1 pc (size vs))" and
      0: "P ⊢ ?σ⇩0 -jvm→ handle P C M a h⇩1 vs ls⇩1 pc⇩1 frs" by iprover
  show ?case (is "?N ∧ (?eq ⟶ (∃pc⇩2. ?H pc⇩2))")
  proof
    show ?N by simp
  next
    { assume ?eq
      with TryThrow⇩1 pc⇩1_in_e⇩1 pc⇩1_not_caught 0
      have "?H pc⇩1" by (simp add:match_ex_entry) auto
      hence "∃pc⇩2. ?H pc⇩2" by iprover
    }
    thus "?eq ⟶ (∃pc⇩2. ?H pc⇩2)" by iprover
  qed
next
  case Nil⇩1 thus ?case by simp
next
  case (Cons⇩1 e h⇩0 ls⇩0 v h⇩1 ls⇩1 es fs h⇩2 ls⇩2)
  let ?pc⇩1 = "pc + length(compE⇩2 e)"
  let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
  let ?σ⇩1 = "(None,h⇩1,(v#vs,ls⇩1,C,M,?pc⇩1)#frs)"
  have 1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1" using Cons⇩1 by fastforce
  let ?pc⇩2 = "?pc⇩1 + length(compEs⇩2 es)"
  have IHs: "PROP ?Ps es h⇩1 ls⇩1 fs h⇩2 ls⇩2 C M ?pc⇩1 (tl ws) xa es' (v#vs) frs
    (I - pcs (compxE⇩2 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,h⇩2,(rev(ws) @ vs,ls⇩2,C,M,?pc⇩2)#frs)"
        using val IHs Cons⇩1.prems by fastforce
      finally show ?trans by(simp add:add.assoc)
    qed
  next
    show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
    proof
      assume throw: ?throw
      then obtain pc⇩2 where
        pc⇩2: "?pc⇩1 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩2 ∧
              ¬ caught P pc⇩2 h⇩2 xa (compxEs⇩2 es ?pc⇩1 (size vs + 1))" and
        2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 (v#vs) ls⇩2 pc⇩2 frs"
        using IHs Cons⇩1.prems
        by(fastforce simp:Cons_eq_append_conv neq_Nil_conv)
      have "?H pc⇩2" using Cons⇩1.prems pc⇩2 jvm_trans[OF 1 2]
        by (auto simp add: handle_Cons)
      thus "∃pc⇩2. ?H pc⇩2" by iprover
    qed
  qed
next
  case ConsThrow⇩1 thus ?case by (fastforce simp:Cons_eq_append_conv)
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 comp⇩2_correct:
assumes "method": "P⇩1 ⊢ C sees M:Ts→T = body in C"
    and eval:   "P⇩1 ⊢⇩1 ⟨body,(h,ls)⟩ ⇒ ⟨e',(h',ls')⟩"
shows "compP⇩2 P⇩1 ⊢ (None,h,[([],ls,C,M,0)]) -jvm→ (exception e',h',[])"
(*<*)
      (is "_ ⊢ ?σ⇩0 -jvm→ ?σ⇩1")
proof -
  let ?P = "compP⇩2 P⇩1"
  have code: "?P,C,M,0 ⊳ compE⇩2 body" using beforeM[OF "method"] by auto
  have xtab: "?P,C,M ⊳ compxE⇩2 body 0 (size[])/{..<size(compE⇩2 body)},size[]"
    using beforexM[OF "method"] 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(compE⇩2 body))])"
      using Jcc[OF eval code xtab] by auto
    also have "?P ⊢ … -jvm→ ?σ⇩1" using beforeM[OF "method"] by auto
    finally have ?thesis .
  }
  moreover
  { fix a assume [simp]: "e' = Throw a"
    obtain pc where pc: "0 ≤ pc ∧ pc < size(compE⇩2 body) ∧
          ¬ caught ?P pc h' a (compxE⇩2 body 0 0)"
    and 1: "?P ⊢ ?σ⇩0 -jvm→ handle ?P C M a h' [] ls' pc []"
      using Jcc[OF eval code xtab] by fastforce
    from pc have "handle ?P C M a h' [] ls' pc [] = ?σ⇩1" using xtab "method"
      by(auto simp:handle_def compMb⇩2_def)
    with 1 have ?thesis by simp
  } 
  ultimately show ?thesis using eval⇩1_final[OF eval] by(auto simp:final_def)
qed
(*>*)

end