src/HOL/MicroJava/BV/LBVComplete.thy
author wenzelm
Tue Jul 16 18:26:09 2002 +0200 (2002-07-16)
changeset 13365 a2c4faad4d35
parent 13101 90b31354fe15
child 15425 6356d2523f73
permissions -rw-r--r--
adapted to locale defs;
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@13078
    12
  is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool" 
kleing@13078
    13
  "is_target step phi pc' \<equiv>
kleing@13078
    14
     \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc))"
kleing@8388
    15
kleing@13078
    16
  make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate"
kleing@13078
    17
  "make_cert step phi B \<equiv> 
kleing@13078
    18
     map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..length phi(] @ [B]"
kleing@13078
    19
kleing@13101
    20
constdefs
kleing@13101
    21
  list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
kleing@13101
    22
  "list_ex P xs \<equiv> \<exists>x \<in> set xs. P x"
kleing@13101
    23
kleing@13101
    24
lemma [code]: "list_ex P [] = False" by (simp add: list_ex_def)
kleing@13101
    25
lemma [code]: "list_ex P (x#xs) = (P x \<or> list_ex P xs)" by (simp add: list_ex_def)
kleing@13101
    26
kleing@13101
    27
lemma [code]:
kleing@13101
    28
  "is_target step phi pc' =
kleing@13101
    29
  list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..length phi(]"
kleing@13101
    30
  apply (simp add: list_ex_def is_target_def set_mem_eq)
kleing@13101
    31
  apply force
kleing@13101
    32
  done
kleing@13101
    33
wenzelm@13365
    34
locale (open) lbvc = lbv + 
kleing@13078
    35
  fixes phi :: "'a list" ("\<phi>")
kleing@13078
    36
  fixes c   :: "'a list" 
kleing@13078
    37
  defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>"
kleing@9012
    38
kleing@13078
    39
  assumes mono: "mono r step (length \<phi>) A"
kleing@13078
    40
  assumes pres: "pres_type step (length \<phi>) A" 
kleing@13078
    41
  assumes phi:  "\<forall>pc < length \<phi>. \<phi>!pc \<in> A \<and> \<phi>!pc \<noteq> \<top>"
kleing@13078
    42
  assumes bounded: "bounded step (length \<phi>)"
kleing@13078
    43
kleing@13078
    44
  assumes B_neq_T: "\<bottom> \<noteq> \<top>" 
kleing@13078
    45
kleing@8388
    46
kleing@13078
    47
lemma (in lbvc) cert: "cert_ok c (length \<phi>) \<top> \<bottom> A"
kleing@13078
    48
proof (unfold cert_ok_def, intro strip conjI)  
kleing@13078
    49
  note [simp] = make_cert_def cert_def nth_append 
kleing@13078
    50
kleing@13078
    51
  show "c!length \<phi> = \<bottom>" by simp
kleing@9757
    52
kleing@13078
    53
  fix pc assume pc: "pc < length \<phi>" 
kleing@13078
    54
  from pc phi B_A show "c!pc \<in> A" by simp
kleing@13078
    55
  from pc phi B_neq_T show "c!pc \<noteq> \<top>" by simp
kleing@13078
    56
qed
kleing@13078
    57
kleing@9559
    58
lemmas [simp del] = split_paired_Ex
kleing@9559
    59
kleing@9012
    60
kleing@13078
    61
lemma (in lbvc) cert_target [intro?]:
kleing@13078
    62
  "\<lbrakk> (pc',s') \<in> set (step pc (\<phi>!pc));
kleing@13078
    63
      pc' \<noteq> pc+1; pc < length \<phi>; pc' < length \<phi> \<rbrakk>
kleing@13078
    64
  \<Longrightarrow> c!pc' = \<phi>!pc'"
kleing@13078
    65
  by (auto simp add: cert_def make_cert_def nth_append is_target_def)
kleing@9012
    66
kleing@9549
    67
kleing@13078
    68
lemma (in lbvc) cert_approx [intro?]:
kleing@13078
    69
  "\<lbrakk> pc < length \<phi>; c!pc \<noteq> \<bottom> \<rbrakk>
kleing@13078
    70
  \<Longrightarrow> c!pc = \<phi>!pc"
kleing@13078
    71
  by (auto simp add: cert_def make_cert_def nth_append)
kleing@13064
    72
kleing@13064
    73
kleing@13078
    74
lemma (in lbv) le_top [simp, intro]:
kleing@13078
    75
  "x <=_r \<top>"
