Theory Correctness2

(*  Title:      Jinja/Compiler/Correctness2.thy
    ID:         $Id: Correctness2.thy,v 1.9 2008-06-24 22:23:29 makarius Exp $
    Author:     Tobias Nipkow
    Copyright   TUM 2003
*)

header {* \isaheader{Correctness of Stage 2} *}

theory Correctness2
imports List_Prefix Compiler2
begin

(*<*)hide (open) const Throw(*>*)

subsection{* Instruction sequences *}

text{* How to select individual instructions and subsequences of
instructions from a program given the class, method and program
counter. *}

constdefs
 before :: "jvm_prog => cname => mname => nat => instr list => bool"
   ("(_,_,_,_/ \<rhd> _)" [51,0,0,0,51] 50)
 "P,C,M,pc \<rhd> is  ≡  is ≤ drop pc (instrs_of P C M)"

 at :: "jvm_prog => cname => mname => nat => instr => bool"
   ("(_,_,_,_/ \<triangleright> _)" [51,0,0,0,51] 50)
 "P,C,M,pc \<triangleright> i  ≡  ∃is. drop pc (instrs_of P C M) = i#is"

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


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

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


lemma [simp]: "P,C,M,pc \<rhd> (is1 @ is2) = (P,C,M,pc \<rhd> is1 ∧ P,C,M,pc + size is1 \<rhd> is2)"
(*<*)
apply(simp add:before_def prefix_def)
apply(subst add_commute)
apply(simp add: drop_drop[symmetric])
apply fastsimp
done
(*>*)

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


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


lemma beforeM:
  "P \<turnstile> C sees M: Ts->T = body in D ==>
  compP2 P,D,M,0 \<rhd> compE2 body @ [Return]"
(*<*)
apply(drule sees_method_idemp)
apply(simp add:before_def compP2_def compMb2_def)
done
(*>*)

text{* This lemma executes a single instruction by rewriting: *}

lemma [simp]:
  "P,C,M,pc \<triangleright> instr ==>
  (P \<turnstile> (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 \<turnstile> σ -jvm-> σ'))"
(*<*)
apply(simp only: exec_all_def)
apply(blast intro: converse_rtranclE converse_rtrancl_into_rtrancl)
done
(*>*)


section{* Exception tables *}

constdefs
  pcs :: "ex_table => nat set"
  "pcs xt  ≡  \<Union>(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)}"
(*<*)
apply(induct e and es)
apply (simp_all add:pcs_def)
apply (fastsimp split:bop.splits)+
done
(*>*)


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 fastsimp(*>*)


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


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


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


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 fastsimp(*>*)


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


constdefs
  caught :: "jvm_prog => pc => heap => addr => ex_table => bool"
  "caught P pc h a xt  ≡
  (∃entry ∈ set xt. matches_ex_entry P (cname_of h a) pc entry)"

  beforex :: "jvm_prog => cname => mname => ex_table => nat set => nat => bool"
              ("(2_,/_,/_ \<rhd>/ _ /'/ _,/_)" [51,0,0,0,0,51] 50)
  "P,C,M \<rhd> 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)"

  dummyx :: "jvm_prog => cname => mname => ex_table => nat set => nat => bool"  ("(2_,_,_ \<triangleright>/ _ '/_,_)" [51,0,0,0,0,51] 50)
  "P,C,M \<triangleright> xt/I,d ≡ P,C,M \<rhd> xt/I,d"

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


lemma beforex_mono: "[| P,C,M \<rhd> xt/I,d'; d' ≤ d |] ==> P,C,M \<rhd> xt/I,d"
(*<*)by(fastsimp simp:beforex_def)(*>*)


lemma [simp]: "P,C,M \<rhd> xt/I,d ==> P,C,M \<rhd> xt/I,Suc d"
(*<*)by(fastsimp intro:beforex_mono)(*>*)


lemma beforex_append[simp]:
  "pcs xt1 ∩ pcs xt2 = {} ==>
  P,C,M \<rhd> xt1 @ xt2/I,d =
  (P,C,M \<rhd> xt1/I-pcs xt2,d  ∧  P,C,M \<rhd> xt2/I-pcs xt1,d ∧ P,C,M \<triangleright> xt1@xt2/I,d)"
(*<*)
apply(rule iffI)
 prefer 2
 apply(simp add:dummyx_def)
apply(auto simp add: beforex_def dummyx_def)
 apply(rule_tac x = xt0 in exI)
 apply auto
apply(rule_tac x = "xt0@xt1" in exI)
apply auto
done
(*>*)


lemma beforex_appendD1:
  "[| P,C,M \<rhd> xt1 @ xt2 @ [(f,t,D,h,d)] / I,d;
    pcs xt1 ⊆ J; J ⊆ I; J ∩ pcs xt2 = {} |]
  ==> P,C,M \<rhd> xt1 / J,d"
(*<*)
apply(auto simp:beforex_def)
apply(rule exI,rule exI,rule conjI, rule refl)
apply(rule conjI, blast)
apply(auto)
apply(subgoal_tac "pc ∉ pcs xt2")
 prefer 2 apply blast
apply (auto split:split_if_asm)
done
(*>*)


lemma beforex_appendD2:
  "[| P,C,M \<rhd> xt1 @ xt2 @ [(f,t,D,h,d)] / I,d;
    pcs xt2 ⊆ J; J ⊆ I; J ∩ pcs xt1 = {} |]
  ==> P,C,M \<rhd> xt2 / J,d"
(*<*)
apply(auto simp:beforex_def)
apply(rule_tac x = "xt0 @ xt1" in exI)
apply fastsimp
done
(*>*)


lemma beforexM:
  "P \<turnstile> C sees M: Ts->T = body in D ==>
  compP2 P,D,M \<rhd> compxE2 body 0 0/{..<size(compE2 body)},0"
(*<*)
apply(drule sees_method_idemp)
apply(drule sees_method_compP[where f = compMb2])
apply(simp add:beforex_def compP2_def compMb2_def)
apply(rule_tac x = "[]" in exI)
using pcs_subset apply fastsimp
done
(*>*)


