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