Theory Correctness2

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

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

theory Correctness2
imports "~~/src/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"
   ("(_,_,_,_/ \<rhd> _)" [51,0,0,0,51] 50) where
 "P,C,M,pc \<rhd> is <-> prefixeq is (drop pc (instrs_of P C M))"

definition at :: "jvm_prog => cname => mname => nat => instr => bool"
   ("(_,_,_,_/ \<triangleright> _)" [51,0,0,0,51] 50) where
 "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(fastforce simp add:before_def at_def prefixeq_def drop_Suc drop_tl)(*>*)

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


lemma [simp]: "P,C,M,pc \<rhd> (is⇣1 @ is⇣2) = (P,C,M,pc \<rhd> is⇣1 ∧ P,C,M,pc + size is⇣1 \<rhd> is⇣2)"
(*<*)
apply(simp add:before_def prefixeq_def)
apply(subst add_commute)
apply(simp add: drop_drop[symmetric])
apply fastforce
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 ==>
  compP⇣2 P,D,M,0 \<rhd> compE⇣2 body @ [Return]"
(*<*)
apply(drule sees_method_idemp)
apply(simp add:before_def compP⇣2_def compMb⇣2_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 *}

definition pcs :: "ex_table => nat set"
where
  "pcs xt  ≡  \<Union>(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)}"
(*<*)
apply(induct e and es)
apply (simp_all add:pcs_def)
apply (fastforce 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(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 \<turnstile> C \<preceq>⇧* 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_,/_,/_ \<rhd>/ _ /'/ _,/_)" [51,0,0,0,0,51] 50) where
  "P,C,M \<rhd> 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_,_,_ \<triangleright>/ _ '/_,_)" [51,0,0,0,0,51] 50) where
  "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(fastforce simp:beforex_def)(*>*)


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


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


lemma beforex_appendD1:
  "[| P,C,M \<rhd> xt⇣1 @ xt⇣2 @ [(f,t,D,h,d)] / I,d;
    pcs xt⇣1 ⊆ J; J ⊆ I; J ∩ pcs xt⇣2 = {} |]
  ==> P,C,M \<rhd> xt⇣1 / 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 xt⇣2")
 prefer 2 apply blast
apply (auto split:split_if_asm)
done
(*>*)


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


lemma beforexM:
  "P \<turnstile> C sees M: Ts->T = body in D ==>
  compP⇣2 P,D,M \<rhd> compxE⇣2 body 0 0/{..<size(compE⇣2 body)},0"
