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