src/HOL/MicroJava/BV/LBVCorrect.thy
author kleing
Thu Sep 21 10:42:49 2000 +0200 (2000-09-21)
changeset 10042 7164dc0d24d8
parent 9970 dfe4747c8318
child 10496 f2d304bdf3cc
permissions -rw-r--r--
unsymbolized
kleing@9757
     1
(*  Title:      HOL/MicroJava/BV/BVLCorrect.thy
kleing@8245
     2
    ID:         $Id$
kleing@8245
     3
    Author:     Gerwin Klein
kleing@8245
     4
    Copyright   1999 Technische Universitaet Muenchen
kleing@9054
     5
*)
kleing@8245
     6
kleing@9054
     7
header {* Correctness of the LBV *}
kleing@8245
     8
kleing@9549
     9
theory LBVCorrect = BVSpec + LBVSpec:
kleing@8245
    10
kleing@9757
    11
lemmas [simp del] = split_paired_Ex split_paired_All
kleing@9757
    12
kleing@8245
    13
constdefs
kleing@10042
    14
fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] => bool"
kleing@10042
    15
"fits phi is G rT s0 cert == 
kleing@10042
    16
  (\<forall>pc s1. pc < length is -->
kleing@10042
    17
    (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 -->
kleing@10042
    18
    (case cert!pc of None   => phi!pc = s1
kleing@10042
    19
                   | Some t => phi!pc = Some t)))"
kleing@9757
    20
kleing@9757
    21
constdefs
kleing@10042
    22
make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] => method_type"
kleing@10042
    23
"make_phi is G rT s0 cert == 
kleing@9757
    24
   map (\<lambda>pc. case cert!pc of 
kleing@10042
    25
               None   => val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) 
kleing@10042
    26
             | Some t => Some t) [0..length is(]"
kleing@9757
    27
kleing@9012
    28
kleing@9757
    29
lemma fitsD_None:
kleing@10042
    30
  "[|fits phi is G rT s0 cert; pc < length is;
kleing@9757
    31
    wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
kleing@10042
    32
    cert ! pc = None|] ==> phi!pc = s1"
kleing@9757
    33
  by (auto simp add: fits_def)
kleing@9012
    34
kleing@9757
    35
lemma fitsD_Some:
kleing@10042
    36
  "[|fits phi is G rT s0 cert; pc < length is;
kleing@9757
    37
    wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
kleing@10042
    38
    cert ! pc = Some t|] ==> phi!pc = Some t"
kleing@9757
    39
  by (auto simp add: fits_def)
kleing@9757
    40
kleing@9757
    41
lemma make_phi_Some:
kleing@9757
    42
  "[| pc < length is; cert!pc = Some t |] ==> 
kleing@9757
    43
  make_phi is G rT s0 cert ! pc = Some t"
kleing@9757
    44
  by (simp add: make_phi_def)
kleing@9757
    45
kleing@9757
    46
lemma make_phi_None:
kleing@9757
    47
  "[| pc < length is; cert!pc = None |] ==> 
kleing@9757
    48
  make_phi is G rT s0 cert ! pc = 
kleing@9757
    49
  val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)"
kleing@9757
    50
  by (simp add: make_phi_def)
kleing@9012
    51
kleing@9012
    52
lemma exists_phi:
kleing@9757
    53
  "\<exists>phi. fits phi is G rT s0 cert"  
kleing@9757
    54
proof - 
kleing@9757
    55
  have "fits (make_phi is G rT s0 cert) is G rT s0 cert"
kleing@9757
    56
    by (auto simp add: fits_def make_phi_Some make_phi_None 
kleing@9757
    57
             split: option.splits) 
kleing@9549
    58
kleing@9757
    59
  thus ?thesis
kleing@9757
    60
    by blast
kleing@9757
    61
qed
kleing@9757
    62
  
kleing@9012
    63
