Theory BVSpecTypeSafe

Up to index of Isabelle/HOL/arrays

theory BVSpecTypeSafe = Correct:
(*  Title:      HOL/MicroJava/BV/BVSpecTypeSafe.thy
    ID:         $Id: BVSpecTypeSafe.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* \isaheader{BV Type Safety Proof}\label{sec:BVSpecTypeSafe} *}

theory BVSpecTypeSafe = Correct:

text {*
  This theory contains proof that the specification of the bytecode
  verifier only admits type safe programs.  
*}

section {* Preliminaries *}

text {*
  Simp and intro setup for the type safety proof:
*}
lemmas defs1 = correct_state_def correct_frame_def wt_instr_def 
               eff_def norm_eff_def eff_bool_def

lemmas correctE = correct_stateE2 correct_frameE

declare eff_defs [simp del]


lemmas [simp del] = split_paired_All


text {*
  If we have a welltyped program and a conforming state, we
  can directly infer that the current instruction is well typed:
*}
lemma wt_jvm_prog_impl_wt_instr_cor:
  "\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
      G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk> 
  \<Longrightarrow> wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc"
  apply (elim correct_stateE correct_frameE)
  apply simp
  apply (blast intro: wt_jvm_prog_impl_wt_instr)
  done


section {* Exception Handling *}

text {*
  Exceptions don't touch anything except the stack:
*}
lemma exec_instr_xcpt:
  "(fst (exec_instr i G hp ihp stk vars Cl sig pc z frs) = Some xcp)
  = (\<exists>stk'. exec_instr i G hp ihp stk vars Cl sig pc z frs =
            (Some xcp, hp, ihp, (stk', vars, Cl, sig, pc, z)#frs))"
  by (cases i, auto simp add: split_beta split: split_if_asm)


text {*
  Relates @{text match_any} from the Bytecode Verifier with 
  @{text match_exception_table} from the operational semantics:
*}
lemma in_match_any:
  "match_exception_table G xcpt pc et = Some pc' \<Longrightarrow> 
  \<exists>C. C \<in> set (match_any G pc et) \<and> G \<turnstile> xcpt \<preceq>C C \<and> 
      match_exception_table G C pc et = Some pc'"
  (is "PROP ?P et" is "?match et \<Longrightarrow> ?match_any et")
proof (induct et)  
  show "PROP ?P []" by simp

  fix e es
  assume IH: "PROP ?P es"
  assume match: "?match (e#es)"

  obtain start_pc end_pc handler_pc catch_type where
    [simp]: "e = (start_pc, end_pc, handler_pc, catch_type)" by (cases e)

  from IH match
  show "?match_any (e#es)" 
  proof (cases "match_exception_entry G xcpt pc e")
    case False
    with match
    have "match_exception_table G xcpt pc es = Some pc'" by simp
    with IH
    obtain C where
      set: "C \<in> set (match_any G pc es)" and
      C:   "G \<turnstile> xcpt \<preceq>C C" and
      m:   "match_exception_table G C pc es = Some pc'" by blast

    from set
    have "C \<in> set (match_any G pc (e#es))" by simp
    moreover
    from False C
    have "¬ match_exception_entry G C pc e"
      by - (erule contrapos_nn, 
            auto simp add: match_exception_entry_def elim: rtrancl_trans)
    with m
    have "match_exception_table G C pc (e#es) = Some pc'" by simp
    moreover note C
    ultimately
    show ?thesis by blast
  next
    case True with match
    have "match_exception_entry G catch_type pc e"
      by (simp add: match_exception_entry_def)
    moreover
    from True match
    obtain 
      "start_pc \<le> pc" 
      "pc < end_pc" 
      "G \<turnstile> xcpt \<preceq>C catch_type" 
      "handler_pc = pc'" 
      by (simp add: match_exception_entry_def)
    ultimately
    show ?thesis by auto
  qed
qed

lemma match_et_imp_match:
  "match_exception_table G X pc et = Some handler
  \<Longrightarrow> match G X pc et = [X]"
  apply (simp add: match_some_entry)
  apply (induct et)
  apply (auto split: split_if_asm)
  done

lemma imageE2:
  "x \<in> A \<Longrightarrow> y = f x \<Longrightarrow> y \<in> f ` A"
  by simp


lemma subcls_obj [iff]: 
  "(G \<turnstile> Object \<preceq>C C) = (C = Object)"
  apply auto
  apply (erule converse_rtranclE, simp)
  apply (erule subcls1.elims)
  apply simp
  done


text {*
  We can prove separately that the recursive search for exception
  handlers (@{text find_handler}) in the frame stack results in 
  a conforming state (if there was no matching exception handler 
  in the current frame). We require that the exception is a valid,
  initialized heap address, and that the state before the exception 
  occured conforms. 
*}
lemma uncaught_xcpt_correct:
  "\<And>f. \<lbrakk> wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T; is_init hp ihp xcp;
      G,phi \<turnstile>JVM (None, hp, ihp, f#frs)\<surd> \<rbrakk>
  \<Longrightarrow> G,phi \<turnstile>JVM (find_handler G (Some xcp) hp ihp frs)\<surd>" 
  (is "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?init; ?correct (None, hp, ihp, f#frs) \<rbrakk> \<Longrightarrow> ?correct (?find frs)")
proof (induct frs) 
  -- "the base case is trivial, as it should be"
  show "?correct (?find [])" by (simp add: correct_state_def)

  -- "we will need both forms @{text wt_jvm_prog} and @{text wf_prog} later"
  assume wt: ?wt 
  then obtain mb where wf: "wf_prog mb G" by (simp add: wt_jvm_prog_def)

  -- "these do not change in the induction:"
  assume adr: ?adr
  assume hp: ?hp
  assume init: ?init
  
  -- "the assumption for the cons case:"
  fix f f' frs'  assume cr: "?correct (None, hp, ihp, f#f'#frs')" 

  -- "the induction hypothesis as produced by Isabelle, immediatly simplified
    with the fixed assumptions above"
  assume "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?init; ?correct (None, hp, ihp, f#frs') \<rbrakk> \<Longrightarrow> ?correct (?find frs')"  
  with wt adr hp init 
  have IH: "\<And>f. ?correct (None, hp, ihp, f#frs') \<Longrightarrow> ?correct (?find frs')" by blast

  obtain stk loc C sig pc r where f' [simp]: "f' = (stk,loc,C,sig,pc,r)" 
    by (cases f') 
  
  from cr have cr': "?correct (None, hp, ihp, f'#frs')" 
    by (unfold correct_state_def, clarsimp) blast
  then obtain rT maxs maxl ins et where
    meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
    by (fastsimp elim!: correct_stateE)

  hence [simp]: "ex_table_of (snd (snd (the (method (G, C) sig)))) = et" by simp

  show "?correct (?find (f'#frs'))" 
  proof (cases "match_exception_table G (cname_of hp xcp) pc et")
    case None
    with cr' IH 
    show ?thesis by simp
  next
    fix handler_pc 
    assume match: "match_exception_table G (cname_of hp xcp) pc et = Some handler_pc"
    (is "?match (cname_of hp xcp) = _")

    from wt meth cr' [simplified]
    have wti: "wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc" 
      by (rule wt_jvm_prog_impl_wt_instr_cor)

    from cr meth
    obtain C' mn pts ST LT z where
      ins: "ins ! pc = Invoke C' mn pts \<or> ins ! pc = Invoke_special C' mn pts" and
      phi: "((ST, LT),z) \<in> phi C sig ! pc" and
      frm: "correct_frame G hp ihp (ST,LT) maxl ins (stk, loc, C, sig, pc, r)" and
      frms: "correct_frames G hp ihp phi rT sig z r frs'" 
      by (simp add: correct_state_def) fast

    from match
    obtain D where
      in_any: "D \<in> set (match_any G pc et)" and
      D:      "G \<turnstile> cname_of hp xcp \<preceq>C D" and
      match': "?match D = Some handler_pc"
      by (blast dest: in_match_any)    

    from ins have "xcpt_names (ins ! pc, G, pc, et) = match_any G pc et" by auto
    with wti phi have 
      "\<forall>D\<in>set (match_any G pc et). the (?match D) < length ins \<and> 
      (([Init (Class D)], LT),z) \<in> phi C sig!the (?match D)"
      apply -
      apply (unfold wt_instr_def xcpt_eff_def eff_def)
      apply clarsimp 
      apply (drule bspec)
      apply (rule UnI2)
      apply (rule imageI)
      apply assumption
      apply clarsimp
      apply (erule subsetD)
      apply (erule imageE2)
      apply simp
      done
    with in_any match' obtain
      pc: "handler_pc < length ins" 
      "(([Init (Class D)], LT),z) \<in> phi C sig ! handler_pc"
      by auto
    
    from frm obtain
     len: "length loc = 1+length (snd sig)+maxl" and
     loc: "approx_loc G hp ihp loc LT" and
     csi: "consistent_init stk loc (ST, LT) ihp" and
     cor: "(fst sig = init \<longrightarrow>
            corresponds stk loc (ST, LT) ihp (fst r) (PartInit C) \<and>
            (\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and> (ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C')))))" 
      by (fastsimp elim!: correct_frameE)

    let ?f = "([xcp], loc, C, sig, handler_pc, r)"    
    have "correct_frame G hp ihp ([Init (Class D)], LT) maxl ins ?f"
    proof -
      from D adr hp
      have "G,hp \<turnstile> xcp ::\<preceq> Class D" 
        by (auto simp add: conf_def obj_ty_def split: heap_entry.split)
      with init 
      have "approx_val G hp ihp xcp (OK (Init (Class D)))" 
        by (simp add: approx_val_def iconf_def)
      with len pc csi cor loc
      show ?thesis 
        by (simp add: correct_frame_def consistent_init_xcp)
           (blast intro: corresponds_xcp)
    qed 

    with cr' match meth pc frms
    show ?thesis by (unfold correct_state_def) auto
  qed
qed


text {*
  The requirement of lemma @{text uncaught_xcpt_correct} (that
  the exception is a valid, initialized reference on the heap) is always met
  for welltyped instructions and conformant states:
*}
lemma exec_instr_xcpt_hp:
  assumes xcpt: "fst (exec_instr (ins!pc) G hp ihp stk vars Cl sig pc r frs) = Some xcp"
  assumes wt: "wt_instr (ins!pc) G Cl rT (phi C sig) maxs (fst sig=init) (length ins) et pc"
  assumes correct: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
  shows "\<exists>adr T. xcp = Addr adr \<and> hp adr = Some T \<and> is_init hp ihp xcp" 
proof -
  note [simp] = split_beta raise_system_xcpt_def
  note [split] = split_if_asm option.split_asm 
  
  from correct have pre: "preallocated hp ihp" ..
  with xcpt show ?thesis 
  proof (cases "ins!pc")
    case New with xcpt pre
    show ?thesis by (auto dest: new_Addr_OutOfMemory dest!: preallocatedD) 
  next
    case Throw 
    from correct obtain ST LT z where
      "((ST, LT), z) \<in> phi C sig ! pc"
      "approx_stk G hp ihp stk ST"
      by (blast elim: correct_stateE correct_frameE)
    with Throw wt xcpt pre show ?thesis
      apply (unfold wt_instr_def) 
      apply clarsimp 
      apply (drule bspec, assumption)
      apply (clarsimp simp add: approx_val_def iconf_def)
      apply (blast dest: non_npD)+
      done
  next
    case Invoke_special with xcpt pre
    show ?thesis by (auto dest: new_Addr_OutOfMemory dest!: preallocatedD) 
  next
    case ArrNew with xcpt pre
    show ?thesis by (auto dest: new_Addr_OutOfMemory dest!: preallocatedD) 
  qed (auto dest!: preallocatedD)
qed


lemma cname_of_xcp [intro]:
  "\<lbrakk>preallocated hp ihp; xcp = Addr (XcptRef x)\<rbrakk> \<Longrightarrow> cname_of hp xcp = Xcpt x"
  by (auto elim: preallocatedE [of hp ihp x])

lemma prealloc_is_init [simp]:
  "preallocated hp ihp \<Longrightarrow> is_init hp ihp (Addr (XcptRef x))"
  by (drule preallocatedD) blast


thm wt_jvm_progD [intro?]

lemma wt_jvm_progE [intro?]:
  "wt_jvm_prog G phi \<Longrightarrow> (\<And>wt. wf_prog wt G \<Longrightarrow> P) \<Longrightarrow> P"
  by (simp add: wt_jvm_prog_def)

text {*
  Finally we can state that the next state always conforms when an exception occured:
*}
lemma xcpt_correct:
  assumes wtp: "wt_jvm_prog G phi"
  assumes meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
  assumes wt: "wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig=init) (length ins) et pc"
  assumes xp: "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = Some xcp"
  assumes s': "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
  assumes correct: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"

  shows "G,phi \<turnstile>JVM state'\<surd>"
proof -
  from wtp obtain wfmb where wf: "wf_prog wfmb G" ..

  note xp' = meth s' xp

  note wtp
  moreover
  from xp wt correct
  obtain adr T where
    adr: "xcp = Addr adr" "hp adr = Some T" "is_init hp ihp xcp"
    by (blast dest: exec_instr_xcpt_hp)
  moreover
  note correct
  ultimately
  have "G,phi \<turnstile>JVM find_handler G (Some xcp) hp ihp frs \<surd>" by (rule uncaught_xcpt_correct)
  with xp'
  have "match_exception_table G (cname_of hp xcp) pc et = None \<Longrightarrow> ?thesis" 
    (is "?m (cname_of hp xcp) = _ \<Longrightarrow> _" is "?match = _ \<Longrightarrow> _")
    by (clarsimp simp add: exec_instr_xcpt split_beta)
  moreover
  { fix handler assume some_handler: "?match = Some handler"
    
    from correct meth obtain ST LT z where
      hp_ok:  "G \<turnstile>h hp \<surd>" and
      h_ini:  "h_init G hp ihp" and
      prehp:  "preallocated hp ihp" and
      class:  "is_class G C" and
      phi_pc: "((ST,LT),z) \<in> phi C sig ! pc" and
      frame:  "correct_frame G hp ihp (ST, LT) maxl ins (stk, loc, C, sig, pc, r)" and
      frames: "correct_frames G hp ihp phi rT sig z r frs"
      ..

    from frame obtain 
      stk: "approx_stk G hp ihp stk ST" and
      loc: "approx_loc G hp ihp loc LT" and
      pc:  "pc < length ins" and
      len: "length loc = length (snd sig)+maxl+1" and
      cin: "consistent_init stk loc (ST, LT) ihp" and
      cor: "fst sig = init \<longrightarrow>
      corresponds stk loc (ST, LT) ihp (fst r) (PartInit C) \<and>
      (\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and> (ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))"
      ..
    
    from wt obtain
      eff: "\<forall>(pc', s')\<in>set (xcpt_eff (ins!pc) G pc (phi C sig!pc) et).
             pc' < length ins \<and> s' \<subseteq> phi C sig!pc'"
      by (simp add: wt_instr_def eff_def)
    
    from some_handler xp'
    have state': 
      "state' = (None, hp, ihp, ([xcp], loc, C, sig, handler, r)#frs)"
      by (cases "ins!pc", auto simp add: raise_system_xcpt_def split_beta  
                               split: split_if_asm) -- "takes long!"

    let ?f' = "([xcp], loc, C, sig, handler, r)"

    from eff xp'
    obtain ST' where
      phi_pc': "((ST', LT),z) \<in> phi C sig ! handler" and
      frame': "correct_frame G hp ihp (ST',LT) maxl ins ?f'" 
    proof (cases "ins!pc")
      case Return -- "can't generate exceptions:"
      with xp' have False by (simp add: split_beta split: split_if_asm)
      thus ?thesis ..
    next
      let ?C = "Init (Class (Xcpt OutOfMemory))"
      case New      
      with some_handler xp'
      have xcp: "xcp = Addr (XcptRef OutOfMemory)"
        by (simp add: raise_system_xcpt_def split_beta new_Addr_OutOfMemory)
      with prehp have "cname_of hp xcp = Xcpt OutOfMemory" ..
      with New some_handler phi_pc eff 
      have
        phi': "(([?C], LT),z) \<in> phi C sig ! handler" and
        pc':  "handler < length ins"
        by (auto simp add: xcpt_eff_def match_et_imp_match) 
      note phi'
      moreover
      { from xcp prehp
        have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt OutOfMemory)" 
          by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
        with xcp prehp 
        have "approx_val G hp ihp xcp (OK ?C)"
          by (simp add: iconf_def approx_val_def)
        with wf pc' len loc cor cin
        have "correct_frame G hp ihp ([?C],LT) maxl ins ?f'" 
          by (simp add: consistent_init_xcp correct_frame_def)
             (blast intro: corresponds_xcp)
      }
      ultimately
      show ?thesis by (rule that) 
    next 
      let ?C = "Init (Class (Xcpt NullPointer))"
      case Getfield
      with some_handler xp'
      have xcp: "xcp = Addr (XcptRef NullPointer)"
        by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
      with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
      with Getfield some_handler phi_pc eff 
      have
        phi': "(([?C],LT),z) \<in> phi C sig ! handler" and
        pc':  "handler < length ins"
        by (auto simp add: xcpt_eff_def match_et_imp_match) 
      note phi'
      moreover
      { from xcp prehp
        have "approx_val G hp ihp xcp (OK ?C)"
          by (auto simp add: iconf_def conf_def obj_ty_def approx_val_def dest!: preallocatedD)
        with wf pc' len loc cor cin
        have "correct_frame G hp ihp ([?C],LT) maxl ins ?f'" 
          by (simp add: consistent_init_xcp correct_frame_def)
             (blast intro: corresponds_xcp)
      }
      ultimately
      show ?thesis by (rule that)
    next
      let ?C = "Init (Class (Xcpt NullPointer))"
      case Putfield
      with some_handler xp'
      have xcp: "xcp = Addr (XcptRef NullPointer)"
        by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
      with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
      with Putfield some_handler phi_pc eff 
      have
        phi': "(([?C],LT),z) \<in> phi C sig ! handler" and
        pc':  "handler < length ins"
        by (auto simp add: xcpt_eff_def match_et_imp_match) 
      note phi'
      moreover
      { from xcp prehp
        have "approx_val G hp ihp xcp (OK ?C)"
          by (auto simp add: iconf_def conf_def obj_ty_def approx_val_def dest!: preallocatedD)
        with wf pc' len loc cor cin
        have "correct_frame G hp ihp ([?C],LT) maxl ins ?f'" 
          by (simp add: consistent_init_xcp correct_frame_def)
             (blast intro: corresponds_xcp)
      }
      ultimately
      show ?thesis by (rule that)
    next
      let ?X = ClassCast
      let ?C = "Init (Class (Xcpt ?X))"
      case Checkcast
      with some_handler xp'
      have xcp: "xcp = Addr (XcptRef ?X)"
        by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
      with prehp have "cname_of hp xcp = Xcpt ?X" ..
      with Checkcast some_handler phi_pc eff 
      have
        phi': "(([?C],LT),z) \<in> phi C sig ! handler" and
        pc':  "handler < length ins"
        by (auto simp add: xcpt_eff_def match_et_imp_match) 
      note phi'
      moreover
      { from xcp prehp
        have "approx_val G hp ihp xcp (OK ?C)"
          by (auto simp add: iconf_def conf_def obj_ty_def approx_val_def dest!: preallocatedD)
        with wf pc' len loc cor cin
        have "correct_frame G hp ihp ([?C],LT) maxl ins ?f'" 
          by (simp add: consistent_init_xcp correct_frame_def)
             (blast intro: corresponds_xcp)
      }
      ultimately
      show ?thesis by (rule that)
    next
      case Invoke
      with phi_pc eff 
      have 
        "\<forall>D\<in>set (match_any G pc et). 
        the (?m D) < length ins \<and> (([Init (Class D)], LT),z) \<in> phi C sig!the (?m D)"
        by (clarsimp simp add: xcpt_eff_def) (fastsimp elim: imageE2)
      moreover
      from some_handler
      obtain D where
        "D \<in> set (match_any G pc et)" and
        D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
        "?m D = Some handler"
        by (blast dest: in_match_any)
      ultimately
      have
        pc':  "handler < length ins" and
        phi': "(([Init (Class D)], LT), z) \<in> phi C sig ! handler"
        by auto

      from xp wt correct
      obtain addr T where
        xcp: "xcp = Addr addr" "hp addr = Some T" "is_init hp ihp xcp"
        by (blast dest: exec_instr_xcpt_hp)
      note phi'
      moreover
      { from xcp D
        have "approx_val G hp ihp xcp (OK (Init (Class D)))"
          by (auto simp add: iconf_def conf_def obj_ty_def approx_val_def dest!: preallocatedD split: heap_entry.split)
        with wf pc' len loc cor cin
        have "correct_frame G hp ihp ([Init (Class D)],LT) maxl ins ?f'" 
          by (simp add: consistent_init_xcp correct_frame_def)
             (blast intro: corresponds_xcp)
      }
      ultimately
      show ?thesis by (rule that)
    next
      case Invoke_special
      with phi_pc eff 
      have 
        "\<forall>D\<in>set (match_any G pc et). 
        the (?m D) < length ins \<and> (([Init (Class D)], LT),z) \<in> phi C sig!the (?m D)"
        by (clarsimp simp add: xcpt_eff_def) (fastsimp elim: imageE2)
      moreover
      from some_handler
      obtain D where
        "D \<in> set (match_any G pc et)" and
        D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
        "?m D = Some handler"
        by (blast dest: in_match_any)
      ultimately
      have
        pc':  "handler < length ins" and
        phi': "(([Init (Class D)], LT), z) \<in> phi C sig ! handler"
        by auto

      from xp wt correct
      obtain addr T where
        xcp: "xcp = Addr addr" "hp addr = Some T" "is_init hp ihp xcp"
        by (blast dest: exec_instr_xcpt_hp)
      note phi'
      moreover
      { from xcp D
        have "approx_val G hp ihp xcp (OK (Init (Class D)))"
          by (auto simp add: iconf_def conf_def obj_ty_def approx_val_def dest!: preallocatedD split: heap_entry.split)
        with wf pc' len loc cor cin
        have "correct_frame G hp ihp ([Init (Class D)],LT) maxl ins ?f'" 
          by (simp add: consistent_init_xcp correct_frame_def)
             (blast intro: corresponds_xcp)
      }
      ultimately
      show ?thesis by (rule that)
    next
      case Throw
      with phi_pc eff 
      have 
        "\<forall>D\<in>set (match_any G pc et). 
        the (?m D) < length ins \<and> (([Init (Class D)], LT),z) \<in> phi C sig!the (?m D)"
        by (clarsimp simp add: xcpt_eff_def) (fastsimp elim: imageE2)
      moreover
      from some_handler
      obtain D where
        "D \<in> set (match_any G pc et)" and
        D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
        "?m D = Some handler"
        by (blast dest: in_match_any)
      ultimately
      have
        pc':  "handler < length ins" and
        phi': "(([Init (Class D)], LT), z) \<in> phi C sig ! handler"
        by auto

      from xp wt correct
      obtain addr T where
        xcp: "xcp = Addr addr" "hp addr = Some T" "is_init hp ihp xcp"
        by (blast dest: exec_instr_xcpt_hp)
      note phi'
      moreover
      { from xcp D
        have "approx_val G hp ihp xcp (OK (Init (Class D)))"
          by (auto simp add: iconf_def conf_def obj_ty_def approx_val_def dest!: preallocatedD split: heap_entry.split)
        with wf pc' len loc cor cin
        have "correct_frame G hp ihp ([Init (Class D)],LT) maxl ins ?f'" 
          by (simp add: consistent_init_xcp correct_frame_def)
             (blast intro: corresponds_xcp)
      }
      ultimately
      show ?thesis by (rule that)
    next
      let ?X1 = OutOfMemory and ?X2 = NegativeArraySize
      let ?C1 = "Init (Class (Xcpt ?X1))" and ?C2 = "Init (Class (Xcpt ?X2))"
      case ArrNew
      with some_handler xp'
      have "xcp = Addr (XcptRef ?X1) \<or> xcp = Addr (XcptRef ?X2)"
        by (simp add: raise_system_xcpt_def split_beta new_Addr_OutOfMemory split: split_if_asm)
      moreover
      { assume xcp: "xcp = Addr (XcptRef ?X1)"        
        with prehp have "cname_of hp xcp = Xcpt ?X1" ..
        with ArrNew some_handler phi_pc eff 
        have
          phi': "(([?C1], LT),z) \<in> phi C sig ! handler" and
          pc':  "handler < length ins"
          by (auto simp add: xcpt_eff_def match_et_imp_match) 
        note phi'
        moreover {
          from xcp prehp
          have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt ?X1)" 
            by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
          with xcp prehp 
          have "approx_val G hp ihp xcp (OK ?C1)"
            by (simp add: iconf_def approx_val_def)
          with wf pc' len loc cor cin
          have "correct_frame G hp ihp ([?C1],LT) maxl ins ?f'" 
            by (simp add: consistent_init_xcp correct_frame_def)
               (blast intro: corresponds_xcp) 
        }
        ultimately
        have ?thesis by (rule that)
      } 
      moreover {
        assume xcp: "xcp = Addr (XcptRef ?X2)"        
        with prehp have "cname_of hp xcp = Xcpt ?X2" ..
        with ArrNew some_handler phi_pc eff 
        have
          phi': "(([?C2], LT),z) \<in> phi C sig ! handler" and
          pc':  "handler < length ins"
          by (auto simp add: xcpt_eff_def match_et_imp_match) 
        note phi'
        moreover {
          from xcp prehp
          have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt ?X2)" 
            by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
          with xcp prehp 
          have "approx_val G hp ihp xcp (OK ?C2)"
            by (simp add: iconf_def approx_val_def)
          with wf pc' len loc cor cin
          have "correct_frame G hp ihp ([?C2],LT) maxl ins ?f'" 
            by (simp add: consistent_init_xcp correct_frame_def)
               (blast intro: corresponds_xcp) 
        }
        ultimately
        have ?thesis by (rule that)
      }
      ultimately show ?thesis by blast
    next
      let ?X1 = ArrayIndexOutOfBounds and ?X2 = NullPointer
      let ?C1 = "Init (Class (Xcpt ?X1))" and ?C2 = "Init (Class (Xcpt ?X2))"
      case ArrLoad
      with some_handler xp'
      have "xcp = Addr (XcptRef ?X1) \<or> xcp = Addr (XcptRef ?X2)"
        by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
      moreover
      { assume xcp: "xcp = Addr (XcptRef ?X1)"        
        with prehp have "cname_of hp xcp = Xcpt ?X1" ..
        with ArrLoad some_handler phi_pc eff 
        have
          phi': "(([?C1], LT),z) \<in> phi C sig ! handler" and
          pc':  "handler < length ins"
          by (auto simp add: xcpt_eff_def match_et_imp_match) 
        note phi'
        moreover {
          from xcp prehp
          have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt ?X1)" 
            by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
          with xcp prehp 
          have "approx_val G hp ihp xcp (OK ?C1)"
            by (simp add: iconf_def approx_val_def)
          with wf pc' len loc cor cin
          have "correct_frame G hp ihp ([?C1],LT) maxl ins ?f'" 
            by (simp add: consistent_init_xcp correct_frame_def)
               (blast intro: corresponds_xcp) 
        }
        ultimately
        have ?thesis by (rule that)
      } 
      moreover {
        assume xcp: "xcp = Addr (XcptRef ?X2)"        
        with prehp have "cname_of hp xcp = Xcpt ?X2" ..
        with ArrLoad some_handler phi_pc eff 
        have
          phi': "(([?C2], LT),z) \<in> phi C sig ! handler" and
          pc':  "handler < length ins"
          by (auto simp add: xcpt_eff_def match_et_imp_match) 
        note phi'
        moreover {
          from xcp prehp
          have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt ?X2)" 
            by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
          with xcp prehp 
          have "approx_val G hp ihp xcp (OK ?C2)"
            by (simp add: iconf_def approx_val_def)
          with wf pc' len loc cor cin
          have "correct_frame G hp ihp ([?C2],LT) maxl ins ?f'" 
            by (simp add: consistent_init_xcp correct_frame_def)
               (blast intro: corresponds_xcp) 
        }
        ultimately
        have ?thesis ..
      }
      ultimately show ?thesis by blast
    next
      let ?X1 = ArrayIndexOutOfBounds and ?X2 = NullPointer and ?X3 = ArrayStore
      let ?C1 = "Init (Class (Xcpt ?X1))" and ?C2 = "Init (Class (Xcpt ?X2))" 
      let ?C3 = "Init (Class (Xcpt ?X3))"
      case ArrStore
      with some_handler xp'
      have "xcp = Addr (XcptRef ?X1) \<or> xcp = Addr (XcptRef ?X2) \<or> xcp = Addr (XcptRef ?X3)"
        by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
      moreover
      { assume xcp: "xcp = Addr (XcptRef ?X1)"        
        with prehp have "cname_of hp xcp = Xcpt ?X1" ..
        with ArrStore some_handler phi_pc eff 
        have
          phi': "(([?C1], LT),z) \<in> phi C sig ! handler" and
          pc':  "handler < length ins"
          by (auto simp add: xcpt_eff_def match_et_imp_match) 
        note phi'
        moreover {
          from xcp prehp
          have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt ?X1)" 
            by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
          with xcp prehp 
          have "approx_val G hp ihp xcp (OK ?C1)"
            by (simp add: iconf_def approx_val_def)
          with wf pc' len loc cor cin
          have "correct_frame G hp ihp ([?C1],LT) maxl ins ?f'" 
            by (simp add: consistent_init_xcp correct_frame_def)
               (blast intro: corresponds_xcp) 
        }
        ultimately
        have ?thesis ..
      } 
      moreover {
        assume xcp: "xcp = Addr (XcptRef ?X2)"        
        with prehp have "cname_of hp xcp = Xcpt ?X2" ..
        with ArrStore some_handler phi_pc eff 
        have
          phi': "(([?C2], LT),z) \<in> phi C sig ! handler" and
          pc':  "handler < length ins"
          by (auto simp add: xcpt_eff_def match_et_imp_match) 
        note phi'
        moreover {
          from xcp prehp
          have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt ?X2)" 
            by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
          with xcp prehp 
          have "approx_val G hp ihp xcp (OK ?C2)"
            by (simp add: iconf_def approx_val_def)
          with wf pc' len loc cor cin
          have "correct_frame G hp ihp ([?C2],LT) maxl ins ?f'" 
            by (simp add: consistent_init_xcp correct_frame_def)
               (blast intro: corresponds_xcp) 
        }
        ultimately
        have ?thesis ..
      }
      moreover {
        assume xcp: "xcp = Addr (XcptRef ?X3)"        
        with prehp have "cname_of hp xcp = Xcpt ?X3" ..
        with ArrStore some_handler phi_pc eff 
        have
          phi': "(([?C3], LT),z) \<in> phi C sig ! handler" and
          pc':  "handler < length ins"
          by (auto simp add: xcpt_eff_def match_et_imp_match) 
        note phi'
        moreover {
          from xcp prehp
          have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt ?X3)" 
            by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
          with xcp prehp 
          have "approx_val G hp ihp xcp (OK ?C3)"
            by (simp add: iconf_def approx_val_def)
          with wf pc' len loc cor cin
          have "correct_frame G hp ihp ([?C3],LT) maxl ins ?f'" 
            by (simp add: consistent_init_xcp correct_frame_def)
               (blast intro: corresponds_xcp) 
        }
        ultimately
        have ?thesis ..
      }
      ultimately show ?thesis by blast
    next
      let ?C = "Init (Class (Xcpt NullPointer))"
      case ArrLength
      with some_handler xp'
      have xcp: "xcp = Addr (XcptRef NullPointer)"
        by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
      with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
      with ArrLength some_handler phi_pc eff 
      have
        phi': "(([?C],LT),z) \<in> phi C sig ! handler" and
        pc':  "handler < length ins"
        by (auto simp add: xcpt_eff_def match_et_imp_match) 
      note phi'
      moreover
      { from xcp prehp
        have "approx_val G hp ihp xcp (OK ?C)"
          by (auto simp add: iconf_def conf_def obj_ty_def approx_val_def dest!: preallocatedD)
        with wf pc' len loc cor cin
        have "correct_frame G hp ihp ([?C],LT) maxl ins ?f'" 
          by (simp add: consistent_init_xcp correct_frame_def)
             (blast intro: corresponds_xcp)
      }
      ultimately
      show ?thesis ..
    qed auto -- "the other instructions do not generate exceptions" 

    from state' meth hp_ok class frames phi_pc' frame' h_ini prehp 
    have ?thesis by simp (rule correct_stateI) 
  }
  ultimately
  show ?thesis by (cases "?match") blast+ 
