Theory BVSpecTypeSafe

(*  Title:      HOL/MicroJava/BV/BVSpecTypeSafe.thy
    ID:         $Id: BVSpecTypeSafe.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

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

theory BVSpecTypeSafe = BVConform:

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 conf_f_def wt_instr_def eff_def norm_eff_def app_def xcpt_app_def

lemmas widen_rules [intro] = conf_widen confT_widen confs_widens confTs_widen

  
section {* Exception Handling *}


text {*
  For the @{text Invoke} instruction the BV has checked all handlers
  that guard the current @{text pc}.
*}
lemma Invoke_handlers:
  "match_ex_table P C pc xt = Some (pc',d') ==> 
  ∃(f,t,D,h,d) ∈ set (relevant_entries P (Invoke n M) pc xt). 
   P \<turnstile> C \<preceq>* D ∧ pc ∈ {f..t(} ∧ pc' = h ∧ d' = d"
  by (induct xt) (auto simp add: relevant_entries_def matches_ex_entry_def 
                                 is_relevant_entry_def split: split_if_asm)


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
  heap address, and that the state before the exception occured
  conforms. 
*} term find_handler
lemma uncaught_xcpt_correct:
  assumes wt: "wf_jvm_progΦ P"
  assumes h:  "h xcp = Some obj"
  shows "!!f. P,Φ \<turnstile> (None, h, f#frs)\<surd> ==> P,Φ \<turnstile> (find_handler P xcp h frs) \<surd>" 
  (is "!!f. ?correct (None, h, f#frs) ==> ?correct (?find frs)")
(*<*)
proof (induct frs) 
  -- "the base
 case is trivial as it should be"
  show "?correct (?find [])" by (simp add: correct_state_def)
next
  -- "we will need both forms @{text wf_jvm_prog} and @{text wf_prog} later"
  from wt obtain mb where wf: "wf_prog mb P" by (simp add: wf_jvm_prog_phi_def)

  -- "the assumption for the cons case:"
  fix f f' frs' assume cr: "?correct (None, h, f#f'#frs')" 

  -- "the induction hypothesis:"
  assume IH: "!!f. ?correct (None, h, f#frs') ==> ?correct (?find frs')" 

  from cr have cr': "?correct (None, h, f'#frs')"
    by (fastsimp simp add: correct_state_def)
    
  obtain stk loc C M pc where [simp]: "f' = (stk,loc,C,M,pc)" by (cases f')

  from cr obtain Ts T mxs mxl0 ins xt where
    meth: "P \<turnstile> C sees M:Ts -> T = (mxs,mxl0,ins,xt) in C"
    by (simp add: correct_state_def, blast)

  hence [simp]: "ex_table_of P C M = xt" by simp

  show "?correct (?find (f'#frs'))" 
  proof (cases "match_ex_table P (cname_of h xcp) pc xt")
    case None with cr' IH [of f'] show ?thesis by fastsimp
  next
    fix pc_d
    assume "match_ex_table P (cname_of h xcp) pc xt = Some pc_d"
    then obtain pc' d' where 
      match: "match_ex_table P (cname_of h xcp) pc xt = Some (pc',d')"
      (is "?match (cname_of h xcp) = _")
      by (cases pc_d) auto 

    from wt meth cr' [simplified]
    have wti: "P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M" 
      by (fastsimp simp add: correct_state_def conf_f_def
                   dest: sees_method_fun
                   elim!: wt_jvm_prog_impl_wt_instr)
    from cr meth
    obtain n M' ST LT where
      ins: "ins!pc = Invoke n M'" (is "_ = ?i") and
      Φ: "Φ C M ! pc = Some (ST, LT)"
      by (fastsimp dest: sees_method_fun simp add: correct_state_def)
    
    from ins match obtain f t D where
      rel: "(f,t,D,pc',d') ∈ set (relevant_entries P (ins!pc) pc xt)" and
      D: "P \<turnstile> cname_of h xcp \<preceq>* D"
      by (fastsimp dest: Invoke_handlers)
    
    from rel have 
      "(pc', Some (Class D # drop (size ST - d') ST, LT)) ∈ set (xcpt_eff (ins!pc) P pc (ST,LT) xt)"
      (is "(_, Some (?ST',_)) ∈ _")
      by (force simp add: xcpt_eff_def image_def)      
    with wti Φ obtain 
      pc: "pc' < size ins" and
      "P \<turnstile> Some (?ST', LT) ≤' Φ C M ! pc'"
      by (clarsimp simp add: defs1) blast
    then obtain ST' LT' where
      Φ': "Φ C M ! pc' = Some (ST',LT')" and
      less: "P \<turnstile> (?ST', LT) ≤i (ST',LT')"
      by (auto simp add: sup_state_opt_any_Some)   
    
    from cr' Φ meth have "conf_f P h (ST, LT) ins f'"
      by (unfold correct_state_def) (fastsimp dest: sees_method_fun)
    hence loc: "P,h \<turnstile> loc [:≤\<top>] LT" and 
          stk: "P,h \<turnstile> stk [:≤] ST" by (unfold conf_f_def) auto
    hence [simp]: "size stk = size ST" by (simp add: list_all2_lengthD)

    let ?f = "(Addr xcp # drop (length stk - d') stk, loc, C, M, pc')"
    have "conf_f P h (ST',LT') ins ?f" 
    proof -
      from wf less loc have "P,h \<turnstile> loc [:≤\<top>] LT'" by simp blast
      moreover from D h have "P,h \<turnstile> Addr xcp :≤ Class D" 
              by (simp add: conf_def obj_ty_def split_beta)
      with less stk
      have "P,h \<turnstile> Addr xcp # drop (length stk - d') stk  [:≤] ST'" 
        by (auto intro!: list_all2_dropI)
      ultimately show ?thesis using pc by (simp add: conf_f_def) 
    qed

    with cr' match Φ' meth pc
    show ?thesis by (unfold correct_state_def) (fastsimp dest: sees_method_fun)
  qed
qed
(*>*)

text {*
  The requirement of lemma @{text uncaught_xcpt_correct} (that
  the exception is a valid reference on the heap) is always met
  for welltyped instructions and conformant states:
*}
lemma exec_instr_xcpt_h:
  "[|  fst (exec_instr (ins!pc) P h stk vars Cl M pc frs) = Some xcp;
       P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M;
       P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd> |]
  ==> ∃obj. h xcp = Some obj" 
  (is "[| ?xcpt; ?wt; ?correct |] ==> ?thesis")