kleing@13078
    76
  by (insert top) simp
kleing@13078
    77
  
kleing@13078
    78
kleing@13078
    79
lemma (in lbv) merge_mono:
kleing@13078
    80
  assumes less:  "ss2 <=|r| ss1"
kleing@13078
    81
  assumes x:     "x \<in> A"
kleing@13078
    82
  assumes ss1:   "snd`set ss1 \<subseteq> A"
kleing@13078
    83
  assumes ss2:   "snd`set ss2 \<subseteq> A"
kleing@13078
    84
  shows "merge c pc ss2 x <=_r merge c pc ss1 x" (is "?s2 <=_r ?s1")
kleing@13064
    85
proof-
kleing@13078
    86
  have "?s1 = \<top> \<Longrightarrow> ?thesis" by simp
kleing@13070
    87
  moreover {
kleing@13078
    88
    assume merge: "?s1 \<noteq> T" 
kleing@13078
    89
    from x ss1 have "?s1 =
kleing@13078
    90
      (if \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
kleing@13078
    91
      then (map snd [(p', t')\<in>ss1 . p'=pc+1]) ++_f x
kleing@13078
    92
      else \<top>)" 
kleing@13078
    93
      by (rule merge_def)  
kleing@13078
    94
    with merge obtain
kleing@13078
    95
      app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc'" 
kleing@13078
    96
           (is "?app ss1") and
kleing@13078
    97
      sum: "(map snd [(p',t')\<in>ss1 . p' = pc+1] ++_f x) = ?s1" 
kleing@13078
    98
           (is "?map ss1 ++_f x = _" is "?sum ss1 = _")
kleing@13078
    99
      by (simp split: split_if_asm)
kleing@13078
   100
    from app less 
kleing@13078
   101
    have "?app ss2" by (blast dest: trans_r lesub_step_typeD)
kleing@13070
   102
    moreover {
kleing@13078
   103
      from ss1 have map1: "set (?map ss1) \<subseteq> A" by auto
kleing@13078
   104
      with x have "?sum ss1 \<in> A" by (auto intro!: plusplus_closed)
kleing@13078
   105
      with sum have "?s1 \<in> A" by simp
kleing@13078
   106
      moreover    
kleing@13078
   107
      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@13078
   108
      from x map1 
kleing@13078
   109
      have "\<forall>x \<in> set (?map ss1). x <=_r ?sum ss1"
kleing@13078
   110
        by clarify (rule pp_ub1)
kleing@13078
   111
      with sum have "\<forall>x \<in> set (?map ss1). x <=_r ?s1" by simp
kleing@13078
   112
      with less have "\<forall>x \<in> set (?map ss2). x <=_r ?s1"
kleing@13078
   113
        by (fastsimp dest!: mapD lesub_step_typeD intro: trans_r)
kleing@13078
   114
      moreover 
kleing@13078
   115
      from map1 x have "x <=_r (?sum ss1)" by (rule pp_ub2)
kleing@13078
   116
      with sum have "x <=_r ?s1" by simp
kleing@13078
   117
      moreover 
kleing@13078
   118
      from ss2 have "set (?map ss2) \<subseteq> A" by auto
kleing@13078
   119
      ultimately
kleing@13078
   120
      have "?sum ss2 <=_r ?s1" using x by - (rule pp_lub)
kleing@13078
   121
    }
kleing@13078
   122
    moreover
kleing@13078
   123
    from x ss2 have 
kleing@13078
   124
      "?s2 =
kleing@13078
   125
      (if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
kleing@13078
   126
      then map snd [(p', t')\<in>ss2 . p' = pc + 1] ++_f x
kleing@13078
   127
      else \<top>)" 
kleing@13078
   128
      by (rule merge_def)
kleing@13078
   129
    ultimately have ?thesis by simp
kleing@13070
   130
  }
kleing@13078
   131
  ultimately show ?thesis by (cases "?s1 = \<top>") auto
kleing@13064
   132
qed
kleing@13064
   133
kleing@13064
   134
kleing@13078
   135
lemma (in lbvc) wti_mono:
kleing@13078
   136
  assumes less: "s2 <=_r s1"
kleing@13078
   137
  assumes pc:   "pc < length \<phi>" 
kleing@13078
   138
  assumes s1:   "s1 \<in> A"
kleing@13078
   139
  assumes s2:   "s2 \<in> A"
kleing@13078
   140
  shows "wti c pc s2 <=_r wti c pc s1" (is "?s2' <=_r ?s1'")
kleing@9549
   141
proof -
kleing@13078
   142
  from mono s2 have "step pc s2 <=|r| step pc s1" by - (rule monoD)
kleing@13071
   143
  moreover
kleing@13078
   144
  from pc cert have "c!Suc pc \<in> A" by - (rule cert_okD3)
kleing@13078
   145
  moreover 
kleing@13078
   146
  from pres s1 pc
kleing@13078
   147
  have "snd`set (step pc s1) \<subseteq> A" by (rule pres_typeD2)
kleing@13071
   148
  moreover
kleing@13071
   149
  from pres s2 pc
kleing@13078
   150
  have "snd`set (step pc s2) \<subseteq> A" by (rule pres_typeD2)
kleing@13071
   151
  ultimately
kleing@13078
   152
  show ?thesis by (simp add: wti merge_mono)
kleing@13071
   153
qed 
kleing@9012
   154
kleing@13078
   155
lemma (in lbvc) wtc_mono:
kleing@13078
   156
  assumes less: "s2 <=_r s1"
kleing@13078
   157
  assumes pc:   "pc < length \<phi>" 
kleing@13078
   158
  assumes s1:   "s1 \<in> A"
kleing@13078
   159
  assumes s2:   "s2 \<in> A"
kleing@13078
   160
  shows "wtc c pc s2 <=_r wtc c pc s1" (is "?s2' <=_r ?s1'")
kleing@13078
   161
proof (cases "c!pc = \<bottom>")
kleing@13078
   162
  case True 
kleing@13078
   163
  moreover have "wti c pc s2 <=_r wti c pc s1" by (rule wti_mono)
kleing@13078
   164
  ultimately show ?thesis by (simp add: wtc)
kleing@13071
   165
next
kleing@13078
   166
  case False
kleing@13078
   167
  have "?s1' = \<top> \<Longrightarrow> ?thesis" by simp
kleing@13078
   168
  moreover {
kleing@13078
   169
    assume "?s1' \<noteq> \<top>" 
kleing@13078
   170
    with False have c: "s1 <=_r c!pc" by (simp add: wtc split: split_if_asm)
kleing@13078
   171
    with less have "s2 <=_r c!pc" ..
kleing@13078
   172
    with False c have ?thesis by (simp add: wtc)
kleing@13078
   173
  }
kleing@13078
   174
  ultimately show ?thesis by (cases "?s1' = \<top>") auto
kleing@9376
   175
qed
kleing@9757
   176
kleing@9559
   177
kleing@13078
   178
lemma (in lbv) top_le_conv [simp]:
kleing@13078
   179
  "\<top> <=_r x = (x = \<top>)"
kleing@13078
   180
  by (insert semilat) (simp add: top top_le_conv) 
kleing@13078
   181
kleing@13078
   182
lemma (in lbv) neq_top [simp, elim]:
kleing@13078
   183
  "\<lbrakk> x <=_r y; y \<noteq> \<top> \<rbrakk> \<Longrightarrow> x \<noteq> \<top>"
kleing@13078
   184
  by (cases "x = T") auto
kleing@13078
   185
kleing@13078
   186
kleing@13078
   187
lemma (in lbvc) stable_wti:
kleing@13078
   188
  assumes stable:  "stable r step \<phi> pc"
kleing@13078
   189
  assumes pc:      "pc < length \<phi>"
kleing@13078
   190
  shows "wti c pc (\<phi>!pc) \<noteq> \<top>"
kleing@9559
   191
proof -
kleing@13078
   192
  let ?step = "step pc (\<phi>!pc)"
kleing@13071
   193
  from stable 
kleing@13078
   194
  have less: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def)
kleing@13071
   195
  
kleing@13078
   196
  from cert pc 
kleing@13078
   197
  have cert_suc: "c!Suc pc \<in> A" by - (rule cert_okD3)
kleing@13071
   198
  moreover  
kleing@13078
   199
  from phi pc have "\<phi>!pc \<in> A" by simp
kleing@13071
   200
  with pres pc 
kleing@13078
   201
  have stepA: "snd`set ?step \<subseteq> A" by - (rule pres_typeD2)  
kleing@13071
   202
  ultimately
kleing@13078
   203
  have "merge c pc ?step (c!Suc pc) =
kleing@13078
   204
    (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
kleing@13078
   205
    then map snd [(p',t')\<in>?step.p'=pc+1] ++_f c!Suc pc
kleing@13078
   206
    else \<top>)" by (rule merge_def)
kleing@13071
   207
  moreover {
kleing@13071
   208
    fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
kleing@13078
   209
    with less have "s' <=_r \<phi>!pc'" by auto
kleing@13078
   210
    also 
kleing@13078
   211
    from bounded pc s' have "pc' < length \<phi>" by (rule boundedD)
kleing@13078
   212
    with s' suc_pc pc have "c!pc' = \<phi>!pc'" ..
kleing@13078
   213
    hence "\<phi>!pc' = c!pc'" ..
kleing@13078
   214
    finally have "s' <=_r c!pc'" .
kleing@13078
   215
  } hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
kleing@13071
   216
  moreover
kleing@13078
   217
  from pc have "Suc pc = length \<phi> \<or> Suc pc < length \<phi>" by auto
kleing@13078
   218
  hence "map snd [(p',t')\<in>?step.p'=pc+1] ++_f c!Suc pc \<noteq> \<top>" 
kleing@13078
   219
         (is "?map ++_f _ \<noteq> _")
kleing@13071
   220
  proof (rule disjE)
kleing@13078
   221
    assume pc': "Suc pc = length \<phi>"
kleing@13078
   222
    with cert have "c!Suc pc = \<bottom>" by (simp add: cert_okD2)
kleing@13071
   223
    moreover 
kleing@13078
   224
    from pc' bounded pc 
kleing@13071
   225
    have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto)
kleing@13071
   226
    hence "[(p',t')\<in>?step.p'=pc+1] = []" by (blast intro: filter_False) 
kleing@13071
   227
    hence "?map = []" by simp
kleing@13078
   228
    ultimately show ?thesis by (simp add: B_neq_T)  
kleing@13071
   229
  next
kleing@13078
   230
    assume pc': "Suc pc < length \<phi>"
kleing@13078
   231
    from pc' phi have "\<phi>!Suc pc \<in> A" by simp
kleing@13071
   232
    moreover note cert_suc
kleing@13071
   233
    moreover from stepA 
kleing@13078
   234
    have "set ?map \<subseteq> A" by auto
kleing@13071
   235
    moreover
kleing@13071
   236
    have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto
kleing@13078
   237
    with less have "\<forall>s' \<in> set ?map. s' <=_r \<phi>!Suc pc" by auto
kleing@13071
   238
    moreover
kleing@13078
   239
    from pc' have "c!Suc pc <=_r \<phi>!Suc pc" 
kleing@13078
   240
      by (cases "c!Suc pc = \<bottom>") (auto dest: cert_approx)
kleing@13071
   241
    ultimately
kleing@13078
   242
    have "?map ++_f c!Suc pc <=_r \<phi>!Suc pc" by (rule pp_lub)
kleing@13078
   243
    moreover
kleing@13078
   244
    from pc' phi have "\<phi>!Suc pc \<noteq> \<top>" by simp
kleing@13078
   245
    ultimately
kleing@13078
   246
    show ?thesis by auto
kleing@9559
   247
  qed
kleing@13071
   248
  ultimately
kleing@13078
   249
  have "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by simp
kleing@13078
   250
  thus ?thesis by (simp add: wti)  
kleing@9376
   251
qed
kleing@9012
   252
kleing@13078
   253
lemma (in lbvc) wti_less:
kleing@13078
   254
  assumes stable:  "stable r step \<phi> pc"
kleing@13078
   255
  assumes suc_pc:   "Suc pc < length \<phi>"
kleing@13078
   256
  shows "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" (is "?wti <=_r _")
kleing@9757
   257
proof -
kleing@13078
   258
  let ?step = "step pc (\<phi>!pc)"
kleing@13071
   259
kleing@13078
   260
  from stable 
kleing@13078
   261
  have less: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def)
kleing@13078
   262
   
kleing@13078
   263
  from suc_pc have pc: "pc < length \<phi>" by simp
kleing@13078
   264
  with cert have cert_suc: "c!Suc pc \<in> A" by - (rule cert_okD3)
kleing@13071
   265
  moreover  
kleing@13078
   266
  from phi pc have "\<phi>!pc \<in> A" by simp
kleing@13078
   267
  with pres pc have stepA: "snd`set ?step \<subseteq> A" by - (rule pres_typeD2)
kleing@13078
   268
  moreover
kleing@13078
   269
  from stable pc have "?wti \<noteq> \<top>" by (rule stable_wti)
kleing@13078
   270
  hence "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by (simp add: wti)
kleing@13071
   271
  ultimately
kleing@13078
   272
  have "merge c pc ?step (c!Suc pc) =
kleing@13078
   273
    map snd [(p',t')\<in>?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s) 
kleing@13078
   274
  hence "?wti = \<dots>" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti)