qed



section {* Single Instructions *}

text {*
  In this section we look at each single (welltyped) instruction, and
  prove that the state after execution of the instruction still conforms.
  Since we have already handled exceptions above, we can now assume, that
  on exception occurs for this (single step) execution.
*}

lemmas [iff] = not_Err_eq

lemma Load_correct:
"\<lbrakk> wf_prog wt G;
    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
    ins!pc = Load idx; 
    wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
    Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs); 
    G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs1 map_eq_Cons) 
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply clarsimp
apply (clarsimp simp add: approx_loc_def list_all2_conv_all_nth)
apply (erule allE, erule impE, assumption)
apply simp
apply (rule conjI)
 apply (erule consistent_init_loc_nth)
 apply simp
 apply simp
apply clarsimp
apply (frule corresponds_loc_nth)
apply simp
apply assumption
apply (clarsimp simp add: corresponds_def corr_stk_def corr_loc_cons)
done


lemma Store_correct:
"\<lbrakk> wf_prog wt G;
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
  ins!pc = Store idx;
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs);
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)  
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply clarsimp
apply (blast intro: approx_loc_imp_approx_loc_subst 
                    consistent_init_store 
                    corresponds_var_upd)
done  


lemma LitPush_correct:
"\<lbrakk> wf_prog wt G;
    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
    ins!pc = LitPush v;
    wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
    Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs);
    G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  apply (elim correctE, assumption)
  apply (clarsimp simp add: defs1 approx_val_def iconf_def init_le_Init 
                            map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply clarsimp
apply (simp add: approx_val_def iconf_def)
  apply (rule conjI)
  apply (fastsimp intro: conf_litval)
  apply (rule conjI)
   apply (clarsimp simp add: is_init_def split: val.split)
  apply (rule conjI)
   apply (erule consistent_init_Init_stk)  
  apply (rule impI, erule impE, assumption, elim conjE exE)
  apply (simp add: corresponds_stk_cons)
  done

lemma widen_Array_Class2 [iff]:
  "G \<turnstile> T.[] \<preceq> Class C = (C = Object)"
  by (auto simp add: widen_Array_Class)

lemma Cast_conf2:
  "\<lbrakk> wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; 
      G\<turnstile>Class C\<preceq>T; is_class G C\<rbrakk> 
  \<Longrightarrow> G,h\<turnstile>v::\<preceq>T"
  apply (unfold cast_ok_def)
  apply (frule widen_Class)
  apply (elim exE disjE) 
  apply (simp add: null)
  apply (clarsimp simp add: conf_def obj_ty_def split: heap_entry.splits)
  apply (cases v)
  apply (auto intro: rtrancl_trans)
  apply (cases v)
  apply auto
  done


lemmas defs2 = defs1 raise_system_xcpt_def

lemma Checkcast_correct:
"\<lbrakk> wt_jvm_prog G phi;
    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
    ins!pc = Checkcast D; 
    wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
    Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs); 
    G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
    fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons approx_val_def wt_jvm_prog_def
                split: split_if_asm)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply clarsimp

