src/HOL/MicroJava/BV/Correct.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 13681 06cce9be31a4
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 
     2 (*  Title:      HOL/MicroJava/BV/Correct.thy
     3     ID:         $Id$
     4     Author:     Cornelia Pusch, Gerwin Klein
     5     Copyright   1999 Technische Universitaet Muenchen
     6 
     7 The invariant for the type safety proof.
     8 *)
     9 
    10 header {* \isaheader{BV Type Safety Invariant} *}
    11 
    12 theory Correct = BVSpec + JVMExec:
    13 
    14 constdefs
    15   approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"
    16   "approx_val G h v any == case any of Err \<Rightarrow> True | OK T \<Rightarrow> G,h\<turnstile>v::\<preceq>T"
    17 
    18   approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool"
    19   "approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
    20 
    21   approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool"
    22   "approx_stk G hp stk ST == approx_loc G hp stk (map OK ST)"
    23 
    24   correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
    25   "correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
    26                          approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
    27                          pc < length ins \<and> length loc=length(snd sig)+maxl+1"
    28 
    29 
    30 consts
    31  correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> bool"
    32 primrec
    33 "correct_frames G hp phi rT0 sig0 [] = True"
    34 
    35 "correct_frames G hp phi rT0 sig0 (f#frs) =
    36   (let (stk,loc,C,sig,pc) = f in
    37   (\<exists>ST LT rT maxs maxl ins et.
    38     phi C sig ! pc = Some (ST,LT) \<and> is_class G C \<and> 
    39     method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \<and>
    40   (\<exists>C' mn pTs. ins!pc = (Invoke C' mn pTs) \<and> 
    41          (mn,pTs) = sig0 \<and> 
    42          (\<exists>apTs D ST' LT'.
    43          (phi C sig)!pc = Some ((rev apTs) @ (Class D) # ST', LT') \<and>
    44          length apTs = length pTs \<and>
    45          (\<exists>D' rT' maxs' maxl' ins' et'.
    46            method (G,D) sig0 = Some(D',rT',(maxs',maxl',ins',et')) \<and>
    47            G \<turnstile> rT0 \<preceq> rT') \<and>
    48    correct_frame G hp (ST, LT) maxl ins f \<and> 
    49    correct_frames G hp phi rT sig frs))))"
    50 
    51 
    52 constdefs
    53  correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
    54                   ("_,_ |-JVM _ [ok]"  [51,51] 50)
    55 "correct_state G phi == \<lambda>(xp,hp,frs).
    56    case xp of
    57      None \<Rightarrow> (case frs of
    58              [] \<Rightarrow> True
    59              | (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and> preallocated hp \<and> 
    60       (let (stk,loc,C,sig,pc) = f
    61              in
    62                          \<exists>rT maxs maxl ins et s.
    63                          is_class G C \<and>
    64                          method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \<and>
    65                          phi C sig ! pc = Some s \<and>
    66        correct_frame G hp s maxl ins f \<and> 
    67              correct_frames G hp phi rT sig fs))
    68    | Some x \<Rightarrow> frs = []" 
    69 
    70 
    71 syntax (xsymbols)
    72  correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
    73                   ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
    74 
    75 
    76 lemma sup_ty_opt_OK:
    77   "(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')"
    78   apply (cases X)
    79   apply auto
    80   done
    81 
    82 
    83 section {* approx-val *}
    84 
    85 lemma approx_val_Err [simp,intro!]:
    86   "approx_val G hp x Err"
    87   by (simp add: approx_val_def)
    88 
    89 lemma approx_val_OK [iff]: 
    90   "approx_val G hp x (OK T) = (G,hp \<turnstile> x ::\<preceq> T)"
    91   by (simp add: approx_val_def)
    92 
    93 lemma approx_val_Null [simp,intro!]:
    94   "approx_val G hp Null (OK (RefT x))"
    95   by (auto simp add: approx_val_def)
    96 
    97 lemma approx_val_sup_heap:
    98   "\<lbrakk> approx_val G hp v T; hp \<le>| hp' \<rbrakk> \<Longrightarrow> approx_val G hp' v T"
    99   by (cases T) (blast intro: conf_hext)+
   100 
   101 lemma approx_val_heap_update:
   102   "\<lbrakk> hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> 
   103   \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
   104   by (cases v, auto simp add: obj_ty_def conf_def)
   105 
   106 lemma approx_val_widen:
   107   "\<lbrakk> approx_val G hp v T; G \<turnstile> T <=o T'; wf_prog wt G \<rbrakk>
   108   \<Longrightarrow> approx_val G hp v T'"
   109   by (cases T', auto simp add: sup_ty_opt_OK intro: conf_widen)
   110 
   111 section {* approx-loc *}
   112 
   113 lemma approx_loc_Nil [simp,intro!]:
   114   "approx_loc G hp [] []"
   115   by (simp add: approx_loc_def)
   116 
   117 lemma approx_loc_Cons [iff]:
   118   "approx_loc G hp (l#ls) (L#LT) = 
   119   (approx_val G hp l L \<and> approx_loc G hp ls LT)"
   120 by (simp add: approx_loc_def)
   121 
   122 lemma approx_loc_nth:
   123   "\<lbrakk> approx_loc G hp loc LT; n < length LT \<rbrakk>
   124   \<Longrightarrow> approx_val G hp (loc!n) (LT!n)"
   125   by (simp add: approx_loc_def list_all2_conv_all_nth)
   126 
   127 lemma approx_loc_imp_approx_val_sup:
   128   "\<lbrakk>approx_loc G hp loc LT; n < length LT; LT ! n = OK T; G \<turnstile> T \<preceq> T'; wf_prog wt G\<rbrakk> 
   129   \<Longrightarrow> G,hp \<turnstile> (loc!n) ::\<preceq> T'"
   130   apply (drule approx_loc_nth, assumption) 
   131   apply simp
   132   apply (erule conf_widen, assumption+)
   133   done
   134 
   135 lemma approx_loc_conv_all_nth:
   136   "approx_loc G hp loc LT = 
   137   (length loc = length LT \<and> (\<forall>n < length loc. approx_val G hp (loc!n) (LT!n)))"
   138   by (simp add: approx_loc_def list_all2_conv_all_nth)
   139 
   140 lemma approx_loc_sup_heap:
   141   "\<lbrakk> approx_loc G hp loc LT; hp \<le>| hp' \<rbrakk>
   142   \<Longrightarrow> approx_loc G hp' loc LT"
   143   apply (clarsimp simp add: approx_loc_conv_all_nth)
   144   apply (blast intro: approx_val_sup_heap)
   145   done
   146 
   147 lemma approx_loc_widen:
   148   "\<lbrakk> approx_loc G hp loc LT; G \<turnstile> LT <=l LT'; wf_prog wt G \<rbrakk>
   149   \<Longrightarrow> approx_loc G hp loc LT'"
   150 apply (unfold Listn.le_def lesub_def sup_loc_def)
   151 apply (simp (no_asm_use) only: list_all2_conv_all_nth approx_loc_conv_all_nth)
   152 apply (simp (no_asm_simp))
   153 apply clarify
   154 apply (erule allE, erule impE) 
   155  apply simp
   156 apply (erule approx_val_widen)
   157  apply simp
   158 apply assumption
   159 done
   160 
   161 lemma loc_widen_Err [dest]:
   162   "\<And>XT. G \<turnstile> replicate n Err <=l XT \<Longrightarrow> XT = replicate n Err"
   163   by (induct n) auto
   164   
   165 lemma approx_loc_Err [iff]:
   166   "approx_loc G hp (replicate n v) (replicate n Err)"
   167   by (induct n) auto
   168 
   169 lemma approx_loc_subst:
   170   "\<lbrakk> approx_loc G hp loc LT; approx_val G hp x X \<rbrakk>
   171   \<Longrightarrow> approx_loc G hp (loc[idx:=x]) (LT[idx:=X])"
   172 apply (unfold approx_loc_def list_all2_def)
   173 apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
   174 done
   175 
   176 lemma approx_loc_append:
   177   "length l1=length L1 \<Longrightarrow>
   178   approx_loc G hp (l1@l2) (L1@L2) = 
   179   (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
   180   apply (unfold approx_loc_def list_all2_def)
   181   apply (simp cong: conj_cong)
   182   apply blast
   183   done
   184 
   185 section {* approx-stk *}
   186 
   187 lemma approx_stk_rev_lem:
   188   "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
   189   apply (unfold approx_stk_def approx_loc_def)
   190   apply (simp add: rev_map [THEN sym])
   191   done
   192 
   193 lemma approx_stk_rev:
   194   "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)"
   195   by (auto intro: subst [OF approx_stk_rev_lem])
   196 
   197 lemma approx_stk_sup_heap:
   198   "\<lbrakk> approx_stk G hp stk ST; hp \<le>| hp' \<rbrakk> \<Longrightarrow> approx_stk G hp' stk ST"
   199   by (auto intro: approx_loc_sup_heap simp add: approx_stk_def)
   200 
   201 lemma approx_stk_widen:
   202   "\<lbrakk> approx_stk G hp stk ST; G \<turnstile> map OK ST <=l map OK ST'; wf_prog wt G \<rbrakk>
   203   \<Longrightarrow> approx_stk G hp stk ST'" 
   204   by (auto elim: approx_loc_widen simp add: approx_stk_def)
   205 
   206 lemma approx_stk_Nil [iff]:
   207   "approx_stk G hp [] []"
   208   by (simp add: approx_stk_def)
   209 
   210 lemma approx_stk_Cons [iff]:
   211   "approx_stk G hp (x#stk) (S#ST) = 
   212   (approx_val G hp x (OK S) \<and> approx_stk G hp stk ST)"
   213   by (simp add: approx_stk_def)
   214 
   215 lemma approx_stk_Cons_lemma [iff]:
   216   "approx_stk G hp stk (S#ST') = 
   217   (\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (OK S) \<and> approx_stk G hp stk' ST')"
   218   by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)
   219 
   220 lemma approx_stk_append:
   221   "approx_stk G hp stk (S@S') \<Longrightarrow>
   222   (\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length S' \<and> 
   223             approx_stk G hp s S \<and> approx_stk G hp stk' S')"
   224   by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
   225 
   226 lemma approx_stk_all_widen:
   227   "\<lbrakk> approx_stk G hp stk ST; \<forall>x \<in> set (zip ST ST'). x \<in> widen G; length ST = length ST'; wf_prog wt G \<rbrakk> 
   228   \<Longrightarrow> approx_stk G hp stk ST'"
   229 apply (unfold approx_stk_def)
   230 apply (clarsimp simp add: approx_loc_conv_all_nth all_set_conv_all_nth)
   231 apply (erule allE, erule impE, assumption)
   232 apply (erule allE, erule impE, assumption)
   233 apply (erule conf_widen, assumption+)
   234 done
   235 
   236 section {* oconf *}
   237 
   238 lemma oconf_field_update:
   239   "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
   240   \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
   241   by (simp add: oconf_def lconf_def)
   242 
   243 lemma oconf_newref:
   244   "\<lbrakk>hp oref = None; G,hp \<turnstile> obj \<surd>; G,hp \<turnstile> obj' \<surd>\<rbrakk> \<Longrightarrow> G,hp(oref\<mapsto>obj') \<turnstile> obj \<surd>"
   245   apply (unfold oconf_def lconf_def)
   246   apply simp
   247   apply (blast intro: conf_hext hext_new)
   248   done
   249 
   250 lemma oconf_heap_update:
   251   "\<lbrakk> hp a = Some obj'; obj_ty obj' = obj_ty obj''; G,hp\<turnstile>obj\<surd> \<rbrakk>
   252   \<Longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
   253   apply (unfold oconf_def lconf_def)
   254   apply (fastsimp intro: approx_val_heap_update)
   255   done
   256 
   257 section {* hconf *}
   258 
   259 lemma hconf_newref:
   260   "\<lbrakk> hp oref = None; G\<turnstile>h hp\<surd>; G,hp\<turnstile>obj\<surd> \<rbrakk> \<Longrightarrow> G\<turnstile>h hp(oref\<mapsto>obj)\<surd>"
   261   apply (simp add: hconf_def)
   262   apply (fast intro: oconf_newref)
   263   done
   264 
   265 lemma hconf_field_update:
   266   "\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs); 
   267      G,hp\<turnstile>v::\<preceq>T; G\<turnstile>h hp\<surd> \<rbrakk> 
   268   \<Longrightarrow> G\<turnstile>h hp(a \<mapsto> (oT, fs(X\<mapsto>v)))\<surd>"
   269   apply (simp add: hconf_def)
   270   apply (fastsimp intro: oconf_heap_update oconf_field_update 
   271                   simp add: obj_ty_def)
   272   done
   273 
   274 section {* preallocated *}
   275 
   276 lemma preallocated_field_update:
   277   "\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs); 
   278      G\<turnstile>h hp\<surd>; preallocated hp \<rbrakk> 
   279   \<Longrightarrow> preallocated (hp(a \<mapsto> (oT, fs(X\<mapsto>v))))"
   280   apply (unfold preallocated_def)
   281   apply (rule allI)
   282   apply (erule_tac x=x in allE)
   283   apply simp
   284   apply (rule ccontr)  
   285   apply (unfold hconf_def)
   286   apply (erule allE, erule allE, erule impE, assumption)
   287   apply (unfold oconf_def lconf_def)
   288   apply (simp del: split_paired_All)
   289   done  
   290 
   291 
   292 lemma 
   293   assumes none: "hp oref = None" and alloc: "preallocated hp"
   294   shows preallocated_newref: "preallocated (hp(oref\<mapsto>obj))"
   295 proof (cases oref)
   296   case (XcptRef x) 
   297   with none alloc have "False" by (auto elim: preallocatedE [of _ x])
   298   thus ?thesis ..
   299 next
   300   case (Loc l)
   301   with alloc show ?thesis by (simp add: preallocated_def)
   302 qed
   303   
   304 section {* correct-frames *}
   305 
   306 lemmas [simp del] = fun_upd_apply
   307 
   308 lemma correct_frames_field_update [rule_format]:
   309   "\<forall>rT C sig. 
   310   correct_frames G hp phi rT sig frs \<longrightarrow> 
   311   hp a = Some (C,fs) \<longrightarrow> 
   312   map_of (fields (G, C)) fl = Some fd \<longrightarrow> 
   313   G,hp\<turnstile>v::\<preceq>fd 
   314   \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs";
   315 apply (induct frs)
   316  apply simp
   317 apply clarify
   318 apply (simp (no_asm_use))
   319 apply clarify
   320 apply (unfold correct_frame_def)
   321 apply (simp (no_asm_use))
   322 apply clarify
   323 apply (intro exI conjI)
   324     apply assumption+
   325    apply (erule approx_stk_sup_heap)
   326    apply (erule hext_upd_obj)
   327   apply (erule approx_loc_sup_heap)
   328   apply (erule hext_upd_obj)
   329  apply assumption+
   330 apply blast
   331 done
   332 
   333 lemma correct_frames_newref [rule_format]:
   334   "\<forall>rT C sig. 
   335   hp x = None \<longrightarrow> 
   336   correct_frames G hp phi rT sig frs \<longrightarrow>
   337   correct_frames G (hp(x \<mapsto> obj)) phi rT sig frs"
   338 apply (induct frs)
   339  apply simp
   340 apply clarify
   341 apply (simp (no_asm_use))
   342 apply clarify
   343 apply (unfold correct_frame_def)
   344 apply (simp (no_asm_use))
   345 apply clarify
   346 apply (intro exI conjI)
   347     apply assumption+
   348    apply (erule approx_stk_sup_heap)
   349    apply (erule hext_new)
   350   apply (erule approx_loc_sup_heap)
   351   apply (erule hext_new)
   352  apply assumption+
   353 apply blast
   354 done
   355 
   356 end