lemma match_ex_table_SomeD2:
 "[| match_ex_table P D pc (ex_table_of P C M) = ⌊(pc',d')⌋;
    P,C,M \<rhd> xt/I,d; ∀x ∈ set xt. ¬ matches_ex_entry P D pc x; pc ∈ I |]
 ==> d' ≤ d"
(*<*)
apply(auto simp:beforex_def)
apply(subgoal_tac "pc ∉ pcs xt0")
apply auto
done
(*>*)


lemma match_ex_table_SomeD1:
  "[| match_ex_table P D pc (ex_table_of P C M) = ⌊(pc',d')⌋;
     P,C,M \<rhd> 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]
(*>*)


constdefs
  handle :: "jvm_prog => cname => mname => addr => heap => val list => val list => nat => frame list
                => jvm_state"
  "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 \<rhd> 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:
 "[| P,C,M \<rhd> xt/I,d; d ≤ size vs; pc ∈ I; pc ∉ pcs xt |] ==>
  handle P C M xa h (ws @ vs) ls pc frs = handle P C M xa h vs ls pc frs"
(*<*)
apply(auto simp:handle_def)
apply(rename_tac pc' d')
apply(subgoal_tac "size ws ≤ length ws + length vs - d'")
apply(simp add:drop_all)
apply(fastsimp dest:match_ex_table_SomeD2 split:nat_diff_split)
done
(*>*)


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