lemma fits_lemma1:
kleing@9757
    64
  "[| wtl_inst_list is G rT cert (length is) 0 s = Ok s'; fits phi is G rT s cert |]
kleing@10042
    65
  ==> \<forall>pc t. pc < length is --> cert!pc = Some t --> phi!pc = Some t"
kleing@9757
    66
proof (intro strip)
kleing@9757
    67
  fix pc t 
kleing@9757
    68
  assume "wtl_inst_list is G rT cert (length is) 0 s = Ok s'"
kleing@9757
    69
  then 
kleing@9757
    70
  obtain s'' where
kleing@9757
    71
    "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s''"
kleing@9757
    72
    by (blast dest: wtl_take)
kleing@9757
    73
  moreover
kleing@9757
    74
  assume "fits phi is G rT s cert" 
kleing@9757
    75
         "pc < length is" 
kleing@9757
    76
         "cert ! pc = Some t"
kleing@9757
    77
  ultimately
kleing@9757
    78
  show "phi!pc = Some t" by (auto dest: fitsD_Some)
kleing@9580
    79
qed
kleing@9012
    80
kleing@9012
    81
kleing@9012
    82
lemma wtl_suc_pc:
kleing@9757
    83
 "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
kleing@9757
    84
     wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s';
kleing@9757
    85
     wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s'';
kleing@9757
    86
     fits phi is G rT s cert; Suc pc < length is |] ==>
kleing@9757
    87
  G \<turnstile> s'' <=' phi ! Suc pc"
kleing@9757
    88
proof -
kleing@9757
    89
  
kleing@9757
    90
  assume all:  "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
kleing@9757
    91
  assume fits: "fits phi is G rT s cert"
kleing@9757
    92
kleing@9757
    93
  assume wtl:  "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and
kleing@9757
    94
         wtc:  "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''" and
kleing@9757
    95
         pc:   "Suc pc < length is"
kleing@9757
    96
kleing@9757
    97
  hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = Ok s''"
kleing@9757
    98
    by (rule wtl_Suc)
kleing@9757
    99
kleing@9757
   100
  from all
kleing@9757
   101
  have app: 
kleing@9757
   102
  "wtl_inst_list (take (Suc pc) is@drop (Suc pc) is) G rT cert (length is) 0 s \<noteq> Err"
kleing@9757
   103
    by simp
kleing@9012
   104
kleing@9757
   105
  from pc 
kleing@9757
   106
  have "0 < length (drop (Suc pc) is)" 
kleing@9757
   107
    by simp
kleing@9757
   108
  then 
kleing@9757
   109
  obtain l ls where
kleing@9757
   110
    "drop (Suc pc) is = l#ls"
kleing@9757
   111
    by (auto simp add: neq_Nil_conv simp del: length_drop)
kleing@9757
   112
  with app wts pc
kleing@9757
   113
  obtain x where 
kleing@9757
   114
    "wtl_cert l G rT s'' cert (length is) (Suc pc) = Ok x"
kleing@9757
   115
    by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
kleing@9012
   116
kleing@10042
   117
  hence c1: "!!t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
kleing@9757
   118
    by (simp add: wtl_cert_def split: if_splits)
kleing@9757
   119
  moreover
kleing@9757
   120
  from fits pc wts
kleing@10042
   121
  have c2: "!!t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc"
kleing@9757
   122
    by - (drule fitsD_Some, auto)
kleing@9757
   123
  moreover
kleing@9757
   124
  from fits pc wts
kleing@9757
   125
  have c3: "cert!Suc pc = None ==> phi!Suc pc = s''"
kleing@9757
   126
    by (rule fitsD_None)
kleing@9757
   127
  ultimately
kleing@9012
   128
kleing@9757
   129
  show ?thesis 
kleing@9757
   130
    by - (cases "cert ! Suc pc", auto)
kleing@9549
   131
qed
kleing@9012
   132
kleing@9376
   133
kleing@9012
   134
