src/HOL/MicroJava/BV/LBVComplete.thy
author kleing
Wed Mar 27 20:44:53 2002 +0100 (2002-03-27)
changeset 13071 f538a1dba7ee
parent 13070 fcfdefa4617b
child 13074 96bf406fd3e5
permissions -rw-r--r--
finished lbv completeness
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@13071
    27
     map (\<lambda>pc. if is_target step phi pc then phi!pc else None) [0..length phi(] @ [None]"
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@13071
    34
  by (simp add: make_cert_def nth_append)
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@13071
    39
  by (auto simp add: make_cert_def nth_append)
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@13071
    59
  "\<lbrakk> fits step cert phi; (pc',s') \<in> set (step pc (OK (phi!pc)));
kleing@13071
    60
      pc' \<noteq> pc+1; 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 wtl_inst_mono:
kleing@13064
   155
  assumes wtl:  "wtl_inst cert f r step pc s1 = OK s1'"
kleing@13071
   156
  assumes less: "OK s2 \<le>|r (OK s1)"
kleing@13064
   157
  assumes pc:   "pc < n" 
kleing@13071
   158
  assumes s1:   "s1 \<in> opt A"
kleing@13071
   159
  assumes s2:   "s2 \<in> opt A"
kleing@13071
   160
  assumes esl:  "err_semilat (A,r,f)"
kleing@13071
   161
  assumes cert: "cert_ok cert n A"
kleing@13071
   162
  assumes mono: "mono (Err.le (Opt.le r)) step n (err (opt A))"
kleing@13071
   163
  assumes pres: "pres_type step n (err (opt A))" 
kleing@13064
   164
  shows "\<exists>s2'. wtl_inst cert f r step pc s2 = OK s2' \<and> OK s2' \<le>|r (OK s1')"
kleing@9549
   165
proof -
kleing@13071
   166
  let "?step s1" = "step pc (OK s1)"
kleing@13071
   167
  let ?cert = "OK (cert!Suc pc)"
kleing@13071
   168
  from wtl 
kleing@13071
   169
  have "merge cert f r pc (?step s1) ?cert = OK s1'" by (simp add: wtl_inst_def)
kleing@13071
   170
  moreover
kleing@13071
   171
  have s2: "OK s2 \<in> err (opt A)" by simp
kleing@13071
   172
  with mono have "?step s2 <=|Err.le (Opt.le r)| ?step s1" by - (rule monoD)
kleing@13071
   173
  moreover note esl
kleing@13071
   174
  moreover
kleing@13071
   175
  from pc cert have "?cert \<in> err (opt A)" by (simp add: cert_okD3)
kleing@13071
   176
  moreover
kleing@13071
   177
  have s1: "OK s1 \<in> err (opt A)" by simp
kleing@13071
   178
  with pres pc
kleing@13071
   179
  have "\<forall>(pc', s')\<in>set (?step s1). s' \<in> err (opt A)"
kleing@13071
   180
    by (blast intro: pres_typeD)  
kleing@13071
   181
  moreover
kleing@13071
   182
  from pres s2 pc
kleing@13071
   183
  have "\<forall>(pc', s')\<in>set (?step s2). s' \<in> err (opt A)" 
kleing@13071
   184
    by (blast intro: pres_typeD)  
kleing@13071
   185
  ultimately
kleing@13071
   186
  obtain s2' where "merge cert f r pc (?step s2) ?cert = s2' \<and> s2' \<le>|r (OK s1')"
kleing@13071
   187
    by (blast dest: merge_mono)
kleing@13071
   188
  thus ?thesis by (simp add: wtl_inst_def)
kleing@13071
   189
qed 
kleing@9012
   190
kleing@13071
   191
lemma wtl_cert_mono:
kleing@13071
   192
  assumes wtl:  "wtl_cert cert f r step pc s1 = OK s1'"
kleing@13071
   193
  assumes less: "OK s2 \<le>|r (OK s1)"
kleing@13071
   194
  assumes pc:   "pc < n" 
kleing@13071
   195
  assumes s1:   "s1 \<in> opt A"