(*<*)
proof -
  note [simp] = split_beta
  note [split] = split_if_asm option.split_asm 
  
  assume wt: ?wt ?correct
  hence pre: "preallocated h" by (simp add: correct_state_def hconf_def)

  assume xcpt: ?xcpt with pre show ?thesis 
  proof (cases "ins!pc")
    case Throw with xcpt wt pre show ?thesis 
      by (clarsimp iff: list_all2_Cons2 simp add: defs1) 
         (auto dest: non_npD simp: is_refT_def elim: preallocatedE)
  qed (auto elim: preallocatedE)
qed
(*>*)

lemma conf_sys_xcpt:
  "[|preallocated h; C ∈ sys_xcpts|] ==> P,h \<turnstile> Addr (addr_of_sys_xcpt C) :≤ Class C"
  by (auto elim: preallocatedE)

lemma match_ex_table_SomeD:
  "match_ex_table P C pc xt = Some (pc',d') ==> 
  ∃(f,t,D,h,d) ∈ set xt. matches_ex_entry P C pc (f,t,D,h,d) ∧ h = pc' ∧ d=d'"
  by (induct xt) (auto split: split_if_asm)


text {*
  Finally we can state that, whenever an exception occurs, the
  next state always conforms:
*}
lemma xcpt_correct:
  assumes wtp:  "wf_jvm_progΦ P"
  assumes meth: "P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C"
  assumes wt:   "P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M"
  assumes xp:   "fst (exec_instr (ins!pc) P h stk loc C M pc frs) = Some xcp"
  assumes s':   "Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs)"
  assumes correct: "P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd>"
  shows "P,Φ \<turnstile> σ'\<surd>"
(*<*)
proof -
  from wtp obtain wfmb where wf: "wf_prog wfmb P" 
    by (simp add: wf_jvm_prog_phi_def)                

  note conf_sys_xcpt [elim!]
  note xp' = meth s' xp

  note wtp
  moreover
  from xp wt correct
  obtain obj where h: "h xcp = Some obj" by (blast dest: exec_instr_xcpt_h)
  moreover note correct
  ultimately
  have "P,Φ \<turnstile> find_handler P xcp h frs \<surd>" by (rule uncaught_xcpt_correct)
  with xp'
  have "match_ex_table P (cname_of h xcp) pc xt = None ==> ?thesis" 
    (is "?m (cname_of h xcp) = _ ==> _" is "?match = _ ==> _")
    by (simp add: split_beta)
  moreover
  { fix pc_d assume "?match = Some pc_d"
    then obtain pc' d' where some_handler: "?match = Some (pc',d')" 
      by (cases pc_d) auto
    
    from correct meth
    obtain ST LT where
      h_ok:  "P \<turnstile> h \<surd>" and
      Φ_pc: "Φ C M ! pc = Some (ST, LT)" and
      frame:  "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and
      frames: "conf_fs P h Φ M (size Ts) T frs"
      by (unfold correct_state_def) (fastsimp dest: sees_method_fun)

    from h_ok have preh: "preallocated h" by (simp add: hconf_def)

    from frame obtain 
      stk: "P,h \<turnstile> stk [:≤] ST" and
      loc: "P,h \<turnstile> loc [:≤\<top>] LT" and
      pc:  "pc < size ins" 
      by (unfold conf_f_def) auto
    
    from stk have [simp]: "size stk = size ST" ..

    from wt Φ_pc have
      eff: "∀(pc', s')∈set (xcpt_eff (ins!pc) P pc (ST,LT) xt).
             pc' < size ins ∧ P \<turnstile> s' ≤' Φ C M!pc'"
      by (auto simp add: defs1)     
    
    let ?stk' = "Addr xcp # drop (length stk - d') stk"
    let ?f = "(?stk', loc, C, M, pc')"
    from some_handler xp' 
    have σ': "σ' = (None, h, ?f#frs)"
      by (simp add: split_beta)

    from some_handler obtain f t D where
      xt: "(f,t,D,pc',d') ∈ set xt" and
      "matches_ex_entry P (cname_of h xcp) pc (f,t,D,pc',d')"
      by (auto dest: match_ex_table_SomeD)

    hence match: "P \<turnstile> cname_of h xcp \<preceq>* D"  "pc ∈ {f..t(}"
      by (auto simp: matches_ex_entry_def)

    from xp obtain
      "(f,t,D,pc',d') ∈ set (relevant_entries P (ins!pc) pc xt)" and
      conf: "P,h \<turnstile> Addr xcp :≤ Class D"
    proof (cases "ins!pc")
      case Return
      with xp have False by (auto simp: split_beta split: split_if_asm)
      thus ?thesis ..
    next
      case New with xp
      have [simp]: "xcp = addr_of_sys_xcpt OutOfMemory" by simp
      with New match preh have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
        by (simp add: is_relevant_entry_def)
      with match preh xt
      show ?thesis by (fastsimp simp add: relevant_entries_def intro: that)
    next
      case Getfield with xp
      have [simp]: "xcp = addr_of_sys_xcpt NullPointer" 
        by (simp add: split_beta split: split_if_asm)
      with Getfield match preh have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
        by (simp add: is_relevant_entry_def)
      with match preh xt
      show ?thesis by (fastsimp simp add: relevant_entries_def intro: that)
    next
      case Putfield with xp
      have [simp]: "xcp = addr_of_sys_xcpt NullPointer" 
        by (simp add: split_beta split: split_if_asm)
      with Putfield match preh have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
        by (simp add: is_relevant_entry_def)
      with match preh xt
      show ?thesis by (fastsimp simp add: relevant_entries_def intro: that)
    next
      case Checkcast with xp
      have [simp]: "xcp = addr_of_sys_xcpt ClassCast" 
        by (simp add: split_beta split: split_if_asm)
      with Checkcast match preh have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
        by (simp add: is_relevant_entry_def)
      with match preh xt
      show ?thesis by (fastsimp simp add: relevant_entries_def intro: that)
    next
      case Invoke with xp match 
      have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
        by (simp add: is_relevant_entry_def)
      moreover
      from xp wt correct obtain obj where xcp: "h xcp = Some obj" 
        by (blast dest: exec_instr_xcpt_h)
      ultimately
      show ?thesis using xt match
        by (auto simp add: relevant_entries_def conf_def split_beta intro: that)
    next
      case Throw with xp match preh 
      have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
        by (simp add: is_relevant_entry_def)
      moreover
      from xp wt correct obtain obj where xcp: "h xcp = Some obj" 
        by (blast dest: exec_instr_xcpt_h)
      ultimately
      show ?thesis using xt match
        by (auto simp add: relevant_entries_def conf_def split_beta intro: that)
    qed auto

    with eff obtain ST' LT' where
      Φ_pc': "Φ C M ! pc' = Some (ST', LT')" and
      pc':   "pc' < size ins" and
      less:  "P \<turnstile> (Class D # drop (size ST - d') ST, LT) ≤i (ST', LT')"
      by (fastsimp simp add: xcpt_eff_def sup_state_opt_any_Some)

    with conf loc stk have "conf_f P h (ST',LT') ins ?f" 
      by (auto simp add: defs1 intro: list_all2_dropI)
    with meth h_ok frames Φ_pc' σ'
    have ?thesis by (unfold correct_state_def) (fastsimp dest: sees_method_fun)
  }
  ultimately
  show ?thesis by (cases "?match") blast+ 