apply (rule conjI)
 apply (clarsimp simp add: approx_val_def iconf_def init_le_Init) 
 apply (blast intro: Cast_conf2)
apply (rule conjI)
 apply (drule consistent_init_pop)
 apply (erule consistent_init_Init_stk)
apply (clarsimp simp add: init_le_Init corresponds_stk_cons)
done

lemma non_np_objD:
  "\<lbrakk>a' \<noteq> Null; G,h \<turnstile> a' ::\<preceq> Class D; field (G, D) F = Some (D, vT); wf_prog b G\<rbrakk> \<Longrightarrow> 
  \<exists>a C fs. a' = Addr a \<and> h a = Some (Obj C fs) \<and> G \<turnstile> C \<preceq>C D"
apply (drule non_npD, assumption)
apply clarsimp
apply (case_tac z)
 apply simp
apply clarsimp
done


lemma Getfield_correct:
"\<lbrakk> wt_jvm_prog G phi;
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
  ins!pc = Getfield F D;
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs); 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
  fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def approx_val_def 
                          iconf_def init_le_Init2)              
apply (drule bspec, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def approx_val_def 
                          iconf_def init_le_Init2
                split: option.split split_if_asm)
apply (frule non_np_objD, rule conf_widen, assumption+)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply (clarsimp simp add: defs2 approx_val_def)
apply (rule conjI) 
 apply (clarsimp simp add: iconf_def init_le_Init)
 apply (rule conjI)
  apply (drule widen_cfs_fields, assumption+)
  apply (simp add: hconf_def oconf_def lconf_def)
  apply (erule allE, erule allE, erule impE, assumption)
  apply (simp (no_asm_use))
  apply (simp add: lconf_def)
  apply (erule allE, erule allE, erule impE, assumption)
  apply clarsimp
 apply (clarsimp simp: is_init_def split: val.split)
 apply (simp add: h_init_def o_init_def l_init_def)
 apply (erule allE, erule allE, erule impE, assumption)
 apply (drule hconfD, assumption)
 apply (drule widen_cfs_fields, assumption+)
 apply (drule oconf_objD, assumption)
 apply (clarsimp simp add: l_init_def)
 apply (erule allE, erule impE) back apply blast
 apply (clarsimp simp add: is_init_def)
apply (clarsimp simp add: init_le_Init corresponds_stk_cons)
apply (blast intro: consistent_init_Init_stk 
                    consistent_init_pop)
done 


lemma Putfield_correct:
"\<lbrakk> wf_prog wt G;
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins!pc = Putfield F D; 
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
  fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
proof -
  assume wf:   "wf_prog wt G"
  assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
  assume ins:  "ins!pc = Putfield F D"
  assume wt:   "wt_instr (ins!pc) G C rT (phi C sig) maxs 
                         (fst sig = init) (length ins) et pc"
  assume exec: "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
  assume conf: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
  assume no_x: "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None"

  from ins conf meth
  obtain ST LT z where
    heap_ok:    "G\<turnstile>h hp\<surd>" and
    pre_alloc:  "preallocated hp ihp" and
    init_ok:    "h_init G hp ihp" and
    phi_pc:     "((ST,LT),z) \<in> phi C sig!pc" and
    is_class_C: "is_class G C" and
    frame:      "correct_frame G hp ihp (ST,LT) maxl ins (stk,loc,C,sig,pc,r)" and
    frames:     "correct_frames G hp ihp phi rT sig z r frs"
    by (fastsimp elim: correct_stateE)

  from phi_pc ins wt
  obtain vT oT vT' tST ST' LT' where 
    ST:      "ST = (Init vT) # (Init oT) # tST" and
    suc_pc:  "Suc pc < length ins" and
    phi_suc: "((tST, LT),z) \<in> phi C sig ! Suc pc" and
    class_D: "is_class G D"  and
    field:   "field (G, D) F = Some (D, vT')" and
    v_less:  "G \<turnstile> Init vT \<preceq>i Init vT'" and
    o_less:  "G \<turnstile> Init oT \<preceq>i Init (Class D)"
    apply (unfold wt_instr_def eff_defs)
    apply clarsimp
    apply (drule bspec, assumption)
    apply clarsimp
    apply (drule subsetD)
    apply (rule imageI, assumption)
    apply (clarsimp simp add: init_le_Init2)
    apply blast
    done

  from ST frame 
  obtain vt ot stk' where
    stk  : "stk = vt#ot#stk'" and
    app_v: "approx_val G hp ihp vt (OK (Init vT))" and
    app_o: "approx_val G hp ihp ot (OK (Init oT))" and
    app_s: "approx_stk G hp ihp stk' tST" and
    app_l: "approx_loc G hp ihp loc LT" and
    consi: "consistent_init (vt#ot#stk') loc ((Init vT)#(Init oT)#tST,LT) ihp" and
    corr:  "fst sig = init \<longrightarrow>
    corresponds (vt#ot#stk') loc (Init vT#Init oT#tST,LT) ihp (fst r) (PartInit C) \<and> 
    (\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and> 
    (ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))" and
    len_l: "length loc = Suc (length (snd sig) + maxl)"
    by - (erule correct_frameE, simp, blast) 

  from app_v app_o obtain 
    "G,hp \<turnstile> vt ::\<preceq> vT" and
    conf_o: "G,hp \<turnstile> ot ::\<preceq> oT" and
    is_init_vo: "is_init hp ihp vt" "is_init hp ihp ot"
    by (simp add: approx_val_def iconf_def)

  with wf v_less have conf_v: "G,hp \<turnstile> vt ::\<preceq> vT'" 
    by (auto intro: conf_widen)


  from exec ins meth stk no_x
  have "ot \<noteq> Null" by (auto simp add: split_beta raise_system_xcpt_def)
  with o_less conf_o field wf
  obtain x C' fs oT' where
    ot_addr: "ot = Addr x" and
    hp_Some: "hp x = Some (Obj C' fs)" and
             "G \<turnstile> (Class C') \<preceq> oT"
    by (fastsimp simp add: conf_def dest!: non_np_objD intro: conf_widen)
  with o_less
  have C': "G \<turnstile> C' \<preceq>C D"
    by (auto dest: widen_trans)
  with wf field
  have fields: "map_of (fields (G, C')) (F, D) = Some vT'"
    by - (rule widen_cfs_fields)

  let ?hp' = "hp(x\<mapsto>Obj C' (fs((F, D)\<mapsto>vt)))" 
  and ?f'  = "(stk', loc, C, sig, Suc pc, r)"
  
  from exec ins meth stk ot_addr hp_Some
  have state': "state' = Norm (?hp', ihp, ?f'#frs)"
    by (simp add: raise_system_xcpt_def)

  from hp_Some have hext: "hp \<le>| ?hp'" by (rule hext_upd_obj)

  with fields hp_Some conf_v heap_ok 
  have hp'_ok: "G \<turnstile>h ?hp' \<surd>" by (blast intro: hconf_imp_hconf_field_update )
    
  from app_v have "is_init hp ihp vt" by (simp add: approx_val_def iconf_def)
    
  with init_ok hp_Some have hp'_init: "h_init G ?hp' ihp" 
    by (rule h_init_field_update)

  from hp_Some heap_ok pre_alloc have pre_alloc': "preallocated ?hp' ihp" 
    by (rule preallocated_field_update)

  from corr have corr':
    "fst sig = init \<longrightarrow>
    corresponds stk' loc (tST, LT) ihp (fst r) (PartInit C) \<and>
    (\<exists>l. fst r = Addr l \<and> ?hp' l \<noteq> None \<and> 
        (ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))"
    by (clarsimp simp add: corresponds_stk_cons simp del: fun_upd_apply) simp

  from consi stk have "consistent_init stk' loc (tST, LT) ihp"
    by (blast intro: consistent_init_pop)

  with wf app_l app_s len_l suc_pc hext corr' 
  have f'_correct: 
    "correct_frame G ?hp' ihp (tST, LT) maxl ins (stk',loc,C,sig,Suc pc,r)"
    by (simp add: correct_frame_def)
       (blast intro: approx_stk_imp_approx_stk_sup_heap
                     approx_loc_imp_approx_loc_sup_heap)

  from wf frames hp_Some fields conf_v
  have "correct_frames G ?hp' ihp phi rT sig z r frs"
    by - (rule  correct_frames_imp_correct_frames_field_update)

  with state' ins meth is_class_C phi_suc hp'_ok hp'_init f'_correct pre_alloc'
  show ?thesis by simp (rule correct_stateI)
qed 


lemma New_correct:
"\<lbrakk> wf_prog wt G;
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
  ins!pc = New X; 
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
  fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
  assume wf:   "wf_prog wt G"
  assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
  assume ins:  "ins!pc = New X"
  assume wt:   "wt_instr (ins!pc) G C rT (phi C sig) maxs 
                         (fst sig = init) (length ins) et pc"
  assume exec: "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
  assume conf: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
  assume no_x: "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None"

  from conf meth
  obtain ST LT z where
    heap_ok:    "G\<turnstile>h hp\<surd>" and
    init_ok:    "h_init G hp ihp" and
    phi_pc:     "((ST,LT),z) \<in> phi C sig!pc" and
    prealloc:   "preallocated hp ihp" and
    is_class_C: "is_class G C" and
    frame:      "correct_frame G hp ihp (ST,LT) maxl ins (stk,loc,C,sig,pc,r)" and
    frames:     "correct_frames G hp ihp phi rT sig z r frs"
    ..

  from phi_pc ins wt
  obtain    
    is_class_X: "is_class G X" and
    maxs:       "length ST < maxs" and
    suc_pc:     "Suc pc < length ins" and
    phi_suc:    "((UnInit X pc#ST, replace (OK (UnInit X pc)) Err LT), z) \<in> phi C sig ! Suc pc" (is "((?ST',?LT'),_) \<in> _") and
    new_type:   "UnInit X pc \<notin> set ST" 
    apply (unfold wt_instr_def eff_def eff_bool_def norm_eff_def)
    apply clarsimp
    apply (drule bspec, assumption)
    apply clarsimp
    apply (drule subsetD, rule imageI, assumption)
    apply clarsimp
    done
 
  obtain oref xp' where
    new_Addr: "new_Addr hp = (oref,xp')"
    by (cases "new_Addr hp") 
  with ins no_x
  obtain hp: "hp oref = None" and "xp' = None"
    by (auto dest: new_AddrD simp add: raise_system_xcpt_def)
  
  with exec ins meth new_Addr 
  have state':
    "state' = Norm (hp(oref\<mapsto>blank G X), ihp(oref := UnInit X pc),
                    (Addr oref # stk, loc, C, sig, Suc pc, r) # frs)" 
    (is "state' = Norm (?hp', ?ihp', ?f # frs)")
    by simp
  moreover
  from wf hp heap_ok is_class_X
  have hp': "G \<turnstile>h ?hp' \<surd>"
    by - (rule hconf_imp_hconf_newref, 
          auto simp add: oconf_def blank_def dest: fields_is_type)
  moreover
  from hp heap_ok init_ok
  have "h_init G ?hp' ?ihp'" by (rule h_init_newref)
  moreover
  from hp have sup: "hp \<le>| ?hp'" by (rule hext_new)
  from frame obtain
    cons:  "consistent_init stk loc (ST, LT) ihp" and
    a_loc: "approx_loc G hp ihp loc LT" and
    a_stk: "approx_stk G hp ihp stk ST" and
    corr:  "fst sig = init \<longrightarrow>
      corresponds stk loc (ST, LT) ihp (fst r) (PartInit C) \<and>
      (\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and> 
       (ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))"
    ..
  from a_loc
  have a_loc': "approx_loc G hp ihp loc ?LT'" by (rule approx_loc_replace_Err) 
  from corr a_loc a_stk new_type hp
  have corr': 
    "fst sig = init \<longrightarrow>
     corresponds (Addr oref#stk) loc (?ST', ?LT') ?ihp' (fst r) (PartInit C) \<and>
     (\<exists>l. fst r = Addr l \<and> ?hp' l \<noteq> None \<and> 
      (?ihp' l = PartInit C \<or> (\<exists>C'. ?ihp' l = Init (Class C'))))"
    apply (clarsimp simp add: corresponds_stk_cons simp del: fun_upd_apply)
    apply (drule corresponds_new_val2, assumption+)
    apply (auto intro: corresponds_replace_Err)
    done
  from new_type have "OK (UnInit X pc) \<notin> set (map OK ST) \<union> set ?LT'" 
    by (auto simp add: replace_removes_elem) 
  with cons a_stk a_loc' hp
  have "consistent_init (Addr oref # stk) loc (?ST',?LT') ?ihp'"
    by (blast intro: consistent_init_newref consistent_init_replace_Err) 
  with hp frame suc_pc wf corr' a_loc'
  have "correct_frame G ?hp' ?ihp' (?ST', ?LT') maxl ins ?f" 
    apply (unfold correct_frame_def)
    apply (clarsimp simp add: map_eq_Cons conf_def blank_def 
                              corresponds_stk_cons)
    apply (insert sup, unfold blank_def)
    apply (blast intro: approx_stk_newref 
                        approx_stk_imp_approx_stk_sup_heap 
                        approx_loc_imp_approx_loc_sup_heap 
                        approx_loc_newref 
                        approx_val_newref
                        sup)
    done      
  moreover
  from hp frames wf heap_ok is_class_X
  have "correct_frames G ?hp' ?ihp' phi rT sig z r frs"
    by (unfold blank_def) 
       (rule correct_frames_imp_correct_frames_newref,
         auto simp add: oconf_def dest: fields_is_type) 
  moreover
  from hp prealloc have "preallocated ?hp' ?ihp'" by (rule preallocated_newref)  
  ultimately
  show ?thesis by simp (rule correct_stateI)
qed
  
text {* \bf Method Invocation *}

lemmas [simp del] = split_paired_Ex

lemma zip_map [rule_format]:
  "\<forall>a. length a = length b \<longrightarrow> 
  zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)"
  apply (induct b) 
   apply simp
  apply clarsimp
  apply (case_tac aa)
  apply simp+
  done


lemma conf_ClassD:
  "G,h\<turnstile> Addr r ::\<preceq> Class C \<Longrightarrow> 
  (\<exists>obj. h r = Some obj \<and> G \<turnstile> the_Class (obj_ty obj) \<preceq>C C)"
  apply (drule conf_RefTD)
  apply clarsimp
  apply (case_tac obj)
  apply auto
  done
  

lemma the_Class_widen:
  "G \<turnstile> the_Class (obj_ty obj) \<preceq>C D \<Longrightarrow> G \<turnstile> obj_ty obj \<preceq> Class D"
  apply (case_tac obj)
  apply auto
  done



lemma Invoke_correct: 
"\<lbrakk> wt_jvm_prog G phi; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = Invoke C' mn pTs; 
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
  fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
