src/HOL/MicroJava/BV/LBVSpec.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 15109 bba563cdd997
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
kleing@9757
     1
(*  Title:      HOL/MicroJava/BV/LBVSpec.thy
kleing@8245
     2
    ID:         $Id$
kleing@8245
     3
    Author:     Gerwin Klein
kleing@8245
     4
    Copyright   1999 Technische Universitaet Muenchen
kleing@9054
     5
*)
kleing@8245
     6
kleing@12911
     7
header {* \isaheader{The Lightweight Bytecode Verifier} *}
kleing@9054
     8
kleing@13062
     9
theory LBVSpec = SemilatAlg + Opt:
kleing@13062
    10
kleing@8245
    11
types
kleing@13078
    12
  's certificate = "'s list"   
kleing@8245
    13
kleing@12516
    14
consts
kleing@13078
    15
merge :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> nat \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's \<Rightarrow> 's"
kleing@12516
    16
primrec
kleing@13078
    17
"merge cert f r T pc []     x = x"
kleing@13078
    18
"merge cert f r T pc (s#ss) x = merge cert f r T pc ss (let (pc',s') = s in 
kleing@13078
    19
                                  if pc'=pc+1 then s' +_f x
kleing@13078
    20
                                  else if s' <=_r (cert!pc') then x
kleing@13078
    21
                                  else T)"
kleing@9757
    22
kleing@13062
    23
constdefs
kleing@13078
    24
wtl_inst :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow>
kleing@13078
    25
             's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's"
kleing@13078
    26
"wtl_inst cert f r T step pc s \<equiv> merge cert f r T pc (step pc s) (cert!(pc+1))"
kleing@8245
    27
kleing@13078
    28
wtl_cert :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow>
kleing@13078
    29
             's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's"
kleing@13078
    30
"wtl_cert cert f r T B step pc s \<equiv>
kleing@13078
    31
  if cert!pc = B then 
kleing@13078
    32
    wtl_inst cert f r T step pc s
kleing@13078
    33
  else
kleing@13078
    34
    if s <=_r (cert!pc) then wtl_inst cert f r T step pc (cert!pc) else T"
kleing@9757
    35
kleing@9757
    36
consts 
kleing@13078
    37
wtl_inst_list :: "'a list \<Rightarrow> 's certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow>
kleing@13078
    38
                  's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's"
kleing@8245
    39
primrec
kleing@13101
    40
"wtl_inst_list []     cert f r T B step pc s = s"
kleing@13101
    41
"wtl_inst_list (i#is) cert f r T B step pc s = 
kleing@13078
    42
    (let s' = wtl_cert cert f r T B step pc s in
kleing@13101
    43
      if s' = T \<or> s = T then T else wtl_inst_list is cert f r T B step (pc+1) s')"
kleing@8245
    44
kleing@8245
    45
constdefs
kleing@13078
    46
  cert_ok :: "'s certificate \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> 's set \<Rightarrow> bool"
kleing@13078
    47
  "cert_ok cert n T B A \<equiv> (\<forall>i < n. cert!i \<in> A \<and> cert!i \<noteq> T) \<and> (cert!n = B)"
kleing@13078
    48
kleing@13078
    49
constdefs
kleing@13078
    50
  bottom :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool"
kleing@13078
    51
  "bottom r B \<equiv> \<forall>x. B <=_r x"
kleing@13078
    52
kleing@13078
    53
wenzelm@13365
    54
locale (open) lbv = semilat +
kleing@13078
    55
  fixes T :: "'a" ("\<top>") 
kleing@13078
    56
  fixes B :: "'a" ("\<bottom>") 
kleing@13078
    57
  fixes step :: "'a step_type" 
kleing@13078
    58
  assumes top: "top r \<top>"
kleing@13078
    59
  assumes T_A: "\<top> \<in> A"
kleing@13078
    60
  assumes bot: "bottom r \<bottom>" 
kleing@13078
    61
  assumes B_A: "\<bottom> \<in> A"
kleing@13078
    62
kleing@13078
    63
  fixes merge :: "'a certificate \<Rightarrow> nat \<Rightarrow> (nat \<times> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a"
kleing@13078
    64
  defines mrg_def: "merge cert \<equiv> LBVSpec.merge cert f r \<top>"
kleing@13062
    65
kleing@13078
    66
  fixes wti :: "'a certificate \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