qed
(*>*)


section {* Single Instructions *}

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

declare defs1 [simp]

lemma Invoke_correct: 
  assumes wtprog: "wf_jvm_progΦ P"
  assumes meth_C: "P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C"
  assumes ins:    "ins ! pc = Invoke M' n"
  assumes wti:    "P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M"
  assumes σ': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs)"
  assumes approx: "P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd>"
  assumes no_xcp: "fst (exec_instr (ins!pc) P h stk loc C M pc frs) = None"
  shows "P,Φ \<turnstile> σ'\<surd>" 
(*<*)
proof -
  note split_paired_Ex [simp del]
  
  from wtprog obtain wfmb where wfprog: "wf_prog wfmb P" 
    by (simp add: wf_jvm_prog_phi_def)
      
  from ins meth_C approx obtain ST LT where
    heap_ok: "P\<turnstile> h\<surd>" and
    Φ_pc:    "Φ C M!pc = Some (ST,LT)" and
    frame:   "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and
    frames:  "conf_fs P h Φ M (size Ts) T frs"
    by (fastsimp dest: sees_method_fun)

  from ins wti Φ_pc
  have n: "n < size ST" by simp
  
  { assume "stk!n = Null"
    with ins no_xcp have False by (simp add: split_beta)
    hence ?thesis ..
  } 
  moreover
  { assume "ST!n = NT"
    moreover 
    from frame have "P,h \<turnstile> stk [:≤] ST" by simp
    with n have "P,h \<turnstile> stk!n :≤ ST!n" by (simp add: list_all2_conv_all_nth)
    ultimately 
    have "stk!n = Null" by simp
    with ins no_xcp have False by (simp add: split_beta)
    hence ?thesis ..
  } 
  moreover {
    assume NT: "ST!n ≠ NT" and Null: "stk!n ≠ Null"
    
    from NT ins wti Φ_pc obtain D D' Ts T m ST' LT' where
      D:   "ST!n = Class D" and
      pc': "pc+1 < size ins" and
      m_D: "P \<turnstile> D sees M': Ts->T = m in D'" and
      Ts:  "P \<turnstile> rev (take n ST) [≤] Ts" and
      Φ':  "Φ C M ! (pc+1) = Some (ST', LT')" and
      LT': "P \<turnstile> LT [≤\<top>] LT'" and
      ST': "P \<turnstile> (T # drop (n+1) ST) [≤] ST'"
      by (clarsimp simp add: sup_state_opt_any_Some) blast

    from frame obtain 
    stk: "P,h \<turnstile> stk [:≤] ST" and
    loc: "P,h \<turnstile> loc [:≤\<top>] LT" by simp
    
    from n stk D have "P,h \<turnstile> stk!n :≤ Class D"
      by (auto simp add: list_all2_conv_all_nth)
    with Null obtain a C' fs where
      Addr:   "stk!n = Addr a" and
      obj:    "h a = Some (C',fs)" and
      C'subD: "P \<turnstile> C' \<preceq>* D"
      by (fastsimp dest!: conf_ClassD) 

    with wfprog m_D
    obtain Ts' T' m' D'' mxs' mxl' ins' xt' where
      m_C': "P \<turnstile> C' sees M': Ts'->T' = (mxs',mxl',ins',xt') in D''" and
      T':   "P \<turnstile> T' ≤ T" and
      Ts':  "P \<turnstile> Ts [≤] Ts'" 
      by (auto dest: sees_method_mono)

    let ?loc' = "Addr a # rev (take n stk) @ replicate mxl' arbitrary"
    let ?f' = "([], ?loc', D'', M', 0)"
    let ?f  = "(stk, loc, C, M, pc)"

    from Addr obj m_C' ins σ' meth_C
    have s': "σ' = (None, h, ?f' # ?f # frs)" by simp

    from Ts n have [simp]: "size Ts = n" 
      by (auto dest: list_all2_lengthD simp: min_def)
    with Ts' have [simp]: "size Ts' = n" 
      by (auto dest: list_all2_lengthD)

    from m_C' wfprog
    obtain mD'': "P \<turnstile> D'' sees M':Ts'->T'=(mxs',mxl',ins',xt') in D''"
      by (fast dest: sees_method_idemp)
    moreover 
    with wtprog 
    obtain start: "wt_start P D'' Ts' mxl' (Φ D'' M')" and ins': "ins' ≠ []"
      by (auto dest: wt_jvm_prog_impl_wt_start)    
    then obtain LT0 where LT0: "Φ D'' M' ! 0 = Some ([], LT0)"
      by (clarsimp simp add: wt_start_def defs1 sup_state_opt_any_Some)
    moreover
    have "conf_f P h ([], LT0) ins' ?f'"
    proof -
      let ?LT = "OK (Class D'') # (map OK Ts') @ (replicate mxl' Err)"

      from stk have "P,h \<turnstile> take n stk [:≤] take n ST" ..
      hence "P,h \<turnstile> rev (take n stk) [:≤] rev (take n ST)" by simp
      also note Ts also note Ts' finally
      have "P,h \<turnstile> rev (take n stk) [:≤\<top>] map OK Ts'" by simp 
      also
      have "P,h \<turnstile> replicate mxl' arbitrary [:≤\<top>] replicate mxl' Err" 
        by simp
      also from m_C' have "P \<turnstile> C' \<preceq>* D''" by (rule sees_method_decl_above)
      with obj have "P,h \<turnstile> Addr a :≤ Class D''" by (simp add: conf_def)
      ultimately
      have "P,h \<turnstile> ?loc' [:≤\<top>] ?LT" by simp
      also from start LT0 have "P \<turnstile> … [≤\<top>] LT0" by (simp add: wt_start_def)
      finally have "P,h \<turnstile> ?loc' [:≤\<top>] LT0" .
      thus ?thesis using ins' by simp
    qed
    ultimately
    have ?thesis using s' Φ_pc approx meth_C m_D T' ins D 
      by (fastsimp dest: sees_method_fun [of _ C])
  }
  ultimately show ?thesis by blast
qed
(*>*)

declare list_all2_Cons2 [iff]

lemma Return_correct:
  assumes wt_prog: "wf_jvm_progΦ P"
  assumes meth: "P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C"
  assumes ins: "ins ! pc = Return"
  assumes wt: "P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M"
  assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs)"
  assumes correct: "P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd>"

  shows "P,Φ \<turnstile> σ'\<surd>"