proof -
  assume wtprog: "wt_jvm_prog G phi"
  assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
  assume ins:    "ins ! pc = Invoke C' mn pTs"
  assume wti:    "wt_instr (ins!pc) G C rT (phi C sig) maxs 
                           (fst sig = init) (length ins) et pc"
  assume state': "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
  assume approx: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
  assume no_xcp: "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None"
  
  from wtprog obtain wfmb where
    wfprog: "wf_prog wfmb G" by (simp add: wt_jvm_prog_def)
      
  from approx method obtain s z where  
    heap_ok: "G\<turnstile>h hp\<surd>" and
    init_ok: "h_init G hp ihp" and
    phi_pc:  "(s,z) \<in> phi C sig!pc" and
    prealloc:"preallocated hp ihp" and
    is_class_C: "is_class G C" and
    frame:   "correct_frame G hp ihp s maxl ins (stk, loc, C, sig, pc, r)" and
    frames:  "correct_frames G hp ihp phi rT sig z r frs"
    ..

  from ins wti phi_pc obtain apTs X ST LT D' rT body where 
    is_class: "is_class G C'" and
    s:  "s = (rev apTs @ X # ST, LT)" and
    l:  "length apTs = length pTs" and
    w: "\<forall>(x,y)\<in>set (zip apTs pTs). G \<turnstile> x \<preceq>i (Init y)" and
    mC': "method (G, C') (mn, pTs) = Some (D', rT, body)" and
    pc:  "Suc pc < length ins" and    
    eff: "norm_eff (Invoke C' mn pTs) G pc (Suc pc) (phi C sig!pc) \<subseteq> phi C sig!Suc pc" and 
    X: "G \<turnstile> X \<preceq>i Init (Class C')" and
    ni: "mn \<noteq> init"
    apply (clarsimp simp add: wt_instr_def eff_def) 
    apply (drule bspec, assumption)
    apply clarsimp
    apply blast
    done

  from s ins frame obtain    
    a_stk: "approx_stk G hp ihp stk (rev apTs @ X # ST)" and
    a_loc: "approx_loc G hp ihp loc LT" and
    init:  "consistent_init stk loc s ihp" and    
    suc_l: "length loc = Suc (length (snd sig) + maxl)"
    by (simp add: correct_frame_def)

  from a_stk obtain opTs stk' oX where
    opTs:   "approx_stk G hp ihp opTs (rev apTs)" and
    oX:     "approx_val G hp ihp oX (OK X)" and
    a_stk': "approx_stk G hp ihp stk' ST" and
    stk':   "stk = opTs @ oX # stk'" and
    l_o:    "length opTs = length apTs" 
            "length stk' = length ST"  
    by (auto dest!:  approx_stk_append_lemma)

  from oX have X_oX: "G,hp,ihp \<turnstile> oX ::\<preceq>i X" by (simp add: approx_val_def)
  with wfprog X have oX_conf: "G,hp \<turnstile> oX ::\<preceq> (Class C')"
    by (auto simp add: approx_val_def iconf_def init_le_Init2 dest: conf_widen)
  from stk' l_o l have oX_pos: "stk ! length pTs = oX" by (simp add: nth_append)
  with state' method ins no_xcp oX_conf obtain ref where oX_Addr: "oX = Addr ref"
    by (auto simp add: raise_system_xcpt_def dest: conf_RefTD)
  with oX_conf 
  obtain D obj where
    hp_Some: "hp ref = Some obj" and 
    D_def:   "D = the_Class (obj_ty obj)" and
    D_le_C': "G \<turnstile> D \<preceq>C C'"
    by (clarsimp dest!: conf_ClassD)

  from D_le_C' wfprog mC'
  obtain D'' rT' mxl' mxs' ins' et' where
    mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')" 
        "G \<turnstile> rT' \<preceq> rT"
    by (auto dest!: subtype_widen_methd) blast

  let ?loc' = "oX # rev opTs @ replicate mxl' arbitrary" 
  let ?f    = "([], ?loc', D'', (mn, pTs), 0, arbitrary)"
  let ?f'   = "(stk, loc, C, sig, pc, r)"

  from oX_Addr oX_pos hp_Some state' method ins stk' l_o l mD D_def
  have state'_val: "state' = Norm (hp, ihp, ?f# ?f' # frs)"
    by (simp add: raise_system_xcpt_def)

  from is_class D_le_C' have is_class_D: "is_class G D" 
    by (auto dest: subcls_is_class2)
  with mD wfprog obtain mD'': 
    "method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')"
    "is_class G D''"
    by (auto dest: method_in_md)

  from wtprog mD'' 
  have start: "wt_start G D'' mn pTs mxl' (phi D'' (mn, pTs)) \<and> ins' \<noteq> []"
    by (auto dest: wt_jvm_prog_impl_wt_start)
  
  let ?T = "OK (Init (Class D''))"
  let ?LT0 = "?T # map OK (map Init pTs) @ replicate mxl' Err"

  from ni start have sup_loc: 
    "(([],?LT0),D''=Object) \<in> phi D'' (mn,pTs) ! 0"
    by (simp add: wt_start_def)

  have c_f: "correct_frame G hp ihp ([], ?LT0) mxl' ins' ?f"
  proof -
    have r: 
      "approx_loc G hp ihp (replicate mxl' arbitrary) (replicate mxl' Err)"
      by (simp add: approx_loc_def approx_val_Err list_all2_def 
                    set_replicate_conv_if)
      
    from wfprog mD is_class_D have "G \<turnstile> Class D \<preceq> Class D''"
      by (auto dest: method_wf_mdecl)
      
    with hp_Some D_def oX_Addr oX X have a: "approx_val G hp ihp oX ?T"
      by (auto simp add: is_init_def init_le_Init2 the_Class_widen
                         approx_val_def iconf_def conf_def)

    from w l          
    have "\<forall>(x,y)\<in>set (zip (map (\<lambda>x. x) apTs) (map Init pTs)). G \<turnstile> x \<preceq>i y"
      by (simp only: zip_map) auto
    hence "\<forall>(x,y)\<in>set (zip apTs (map Init pTs)). G \<turnstile> x \<preceq>i y" by simp
    with l  
    have "\<forall>(x,y)\<in>set (zip (rev apTs) (rev (map Init pTs))). G \<turnstile> x \<preceq>i y"
      by (auto simp add: zip_rev)
    with wfprog l l_o opTs
    have "approx_loc G hp ihp opTs (map OK (rev (map Init pTs)))"
      by (auto intro: assConv_approx_stk_imp_approx_loc)
    hence "approx_stk G hp ihp opTs (rev (map Init pTs))"
      by (simp add: approx_stk_def)
    hence "approx_stk G hp ihp (rev opTs) (map Init pTs)"
      by (simp add: approx_stk_rev)
    hence "approx_loc G hp ihp (rev opTs) (map OK (map Init pTs))"
      by (simp add: approx_stk_def)
    with r a l_o l 
    have loc: "approx_loc G hp ihp ?loc' ?LT0"
      by (auto simp add: approx_loc_append approx_stk_def)

    from l l_o have "length pTs = length opTs" by auto
    hence "consistent_init [] ?loc' ([],?LT0) ihp"
      by (blast intro: consistent_init_start)

    with start loc l_o l ni  show ?thesis by (simp add: correct_frame_def)
  qed

  from state'_val heap_ok mD'' ins method phi_pc s l 
    frames c_f frame is_class_C ni init_ok prealloc sup_loc
  show "G,phi \<turnstile>JVM state'\<surd>"
    apply simp
    apply (rule correct_stateI, assumption+) 
    apply clarsimp
    apply (intro exI conjI impI)
    apply assumption+
    apply (rule refl)
    apply assumption+
    done
qed

lemma Invoke_special_correct: 
"\<lbrakk> wt_jvm_prog G phi; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = Invoke_special C' mn pTs; 
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
  fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
  assume wtprog: "wt_jvm_prog G phi"
  assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
  assume ins:    "ins ! pc = Invoke_special C' mn pTs"
  assume wti:    "wt_instr (ins!pc) G C rT (phi C sig) maxs 
                           (fst sig = init) (length ins) et pc"
  assume state': "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
  assume approx: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
  assume no_x:   "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None"
  
  from wtprog obtain wfmb where wfprog: "wf_prog wfmb G" 
    by (simp add: wt_jvm_prog_def)

  from approx method obtain s z where  
    heap_ok: "G\<turnstile>h hp\<surd>" and
    init_ok: "h_init G hp ihp" and
    prealloc:"preallocated hp ihp" and
    phi_pc:  "(s,z) \<in> phi C sig!pc" and
    is_class_C: "is_class G C" and
    frame:   "correct_frame G hp ihp s maxl ins (stk, loc, C, sig, pc, r)" and
    frames:  "correct_frames G hp ihp phi rT sig z r frs"
    ..

  from ins wti phi_pc obtain apTs X ST LT rT' maxs' mxl' ins' et' where 
    s: "s = (rev apTs @ X # ST, LT)" and
    l: "length apTs = length pTs" and
    is_class: "is_class G C'" and
    w: "\<forall>(x,y)\<in>set (zip apTs pTs). G \<turnstile> x \<preceq>i (Init y)" and
    mC': "method (G, C') (mn, pTs) = Some (C', rT', maxs', mxl', ins', et')" and
    pc:  "Suc pc < length ins" and    
    eff: "norm_eff (Invoke_special C' mn pTs) G pc (Suc pc) (phi C sig!pc) \<subseteq> 
          phi C sig!Suc pc" and
    X: "(\<exists>pc. X = UnInit C' pc) \<or> (X = PartInit C \<and> G \<turnstile> C \<prec>C1 C' \<and> ¬z)" and
    is_init: "mn = init"
    apply (clarsimp simp add: wt_instr_def split_paired_Ex eff_def) 
    apply (drule bspec, assumption)
    apply clarsimp
    apply blast
    done

  from s ins frame obtain    
    a_stk: "approx_stk G hp ihp stk (rev apTs @ X # ST)" and
    a_loc: "approx_loc G hp ihp loc LT" and
    init:  "consistent_init stk loc (rev apTs @ X # ST, LT) ihp" and
    corr:  "fst sig = init \<longrightarrow> corresponds stk loc s ihp (fst r) (PartInit C) \<and>
            (\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and> 
              (ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))" and
    suc_l: "length loc = Suc (length (snd sig) + maxl)"
    by (simp add: correct_frame_def) 

  from a_stk obtain opTs stk' oX where
    opTs:   "approx_stk G hp ihp opTs (rev apTs)" and
    oX:     "approx_val G hp ihp oX (OK X)" and
    a_stk': "approx_stk G hp ihp stk' ST" and
    stk':   "stk = opTs @ oX # stk'" and
    l_o:    "length opTs = length apTs" 
            "length stk' = length ST"  
    by (fastsimp dest!: approx_stk_append_lemma)

  from stk' l_o l have oX_pos: "stk ! length pTs = oX" by (simp add: nth_append)

  from state' method ins no_x oX_pos have "oX \<noteq> Null" 
    by (simp add: raise_system_xcpt_def split: split_if_asm)

  from wfprog oX have oX_conf: "G,hp,ihp \<turnstile> oX ::\<preceq>i X"
    by (simp add: approx_val_def)
  with X
  obtain ref D fs where 
    oX_Addr: "oX = Addr ref" and
    hp_Some: "hp ref = Some (Obj D fs)" and 
    D_le_C': "G \<turnstile> D \<preceq>C C'"
    apply -
    apply (erule disjE)
     apply (fastsimp simp add: iconf_def dest!: conf_ClassD)
    apply (fastsimp simp add: iconf_def dest!: conf_ClassD dest: rtrancl_into_rtrancl)
    done

  let ?new  = "new_Addr hp"
  let ?ref' = "fst ?new"
  let ?xp'  = "snd ?new"
  let ?hp'  = "hp(?ref'\<mapsto>blank G D)"
  let ?loc' = "Addr ?ref' # rev opTs @ replicate mxl' arbitrary" 
  let ?ihp' = "if C' = Object then 
               ihp(?ref':= Init (Class D)) 
               else 
               ihp(?ref' := PartInit C')"
  let ?r'   = "if C' = Object then 
               (Addr ?ref', Addr ?ref') 
               else 
               (Addr ?ref', Null)"
  let ?f    = "([], ?loc', C', (mn, pTs), 0, ?r')" 
  let ?f'   = "(stk, loc, C, sig, pc, r)"

  from state' method ins no_x have norm: "?xp' = None" 
    by (simp add: split_beta split: split_if_asm)
  
  with oX_Addr oX_pos hp_Some state' method ins stk' l_o l mC' 
  have state'_val: "state' = Norm (?hp', ?ihp', ?f# ?f' # frs)"
    by (simp add: raise_system_xcpt_def split_beta)
      
  obtain ref' xp' where 
    new_Addr: "new_Addr hp = (ref',xp')" 
    by (cases "new_Addr hp") auto
  with norm have new_ref': "hp ref' = None" by (auto dest: new_AddrD)

  from is_class D_le_C' have is_class_D: "is_class G D" 
    by (auto dest: subcls_is_class2)

  from wtprog is_class mC'
  have start: "wt_start G C' mn pTs mxl' (phi C' (mn, pTs)) \<and> ins' \<noteq> []"
    by (auto dest: wt_jvm_prog_impl_wt_start)
      
  let ?T = "OK (if C' \<noteq> Object then PartInit C' else Init (Class C'))" 
  let ?LT0 = "?T # map OK (map Init pTs) @ replicate mxl' Err"

  from start is_init
  have LT0: "(([], ?LT0),C'=Object) \<in> phi C' (mn, pTs) ! 0"
    by (clarsimp simp add: wt_start_def)

  have c_f: "correct_frame G ?hp' ?ihp' ([], ?LT0) mxl' ins' ?f"
  proof -        
    have r: 
      "approx_loc G ?hp' ?ihp' (replicate mxl' arbitrary) (replicate mxl' Err)"
      by (simp add: approx_loc_def approx_val_Err list_all2_def 
                    set_replicate_conv_if)

    from new_Addr obtain fs where "?hp' ref' = Some (Obj D fs)" by (simp add: blank_def)
    hence "G,?hp' \<turnstile> Addr ref' ::\<preceq> Class C'"
      by (auto simp add: new_Addr D_le_C' intro: conf_obj_AddrI)
    hence a: "approx_val G ?hp' ?ihp' (Addr ?ref') ?T"
      by (auto simp add: approx_val_def iconf_def new_Addr 
                         blank_def is_init_def)
    from w l          
    have "\<forall>(x,y)\<in>set (zip (map (\<lambda>x. x) apTs) (map Init pTs)). G \<turnstile> x \<preceq>i y"
      by (simp only: zip_map) auto
    hence "\<forall>(x,y)\<in>set (zip apTs (map Init pTs)). G \<turnstile> x \<preceq>i y" by simp
    with l
    have "\<forall>(x,y)\<in>set (zip (rev apTs) (rev (map Init pTs))). G \<turnstile> x \<preceq>i y"
      by (auto simp add: zip_rev)
    with wfprog l l_o opTs
    have "approx_loc G hp ihp opTs (map OK (rev (map Init pTs)))"
      by (auto intro: assConv_approx_stk_imp_approx_loc)
    hence "approx_stk G hp ihp opTs (rev (map Init pTs))"
      by (simp add: approx_stk_def)
    hence "approx_stk G hp ihp (rev opTs) (map Init pTs)"
      by (simp add: approx_stk_rev)
    hence "approx_loc G hp ihp (rev opTs) (map OK (map Init pTs))"
      by (simp add: approx_stk_def)
    with new_Addr new_ref'
    have "approx_loc G hp ?ihp' (rev opTs) (map OK (map Init pTs))"
      by (auto dest: approx_loc_newref)
    moreover
    from new_Addr new_ref' have "hp \<le>| ?hp'" by simp
    ultimately
    have "approx_loc G ?hp' ?ihp' (rev opTs) (map OK (map Init pTs))"
      by (rule approx_loc_imp_approx_loc_sup_heap)
    with r a l_o l 
    have loc: "approx_loc G ?hp' ?ihp' ?loc' ?LT0"
      by (auto simp add: approx_loc_append)
        
    from new_Addr new_ref' l_o l have corr': 
      "corresponds [] ?loc' ([], ?LT) ?ihp' (Addr ref') (PartInit C')"
      apply (simp add: corresponds_def corr_stk_def corr_loc_cons 
                  split del: split_if)
      apply (rule conjI)
       apply (simp add: corr_val_def)
      apply (rule corr_loc_start)
        apply clarsimp
        apply (erule disjE)
         apply (erule imageE, erule imageE)
         apply simp 
         apply blast
        apply (drule in_set_replicateD)
        apply assumption
       apply simp
      apply blast
      done

    from l_o l
    have "length (rev opTs @ replicate mxl' arbitrary) = 
          length (map OK (map Init pTs) @ replicate mxl' Err)" by simp
    moreover
    have "\<forall>x\<in>set (map OK (map Init pTs) @ replicate mxl' Err). 
          x = Err \<or> (\<exists>t. x = OK (Init t))"
      by (auto dest: in_set_replicateD)
    ultimately
    have "consistent_init [] ?loc' ([], ?LT0) ?ihp'"
      apply (unfold consistent_init_def)
      apply (unfold corresponds_def)
      apply (simp (no_asm) add: corr_stk_def corr_loc_empty corr_loc_cons
                     split del: split_if)
      apply safe
       apply (rule exI)
       apply (rule conjI)
        apply (simp (no_asm))
       apply (rule corr_loc_start)
        apply assumption+
        apply blast
       apply (rule exI)
       apply (rule conjI)
        defer
        apply (blast intro: corr_loc_start)
       apply (rule impI)
       apply (simp add: new_Addr split del: split_if)
       apply (rule conjI)
        apply (rule refl)
       apply (simp add: corr_val_def new_Addr split: split_if_asm)
       done

     with start loc l_o l corr' new_Addr new_ref' 
     show ?thesis by (simp add: correct_frame_def split: split_if_asm) 
   qed

   from a_stk a_loc init suc_l pc new_Addr new_ref' s corr 
   have c_f': "correct_frame G ?hp' ?ihp' (rev apTs @ X # ST, LT) maxl ins ?f'"
     apply (unfold correct_frame_def)
     apply simp
     apply (rule conjI)
      apply (rule impI)
      apply (rule conjI)
       apply (drule approx_stk_newref, assumption)
       apply (rule approx_stk_imp_approx_stk_sup_heap, assumption)
       apply simp
      apply (rule conjI)
       apply (drule approx_loc_newref, assumption)
       apply (rule approx_loc_imp_approx_loc_sup_heap, assumption)
       apply simp
      apply (rule conjI)
       apply (rule consistent_init_new_val, assumption+)
       apply (rule impI, erule impE, assumption, elim exE conjE)
       apply (rule conjI)
        apply (rule corresponds_new_val2, assumption+)
        apply simp
        apply (rule exI, rule conjI)
          apply (rule impI) 
          apply assumption 
         apply simp 
        apply (rule impI)
        apply (rule conjI)
         apply (drule approx_stk_newref, assumption)
         apply (rule approx_stk_imp_approx_stk_sup_heap, assumption)
         apply simp
        apply (rule conjI)
         apply (drule approx_loc_newref, assumption)
         apply (rule approx_loc_imp_approx_loc_sup_heap, assumption)
         apply simp
        apply (rule conjI)
         apply (rule consistent_init_new_val, assumption+)
        apply (rule impI, erule impE, assumption, elim exE conjE)
        apply (rule conjI)
         apply (rule corresponds_new_val2, assumption+)
        apply simp
        apply (rule exI, rule conjI)
         apply (rule impI)
         apply (rule conjI)
          apply assumption
         apply simp
        apply simp
        done

  from new_Addr new_ref' heap_ok is_class_D wfprog
  have hp'_ok: "G \<turnstile>h ?hp' \<surd>"
    by (auto intro: hconf_imp_hconf_newref oconf_blank)

  with new_Addr new_ref'
  have ihp'_ok: "h_init G ?hp' ?ihp'"
    by (auto intro!: h_init_newref)

  from hp_Some new_ref' have neq_ref: "ref \<noteq> ref'" by auto

  with new_Addr oX_Addr X oX hp_Some 
  have ctor_ok: 
    "constructor_ok G ?hp' ?ihp' (Addr ref) C' (C'=Object) ?r'"
    apply (unfold constructor_ok_def)
    apply (simp add: approx_val_def iconf_def)
    apply (erule disjE)
     apply (clarsimp simp add: blank_def)
    apply (elim exE conjE)
    apply (simp add: blank_def)
    done

  from new_Addr new_ref' frames
  have c_frs: "correct_frames G ?hp' ?ihp' phi rT sig z r frs"
    by (auto simp add: blank_def 
             intro: correct_frames_imp_correct_frames_newref)      

  from new_Addr new_ref' prealloc have prealloc': "preallocated ?hp' ?ihp'" 
    by (auto intro: preallocated_newref)

  from state'_val heap_ok mC' ins method phi_pc s l ctor_ok c_f' c_frs
       frames LT0 c_f is_class_C is_class new_Addr new_ref' hp'_ok ihp'_ok
       prealloc'
  show "G,phi \<turnstile>JVM state'\<surd>"
    apply (unfold correct_state_def)
    apply (simp split del: split_if)

    apply (intro exI conjI impI)
        apply assumption+
        apply (rule refl)
       apply assumption+
      apply (simp add: oX_pos oX_Addr hp_Some neq_ref)
     apply assumption+
    done
qed

lemmas [simp del] = map_append

lemma Return_correct_not_init:
"\<lbrakk> fst sig \<noteq> init;
  wt_jvm_prog G phi; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = Return; 
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
  assume wtjvm: "wt_jvm_prog G phi"
  assume mthd:  "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
  assume ins:   "ins!pc = Return"
  assume wt:    "wt_instr (ins!pc) G C rT (phi C sig) maxs 
                          (fst sig = init) (length ins) et pc"
  assume state: "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
  assume approx:"G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"

  from approx mthd 
  obtain s z where
    heap_ok: "G \<turnstile>h hp\<surd>" and
    init_ok: "h_init G hp ihp" and
    prealloc:"preallocated hp ihp" and
    classC:  "is_class G C" and
    some:    "(s,z) \<in> phi C sig ! pc" and
    frame:   "correct_frame G hp ihp s maxl ins (stk, loc, C, sig, pc, r)" and
    frames:  "correct_frames G hp ihp phi rT sig z r frs"
    ..

  obtain mn pTs where sig: "sig = (mn,pTs)" by (cases sig)
  moreover assume "fst sig \<noteq> init"
  ultimately have not_init: "mn \<noteq> init" by simp

  from ins some sig wt
  obtain T ST LT where
    s:  "s = (T # ST, LT)" and
    T:  "G \<turnstile> T \<preceq>i Init rT"
    apply (clarsimp simp add: wt_instr_def eff_def eff_bool_def norm_eff_def)
    apply (drule bspec, assumption)
    apply clarsimp
    apply blast
    done

  from frame s 
  obtain rval stk' loc where
    stk: "stk = rval # stk'" and  
    val: "approx_val G hp ihp rval (OK T)" and
    approx_stk: "approx_stk G hp ihp stk' ST" and
    approx_val: "approx_loc G hp ihp loc LT" and
    consistent: "consistent_init stk loc (T # ST, LT) ihp" and
    len: "length loc = Suc (length (snd sig) + maxl)" and
    pc: "pc < length ins" 
    by (simp add: correct_frame_def) blast

  from stk mthd ins state
  have "frs = [] \<Longrightarrow> ?thesis" by (simp add: correct_state_def)
  moreover
  { fix f frs' assume frs: "frs = f#frs'"
    obtain stk0 loc0 C0 sig0 pc0 r0 where
      f: "f = (stk0, loc0, C0, sig0, pc0, r0)" by (cases f)
   
    let ?r'   = "(stk0 ! length pTs, snd r0)"
    let ?stk' = "drop (Suc (length pTs)) stk0"
    let ?f'   = "(rval#?stk',loc0,C0,sig0,Suc pc0,r0)"

    from stk mthd ins sig f frs not_init state
    have state': "state' = Norm (hp, ihp, ?f' # frs')" by (simp add: split_beta)
    
    from f frs frames sig 
    obtain ST0 LT0 T0 z0 rT0 maxs0 maxl0 ins0 et0 C' apTs D D' rT' body' where
      class_C0: "is_class G C0" and
      methd_C0: "method (G, C0) sig0 = Some (C0, rT0, maxs0, maxl0, ins0, et0)" and
      ins0:     "ins0 ! pc0 = Invoke C' mn pTs \<or> 
                 ins0 ! pc0 = Invoke_special C' mn pTs" and
      phi_pc0:  "((rev apTs @ T0 # ST0, LT0), z0) \<in> phi C0 sig0 ! pc0" and
      apTs:     "length apTs = length pTs" and
      methd_C': "method (G, C') sig = Some (D', rT', body')" "G \<turnstile> rT \<preceq> rT'" and
      c_fr:     "correct_frame G hp ihp (rev apTs @ T0 # ST0, LT0) maxl0 ins0 
                              (stk0, loc0, C0, sig0, pc0, r0)" and
      c_frs:    "correct_frames G hp ihp phi rT0 sig0 z0 r0 frs'"
      apply simp (* fixme: this script sucks *)
      apply (elim conjE exE)
      apply (rule that)
       apply assumption+
       apply simp
       apply assumption+
       apply simp
       apply (rule conjI, rule refl)+
       apply (rule refl)
       apply assumption+
       apply simp
       apply assumption
      done

    from c_fr obtain 
      a_stk0: "approx_stk G hp ihp stk0 (rev apTs @ T0 # ST0)" and
      a_loc0: "approx_loc G hp ihp loc0 LT0" and
      cons0:  "consistent_init stk0 loc0 (rev apTs @ T0 # ST0, LT0) ihp" and
      corr0:  "fst sig0 = init \<longrightarrow> 
      corresponds stk0 loc0 (rev apTs @ T0 # ST0, LT0) ihp (fst r0) (PartInit C0) \<and>
      (\<exists>l. fst r0 = Addr l \<and> hp l \<noteq> None \<and> 
      (ihp l = PartInit C0 \<or> (\<exists>C'. ihp l = Init (Class C'))))" and
      pc0:    "pc0 < length ins0" and 
      lenloc0:"length loc0 = Suc (length (snd sig0) + maxl0)"
      by (unfold correct_frame_def) simp

    from pc0 wtjvm methd_C0 have wt0: 
      "wt_instr (ins0!pc0) G C0 rT0 (phi C0 sig0) maxs0 
                (fst sig0 = init) (length ins0) et0 pc0"
      by - (rule wt_jvm_prog_impl_wt_instr)
    
    from ins0 apTs phi_pc0 not_init sig methd_C' wt0
    obtain 
      Suc_pc0:     "Suc pc0 < length ins0" and
      phi_Suc_pc0: "((Init rT' # ST0, LT0),z0) \<in> phi C0 sig0 ! Suc pc0" and
      T0:          "G \<turnstile> T0 \<preceq>i Init (Class C')" 
      apply (simp add: wt_instr_def)
      apply (erule disjE)
       apply (clarsimp simp add: eff_def eff_bool_def norm_eff_def)
       apply (drule bspec, assumption)
       apply clarsimp
       apply (drule subsetD, rule imageI, assumption)
       apply clarsimp
      apply simp
      done

    from wtjvm obtain mb where wf: "wf_prog mb G" by (simp add: wt_jvm_prog_def)

    from a_stk0 obtain apts v stk0' where
      stk0':   "stk0 = apts @ v # stk0'" and
      len:     "length apts = length apTs" and
      v:       "approx_val G hp ihp v (OK T0)" and      
      a_stk0': "approx_stk G hp ihp stk0' ST0"
      by - (drule approx_stk_append_lemma, auto)
    
    from stk0' len v a_stk0' wf apTs val T wf methd_C'
    have a_stk':
      "approx_stk G hp ihp (rval # drop (Suc (length pTs)) stk0) (Init rT'#ST0)"
      apply simp
      apply (rule approx_val_widen, assumption+)
      apply (clarsimp simp add: init_le_Init2)
      apply (erule widen_trans)
      apply assumption
      done

    from stk0' len apTs cons0
    have cons':
      "consistent_init (rval # drop (Suc (length pTs)) stk0) loc0 
                       (Init rT'#ST0, LT0) ihp"
      apply simp
      apply (drule consistent_init_append)
       apply simp
      apply (drule consistent_init_pop)
      apply (rule consistent_init_Init_stk)
      apply assumption
      done

    from stk0' len apTs corr0
    have corr':
      "fst sig0 = init \<longrightarrow> 
      corresponds (rval # drop (Suc (length pTs)) stk0) loc0 
                  (Init rT'#ST0, LT0) ihp (fst r0) (PartInit C0) \<and>
      (\<exists>l. fst r0 = Addr l \<and> hp l \<noteq> None \<and> 
           (ihp l = PartInit C0 \<or> (\<exists>C'. ihp l = Init (Class C'))))"
      apply clarsimp
      apply (drule corresponds_append)
       apply simp
      apply (simp add: corresponds_stk_cons)
      done
              
    with cons' lenloc0 a_loc0 Suc_pc0 a_stk' wf 
    have frame':
      "correct_frame G hp ihp (Init rT' # ST0,LT0) maxl0 ins0 ?f'"
      by (simp add: correct_frame_def)
    
    from state' heap_ok init_ok frame' c_frs class_C0 methd_C0 phi_Suc_pc0 prealloc
    have ?thesis by (simp add: correct_state_def) blast
  }
  ultimately
  show "G,phi \<turnstile>JVM state'\<surd>" by (cases frs, blast+)
qed


lemma Return_correct_init:
"\<lbrakk> fst sig = init;
  wt_jvm_prog G phi; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = Return; 
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs); 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
proof -
  assume wtjvm: "wt_jvm_prog G phi"
  assume mthd:  "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
  assume ins:   "ins!pc = Return"
  assume wt:    "wt_instr (ins!pc) G C rT (phi C sig) maxs 
                          (fst sig = init) (length ins) et pc"
  assume state: "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
  assume approx:"G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"

  from approx mthd 
  obtain s z where
    heap_ok: "G \<turnstile>h hp\<surd>" and
    init_ok: "h_init G hp ihp" and
    prealloc:"preallocated hp ihp" and
    classC:  "is_class G C" and
    some:    "(s,z)\<in> phi C sig ! pc" and
    frame:   "correct_frame G hp ihp s maxl ins (stk, loc, C, sig, pc, r)" and
    frames:  "correct_frames G hp ihp phi rT sig z r frs"
    ..

  obtain mn pTs where sig: "sig = (mn,pTs)" by (cases sig)
  moreover assume sig_in: "fst sig = init"
  ultimately have is_init: "mn = init" by simp

  from ins some sig is_init wt
  obtain T ST LT where
    s:  "s = (T # ST, LT)" and
    T:  "G \<turnstile> T \<preceq>i Init rT" and
    z:  "z" 
    apply (clarsimp simp add: wt_instr_def eff_def eff_bool_def norm_eff_def) 
    apply (drule bspec, assumption)
    apply clarsimp
    apply blast
    done

  from frame s sig_in
  obtain rval stk' loc where
    stk: "stk = rval # stk'" and  
    val: "approx_val G hp ihp rval (OK T)" and
    approx_stk: "approx_stk G hp ihp stk' ST" and
    approx_val: "approx_loc G hp ihp loc LT" and
    consistent: "consistent_init stk loc (T # ST, LT) ihp" and
    corr: "corresponds stk loc (T # ST, LT) ihp (fst r) (PartInit C)" and
    len: "length loc = Suc (length (snd sig) + maxl)"
    by (simp add: correct_frame_def) blast 

  from stk mthd ins state
  have "frs = [] \<Longrightarrow> ?thesis" by (simp add: correct_state_def)
  moreover
  { fix f frs' assume frs: "frs = f#frs'"
    obtain stk0 loc0 C0 sig0 pc0 r0 where
      f: "f = (stk0, loc0, C0, sig0, pc0, r0)" by (cases f)
       
    from f frs frames sig is_init 
    obtain ST0 LT0 T0 z0 rT0 maxs0 maxl0 ins0 et0 C' apTs D D' rT' body' where
      class_C0: "is_class G C0" and
      methd_C0: "method (G, C0) sig0 = Some (C0, rT0, maxs0, maxl0, ins0, et0)" and
      ins0:     "ins0 ! pc0 = Invoke C' mn pTs \<or> 
                 ins0 ! pc0 = Invoke_special C' mn pTs" and
      phi_pc0:  "((rev apTs @ T0 # ST0, LT0), z0) \<in> phi C0 sig0 ! pc0" and
      apTs:     "length apTs = length pTs" and 
      methd_C': "method (G, C') sig = Some (D', rT', body')" "G \<turnstile> rT \<preceq> rT'" and
      ctor_ok:  "constructor_ok G hp ihp (stk0 ! length apTs) C' z r" and
      c_fr:     "correct_frame G hp ihp (rev apTs @ T0 # ST0, LT0) maxl0 ins0 
                               (stk0, loc0, C0, sig0, pc0, r0)" and
      c_frs:    "correct_frames G hp ihp phi rT0 sig0 z0 r0 frs'" 
      apply simp 
      apply (elim conjE exE)
      apply (rule that)
       apply assumption+
       apply simp
       apply simp
       apply assumption+
       apply simp
       apply (rule conjI,rule refl)+ 
       apply (rule refl)
       apply assumption+       
       apply simp
       apply assumption
      done

    from c_fr 
    obtain 
      a_stk0: "approx_stk G hp ihp stk0 (rev apTs @ T0 # ST0)" and
      a_loc0: "approx_loc G hp ihp loc0 LT0" and
      cons0:  "consistent_init stk0 loc0 (rev apTs @ T0 # ST0, LT0) ihp" and
      corr0:  "fst sig0 = init \<longrightarrow> 
      corresponds stk0 loc0 (rev apTs @ T0 # ST0, LT0) ihp (fst r0) (PartInit C0) \<and>
      (\<exists>l. fst r0 = Addr l \<and> hp l \<noteq> None \<and> 
       (ihp l = PartInit C0 \<or> (\<exists>C'. ihp l = Init (Class C'))))" and
      pc0:    "pc0 < length ins0" and
      lenloc0:"length loc0 = Suc (length (snd sig0) + maxl0)"
      by (unfold correct_frame_def) simp
    
    from pc0 wtjvm methd_C0 have wt0: 
      "wt_instr (ins0!pc0) G C0 rT0 (phi C0 sig0) maxs0 
                (fst sig0 = init) (length ins0) et0 pc0"
      by - (rule wt_jvm_prog_impl_wt_instr)

    let ?z'  = "if \<exists>D. T0 = PartInit D then True else z0"
    let ?ST' = "Init rT' # replace T0 (Init (theClass T0)) ST0"
    let ?LT' = "replace (OK T0) (OK (Init (theClass T0))) LT0"

    from ins0 apTs phi_pc0 is_init sig methd_C' wt0 
    obtain 
      Suc_pc0: "Suc pc0 < length ins0" and
      phi_Suc_pc0: "((?ST',?LT'),?z') \<in> phi C0 sig0 ! Suc pc0" and
      T0:      "(\<exists>pc. T0 = UnInit C' pc) \<or> 
                (T0 = PartInit C0 \<and> G \<turnstile> C0 \<prec>C1 C' \<and> ¬z0)" 
      apply (simp add: wt_instr_def) 
      apply (erule disjE)
       apply simp
      apply (clarsimp simp add: eff_def eff_bool_def norm_eff_def)
      apply (drule bspec, assumption)
      apply clarsimp
      apply (drule subsetD, rule imageI, assumption)
      apply (clarsimp simp add: nth_append)
      done
    
    from a_stk0 obtain apts oX stk0' where
      stk0': "stk0 = apts @ oX # stk0'" "length apts = length apTs" and
      a_val: "approx_val G hp ihp oX (OK T0)" and
      a_stk: "approx_stk G hp ihp stk0' ST0"
      by - (drule approx_stk_append_lemma, auto)

    with apTs have oX_pos: "stk0!length pTs = oX" by (simp add: nth_append)

    let ?c    = "snd r"
    let ?r'   = "if r0 = (oX,Null) then (oX, ?c) else r0"
    let ?stk' = "rval#(replace oX ?c stk0')"
    let ?loc' = "replace oX ?c loc0"
    let ?f'   = "(?stk',?loc',C0,sig0,Suc pc0,?r')"

    from stk apTs stk0' mthd ins sig f frs is_init state oX_pos
    have state': "state' = Norm (hp, ihp, ?f' # frs')" by (simp add: split_beta) 

    from wtjvm obtain mb where "wf_prog mb G" by (simp add: wt_jvm_prog_def)

    from ctor_ok z apTs oX_pos a_val T0    
    obtain C'' D pc' a c fs1 fs3 where
      a:     "oX = Addr a" and
      ihp_a: "ihp a = UnInit C'' pc' \<or> ihp a = PartInit D" and
      hp_a:  "hp a = Some (Obj C'' fs1)" and
      c:     "snd r = Addr c" and
      ihp_c: "ihp c = Init (Class C'')" and
      hp_c:  "hp c = Some (Obj C'' fs3)"  
      by (simp add: constructor_ok_def, clarify) auto

    from a_val a hp_a T0
    have "G \<turnstile> C'' \<preceq>C C'\<and> (T0 = PartInit C0 \<longrightarrow> G \<turnstile> C'' \<preceq>C C0)"
      apply -
      apply (erule disjE)
       apply (clarsimp simp add: approx_val_def iconf_def)
      apply (clarsimp simp add: approx_val_def iconf_def)
      apply (simp add: conf_def)
      apply (rule rtrancl_trans, assumption)
      apply blast
      done

    with c hp_c ihp_c heap_ok T0
    have a_val':
      "approx_val G hp ihp (snd r) (OK (Init (theClass T0)))"
      apply (simp add: approx_val_def iconf_def is_init_def)
      apply (erule disjE)
       apply clarsimp
       apply (rule conf_obj_AddrI, assumption+)
      apply clarsimp
      apply (rule conf_obj_AddrI, assumption+)
      done

    from stk0' cons0  T0
    have corr:
      "corresponds stk0' loc0 (ST0,LT0) ihp oX T0"
      apply simp
      apply (erule disjE)
       apply (elim exE)
       apply (drule consistent_init_append) 
        apply simp
       apply (drule consistent_init_corresponds_stk_cons)
        apply blast
       apply (simp add: corresponds_stk_cons)
      apply (drule consistent_init_append) 
       apply simp
      apply (drule consistent_init_corresponds_stk_cons)
       apply blast
      apply (simp add: corresponds_stk_cons)
      done
    
    from a_val a_val' a_loc0 T0 corr
    have a_loc':
      "approx_loc G hp ihp ?loc' ?LT'"
      by (auto elim: approx_loc_replace simp add: corresponds_def)

    from wf T methd_C' a_val a_val' a_stk corr T0 val
    have a_stk':
      "approx_stk G hp ihp ?stk' ?ST'"
      apply -
      apply clarsimp
      apply (rule conjI)
       apply (clarsimp simp add: approx_val_def iconf_def init_le_Init2)
       apply (rule conf_widen, assumption+)
       apply (erule widen_trans, assumption)
      apply (unfold approx_stk_def)
      apply (erule disjE)
       apply (elim exE conjE)
       apply (drule approx_loc_replace)
           apply assumption back
          apply assumption 
         apply blast
        apply (simp add: corresponds_def corr_stk_def)
       apply (simp add: replace_map_OK)
      apply (elim exE conjE)
      apply (drule approx_loc_replace)
          apply assumption back
         apply assumption 
        apply blast
       apply (simp add: corresponds_def corr_stk_def)
      apply (simp add: replace_map_OK)
      done
    
    from stk0' apTs cons0
    have "consistent_init stk0' loc0 (ST0,LT0) ihp"
      apply simp
      apply (drule consistent_init_append, simp)
      apply (erule consistent_init_pop)
      done

    with a_stk a_loc0 a_val
    have cons': "consistent_init ?stk' ?loc' (?ST', ?LT') ihp"
      apply -
      apply (rule consistent_init_Init_stk)
      apply (erule consisten_init_replace)
       apply assumption+
      apply (rule refl)
      done      
    
    from stk0' len apTs corr0
    have 
      "fst sig0 = init \<longrightarrow> 
      corresponds (rval # stk0') loc0 (Init rT'#ST0, LT0) ihp (fst r0) (PartInit C0)"
      apply clarsimp
      apply (drule corresponds_append)
       apply simp
      apply (simp add: corresponds_stk_cons)
      done    
    with a_stk a_loc0 a_val
    have corr':
      "fst sig0 = init \<longrightarrow> 
      corresponds ?stk' ?loc' (?ST', ?LT') ihp (fst r0) (PartInit C0)"
      apply -
      apply clarify
      apply (simp add: corresponds_stk_cons)
      apply (erule corresponds_replace)
        apply assumption+
       apply simp
      apply blast
      done

    have fst_r': "fst ?r' = fst r0" by simp

    from lenloc0 a_loc' Suc_pc0 a_stk' cons' fst_r' corr' corr0 
    have c_fr': "correct_frame G hp ihp (?ST', ?LT') maxl0 ins0 ?f'"
      apply (unfold correct_frame_def)
      apply clarify
      apply (clarsimp simp add: map_eq_Cons split del: split_if)
      done    

    from c_frs
    have frs'1: 
      "fst sig0 \<noteq> init \<Longrightarrow> correct_frames G hp ihp phi rT0 sig0 ?z' ?r' frs'"
      apply -
      apply (cases frs')
       apply simp
      apply (clarsimp split del: split_if)
      apply (intro exI conjI)
          apply assumption+
         apply (rule refl)
        apply assumption+
      done 
    moreover
    have frs'2: "frs' = [] \<Longrightarrow> correct_frames G hp ihp phi rT0 sig0 ?z' ?r' frs'"
      by simp
    moreover
    { fix f'' frs'' 
      assume cons: "frs' = f'' # frs''"
      assume sig0_in: "fst sig0 = init"

      { assume eq: "oX = fst r0"
        with corr0 sig0_in
        have "corresponds stk0 loc0 (rev apTs @ T0 # ST0, LT0) ihp oX (PartInit C0)" 
          by simp
        with stk0'
        have "corresponds (oX#stk0') loc0 (T0#ST0, LT0) ihp oX (PartInit C0)" 
          apply simp
          apply (rule corresponds_append)
          apply assumption
          apply simp
          done
        with a ihp_a eq corr0 sig0_in T0 
        have "ihp a = PartInit C0" 
          by (clarsimp simp add: corresponds_stk_cons corr_val_def)
        with a T0 a_val 
        have z0: "T0 = PartInit C0 \<and> ¬z0" 
          by (auto simp add: approx_val_def iconf_def)
        from c_frs sig0_in z0 cons
        have "snd r0 = Null"
          apply -
          apply (drule correct_frames_ctor_ok)
          apply clarsimp
          apply (simp add: constructor_ok_def split_beta)
          done      
        moreover
        have "r0 = (fst r0, snd r0)" by simp
        ultimately
        have eq_r0: "r0 = (oX, Null)" by (simp  add: eq)
        with apTs oX_pos ctor_ok c_frs z cons
        have "correct_frames G hp ihp phi rT0 sig0 True (oX, ?c) frs'"           
          apply (clarsimp split del: split_if)
          apply (intro exI conjI)
               apply assumption+
              apply (rule refl)
             apply assumption+
          apply (rule impI, erule impE, assumption)
           apply (rule constructor_ok_pass_val)
             apply assumption
            apply simp
           apply simp
           apply assumption+
          done
        with oX_pos apTs z0 eq_r0
        have "correct_frames G hp ihp phi rT0 sig0 ?z' ?r' frs'" by simp
      }
      moreover
      { assume neq: "oX \<noteq> fst r0"      
        with T0 stk0' corr0 sig0_in
        have "\<exists>pc'. T0 = UnInit C' pc'" 
          apply simp
          apply (erule disjE)
           apply simp  
          apply clarify
          apply (drule corresponds_append)
           apply simp
          apply (simp add: corresponds_stk_cons)
          done
        with c_frs apTs oX_pos neq
        have "correct_frames G hp ihp phi rT0 sig0 ?z' ?r' frs'" by clarsimp
      }
      ultimately
      have "correct_frames G hp ihp phi rT0 sig0 ?z' ?r' frs'" by blast
    }
    ultimately
    have "correct_frames G hp ihp phi rT0 sig0 ?z' ?r' frs'" 
      by (cases frs', blast+)
    
    with state' heap_ok init_ok c_frs class_C0 methd_C0 phi_Suc_pc0 c_fr' prealloc
    have ?thesis by (unfold correct_state_def) fastsimp
  }
  ultimately
  show "G,phi \<turnstile>JVM state'\<surd>" by (cases frs, blast+)
qed

lemma Return_correct:
"\<lbrakk> wt_jvm_prog G phi; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = Return; 
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  apply (cases "fst sig = init")
   apply (rule Return_correct_init)
   apply assumption+
  apply (rule Return_correct_not_init)
   apply simp
  apply assumption+
  done

lemmas [simp] = map_append

lemma Goto_correct:
"\<lbrakk> wf_prog wt G; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = Goto branch; 
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2)
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply clarsimp
done


lemma Ifcmpeq_correct:
"\<lbrakk> wf_prog wt G; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = Ifcmpeq branch; 
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2)
apply (drule bspec, assumption)
apply clarsimp
apply (rule conjI, rule impI)
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply clarsimp
 apply (rule conjI)
  apply (drule consistent_init_pop)+
  apply assumption
 apply (rule impI, erule impE, assumption, erule conjE)
  apply (drule corresponds_pop)+
  apply assumption
apply (rule impI)
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply clarsimp
apply (rule conjI)
 apply (drule consistent_init_pop)+
 apply assumption
apply (rule impI, erule impE, assumption, erule conjE)
apply (drule corresponds_pop)+
apply assumption
done

lemma Pop_correct:
"\<lbrakk> wf_prog wt G; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = Pop;
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply clarsimp
apply (fast dest: consistent_init_pop corresponds_pop)
done


lemma Dup_correct:
"\<lbrakk> wf_prog wt G; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = Dup;
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply clarsimp
apply (rule conjI)
 apply (erule consistent_init_Dup)
apply (rule impI, erule impE, assumption, erule conjE)
apply (erule corresponds_Dup)
done


lemma Dup_x1_correct: 
"\<lbrakk> wf_prog wt G; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = Dup_x1;
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply clarsimp
apply (rule conjI)
 apply (erule consistent_init_Dup_x1)
apply (rule impI, erule impE, assumption, erule conjE)
apply (erule corresponds_Dup_x1)
done


lemma Dup_x2_correct:
"\<lbrakk> wf_prog wt G; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = Dup_x2;
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply clarsimp
apply (rule conjI)
 apply (erule consistent_init_Dup_x2)
apply (rule impI, erule impE, assumption, erule conjE)
apply (erule corresponds_Dup_x2)
done


lemma Swap_correct:
"\<lbrakk> wf_prog wt G; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = Swap;
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply clarsimp
apply (rule conjI)
 apply (erule consistent_init_Swap)
apply (rule impI, erule impE, assumption, erule conjE)
apply (erule corresponds_Swap)
done


lemma IAdd_correct:
"\<lbrakk> wf_prog wt G; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = IAdd; 
  wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons) 
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply (clarsimp simp add: approx_val_def iconf_def init_le_Init conf_def)
apply (simp add: is_init_def)
apply (drule consistent_init_pop)+
apply (simp add: corresponds_stk_cons)
apply (blast intro: consistent_init_Init_stk)                    
done

lemma Throw_correct:
"\<lbrakk> wf_prog wt G; 
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  ins ! pc = Throw; 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ; 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
  fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  by simp


lemma Jsr_correct:
  "\<lbrakk>wf_prog wt G;
  method (G, C) sig = Some (C, rT, maxs, maxl, ins, et); 
  Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
  G,phi \<turnstile>JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) \<surd>;
  wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
  fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None; ins ! pc = Jsr b\<rbrakk>
  \<Longrightarrow> G,phi \<turnstile>JVM state' \<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons) 
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply clarsimp
apply (rule conjI)
 apply (simp add: approx_val_def iconf_def is_init_def)
apply (rule conjI)
 apply (erule consistent_init_Init_stk)
apply (rule impI, erule impE, assumption, erule conjE)
apply (simp add: corresponds_def corr_stk_def corr_loc_cons)
done


lemma phi_finite:
  assumes wt: "wt_jvm_prog G phi"
  assumes meth: "method (G, C) sig = Some (C, rT, maxs, maxl, ins, et)"
  assumes corr: "G,phi \<turnstile>JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) \<surd>"
  shows "finite (phi C sig!pc)"
proof -
  from corr meth
  have len: "pc < length ins" and "is_class G C"
    by (unfold correct_state_def correct_frame_def) auto
  with wt meth
  have "wt_method G C (fst sig) (snd sig) rT maxs maxl ins et (phi C sig)"
    by (auto dest: method_wf_mdecl simp add: wt_jvm_prog_def wf_mdecl_def)
  with len obtain maxr where
    "set (phi C sig) \<subseteq> Pow (address_types G maxs maxr (length ins))" 
    "pc < length (phi C sig)"
    by (clarsimp simp add: wt_method_def check_types_def states_def)
  hence "phi C sig ! pc \<in> Pow (address_types G maxs maxr (length ins))"
    by (auto intro!: nth_in)
  thus ?thesis by (auto elim: finite_subset intro: finite_address_types)
qed


lemma obj_ty_is_RefT [simp, dest!]:
  "obj_ty x = PrimT T \<Longrightarrow> False"
  apply (cases x)
  apply auto
  done

lemma Ret_correct:
  "\<lbrakk>wt_jvm_prog G phi;
  method (G, C) sig = Some (C, rT, maxs, maxl, ins, et); Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
  G,phi \<turnstile>JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) \<surd>;
  wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
  fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None; ins ! pc = Ret idx\<rbrakk>
  \<Longrightarrow> G,phi \<turnstile>JVM state' \<surd>"
apply (frule phi_finite, assumption+)
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons) 
apply (simp add: set_SOME_lists finite_imageI)
apply (drule bspec, assumption)
apply clarsimp
apply (drule bspec)
apply (rule UnI1)
apply (rule imageI)
apply (rule imageI)
apply assumption
apply (clarsimp simp add: theRA_def)
apply (subgoal_tac "loc!idx = RetAddr ra")
apply (simp add: split_def)
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply simp
 apply (rule conjI, assumption)
 apply simp
 apply simp
apply (clarsimp simp add: approx_loc_def list_all2_conv_all_nth)
apply (erule allE, erule impE, assumption)
apply (clarsimp simp add: approx_val_def iconf_def conf_def)
apply (cases "loc!idx")
apply auto
done

lemma conf_ArrayD:
  "G,hp \<turnstile> s ::\<preceq> T.[] \<Longrightarrow>
  s = Null \<or> (\<exists>l T' len en. s = Addr l \<and> hp l = Some (Arr T' len en) \<and> G \<turnstile> T' \<preceq> T)"  
  apply (cases s)
  apply (auto simp add: conf_def)
  apply (case_tac z)
  apply (auto dest: widen_Array_Array widen_Array2)
  done
  

lemma ArrLength_correct:
  "\<lbrakk>wf_prog wf_mb G;
  method (G, C) sig = Some (C, rT, maxs, maxl, ins, et); Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
  G,phi \<turnstile>JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) \<surd>;
  wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
  fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None; ins ! pc = ArrLength\<rbrakk>
  \<Longrightarrow> G,phi \<turnstile>JVM state' \<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons split_beta)