kleing@13071
   196
  assumes s2:   "s2 \<in> opt A"
kleing@13071
   197
  assumes esl:  "err_semilat (A,r,f)"
kleing@13071
   198
  assumes cert: "cert_ok cert n A"
kleing@13071
   199
  assumes mono: "mono (Err.le (Opt.le r)) step n (err (opt A))"
kleing@13071
   200
  assumes pres: "pres_type step n (err (opt A))" 
kleing@13071
   201
  shows "\<exists>s2'. wtl_cert cert f r step pc s2 = OK s2' \<and> OK s2' \<le>|r (OK s1')"
kleing@13071
   202
proof (cases "cert!pc")
kleing@13071
   203
  case None
kleing@13071
   204
  with wtl have "wtl_inst cert f r step pc s1 = OK s1'" 
kleing@13071
   205
    by (simp add: wtl_cert_def)
kleing@13071
   206
  hence "\<exists>s2'. wtl_inst cert f r step pc s2 = OK s2' \<and> OK s2' \<le>|r (OK s1')"
kleing@13071
   207
    by - (rule wtl_inst_mono)
kleing@13071
   208
  with None show ?thesis by (simp add: wtl_cert_def)
kleing@13071
   209
next
kleing@13071
   210
  case (Some s')
kleing@13071
   211
  with wtl obtain 
kleing@13071
   212
    wti: "wtl_inst cert f r step pc (Some s') = OK s1'" and
kleing@13071
   213
    s':  "OK s1 \<le>|r OK (Some s')"
kleing@13071
   214
    by (auto simp add: wtl_cert_def split: split_if_asm)
kleing@13071
   215
  from esl have order: "order (Opt.le r)" by simp
kleing@13071
   216
  hence "order (Err.le (Opt.le r))" by simp
kleing@13071
   217
  with less s' have "OK s2 \<le>|r OK (Some s')" by - (drule order_trans)
kleing@13071
   218
  with Some wti order show ?thesis by (simp add: wtl_cert_def)
kleing@9376
   219
qed
kleing@9757
   220
kleing@9559
   221
kleing@13071
   222
lemma stable_wtl:
kleing@13071
   223
  assumes stable:  "stable (Err.le (Opt.le r)) step (map OK phi) pc"
kleing@13071
   224
  assumes fits:    "fits step cert phi"  
kleing@13071
   225
  assumes pc:      "pc < length phi"
kleing@13071
   226
  assumes bounded: "bounded step (length phi)"
kleing@13071
   227
  assumes esl:     "err_semilat (A, r, f)"
kleing@13071
   228
  assumes cert_ok: "cert_ok cert (length phi) A"
kleing@13071
   229
  assumes phi_ok:  "\<forall>pc < length phi. phi!pc \<in> opt A"
kleing@13071
   230
  assumes pres:    "pres_type step (length phi) (err (opt A))" 
kleing@13071
   231
  shows "wtl_inst cert f r step pc (phi!pc) \<noteq> Err"
kleing@9559
   232
proof -
kleing@13071
   233
  from esl have order: "order (Opt.le r)" by simp
kleing@9559
   234
kleing@13071
   235
  let ?step = "step pc (OK (phi!pc))"
kleing@13071
   236
  from pc have [simp]: "map OK phi ! pc = OK (phi!pc)" by simp
kleing@13071
   237
  from stable 
kleing@13071
   238
  have less: "\<forall>(q,s')\<in>set ?step. s' \<le>|r (map OK phi!q)" 
kleing@13071
   239
    by (simp add: stable_def)
kleing@13071
   240
  
kleing@13071
   241
  from cert_ok pc
kleing@13071
   242
  have cert_suc: "OK (cert!Suc pc) \<in> err (opt A)" by (auto dest: cert_okD3)
kleing@13071
   243
  moreover  
kleing@13071
   244
  from phi_ok pc
kleing@13071
   245
  have "OK (phi!pc) \<in> err (opt A)" by simp
kleing@13071
   246
  with pres pc 
kleing@13071
   247
  have stepA: "\<forall>(pc',s') \<in> set ?step. s' \<in> err (opt A)" 