(*<*)
proof -
  from wt_prog 
  obtain wfmb where wf: "wf_prog wfmb P" by (simp add: wf_jvm_prog_phi_def)

  from meth ins s'
  have "frs = [] ==> ?thesis" by (simp add: correct_state_def)
  moreover
  { fix f frs' assume frs': "frs = f#frs'"
    moreover obtain stk' loc' C' M' pc' where 
      f: "f = (stk',loc',C',M',pc')" by (cases f)
    moreover note meth ins s'
    ultimately
    have σ':
      "σ' = (None,h,(hd stk#(drop (1+size Ts) stk'),loc',C',M',pc'+1)#frs')"
      (is "σ' = (None,h,?f'#frs')")
      by simp
    
    from correct meth
    obtain ST LT where
      h_ok:   "P \<turnstile> h \<surd>" and
      Φ_pc: "Φ C M ! pc = Some (ST, LT)" and
      frame:  "conf_f P h (ST, LT) ins (stk,loc,C,M,pc)" and
      frames: "conf_fs P h Φ M (size Ts) T frs"
      by (auto dest: sees_method_fun simp add: correct_state_def)

    from Φ_pc ins wt
    obtain U ST0 where "ST = U # ST0" "P \<turnstile> U ≤ T"
      by (simp add: wt_instr_def app_def) blast    
    with wf frame 
    have hd_stk: "P,h \<turnstile> hd stk :≤ T" by (auto simp add: conf_f_def)

    from f frs' frames
    obtain ST' LT' Ts'' T'' mxs' mxl0' ins' xt' D Ts' T' m D' where
      Φ': "Φ C' M' ! pc' = Some (ST', LT')" and
      meth_C':  "P \<turnstile> C' sees M':Ts''->T''=(mxs',mxl0',ins',xt') in C'" and
      ins': "ins' ! pc' = Invoke M (size Ts)" and
      D: "ST' ! (size Ts) = Class D" and
      meth_D: "P \<turnstile> D sees M: Ts'->T' = m in D'" and
      T': "P \<turnstile> T ≤ T'" and
      frame':   "conf_f P h (ST',LT') ins' f" and
      conf_fs:  "conf_fs P h Φ M' (size Ts'') T'' frs'"
      by clarsimp blast

    from f frame' obtain
      stk': "P,h \<turnstile> stk' [:≤] ST'" and
      loc': "P,h \<turnstile> loc' [:≤\<top>] LT'" and
      pc':  "pc' < size ins'"
      by (simp add: conf_f_def)
    
    from wt_prog meth_C' pc'  
    have "P,T'',mxs',size ins',xt' \<turnstile> ins'!pc',pc' :: Φ C' M'"
      by (rule wt_jvm_prog_impl_wt_instr)
    with ins' Φ' D meth_D
    obtain aTs ST'' LT'' where
      Φ_suc:   "Φ C' M' ! Suc pc' = Some (ST'', LT'')" and
      less:    "P \<turnstile> (T' # drop (size Ts+1) ST', LT') ≤i (ST'', LT'')" and
      suc_pc': "Suc pc' < size ins'" 
      by (clarsimp simp add: sup_state_opt_any_Some) blast

    from hd_stk T' have hd_stk': "P,h \<turnstile> hd stk :≤ T'"  ..
        
    have frame'':
      "conf_f P h (ST'',LT'') ins' ?f'" 
    proof -
      from stk'
      have "P,h \<turnstile> drop (1+size Ts) stk' [:≤] drop (1+size Ts) ST'" ..
      moreover
      with hd_stk' less
      have "P,h \<turnstile> hd stk # drop (1+size Ts) stk' [:≤] ST''" by auto
      moreover
      from wf loc' less have "P,h \<turnstile> loc' [:≤\<top>] LT''" by auto
      moreover note suc_pc' 
      ultimately show ?thesis by (simp add: conf_f_def)
    qed

    with σ' frs' f meth h_ok hd_stk Φ_suc frames meth_C' Φ'  
    have ?thesis by (fastsimp dest: sees_method_fun [of _ C'])
  }
  ultimately
  show ?thesis by (cases frs) blast+
qed
(*>*)

declare sup_state_opt_any_Some [iff]
declare not_Err_eq [iff]

lemma Load_correct:
"[| wf_prog wt P;
    P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C; 
    ins!pc = Load idx; 
    P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M; 
    Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs); 
    P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd> |]