kleing@13078
    67
  defines wti_def: "wti cert \<equiv> wtl_inst cert f r \<top> step"
kleing@13078
    68
 
kleing@13078
    69
  fixes wtc :: "'a certificate \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
kleing@13078
    70
  defines wtc_def: "wtc cert \<equiv> wtl_cert cert f r \<top> \<bottom> step"
kleing@13078
    71
kleing@13078
    72
  fixes wtl :: "'b list \<Rightarrow> 'a certificate \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
kleing@13078
    73
  defines wtl_def: "wtl ins cert \<equiv> wtl_inst_list ins cert f r \<top> \<bottom> step"
kleing@13078
    74
kleing@13078
    75
kleing@13078
    76
lemma (in lbv) wti:
kleing@13078
    77
  "wti c pc s \<equiv> merge c pc (step pc s) (c!(pc+1))"
kleing@13078
    78
  by (simp add: wti_def mrg_def wtl_inst_def)
kleing@13078
    79
kleing@13078
    80
lemma (in lbv) wtc: 
kleing@13078
    81
  "wtc c pc s \<equiv> if c!pc = \<bottom> then wti c pc s else if s <=_r c!pc then wti c pc (c!pc) else \<top>"
kleing@13078
    82
  by (unfold wtc_def wti_def wtl_cert_def)
kleing@13078
    83
kleing@13078
    84
kleing@13078
    85
lemma cert_okD1 [intro?]:
kleing@13078
    86
  "cert_ok c n T B A \<Longrightarrow> pc < n \<Longrightarrow> c!pc \<in> A"
kleing@13062
    87
  by (unfold cert_ok_def) fast
kleing@13062
    88
kleing@13078
    89
lemma cert_okD2 [intro?]:
kleing@13078
    90
  "cert_ok c n T B A \<Longrightarrow> c!n = B"
kleing@13071
    91
  by (simp add: cert_ok_def)
kleing@13071
    92
kleing@13078
    93
lemma cert_okD3 [intro?]:
kleing@13078
    94
  "cert_ok c n T B A \<Longrightarrow> B \<in> A \<Longrightarrow> pc < n \<Longrightarrow> c!Suc pc \<in> A"
kleing@13071
    95
  by (drule Suc_leI) (auto simp add: le_eq_less_or_eq dest: cert_okD1 cert_okD2)
kleing@13071
    96
kleing@13078
    97
lemma cert_okD4 [intro?]:
kleing@13078
    98
  "cert_ok c n T B A \<Longrightarrow> pc < n \<Longrightarrow> c!pc \<noteq> T"
kleing@13078
    99
  by (simp add: cert_ok_def)
kleing@13062
   100
kleing@13062
   101
declare Let_def [simp]
kleing@13062
   102
kleing@13062
   103
section "more semilattice lemmas"
kleing@13062
   104
kleing@13078
   105
kleing@13078
   106
lemma (in lbv) sup_top [simp, elim]:
kleing@13078
   107
  assumes x: "x \<in> A" 
kleing@13078
   108
  shows "x +_f \<top> = \<top>"
kleing@13062
   109
proof -
kleing@13078
   110
  from top have "x +_f \<top> <=_r \<top>" ..
kleing@13078
   111
  moreover from x have "\<top> <=_r x +_f \<top>" ..
kleing@13078
   112
  ultimately show ?thesis ..
kleing@13062
   113
qed
kleing@13062
   114
  
kleing@13078
   115
lemma (in lbv) plusplussup_top [simp, elim]:
kleing@13078
   116
  "set xs \<subseteq> A \<Longrightarrow> xs ++_f \<top> = \<top>"
kleing@13062
   117
  by (induct xs) auto
kleing@13078
   118
kleing@13078
   119
kleing@13062
   120
kleing@13078
   121
lemma (in semilat) pp_ub1':
kleing@13078
   122
  assumes S: "snd`set S \<subseteq> A" 
kleing@13078
   123
  assumes y: "y \<in> A" and ab: "(a, b) \<in> set S" 
kleing@13078
   124
  shows "b <=_r map snd [(p', t')\<in>S . p' = a] ++_f y"
kleing@13078
   125
proof -
kleing@13078
   126
  from S have "\<forall>(x,y) \<in> set S. y \<in> A" by auto