kleing@13071
   275
  also {
kleing@13078
   276
    from suc_pc phi have "\<phi>!Suc pc \<in> A" by simp
kleing@13071
   277
    moreover note cert_suc
kleing@13078
   278
    moreover from stepA have "set ?map \<subseteq> A" by auto
kleing@13071
   279
    moreover
kleing@13071
   280
    have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto
kleing@13078
   281
    with less have "\<forall>s' \<in> set ?map. s' <=_r \<phi>!Suc pc" by auto
kleing@13071
   282
    moreover
kleing@13078
   283
    from suc_pc have "c!Suc pc <=_r \<phi>!Suc pc"
kleing@13078
   284
      by (cases "c!Suc pc = \<bottom>") (auto dest: cert_approx)
kleing@13071
   285
    ultimately
kleing@13078
   286
    have "?sum <=_r \<phi>!Suc pc" by (rule pp_lub)
kleing@13071
   287
  }
kleing@13071
   288
  finally show ?thesis .
kleing@13071
   289
qed
kleing@9012
   290
kleing@13078
   291
lemma (in lbvc) stable_wtc:
kleing@13078
   292
  assumes stable:  "stable r step phi pc"
kleing@13078
   293
  assumes pc:      "pc < length \<phi>"
kleing@13078
   294
  shows "wtc c pc (\<phi>!pc) \<noteq> \<top>"
