src/HOL/MicroJava/BV/LBVComplete.thy
author kleing
Thu Feb 21 09:54:08 2002 +0100 (2002-02-21)
changeset 12911 704713ca07ea
parent 12516 d09d0f160888
child 13006 51c5f3f11d16
permissions -rw-r--r--
new document
kleing@8388
     1
(*  Title:      HOL/MicroJava/BV/LBVComplete.thy
kleing@8388
     2
    ID:         $Id$
kleing@8388
     3
    Author:     Gerwin Klein
kleing@8388
     4
    Copyright   2000 Technische Universitaet Muenchen
kleing@9054
     5
*)
kleing@8388
     6
kleing@12911
     7
header {* \isaheader{Completeness of the LBV} *}
kleing@8388
     8
kleing@12516
     9
(* This theory is currently broken. The port to exceptions
kleing@12516
    10
  didn't make it into the Isabelle 2001 release. It is included for 
kleing@12516
    11
  documentation only. See Isabelle 99-2 for a working copy of this
kleing@12516
    12
  theory. *)
kleing@12516
    13
kleing@12516
    14
theory LBVComplete = BVSpec + LBVSpec + EffectMono:
kleing@9549
    15
kleing@8388
    16
constdefs
kleing@10042
    17
  contains_targets :: "[instr list, certificate, method_type, p_count] => bool"
kleing@10042
    18
  "contains_targets ins cert phi pc == 
kleing@9757
    19
     \<forall>pc' \<in> set (succs (ins!pc) pc). 
kleing@10042
    20
      pc' \<noteq> pc+1 \<and> pc' < length ins --> cert!pc' = phi!pc'"
kleing@8388
    21
kleing@10042
    22
  fits :: "[instr list, certificate, method_type] => bool"
kleing@10042
    23
  "fits ins cert phi == \<forall>pc. pc < length ins --> 
kleing@9757
    24
                       contains_targets ins cert phi pc \<and>
kleing@9757
    25
                       (cert!pc = None \<or> cert!pc = phi!pc)"
kleing@9012
    26
kleing@10042
    27
  is_target :: "[instr list, p_count] => bool" 
kleing@10042
    28
  "is_target ins pc == 
kleing@9757
    29
     \<exists>pc'. pc \<noteq> pc'+1 \<and> pc' < length ins \<and> pc \<in> set (succs (ins!pc') pc')"
kleing@8388
    30
kleing@8388
    31
kleing@8388
    32
constdefs 
kleing@10042
    33
  make_cert :: "[instr list, method_type] => certificate"
kleing@10042
    34
  "make_cert ins phi == 
kleing@9757
    35
     map (\<lambda>pc. if is_target ins pc then phi!pc else None) [0..length ins(]"
kleing@9757
    36
kleing@10042
    37
  make_Cert :: "[jvm_prog, prog_type] => prog_certificate"
kleing@10628
    38
  "make_Cert G Phi ==  \<lambda> C sig. let (C,rT,(maxs,maxl,b)) = the (method (G,C) sig)
kleing@10628
    39
                                in make_cert b (Phi C sig)"
kleing@8388
    40
  
kleing@9559
    41
lemmas [simp del] = split_paired_Ex
kleing@9559
    42
kleing@9757
    43
lemma make_cert_target:
kleing@9757
    44
  "[| pc < length ins; is_target ins pc |] ==> make_cert ins phi ! pc = phi!pc"
kleing@9757
    45
  by (simp add: make_cert_def)
kleing@9012
    46
kleing@9757
    47
lemma make_cert_approx:
kleing@9757
    48
  "[| pc < length ins; make_cert ins phi ! pc \<noteq> phi ! pc |] ==> 
kleing@9757
    49
   make_cert ins phi ! pc = None"
kleing@9757
    50
  by (auto simp add: make_cert_def)
kleing@9012
    51
kleing@9757
    52
lemma make_cert_contains_targets:
kleing@9757
    53
  "pc < length ins ==> contains_targets ins (make_cert ins phi) phi pc"
kleing@11085
    54
proof (unfold contains_targets_def, intro strip, elim conjE) 
kleing@9549
    55
  fix pc'
kleing@9549
    56
  assume "pc < length ins" 
kleing@9757
    57
         "pc' \<in> set (succs (ins ! pc) pc)" 
kleing@9757
    58
         "pc' \<noteq> pc+1" and
kleing@9757
    59
    pc': "pc' < length ins"
kleing@9549
    60
kleing@9757
    61
  hence "is_target ins pc'" 
kleing@9757
    62
    by (auto simp add: is_target_def)
kleing@9549
    63
kleing@9549
    64
  with pc'
kleing@9757
    65
  show "make_cert ins phi ! pc' = phi ! pc'" 
kleing@9757
    66
    by (auto intro: make_cert_target)
kleing@9549
    67
qed
kleing@9012
    68
kleing@9757
    69
theorem fits_make_cert:
kleing@9757
    70
  "fits ins (make_cert ins phi) phi"
kleing@9757
    71
  by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets)