lemma wtl_fits_wt:
kleing@9757
   135
  "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err; 
kleing@9757
   136
      fits phi is G rT s cert; pc < length is |] ==>
kleing@9757
   137
   wt_instr (is!pc) G rT phi (length is) pc"
kleing@9757
   138
proof -
kleing@9757
   139
kleing@9757
   140
  assume fits: "fits phi is G rT s cert"
kleing@9012
   141
kleing@9757
   142
  assume pc:  "pc < length is" and
kleing@9757
   143
         wtl: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
kleing@9757
   144
        
kleing@9757
   145
  then
kleing@9757
   146
  obtain s' s'' where
kleing@9757
   147
    w: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and
kleing@9757
   148
    c: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''"
kleing@9757
   149
    by - (drule wtl_all, auto)
kleing@9757
   150
kleing@9757
   151
  from fits wtl pc
kleing@9757
   152
  have cert_Some: 
kleing@10042
   153
    "!!t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t"
kleing@9757
   154
    by (auto dest: fits_lemma1)
kleing@9549
   155
  
kleing@9757
   156
  from fits wtl pc
kleing@9757
   157
  have cert_None: "cert!pc = None ==> phi!pc = s'"
kleing@9757
   158
    by - (drule fitsD_None)
kleing@9757
   159
  
kleing@9757
   160
  from pc c cert_None cert_Some
kleing@9757
   161
  have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert (length is) pc = Ok s''"
kleing@9757
   162
    by (auto simp add: wtl_cert_def split: if_splits option.splits)
kleing@9757
   163
kleing@9757
   164
  { fix pc'
kleing@9757
   165
    assume pc': "pc' \<in> set (succs (is!pc) pc)"
kleing@9012
   166
kleing@9757
   167
    with wti
kleing@9757
   168
    have less: "pc' < length is"  
kleing@9757
   169
      by (simp add: wtl_inst_Ok)
kleing@9549
   170
kleing@9757
   171
    have "G \<turnstile> step (is!pc) G (phi!pc) <=' phi ! pc'" 
kleing@9757
   172
    proof (cases "pc' = Suc pc")
kleing@9757
   173
      case False          
kleing@9757
   174
      with wti pc'
kleing@9757
   175
      have G: "G \<turnstile> step (is ! pc) G (phi ! pc) <=' cert ! pc'" 
kleing@9757
   176
        by (simp add: wtl_inst_Ok)
kleing@9549
   177
kleing@9757
   178
      hence "cert!pc' = None ==> step (is ! pc) G (phi ! pc) = None"
kleing@9757
   179
        by simp
kleing@9757
   180
      hence "cert!pc' = None ==> ?thesis"
kleing@9757
   181
        by simp
kleing@9757
   182
kleing@9757
   183
      moreover
kleing@9757
   184
      { fix t
kleing@9757
   185
        assume "cert!pc' = Some t"
kleing@9757
   186
        with less
kleing@9757
   187
        have "phi!pc' = cert!pc'"
kleing@9757
   188
          by (simp add: cert_Some)
kleing@9757
   189
        with G
kleing@9757
   190
        have ?thesis
kleing@9757
   191
          by simp
kleing@9757
   192
      }
kleing@9012
   193
kleing@9757
   194
      ultimately
kleing@9757
   195
      show ?thesis by blast      
kleing@9757
   196
    next
kleing@9757
   197
      case True
kleing@9757
   198
      with pc' wti
kleing@9757
   199
      have "step (is ! pc) G (phi ! pc) = s''"  
kleing@9757
   200
        by (simp add: wtl_inst_Ok)
kleing@9757
   201
      also
kleing@9757
   202
      from w c fits pc wtl 
kleing@9757
   203
      have "Suc pc < length is ==> G \<turnstile> s'' <=' phi ! Suc pc"
kleing@9757
   204
        by - (drule wtl_suc_pc)
kleing@9757
   205
      with True less
kleing@9757
   206
      have "G \<turnstile> s'' <=' phi ! Suc pc" 
kleing@9757
   207
        by blast
kleing@9757
   208
      finally
kleing@9757
   209
      show ?thesis 
kleing@9757
   210
        by (simp add: True)
kleing@9757
   211
    qed
kleing@9757
   212
  }