(*<*)
apply(drule sees_method_idemp)
apply(drule sees_method_compP[where f = compMb⇣2])
apply(simp add:beforex_def compP⇣2_def compMb⇣2_def)
apply(rule_tac x = "[]" in exI)
using pcs_subset apply fastforce
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 xt⇣0")
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]
(*>*)


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 \<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(fastforce dest:match_ex_table_SomeD2 split:nat_diff_split)
done
(*>*)


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 \<turnstile>⇩1 ⟨e,(h⇣0,ls⇣0)⟩ => ⟨ef,(h⇣1,ls⇣1)⟩ ==>
  (!!C M pc v xa vs frs I.
     [| P,C,M,pc \<rhd> compE⇣2 e; P,C,M \<rhd> compxE⇣2 e pc (size vs)/I,size vs;
       {pc..<pc+size(compE⇣2 e)} ⊆ I |] ==>
     (ef = Val v -->
      P \<turnstile> (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 \<turnstile> (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 \<turnstile>⇩1 ⟨es,(h⇣0,ls⇣0)⟩ [=>] ⟨fs,(h⇣1,ls⇣1)⟩ ==>
    (!!C M pc ws xa es' vs frs I.
      [| P,C,M,pc \<rhd> compEs⇣2 es; P,C,M \<rhd> compxEs⇣2 es pc (size vs)/I,size vs;
       {pc..<pc+size(compEs⇣2 es)} ⊆ I |] ==>
      (fs = map Val ws -->
       P \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> … -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 \<turnstile> (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 \<turnstile> … -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 \<turnstile> (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 \<turnstile> … -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 \<turnstile> (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 \<turnstile> (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 \<turnstile> … -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 \<turnstile> … -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 \<turnstile> (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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> (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 \<turnstile> … -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 \<turnstile> (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 \<turnstile> … -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 \<turnstile> (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 \<turnstile> … -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 \<turnstile> (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 \<turnstile> … -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 \<turnstile> … -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 \<turnstile> (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 \<turnstile> … -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 \<turnstile> … -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 \<turnstile> (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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile>⇩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 \<turnstile> ?σ⇣0 -jvm-> ?σ⇣1" using Call⇣1 by fastforce
  also have "P \<turnstile> … -jvm-> ?σ⇣2" using IH_es Call⇣1.prems by fastforce
  also have "P \<turnstile> … -jvm-> ?σ⇣2'"
    using Call⇣1 by(auto simp add: nth_append compMb⇣2_def)
  finally have 1: "P \<turnstile> ?σ⇣0 -jvm-> ?σ⇣2'".
  have "P⇣1 \<turnstile> Ca sees M': Ts->T = body in D" by fact
  then have M'_in_D: "P⇣1 \<turnstile> D sees M': Ts->T = body in D"
    by(rule sees_method_idemp) 
  hence M'_code: "compP⇣2 P⇣1,D,M',0 \<rhd> compE⇣2 body @ [Return]"
    and M'_xtab: "compP⇣2 P⇣1,D,M' \<rhd> 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 \<turnstile> ?σ⇣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 \<turnstile> … -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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile>⇩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 \<turnstile> (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 \<turnstile> … -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 \<turnstile> … -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 \<turnstile> ?σ⇣0 -jvm-> (None,h⇣1,(w#vs,ls⇣1,C,M,?pc⇣1)#frs)"
    using Seq⇣1 by fastforce
  also have "P \<turnstile> … -jvm-> ?σ⇣1" using Seq⇣1 by auto
  finally have eval⇣1: "P \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> … -jvm-> ?σ⇣1" using CondT⇣1 by auto
  finally have eval⇣1: "P \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> … -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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> … -jvm-> ?σ⇣1" using CondF⇣1 by auto
  finally have eval⇣1: "P \<turnstile> ?σ⇣0 -jvm-> ?σ⇣1".
  show ?case (is "?Norm ∧ ?Err")
  proof
    show ?Norm (is "?val --> ?trans")
    proof
      assume val: ?val
      note eval⇣1
      also have "P \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> (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 \<turnstile> … -jvm-> (None,h⇣1,(vs,ls⇣1,C,M,?pc')#frs)"
    using WhileF⇣1 by (auto simp:add_assoc)
  also have "P \<turnstile> … -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 \<turnstile> ?σ⇣0 -jvm-> (None,h⇣1,(Bool True#vs,ls⇣1,C,M,?pc)#frs)"
    using WhileT⇣1 by fastforce
  also have "P \<turnstile> … -jvm-> (None,h⇣1,(vs,ls⇣1,C,M,?pc+1)#frs)"
    using WhileT⇣1.prems by auto
  also have "P \<turnstile> … -jvm-> (None,h⇣2,(v⇣1#vs,ls⇣2,C,M,?pc')#frs)"
    using WhileT⇣1 by(fastforce)
  also have "P \<turnstile> … -jvm-> ?σ⇣2" using WhileT⇣1.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,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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> … -jvm-> ?σ⇣1" using  WhileBodyThrow⇣1 by auto
  finally have eval⇣1: "P \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> (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 \<turnstile> … -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 \<turnstile> (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 \<turnstile> … -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 \<rhd> compxE⇣2 (try e⇣1 catch(Ci i) e⇣2) pc (size vs) / I,size vs" by fact
  hence "P,C,M \<rhd> 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:split_if_asm)
  hence "P \<turnstile> (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 \<turnstile> … -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 \<rhd> ?xt/I,size vs" by fact+
  have "P \<turnstile> ?σ⇣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 \<rhd> 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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> D \<preceq>⇧* 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 \<turnstile> … -jvm-> ?σ⇣1" using TryCatch⇣1 by auto
  finally have 1: "P \<turnstile> ?σ⇣0 -jvm-> ?σ⇣1" .
  let ?pc⇣2 = "?pc⇣1' + length(compE⇣2 e⇣2)"
  let ?I⇣2 = "{?pc⇣1' ..< ?pc⇣2}"
  have "P,C,M \<rhd> compxE⇣2 ?e pc (size vs) / I,size vs" by fact
  hence beforex⇣2: "P,C,M \<rhd> 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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<rhd> ?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 \<rhd> 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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> ?σ⇣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 \<turnstile> C sees M:Ts->T = body in C"
    and eval:   "P⇣1 \<turnstile>⇩1 ⟨body,(h,ls)⟩ => ⟨e',(h',ls')⟩"
shows "compP⇣2 P⇣1 \<turnstile> (None,h,[([],ls,C,M,0)]) -jvm-> (exception e',h',[])"
(*<*)
      (is "_ \<turnstile> ?σ⇣0 -jvm-> ?σ⇣1")
proof -
  let ?P = "compP⇣2 P⇣1"
  have code: "?P,C,M,0 \<rhd> compE⇣2 body" using beforeM[OF method] by auto
  have xtab: "?P,C,M \<rhd> 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 \<turnstile> ?σ⇣0 -jvm-> (None,h',[([v],ls',C,M,size(compE⇣2 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(compE⇣2 body) ∧
          ¬ caught ?P pc h' a (compxE⇣2 body 0 0)"
    and 1: "?P \<turnstile> ?σ⇣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