==> P,Φ \<turnstile> σ'\<surd>"
  by (fastsimp dest: sees_method_fun [of _ C] elim!: confTs_confT_sup)

lemma Store_correct:
"[| wf_prog wt P;
  P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C;
  ins!pc = Store idx;
  P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M;
  Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs);
  P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd> |]
==> P,Φ \<turnstile> σ'\<surd>"
(*<*)
  apply clarsimp 
  apply (drule (1) sees_method_fun)
  apply clarsimp
  apply (blast intro!: list_all2_update_cong2)
  done
(*>*)


lemma Push_correct:
"[| wf_prog wt P;
    P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C; 
    ins!pc = Push v;
    P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M; 
    Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs);
    P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd> |]
==> P,Φ \<turnstile> σ'\<surd>" 
(*<*)
  apply clarsimp 
  apply (drule (1) sees_method_fun)
  apply clarsimp
  apply (blast dest: typeof_lit_conf)
  done
(*>*)


lemma Cast_conf2:
  "[| wf_prog ok P; P,h \<turnstile> v :≤ T; is_refT T; cast_ok P C h v; 
     P \<turnstile> Class C ≤ T'; is_class P C|] 
  ==> P,h \<turnstile> v :≤ T'"
(*<*)
  apply (unfold cast_ok_def is_refT_def)
  apply (frule Class_widen)
  apply (elim exE disjE) 
     apply simp
    apply simp
   apply simp  
  apply (clarsimp simp add: conf_def obj_ty_def)
  apply (cases v)
  apply (auto intro: rtrancl_trans)
  done
(*>*)


lemma Checkcast_correct:
"[| wf_jvm_progΦ P;
    P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C; 
    ins!pc = Checkcast D; 
    P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M; 
    Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ; 
    P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd>;
    fst (exec_instr (ins!pc) P h stk loc C M pc frs) = None |] 
==> P,Φ \<turnstile> σ'\<surd>"
(*<*)
  apply (clarsimp simp add: wf_jvm_prog_phi_def split: split_if_asm)
  apply (drule (1) sees_method_fun)
  apply (blast intro: Cast_conf2)
  done
(*>*)

declare split_paired_All [simp del]

lemmas widens_Cons [iff] = rel_list_all2_Cons1 [of "widen P", standard]

lemma Getfield_correct:
  assumes wf: "wf_prog wt P"
  assumes mC: "P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C"
  assumes i:  "ins!pc = Getfield F D"
  assumes wt: "P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M"
  assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs)"
  assumes cf: "P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd>"
  assumes xc: "fst (exec_instr (ins!pc) P h stk loc C M pc frs) = None"

  shows "P,Φ \<turnstile> σ'\<surd>"