kleing@9549
    72
kleing@9549
    73
lemma fitsD: 
kleing@9757
    74
  "[| fits ins cert phi; pc' \<in> set (succs (ins!pc) pc); 
kleing@9757
    75
      pc' \<noteq> Suc pc; pc < length ins; pc' < length ins |]
kleing@9757
    76
  ==> cert!pc' = phi!pc'"
kleing@9757
    77
  by (clarsimp simp add: fits_def contains_targets_def)
kleing@9549
    78
kleing@9549
    79
lemma fitsD2:
kleing@9757
    80
   "[| fits ins cert phi; pc < length ins; cert!pc = Some s |]
kleing@9757
    81
  ==> cert!pc = phi!pc"
kleing@9757
    82
  by (auto simp add: fits_def)
kleing@9757
    83
                           
kleing@9549
    84
lemma wtl_inst_mono:
kleing@10592
    85
  "[| wtl_inst i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; 
kleing@9757
    86
      pc < length ins;  G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
kleing@10592
    87
  \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
kleing@9549
    88
proof -
kleing@9549
    89
  assume pc:   "pc < length ins" "i = ins!pc"
kleing@10592
    90
  assume wtl:  "wtl_inst i G rT s1 cert mxs mpc pc = OK s1'"
kleing@9549
    91
  assume fits: "fits ins cert phi"
kleing@9757
    92
  assume G:    "G \<turnstile> s2 <=' s1"
kleing@9549
    93
  
kleing@12516
    94
  let "?eff s" = "eff i G s"
kleing@9012
    95
kleing@9549
    96
  from wtl G
kleing@10592
    97
  have app: "app i G mxs rT s2" by (auto simp add: wtl_inst_OK app_mono)
kleing@9549
    98
  
kleing@9549
    99
  from wtl G
kleing@12516
   100
  have eff: "G \<turnstile> ?eff s2 <=' ?eff s1" 
kleing@12516
   101
    by (auto intro: eff_mono simp add: wtl_inst_OK)
kleing@9012
   102
kleing@10496
   103
  { also
kleing@9549
   104
    fix pc'
kleing@10496
   105
    assume "pc' \<in> set (succs i pc)" "pc' \<noteq> pc+1"
kleing@10496
   106
    with wtl 
kleing@12516
   107
    have "G \<turnstile> ?eff s1 <=' cert!pc'"
kleing@10496
   108
      by (auto simp add: wtl_inst_OK) 
kleing@9549
   109
    finally
kleing@12516
   110
    have "G\<turnstile> ?eff s2 <=' cert!pc'" .
kleing@9549
   111
  } note cert = this
kleing@9549
   112
    
kleing@10592
   113
  have "\<exists>s2'. wtl_inst i G rT s2 cert mxs mpc pc = OK s2' \<and> G \<turnstile> s2' <=' s1'"