kleing@13071
   248
    by (blast dest: pres_typeD)
kleing@13071
   249
  ultimately
kleing@13071
   250
  have "merge cert f r pc ?step (OK (cert!Suc pc)) =
kleing@13071
   251
    (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))
kleing@13071
   252
    then map snd [(p',t')\<in>?step.p'=pc+1] ++|f (OK (cert!Suc pc))
kleing@13071
   253
    else Err)" using esl by - (rule merge_def)
kleing@13071
   254
  moreover {
kleing@13071
   255
    fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
kleing@13071
   256
    from bounded pc s' have pc': "pc' < length phi" by (rule boundedD)
kleing@13071
   257
    hence [simp]: "map OK phi ! pc' = OK (phi!pc')" by simp
kleing@13071
   258
    with s' less have "s' \<le>|r OK (phi!pc')" by auto
kleing@13071
   259
    also from fits s' suc_pc pc pc' 
kleing@13071
   260
    have "cert!pc' = phi!pc'" by (rule fitsD)
kleing@13071
   261
    hence "phi!pc' = cert!pc'" ..
kleing@13071
   262
    finally have "s' \<le>|r (OK (cert!pc'))" .
kleing@13071
   263
  } hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))" by auto
kleing@13071
   264
  moreover
kleing@13071
   265
  from pc have "Suc pc = length phi \<or> Suc pc < length phi" by auto
kleing@13071
   266
  hence "(map snd [(p',t')\<in>?step.p'=pc+1] ++|f (OK (cert!Suc pc))) \<noteq> Err" 
kleing@13071
   267
         (is "(?map ++|f _) \<noteq> _")
kleing@13071
   268
  proof (rule disjE)
kleing@13071
   269
    assume pc': "Suc pc = length phi"
kleing@13071
   270
    with cert_ok have "cert!Suc pc = None" by (simp add: cert_okD2)
kleing@13071
   271
    moreover 
kleing@13071
   272
    from pc' bounded pc
kleing@13071
   273
    have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto)
kleing@13071
   274
    hence "[(p',t')\<in>?step.p'=pc+1] = []" by (blast intro: filter_False) 
kleing@13071
   275
    hence "?map = []" by simp
kleing@13071
   276
    ultimately show ?thesis by simp
kleing@13071
   277
  next
kleing@13071
   278
    assume pc': "Suc pc < length phi"
kleing@13071
   279
    hence [simp]: "map OK phi ! Suc pc = OK (phi!Suc pc)" by simp
kleing@13071
   280
    from esl
kleing@13071
   281
    have "semilat (err (opt A), Err.le (Opt.le r), lift2 (Opt.sup f))"
kleing@13071
   282
      by (simp add: Err.sl_def)
kleing@13071
   283
    moreover
kleing@13071
   284
    from pc' phi_ok 
kleing@13071
   285
    have "OK (phi!Suc pc) \<in> err (opt A)" by simp
kleing@13071
   286
    moreover note cert_suc
kleing@13071
   287
    moreover from stepA 
kleing@13071
   288
    have "snd`(set ?step) \<subseteq> err (opt A)" by auto
kleing@13071
   289
    hence "set ?map \<subseteq> err (opt A)" by auto
kleing@13071
   290
    moreover
kleing@13071
   291
    have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto
kleing@13071
   292
    with less have "\<forall>s' \<in> set ?map. s' \<le>|r OK (phi!Suc pc)" by auto
kleing@13071
   293
    moreover
kleing@13071
   294
    from order fits pc' 
kleing@13071
   295
    have "OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)"     
kleing@13071
   296
      by (cases "cert!Suc pc") (simp, blast dest: fitsD2) 
kleing@13071
   297
    ultimately
kleing@13071
   298
    have "?map ++|f OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)" by (rule lub)
kleing@13071
   299
    thus ?thesis by auto
kleing@9559
   300
  qed
kleing@13071
   301
  ultimately
kleing@13071
   302
  have "merge cert f r pc ?step (OK (cert!Suc pc)) \<noteq> Err" by simp