kleing@13078
   295
proof -
kleing@13078
   296
  have wti: "wti c pc (\<phi>!pc) \<noteq> \<top>" by (rule stable_wti)   
kleing@13078
   297
  show ?thesis
kleing@13078
   298
  proof (cases "c!pc = \<bottom>")
kleing@13078
   299
    case True with wti show ?thesis by (simp add: wtc)
kleing@13078
   300
  next
kleing@13078
   301
    case False
kleing@13078
   302
    with pc have "c!pc = \<phi>!pc" ..    
kleing@13078
   303
    with False wti show ?thesis by (simp add: wtc)
kleing@13078
   304
  qed
kleing@13078
   305
qed
kleing@9012
   306
kleing@13078
   307
lemma (in lbvc) wtc_less:
kleing@13078
   308
  assumes stable: "stable r step \<phi> pc"
kleing@13078
   309
  assumes suc_pc: "Suc pc < length \<phi>"
kleing@13078
   310
  shows "wtc c pc (\<phi>!pc) <=_r \<phi>!Suc pc" (is "?wtc <=_r _")
kleing@13078
   311
proof (cases "c!pc = \<bottom>")
kleing@13078
   312
  case True
kleing@13078
   313
  moreover have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less)
kleing@13078
   314
  ultimately show ?thesis by (simp add: wtc)