kleing@9757
   114
  proof (cases "pc+1 \<in> set (succs i pc)")
kleing@9549
   115
    case True
kleing@9549
   116
    with wtl
kleing@12516
   117
    have s1': "s1' = ?eff s1" by (simp add: wtl_inst_OK)
kleing@9012
   118
kleing@12516
   119
    have "wtl_inst i G rT s2 cert mxs mpc pc = OK (?eff s2) \<and> G \<turnstile> ?eff s2 <=' s1'" 
kleing@9580
   120
      (is "?wtl \<and> ?G")
kleing@9549
   121
    proof
kleing@9549
   122
      from True s1'
kleing@12516
   123
      show ?G by (auto intro: eff)
kleing@9549
   124
kleing@9549
   125
      from True app wtl
kleing@9549
   126
      show ?wtl
kleing@10496
   127
        by (clarsimp intro!: cert simp add: wtl_inst_OK)
kleing@9376
   128
    qed
kleing@9549
   129
    thus ?thesis by blast
kleing@9376
   130
  next
kleing@9549
   131
    case False
kleing@9549
   132
    with wtl
kleing@10496
   133
    have "s1' = cert ! Suc pc" by (simp add: wtl_inst_OK)
kleing@9012
   134
kleing@9549
   135
    with False app wtl
kleing@10592
   136
    have "wtl_inst i G rT s2 cert mxs mpc pc = OK s1' \<and> G \<turnstile> s1' <=' s1'"
kleing@10496
   137
      by (clarsimp intro!: cert simp add: wtl_inst_OK)
kleing@9549
   138
kleing@9549
   139
    thus ?thesis by blast
kleing@9549
   140
  qed
kleing@9012
   141
  
kleing@9549
   142
  with pc show ?thesis by simp
kleing@9376
   143
qed
kleing@9757
   144
kleing@9559
   145
kleing@9757
   146
lemma wtl_cert_mono:
kleing@10592
   147
  "[| wtl_cert i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; 
kleing@9757
   148
      pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
kleing@10592
   149
  \<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
kleing@9559
   150
proof -
kleing@10592
   151
  assume wtl:  "wtl_cert i G rT s1 cert mxs mpc pc = OK s1'" and
kleing@9559
   152
         fits: "fits ins cert phi" "pc < length ins"
kleing@9757
   153
               "G \<turnstile> s2 <=' s1" "i = ins!pc"
kleing@9559
   154
kleing@9559
   155
  show ?thesis
wenzelm@9664
   156
  proof (cases (open) "cert!pc")
kleing@9559
   157
    case None
kleing@9580
   158
    with wtl fits
kleing@9580
   159
    show ?thesis 
wenzelm@9941
   160
      by - (rule wtl_inst_mono [elim_format], (simp add: wtl_cert_def)+)
kleing@9559
   161
  next
kleing@9559
   162
    case Some
kleing@9580
   163
    with wtl fits
kleing@9559
   164
kleing@9757
   165
    have G: "G \<turnstile> s2 <=' (Some a)"
kleing@9757
   166
      by - (rule sup_state_opt_trans, auto simp add: wtl_cert_def split: if_splits)
kleing@9559
   167
kleing@9559
   168
    from Some wtl
kleing@10592
   169
    have "wtl_inst i G rT (Some a) cert mxs mpc pc = OK s1'" 
kleing@9757
   170
      by (simp add: wtl_cert_def split: if_splits)
kleing@9559
   171
kleing@9559
   172
    with G fits
kleing@10592
   173
    have "\<exists> s2'. wtl_inst (ins!pc) G rT (Some a) cert mxs mpc pc = OK s2' \<and> 