kleing@9757
   213
  
kleing@9757
   214
  with wti
kleing@9757
   215
  show ?thesis
kleing@9757
   216
    by (auto simp add: wtl_inst_Ok wt_instr_def)
kleing@9549
   217
qed
kleing@9549
   218
kleing@9549
   219
kleing@9012
   220
    
kleing@9012
   221
lemma fits_first:
kleing@9757
   222
  "[| 0 < length is; wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err; 
kleing@9757
   223
      fits phi is G rT s cert |] ==> 
kleing@9757
   224
  G \<turnstile> s <=' phi ! 0"
kleing@9580
   225
proof -
kleing@9757
   226
  assume wtl:  "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
kleing@9757
   227
  assume fits: "fits phi is G rT s cert"
kleing@9757
   228
  assume pc:   "0 < length is"
kleing@9757
   229
kleing@9757
   230
  from wtl
kleing@9757
   231
  have wt0: "wtl_inst_list (take 0 is) G rT cert (length is) 0 s = Ok s"
kleing@9757
   232
    by simp
kleing@9549
   233
  
kleing@9757
   234
  with fits pc
kleing@9757
   235
  have "cert!0 = None ==> phi!0 = s"
kleing@9757
   236
    by (rule fitsD_None)
kleing@9757
   237
  moreover    
kleing@9757
   238
  from fits pc wt0
kleing@10042
   239
  have "!!t. cert!0 = Some t ==> phi!0 = cert!0"
kleing@9757
   240
    by - (drule fitsD_Some, auto)
kleing@9757
   241
  moreover
kleing@9757
   242
  from pc
kleing@9757
   243
  obtain x xs where "is = x#xs" 
kleing@9549
   244
    by (simp add: neq_Nil_conv) (elim, rule that)
kleing@9757
   245
  with wtl
kleing@9757
   246
  obtain s' where
kleing@9757
   247
    "wtl_cert x G rT s cert (length is) 0 = Ok s'"
kleing@9757
   248
    by simp (elim, rule that, simp)
kleing@9757
   249
  hence 
kleing@10042
   250
    "!!t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
kleing@9757
   251
    by (simp add: wtl_cert_def split: if_splits)
kleing@9012
   252
kleing@9757
   253
  ultimately
kleing@9549
   254
  show ?thesis
kleing@9757
   255
    by - (cases "cert!0", auto)
kleing@9757
   256
qed
kleing@9549
   257
kleing@8245
   258
  
kleing@9012
   259
lemma wtl_method_correct:
kleing@9757
   260
"wtl_method G C pTs rT mxl ins cert ==> \<exists> phi. wt_method G C pTs rT mxl ins phi"
kleing@9757
   261
proof (unfold wtl_method_def, simp only: Let_def, elim conjE)
kleing@9757
   262
  let "?s0" = "Some ([], Ok (Class C) # map Ok pTs @ replicate mxl Err)"
kleing@9757
   263
  assume pc:  "0 < length ins"
kleing@9757
   264
  assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \<noteq> Err"
kleing@9549
   265
kleing@9757
   266
  obtain phi where fits: "fits phi ins G rT ?s0 cert"    
wenzelm@9941
   267
    by (rule exists_phi [elim_format]) blast
kleing@9549
   268
kleing@9549
   269
  with wtl
kleing@9549
   270
  have allpc:
kleing@10042
   271
    "\<forall>pc. pc < length ins --> wt_instr (ins ! pc) G rT phi (length ins) pc"
kleing@9757
   272
    by (blast intro: wtl_fits_wt)
kleing@9549
   273
kleing@9757
   274
  from pc wtl fits