(*<*)
proof -
  from mC cf obtain ST LT where    
    "h\<surd>": "P \<turnstile> h \<surd>" and
    Φ: "Φ C M ! pc = Some (ST,LT)" and
    stk: "P,h \<turnstile> stk [:≤] ST" and loc: "P,h \<turnstile> loc [:≤\<top>] LT" and
    pc: "pc < size ins" and 
    fs: "conf_fs P h Φ M (size Ts) T frs"
    by (fastsimp dest: sees_method_fun)
       
  from i Φ wt obtain oT ST'' vT ST' LT' vT' where 
    oT: "P \<turnstile> oT ≤ Class D" and
    ST: "ST = oT # ST''" and
    F:  "P \<turnstile> D sees F:vT in D" and
    pc': "pc+1 < size ins"  and
    Φ': "Φ C M ! (pc+1) = Some (vT'#ST', LT')" and
    ST': "P \<turnstile> ST'' [≤] ST'" and LT': "P \<turnstile> LT [≤\<top>] LT'" and  
    vT': "P \<turnstile> vT ≤ vT'"
    by fastsimp                       

  from stk ST obtain ref stk' where 
    stk': "stk = ref#stk'" and
    ref:  "P,h \<turnstile> ref :≤ oT" and
    ST'': "P,h \<turnstile> stk' [:≤] ST''"
    by auto

  from stk' i mC s' xc have "ref ≠ Null"
    by (simp add: split_beta split:split_if_asm)
  moreover from ref oT have "P,h \<turnstile> ref :≤ Class D" ..
  ultimately obtain a D' fs where 
    a: "ref = Addr a" and h: "h a = Some (D', fs)" and D': "P \<turnstile> D' \<preceq>* D"
    by (blast dest: non_npD)

  from D' F have has_field: "P \<turnstile> D' has F:vT in D"      
    by (blast intro: has_field_mono has_visible_field)
  moreover from "h\<surd>" h have "P,h \<turnstile> (D', fs) \<surd>" by (rule hconfD)
  ultimately obtain v where v: "fs (F, D) = Some v" "P,h \<turnstile> v :≤ vT"
    by (clarsimp simp add: oconf_def fconf_def has_field_def)        
       (blast dest: has_fields_fun)

  from a h i mC s' stk' v
  have "σ' = (None, h, (v#stk',loc,C,M,pc+1)#frs)" by simp
  moreover
  from ST'' ST' have "P,h \<turnstile> stk' [:≤] ST'" ..
  moreover
  from v vT' have "P,h \<turnstile> v :≤ vT'" by blast
  moreover
  from loc LT' have "P,h \<turnstile> loc [:≤\<top>] LT'" ..
  moreover
  note "h\<surd>" mC Φ' pc' v fs
  ultimately
  show "P,Φ \<turnstile> σ' \<surd>" by fastsimp
qed
(*>*)

lemma Putfield_correct:
  assumes wf: "wf_prog wt P"
  assumes mC: "P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C"
  assumes i:  "ins!pc = Putfield F D"
  assumes wt: "P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M"
  assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs)"
  assumes cf: "P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd>"
  assumes xc: "fst (exec_instr (ins!pc) P h stk loc C M pc frs) = None"

  shows "P,Φ \<turnstile> σ'\<surd>"
(*<*)
proof -
  from mC cf obtain ST LT where    
    "h\<surd>": "P \<turnstile> h \<surd>" and    
    Φ: "Φ C M ! pc = Some (ST,LT)" and
    stk: "P,h \<turnstile> stk [:≤] ST" and loc: "P,h \<turnstile> loc [:≤\<top>] LT" and
    pc: "pc < size ins" and 
    fs: "conf_fs P h Φ M (size Ts) T frs"
    by (fastsimp dest: sees_method_fun)
  
  from i Φ wt obtain vT vT' oT ST'' ST' LT' where 
    ST: "ST = vT # oT # ST''" and
    field: "P \<turnstile> D sees F:vT' in D" and
    oT: "P \<turnstile> oT ≤ Class D" and vT: "P \<turnstile> vT ≤ vT'" and
    pc': "pc+1 < size ins" and 
    Φ': "Φ C M!(pc+1) = Some (ST',LT')" and
    ST': "P \<turnstile> ST'' [≤] ST'" and LT': "P \<turnstile> LT [≤\<top>] LT'"
    by clarsimp blast

  from stk ST obtain v ref stk' where 
    stk': "stk = v#ref#stk'" and
    v:    "P,h \<turnstile> v :≤ vT" and 
    ref:  "P,h \<turnstile> ref :≤ oT" and
    ST'': "P,h \<turnstile> stk' [:≤] ST''"
    by auto

  from stk' i mC s' xc have "ref ≠ Null" by (auto simp add: split_beta)
  moreover from ref oT have "P,h \<turnstile> ref :≤ Class D" ..
  ultimately obtain a D' fs where 
    a: "ref = Addr a" and h: "h a = Some (D', fs)" and D': "P \<turnstile> D' \<preceq>* D"
    by (blast dest: non_npD)

  from v vT have vT': "P,h \<turnstile> v :≤ vT'" ..

  from field D' have has_field: "P \<turnstile> D' has F:vT' in D"
    by (blast intro: has_field_mono has_visible_field)

  let ?h' = "h(a\<mapsto>(D', fs((F, D)\<mapsto>v)))" and ?f' = "(stk',loc,C,M,pc+1)"
  from h have hext: "h \<unlhd> ?h'" by (rule hext_upd_obj) 

  from a h i mC s' stk' 
  have "σ' = (None, ?h', ?f'#frs)" by simp
  moreover
  from "h\<surd>" h have "P,h \<turnstile> (D',fs)\<surd>" by (rule hconfD) 
  with has_field vT' have "P,h \<turnstile> (D',fs((F, D)\<mapsto>v))\<surd>" ..
  with "h\<surd>" have "P \<turnstile> ?h'\<surd>" by - (rule hconf_upd_obj) 
  moreover
  from ST'' ST' have "P,h \<turnstile> stk' [:≤] ST'" ..
  with hext have "P,?h' \<turnstile> stk' [:≤] ST'" by - (rule confs_hext)
  moreover
  from loc LT' have "P,h \<turnstile> loc [:≤\<top>] LT'" ..
  with hext have "P,?h' \<turnstile> loc [:≤\<top>] LT'" by - (rule confTs_hext)
  moreover
  from fs hext
  have "conf_fs P ?h' Φ M (size Ts) T frs" by (rule conf_fs_hext)
  moreover
  note mC Φ' pc' 
  ultimately
  show "P,Φ \<turnstile> σ' \<surd>" by fastsimp