kleing@13071
   303
  thus ?thesis by (simp add: wtl_inst_def)  
kleing@9376
   304
qed
kleing@9012
   305
kleing@13071
   306
lemma stable_cert:
kleing@13071
   307
  assumes stable:  "stable (Err.le (Opt.le r)) step (map OK phi) pc"
kleing@13071
   308
  assumes fits:    "fits step cert phi"  
kleing@13071
   309
  assumes pc:      "pc < length phi"
kleing@13071
   310
  assumes bounded: "bounded step (length phi)"
kleing@13071
   311
  assumes esl:     "err_semilat (A, r, f)"
kleing@13071
   312
  assumes cert_ok: "cert_ok cert (length phi) A"
kleing@13071
   313
  assumes phi_ok:  "\<forall>pc < length phi. phi!pc \<in> opt A"
kleing@13071
   314
  assumes pres:    "pres_type step (length phi) (err (opt A))" 
kleing@13071
   315
  shows "wtl_cert cert f r step pc (phi!pc) \<noteq> Err"
kleing@9757
   316
proof -
kleing@13071
   317
  have wtl: "wtl_inst cert f r step pc (phi!pc) \<noteq> Err" by (rule stable_wtl)   
kleing@13071
   318
  show ?thesis
kleing@13071
   319
  proof (cases "cert!pc")
kleing@13071
   320
    case None with wtl show ?thesis by (simp add: wtl_cert_def)
kleing@13071
   321
  next
kleing@13071
   322
    case (Some s)
kleing@13071
   323
    with pc fits have "cert!pc = phi!pc" by - (rule fitsD2)
kleing@13071
   324
    with Some have "phi!pc = Some s" by simp
kleing@13071
   325
    with Some wtl esl show ?thesis by (simp add: wtl_cert_def)
kleing@9549
   326
  qed
kleing@9549
   327
qed
kleing@9559
   328
  
kleing@9012
   329
kleing@13071
   330
lemma wtl_less:
kleing@13071
   331
  assumes stable:  "stable (Err.le (Opt.le r)) step (map OK phi) pc"
kleing@13071
   332
  assumes wtl:     "wtl_inst cert f r step pc (phi!pc) = OK s"
kleing@13071
   333
  assumes fits:    "fits step cert phi"  
kleing@13071
   334
  assumes suc_pc:   "Suc pc < length phi"
kleing@13071
   335
  assumes bounded: "bounded step (length phi)"
kleing@13071
   336
  assumes esl:     "err_semilat (A, r, f)"
kleing@13071
   337
  assumes cert_ok: "cert_ok cert (length phi) A"
kleing@13071
   338
  assumes phi_ok:  "\<forall>pc < length phi. phi!pc \<in> opt A"
kleing@13071
   339
  assumes pres:    "pres_type step (length phi) (err (opt A))" 
kleing@13071
   340
  shows "OK s \<le>|r OK (phi!Suc pc)"
kleing@13071
   341
proof -
kleing@13071
   342
  from esl have order: "order (Opt.le r)" by simp
kleing@13071
   343
kleing@13071
   344
  let ?step = "step pc (OK (phi!pc))"
kleing@13071
   345
  from suc_pc have [simp]: "map OK phi ! pc = OK (phi!pc)" by simp
kleing@13071
   346
  from suc_pc have [simp]: "map OK phi ! Suc pc = OK (phi!Suc pc)" by simp
kleing@13071
   347
  from suc_pc have pc: "pc < length phi" by simp
kleing@13071
   348
kleing@13071
   349
  from stable
kleing@13071
   350
  have less: "\<forall>(q,s')\<in>set ?step. s' \<le>|r (map OK phi!q)" 
kleing@13071
   351
    by (simp add: stable_def)
kleing@13071
   352
  
kleing@13071
   353
  from cert_ok pc
kleing@13071
   354
  have cert_suc: "OK (cert!Suc pc) \<in> err (opt A)" by (auto dest: cert_okD3)
kleing@13071
   355
  moreover  
kleing@13071
   356
  from phi_ok pc