kleing@9549
   275
  have "wt_start G C pTs mxl phi"
kleing@9757
   276
    by (unfold wt_start_def) (rule fits_first)
kleing@9549
   277
kleing@9757
   278
  with pc allpc 
kleing@9549
   279
  show ?thesis by (auto simp add: wt_method_def)
kleing@9549
   280
qed
kleing@9012
   281
kleing@9012
   282
kleing@9012
   283
theorem wtl_correct:
kleing@9580
   284
"wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
kleing@9580
   285
proof (clarsimp simp add: wt_jvm_prog_def wf_prog_def, intro conjI)
kleing@9012
   286
kleing@9580
   287
  assume wtl_prog: "wtl_jvm_prog G cert"
kleing@9580
   288
  thus "ObjectC \<in> set G" by (simp add: wtl_jvm_prog_def wf_prog_def)
kleing@9012
   289
kleing@9580
   290
  from wtl_prog 
kleing@9580
   291
  show uniqueG: "unique G" by (simp add: wtl_jvm_prog_def wf_prog_def)
kleing@9012
   292
kleing@9757
   293
  show "\<exists>Phi. Ball (set G) (wf_cdecl (\<lambda>G C (sig,rT,maxl,b). 
kleing@9757
   294
              wt_method G C (snd sig) rT maxl b (Phi C sig)) G)"
kleing@9580
   295
    (is "\<exists>Phi. ?Q Phi")
kleing@9580
   296
  proof (intro exI)
kleing@9757
   297
    let "?Phi" = "\<lambda> C sig. 
kleing@10042
   298
      let (C,x,y,mdecls) = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
kleing@10042
   299
          (sig,rT,maxl,b) = SOME (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
kleing@10042
   300
      in SOME phi. wt_method G C (snd sig) rT maxl b phi"
kleing@9580
   301
    from wtl_prog
kleing@9580
   302
    show "?Q ?Phi"
kleing@9580
   303
    proof (unfold wf_cdecl_def, intro)
kleing@9580
   304
      fix x a b aa ba ab bb m
kleing@9580
   305
      assume 1: "x \<in> set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \<in> set bb"
kleing@9580
   306
      with wtl_prog
kleing@9757
   307
      show "wf_mdecl (\<lambda>G C (sig,rT,maxl,b). 
kleing@9757
   308
            wt_method G C (snd sig) rT maxl b (?Phi C sig)) G a m"
kleing@9757
   309
      proof (simp add: wf_mdecl_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def, 
kleing@9757
   310
             elim conjE)
kleing@9580
   311
        apply_end (drule bspec, assumption, simp, elim conjE)
kleing@9580
   312
        assume "\<forall>(sig,rT,mb)\<in>set bb. wf_mhead G sig rT \<and> 
kleing@9580
   313
                 (\<lambda>(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb"
kleing@9580
   314
               "unique bb"
kleing@9580
   315
        with 1 uniqueG
kleing@9580
   316
        show "(\<lambda>(sig,rT,mb).
kleing@9580
   317
          wf_mhead G sig rT \<and>
kleing@9580
   318
          (\<lambda>(maxl,b).
kleing@9012
   319
              wt_method G a (snd sig) rT maxl b 
kleing@9580
   320
               ((\<lambda>(C,x,y,mdecls).
kleing@9580
   321
                    (\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b))
kleing@10042
   322
                     (SOME (sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig))
kleing@10042
   323
                 (SOME (Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
kleing@9012
   324
          by - (drule bspec, assumption, 
kleing@9580
   325
                clarsimp dest!: wtl_method_correct,
paulson@9970
   326
                clarsimp intro!: someI simp add: unique_epsilon) 
kleing@9580
   327
      qed
kleing@9580
   328
    qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
kleing@9580
   329
  qed
kleing@9580
   330
qed
kleing@9012
   331
    
kleing@9012
   332
kleing@9580
   333
end