kleing@13071
   315
next
kleing@13078
   316
  case False
kleing@13078
   317
  from suc_pc have pc: "pc < length \<phi>" by simp
kleing@13078
   318
  hence "?wtc \<noteq> \<top>" by - (rule stable_wtc)
kleing@13078
   319
  with False have "?wtc = wti c pc (c!pc)" 
kleing@13078
   320
    by (unfold wtc) (simp split: split_if_asm)
kleing@13078
   321
  also from pc False have "c!pc = \<phi>!pc" .. 
kleing@13078
   322
  finally have "?wtc = wti c pc (\<phi>!pc)" .
kleing@13078
   323
  also have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less)
kleing@13078
   324
  finally show ?thesis .
kleing@13071
   325
qed
kleing@13071
   326
kleing@13071
   327
kleing@13078
   328
lemma (in lbvc) wt_step_wtl_lemma:
kleing@13078
   329
  assumes wt_step: "wt_step r \<top> step \<phi>"
kleing@13078
   330
  shows "\<And>pc s. pc+length ls = length \<phi> \<Longrightarrow> s <=_r \<phi>!pc \<Longrightarrow> s \<in> A \<Longrightarrow> s\<noteq>\<top> \<Longrightarrow>
kleing@13078
   331
                wtl ls c pc s \<noteq> \<top>"
kleing@13078
   332
  (is "\<And>pc s. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?wtl ls pc s \<noteq> _")
kleing@13078
   333
proof (induct ls)
kleing@13078
   334
  fix pc s assume "s\<noteq>\<top>" thus "?wtl [] pc s \<noteq> \<top>" by simp
kleing@13071
   335