kleing@13078
   127
  with semilat y ab show ?thesis by - (rule ub1')
kleing@13078
   128
qed 
kleing@13062
   129
kleing@13078
   130
lemma (in lbv) bottom_le [simp, intro]:
kleing@13078
   131
  "\<bottom> <=_r x"
kleing@13078
   132
  by (insert bot) (simp add: bottom_def)
kleing@13062
   133
kleing@13078
   134
lemma (in lbv) le_bottom [simp]:
kleing@13078
   135
  "x <=_r \<bottom> = (x = \<bottom>)"
kleing@13078
   136
  by (blast intro: antisym_r)
kleing@13078
   137
kleing@13062
   138
kleing@13062
   139
kleing@13062
   140
section "merge"
kleing@13062
   141
kleing@13078
   142
lemma (in lbv) merge_Nil [simp]:
kleing@13078
   143
  "merge c pc [] x = x" by (simp add: mrg_def)
kleing@13078
   144
kleing@13078
   145
lemma (in lbv) merge_Cons [simp]:
kleing@13078
   146
  "merge c pc (l#ls) x = merge c pc ls (if fst l=pc+1 then snd l +_f x
kleing@13078
   147
                                        else if snd l <=_r (c!fst l) then x
kleing@13078
   148
                                        else \<top>)"
kleing@13078
   149
  by (simp add: mrg_def split_beta)
kleing@13078
   150
kleing@13078
   151
lemma (in lbv) merge_Err [simp]:
kleing@13078
   152
  "snd`set ss \<subseteq> A \<Longrightarrow> merge c pc ss \<top> = \<top>"
kleing@13062
   153
  by (induct ss) auto
kleing@8245
   154
kleing@13078
   155
lemma (in lbv) merge_not_top:
kleing@13078
   156
  "\<And>x. snd`set ss \<subseteq> A \<Longrightarrow> merge c pc ss x \<noteq> \<top> \<Longrightarrow> 