kleing@13071
   357
  have "OK (phi!pc) \<in> err (opt A)" by simp
kleing@13071
   358
  with pres pc 
kleing@13071
   359
  have stepA: "\<forall>(pc',s') \<in> set ?step. s' \<in> err (opt A)" 
kleing@13071
   360
    by (blast dest: pres_typeD)
kleing@13071
   361
  ultimately
kleing@13071
   362
  have "merge cert f r pc ?step (OK (cert!Suc pc)) =
kleing@13071
   363
    (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))
kleing@13071
   364
    then map snd [(p',t')\<in>?step.p'=pc+1] ++|f (OK (cert!Suc pc))
kleing@13071
   365
    else Err)" using esl by - (rule merge_def)
kleing@13071
   366
  with wtl have
kleing@13071
   367
    "OK s = (map snd [(p',t')\<in>?step.p'=pc+1] ++|f (OK (cert!Suc pc)))" 
kleing@13071
   368
    (is "_ = (?map ++|f _)" is "_ = ?sum")
kleing@13071
   369
    by (simp add: wtl_inst_def split: split_if_asm)
kleing@13071
   370
  also {
kleing@13071
   371
    from esl
kleing@13071
   372
    have "semilat (err (opt A), Err.le (Opt.le r), lift2 (Opt.sup f))"
kleing@13071
   373
      by (simp add: Err.sl_def)
kleing@13071
   374
    moreover
kleing@13071
   375
    from suc_pc phi_ok 
kleing@13071
   376
    have "OK (phi!Suc pc) \<in> err (opt A)" by simp
kleing@13071
   377
    moreover note cert_suc
kleing@13071
   378
    moreover from stepA 
kleing@13071
   379
    have "snd`(set ?step) \<subseteq> err (opt A)" by auto
kleing@13071
   380
    hence "set ?map \<subseteq> err (opt A)" by auto
kleing@13071
   381
    moreover
kleing@13071
   382
    have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto
kleing@13071
   383
    with less have "\<forall>s' \<in> set ?map. s' \<le>|r OK (phi!Suc pc)" by auto
kleing@13071
   384
    moreover
kleing@13071
   385
    from order fits suc_pc
kleing@13071
   386
    have "OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)"     
kleing@13071
   387
      by (cases "cert!Suc pc") (simp, blast dest: fitsD2) 
kleing@13071
   388
    ultimately
kleing@13071
   389
    have "?sum \<le>|r OK (phi!Suc pc)" by (rule lub)
kleing@13071
   390
  }
kleing@13071
   391
  finally show ?thesis .
kleing@13071
   392
qed
kleing@9012
   393
kleing@9012
   394
kleing@13071
   395
lemma cert_less:
kleing@13071
   396
  assumes stable:  "stable (Err.le (Opt.le r)) step (map OK phi) pc"
kleing@13071
   397
  assumes cert:    "wtl_cert cert f r step pc (phi!pc) = OK s"
kleing@13071
   398
  assumes fits:    "fits step cert phi"  
kleing@13071
   399
  assumes suc_pc:   "Suc pc < length phi"
kleing@13071
   400
  assumes bounded: "bounded step (length phi)"
kleing@13071
   401
  assumes esl:     "err_semilat (A, r, f)"
kleing@13071
   402
  assumes cert_ok: "cert_ok cert (length phi) A"
kleing@13071
   403
  assumes phi_ok:  "\<forall>pc < length phi. phi!pc \<in> opt A"
kleing@13071
   404
  assumes pres:    "pres_type step (length phi) (err (opt A))" 
kleing@13071
   405
  shows "OK s \<le>|r OK (phi!Suc pc)"
kleing@13071
   406
proof (cases "cert!pc")
kleing@13071
   407
  case None with cert 
kleing@13071
   408
  have "wtl_inst cert f r step pc (phi!pc) = OK s" by (simp add: wtl_cert_def)
kleing@13071
   409
  thus ?thesis by - (rule wtl_less)
kleing@13071
   410