kleing@9757
   174
                 (G \<turnstile> s2' <=' s1')"
kleing@9757
   175
      by - (rule wtl_inst_mono, (simp add: wtl_cert_def)+)
kleing@9559
   176
    
kleing@9580
   177
    with Some G
kleing@9757
   178
    show ?thesis by (simp add: wtl_cert_def)
kleing@9559
   179
  qed
kleing@9559
   180
qed
kleing@9559
   181
kleing@9757
   182
 
kleing@9012
   183
lemma wt_instr_imp_wtl_inst:
kleing@10592
   184
  "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
kleing@9757
   185
      pc < length ins; length ins = max_pc |] ==> 
kleing@10592
   186
  wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
kleing@9757
   187
 proof -
kleing@10592
   188
  assume wt:   "wt_instr (ins!pc) G rT phi mxs max_pc pc" 
kleing@9549
   189
  assume fits: "fits ins cert phi"
kleing@9549
   190
  assume pc:   "pc < length ins" "length ins = max_pc"
kleing@9549
   191
kleing@9549
   192
  from wt 
kleing@10592
   193
  have app: "app (ins!pc) G mxs rT (phi!pc)" by (simp add: wt_instr_def)
kleing@9549
   194
kleing@9549
   195
  from wt pc
kleing@10042
   196
  have pc': "!!pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
kleing@9549
   197
    by (simp add: wt_instr_def)
kleing@9376
   198
kleing@12516
   199
  let ?s' = "eff (ins!pc) G (phi!pc)"
kleing@9549
   200
kleing@9549
   201
  from wt fits pc
kleing@10042
   202
  have cert: "!!pc'. [|pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1|] 
kleing@10042
   203
    ==> G \<turnstile> ?s' <=' cert!pc'"
kleing@9757
   204
    by (auto dest: fitsD simp add: wt_instr_def)     
kleing@9549
   205
kleing@9757
   206
  from app pc cert pc'
kleing@9757
   207
  show ?thesis
kleing@10496
   208
    by (auto simp add: wtl_inst_OK)
kleing@9376
   209
qed
kleing@9012
   210
kleing@9757
   211
lemma wt_less_wtl:
kleing@10592
   212
  "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; 
kleing@10592
   213
      wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s;
kleing@9757
   214
      fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> 
kleing@9757
   215
  G \<turnstile> s <=' phi ! Suc pc"
kleing@9376
   216
proof -
kleing@10592
   217
  assume wt:   "wt_instr (ins!pc) G rT phi mxs max_pc pc" 
kleing@10592
   218
  assume wtl:  "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s"
kleing@9757
   219
  assume fits: "fits ins cert phi"
kleing@9757
   220
  assume pc:   "Suc pc < length ins" "length ins = max_pc"
kleing@9757
   221
kleing@9757
   222
  { assume suc: "Suc pc \<in> set (succs (ins ! pc) pc)"
kleing@12516
   223
    with wtl have "s = eff (ins!pc) G (phi!pc)"
kleing@10496
   224
      by (simp add: wtl_inst_OK)
kleing@9757
   225
    also from suc wt have "G \<turnstile> ... <=' phi!Suc pc"
kleing@9757
   226
      by (simp add: wt_instr_def)
kleing@9757
   227
    finally have ?thesis .
kleing@9757
   228
  }
kleing@9012
   229
kleing@9757
   230
  moreover
kleing@9757
   231
  { assume "Suc pc \<notin> set (succs (ins ! pc) pc)"
kleing@9757
   232
    
kleing@9757
   233
    with wtl
kleing@9757
   234
    have "s = cert!Suc pc" 
kleing@10496
   235
      by (simp add: wtl_inst_OK)
kleing@9757
   236
    with fits pc
kleing@9757
   237
    have ?thesis
kleing@9757
   238
      by - (cases "cert!Suc pc", simp, drule fitsD2, assumption+, simp)
kleing@9757
   239
  }
kleing@9757
   240
kleing@9757
   241
  ultimately
kleing@9757
   242
  show ?thesis by blast
kleing@9757
   243
qed
kleing@9757
   244
  
kleing@9757
   245
kleing@9757
   246
lemma wt_instr_imp_wtl_cert:
kleing@10592
   247
  "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