qed
(*>*)
  
(* FIXME: move *)
lemma has_fields_b_fields: 
  "P \<turnstile> C has_fields FDTs ==> fields P C = FDTs"
(*<*)
  apply (unfold fields_def)                    
  apply (blast intro: the_equality has_fields_fun)
  done                                                
(*>*)
  
(* FIXME: move *)
lemma oconf_blank [intro, simp]:
    "[|is_class P C; wf_prog wt P|] ==> P,h \<turnstile> blank P C \<surd>"
(*<*)
  apply (unfold blank_def oconf_def)    
  apply (simp add: has_fields_b_fields fconf_init_fields wf_Fields_Ex
                   cong: conj_cong)                                   
  done                                                                    
(*>*)

lemma obj_ty_blank [iff]: "obj_ty (blank P C) = Class C"
  by (simp add: blank_def)

lemma New_correct:
  assumes wf:   "wf_prog wt P"
  assumes meth: "P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C"
  assumes ins:  "ins!pc = New X"
  assumes wt:   "P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M"
  assumes exec: "Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs)"
  assumes conf: "P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd>"
  assumes no_x: "fst (exec_instr (ins!pc) P h stk loc C M pc frs) = None"
  shows "P,Φ \<turnstile> σ'\<surd>"
(*<*)
proof - 
  from ins conf meth
  obtain ST LT where
    heap_ok: "P\<turnstile> h\<surd>" and
    Φ_pc:    "Φ C M!pc = Some (ST,LT)" and
    frame:   "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and
    frames:  "conf_fs P h Φ M (size Ts) T frs"
    by (auto dest: sees_method_fun)

  from Φ_pc ins wt
  obtain ST' LT' where
    is_class_X: "is_class P X" and
    mxs:       "size ST < mxs" and
    suc_pc:     "pc+1 < size ins" and
    Φ_suc:      "Φ C M!(pc+1) = Some (ST', LT')" and
    less:       "P \<turnstile> (Class X # ST, LT) ≤i (ST', LT')"
    by auto

  from ins no_x obtain oref where new_Addr: "new_Addr h = Some oref" by auto
  hence h: "h oref = None" by (rule new_Addr_SomeD) 
  
  with exec ins meth new_Addr have σ':
    "σ' = (None, h(oref \<mapsto> blank P X), (Addr oref#stk,loc,C,M,pc+1)#frs)"
    (is "σ' = (None, ?h', ?f # frs)")
    by simp    
  moreover
  from wf h heap_ok is_class_X have h': "P \<turnstile> ?h' \<surd>"
    by (auto intro: hconf_new)
  moreover
  from h frame less suc_pc wf
  have "conf_f P ?h' (ST', LT') ins ?f"
    apply (clarsimp simp add: fun_upd_apply conf_def blank_def split_beta)
    apply (auto intro: confs_hext confTs_hext)
    done      
  moreover
  from h have "h \<unlhd> ?h'" by simp
  with frames have "conf_fs P ?h' Φ M (size Ts) T frs" by (rule conf_fs_hext)
  ultimately
  show ?thesis using meth Φ_suc by fastsimp 
qed
(*>*)


lemma Goto_correct:
"[| wf_prog wt P; 
  P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C; 
  ins ! pc = Goto branch; 
  P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M; 
  Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ; 
  P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd> |] 
==> P,Φ \<turnstile> σ'\<surd>"
(*<*)
apply clarsimp 
apply (drule (1) sees_method_fun)
apply fastsimp
done
(*>*)


lemma IfFalse_correct:
"[| wf_prog wt P; 
  P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C; 
  ins ! pc = IfFalse branch; 
  P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M; 
  Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ; 
  P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd> |] 
==> P,Φ \<turnstile> σ'\<surd>"
(*<*)
apply clarsimp
apply (drule (1) sees_method_fun)
apply fastsimp
done
(*>*)

lemma CmpEq_correct:
"[| wf_prog wt P; 
  P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C; 
  ins ! pc = CmpEq;
  P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M; 
  Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ; 
  P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd> |] 
==> P,Φ \<turnstile> σ'\<surd>"
(*<*)
apply clarsimp
apply (drule (1) sees_method_fun)
apply fastsimp
done
(*>*)

lemma Pop_correct:
"[| wf_prog wt P; 
  P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C; 
  ins ! pc = Pop;
  P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M; 
  Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ; 
  P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd> |] 
==> P,Φ \<turnstile> σ'\<surd>"
(*<*)
apply clarsimp
apply (drule (1) sees_method_fun)
apply fastsimp
done
(*>*)


lemma IAdd_correct:
"[| wf_prog wt P; 
  P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C; 
  ins ! pc = IAdd; 
  P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M; 
  Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ; 
  P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd> |] 
==> P,Φ \<turnstile> σ'\<surd>"
(*<*)
apply (clarsimp simp add: conf_def)
apply (drule (1) sees_method_fun)
apply fastsimp
done
(*>*)