apply (drule bspec, assumption)
apply clarsimp 
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply (clarsimp simp add: approx_val_def iconf_def dest!: conf_ArrayD)
apply (erule disjE, simp)
apply (clarsimp simp add: is_init_def)
apply (rule conjI)
 apply (drule consistent_init_pop)
 apply (erule consistent_init_Init_stk)
apply (rule impI, erule impE, assumption, erule conjE)
apply (drule corresponds_pop)
apply (simp add: corresponds_stk_cons)
done

lemma conf_IntegerD:
  "G,hp \<turnstile> v ::\<preceq> PrimT Integer \<Longrightarrow> \<exists>i. v = Intg i"
  apply (unfold conf_def)
  apply (cases v)
  apply auto
  done
  
lemma not_int:
  "\<lbrakk>¬ int len \<le> i; ¬ i < 0\<rbrakk> \<Longrightarrow> nat i < len"
  by (simp add: linorder_not_le nat_less_iff)
  

lemma ArrLoad_correct:
  "\<lbrakk>wf_prog wf_mb G;
  method (G, C) sig = Some (C, rT, maxs, maxl, ins, et); Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
  G,phi \<turnstile>JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) \<surd>;
  wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
  fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None; ins ! pc = ArrLoad\<rbrakk>
  \<Longrightarrow> G,phi \<turnstile>JVM state' \<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons split_beta)
