src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10042 7164dc0d24d8
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
     1 (*  Title:      HOL/MicroJava/BV/BVSpecTypeSafe.thy
     2     ID:         $Id$
     3     Author:     Cornelia Pusch
     4     Copyright   1999 Technische Universitaet Muenchen
     5 
     6 Proof that the specification of the bytecode verifier only admits type safe
     7 programs.
     8 *)
     9 
    10 header "Type Safety Proof"
    11 
    12 theory BVSpecTypeSafe = Correct:
    13 
    14 lemmas defs1 = sup_state_def correct_state_def correct_frame_def wt_instr_def step_def
    15 lemmas [simp del] = split_paired_All
    16 
    17 lemma wt_jvm_prog_impl_wt_instr_cor:
    18   "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); 
    19       G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
    20   ==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"
    21 apply (unfold correct_state_def Let_def correct_frame_def)
    22 apply simp
    23 apply (blast intro: wt_jvm_prog_impl_wt_instr)
    24 done
    25 
    26 lemma Load_correct:
    27 "\<lbrakk> wf_prog wt G;
    28    method (G,C) sig = Some (C,rT,maxl,ins); 
    29    ins!pc = Load idx; 
    30    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    31    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
    32    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
    33 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    34 apply (clarsimp simp add: defs1 map_eq_Cons)
    35 apply (rule conjI)
    36  apply (rule approx_loc_imp_approx_val_sup)
    37  apply simp+
    38 apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
    39 done
    40 
    41 lemma Store_correct:
    42 "\<lbrakk> wf_prog wt G;
    43   method (G,C) sig = Some (C,rT,maxl,ins);
    44   ins!pc = Store idx;
    45   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
    46   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
    47   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
    48 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    49 apply (clarsimp simp add: defs1 map_eq_Cons)
    50 apply (rule conjI)
    51  apply (blast intro: approx_stk_imp_approx_stk_sup)
    52 apply (blast intro: approx_loc_imp_approx_loc_subst approx_loc_imp_approx_loc_sup)
    53 done
    54 
    55 
    56 lemma conf_Intg_Integer [iff]:
    57   "G,h \<turnstile> Intg i \<Colon>\<preceq> PrimT Integer"
    58 by (simp add: conf_def)
    59 
    60 
    61 lemma Bipush_correct:
    62 "\<lbrakk> wf_prog wt G;
    63   method (G,C) sig = Some (C,rT,maxl,ins); 
    64   ins!pc = Bipush i; 
    65   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    66   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
    67   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
    68 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    69 apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
    70 apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
    71 done
    72 
    73 lemma NT_subtype_conv:
    74   "G \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))"
    75 proof -
    76   have "\<And>T T'. G \<turnstile> T' \<preceq> T \<Longrightarrow> T' = NT \<longrightarrow> (T=NT | (\<exists>C. T = Class C))"
    77     apply (erule widen.induct)
    78     apply auto
    79     apply (case_tac R)
    80     apply auto
    81     done
    82   note l = this
    83 
    84   show ?thesis 
    85     by (force intro: null dest: l)
    86 qed
    87 
    88 lemma Aconst_null_correct:
    89 "\<lbrakk> wf_prog wt G;
    90   method (G,C) sig = Some (C,rT,maxl,ins); 
    91   ins!pc =  Aconst_null; 
    92   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    93   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
    94   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
    95 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    96 apply (clarsimp simp add: defs1 map_eq_Cons)
    97 apply (rule conjI)
    98  apply (force simp add: approx_val_Null NT_subtype_conv)
    99 apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
   100 done
   101 
   102 
   103 lemma Cast_conf2:
   104   "\<lbrakk>wf_prog ok G; G,h\<turnstile>v\<Colon>\<preceq>RefT rt; cast_ok G C h v; G\<turnstile>Class C\<preceq>T; is_class G C\<rbrakk> 
   105   \<Longrightarrow> G,h\<turnstile>v\<Colon>\<preceq>T"
   106 apply (unfold cast_ok_def)
   107 apply (frule widen_Class)
   108 apply (elim exE disjE)
   109  apply (simp add: null)
   110 apply (clarsimp simp add: conf_def obj_ty_def)
   111 apply (cases v)
   112 apply (auto intro: null rtrancl_trans)
   113 done
   114 
   115 
   116 lemma Checkcast_correct:
   117 "\<lbrakk> wf_prog wt G;
   118   method (G,C) sig = Some (C,rT,maxl,ins); 
   119   ins!pc = Checkcast D; 
   120   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   121   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   122   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   123 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   124 apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def)
   125 apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2)
   126 done
   127 
   128 
   129 lemma Getfield_correct:
   130 "\<lbrakk> wf_prog wt G;
   131   method (G,C) sig = Some (C,rT,maxl,ins); 
   132   ins!pc = Getfield F D; 
   133   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   134   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   135   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   136 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   137 apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split)
   138 apply (frule conf_widen)
   139 apply assumption+
   140 apply (drule conf_RefTD)
   141 apply (clarsimp simp add: defs1 approx_val_def)
   142 apply (rule conjI)
   143  apply (drule widen_cfs_fields)
   144  apply assumption+
   145  apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def)
   146 apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
   147 done
   148 
   149 lemma Putfield_correct:
   150 "\<lbrakk> wf_prog wt G;
   151   method (G,C) sig = Some (C,rT,maxl,ins); 
   152   ins!pc = Putfield F D; 
   153   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   154   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   155   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   156 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   157 apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split)
   158 apply (clarsimp simp add: approx_val_def)
   159 apply (frule conf_widen)
   160 prefer 2
   161 apply assumption
   162 apply assumption
   163 apply (drule conf_RefTD)
   164 apply clarsimp
   165 apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap
   166   approx_stk_imp_approx_stk_sup
   167   approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
   168   hconf_imp_hconf_field_update
   169   correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields)
   170 done
   171 
   172 lemma collapse_paired_All:
   173   "(\<forall>x y. P(x,y)) = (\<forall>z. P z)"
   174   by fast
   175 
   176 lemma New_correct:
   177 "\<lbrakk> wf_prog wt G;
   178   method (G,C) sig = Some (C,rT,maxl,ins); 
   179   ins!pc = New cl_idx; 
   180   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   181   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   182   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   183 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   184 apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def
   185 		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
   186        split: option.split)
   187 apply (force dest!: iffD1 [OF collapse_paired_All]
   188             intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap approx_stk_imp_approx_stk_sup
   189                    approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
   190                    hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref
   191                    correct_init_obj simp add:  NT_subtype_conv approx_val_def conf_def
   192 		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
   193        split: option.split)
   194 done
   195 
   196 
   197 (****** Method Invocation ******)
   198 
   199 lemmas [simp del] = split_paired_Ex
   200 
   201 lemma Invoke_correct:
   202 "\<lbrakk> wt_jvm_prog G phi; 
   203   method (G,C) sig = Some (C,rT,maxl,ins); 
   204   ins ! pc = Invoke C' mn pTs; 
   205   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   206   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   207   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   208 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
   209 proof -
   210   assume wtprog: "wt_jvm_prog G phi"
   211   assume method: "method (G,C) sig = Some (C,rT,maxl,ins)"
   212   assume ins:    "ins ! pc = Invoke C' mn pTs"
   213   assume wti:    "wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"
   214   assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
   215   assume approx: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
   216   
   217   from wtprog 
   218   obtain wfmb where
   219     wfprog: "wf_prog wfmb G" 
   220     by (simp add: wt_jvm_prog_def)
   221 
   222   from ins method approx
   223   obtain s where
   224     heap_ok: "G\<turnstile>h hp\<surd>" and
   225     phi_pc:  "phi C sig!pc = Some s" and
   226     frame:   "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and
   227     frames:  "correct_frames G hp phi rT sig frs"
   228     by (clarsimp simp add: correct_state_def)
   229 
   230   from ins wti phi_pc
   231   obtain apTs X ST LT D' rT body where 
   232     s: "s = (rev apTs @ X # ST, LT)" and
   233     l: "length apTs = length pTs" and
   234     X: "G\<turnstile> X \<preceq> Class C'" and
   235     w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and
   236     mC': "method (G, C') (mn, pTs) = Some (D', rT, body)" and
   237     pc:  "Suc pc < length ins" and
   238     step: "G \<turnstile> step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc"
   239     by (simp add: wt_instr_def) (elim exE conjE, rule that)
   240 
   241   from step
   242   obtain ST' LT' where
   243     s': "phi C sig ! Suc pc = Some (ST', LT')"
   244     by (simp add: step_def split_paired_Ex) (elim, rule that)
   245 
   246   from X 
   247   obtain T where
   248     X_Ref: "X = RefT T"
   249     by - (drule widen_RefT2, erule exE, rule that)
   250   
   251   from s ins frame 
   252   obtain 
   253     a_stk: "approx_stk G hp stk (rev apTs @ X # ST)" and
   254     a_loc: "approx_loc G hp loc LT" and
   255     suc_l: "length loc = Suc (length (snd sig) + maxl)"
   256     by (simp add: correct_frame_def)
   257 
   258   from a_stk
   259   obtain opTs stk' oX where
   260     opTs:   "approx_stk G hp opTs (rev apTs)" and
   261     oX:     "approx_val G hp oX (Ok X)" and
   262     a_stk': "approx_stk G hp stk' ST" and
   263     stk':   "stk = opTs @ oX # stk'" and
   264     l_o:    "length opTs = length apTs" 
   265             "length stk' = length ST" 
   266     by - (drule approx_stk_append_lemma, simp, elim, simp)
   267 
   268   from oX 
   269   have "\<exists>T'. typeof (option_map obj_ty \<circ> hp) oX = Some T' \<and> G \<turnstile> T' \<preceq> X"
   270     by (clarsimp simp add: approx_val_def conf_def)
   271 
   272   with X_Ref
   273   obtain T' where
   274     oX_Ref: "typeof (option_map obj_ty \<circ> hp) oX = Some (RefT T')"
   275             "G \<turnstile> RefT T' \<preceq> X" 
   276     apply (elim, simp)
   277     apply (frule widen_RefT2)
   278     by (elim, simp)
   279 
   280   from stk' l_o l
   281   have oX_pos: "last (take (Suc (length pTs)) stk) = oX" 
   282     by simp
   283 
   284   with state' method ins 
   285   have Null_ok: "oX = Null \<Longrightarrow> ?thesis"
   286     by (simp add: correct_state_def raise_xcpt_def)
   287   
   288   { fix ref
   289     assume oX_Addr: "oX = Addr ref"
   290     
   291     with oX_Ref
   292     obtain obj where
   293       loc: "hp ref = Some obj" "obj_ty obj = RefT T'"
   294       by clarsimp
   295 
   296     then 
   297     obtain D where
   298       obj_ty: "obj_ty obj = Class D"
   299       by (auto simp add: obj_ty_def)
   300 
   301     with X_Ref oX_Ref loc
   302     obtain D: "G \<turnstile> Class D \<preceq> X"
   303       by simp
   304 
   305     with X_Ref
   306     obtain X' where 
   307       X': "X = Class X'"
   308       by - (drule widen_Class, elim, rule that)
   309       
   310     with X
   311     have "G \<turnstile> X' \<preceq>C C'" 
   312       by simp
   313 
   314     with mC' wfprog
   315     obtain D0 rT0 maxl0 ins0 where
   316       mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxl0, ins0)" "G\<turnstile>rT0\<preceq>rT"
   317       by (auto dest: subtype_widen_methd)
   318 
   319     from X' D
   320     have "G \<turnstile> D \<preceq>C X'" 
   321       by simp
   322 
   323     with wfprog mX
   324     obtain D'' rT' mxl' ins' where
   325       mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxl', ins')" 
   326           "G \<turnstile> rT' \<preceq> rT0"
   327       by (auto dest: subtype_widen_methd)
   328 
   329     from mX mD
   330     have rT': "G \<turnstile> rT' \<preceq> rT"
   331       by - (rule widen_trans)
   332     
   333     from mD wfprog
   334     obtain mD'': 
   335       "method (G, D'') (mn, pTs) = Some (D'', rT', mxl', ins')"
   336       "is_class G D''" 
   337       by (auto dest: method_in_md)
   338       
   339     from loc obj_ty
   340     have "fst (the (hp ref)) = D"
   341       by (simp add: obj_ty_def)
   342 
   343     with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD 
   344     have state'_val:
   345       "state' =
   346        Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' arbitrary, 
   347                   D'', (mn, pTs), 0) # (stk', loc, C, sig, Suc pc) # frs)"
   348       (is "state' = Norm (hp, ?f # ?f' # frs)")
   349       by (simp add: raise_xcpt_def)
   350     
   351     from wtprog mD''
   352     have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \<and> ins' \<noteq> []"
   353       by (auto dest: wt_jvm_prog_impl_wt_start)
   354     
   355     then
   356     obtain LT0 where
   357       LT0: "phi D'' (mn, pTs) ! 0 = Some ([], LT0)"
   358       by (clarsimp simp add: wt_start_def sup_state_def)
   359 
   360     have c_f: "correct_frame G hp ([], LT0) mxl' ins' ?f"
   361     proof -
   362       from start LT0
   363       have sup_loc: 
   364         "G \<turnstile> (Ok (Class D'') # map Ok pTs @ replicate mxl' Err) <=l LT0"
   365         (is "G \<turnstile> ?LT <=l LT0")
   366         by (simp add: wt_start_def sup_state_def)
   367 
   368       have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)"
   369         by (simp add: approx_loc_def approx_val_Err list_all2_def set_replicate_conv_if)
   370 
   371       from wfprog mD
   372       have "G \<turnstile> Class D \<preceq> Class D''"
   373         by (auto dest: method_wf_mdecl)
   374       with obj_ty loc
   375       have a: "approx_val G hp (Addr ref) (Ok (Class D''))"
   376         by (simp add: approx_val_def conf_def)
   377 
   378       from w l
   379       have "\<forall>x\<in>set (zip (rev apTs) (rev pTs)). x \<in> widen G"
   380         by (auto simp add: zip_rev)
   381       with wfprog l l_o opTs
   382       have "approx_loc G hp opTs (map Ok (rev pTs))"
   383         by (auto intro: assConv_approx_stk_imp_approx_loc)
   384       hence "approx_stk G hp opTs (rev pTs)"
   385         by (simp add: approx_stk_def)
   386       hence "approx_stk G hp (rev opTs) pTs"
   387         by (simp add: approx_stk_rev)
   388 
   389       with r a l_o l
   390       have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' arbitrary) ?LT"
   391         (is "approx_loc G hp ?lt ?LT")
   392         by (auto simp add: approx_loc_append approx_stk_def)
   393 
   394       from wfprog this sup_loc
   395       have "approx_loc G hp ?lt LT0"
   396         by (rule approx_loc_imp_approx_loc_sup)
   397 
   398       with start l_o l
   399       show ?thesis
   400         by (simp add: correct_frame_def)
   401     qed
   402 
   403     have c_f': "correct_frame G hp (tl ST', LT') maxl ins ?f'"
   404     proof -    
   405       from s s' mC' step l
   406       have "G \<turnstile> LT <=l LT'"
   407         by (simp add: step_def sup_state_def)
   408       with wfprog a_loc
   409       have a: "approx_loc G hp loc LT'"
   410         by (rule approx_loc_imp_approx_loc_sup)
   411       moreover
   412       from s s' mC' step l
   413       have  "G \<turnstile> map Ok ST <=l map Ok (tl ST')"
   414         by (auto simp add: step_def sup_state_def map_eq_Cons)
   415       with wfprog a_stk'
   416       have "approx_stk G hp stk' (tl ST')"
   417         by (rule approx_stk_imp_approx_stk_sup)
   418       ultimately
   419       show ?thesis
   420         by (simp add: correct_frame_def suc_l pc)
   421     qed
   422 
   423     with state'_val heap_ok mD'' ins method phi_pc s X' l 
   424          frames s' LT0 c_f c_f'
   425     have ?thesis
   426       by (simp add: correct_state_def) (intro exI conjI, force+)
   427   }
   428   
   429   with Null_ok oX_Ref
   430   show "G,phi \<turnstile>JVM state'\<surd>"
   431     by - (cases oX, auto)
   432 qed
   433 
   434 lemmas [simp del] = map_append
   435 
   436 lemma Return_correct:
   437 "\<lbrakk> wt_jvm_prog G phi;  
   438   method (G,C) sig = Some (C,rT,maxl,ins); 
   439   ins ! pc = Return; 
   440   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   441   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   442   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   443 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   444 apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm)
   445 apply (frule wt_jvm_prog_impl_wt_instr)
   446 apply (assumption, erule Suc_lessD)
   447 apply (unfold wt_jvm_prog_def)
   448 apply (fastsimp
   449   dest: subcls_widen_methd
   450   elim: widen_trans [COMP swap_prems_rl]
   451   intro: conf_widen
   452   simp: approx_val_def append_eq_conv_conj map_eq_Cons defs1)
   453 done
   454 
   455 lemmas [simp] = map_append
   456 
   457 lemma Goto_correct:
   458 "\<lbrakk> wf_prog wt G; 
   459   method (G,C) sig = Some (C,rT,maxl,ins); 
   460   ins ! pc = Goto branch; 
   461   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   462   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   463   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   464 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   465 apply (clarsimp simp add: defs1)
   466 apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
   467 done
   468 
   469 
   470 lemma Ifcmpeq_correct:
   471 "\<lbrakk> wf_prog wt G; 
   472   method (G,C) sig = Some (C,rT,maxl,ins); 
   473   ins ! pc = Ifcmpeq branch; 
   474   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   475   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   476   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   477 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   478 apply (clarsimp simp add: defs1)
   479 apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
   480 done
   481 
   482 lemma Pop_correct:
   483 "\<lbrakk> wf_prog wt G; 
   484   method (G,C) sig = Some (C,rT,maxl,ins); 
   485   ins ! pc = Pop;
   486   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   487   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   488   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   489 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   490 apply (clarsimp simp add: defs1)
   491 apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
   492 done
   493 
   494 lemma Dup_correct:
   495 "\<lbrakk> wf_prog wt G; 
   496   method (G,C) sig = Some (C,rT,maxl,ins); 
   497   ins ! pc = Dup;
   498   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   499   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   500   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   501 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   502 apply (clarsimp simp add: defs1 map_eq_Cons)
   503 apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   504              simp add: defs1 map_eq_Cons)
   505 done
   506 
   507 lemma Dup_x1_correct:
   508 "\<lbrakk> wf_prog wt G; 
   509   method (G,C) sig = Some (C,rT,maxl,ins); 
   510   ins ! pc = Dup_x1;
   511   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   512   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   513   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   514 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   515 apply (clarsimp simp add: defs1 map_eq_Cons)
   516 apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   517              simp add: defs1 map_eq_Cons)
   518 done
   519 
   520 lemma Dup_x2_correct:
   521 "\<lbrakk> wf_prog wt G; 
   522   method (G,C) sig = Some (C,rT,maxl,ins); 
   523   ins ! pc = Dup_x2;
   524   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   525   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   526   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   527 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   528 apply (clarsimp simp add: defs1 map_eq_Cons)
   529 apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   530              simp add: defs1 map_eq_Cons)
   531 done
   532 
   533 lemma Swap_correct:
   534 "\<lbrakk> wf_prog wt G; 
   535   method (G,C) sig = Some (C,rT,maxl,ins); 
   536   ins ! pc = Swap;
   537   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   538   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   539   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   540 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   541 apply (clarsimp simp add: defs1 map_eq_Cons)
   542 apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   543              simp add: defs1 map_eq_Cons)
   544 done
   545 
   546 lemma IAdd_correct:
   547 "\<lbrakk> wf_prog wt G; 
   548   method (G,C) sig = Some (C,rT,maxl,ins); 
   549   ins ! pc = IAdd; 
   550   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   551   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   552   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   553 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   554 apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
   555 apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup)
   556 done
   557 
   558 
   559 (** instr correct **)
   560 
   561 lemma instr_correct:
   562 "\<lbrakk> wt_jvm_prog G phi; 
   563   method (G,C) sig = Some (C,rT,maxl,ins); 
   564   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
   565   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   566 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   567 apply (frule wt_jvm_prog_impl_wt_instr_cor)
   568 apply assumption+
   569 apply (cases "ins!pc")
   570 prefer 9
   571 apply (blast intro: Invoke_correct)
   572 prefer 9
   573 apply (blast intro: Return_correct)
   574 apply (unfold wt_jvm_prog_def)
   575 apply (fast intro: Load_correct Store_correct Bipush_correct Aconst_null_correct 
   576        Checkcast_correct Getfield_correct Putfield_correct New_correct 
   577        Goto_correct Ifcmpeq_correct Pop_correct Dup_correct 
   578        Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+
   579 done
   580 
   581 
   582 (** Main **)
   583 
   584 lemma correct_state_impl_Some_method:
   585   "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> 
   586   \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
   587 by (auto simp add: correct_state_def Let_def)
   588 
   589 
   590 lemma BV_correct_1 [rule_format]:
   591 "\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> 
   592  \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   593 apply (simp only: split_tupled_all)
   594 apply (rename_tac xp hp frs)
   595 apply (case_tac xp)
   596  apply (case_tac frs)
   597   apply simp
   598  apply (simp only: split_tupled_all)
   599  apply hypsubst
   600  apply (frule correct_state_impl_Some_method)
   601  apply (force intro: instr_correct)
   602 apply (case_tac frs)
   603 apply simp_all
   604 done
   605 
   606 
   607 lemma L0:
   608   "\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
   609 by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex)
   610 
   611 lemma L1:
   612   "\<lbrakk>wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]\<rbrakk> 
   613   \<Longrightarrow> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
   614 apply (drule L0)
   615 apply assumption
   616 apply (fast intro: BV_correct_1)
   617 done
   618 
   619 
   620 theorem BV_correct [rule_format]:
   621 "\<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>"
   622 apply (unfold exec_all_def)
   623 apply (erule rtrancl_induct)
   624  apply simp
   625 apply (auto intro: BV_correct_1)
   626 done
   627 
   628 
   629 theorem BV_correct_initial:
   630 "\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk> 
   631  \<Longrightarrow>  approx_stk G hp stk (fst (the (((phi  C)  sig) ! pc))) \<and> approx_loc G hp loc (snd (the (((phi  C)  sig) ! pc)))"
   632 apply (drule BV_correct)
   633 apply assumption+
   634 apply (simp add: correct_state_def correct_frame_def split_def split: option.splits)
   635 done
   636 
   637 end