src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
changeset 59682 d662d096f72b
parent 58886 8a6cac7c7247
child 61361 8b5f00202e1a
     1.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Mar 10 23:04:40 2015 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Mar 12 14:58:32 2015 +0100
     1.3 @@ -811,7 +811,7 @@
     1.4  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
     1.5  proof -
     1.6    assume wtprog: "wt_jvm_prog G phi"
     1.7 -  assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
     1.8 +  assume "method": "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
     1.9    assume ins:    "ins ! pc = Invoke C' mn pTs"
    1.10    assume wti:    "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
    1.11    assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
    1.12 @@ -823,7 +823,7 @@
    1.13      wfprog: "wf_prog wfmb G" 
    1.14      by (simp add: wt_jvm_prog_def)
    1.15        
    1.16 -  from ins method approx
    1.17 +  from ins "method" approx
    1.18    obtain s where
    1.19      heap_ok: "G\<turnstile>h hp\<surd>" and
    1.20      prealloc:"preallocated hp" and
    1.21 @@ -880,7 +880,7 @@
    1.22    from stk' l_o l
    1.23    have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp
    1.24  
    1.25 -  with state' method ins no_xcp oX_conf
    1.26 +  with state' "method" ins no_xcp oX_conf
    1.27    obtain ref where oX_Addr: "oX = Addr ref"
    1.28      by (auto simp add: raise_system_xcpt_def dest: conf_RefTD)
    1.29  
    1.30 @@ -922,7 +922,7 @@
    1.31        
    1.32    from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def)
    1.33  
    1.34 -  with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp
    1.35 +  with oX_Addr oX_pos state' "method" ins stk' l_o l loc obj_ty mD no_xcp
    1.36    have state'_val:
    1.37      "state' =
    1.38       Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' undefined, 
    1.39 @@ -972,7 +972,7 @@
    1.40      show ?thesis by (simp add: correct_frame_def)
    1.41    qed
    1.42  
    1.43 -  from state'_val heap_ok mD'' ins method phi_pc s X' l mX
    1.44 +  from state'_val heap_ok mD'' ins "method" phi_pc s X' l mX
    1.45         frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc and l
    1.46    show ?thesis
    1.47      apply (simp add: correct_state_def)