kleing@13078
   157
  \<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r (c!pc'))"
kleing@13078
   158
  (is "\<And>x. ?set ss \<Longrightarrow> ?merge ss x \<Longrightarrow> ?P ss")
kleing@13062
   159
proof (induct ss)
kleing@13062
   160
  show "?P []" by simp
kleing@13062
   161
next
kleing@13078
   162
  fix x ls l
kleing@13078
   163
  assume "?set (l#ls)" then obtain set: "snd`set ls \<subseteq> A" by simp
kleing@13078
   164
  assume merge: "?merge (l#ls) x" 
kleing@13062
   165
  moreover
kleing@13062
   166
  obtain pc' s' where [simp]: "l = (pc',s')" by (cases l)
kleing@13062
   167
  ultimately
kleing@13078
   168
  obtain x' where "?merge ls x'" by simp 
kleing@13078
   169
  assume "\<And>x. ?set ls \<Longrightarrow> ?merge ls x \<Longrightarrow> ?P ls" hence "?P ls" .
kleing@13062
   170
  moreover
kleing@13078
   171
  from merge set
kleing@13078
   172
  have "pc' \<noteq> pc+1 \<longrightarrow> s' <=_r (c!pc')" by (simp split: split_if_asm)
kleing@13062
   173
  ultimately
kleing@13062
   174
  show "?P (l#ls)" by simp
kleing@13062
   175
qed
kleing@13062
   176
kleing@9012
   177
kleing@13078
   178
lemma (in lbv) merge_def:
kleing@13062
   179
  shows 
kleing@13078
   180
  "\<And>x. x \<in> A \<Longrightarrow> snd`set ss \<subseteq> A \<Longrightarrow>
kleing@13078
   181
  merge c pc ss x = 
kleing@13078
   182
  (if \<forall>(pc',s') \<in> set ss. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc' then
kleing@13078
   183
    map snd [(p',t') \<in> ss. p'=pc+1] ++_f x
kleing@13078
   184
  else \<top>)" 
kleing@13062
   185
  (is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?merge ss x = ?if ss x" is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?P ss x")
kleing@13062
   186
proof (induct ss)
kleing@13062
   187
  fix x show "?P [] x" by simp
kleing@13062
   188
next 
kleing@13078
   189
  fix x assume x: "x \<in> A" 
kleing@13078
   190
  fix l::"nat \<times> 'a" and ls  
kleing@13078
   191
  assume "snd`set (l#ls) \<subseteq> A"
kleing@13078
   192
  then obtain l: "snd l \<in> A" and ls: "snd`set ls \<subseteq> A" by auto
kleing@13078
   193
  assume "\<And>x. x \<in> A \<Longrightarrow> snd`set ls \<subseteq> A \<Longrightarrow> ?P ls x" 
kleing@13078
   194
  hence IH: "\<And>x. x \<in> A \<Longrightarrow> ?P ls x" .
kleing@13062
   195
  obtain pc' s' where [simp]: "l = (pc',s')" by (cases l)
kleing@13062
   196
  hence "?merge (l#ls) x = ?merge ls 
kleing@13078
   197
    (if pc'=pc+1 then s' +_f x else if s' <=_r c!pc' then x else \<top>)"
kleing@13062
   198
    (is "?merge (l#ls) x = ?merge ls ?if'")
kleing@13062
   199
    by simp 
kleing@13062
   200
  also have "\<dots> = ?if ls ?if'" 
kleing@13062
   201
  proof -
kleing@13078
   202
    from l have "s' \<in> A" by simp
kleing@13078
   203
    with x have "s' +_f x \<in> A" by simp
kleing@13078
   204
    with x have "?if' \<in> A" by auto
kleing@13062
   205
    hence "?P ls ?if'" by (rule IH) thus ?thesis by simp
kleing@13062
   206
  qed
kleing@13062
   207
  also have "\<dots> = ?if (l#ls) x"
kleing@13078
   208
    proof (cases "\<forall>(pc', s')\<in>set (l#ls). pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'")
kleing@13062
   209
      case True
kleing@13078
   210
      hence "\<forall>(pc', s')\<in>set ls. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
kleing@13062
   211
      moreover
kleing@13062
   212
      from True have 
kleing@13078
   213
        "map snd [(p',t')\<in>ls . p'=pc+1] ++_f ?if' = 
kleing@13078
   214
        (map snd [(p',t')\<in>l#ls . p'=pc+1] ++_f x)"
kleing@13062
   215
        by simp
kleing@13062
   216
      ultimately
kleing@13062
   217
      show ?thesis using True by simp
kleing@13062
   218
    next
kleing@13078
   219
      case False 
kleing@13078
   220
      moreover
kleing@13078
   221
      from ls have "set (map snd [(p', t')\<in>ls . p' = Suc pc]) \<subseteq> A" by auto
kleing@13078
   222
      ultimately show ?thesis by auto
kleing@13062
   223
    qed
kleing@13062
   224
  finally show "?P (l#ls) x" .
kleing@13062
   225
qed
kleing@13062
   226
kleing@13078
   227
lemma (in lbv) merge_not_top_s:
kleing@13078
   228
  assumes x:  "x \<in> A" and ss: "snd`set ss \<subseteq> A"
kleing@13078
   229
  assumes m:  "merge c pc ss x \<noteq> \<top>"
kleing@13078
   230
  shows "merge c pc ss x = (map snd [(p',t') \<in> ss. p'=pc+1] ++_f x)"
kleing@13062
   231
proof -
kleing@13078
   232
  from ss m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc')" 
kleing@13078
   233
    by (rule merge_not_top)
kleing@13078
   234
  with x ss m show ?thesis by - (drule merge_def, auto split: split_if_asm)
kleing@13062
   235
qed
kleing@13062
   236
kleing@13062
   237
section "wtl-inst-list"
kleing@10042
   238
kleing@10812
   239
lemmas [iff] = not_Err_eq
kleing@10812
   240
kleing@13078
   241
lemma (in lbv) wtl_Nil [simp]: "wtl [] c pc s = s" 
kleing@13078
   242
  by (simp add: wtl_def)
kleing@13078
   243
kleing@13078
   244
lemma (in lbv) wtl_Cons [simp]: 
kleing@13078
   245
  "wtl (i#is) c pc s = 
kleing@13078
   246
  (let s' = wtc c pc s in if s' = \<top> \<or> s = \<top> then \<top> else wtl is c (pc+1) s')"
kleing@13078
   247
  by (simp add: wtl_def wtc_def)
kleing@13078
   248
kleing@13078
   249
lemma (in lbv) wtl_Cons_not_top:
kleing@13078
   250
  "wtl (i#is) c pc s \<noteq> \<top> = 
kleing@13078
   251
  (wtc c pc s \<noteq> \<top> \<and> s \<noteq> T \<and> wtl is c (pc+1) (wtc c pc s) \<noteq> \<top>)"
kleing@10812
   252
  by (auto simp del: split_paired_Ex)
kleing@9549
   253
kleing@13078
   254
lemma (in lbv) wtl_top [simp]:  "wtl ls c pc \<top> = \<top>"
kleing@13078
   255
  by (cases ls) auto
kleing@13078
   256
kleing@13078
   257
lemma (in lbv) wtl_not_top:
kleing@13078
   258
  "wtl ls c pc s \<noteq> \<top> \<Longrightarrow> s \<noteq> \<top>"
kleing@13078
   259
  by (cases "s=\<top>") auto
kleing@9012
   260
kleing@13078
   261
lemma (in lbv) wtl_append [simp]:
kleing@13078
   262
  "\<And>pc s. wtl (a@b) c pc s = wtl b c (pc+length a) (wtl a c pc s)"
kleing@13078
   263
  by (induct a) auto
kleing@13078
   264
kleing@13078
   265
lemma (in lbv) wtl_take:
kleing@13078
   266
  "wtl is c pc s \<noteq> \<top> \<Longrightarrow> wtl (take pc' is) c pc s \<noteq> \<top>"
kleing@13078
   267
  (is "?wtl is \<noteq> _ \<Longrightarrow> _")
kleing@9183
   268
proof -
kleing@13078
   269
  assume "?wtl is \<noteq> \<top>"
kleing@13078
   270
  hence "?wtl (take pc' is @ drop pc' is) \<noteq> \<top>" by simp  
kleing@13078
   271
  thus ?thesis by (auto dest!: wtl_not_top simp del: append_take_drop_id)
kleing@9757
   272
qed
kleing@9012
   273
kleing@9757
   274
lemma take_Suc:
kleing@13078
   275
  "\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
kleing@9757
   276
proof (induct l)
kleing@9757
   277
  show "?P []" by simp
kleing@12516
   278
next
kleing@12516
   279
  fix x xs assume IH: "?P xs"  
kleing@9757
   280
  show "?P (x#xs)"
kleing@9757
   281
  proof (intro strip)
kleing@12516
   282
    fix n assume "n < length (x#xs)"
kleing@12516
   283
    with IH show "take (Suc n) (x # xs) = take n (x # xs) @ [(x # xs) ! n]" 
kleing@12516
   284
      by (cases n, auto)
kleing@9183
   285
  qed
kleing@9183
   286
qed
kleing@9012
   287
kleing@13078
   288
lemma (in lbv) wtl_Suc:
kleing@13078
   289
  assumes suc: "pc+1 < length is"
kleing@13078
   290
  assumes wtl: "wtl (take pc is) c 0 s \<noteq> \<top>"
kleing@13078
   291
  shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
kleing@9183
   292
proof -
kleing@13062
   293
  from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
kleing@13078
   294
  with suc wtl show ?thesis by (simp add: min_def)
kleing@9183
   295
qed
kleing@9012
   296
kleing@13078
   297
lemma (in lbv) wtl_all:
kleing@13078
   298
  assumes all: "wtl is c 0 s \<noteq> \<top>" (is "?wtl is \<noteq> _") 
kleing@13078
   299
  assumes pc:  "pc < length is"
kleing@13078
   300
  shows  "wtc c pc (wtl (take pc is) c 0 s) \<noteq> \<top>"
kleing@9183
   301
proof -
kleing@13062
   302
  from pc have "0 < length (drop pc is)" by simp
kleing@12516
   303
  then  obtain i r where Cons: "drop pc is = i#r" 
nipkow@15109
   304
    by (auto simp add: neq_Nil_conv simp del: length_drop drop_eq_Nil)
kleing@9757
   305
  hence "i#r = drop pc is" ..
kleing@13078
   306
  with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp 
kleing@12516
   307
  from pc have "is!pc = drop pc is ! 0" by simp
kleing@12516
   308
  with Cons have "is!pc = i" by simp
kleing@13078
   309
  with take pc show ?thesis by (auto simp add: min_def split: split_if_asm)
kleing@9183
   310
qed
kleing@9012
   311
kleing@13062
   312
section "preserves-type"
kleing@13062
   313
kleing@13078
   314
lemma (in lbv) merge_pres:
kleing@13078
   315
  assumes s0: "snd`set ss \<subseteq> A" and x: "x \<in> A"
kleing@13078
   316
  shows "merge c pc ss x \<in> A"
kleing@13062
   317
proof -
kleing@13078
   318
  from s0 have "set (map snd [(p', t')\<in>ss . p'=pc+1]) \<subseteq> A" by auto
kleing@13078
   319
  with x  have "(map snd [(p', t')\<in>ss . p'=pc+1] ++_f x) \<in> A"
kleing@13062
   320
    by (auto intro!: plusplus_closed)
kleing@13078
   321
  with s0 x show ?thesis by (simp add: merge_def T_A)
kleing@13062
   322
qed
kleing@13062
   323
  
kleing@13062
   324
kleing@13078
   325
lemma pres_typeD2:
kleing@13078
   326
  "pres_type step n A \<Longrightarrow> s \<in> A \<Longrightarrow> p < n \<Longrightarrow> snd`set (step p s) \<subseteq> A"
kleing@13078
   327
  by auto (drule pres_typeD)
kleing@13062
   328
kleing@13078
   329
kleing@13078
   330
lemma (in lbv) wti_pres [intro?]:
kleing@13078
   331
  assumes pres: "pres_type step n A" 
kleing@13078
   332
  assumes cert: "c!(pc+1) \<in> A"
kleing@13078
   333
  assumes s_pc: "s \<in> A" "pc < n"
kleing@13078
   334
  shows "wti c pc s \<in> A"
kleing@13062
   335
proof -
kleing@13078
   336
  from pres s_pc have "snd`set (step pc s) \<subseteq> A" by (rule pres_typeD2)
kleing@13078
   337
  with cert show ?thesis by (simp add: wti merge_pres)
kleing@13062
   338
qed
kleing@13062
   339
kleing@13062
   340
kleing@13078
   341
lemma (in lbv) wtc_pres:
kleing@13078
   342
  assumes "pres_type step n A"
kleing@13078
   343
  assumes "c!pc \<in> A" and "c!(pc+1) \<in> A"
kleing@13078
   344
  assumes "s \<in> A" and "pc < n"
kleing@13078
   345
  shows "wtc c pc s \<in> A"
kleing@13062
   346
proof -
kleing@13078
   347
  have "wti c pc s \<in> A" ..
kleing@13078
   348
  moreover have "wti c pc (c!pc) \<in> A" ..
kleing@13078
   349
  ultimately show ?thesis using T_A by (simp add: wtc) 
kleing@13062
   350
qed
kleing@13062
   351
kleing@13078
   352
kleing@13078
   353
lemma (in lbv) wtl_pres:
kleing@13078
   354
  assumes pres: "pres_type step (length is) A"
kleing@13078
   355
  assumes cert: "cert_ok c (length is) \<top> \<bottom> A"
kleing@13078
   356
  assumes s:    "s \<in> A" 
kleing@13078
   357
  assumes all:  "wtl is c 0 s \<noteq> \<top>"
kleing@13078
   358
  shows "pc < length is \<Longrightarrow> wtl (take pc is) c 0 s \<in> A"
kleing@13078
   359
  (is "?len pc \<Longrightarrow> ?wtl pc \<in> A")
kleing@13062
   360
proof (induct pc)
kleing@13078
   361
  from s show "?wtl 0 \<in> A" by simp
kleing@13062
   362
next
kleing@13078
   363
  fix n assume "Suc n < length is"
kleing@13078
   364
  then obtain n: "n < length is" by simp  
kleing@13078
   365
  assume "n < length is \<Longrightarrow> ?wtl n \<in> A"
kleing@13078
   366
  hence "?wtl n \<in> A" .
kleing@13078
   367
  moreover
kleing@13078
   368
  from cert have "c!n \<in> A" by (rule cert_okD1)
kleing@13062
   369
  moreover
kleing@13062
   370
  have n1: "n+1 < length is" by simp
kleing@13078
   371
  with cert have "c!(n+1) \<in> A" by (rule cert_okD1)
kleing@13062
   372
  ultimately
kleing@13078
   373
  have "wtc c n (?wtl n) \<in> A" by - (rule wtc_pres)
kleing@13078
   374
  also
kleing@13078
   375
  from all n have "?wtl n \<noteq> \<top>" by - (rule wtl_take)
kleing@13078
   376
  with n1 have "wtc c n (?wtl n) = ?wtl (n+1)" by (rule wtl_Suc [symmetric])
kleing@13078
   377
  finally  show "?wtl (Suc n) \<in> A" by simp
kleing@13062
   378
qed
kleing@13062
   379
kleing@10042
   380
kleing@9183
   381
end