kleing@9757
   248
      pc < length ins; length ins = max_pc |] ==> 
kleing@10592
   249
  wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
kleing@9757
   250
proof -
kleing@10592
   251
  assume "wt_instr (ins!pc) G rT phi mxs max_pc pc" and 
kleing@9757
   252
   fits: "fits ins cert phi" and
kleing@9757
   253
     pc: "pc < length ins" and
kleing@9757
   254
         "length ins = max_pc"
kleing@9012
   255
  
kleing@10592
   256
  hence wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
kleing@9757
   257
    by (rule wt_instr_imp_wtl_inst)
kleing@9757
   258
kleing@9757
   259
  hence "cert!pc = None ==> ?thesis"
kleing@9757
   260
    by (simp add: wtl_cert_def)
kleing@9012
   261
kleing@9757
   262
  moreover
kleing@9757
   263
  { fix s
kleing@9757
   264
    assume c: "cert!pc = Some s"
kleing@9757
   265
    with fits pc
kleing@9757
   266
    have "cert!pc = phi!pc"
kleing@9757
   267
      by (rule fitsD2)
kleing@9757
   268
    from this c wtl
kleing@9757
   269
    have ?thesis
kleing@9757
   270
      by (clarsimp simp add: wtl_cert_def)
kleing@9757
   271
  }
kleing@9757
   272
kleing@9757
   273
  ultimately
kleing@9757
   274
  show ?thesis by blast
kleing@9757
   275
qed
kleing@9757
   276
  
kleing@9012
   277
kleing@9757
   278
lemma wt_less_wtl_cert:
kleing@10592
   279
  "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; 
kleing@10592
   280
      wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s;
kleing@9757
   281
      fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> 
kleing@9757
   282
  G \<turnstile> s <=' phi ! Suc pc"
kleing@9757
   283
proof -
kleing@10592
   284
  assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s"
kleing@9757
   285
kleing@10592
   286
  assume wti: "wt_instr (ins!pc) G rT phi mxs max_pc pc"
kleing@9757
   287
              "fits ins cert phi" 
kleing@9757
   288
              "Suc pc < length ins" "length ins = max_pc"
kleing@9757
   289
  
kleing@9757
   290
  { assume "cert!pc = None"
kleing@9757
   291
    with wtl
kleing@10592
   292
    have "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s"
kleing@9757
   293
      by (simp add: wtl_cert_def)
kleing@9757
   294
    with wti
kleing@9757
   295
    have ?thesis
kleing@9757
   296
      by - (rule wt_less_wtl)
kleing@9757
   297
  }
kleing@9757
   298
  moreover
kleing@9757
   299
  { fix t
kleing@9757
   300
    assume c: "cert!pc = Some t"
kleing@9757
   301
    with wti
kleing@9757
   302
    have "cert!pc = phi!pc"
kleing@9757
   303
      by - (rule fitsD2, simp+)
kleing@9757
   304
    with c wtl
kleing@10592
   305
    have "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s"
kleing@9757
   306
      by (simp add: wtl_cert_def)
kleing@9757
   307
    with wti
kleing@9757
   308
    have ?thesis
kleing@9757
   309
      by - (rule wt_less_wtl)
kleing@9757
   310
  }   
kleing@9757
   311
    
kleing@9757
   312
  ultimately
kleing@9757
   313
  show ?thesis by blast
kleing@9549
   314
qed
kleing@9012
   315
kleing@9559
   316
text {*
kleing@9559
   317
  \medskip
kleing@9559
   318
  Main induction over the instruction list.
kleing@9559
   319
*}
kleing@9012
   320
kleing@9012
   321
theorem wt_imp_wtl_inst_list:
kleing@10042
   322
"\<forall> pc. (\<forall>pc'. pc' < length all_ins --> 
kleing@10592
   323
        wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc') -->
kleing@10042
   324
       fits all_ins cert phi --> 
kleing@10042
   325
       (\<exists>l. pc = length l \<and> all_ins = l@ins) -->  
