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