lemma Throw_correct:
"[| wf_prog wt P; 
  P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C; 
  ins ! pc = Throw; 
  Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ; 
  P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd>;
  fst (exec_instr (ins!pc) P h stk loc C M pc frs) = None |] 
==> P,Φ \<turnstile> σ'\<surd>"
  by simp


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:
"[| wf_jvm_progΦ P;
  P \<turnstile> C sees M:Ts->T=(mxs,mxl0,ins,xt) in C;
  Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs); 
  P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd> |] 
==> P,Φ \<turnstile> σ'\<surd>"
(*<*)
apply (subgoal_tac "P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: Φ C M")
 prefer 2
 apply (erule wt_jvm_prog_impl_wt_instr, assumption)
 apply clarsimp
 apply (drule (1) sees_method_fun)
 apply simp                                 
apply (cases "fst (exec_instr (ins!pc) P h stk loc C M pc frs)")
 prefer 2
 apply (erule xcpt_correct, assumption+) 
apply (frule wt_jvm_progD, erule exE)
apply (cases "ins!pc")
apply (rule Load_correct, assumption+)
apply (rule Store_correct, assumption+)
apply (rule Push_correct, assumption+)
apply (rule New_correct, assumption+)
apply (rule Getfield_correct, assumption+)
apply (rule Putfield_correct, assumption+)
apply (rule Checkcast_correct, assumption+)
apply (rule Invoke_correct, assumption+)
apply (rule Return_correct, assumption+)
apply (rule Pop_correct, assumption+)
apply (rule IAdd_correct, assumption+)
apply (rule Goto_correct, assumption+)
apply (rule CmpEq_correct, assumption+)
apply (rule IfFalse_correct, assumption+)
apply (rule Throw_correct, assumption+)
done
(*>*)

section {* Main *}

lemma correct_state_impl_Some_method:
  "P,Φ \<turnstile> (None, h, (stk,loc,C,M,pc)#frs)\<surd> 
  ==> ∃m Ts T. P \<turnstile> C sees M:Ts->T = m in C"
  by fastsimp

lemma BV_correct_1 [rule_format]:
"!!σ. [| wf_jvm_progΦ P; P,Φ \<turnstile> σ\<surd>|] ==> P \<turnstile> σ -jvm->1 σ' --> P,Φ \<turnstile> σ'\<surd>"
(*<*)
apply (simp only: split_tupled_all exec_1_iff)
apply (rename_tac xp h 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 clarify
 apply (rule instr_correct)
 apply assumption+
 apply (rule sym)
 apply assumption+
apply (case_tac frs)
apply simp_all
done
(*>*)


theorem progress:
  "[| xp=None; frs≠[] |] ==> ∃σ'. P \<turnstile> (xp,h,frs) -jvm->1 σ'"
  by (clarsimp simp add: exec_1_iff neq_Nil_conv split_beta
               simp del: split_paired_Ex)

lemma progress_conform:
  "[|wf_jvm_progΦ P; P,Φ \<turnstile> (xp,h,frs)\<surd>; xp=None; frs≠[]|] 
  ==> ∃σ'. P \<turnstile> (xp,h,frs) -jvm->1 σ' ∧ P,Φ \<turnstile> σ'\<surd>"
(*<*)
apply (drule progress)
apply assumption
apply (fast intro: BV_correct_1)
done
(*>*)

theorem BV_correct [rule_format]:
"[| wf_jvm_progΦ P; P \<turnstile> σ -jvm-> σ' |] ==> P,Φ \<turnstile> σ\<surd> --> P,Φ \<turnstile> σ'\<surd>"
(*<*)
apply (simp only: exec_all_def1)
apply (erule rtrancl_induct)
 apply simp
apply clarify
apply (erule (2) BV_correct_1)
done
(*>*)

lemma hconf_start:   
  assumes wf: "wf_prog wf_mb P"
  shows "P \<turnstile> (start_heap P) \<surd>"
(*<*)
  apply (unfold hconf_def)
  apply (simp add: preallocated_start)
  apply (clarify)
  apply (drule sym)
  apply (unfold start_heap_def)
  apply (insert wf)
  apply (auto simp add: fun_upd_apply is_class_xcpt split: split_if_asm)
  done
(*>*)
    
lemma BV_correct_initial: 
  shows "[| wf_jvm_progΦ P; P \<turnstile> C sees M:[]->T = m in C |]
  ==> P,Φ \<turnstile> start_state P C M \<surd>"
(*<*)
  apply (cases m)                            
  apply (unfold  start_state_def)
  apply (unfold correct_state_def)
  apply (simp del: defs1)
  apply (rule conjI)
   apply (simp add: wf_jvm_prog_phi_def hconf_start) 
  apply (drule wt_jvm_prog_impl_wt_start, assumption+)
  apply (unfold conf_f_def wt_start_def)
  apply fastsimp
  done
(*>*)

theorem typesafe:
  assumes welltyped:   "wf_jvm_progΦ P"
  assumes main_method: "P \<turnstile> C sees M:[]->T = m in C"
  shows "P \<turnstile> start_state P C M -jvm-> σ  ==>  P,Φ \<turnstile> σ \<surd>"
(*<*)
proof -
  from welltyped main_method
  have "P,Φ \<turnstile> start_state P C M \<surd>" by (rule BV_correct_initial)
  moreover
  assume "P \<turnstile> start_state P C M -jvm-> σ"
  ultimately  
  show "P,Φ \<turnstile> σ \<surd>" using welltyped by - (rule BV_correct)
qed
(*>*)
  
end