next
kleing@13071
   411
  case (Some s') with cert 
kleing@13071
   412
  have "wtl_inst cert f r step pc (Some s') = OK s" 
kleing@13071
   413
    by (simp add: wtl_cert_def split: split_if_asm)
kleing@13071
   414
  also
kleing@13071
   415
  from suc_pc have "pc < length phi" by simp
kleing@13071
   416
  with fits Some have "cert!pc = phi!pc" by - (rule fitsD2)
kleing@13071
   417
  with Some have "Some s' = phi!pc" by simp
kleing@13071
   418
  finally
kleing@13071
   419
  have "wtl_inst cert f r step pc (phi!pc) = OK s" .
kleing@13071
   420
  thus ?thesis by - (rule wtl_less)
kleing@13071
   421
qed
kleing@13071
   422
kleing@13071
   423
kleing@13071
   424
  
kleing@13071
   425
lemma wt_step_wtl_lemma:
kleing@13071
   426
  assumes wt_step: "wt_step (Err.le (Opt.le r)) Err step (map OK phi)"
kleing@13071
   427
  assumes fits:    "fits step cert phi"  
kleing@13071
   428
  assumes bounded: "bounded step (length phi)"
kleing@13071
   429
  assumes esl:     "err_semilat (A, r, f)"
kleing@13071
   430
  assumes cert_ok: "cert_ok cert (length phi) A"
kleing@13071
   431
  assumes phi_ok:  "\<forall>pc < length phi. phi!pc \<in> opt A"
kleing@13071
   432
  assumes pres:    "pres_type step (length phi) (err (opt A))" 
kleing@13071
   433
  assumes mono:    "mono (Err.le (Opt.le r)) step (length phi) (err (opt A))"
kleing@13071
   434
  shows "\<And>pc s. pc+length ins = length phi \<Longrightarrow> OK s \<le>|r OK (phi!pc) \<Longrightarrow> s \<in> opt A \<Longrightarrow>
kleing@13071
   435
                wtl_inst_list ins cert f r step pc s \<noteq> Err"
kleing@13071
   436
  (is "\<And>pc s. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?wtl ins pc s \<noteq> Err")
kleing@13071
   437
proof (induct ins)
kleing@13071
   438
  fix pc s show "?wtl [] pc s \<noteq> Err" by simp
kleing@13071
   439
next
kleing@13071
   440
  fix pc s i ins
kleing@13071
   441
  assume "\<And>pc s. pc+length ins=length phi \<Longrightarrow> OK s \<le>|r OK (phi!pc) \<Longrightarrow> s \<in> opt A \<Longrightarrow>
kleing@13071
   442
                 ?wtl ins pc s \<noteq> Err"
kleing@9757
   443
  moreover
kleing@13071
   444
  assume pc_l: "pc + length (i#ins) = length phi"
kleing@13071
   445
  hence suc_pc_l: "Suc pc + length ins = length phi" by simp
kleing@13071
   446
  ultimately
kleing@13071
   447
  have IH: 
kleing@13071
   448
    "\<And>s. OK s \<le>|r OK (phi!Suc pc) \<Longrightarrow> s \<in> opt A \<Longrightarrow> ?wtl ins (Suc pc) s \<noteq> Err" .
kleing@13071
   449
kleing@13071
   450
  from pc_l obtain pc: "pc < length phi" by simp
kleing@13071
   451
  with wt_step 
kleing@13071
   452
  have stable: "stable (Err.le (Opt.le r)) step (map OK phi) pc" 
kleing@13071
   453
    by (simp add: wt_step_def)
kleing@13071
   454
  moreover
kleing@13071
   455
  assume s_phi: "OK s \<le>|r OK (phi!pc)"
kleing@13071
   456
  ultimately 
kleing@13071
   457
  have "wtl_cert cert f r step pc (phi!pc) \<noteq> Err" by - (rule stable_cert)
kleing@13071
   458
  then obtain s'' where s'': "wtl_cert cert f r step pc (phi!pc) = OK s''" by fast
kleing@13071
   459
  moreover 
kleing@13071
   460
  from phi_ok pc 
kleing@13071
   461
  have phi_pc: "phi!pc \<in> opt A" by simp
kleing@13071
   462
  moreover 
kleing@13071
   463
  assume s: "s \<in> opt A"
kleing@9757
   464
  ultimately
kleing@13071
   465
  obtain s' where "wtl_cert cert f r step pc s = OK s'"
kleing@13071
   466
    by - (drule wtl_cert_mono, assumption+, blast)
kleing@13071
   467
  hence "ins = [] \<Longrightarrow> ?wtl (i#ins) pc s \<noteq> Err" by simp
kleing@13071
   468
  moreover {
kleing@13071
   469
    assume "ins \<noteq> []" 
kleing@13071
   470
    with pc_l have suc_pc: "Suc pc < length phi" by (auto simp add: neq_Nil_conv)
kleing@13071
   471
    with stable s'' have "OK s'' \<le>|r OK (phi!Suc pc)" by - (rule cert_less)
kleing@13071
   472
    moreover
kleing@13071
   473
    from s'' s_phi obtain s' where 
kleing@13071
   474
      cert: "wtl_cert cert f r step pc s = OK s'" and
kleing@13071
   475
      "OK s' \<le>|r OK s''"
kleing@13071
   476
      using phi_pc
kleing@13071
   477
      by - (drule wtl_cert_mono, assumption+, blast)
kleing@13071
   478
    moreover from esl have "order (Err.le (Opt.le r))" by simp
kleing@13071
   479
    ultimately have less: "OK s' \<le>|r OK (phi!Suc pc)" by - (rule order_trans)
kleing@13071
   480
kleing@13071
   481
    from cert_ok suc_pc have "cert!pc \<in> opt A" and "cert!(pc+1) \<in> opt A" 
kleing@13071
   482
      by (auto simp add: cert_ok_def)
kleing@13071
   483
    with s cert pres have "s' \<in> opt A" by - (rule wtl_cert_pres) 
kleing@13071
   484
kleing@13071
   485
    with less IH have "?wtl ins (Suc pc) s' \<noteq> Err" by blast
kleing@13071
   486
    with cert have "?wtl (i#ins) pc s \<noteq> Err" by simp 
kleing@13071
   487
  }
kleing@13071
   488
  ultimately show "?wtl (i#ins) pc s \<noteq> Err" by (cases ins) auto 
kleing@9580
   489
qed
kleing@9012
   490
kleing@9012
   491
kleing@10628
   492
theorem wtl_complete:
kleing@13071
   493
  assumes "wt_step (Err.le (Opt.le r)) Err step (map OK phi)"
kleing@13071
   494
  assumes "OK s \<le>|r OK (phi!0)" and "s \<in> opt A"
kleing@13071
   495
  defines cert:  "cert \<equiv> make_cert step phi"
kleing@13071
   496
kleing@13071
   497
  assumes "bounded step (length phi)" and "err_semilat (A, r, f)"
kleing@13071
   498
  assumes "pres_type step (length phi) (err (opt A))" 
kleing@13071
   499
  assumes "mono (Err.le (Opt.le r)) step (length phi) (err (opt A))"
kleing@13071
   500
  assumes "length ins = length phi"
kleing@13071
   501
  assumes phi_ok:  "\<forall>pc < length phi. phi!pc \<in> opt A"
kleing@13071
   502
kleing@13071
   503
  shows "wtl_inst_list ins cert f r step 0 s \<noteq> Err"
kleing@10628
   504
proof -
kleing@13071
   505
  have "0+length ins = length phi" by simp
kleing@13071
   506
  moreover
kleing@13071
   507
  have "fits step cert phi" by (unfold cert) (rule fits_make_cert)
kleing@13071
   508
  moreover
kleing@13071
   509
  from phi_ok have "cert_ok cert (length phi) A"
kleing@13071
   510
    by (simp add: cert make_cert_def cert_ok_def nth_append)
kleing@13071
   511
  ultimately
kleing@13071
   512
  show ?thesis by - (rule wt_step_wtl_lemma)
kleing@13071
   513
qed
kleing@10592
   514
kleing@9549
   515
kleing@9549
   516
end