next
kleing@13078
   336
  fix pc s i ls
kleing@13078
   337
  assume "\<And>pc s. pc+length ls=length \<phi> \<Longrightarrow> s <=_r \<phi>!pc \<Longrightarrow> s \<in> A \<Longrightarrow> s\<noteq>\<top> \<Longrightarrow> 
kleing@13078
   338
                  ?wtl ls pc s \<noteq> \<top>"
kleing@9757
   339
  moreover
kleing@13078
   340
  assume pc_l: "pc + length (i#ls) = length \<phi>"
kleing@13078
   341
  hence suc_pc_l: "Suc pc + length ls = length \<phi>" by simp
kleing@13071
   342
  ultimately
kleing@13078
   343
  have IH: "\<And>s. s <=_r \<phi>!Suc pc \<Longrightarrow> s \<in> A \<Longrightarrow> s \<noteq> \<top> \<Longrightarrow> ?wtl ls (Suc pc) s \<noteq> \<top>" .
kleing@13071
   344
kleing@13078
   345
  from pc_l obtain pc: "pc < length \<phi>" by simp
kleing@13078
   346
  with wt_step have stable: "stable r step \<phi> pc" by (simp add: wt_step_def)
kleing@13071
   347
  moreover
kleing@13078
   348
  assume s_phi: "s <=_r \<phi>!pc"
kleing@13071
   349
  ultimately 
kleing@13078
   350
  have wt_phi: "wtc c pc (\<phi>!pc) \<noteq> \<top>" by - (rule stable_wtc)
kleing@13078
   351
kleing@13078
   352
  from phi pc have phi_pc: "\<phi>!pc \<in> A" by simp
kleing@13071
   353
  moreover 
kleing@13078
   354
  assume s: "s \<in> A"
kleing@9757
   355
  ultimately
kleing@13078
   356
  have wt_s_phi: "wtc c pc s <=_r wtc c pc (\<phi>!pc)" using s_phi by - (rule wtc_mono)
kleing@13078
   357
  with wt_phi have wt_s: "wtc c pc s \<noteq> \<top>" by simp
kleing@13078
   358
  moreover
kleing@13078
   359
  assume s: "s \<noteq> \<top>" 
kleing@13078
   360
  ultimately
kleing@13078
   361
  have "ls = [] \<Longrightarrow> ?wtl (i#ls) pc s \<noteq> \<top>" by simp
kleing@13071
   362
  moreover {
kleing@13078
   363
    assume "ls \<noteq> []" 
kleing@13078
   364
    with pc_l have suc_pc: "Suc pc < length \<phi>" by (auto simp add: neq_Nil_conv)
kleing@13078
   365
    with stable have "wtc c pc (phi!pc) <=_r \<phi>!Suc pc" by (rule wtc_less)
kleing@13078
   366
    with wt_s_phi have "wtc c pc s <=_r \<phi>!Suc pc" by (rule trans_r)      
kleing@13071
   367
    moreover
kleing@13078
   368
    from cert suc_pc have "c!pc \<in> A" "c!(pc+1) \<in> A" 
kleing@13071
   369
      by (auto simp add: cert_ok_def)
kleing@13078
   370
    with pres have "wtc c pc s \<in> A" by (rule wtc_pres)
kleing@13078
   371
    ultimately
kleing@13078
   372
    have "?wtl ls (Suc pc) (wtc c pc s) \<noteq> \<top>" using IH wt_s by blast
kleing@13078
   373
    with s wt_s have "?wtl (i#ls) pc s \<noteq> \<top>" by simp 
kleing@13071
   374
  }
kleing@13078
   375
  ultimately show "?wtl (i#ls) pc s \<noteq> \<top>" by (cases ls) blast+
kleing@9580
   376
qed
kleing@9012
   377
kleing@13078
   378
  
kleing@13078
   379
theorem (in lbvc) wtl_complete:
kleing@13078
   380
  assumes "wt_step r \<top> step \<phi>"
kleing@13078
   381
  assumes "s <=_r \<phi>!0" and "s \<in> A" and "s \<noteq> \<top>" and "length ins = length phi"
kleing@13078
   382
  shows "wtl ins c 0 s \<noteq> \<top>"
kleing@13078
   383
proof -  
kleing@13071
   384
  have "0+length ins = length phi" by simp
kleing@13078
   385
  thus ?thesis by - (rule wt_step_wtl_lemma)
kleing@13071
   386
qed
kleing@10592
   387
kleing@9549
   388
kleing@9549
   389
end