kleing@10042
   326
       pc < length all_ins -->      
kleing@10042
   327
       (\<forall> s. (G \<turnstile> s <=' (phi!pc)) --> 
kleing@10592
   328
             wtl_inst_list ins G rT cert mxs (length all_ins) pc s \<noteq> Err)" 
kleing@10042
   329
(is "\<forall>pc. ?wt --> ?fits --> ?l pc ins --> ?len pc --> ?wtl pc ins"  
kleing@9757
   330
 is "\<forall>pc. ?C pc ins" is "?P ins") 
kleing@9559
   331
proof (induct "?P" "ins")
kleing@9559
   332
  case Nil
kleing@9559
   333
  show "?P []" by simp
kleing@9559
   334
next
kleing@9559
   335
  fix i ins'
kleing@9559
   336
  assume Cons: "?P ins'"
kleing@9012
   337
kleing@9559
   338
  show "?P (i#ins')" 
kleing@9559
   339
  proof (intro allI impI, elim exE conjE)
kleing@9559
   340
    fix pc s l
kleing@10042
   341
    assume wt  : "\<forall>pc'. pc' < length all_ins --> 
kleing@10592
   342
                        wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc'"
kleing@9559
   343
    assume fits: "fits all_ins cert phi"
kleing@9559
   344
    assume l   : "pc < length all_ins"
kleing@9757
   345
    assume G   : "G \<turnstile> s <=' phi ! pc"
kleing@9559
   346
    assume pc  : "all_ins = l@i#ins'" "pc = length l"
kleing@9559
   347
    hence  i   : "all_ins ! pc = i"
kleing@9559
   348
      by (simp add: nth_append)
kleing@9012
   349
kleing@9559
   350
    from l wt
kleing@10592
   351
    have wti: "wt_instr (all_ins!pc) G rT phi mxs (length all_ins) pc" by blast
kleing@9012
   352
kleing@9559
   353
    with fits l 
kleing@10592
   354
    have c: "wtl_cert (all_ins!pc) G rT (phi!pc) cert mxs (length all_ins) pc \<noteq> Err"
kleing@9757
   355
      by - (drule wt_instr_imp_wtl_cert, auto)
kleing@9559
   356
    
kleing@9559
   357
    from Cons
kleing@9559
   358
    have "?C (Suc pc) ins'" by blast
kleing@9559
   359
    with wt fits pc
kleing@10042
   360
    have IH: "?len (Suc pc) --> ?wtl (Suc pc) ins'" by auto
kleing@9012
   361
kleing@10592
   362
    show "wtl_inst_list (i#ins') G rT cert mxs (length all_ins) pc s \<noteq> Err" 
kleing@9559
   363
    proof (cases "?len (Suc pc)")
kleing@9559
   364
      case False
kleing@9559
   365
      with pc
kleing@9559
   366
      have "ins' = []" by simp
kleing@9757
   367
      with G i c fits l
kleing@9757
   368
      show ?thesis by (auto dest: wtl_cert_mono)
kleing@9559
   369
    next
kleing@9559
   370
      case True
kleing@9559
   371
      with IH
kleing@9757
   372
      have wtl: "?wtl (Suc pc) ins'" by blast
kleing@9757
   373
kleing@9757
   374
      from c wti fits l True
kleing@9757
   375
      obtain s'' where
kleing@10592
   376
        "wtl_cert (all_ins!pc) G rT (phi!pc) cert mxs (length all_ins) pc = OK s''"
kleing@9757
   377
        "G \<turnstile> s'' <=' phi ! Suc pc"
kleing@9757
   378
        by clarsimp (drule wt_less_wtl_cert, auto)
kleing@9757
   379
      moreover
kleing@9757
   380
      from calculation fits G l
kleing@9559
   381
      obtain s' where
kleing@10592
   382
        c': "wtl_cert (all_ins!pc) G rT s cert mxs (length all_ins) pc = OK s'" and
kleing@9757
   383
        "G \<turnstile> s' <=' s''"
kleing@9757
   384
        by - (drule wtl_cert_mono, auto)
kleing@9757
   385
      ultimately
kleing@9757
   386
      have G': "G \<turnstile> s' <=' phi ! Suc pc" 
kleing@9757
   387
        by - (rule sup_state_opt_trans)
kleing@9757
   388
kleing@9757
   389
      with wtl
kleing@10592
   390
      have "wtl_inst_list ins' G rT cert mxs (length all_ins) (Suc pc) s' \<noteq> Err"
kleing@9757
   391
        by auto
kleing@9757
   392
kleing@9757
   393
      with i c'
kleing@9559
   394
      show ?thesis by auto
kleing@9549
   395
    qed
kleing@9549
   396
  qed
kleing@9549
   397
qed
kleing@9559
   398
  
kleing@9012
   399
kleing@9012
   400
lemma fits_imp_wtl_method_complete:
kleing@10592
   401
  "[| wt_method G C pTs rT mxs mxl ins phi; fits ins cert phi |] 
kleing@10592
   402
  ==> wtl_method G C pTs rT mxs mxl ins cert"
kleing@9594
   403
by (simp add: wt_method_def wtl_method_def)
wenzelm@9941
   404
   (rule wt_imp_wtl_inst_list [rule_format, elim_format], auto simp add: wt_start_def) 
kleing@9012
   405
kleing@9012
   406
kleing@9012
   407
lemma wtl_method_complete:
kleing@10592
   408
  "wt_method G C pTs rT mxs mxl ins phi 
kleing@10592
   409
  ==> wtl_method G C pTs rT mxs mxl ins (make_cert ins phi)"
kleing@9580
   410
proof -
kleing@10592
   411
  assume "wt_method G C pTs rT mxs mxl ins phi" 
kleing@9757
   412
  moreover
kleing@9757
   413
  have "fits ins (make_cert ins phi) phi"
kleing@9757
   414
    by (rule fits_make_cert)
kleing@9757
   415
  ultimately
kleing@9757
   416
  show ?thesis 
kleing@9757
   417
    by (rule fits_imp_wtl_method_complete)
kleing@9580
   418
qed
kleing@9012
   419
kleing@9012
   420
kleing@10628
   421
theorem wtl_complete:
kleing@9757
   422
  "wt_jvm_prog G Phi ==> wtl_jvm_prog G (make_Cert G Phi)"
kleing@10628
   423
proof -
kleing@10628
   424
  assume wt: "wt_jvm_prog G Phi"
kleing@10628
   425
   
kleing@10628
   426
  { fix C S fs mdecls sig rT code
kleing@10628
   427
    assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls"
kleing@10628
   428
    moreover
kleing@10628
   429
    from wt obtain wf_mb where "wf_prog wf_mb G" 
kleing@10628
   430
      by (blast dest: wt_jvm_progD)
kleing@10628
   431
    ultimately
kleing@10628
   432
    have "method (G,C) sig = Some (C,rT,code)"
kleing@10628
   433
      by (simp add: methd)
kleing@10628
   434
  } note this [simp]
kleing@10628
   435
 
kleing@10628
   436
  from wt
kleing@10628
   437
  show ?thesis
kleing@10628
   438
    apply (clarsimp simp add: wt_jvm_prog_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
kleing@10628
   439
    apply (drule bspec, assumption)
kleing@10628
   440
    apply (clarsimp simp add: wf_mdecl_def)
kleing@10628
   441
    apply (drule bspec, assumption)
kleing@10628
   442
    apply (clarsimp simp add: make_Cert_def)
kleing@10628
   443
    apply (clarsimp dest!: wtl_method_complete)    
kleing@10628
   444
    done
kleing@10592
   445
kleing@10628
   446
qed   
kleing@10628
   447
      
kleing@9559
   448
lemmas [simp] = split_paired_Ex
kleing@9549
   449
kleing@9549
   450
end