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