apply (drule bspec, assumption)
apply clarsimp 
apply (rule exI)+
apply (rule conjI)
 apply (erule subsetD)
 apply (erule imageE2)
 apply simp
 apply (rule conjI, rule refl)+
 apply (rule refl)
apply (clarsimp simp add: approx_val_def iconf_def raise_system_xcpt_def 
                dest!: conf_ArrayD conf_IntegerD split: split_if_asm)
apply (clarsimp simp add: is_init_def)
apply (drule hconfD, assumption)
apply (clarsimp simp add: oconf_def)
apply (drule not_int, assumption)
apply (erule allE, erule impE, assumption)
apply clarsimp
apply (rule conjI)
 apply (erule conf_widen, assumption+)
apply (rule conjI)
 apply (clarsimp simp add: h_init_def)
 apply (erule allE, erule allE, erule impE, assumption)
 apply (clarsimp simp add: o_init_def l_init_def)
 apply (erule_tac x="nat i" in allE)
 apply (erule impE) back
  apply simp
 apply (clarsimp simp add: is_init_def)
apply (rule conjI)
 apply (drule consistent_init_pop)+
 apply (erule consistent_init_Init_stk)
apply (rule impI, erule impE, assumption, erule conjE)
apply (simp add: corresponds_stk_cons)
done


lemma iconf_Init [iff]:
  "(G,hp,ihp \<turnstile> v ::\<preceq>i Init T) = (G,hp \<turnstile> v ::\<preceq> T \<and> is_init hp ihp v)"
  by (unfold iconf_def) simp


lemma oconf_array_update:
  "\<lbrakk>G,hp \<turnstile> v ::\<preceq> T; G,hp \<turnstile> (Arr T l en)\<surd> \<rbrakk>
  \<Longrightarrow> G,hp \<turnstile> Arr T l (en(i\<mapsto>v)) \<surd>"
  by (simp add: oconf_def lconf_def)


lemma hconf_array_update:
  "\<lbrakk>G \<turnstile>h hp\<surd>;
    hp oloc = Some (Arr T l en);
    G,hp \<turnstile> v ::\<preceq> T\<rbrakk> \<Longrightarrow>
  G \<turnstile>h hp(oloc \<mapsto> Arr T l (en(i\<mapsto>v)))\<surd>"
  apply (simp add: hconf_def)  
  apply (force intro: oconf_imp_oconf_heap_update oconf_array_update 
               simp add: obj_ty_def)
  done


