src/HOL/MicroJava/BV/Correct.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/Correct.thy
     2     ID:         $Id$
     3     Author:     Cornelia Pusch
     4     Copyright   1999 Technische Universitaet Muenchen
     5 
     6 The invariant for the type safety proof.
     7 *)
     8 
     9 header "Type Safety Invariant"
    10 
    11 theory Correct = BVSpec:
    12 
    13 constdefs
    14  approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"
    15 "approx_val G h v any \<equiv> case any of Err \<Rightarrow> True | Ok T \<Rightarrow> G,h\<turnstile>v\<Colon>\<preceq>T"
    16 
    17  approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool"
    18 "approx_loc G hp loc LT \<equiv> list_all2 (approx_val G hp) loc LT"
    19 
    20  approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool"
    21 "approx_stk G hp stk ST \<equiv> approx_loc G hp stk (map Ok ST)"
    22 
    23  correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
    24 "correct_frame G hp \<equiv> \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
    25    approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
    26    pc < length ins \<and> length loc=length(snd sig)+maxl+1"
    27 
    28  correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
    29 "correct_frame_opt G hp s \<equiv> case s of None \<Rightarrow> \<lambda>maxl ins f. False | Some t \<Rightarrow> correct_frame G hp t"
    30 
    31 
    32 consts
    33  correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> bool"
    34 primrec
    35 "correct_frames G hp phi rT0 sig0 [] = True"
    36 
    37 "correct_frames G hp phi rT0 sig0 (f#frs) =
    38 	(let (stk,loc,C,sig,pc) = f in
    39   (\<exists>ST LT rT maxl ins.
    40     phi C sig ! pc = Some (ST,LT) \<and> 
    41     method (G,C) sig = Some(C,rT,(maxl,ins)) \<and>
    42 	(\<exists>C' mn pTs k. pc = k+1 \<and> ins!k = (Invoke C' mn pTs) \<and>
    43          (mn,pTs) = sig0 \<and> 
    44          (\<exists>apTs D ST' LT'.
    45          (phi C sig)!k = Some ((rev apTs) @ (Class D) # ST', LT') \<and>
    46          length apTs = length pTs \<and>
    47          (\<exists>D' rT' maxl' ins'.
    48            method (G,D) sig0 = Some(D',rT',(maxl',ins')) \<and>
    49            G \<turnstile> rT0 \<preceq> rT') \<and>
    50 	 correct_frame G hp (tl ST, LT) maxl ins f \<and> 
    51 	 correct_frames G hp phi rT sig frs))))"
    52 
    53 
    54 constdefs
    55  correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
    56                   ("_,_\<turnstile>JVM _\<surd>"  [51,51] 50)
    57 "correct_state G phi \<equiv> \<lambda>(xp,hp,frs).
    58    case xp of
    59      None \<Rightarrow> (case frs of
    60 	           [] \<Rightarrow> True
    61              | (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and>
    62 			(let (stk,loc,C,sig,pc) = f
    63 		         in
    64                          \<exists>rT maxl ins s.
    65                          method (G,C) sig = Some(C,rT,(maxl,ins)) \<and>
    66                          phi C sig ! pc = Some s \<and>
    67 			 correct_frame G hp s maxl ins f \<and> 
    68 		         correct_frames G hp phi rT sig fs))
    69    | Some x \<Rightarrow> True" 
    70 
    71 
    72 lemma sup_heap_newref:
    73   "hp x = None \<Longrightarrow> hp \<le>| hp(newref hp \<mapsto> obj)"
    74 apply (unfold hext_def)
    75 apply clarsimp
    76 apply (drule newref_None 1) back
    77 apply simp
    78 .
    79 
    80 lemma sup_heap_update_value:
    81   "hp a = Some (C,od') \<Longrightarrow> hp \<le>| hp (a \<mapsto> (C,od))"
    82 by (simp add: hext_def)
    83 
    84 
    85 (** approx_val **)
    86 
    87 lemma approx_val_Err:
    88   "approx_val G hp x Err"
    89 by (simp add: approx_val_def)
    90 
    91 lemma approx_val_Null:
    92   "approx_val G hp Null (Ok (RefT x))"
    93 by (auto intro: null simp add: approx_val_def)
    94 
    95 lemma approx_val_imp_approx_val_assConvertible [rule_format]: 
    96   "wf_prog wt G \<Longrightarrow> approx_val G hp v (Ok T) \<longrightarrow> G\<turnstile> T\<preceq>T' \<longrightarrow> approx_val G hp v (Ok T')"
    97 by (cases T) (auto intro: conf_widen simp add: approx_val_def)
    98 
    99 lemma approx_val_imp_approx_val_sup_heap [rule_format]:
   100   "approx_val G hp v at \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_val G hp' v at"
   101 apply (simp add: approx_val_def split: err.split)
   102 apply (blast intro: conf_hext)
   103 .
   104 
   105 lemma approx_val_imp_approx_val_heap_update:
   106   "\<lbrakk>hp a = Some obj'; G,hp\<turnstile> v\<Colon>\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> 
   107   \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v\<Colon>\<preceq>T"
   108 by (cases v, auto simp add: obj_ty_def conf_def)
   109 
   110 lemma approx_val_imp_approx_val_sup [rule_format]:
   111   "wf_prog wt G \<Longrightarrow> (approx_val G h v us) \<longrightarrow> (G \<turnstile> us <=o us') \<longrightarrow> (approx_val G h v us')"
   112 apply (simp add: sup_PTS_eq approx_val_def split: err.split)
   113 apply (blast intro: conf_widen)
   114 .
   115 
   116 lemma approx_loc_imp_approx_val_sup:
   117   "\<lbrakk>wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at\<rbrakk>
   118   \<Longrightarrow> approx_val G hp v at"
   119 apply (unfold approx_loc_def)
   120 apply (unfold list_all2_def)
   121 apply (auto intro: approx_val_imp_approx_val_sup simp add: split_def all_set_conv_all_nth)
   122 .
   123 
   124 
   125 (** approx_loc **)
   126 
   127 lemma approx_loc_Cons [iff]:
   128   "approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \<and> approx_loc G hp xs ls)"
   129 by (simp add: approx_loc_def)
   130 
   131 lemma assConv_approx_stk_imp_approx_loc [rule_format]:
   132   "wf_prog wt G \<Longrightarrow> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) 
   133   \<longrightarrow> length tys_n = length ts \<longrightarrow> approx_stk G hp s tys_n \<longrightarrow> 
   134   approx_loc G hp s (map Ok ts)"
   135 apply (unfold approx_stk_def approx_loc_def list_all2_def)
   136 apply (clarsimp simp add: all_set_conv_all_nth)
   137 apply (rule approx_val_imp_approx_val_assConvertible)
   138 apply auto
   139 .
   140 
   141 
   142 lemma approx_loc_imp_approx_loc_sup_heap [rule_format]:
   143   "\<forall>lvars. approx_loc G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_loc G hp' lvars lt"
   144 apply (unfold approx_loc_def list_all2_def)
   145 apply (cases lt)
   146  apply simp
   147 apply clarsimp
   148 apply (rule approx_val_imp_approx_val_sup_heap)
   149 apply auto
   150 .
   151 
   152 lemma approx_loc_imp_approx_loc_sup [rule_format]:
   153   "wf_prog wt G \<Longrightarrow> approx_loc G hp lvars lt \<longrightarrow> G \<turnstile> lt <=l lt' \<longrightarrow> approx_loc G hp lvars lt'"
   154 apply (unfold sup_loc_def approx_loc_def list_all2_def)
   155 apply (auto simp add: all_set_conv_all_nth)
   156 apply (auto elim: approx_val_imp_approx_val_sup)
   157 .
   158 
   159 
   160 lemma approx_loc_imp_approx_loc_subst [rule_format]:
   161   "\<forall>loc idx x X. (approx_loc G hp loc LT) \<longrightarrow> (approx_val G hp x X) 
   162   \<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
   163 apply (unfold approx_loc_def list_all2_def)
   164 apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
   165 .
   166 
   167 
   168 lemmas [cong] = conj_cong 
   169 
   170 lemma approx_loc_append [rule_format]:
   171   "\<forall>L1 l2 L2. length l1=length L1 \<longrightarrow> 
   172   approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
   173 apply (unfold approx_loc_def list_all2_def)
   174 apply simp
   175 apply blast
   176 .
   177 
   178 lemmas [cong del] = conj_cong
   179 
   180 
   181 (** approx_stk **)
   182 
   183 lemma approx_stk_rev_lem:
   184   "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
   185 apply (unfold approx_stk_def approx_loc_def list_all2_def)
   186 apply (auto simp add: zip_rev sym [OF rev_map])
   187 .
   188 
   189 lemma approx_stk_rev:
   190   "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)"
   191 by (auto intro: subst [OF approx_stk_rev_lem])
   192 
   193 
   194 lemma approx_stk_imp_approx_stk_sup_heap [rule_format]:
   195   "\<forall>lvars. approx_stk G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_stk G hp' lvars lt"
   196 by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
   197 
   198 lemma approx_stk_imp_approx_stk_sup [rule_format]:
   199   "wf_prog wt G \<Longrightarrow> approx_stk G hp lvars st \<longrightarrow> (G \<turnstile> map Ok st <=l (map Ok st')) 
   200   \<longrightarrow> approx_stk G hp lvars st'" 
   201 by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def)
   202 
   203 lemma approx_stk_Nil [iff]:
   204   "approx_stk G hp [] []"
   205 by (simp add: approx_stk_def approx_loc_def)
   206 
   207 lemma approx_stk_Cons [iff]:
   208   "approx_stk G hp (x # stk) (S#ST) = 
   209    (approx_val G hp x (Ok S) \<and> approx_stk G hp stk ST)"
   210 by (simp add: approx_stk_def approx_loc_def)
   211 
   212 lemma approx_stk_Cons_lemma [iff]:
   213   "approx_stk G hp stk (S#ST') = 
   214   (\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (Ok S) \<and> approx_stk G hp stk' ST')"
   215 by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)
   216 
   217 lemma approx_stk_append_lemma:
   218   "approx_stk G hp stk (S@ST') \<Longrightarrow>
   219    (\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length ST' \<and> 
   220              approx_stk G hp s S \<and> approx_stk G hp stk' ST')"
   221 by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
   222 
   223 
   224 (** oconf **)
   225 
   226 lemma correct_init_obj:
   227   "\<lbrakk>is_class G C; wf_prog wt G\<rbrakk> \<Longrightarrow> 
   228   G,h \<turnstile> (C, map_of (map (\<lambda>(f,fT).(f,default_val fT)) (fields(G,C)))) \<surd>"
   229 apply (unfold oconf_def lconf_def)
   230 apply (simp add: map_of_map)
   231 apply (force intro: defval_conf dest: map_of_SomeD is_type_fields)
   232 .
   233 
   234 
   235 lemma oconf_imp_oconf_field_update [rule_format]:
   236   "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v\<Colon>\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
   237   \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
   238 by (simp add: oconf_def lconf_def)
   239 
   240 
   241 lemma oconf_imp_oconf_heap_newref [rule_format]:
   242 "hp x = None \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G,hp\<turnstile>obj'\<surd> \<longrightarrow> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>"
   243 apply (unfold oconf_def lconf_def)
   244 apply simp
   245 apply (fast intro: conf_hext sup_heap_newref)
   246 .
   247 
   248 
   249 lemma oconf_imp_oconf_heap_update [rule_format]:
   250   "hp a = Some obj' \<longrightarrow> obj_ty obj' = obj_ty obj'' \<longrightarrow> G,hp\<turnstile>obj\<surd> 
   251   \<longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
   252 apply (unfold oconf_def lconf_def)
   253 apply simp
   254 apply (force intro: approx_val_imp_approx_val_heap_update)
   255 .
   256 
   257 
   258 (** hconf **)
   259 
   260 
   261 lemma hconf_imp_hconf_newref [rule_format]:
   262   "hp x = None \<longrightarrow> G\<turnstile>h hp\<surd> \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
   263 apply (simp add: hconf_def)
   264 apply (fast intro: oconf_imp_oconf_heap_newref)
   265 .
   266 
   267 lemma hconf_imp_hconf_field_update [rule_format]:
   268   "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> 
   269   G,hp\<turnstile>v\<Colon>\<preceq>T \<and> G\<turnstile>h hp\<surd> \<longrightarrow> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>"
   270 apply (simp add: hconf_def)
   271 apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update 
   272              simp add: obj_ty_def)
   273 .
   274 
   275 (** correct_frames **)
   276 
   277 lemmas [simp del] = fun_upd_apply
   278 
   279 lemma correct_frames_imp_correct_frames_field_update [rule_format]:
   280   "\<forall>rT C sig. correct_frames G hp phi rT sig frs \<longrightarrow> 
   281   hp a = Some (C,od) \<longrightarrow> map_of (fields (G, C)) fl = Some fd \<longrightarrow> 
   282   G,hp\<turnstile>v\<Colon>\<preceq>fd 
   283   \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>v)))) phi rT sig frs";
   284 apply (induct frs)
   285  apply simp
   286 apply (clarsimp simp add: correct_frame_def) (*takes long*)
   287 apply (intro exI conjI)
   288      apply simp
   289     apply simp
   290    apply force
   291   apply simp
   292  apply (rule approx_stk_imp_approx_stk_sup_heap)
   293   apply simp
   294  apply (rule sup_heap_update_value)
   295  apply simp
   296 apply (rule approx_loc_imp_approx_loc_sup_heap)
   297  apply simp
   298 apply (rule sup_heap_update_value)
   299 apply simp
   300 .
   301 
   302 lemma correct_frames_imp_correct_frames_newref [rule_format]:
   303   "\<forall>rT C sig. hp x = None \<longrightarrow> correct_frames G hp phi rT sig frs \<and> oconf G hp obj 
   304   \<longrightarrow> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
   305 apply (induct frs)
   306  apply simp
   307 apply (clarsimp simp add: correct_frame_def)
   308 apply (intro exI conjI)
   309      apply simp
   310     apply simp
   311    apply force
   312   apply simp
   313  apply (rule approx_stk_imp_approx_stk_sup_heap)
   314   apply simp
   315  apply (rule sup_heap_newref)
   316  apply simp
   317 apply (rule approx_loc_imp_approx_loc_sup_heap)
   318  apply simp
   319 apply (rule sup_heap_newref)
   320 apply simp
   321 .
   322 
   323 end
   324