lemma fixes P1 defines [simp]: "P ≡ compP2 P1"
shows Jcc:
  "P1 \<turnstile>1 ⟨e,(h0,ls0)⟩ => ⟨ef,(h1,ls1)⟩ ==>
  (!!C M pc v xa vs frs I.
     [| P,C,M,pc \<rhd> compE2 e; P,C,M \<rhd> compxE2 e pc (size vs)/I,size vs;
       {pc..<pc+size(compE2 e)} ⊆ I |] ==>
     (ef = Val v -->
      P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
            (None,h1,(v#vs,ls1,C,M,pc+size(compE2 e))#frs))
     ∧
     (ef = Throw xa -->
      (∃pc1. pc ≤ pc1 ∧ pc1 < pc + size(compE2 e) ∧
               ¬ caught P pc1 h1 xa (compxE2 e pc (size vs)) ∧
               P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm-> handle P C M xa h1 vs ls1 pc1 frs)))"
(*<*)
  (is "_ ==> (!!C M pc v xa vs frs I.
                  PROP ?P e h0 ls0 ef h1 ls1 C M pc v xa vs frs I)")
(*>*)

and "P1 \<turnstile>1 ⟨es,(h0,ls0)⟩ [=>] ⟨fs,(h1,ls1)⟩ ==>
    (!!C M pc ws xa es' vs frs I.
      [| P,C,M,pc \<rhd> compEs2 es; P,C,M \<rhd> compxEs2 es pc (size vs)/I,size vs;
       {pc..<pc+size(compEs2 es)} ⊆ I |] ==>
      (fs = map Val ws -->
       P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
             (None,h1,(rev ws @ vs,ls1,C,M,pc+size(compEs2 es))#frs))
      ∧
      (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)) ∧
                P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm-> handle P C M xa h1 vs ls1 pc1 frs)))"
(*<*)
  (is "_ ==> (!!C M pc ws xa es' vs frs I.
                  PROP ?Ps es h0 ls0 fs h1 ls1 C M pc ws xa es' vs frs I)")
proof (induct rule:eval1_evals1_inducts)
  case New1 thus ?case by (clarsimp simp add:blank_def expand_fun_eq)
next
  case NewFail1 thus ?case by(auto simp: handle_def pcs_def)
next
  case (Cast1 e h0 ls0 a h1 ls1 D fs C')
  let ?pc = "pc + length(compE2 e)"
  have "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
             (None,h1,(Addr a#vs,ls1,C,M,?pc)#frs)" using Cast1 by fastsimp
  also have "P \<turnstile> … -jvm-> (None,h1,(Addr a#vs,ls1,C,M,?pc+1)#frs)"
    using Cast1 by (auto simp add:cast_ok_def)
  finally show ?case by auto
next
  case (CastNull1 e h0 ls0 h1 ls1 C')
  let ?pc = "pc + length(compE2 e)"
  have "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
            (None,h1,(Null#vs,ls1,C,M,?pc)#frs)"
    using CastNull1 by fastsimp
  also have "P \<turnstile> … -jvm-> (None,h1,(Null#vs,ls1,C,M,?pc+1)#frs)"
    using CastNull1 by (auto simp add:cast_ok_def)
  finally show ?case by auto
next
  case (CastFail1 e h0 ls0 a h1 ls1 D fs C')
  let ?pc = "pc + length(compE2 e)"
  let ?xa = "addr_of_sys_xcpt ClassCast"
  have "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
             (None,h1,(Addr a#vs,ls1,C,M,?pc)#frs)"
    using CastFail1 by fastsimp
  also have "P \<turnstile> … -jvm-> handle P C M ?xa h1 (Addr a#vs) ls1 ?pc frs"
    using CastFail1 by (auto simp add:handle_def cast_ok_def)
  also have "handle P C M ?xa h1 (Addr a#vs) ls1 ?pc frs =
             handle P C M ?xa h1 vs ls1 ?pc frs"
    using CastFail1.prems by(auto simp:handle_Cons)
  finally have exec: "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm-> …".
  show ?case (is "?N ∧ (?eq --> (∃pc1. ?H pc1))")
  proof
    show ?N by simp
  next
    have "?eq --> ?H ?pc" using exec by auto
    thus "?eq --> (∃pc1. ?H pc1)" by blast
  qed
next
  case CastThrow1 thus ?case by fastsimp
next
  case Val1 thus ?case by simp
next
  case Var1 thus ?case by auto
next
  case (BinOp1 e1 h0 ls0 v1 h1 ls1 e2 v2 h2 ls2 bop w)
  let ?pc1 = "pc + length(compE2 e1)"
  let ?pc2 = "?pc1 + length(compE2 e2)"
  have IH2: "PROP ?P e2 h1 ls1 (Val v2) h2 ls2 C M ?pc1 v2 xa (v1#vs) frs
                     (I - pcs(compxE2 e1 pc (size vs)))" by fact
  have "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
             (None,h1,(v1#vs,ls1,C,M,?pc1)#frs)" using BinOp1 by fastsimp
  also have "P \<turnstile> … -jvm-> (None,h2,(v2#v1#vs,ls2,C,M,?pc2)#frs)"
    using BinOp1.prems IH2 by fastsimp
  also have "P \<turnstile> … -jvm-> (None,h2,(w#vs,ls2,C,M,?pc2+1)#frs)"
    using BinOp1 by(cases bop) auto
  finally show ?case by (auto split: bop.splits simp:add_assoc)
next
  case BinOpThrow11 thus ?case by(fastsimp)
next
  case (BinOpThrow21 e1 h0 ls0 v1 h1 ls1 e2 e h2 ls2 bop)
  let ?pc = "pc + length(compE2 e1)"
  let ?σ1 = "(None,h1,(v1#vs,ls1,C,M,?pc)#frs)"
  have 1: "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm-> ?σ1"
    using BinOpThrow21 by fastsimp
  show ?case (is "?N ∧ (?eq --> (∃pc2. ?H pc2))")
  proof
    show ?N by simp
  next
    { assume ?eq
      moreover
      have "PROP ?P e2 h1 ls1 (throw e) h2 ls2 C M ?pc v xa (v1#vs) frs
                     (I - pcs(compxE2 e1 pc (size vs)))" by fact
      ultimately obtain pc2 where
        pc2: "?pc ≤ pc2 ∧ pc2 < ?pc + size(compE2 e2) ∧
              ¬ caught P pc2 h2 xa (compxE2 e2 ?pc (size vs + 1))" and
        2: "P \<turnstile> ?σ1 -jvm-> handle P C M xa h2 (v1#vs) ls2 pc2 frs"
        using BinOpThrow21.prems by fastsimp
      have 3: "P \<turnstile> ?σ1 -jvm-> handle P C M xa h2 vs ls2 pc2 frs"
        using 2 BinOpThrow21.prems pc2 by(auto simp:handle_Cons)
      have "?H pc2" using pc2 jvm_trans[OF 1 3] by auto
      hence "∃pc2. ?H pc2" by iprover
    }
    thus "?eq --> (∃pc2. ?H pc2)" by iprover
  qed
next
  case (FAcc1 e h0 ls0 a h1 ls1 C fs F D w)
  let ?pc = "pc + length(compE2 e)"
  have "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
             (None,h1,(Addr a#vs,ls1,C,M,?pc)#frs)" using FAcc1 by fastsimp
  also have "P \<turnstile> … -jvm-> (None,h1,(w#vs,ls1,C,M,?pc+1)#frs)"
    using FAcc1 by auto
  finally show ?case by auto
next
  case (FAccNull1 e h0 ls0 h1 ls1 F D)
  let ?pc = "pc + length(compE2 e)"
  let ?xa = "addr_of_sys_xcpt NullPointer"
  have "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
             (None,h1,(Null#vs,ls1,C,M,?pc)#frs)" using FAccNull1 by fastsimp
  also have "P \<turnstile> … -jvm-> handle P C M ?xa h1 (Null#vs) ls1 ?pc frs"
    using FAccNull1.prems
    by(fastsimp simp:split_beta handle_def simp del: split_paired_Ex)
  also have "handle P C M ?xa h1 (Null#vs) ls1 ?pc frs =
             handle P C M ?xa h1 vs ls1 ?pc frs"
    using FAccNull1.prems by(auto simp add:handle_Cons)
  finally show ?case by (auto intro: exI[where x = ?pc])
next
  case FAccThrow1 thus ?case by fastsimp
next
  case (LAss1 e h0 ls0 w h1 ls1 i ls2)
  let ?pc = "pc + length(compE2 e)"
  have "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
             (None,h1,(w#vs,ls1,C,M,?pc)#frs)" using LAss1 by fastsimp
  also have "P \<turnstile> … -jvm-> (None,h1,(Unit#vs,ls2,C,M,?pc+2)#frs)"
    using LAss1 by auto
  finally show ?case using LAss1 by auto
next
  case LAssThrow1 thus ?case by fastsimp
next
  case (FAss1 e1 h0 ls0 a h1 ls1 e2 w h2 ls2 C fs fs' F D h2')
  let ?pc1 = "pc + length(compE2 e1)"
  let ?pc2 = "?pc1 + length(compE2 e2)"
  have IH2: "PROP ?P e2 h1 ls1 (Val w) h2 ls2 C M ?pc1 w xa (Addr a#vs) frs
                     (I - pcs(compxE2 e1 pc (size vs)))" by fact
  have "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
             (None,h1,(Addr a#vs,ls1,C,M,?pc1)#frs)" using FAss1 by fastsimp
  also have "P \<turnstile> … -jvm-> (None,h2,(w#Addr a#vs,ls2,C,M,?pc2)#frs)"
    using FAss1.prems IH2 by fastsimp
  also have "P \<turnstile> … -jvm-> (None,h2',(Unit#vs,ls2,C,M,?pc2+2)#frs)"
    using FAss1 by auto
  finally show ?case using FAss1 by (auto simp:add_assoc)
next
  case (FAssNull1 e1 h0 ls0 h1 ls1 e2 w h2 ls2 F D)
  let ?pc1 = "pc + length(compE2 e1)"
  let ?pc2 = "?pc1 + length(compE2 e2)"
  let ?xa = "addr_of_sys_xcpt NullPointer"
  have IH2: "PROP ?P e2 h1 ls1 (Val w) h2 ls2 C M ?pc1 w xa (Null#vs) frs
                     (I - pcs(compxE2 e1 pc (size vs)))" by fact
  have "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
             (None,h1,(Null#vs,ls1,C,M,?pc1)#frs)" using FAssNull1 by fastsimp
  also have "P \<turnstile> … -jvm-> (None,h2,(w#Null#vs,ls2,C,M,?pc2)#frs)"
    using FAssNull1.prems IH2 by fastsimp
  also have "P \<turnstile> … -jvm-> handle P C M ?xa h2 (w#Null#vs) ls2 ?pc2 frs"
    using FAssNull1.prems
    by(fastsimp simp:split_beta handle_def simp del: split_paired_Ex)
  also have "handle P C M ?xa h2 (w#Null#vs) ls2 ?pc2 frs =
             handle P C M ?xa h2 vs ls2 ?pc2 frs"
    using FAssNull1.prems by(auto simp add:handle_Cons)
  finally show ?case by (auto intro: exI[where x = ?pc2])
next
  case (FAssThrow21 e1 h0 ls0 w h1 ls1 e2 e' h2 ls2 F D)
  let ?pc1 = "pc + length(compE2 e1)"
  let ?σ1 = "(None,h1,(w#vs,ls1,C,M,?pc1)#frs)"
  have 1: "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm-> ?σ1"
    using FAssThrow21 by fastsimp
  show ?case (is "?N ∧ (?eq --> (∃pc2. ?H pc2))")
  proof
    show ?N by simp
  next
    { assume ?eq
      moreover
      have "PROP ?P e2 h1 ls1 (throw e') h2 ls2 C M ?pc1 v xa (w#vs) frs
                    (I - pcs (compxE2 e1 pc (length vs)))" by fact
      ultimately obtain pc2 where
        pc2: "?pc1 ≤ pc2 ∧ pc2 < ?pc1 + size(compE2 e2) ∧
              ¬ caught P pc2 h2 xa (compxE2 e2 ?pc1 (size vs + 1))" and
        2: "P \<turnstile> ?σ1 -jvm-> handle P C M xa h2 (w#vs) ls2 pc2 frs"
        using FAssThrow21.prems by fastsimp
      have 3: "P \<turnstile> ?σ1 -jvm-> handle P C M xa h2 vs ls2 pc2 frs"
        using 2 FAssThrow21.prems pc2 by(auto simp:handle_Cons)
      have "?H pc2" using pc2 jvm_trans[OF 1 3]       by auto
      hence "∃pc2. ?H pc2" by iprover
    }
    thus "?eq --> (∃pc2. ?H pc2)" by iprover
  qed
next
  case FAssThrow11 thus ?case by fastsimp
next
  case (Call1 e h0 ls0 a h1 ls1 es pvs h2 ls2 Ca fs M' Ts T body D ls2' f h3 ls3)
  have "P1 \<turnstile>1 ⟨es,(h1, ls1)⟩ [=>] ⟨map Val pvs,(h2, ls2)⟩" by fact
  hence [simp]: "length es = length pvs" by(auto dest:evals1_preserves_elen)
  let ?σ0 = "(None,h0,(vs, ls0, C,M,pc)#frs)"
  let ?pc1 = "pc + length(compE2 e)"
  let ?σ1 = "(None,h1,(Addr a # vs, ls1, C,M,?pc1)#frs)"
  let ?pc2 = "?pc1 + length(compEs2 es)"
  let ?frs2 = "(rev pvs @ Addr a # vs, ls2, C,M,?pc2)#frs"
  let ?σ2 = "(None,h2,?frs2)"
  let ?frs2' = "([], ls2', D,M',0) # ?frs2"
  let ?σ2' = "(None, h2, ?frs2')"
  have IH_es: "PROP ?Ps es h1 ls1 (map Val pvs) h2 ls2 C M ?pc1 pvs xa
                    (map Val pvs) (Addr a # vs) frs (I - pcs(compxE2 e pc (size vs)))" by fact
  have "P \<turnstile> ?σ0 -jvm-> ?σ1" using Call1 by fastsimp
  also have "P \<turnstile> … -jvm-> ?σ2" using IH_es Call1.prems by fastsimp
  also have "P \<turnstile> … -jvm-> ?σ2'"
    using Call1 by(auto simp add: nth_append compMb2_def)
  finally have 1: "P \<turnstile> ?σ0 -jvm-> ?σ2'".
  have "P1 \<turnstile> Ca sees M': Ts->T = body in D" by fact
  then have M'_in_D: "P1 \<turnstile> D sees M': Ts->T = body in D"
    by(rule sees_method_idemp) 
  hence M'_code: "compP2 P1,D,M',0 \<rhd> compE2 body @ [Return]"
    and M'_xtab: "compP2 P1,D,M' \<rhd> compxE2 body 0 0/{..<size(compE2 body)},0"
    by(rule beforeM, rule beforexM)
  have IH_body: "PROP ?P body h2 ls2' f h3 ls3 D M' 0 v xa [] ?frs2 ({..<size(compE2 body)})" by fact
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val --> ?trans")
    proof
      assume val: ?val
      note 1
      also have "P \<turnstile> ?σ2' -jvm->
                     (None,h3,([v],ls3,D,M',size(compE2 body))#?frs2)"
        using val IH_body Call1.prems M'_code M'_xtab
        by (fastsimp simp del:split_paired_Ex)
      also have "P \<turnstile> … -jvm-> (None, h3, (v # vs, ls2, C,M,?pc2+1)#frs)"
        using Call1 M'_code M'_in_D by(auto simp: nth_append compMb2_def)
      finally show ?trans by(simp add:add_assoc)
    qed
  next
    show ?Err (is "?throw --> (∃pc2. ?H pc2)")
    proof
      assume throw: ?throw
      with IH_body obtain pc2 where
        pc2: "0 ≤ pc2 ∧ pc2 < size(compE2 body) ∧
              ¬ caught P pc2 h3 xa (compxE2 body 0 0)" and
        2: "P \<turnstile> ?σ2' -jvm-> handle P D M' xa h3 [] ls3 pc2 ?frs2"
        using Call1.prems M'_code M'_xtab
        by (fastsimp simp del:split_paired_Ex)
      have "handle P D M' xa h3 [] ls3 pc2 ?frs2 =
            handle P C M xa h3 (rev pvs @ Addr a # vs) ls2 ?pc2 frs"
        using pc2 M'_in_D by(auto simp add:handle_def)
      also have "… = handle P C M xa h3 vs ls2 ?pc2 frs"
        using Call1.prems by(auto simp add:handle_append handle_Cons)
      finally have "?H ?pc2" using pc2 jvm_trans[OF 1 2] by auto
      thus "∃pc2. ?H pc2" by iprover
    qed
  qed
next
  case (CallParamsThrow1 e h0 ls0 w h1 ls1 es es' h2 ls2 pvs ex es'' M')
  let ?σ0 = "(None,h0,(vs, ls0, C,M,pc)#frs)"
  let ?pc1 = "pc + length(compE2 e)"
  let ?σ1 = "(None,h1,(w # vs, ls1, C,M,?pc1)#frs)"
  let ?pc2 = "?pc1 + length(compEs2 es)"
  have 1: "P \<turnstile> ?σ0 -jvm-> ?σ1" using CallParamsThrow1 by fastsimp
  show ?case (is "?N ∧ (?eq --> (∃pc2. ?H pc2))")
  proof
    show ?N by simp
  next
    { assume ?eq
      moreover
      have "PROP ?Ps es h1 ls1 es' h2 ls2 C M ?pc1 pvs xa es'' (w#vs) frs
        (I - pcs (compxE2 e pc (length vs)))" by fact
      ultimately have "∃pc2.
        (?pc1 ≤ pc2 ∧ pc2 < ?pc1 + size(compEs2 es) ∧
         ¬ caught P pc2 h2 xa (compxEs2 es ?pc1 (size vs + 1))) ∧
        P \<turnstile> ?σ1 -jvm-> handle P C M xa h2 (w#vs) ls2 pc2 frs"
        (is "∃pc2. ?PC pc2 ∧ ?Exec pc2")
        using CallParamsThrow1 by force
      then obtain pc2 where pc2: "?PC pc2" and 2: "?Exec pc2" by iprover
      have "?H pc2" using pc2 jvm_trans[OF 1 2] CallParamsThrow1
        by(auto simp:handle_Cons)
      hence "∃pc2. ?H pc2" by iprover
    }
    thus "?eq --> (∃pc2. ?H pc2)" by iprover
  qed
next
  case (CallNull1 e h0 ls0 h1 ls1 es pvs h2 ls2 M')
  have "P1 \<turnstile>1 ⟨es,(h1, ls1)⟩ [=>] ⟨map Val pvs,(h2, ls2)⟩" by fact
  hence [simp]: "length es = length pvs" by(auto dest:evals1_preserves_elen)
  let ?pc1 = "pc + length(compE2 e)"
  let ?pc2 = "?pc1 + length(compEs2 es)"
  let ?xa = "addr_of_sys_xcpt NullPointer"
  have IH_es: "PROP ?Ps es h1 ls1 (map Val pvs) h2 ls2 C M ?pc1 pvs xa
                    (map Val pvs) (Null#vs) frs (I - pcs(compxE2 e pc (size vs)))" by fact
  have "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
             (None,h1,(Null#vs,ls1,C,M,?pc1)#frs)" using CallNull1 by fastsimp
  also have "P \<turnstile> … -jvm-> (None,h2,(rev pvs@Null#vs,ls2,C,M,?pc2)#frs)"
    using CallNull1 IH_es by fastsimp
  also have "P \<turnstile> … -jvm-> handle P C M ?xa h2 (rev pvs@Null#vs) ls2 ?pc2 frs"
    using CallNull1.prems
    by(auto simp:split_beta handle_def nth_append simp del: split_paired_Ex)
  also have "handle P C M ?xa h2 (rev pvs@Null#vs) ls2 ?pc2 frs =
             handle P C M ?xa h2 vs ls2 ?pc2 frs"
    using CallNull1.prems by(auto simp:handle_Cons handle_append)
  finally show ?case by (auto intro: exI[where x = ?pc2])
next
  case CallObjThrow1 thus ?case by fastsimp
next
  case Block1 thus ?case by auto
next
  case (Seq1 e1 h0 ls0 w h1 ls1 e2 e2' h2 ls2)
  let ?pc1 = "pc + length(compE2 e1)"
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc)#frs)"
  let ?σ1 = "(None,h1,(vs,ls1,C,M,?pc1+1)#frs)"
  have "P \<turnstile> ?σ0 -jvm-> (None,h1,(w#vs,ls1,C,M,?pc1)#frs)"
    using Seq1 by fastsimp
  also have "P \<turnstile> … -jvm-> ?σ1" using Seq1 by auto
  finally have eval1: "P \<turnstile> ?σ0 -jvm-> ?σ1".
  let ?pc2 = "?pc1 + 1 + length(compE2 e2)"
  have IH2: "PROP ?P e2 h1 ls1 e2' h2 ls2 C M (?pc1+1) v xa vs frs
                     (I - pcs(compxE2 e1 pc (size vs)))" by fact
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val --> ?trans")
    proof
      assume val: ?val
      note eval1
      also have "P \<turnstile> ?σ1 -jvm-> (None,h2,(v#vs,ls2,C,M,?pc2)#frs)"
        using val Seq1.prems IH2 by fastsimp
      finally show ?trans by(simp add:add_assoc)
    qed
  next
    show ?Err (is "?throw --> (∃pc2. ?H pc2)")
    proof
      assume throw: ?throw
      then obtain pc2 where
        pc2: "?pc1+1 ≤ pc2 ∧ pc2 < ?pc2 ∧
              ¬ caught P pc2 h2 xa (compxE2 e2 (?pc1+1) (size vs))" and
        eval2: "P \<turnstile> ?σ1 -jvm-> handle P C M xa h2 vs ls2 pc2 frs"
        using IH2 Seq1.prems by fastsimp
      have "?H pc2" using pc2 jvm_trans[OF eval1 eval2]     by auto
      thus "∃pc2. ?H pc2" by iprover
    qed
  qed
next
  case SeqThrow1 thus ?case by fastsimp
next
  case (CondT1 e h0 ls0 h1 ls1 e1 e' h2 ls2 e2)
  let ?pc1 = "pc + length(compE2 e)"
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc)#frs)"
  let ?σ1 = "(None,h1,(vs,ls1,C,M,?pc1+1)#frs)"
  have "P \<turnstile> ?σ0 -jvm-> (None,h1,(Bool(True)#vs,ls1,C,M,?pc1)#frs)"
    using CondT1 by (fastsimp simp add: Int_Un_distrib)
  also have "P \<turnstile> … -jvm-> ?σ1" using CondT1 by auto
  finally have eval1: "P \<turnstile> ?σ0 -jvm-> ?σ1".
  let ?pc1' = "?pc1 + 1 + length(compE2 e1)"
  let ?pc2' = "?pc1' + 1 + length(compE2 e2)"
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val --> ?trans")
    proof
      assume val: ?val
      note eval1
      also have "P \<turnstile> ?σ1 -jvm-> (None,h2,(v#vs,ls2,C,M,?pc1')#frs)"
        using val CondT1 by(fastsimp simp:Int_Un_distrib)
      also have "P \<turnstile> … -jvm-> (None,h2,(v#vs,ls2,C,M,?pc2')#frs)"
        using CondT1 by(auto simp:add_assoc)
      finally show ?trans by(simp add:add_assoc)
    qed
  next
    show ?Err (is "?throw --> (∃pc2. ?H pc2)")
    proof
      let ?d = "size vs"
      let ?I = "I - pcs(compxE2 e pc ?d) - pcs(compxE2 e2 (?pc1'+1) ?d)"
      assume throw: ?throw
      moreover
      have "PROP ?P e1 h1 ls1 e' h2 ls2 C M (?pc1+1) v xa vs frs ?I" by fact
      ultimately obtain pc2 where
        pc2: "?pc1+1 ≤ pc2 ∧ pc2 < ?pc1' ∧
              ¬ caught P pc2 h2 xa (compxE2 e1 (?pc1+1) (size vs))" and
        eval2: "P \<turnstile> ?σ1 -jvm-> handle P C M xa h2 vs ls2 pc2 frs"
        using CondT1.prems by (fastsimp simp:Int_Un_distrib)
      have "?H pc2" using pc2 jvm_trans[OF eval1 eval2]     by auto
      thus "∃pc2. ?H pc2" by iprover
    qed
  qed
next
  case (CondF1 e h0 ls0 h1 ls1 e2 e' h2 ls2 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)#frs)"
  let ?σ1 = "(None,h1,(vs,ls1,C,M,?pc2)#frs)"
  have "P \<turnstile> ?σ0 -jvm-> (None,h1,(Bool(False)#vs,ls1,C,M,?pc1)#frs)"
    using CondF1 by (fastsimp simp add: Int_Un_distrib)
  also have "P \<turnstile> … -jvm-> ?σ1" using CondF1 by auto
  finally have eval1: "P \<turnstile> ?σ0 -jvm-> ?σ1".
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val --> ?trans")
    proof
      assume val: ?val
      note eval1
      also have "P \<turnstile> ?σ1 -jvm-> (None,h2,(v#vs,ls2,C,M,?pc2')#frs)"
        using val CondF1 by(fastsimp simp:Int_Un_distrib)
      finally show ?trans by(simp add:add_assoc)
    qed
  next
    show ?Err (is "?throw --> (∃pc2. ?H pc2)")
    proof
      let ?d = "size vs"
      let ?I = "I - pcs(compxE2 e pc ?d) - pcs(compxE2 e1 (?pc1+1) ?d)"
      assume throw: ?throw
      moreover
      have "PROP ?P e2 h1 ls1 e' h2 ls2 C M ?pc2 v xa vs frs ?I" by fact
      ultimately obtain pc2 where
        pc2: "?pc2 ≤ pc2 ∧ pc2 < ?pc2' ∧
              ¬ caught P pc2 h2 xa (compxE2 e2 ?pc2 ?d)" and
        eval2: "P \<turnstile> ?σ1 -jvm-> handle P C M xa h2 vs ls2 pc2 frs"
        using CondF1.prems by(fastsimp simp:Int_Un_distrib)
      have "?H pc2" using pc2 jvm_trans[OF eval1 eval2]     by auto
      thus "∃pc2. ?H pc2" by iprover
    qed
  qed
next
  case (CondThrow1 e h0 ls0 f h1 ls1 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 "pcs(compxE2 e pc ?d) ∩ pcs(?xt1 @ ?xt2) = {}"
    using CondThrow1.prems by (simp add:Int_Un_distrib)
  moreover have "PROP ?P e h0 ls0 (throw f) h1 ls1 C M pc v xa vs frs ?I" by fact
  ultimately show ?case using CondThrow1.prems by fastsimp
next
  case (WhileF1 e h0 ls0 h1 ls1 c)
  let ?pc = "pc + length(compE2 e)"
  let ?pc' = "?pc + length(compE2 c) + 3"
  have "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
            (None,h1,(Bool False#vs,ls1,C,M,?pc)#frs)"
    using WhileF1 by fastsimp
  also have "P \<turnstile> … -jvm-> (None,h1,(vs,ls1,C,M,?pc')#frs)"
    using WhileF1 by (auto simp:add_assoc)
  also have "P \<turnstile> … -jvm-> (None,h1,(Unit#vs,ls1,C,M,?pc'+1)#frs)"
    using WhileF1.prems by (auto simp:nat_number)
  finally show ?case by (simp add:add_assoc nat_number)
next
  case (WhileT1 e h0 ls0 h1 ls1 c v1 h2 ls2 e3 h3 ls3)
  let ?pc = "pc + length(compE2 e)"
  let ?pc' = "?pc + length(compE2 c) + 1"
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc)#frs)"
  let ?σ2 = "(None,h2,(vs,ls2,C,M,pc)#frs)"
  have "P \<turnstile> ?σ0 -jvm-> (None,h1,(Bool True#vs,ls1,C,M,?pc)#frs)"
    using WhileT1 by fastsimp
  also have "P \<turnstile> … -jvm-> (None,h1,(vs,ls1,C,M,?pc+1)#frs)"
    using WhileT1.prems by auto
  also have "P \<turnstile> … -jvm-> (None,h2,(v1#vs,ls2,C,M,?pc')#frs)"
    using WhileT1 by(fastsimp)
  also have "P \<turnstile> … -jvm-> ?σ2" using WhileT1.prems by auto
  finally have 1: "P \<turnstile> ?σ0 -jvm-> ?σ2".
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val --> ?trans")
    proof
      assume val: ?val
      note 1
      also have "P \<turnstile> ?σ2 -jvm-> (None,h3,(v#vs,ls3,C,M,?pc'+3)#frs)"
        using val WhileT1 by (auto simp add:add_assoc nat_number)
      finally show ?trans by(simp add:add_assoc nat_number)
    qed
  next
    show ?Err (is "?throw --> (∃pc2. ?H pc2)")
    proof
      assume throw: ?throw
      moreover
      have "PROP ?P (while (e) c) h2 ls2 e3 h3 ls3 C M pc v xa vs frs I" by fact
      ultimately obtain pc2 where
        pc2: "pc ≤ pc2 ∧ pc2 < ?pc'+3 ∧
              ¬ caught P pc2 h3 xa (compxE2 (while (e) c) pc (size vs))" and
        2: "P \<turnstile> ?σ2 -jvm-> handle P C M xa h3 vs ls3 pc2 frs"
        using WhileT1.prems by (auto simp:add_assoc nat_number)
      have "?H pc2" using pc2 jvm_trans[OF 1 2] by auto
      thus "∃pc2. ?H pc2" by iprover
    qed
  qed
next
  case WhileCondThrow1 thus ?case by fastsimp
next
  case (WhileBodyThrow1 e h0 ls0 h1 ls1 c e' h2 ls2)
  let ?pc1 = "pc + length(compE2 e)"
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc)#frs)"
  let ?σ1 = "(None,h1,(vs,ls1,C,M,?pc1+1)#frs)"
  have "P \<turnstile> ?σ0 -jvm-> (None,h1,(Bool(True)#vs,ls1,C,M,?pc1)#frs)"
    using WhileBodyThrow1 by (fastsimp simp add: Int_Un_distrib)
  also have "P \<turnstile> … -jvm-> ?σ1" using  WhileBodyThrow1 by auto
  finally have eval1: "P \<turnstile> ?σ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 --> (∃pc2. ?H pc2)")
    proof
      assume throw: ?throw
      moreover
      have "PROP ?P c h1 ls1 (throw e') h2 ls2 C M (?pc1+1) v xa vs frs
                    (I - pcs (compxE2 e pc (size vs)))" by fact
      ultimately obtain pc2 where
        pc2: "?pc1+1 ≤ pc2 ∧ pc2 < ?pc1' ∧
              ¬ caught P pc2 h2 xa (compxE2 c (?pc1+1) (size vs))" and
        eval2: "P \<turnstile> ?σ1 -jvm-> handle P C M xa h2 vs ls2 pc2 frs"
        using WhileBodyThrow1.prems by (fastsimp simp:Int_Un_distrib)
      have "?H pc2" using pc2 jvm_trans[OF eval1 eval2]     by auto
      thus "∃pc2. ?H pc2" by iprover
    qed
  qed
next
  case (Throw1 e h0 ls0 a h1 ls1)
  let ?pc = "pc + size(compE2 e)"
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm by simp
  next
    show ?Err (is "?throw --> (∃pc1. ?H pc1)")
    proof
      assume ?throw
      hence "P \<turnstile> (None, h0, (vs, ls0, C, M, pc) # frs) -jvm->
                 (None, h1, (Addr xa#vs, ls1, C, M, ?pc) # frs)"
        using Throw1 by fastsimp
      also have "P \<turnstile> … -jvm-> handle P C M xa h1 (Addr xa#vs) ls1 ?pc frs"
        using Throw1.prems by(auto simp add:handle_def)
      also have "handle P C M xa h1 (Addr xa#vs) ls1 ?pc frs =
                 handle P C M xa h1 vs ls1 ?pc frs"
        using Throw1.prems by(auto simp add:handle_Cons)
      finally have "?H ?pc" by simp
      thus "∃pc1. ?H pc1" by iprover
    qed
  qed
next
  case (ThrowNull1 e h0 ls0 h1 ls1)
  let ?pc = "pc + size(compE2 e)"
  let ?xa = "addr_of_sys_xcpt NullPointer"
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm by simp
  next
    show ?Err (is "?throw --> (∃pc1. ?H pc1)")
    proof
      assume throw: ?throw
      have "P \<turnstile> (None, h0, (vs, ls0, C, M, pc) # frs) -jvm->
                 (None, h1, (Null#vs, ls1, C, M, ?pc) # frs)"
        using ThrowNull1 by fastsimp
      also have "P \<turnstile> … -jvm->  handle P C M ?xa h1 (Null#vs) ls1 ?pc frs"
        using ThrowNull1.prems by(auto simp add:handle_def)
      also have "handle P C M ?xa h1 (Null#vs) ls1 ?pc frs =
                 handle P C M ?xa h1 vs ls1 ?pc frs"
        using ThrowNull1.prems by(auto simp add:handle_Cons)
      finally have "?H ?pc" using throw by simp
      thus "∃pc1. ?H pc1" by iprover
    qed
  qed
next
  case ThrowThrow1 thus ?case by fastsimp
next
  case (Try1 e1 h0 ls0 v1 h1 ls1 Ci i e2)
  let ?pc1 = "pc + length(compE2 e1)"
  let ?pc1' = "?pc1 + 2 + length(compE2 e2)"
  have "P,C,M \<rhd> compxE2 (try e1 catch(Ci i) e2) pc (size vs) / I,size vs" by fact
  hence "P,C,M \<rhd> compxE2 e1 pc (size vs) /
                 {pc..<pc + length (compE2 e1)},size vs"
    using Try1.prems by (fastsimp simp:beforex_def split:split_if_asm)
  hence "P \<turnstile> (None,h0,(vs,ls0,C,M,pc)#frs) -jvm->
             (None,h1,(v1#vs,ls1,C,M,?pc1)#frs)" using Try1 by auto
  also have "P \<turnstile> … -jvm-> (None,h1,(v1#vs,ls1,C,M,?pc1')#frs)"
    using Try1.prems by auto
  finally show ?case by (auto simp:add_assoc)
next
  case (TryCatch1 e1 h0 ls0 a h1 ls1 D fs Ci i e2 e2' h2 ls2)
  let ?e = "try e1 catch(Ci i) e2"
  let ?xt = "compxE2 ?e pc (size vs)"
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc)#frs)"
  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') # frs)"
  have I: "{pc..<pc + length (compE2 (try e1 catch(Ci i) e2))} ⊆ I"
   and beforex: "P,C,M \<rhd> ?xt/I,size vs" by fact+
  have "P \<turnstile> ?σ0 -jvm-> (None,h1,((Addr a)#vs,ls1,C,M, ?pc1+1) # frs)"
  proof -
    have "PROP ?P e1 h0 ls0 (Throw a) h1 ls1 C M pc w a vs frs {pc..<pc + length (compE2 e1)}"
      by fact
    moreover have "P,C,M \<rhd> 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)) ∧
             P \<turnstile> ?σ0 -jvm-> handle P C M a h1 vs ls1 pc1 frs"
      using  TryCatch1.prems by auto
    then obtain pc1 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 \<turnstile> ?σ0 -jvm-> handle P C M a h1 vs ls1 pc1 frs" 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 \<turnstile> D \<preceq>* 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 by(simp add:handle_def matches_ex_entry_def)
  qed
  also have "P \<turnstile> … -jvm-> ?σ1" using TryCatch1 by auto
  finally have 1: "P \<turnstile> ?σ0 -jvm-> ?σ1" .
  let ?pc2 = "?pc1' + length(compE2 e2)"
  let ?I2 = "{?pc1' ..< ?pc2}"
  have "P,C,M \<rhd> compxE2 ?e pc (size vs) / I,size vs" by fact
  hence beforex2: "P,C,M \<rhd> 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 e2' h2 ls2 C M ?pc1' 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 \<turnstile> ?σ1 -jvm-> (None,h2,(v#vs,ls2,C,M,?pc2)#frs)"
        using val beforex2 IH2 TryCatch1.prems by auto
      finally show ?trans by(simp add:add_assoc)
    qed
  next
    show ?Err (is "?throw --> (∃pc2. ?H pc2)")
    proof
      assume throw: ?throw
      then obtain pc2 where
        pc2: "?pc1+2 ≤ pc2 ∧ pc2 < ?pc2 ∧
              ¬ caught P pc2 h2 xa (compxE2 e2 ?pc1' (size vs))" and
        2: "P \<turnstile> ?σ1 -jvm-> handle P C M xa h2 vs ls2 pc2 frs"
        using IH2 beforex2 TryCatch1.prems by auto
      have "?H pc2" using pc2 jvm_trans[OF 1 2]
        by (simp add:match_ex_entry) (fastsimp)
      thus "∃pc2. ?H pc2" by iprover
    qed
  qed
next
  case (TryThrow1 e1 h0 ls0 a h1 ls1 D fs Ci i e2)
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc)#frs)"
  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 \<rhd> ?xt/I,size vs" by fact+
  have "PROP ?P e1 h0 ls0 (Throw a) h1 ls1 C M pc w a vs frs {pc..<pc + length (compE2 e1)}" by fact
  moreover have "P,C,M \<rhd> 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)) ∧
             P \<turnstile> ?σ0 -jvm-> handle P C M a h1 vs ls1 pc1 frs"
      using TryThrow1.prems by auto
    then obtain pc1 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 \<turnstile> ?σ0 -jvm-> handle P C M a h1 vs ls1 pc1 frs" by iprover
  show ?case (is "?N ∧ (?eq --> (∃pc2. ?H pc2))")
  proof
    show ?N by simp
  next
    { assume ?eq
      with TryThrow1 pc1_in_e1 pc1_not_caught 0
      have "?H pc1" by (simp add:match_ex_entry) auto
      hence "∃pc2. ?H pc2" by iprover
    }
    thus "?eq --> (∃pc2. ?H pc2)" by iprover
  qed
next
  case Nil1 thus ?case by simp
next
  case (Cons1 e h0 ls0 v h1 ls1 es fs h2 ls2)
  let ?pc1 = "pc + length(compE2 e)"
  let ?σ0 = "(None,h0,(vs,ls0,C,M,pc)#frs)"
  let ?σ1 = "(None,h1,(v#vs,ls1,C,M,?pc1)#frs)"
  have 1: "P \<turnstile> ?σ0 -jvm-> ?σ1" using Cons1 by fastsimp
  let ?pc2 = "?pc1 + length(compEs2 es)"
  have IHs: "PROP ?Ps es h1 ls1 fs h2 ls2 C M ?pc1 (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 \<turnstile> ?σ1 -jvm-> (None,h2,(rev(ws) @ vs,ls2,C,M,?pc2)#frs)"
        using val IHs Cons1.prems by fastsimp
      finally show ?trans by(simp add:add_assoc)
    qed
  next
    show ?Err (is "?throw --> (∃pc2. ?H pc2)")
    proof
      assume throw: ?throw
      then obtain pc2 where
        pc2: "?pc1 ≤ pc2 ∧ pc2 < ?pc2 ∧
              ¬ caught P pc2 h2 xa (compxEs2 es ?pc1 (size vs + 1))" and
        2: "P \<turnstile> ?σ1 -jvm-> handle P C M xa h2 (v#vs) ls2 pc2 frs"
        using IHs Cons1.prems
        by(fastsimp simp:Cons_eq_append_conv neq_Nil_conv)
      have "?H pc2" using Cons1.prems pc2 jvm_trans[OF 1 2]
        by (auto simp add: handle_Cons)
      thus "∃pc2. ?H pc2" by iprover
    qed
  qed
next
  case ConsThrow1 thus ?case by (fastsimp 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

consts exception :: "'a exp => addr option"
recdef exception "{}"
"exception(Throw a) = Some a"
"exception e = None"


lemma comp2_correct:
assumes method: "P1 \<turnstile> C sees M:Ts->T = body in C"
    and eval:   "P1 \<turnstile>1 ⟨body,(h,ls)⟩ => ⟨e',(h',ls')⟩"
shows "compP2 P1 \<turnstile> (None,h,[([],ls,C,M,0)]) -jvm-> (exception e',h',[])"
(*<*)
      (is "_ \<turnstile> ?σ0 -jvm-> ?σ1")
proof -
  let ?P = "compP2 P1"
  have code: "?P,C,M,0 \<rhd> compE2 body" using beforeM[OF method] by auto
  have xtab: "?P,C,M \<rhd> compxE2 body 0 (size[])/{..<size(compE2 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 \<turnstile> ?σ0 -jvm-> (None,h',[([v],ls',C,M,size(compE2 body))])"
      using Jcc[OF eval code xtab] by auto
    also have "?P \<turnstile> … -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(compE2 body) ∧
          ¬ caught ?P pc h' a (compxE2 body 0 0)"
    and 1: "?P \<turnstile> ?σ0 -jvm-> handle ?P C M a h' [] ls' pc []"
      using Jcc[OF eval code xtab] by fastsimp
    from pc have "handle ?P C M a h' [] ls' pc [] = ?σ1" using xtab method
      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