lemma h_init_array_update:
  "\<lbrakk> h_init G hp ihp; hp x = Some (Arr T l en); is_init hp ihp v \<rbrakk>
  \<Longrightarrow> h_init G (hp(x\<mapsto>Arr T l (en(i\<mapsto>v)))) ihp"
  apply (unfold h_init_def o_init_def l_init_def)
  apply clarsimp
  apply (rule conjI)
   apply clarify
   apply (rule conjI)
    apply (clarsimp simp add: is_init_def)
   apply clarsimp
   apply (elim allE, erule impE, assumption)
   apply (clarsimp split: split_if_asm)
   apply (elim allE, erule impE, assumption)
   apply (clarsimp simp add: is_init_def)
  apply (clarsimp split: heap_entry.split)
  apply (rule conjI)
   apply clarify
   apply (elim allE, erule impE, assumption, simp,
          elim allE, 
          erule impE, rule exI, assumption)
   apply (clarsimp simp add: is_init_def)
  apply clarify
  apply (elim allE, erule impE, assumption) back
  apply simp
  apply (erule allE, erule impE, simp)
  apply (clarsimp simp add: is_init_def)  
  done  

lemma ArrStore_correct:
  assumes wf:   "wf_prog wt G"
  assumes meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
  assumes ins:  "ins!pc = ArrStore"
  assumes wt:   "wt_instr (ins!pc) G C rT (phi C sig) maxs 
                         (fst sig = init) (length ins) et pc"
  assumes exec: "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
  assumes conf: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
  assumes no_x: "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None"

  shows "G,phi \<turnstile>JVM state' \<surd>"
proof -
  from ins conf meth
  obtain ST LT z where
    heap_ok:    "G\<turnstile>h hp\<surd>" and
    pre_alloc:  "preallocated hp ihp" and
    init_ok:    "h_init G hp ihp" and
    phi_pc:     "((ST,LT),z) \<in> phi C sig!pc" and
    is_class_C: "is_class G C" and
    frame:      "correct_frame G hp ihp (ST,LT) maxl ins (stk,loc,C,sig,pc,r)" and
    frames:     "correct_frames G hp ihp phi rT sig z r frs"
    by (fastsimp elim: correct_stateE)

  from phi_pc ins wt
  obtain T T' tST where 
    ST:      "ST = Init T # Init (PrimT Integer) # Init (T'.[]) # tST" and
    suc_pc:  "Suc pc < length ins" and
    phi_suc: "((tST, LT),z) \<in> phi C sig ! Suc pc" 
    apply (unfold wt_instr_def eff_defs)
    apply clarsimp
    apply (drule bspec, assumption)
    apply clarsimp
    apply (drule subsetD)
    apply (rule imageI, assumption)
    apply clarsimp
    apply blast
    done

  from ST frame 
  obtain val idx aref stk' where
    stk : "stk = val # idx # aref # stk'" and
    val : "G,hp,ihp \<turnstile> val ::\<preceq>i Init T" and
    idx : "G,hp,ihp \<turnstile> idx ::\<preceq>i Init (PrimT Integer)" and
    aref: "G,hp,ihp \<turnstile> aref ::\<preceq>i Init (T'.[])" and
    app_s: "approx_stk G hp ihp stk' tST" and
    app_l: "approx_loc G hp ihp loc LT" and
    consi: "consistent_init stk loc (ST,LT) ihp" and
    corr:  "fst sig = init \<longrightarrow> 
            corresponds stk loc (ST,LT) ihp (fst r) (PartInit C) \<and>
            (\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and> 
            (ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))" and
    len_l: "length loc = Suc (length (snd sig) + maxl)"
    by (clarsimp elim!: correct_frameE simp add: approx_val_def) blast

  from exec ins meth stk no_x
  have "aref \<noteq> Null" by (auto simp add: split_beta raise_system_xcpt_def)
  with aref
  obtain x T'' len en where
    addr:    "aref = Addr x" and
    hp_Some: "hp x = Some (Arr T'' len en)"
    by (fastsimp simp add: iconf_def dest!: conf_ArrayD)
  moreover
  from idx obtain i where
    i: "idx = Intg i"
    by (fastsimp simp add: conf_def dest: conf_IntegerD)
  moreover note exec ins meth stk no_x
  ultimately
  obtain val_T'': "G,hp \<turnstile> val ::\<preceq> T''" 
    and  bounds: "¬i < 0 \<and> ¬int len \<le> i"    
    by (auto simp add: raise_system_xcpt_def split: split_if_asm)

  let ?hp' = "hp(x\<mapsto>Arr T'' len (en(nat i\<mapsto>val)))" 
  and ?f'  = "(stk', loc, C, sig, Suc pc, r)"
  
  from exec ins meth stk addr i bounds hp_Some val_T''
  have state': "state' = Norm (?hp', ihp, ?f'#frs)"
    by (simp add: raise_system_xcpt_def)

  from hp_Some have hext: "hp \<le>| ?hp'" by (rule hext_upd_arr)

  from heap_ok hp_Some val_T'' 
  have hp'_ok: "G \<turnstile>h ?hp' \<surd>" by (rule hconf_array_update)
  moreover
  from val have "is_init hp ihp val" by (clarsimp simp add: init_le_Init2)    
  with init_ok hp_Some have hp'_init: "h_init G ?hp' ihp" 
    by (rule h_init_array_update)
  moreover
  from hp_Some heap_ok pre_alloc have pre_alloc': "preallocated ?hp' ihp" 
    by (rule preallocated_array_update)
  moreover
  from corr ST stk have corr':
    "fst sig = init \<longrightarrow>
    corresponds stk' loc (tST, LT) ihp (fst r) (PartInit C) \<and>
    (\<exists>l. fst r = Addr l \<and> ?hp' l \<noteq> None \<and> 
        (ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))"
    by (clarsimp simp add: corresponds_stk_cons simp del: fun_upd_apply) simp
  moreover
  from consi ST stk have "consistent_init stk' loc (tST, LT) ihp"
    by (blast intro: consistent_init_pop)
  with wf app_l app_s len_l suc_pc hext corr' ST stk
  have f'_correct: 
    "correct_frame G ?hp' ihp (tST, LT) maxl ins (stk',loc,C,sig,Suc pc,r)"
    by (simp add: correct_frame_def)
       (blast intro: approx_stk_imp_approx_stk_sup_heap
                     approx_loc_imp_approx_loc_sup_heap)
  moreover
  from frames hp_Some 
  have "correct_frames G ?hp' ihp phi rT sig z r frs"
    by (rule correct_frames_array_update)
  moreover
  note state' ins meth is_class_C phi_suc
  ultimately
  show ?thesis by simp (rule correct_stateI)
qed

lemma oconf_blank_arr:
  "G,hp \<turnstile> blank_arr T (nat l) \<surd>" 
  apply (unfold oconf_def blank_arr_def conf_def)
  apply (cases T)
  apply auto
  apply (case_tac prim_ty)
  apply auto
  done


lemma h_init_new_array:
  "\<lbrakk>hp r = None; G \<turnstile>h hp \<surd>; h_init G hp ihp\<rbrakk> \<Longrightarrow> h_init G (hp(r\<mapsto>blank_arr T l)) (ihp(r := T'))"
  apply (unfold h_init_def o_init_def l_init_def blank_arr_def)
  apply clarsimp
  apply (rule conjI)
   apply clarsimp
   apply (rule is_init_default_val)
  apply (clarsimp split: heap_entry.split)
  apply (rule conjI)
   apply clarify
   apply (elim allE, erule impE, assumption)
   apply simp
   apply (elim allE, erule impE)
    apply fastsimp
   apply clarsimp
   apply (simp add: is_init_def)
   apply (drule hconfD, assumption)
   apply (drule oconf_objD, assumption)
   apply clarsimp
   apply (drule new_locD, assumption) 
   apply simp
  apply clarify
  apply (elim allE, erule impE, assumption)
  apply simp
  apply (elim allE, erule impE)
   apply fastsimp
  apply clarsimp
  apply (simp add: is_init_def)
  apply (drule hconfD, assumption) 
  apply (drule oconf_arrD, assumption)
  apply clarsimp
  apply (drule new_locD, assumption)
  apply simp    
  done



lemma ArrNew_correct:
  assumes wf:   "wf_prog wt G"
  assumes meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
  assumes ins:  "ins!pc = ArrNew T"
  assumes wt:   "wt_instr (ins!pc) G C rT (phi C sig) maxs 
                         (fst sig = init) (length ins) et pc"
  assumes exec: "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
  assumes conf: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
  assumes no_x: "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None"

  shows "G,phi \<turnstile>JVM state' \<surd>"
proof -
  from ins conf meth
  obtain ST LT z where
    heap_ok:    "G\<turnstile>h hp\<surd>" and
    pre_alloc:  "preallocated hp ihp" and
    init_ok:    "h_init G hp ihp" and
    phi_pc:     "((ST,LT),z) \<in> phi C sig!pc" and
    is_class_C: "is_class G C" and
    frame:      "correct_frame G hp ihp (ST,LT) maxl ins (stk,loc,C,sig,pc,r)" and
    frames:     "correct_frames G hp ihp phi rT sig z r frs"
    by (fastsimp elim: correct_stateE)

  from phi_pc ins wt
  obtain ST' where 
    ST:      "ST = Init (PrimT Integer) # ST'" and
    type:    "is_type G T" "noRA T" "Suc (dim T) \<le> max_dim" and
    suc_pc:  "Suc pc < length ins" and    
    phi_suc: "((Init (T.[]) # ST', LT),z) \<in> phi C sig ! Suc pc" (is "((?ST',_),_) \<in> _")
    apply (unfold wt_instr_def eff_defs)
    apply clarsimp
    apply (drule bspec, assumption)
    apply clarsimp
    apply (drule subsetD)
    apply (rule imageI, assumption)
    apply clarsimp
    done

  from ST frame 
  obtain len stk' where
    stk : "stk = len # stk'" and
    len : "G,hp,ihp \<turnstile> len ::\<preceq>i Init (PrimT Integer)" and
    app_s: "approx_stk G hp ihp stk' ST'" and
    app_l: "approx_loc G hp ihp loc LT" and
    consi: "consistent_init stk loc (ST,LT) ihp" and
    corr:  "fst sig = init \<longrightarrow> 
            corresponds stk loc (ST,LT) ihp (fst r) (PartInit C) \<and>
            (\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and> 
            (ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))" and
    len_l: "length loc = Suc (length (snd sig) + maxl)"
    by (clarsimp elim!: correct_frameE simp add: approx_val_def) blast

  from len obtain l where l: "len = Intg l" by (clarsimp dest!: conf_IntegerD)

  obtain ref xp' where
    new_Addr: "new_Addr hp = (ref,xp')"
    by (cases "new_Addr hp") 
  with ins l stk no_x
  obtain hp: "hp ref = None" and "xp' = None" and pos: "¬ l < 0"
    by (auto dest: new_AddrD simp add: raise_system_xcpt_def split: split_if_asm)
  
  with exec ins meth new_Addr l stk 
  have state':
    "state' = Norm (hp(ref\<mapsto>blank_arr T (nat l)), ihp(ref := Init (T.[])),
                    (Addr ref # stk', loc, C, sig, Suc pc, r) # frs)" 
    (is "state' = Norm (?hp', ?ihp', ?f # frs)")
    by (simp add: raise_system_xcpt_def)
  moreover
  from hp heap_ok have hp': "G \<turnstile>h ?hp' \<surd>" by (intro hconf_imp_hconf_newref oconf_blank_arr) 
  moreover
  from hp heap_ok init_ok 
  have "h_init G ?hp' ?ihp'" by (rule h_init_new_array)
  moreover
  from hp have sup: "hp \<le>| ?hp'" by (rule hext_new)
  from frame obtain
    cons:  "consistent_init stk loc (ST, LT) ihp" and
    a_loc: "approx_loc G hp ihp loc LT" and
    a_stk: "approx_stk G hp ihp stk ST" and
    corr:  "fst sig = init \<longrightarrow>
      corresponds stk loc (ST, LT) ihp (fst r) (PartInit C) \<and>
      (\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and> 
       (ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))"
    ..
  have ref_conf: "G,hp(ref\<mapsto>blank_arr T (nat l)) \<turnstile> Addr ref ::\<preceq> T.[]"
    by (unfold conf_def blank_arr_def) auto
  from corr a_loc a_stk hp ST stk
  have corr': 
    "fst sig = init \<longrightarrow>
     corresponds (Addr ref#stk') loc (?ST', LT) ?ihp' (fst r) (PartInit C) \<and>
     (\<exists>l. fst r = Addr l \<and> ?hp' l \<noteq> None \<and> 
      (?ihp' l = PartInit C \<or> (\<exists>C'. ?ihp' l = Init (Class C'))))"
    apply (clarsimp simp add: corresponds_stk_cons simp del: fun_upd_apply)
    apply (auto intro: corresponds_new_val2)
    done  
  from cons ST stk a_loc a_stk hp
  have "consistent_init (Addr ref # stk') loc (?ST',LT) ?ihp'"
    by (auto intro: consistent_init_Init_stk consistent_init_new_val dest: consistent_init_pop)
  with hp sup frame suc_pc wf corr' a_stk a_loc stk ST ref_conf
  have "correct_frame G ?hp' ?ihp' (?ST', LT) maxl ins ?f" 
    apply (unfold correct_frame_def)
    apply (clarsimp simp add: corresponds_stk_cons)
    apply (rule conjI)
     apply (clarsimp simp add: approx_val_def is_init_def)    
    apply (blast intro: approx_stk_newref 
                        approx_stk_imp_approx_stk_sup_heap 
                        approx_loc_imp_approx_loc_sup_heap 
                        approx_loc_newref 
                        approx_val_newref
                        sup)
    done      
  moreover
  from hp frames
  have "correct_frames G ?hp' ?ihp' phi rT sig z r frs"
    by (rule correct_frames_imp_correct_frames_newref)
  moreover
  from hp pre_alloc have "preallocated ?hp' ?ihp'" by (rule preallocated_newref)  
  ultimately
  show ?thesis by simp (rule correct_stateI)
qed


text {*
  The next theorem collects the results of the sections above,
  i.e.~exception handling and the execution step for each 
  instruction. It states type safety for single step execution:
  in welltyped programs, a conforming state is transformed
  into another conforming state when one instruction is executed.
*}
theorem instr_correct:
"\<lbrakk> wt_jvm_prog G phi;
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs); 
  G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk> 
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (frule wt_jvm_prog_impl_wt_instr_cor)
apply assumption+
apply (cases "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs)")
defer
apply (erule xcpt_correct, assumption+) 
apply (cases "ins!pc")
prefer 21
apply (rule Ret_correct, assumption+)
prefer 8
apply (rule Invoke_correct, assumption+)
prefer 8
apply (rule Invoke_special_correct, assumption+)
prefer 8
apply (rule Return_correct, assumption+)
prefer 5
apply (rule Getfield_correct, assumption+)
prefer 6
apply (rule Checkcast_correct, assumption+)

apply (unfold wt_jvm_prog_def)
apply (rule Load_correct, assumption+)
apply (rule Store_correct, assumption+)
apply (rule LitPush_correct, assumption+)
apply (rule New_correct, assumption+)
apply (rule Putfield_correct, assumption+)
apply (rule Pop_correct, assumption+)
apply (rule Dup_correct, assumption+)
apply (rule Dup_x1_correct, assumption+)
apply (rule Dup_x2_correct, assumption+)
apply (rule Swap_correct, assumption+)
apply (rule IAdd_correct, assumption+)
apply (rule Goto_correct, assumption+)
apply (rule Ifcmpeq_correct, assumption+)
apply (rule Throw_correct, assumption+)
apply (rule Jsr_correct, assumption+)
apply (rule ArrLoad_correct, assumption+)
apply (rule ArrStore_correct, assumption+)
apply (rule ArrLength_correct, assumption+)
apply (rule ArrNew_correct, assumption+)
done

section {* Main *}

lemma correct_state_impl_Some_method:
  "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> 
  \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
by (auto simp add: correct_state_def Let_def)


lemma BV_correct_1 [rule_format]:
"\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> 
 \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (simp only: split_tupled_all)
apply (rename_tac xp hp ihp frs)
apply (case_tac xp)
 apply (case_tac frs)
  apply simp
 apply (simp only: split_tupled_all)
 apply hypsubst
 apply (frule correct_state_impl_Some_method)
 apply (force intro: instr_correct)
apply (case_tac frs)
apply simp_all
done

lemma L0:
  "\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,ihp,frs) = Some state')"
by (clarsimp simp add: neq_Nil_conv split_beta)

lemma L1:
  "\<lbrakk>wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,ihp,frs)\<surd>; xp=None; frs\<noteq>[]\<rbrakk> 
  \<Longrightarrow> \<exists>state'. exec(G,xp,hp,ihp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
apply (drule L0)
apply assumption
apply (fast intro: BV_correct_1)
done

theorem BV_correct [rule_format]:
"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>"
apply (unfold exec_all_def)
apply (erule rtrancl_induct)
 apply simp
apply (auto intro: BV_correct_1)
done


theorem BV_correct_implies_approx:
"\<lbrakk> wt_jvm_prog G phi; 
  G \<turnstile> s0 -jvm\<rightarrow> (None,hp,ihp,(stk,loc,C,sig,pc,r)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk> 
\<Longrightarrow> \<exists>ST LT z. ((ST,LT),z) \<in> (phi C sig) ! pc \<and>
    approx_stk G hp ihp stk ST \<and> 
    approx_loc G hp ihp loc LT"
apply (drule BV_correct)
apply assumption+
apply (clarsimp simp add: correct_state_def correct_frame_def split_def 
            split: option.splits)
apply blast
apply blast
done

lemma hconf_start:
  fixes G :: jvm_prog ("\<Gamma>")
  assumes wf: "wf_prog wf_mb \<Gamma>"
  shows "\<Gamma> \<turnstile>h (start_heap \<Gamma>) \<surd>"
  apply (unfold hconf_def start_heap_def)
  apply (auto simp add: blank_def oconf_def split: split_if_asm)
  apply (simp add: fields_is_type [OF _ wf is_class_xcpt [OF wf]])+
  done

lemma hinit_start:
  fixes G :: jvm_prog ("\<Gamma>")
  assumes wf: "wf_prog wf_mb \<Gamma>"
  shows "h_init \<Gamma> (start_heap \<Gamma>) start_iheap"
  apply (unfold h_init_def start_heap_def start_iheap_def)
  apply (auto simp add: blank_def o_init_def l_init_def 
                        is_init_def split: split_if_asm)  
  apply (auto simp add: init_vars_def map_of_map)
  done
   
lemma consistent_init_start:
  "consistent_init [] (Null#replicate n arbitrary) ([],  OK (Init (Class C))#replicate n Err) hp"  
  apply (induct n)
  apply (auto simp add: consistent_init_def corresponds_def corr_stk_def corr_loc_def)
  done

lemma BV_correct_initial: 
  fixes G :: jvm_prog ("\<Gamma>") and Phi :: prog_type ("\<Phi>")
  shows 
  "wt_jvm_prog \<Gamma> \<Phi> \<Longrightarrow> is_class \<Gamma> C \<Longrightarrow> method (\<Gamma>,C) (m,[]) = Some (C, b) \<Longrightarrow> m \<noteq> init
  \<Longrightarrow> \<Gamma>,\<Phi> \<turnstile>JVM start_state G C m \<surd>"
  apply (cases b)
  apply (unfold  start_state_def)
  apply (unfold correct_state_def)
  apply (auto simp add: preallocated_start)
    apply (simp add: wt_jvm_prog_def hconf_start)
   apply (simp add: wt_jvm_prog_def hinit_start)
  apply (drule wt_jvm_prog_impl_wt_start, assumption+)
  apply (clarsimp simp add: wt_start_def)
  apply (auto simp add: correct_frame_def)
    apply (simp add: approx_stk_def)
  apply (rule exI, rule conjI)
  apply (rule exI, assumption)
  apply clarsimp 
  apply (simp add: consistent_init_start)
  apply (auto simp add: approx_val_def iconf_def is_init_def dest!: widen_RefT)
  done  

theorem typesafe:
  fixes G :: jvm_prog ("\<Gamma>") and Phi :: prog_type ("\<Phi>")
  assumes welltyped: "wt_jvm_prog \<Gamma> \<Phi>" and
          main: "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)" "m \<noteq> init"
  shows 
  "G \<turnstile> start_state \<Gamma> C m -jvm\<rightarrow> s  \<Longrightarrow>  \<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
proof -
  from welltyped main
  have "\<Gamma>,\<Phi> \<turnstile>JVM start_state \<Gamma> C m \<surd>" by (rule BV_correct_initial)
  moreover
  assume "G \<turnstile> start_state \<Gamma> C m -jvm\<rightarrow> s"
  ultimately  
  show "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" using welltyped by - (rule BV_correct)
qed
  
end

Preliminaries

lemmas defs1:

  correct_state G phi ==
  %(xp, hp, ihp, frs).
     case xp of
     None =>
       case frs of [] => True
       | f # fs =>
           G |-h hp [ok] &
           h_init G hp ihp &
           preallocated hp ihp &
           (let (stk, loc, C, sig, pc, r) = f
            in EX rT maxs maxl ins et s z.
                  is_class G C &
                  method (G, C) sig = Some (C, rT, maxs, maxl, ins, et) &
                  (s, z) : phi C sig ! pc &
                  correct_frame G hp ihp s maxl ins f &
                  correct_frames G hp ihp phi rT sig z r fs)
     | Some x => frs = []
  correct_frame G hp i ==
  %(ST, LT) maxl ins (stk, loc, C, sig, pc, r).
     approx_stk G hp i stk ST &
     approx_loc G hp i loc LT &
     consistent_init stk loc (ST, LT) i &
     (fst sig = init -->
      corresponds stk loc (ST, LT) i (fst r) (PartInit C) &
      (EX l. fst r = Addr l &
             hp l ~= None &
             (i l = PartInit C | (EX C'. i l = Init (Class C'))))) &
     pc < length ins & length loc = length (snd sig) + maxl + 1
  wt_instr i G C rT phi mxs ini max_pc et pc ==
  app i G C pc mxs max_pc rT ini et (phi ! pc) &
  (ALL (pc', s'):set (eff i G pc et (phi ! pc)). pc' < max_pc & s' <= phi ! pc')
  eff i G pc et at ==
  map (%pc'. (pc', norm_eff i G pc pc' at)) (succs i pc at) @
  xcpt_eff i G pc at et
  norm_eff i G pc pc' at ==
  eff_bool i G pc `
  (if EX idx. i = Ret idx then {s. s : at & pc' = theRA (theIdx i) s} else at)
  eff_bool i G pc ==
  %((ST, LT), z).
     (eff' (i, G, pc, ST, LT),
      if EX C p D. i = Invoke_special C init p & ST ! length p = PartInit D
      then True else z)

lemmas correctE:

  [| G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     !!ST LT z.
        [| G |-h hp [ok]; h_init G hp ihp; preallocated hp ihp; is_class G C;
           ((ST, LT), z) : phi C sig ! pc;
           correct_frame G hp ihp (ST, LT) maxl ins (stk, loc, C, sig, pc, r);
           correct_frames G hp ihp phi rT sig z r frs |]
        ==> P |]
  ==> P
  [| correct_frame G hp ihp (ST, LT) maxl ins (stk, loc, C, sig, pc, r);
     [| approx_stk G hp ihp stk ST; approx_loc G hp ihp loc LT;
        consistent_init stk loc (ST, LT) ihp;
        fst sig = init -->
        corresponds stk loc (ST, LT) ihp (fst r) (PartInit C) &
        (EX l. fst r = Addr l &
               hp l ~= None &
               (ihp l = PartInit C | (EX C'. ihp l = Init (Class C'))));
        pc < length ins; length loc = length (snd sig) + maxl + 1 |]
     ==> P |]
  ==> P

lemmas

  (ALL x. P x) = (ALL a b. P (a, b))

lemma wt_jvm_prog_impl_wt_instr_cor:

  [| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
       pc

Exception Handling

lemma exec_instr_xcpt:

  (fst (exec_instr i G hp ihp stk vars Cl sig pc z frs) = Some xcp) =
  (EX stk'.
      exec_instr i G hp ihp stk vars Cl sig pc z frs =
      (Some xcp, hp, ihp, (stk', vars, Cl, sig, pc, z) # frs))

lemma in_match_any:

  match_exception_table G xcpt pc et = Some pc'
  ==> EX C. C : set (match_any G pc et) &
            G |- xcpt <=C C & match_exception_table G C pc et = Some pc'

lemma match_et_imp_match:

  match_exception_table G X pc et = Some handler ==> match G X pc et = [X]

lemma imageE2:

  [| x : A; y = f x |] ==> y : f ` A

lemma subcls_obj:

  G |- Object <=C C = (C = Object)

lemma uncaught_xcpt_correct:

  [| wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T; is_init hp ihp xcp;
     G,phi |-JVM Norm (hp, ihp, f # frs) [ok] |]
  ==> G,phi |-JVM find_handler G (Some xcp) hp ihp frs [ok]

lemma

  [| fst (exec_instr (ins ! pc) G hp ihp stk vars Cl sig pc r frs) = Some xcp;
     wt_instr (ins ! pc) G Cl rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> EX adr T. xcp = Addr adr & hp adr = Some T & is_init hp ihp xcp

lemma cname_of_xcp:

  [| preallocated hp ihp; xcp = Addr (XcptRef x) |] ==> cname_of hp xcp = Xcpt x

lemma prealloc_is_init:

  preallocated hp ihp ==> is_init hp ihp (Addr (XcptRef x))

lemma wt_jvm_progE:

  [| wt_jvm_prog G phi; !!wt. wf_prog wt G ==> P |] ==> P

lemma

  [| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = Some xcp;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

Single Instructions

lemmas

  (x ~= Err) = (EX a. x = OK a)

lemma Load_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Load idx;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemma Store_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Store idx;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemma LitPush_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = LitPush v;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemma widen_Array_Class2:

  G |- T.[] <= Class C = (C = Object)

lemma Cast_conf2:

  [| wf_prog ok G; G,h |- v ::<= RefT rt; cast_ok G C h v; G |- Class C <= T;
     is_class G C |]
  ==> G,h |- v ::<= T

lemmas defs2:

  correct_state G phi ==
  %(xp, hp, ihp, frs).
     case xp of
     None =>
       case frs of [] => True
       | f # fs =>
           G |-h hp [ok] &
           h_init G hp ihp &
           preallocated hp ihp &
           (let (stk, loc, C, sig, pc, r) = f
            in EX rT maxs maxl ins et s z.
                  is_class G C &
                  method (G, C) sig = Some (C, rT, maxs, maxl, ins, et) &
                  (s, z) : phi C sig ! pc &
                  correct_frame G hp ihp s maxl ins f &
                  correct_frames G hp ihp phi rT sig z r fs)
     | Some x => frs = []
  correct_frame G hp i ==
  %(ST, LT) maxl ins (stk, loc, C, sig, pc, r).
     approx_stk G hp i stk ST &
     approx_loc G hp i loc LT &
     consistent_init stk loc (ST, LT) i &
     (fst sig = init -->
      corresponds stk loc (ST, LT) i (fst r) (PartInit C) &
      (EX l. fst r = Addr l &
             hp l ~= None &
             (i l = PartInit C | (EX C'. i l = Init (Class C'))))) &
     pc < length ins & length loc = length (snd sig) + maxl + 1
  wt_instr i G C rT phi mxs ini max_pc et pc ==
  app i G C pc mxs max_pc rT ini et (phi ! pc) &
  (ALL (pc', s'):set (eff i G pc et (phi ! pc)). pc' < max_pc & s' <= phi ! pc')
  eff i G pc et at ==
  map (%pc'. (pc', norm_eff i G pc pc' at)) (succs i pc at) @
  xcpt_eff i G pc at et
  norm_eff i G pc pc' at ==
  eff_bool i G pc `
  (if EX idx. i = Ret idx then {s. s : at & pc' = theRA (theIdx i) s} else at)
  eff_bool i G pc ==
  %((ST, LT), z).
     (eff' (i, G, pc, ST, LT),
      if EX C p D. i = Invoke_special C init p & ST ! length p = PartInit D
      then True else z)
  raise_system_xcpt b x == if b then Some (Addr (XcptRef x)) else None

lemma Checkcast_correct:

  [| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Checkcast D;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
  ==> G,phi |-JVM state' [ok]

lemma non_np_objD:

  [| a' ~= Null; G,h |- a' ::<= Class D; field (G, D) F = Some (D, vT);
     wf_prog b G |]
  ==> EX a C fs. a' = Addr a & h a = Some (Obj C fs) & G |- C <=C D

lemma Getfield_correct:

  [| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Getfield F D;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
  ==> G,phi |-JVM state' [ok]

lemma Putfield_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Putfield F D;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
  ==> G,phi |-JVM state' [ok]

lemma New_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = New X;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
  ==> G,phi |-JVM state' [ok]

lemmas

  (EX x. P x) = (EX a b. P (a, b))

lemma zip_map:

  length a = length b
  ==> zip (map f a) (map g b) = map (%(x, y). (f x, g y)) (zip a b)

lemma conf_ClassD:

  G,h |- Addr r ::<= Class C
  ==> EX obj. h r = Some obj & G |- the_Class (obj_ty obj) <=C C

lemma the_Class_widen:

  G |- the_Class (obj_ty obj) <=C D ==> G |- obj_ty obj <= Class D

lemma Invoke_correct:

  [| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Invoke C' mn pTs;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
  ==> G,phi |-JVM state' [ok]

lemma Invoke_special_correct:

  [| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Invoke_special C' mn pTs;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
  ==> G,phi |-JVM state' [ok]

lemmas

  map f (xs @ ys) = map f xs @ map f ys

lemma Return_correct_not_init:

  [| fst sig ~= init; wt_jvm_prog G phi;
     method (G, C) sig = Some (C, rT, maxs, maxl, ins, et); ins ! pc = Return;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemma Return_correct_init:

  [| fst sig = init; wt_jvm_prog G phi;
     method (G, C) sig = Some (C, rT, maxs, maxl, ins, et); ins ! pc = Return;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemma Return_correct:

  [| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Return;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemmas

  map f (xs @ ys) = map f xs @ map f ys

lemma Goto_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Goto branch;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemma Ifcmpeq_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Ifcmpeq branch;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemma Pop_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Pop;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemma Dup_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Dup;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemma Dup_x1_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Dup_x1;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemma Dup_x2_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Dup_x2;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemma Swap_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Swap;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemma IAdd_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = IAdd;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

lemma Throw_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = Throw;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
  ==> G,phi |-JVM state' [ok]

lemma Jsr_correct:

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None;
     ins ! pc = Jsr b |]
  ==> G,phi |-JVM state' [ok]

lemma

  [| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> finite (phi C sig ! pc)

lemma obj_ty_is_RefT:

  obj_ty x = PrimT T ==> False

lemma Ret_correct:

  [| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None;
     ins ! pc = Ret idx |]
  ==> G,phi |-JVM state' [ok]

lemma conf_ArrayD:

  G,hp |- s ::<= T.[]
  ==> s = Null |
      (EX l T' len en. s = Addr l & hp l = Some (Arr T' len en) & G |- T' <= T)

lemma ArrLength_correct:

  [| wf_prog wf_mb G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None;
     ins ! pc = ArrLength |]
  ==> G,phi |-JVM state' [ok]

lemma conf_IntegerD:

  G,hp |- v ::<= PrimT Integer ==> EX i. v = Intg i

lemma not_int:

  [| ¬ int len <= i; ¬ i < 0 |] ==> nat i < len

lemma ArrLoad_correct:

  [| wf_prog wf_mb G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None;
     ins ! pc = ArrLoad |]
  ==> G,phi |-JVM state' [ok]

lemma iconf_Init:

  (G,hp,ihp \<turnstile> v ::\<preceq>i Init T) =
  (G,hp |- v ::<= T & is_init hp ihp v)

lemma oconf_array_update:

  [| G,hp |- v ::<= T; G,hp |- Arr T l en [ok] |]
  ==> G,hp |- Arr T l (en(i|->v)) [ok]

lemma hconf_array_update:

  [| G |-h hp [ok]; hp oloc = Some (Arr T l en); G,hp |- v ::<= T |]
  ==> G |-h hp(oloc|->Arr T l (en(i|->v))) [ok]

lemma h_init_array_update:

  [| h_init G hp ihp; hp x = Some (Arr T l en); is_init hp ihp v |]
  ==> h_init G (hp(x|->Arr T l (en(i|->v)))) ihp

lemma

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = ArrStore;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
  ==> G,phi |-JVM state' [ok]

lemma oconf_blank_arr:

  G,hp |- blank_arr T (nat l) [ok]

lemma h_init_new_array:

  [| hp r = None; G |-h hp [ok]; h_init G hp ihp |]
  ==> h_init G (hp(r|->blank_arr T l)) (ihp(r := T'))

lemma

  [| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     ins ! pc = ArrNew T;
     wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
      pc;
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
     fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
  ==> G,phi |-JVM state' [ok]

theorem instr_correct:

  [| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
     Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
     G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
  ==> G,phi |-JVM state' [ok]

Main

lemma correct_state_impl_Some_method:

  G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok]
  ==> EX meth. method (G, C) sig = Some (C, meth)

lemma BV_correct_1:

  [| wt_jvm_prog G phi; G,phi |-JVM state [ok]; exec (G, state) = Some state' |]
  ==> G,phi |-JVM state' [ok]

lemma L0:

  [| xp = None; frs ~= [] |]
  ==> EX state'. exec (G, xp, hp, ihp, frs) = Some state'

lemma L1:

  [| wt_jvm_prog G phi; G,phi |-JVM (xp, hp, ihp, frs) [ok]; xp = None;
     frs ~= [] |]
  ==> EX state'.
         exec (G, xp, hp, ihp, frs) = Some state' & G,phi |-JVM state' [ok]

theorem BV_correct:

  [| wt_jvm_prog G phi; G |- s -jvm-> t; G,phi |-JVM s [ok] |]
  ==> G,phi |-JVM t [ok]

theorem BV_correct_implies_approx:

  [| wt_jvm_prog G phi;
     G |- s0 -jvm-> Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs);
     G,phi |-JVM s0 [ok] |]
  ==> EX ST LT z.
         ((ST, LT), z) : phi C sig ! pc &
         approx_stk G hp ihp stk ST & approx_loc G hp ihp loc LT

lemma

  wf_prog wf_mb G ==> G |-h start_heap G [ok]

lemma

  wf_prog wf_mb G ==> h_init G (start_heap G) start_iheap

lemma consistent_init_start:

  consistent_init [] (Null # replicate n arbitrary)
   ([], OK (Init (Class C)) # replicate n Err) hp

lemma

  [| wt_jvm_prog G Phi; is_class G C; method (G, C) (m, []) = Some (C, b);
     m ~= init |]
  ==> G,Phi |-JVM start_state G C m [ok]

theorem

  [| wt_jvm_prog G Phi; is_class G C; method (G, C) (m, []) = Some (C, b);
     m ~= init; G |- start_state G C m -jvm-> s |]
  ==> G,Phi |-JVM s [ok]