summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/MicroJava/BV/LBVComplete.thy

author | wenzelm |

Thu Oct 04 20:29:42 2007 +0200 (2007-10-04) | |

changeset 24850 | 0cfd722ab579 |

parent 23467 | d1b97708d5eb |

child 27681 | 8cedebf55539 |

permissions | -rw-r--r-- |

Name.uu, Name.aT;

1 (* Title: HOL/MicroJava/BV/LBVComplete.thy

2 ID: $Id$

3 Author: Gerwin Klein

4 Copyright 2000 Technische Universitaet Muenchen

5 *)

7 header {* \isaheader{Completeness of the LBV} *}

9 theory LBVComplete

10 imports LBVSpec Typing_Framework

11 begin

13 constdefs

14 is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool"

15 "is_target step phi pc' \<equiv>

16 \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc))"

18 make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate"

19 "make_cert step phi B \<equiv>

20 map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]"

22 lemma [code]:

23 "is_target step phi pc' =

24 list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]"

25 by (force simp: list_ex_iff is_target_def mem_iff)

28 locale (open) lbvc = lbv +

29 fixes phi :: "'a list" ("\<phi>")

30 fixes c :: "'a list"

31 defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>"

33 assumes mono: "mono r step (length \<phi>) A"

34 assumes pres: "pres_type step (length \<phi>) A"

35 assumes phi: "\<forall>pc < length \<phi>. \<phi>!pc \<in> A \<and> \<phi>!pc \<noteq> \<top>"

36 assumes bounded: "bounded step (length \<phi>)"

38 assumes B_neq_T: "\<bottom> \<noteq> \<top>"

41 lemma (in lbvc) cert: "cert_ok c (length \<phi>) \<top> \<bottom> A"

42 proof (unfold cert_ok_def, intro strip conjI)

43 note [simp] = make_cert_def cert_def nth_append

45 show "c!length \<phi> = \<bottom>" by simp

47 fix pc assume pc: "pc < length \<phi>"

48 from pc phi B_A show "c!pc \<in> A" by simp

49 from pc phi B_neq_T show "c!pc \<noteq> \<top>" by simp

50 qed

52 lemmas [simp del] = split_paired_Ex

55 lemma (in lbvc) cert_target [intro?]:

56 "\<lbrakk> (pc',s') \<in> set (step pc (\<phi>!pc));

57 pc' \<noteq> pc+1; pc < length \<phi>; pc' < length \<phi> \<rbrakk>

58 \<Longrightarrow> c!pc' = \<phi>!pc'"

59 by (auto simp add: cert_def make_cert_def nth_append is_target_def)

62 lemma (in lbvc) cert_approx [intro?]:

63 "\<lbrakk> pc < length \<phi>; c!pc \<noteq> \<bottom> \<rbrakk>

64 \<Longrightarrow> c!pc = \<phi>!pc"

65 by (auto simp add: cert_def make_cert_def nth_append)

68 lemma (in lbv) le_top [simp, intro]:

69 "x <=_r \<top>"

70 by (insert top) simp

73 lemma (in lbv) merge_mono:

74 assumes less: "ss2 <=|r| ss1"

75 assumes x: "x \<in> A"

76 assumes ss1: "snd`set ss1 \<subseteq> A"

77 assumes ss2: "snd`set ss2 \<subseteq> A"

78 shows "merge c pc ss2 x <=_r merge c pc ss1 x" (is "?s2 <=_r ?s1")

79 proof-

80 have "?s1 = \<top> \<Longrightarrow> ?thesis" by simp

81 moreover {

82 assume merge: "?s1 \<noteq> T"

83 from x ss1 have "?s1 =

84 (if \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'

85 then (map snd [(p', t') \<leftarrow> ss1 . p'=pc+1]) ++_f x

86 else \<top>)"

87 by (rule merge_def)

88 with merge obtain

89 app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc'"

90 (is "?app ss1") and

91 sum: "(map snd [(p',t') \<leftarrow> ss1 . p' = pc+1] ++_f x) = ?s1"

92 (is "?map ss1 ++_f x = _" is "?sum ss1 = _")

93 by (simp split: split_if_asm)

94 from app less

95 have "?app ss2" by (blast dest: trans_r lesub_step_typeD)

96 moreover {

97 from ss1 have map1: "set (?map ss1) \<subseteq> A" by auto

98 with x have "?sum ss1 \<in> A" by (auto intro!: plusplus_closed semilat)

99 with sum have "?s1 \<in> A" by simp

100 moreover

101 have mapD: "\<And>x ss. x \<in> set (?map ss) \<Longrightarrow> \<exists>p. (p,x) \<in> set ss \<and> p=pc+1" by auto

102 from x map1

103 have "\<forall>x \<in> set (?map ss1). x <=_r ?sum ss1"

104 by clarify (rule pp_ub1)

105 with sum have "\<forall>x \<in> set (?map ss1). x <=_r ?s1" by simp

106 with less have "\<forall>x \<in> set (?map ss2). x <=_r ?s1"

107 by (fastsimp dest!: mapD lesub_step_typeD intro: trans_r)

108 moreover

109 from map1 x have "x <=_r (?sum ss1)" by (rule pp_ub2)

110 with sum have "x <=_r ?s1" by simp

111 moreover

112 from ss2 have "set (?map ss2) \<subseteq> A" by auto

113 ultimately

114 have "?sum ss2 <=_r ?s1" using x by - (rule pp_lub)

115 }

116 moreover

117 from x ss2 have

118 "?s2 =

119 (if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'

120 then map snd [(p', t') \<leftarrow> ss2 . p' = pc + 1] ++_f x

121 else \<top>)"

122 by (rule merge_def)

123 ultimately have ?thesis by simp

124 }

125 ultimately show ?thesis by (cases "?s1 = \<top>") auto

126 qed

129 lemma (in lbvc) wti_mono:

130 assumes less: "s2 <=_r s1"

131 assumes pc: "pc < length \<phi>"

132 assumes s1: "s1 \<in> A"

133 assumes s2: "s2 \<in> A"

134 shows "wti c pc s2 <=_r wti c pc s1" (is "?s2' <=_r ?s1'")

135 proof -

136 from mono pc s2 less have "step pc s2 <=|r| step pc s1" by (rule monoD)

137 moreover

138 from cert B_A pc have "c!Suc pc \<in> A" by (rule cert_okD3)

139 moreover

140 from pres s1 pc

141 have "snd`set (step pc s1) \<subseteq> A" by (rule pres_typeD2)

142 moreover

143 from pres s2 pc

144 have "snd`set (step pc s2) \<subseteq> A" by (rule pres_typeD2)

145 ultimately

146 show ?thesis by (simp add: wti merge_mono)

147 qed

149 lemma (in lbvc) wtc_mono:

150 assumes less: "s2 <=_r s1"

151 assumes pc: "pc < length \<phi>"

152 assumes s1: "s1 \<in> A"

153 assumes s2: "s2 \<in> A"

154 shows "wtc c pc s2 <=_r wtc c pc s1" (is "?s2' <=_r ?s1'")

155 proof (cases "c!pc = \<bottom>")

156 case True

157 moreover from less pc s1 s2 have "wti c pc s2 <=_r wti c pc s1" by (rule wti_mono)

158 ultimately show ?thesis by (simp add: wtc)

159 next

160 case False

161 have "?s1' = \<top> \<Longrightarrow> ?thesis" by simp

162 moreover {

163 assume "?s1' \<noteq> \<top>"

164 with False have c: "s1 <=_r c!pc" by (simp add: wtc split: split_if_asm)

165 with less have "s2 <=_r c!pc" ..

166 with False c have ?thesis by (simp add: wtc)

167 }

168 ultimately show ?thesis by (cases "?s1' = \<top>") auto

169 qed

172 lemma (in lbv) top_le_conv [simp]:

173 "\<top> <=_r x = (x = \<top>)"

174 by (insert semilat) (simp add: top top_le_conv)

176 lemma (in lbv) neq_top [simp, elim]:

177 "\<lbrakk> x <=_r y; y \<noteq> \<top> \<rbrakk> \<Longrightarrow> x \<noteq> \<top>"

178 by (cases "x = T") auto

181 lemma (in lbvc) stable_wti:

182 assumes stable: "stable r step \<phi> pc"

183 assumes pc: "pc < length \<phi>"

184 shows "wti c pc (\<phi>!pc) \<noteq> \<top>"

185 proof -

186 let ?step = "step pc (\<phi>!pc)"

187 from stable

188 have less: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def)

190 from cert B_A pc

191 have cert_suc: "c!Suc pc \<in> A" by (rule cert_okD3)

192 moreover

193 from phi pc have "\<phi>!pc \<in> A" by simp

194 from pres this pc

195 have stepA: "snd`set ?step \<subseteq> A" by (rule pres_typeD2)

196 ultimately

197 have "merge c pc ?step (c!Suc pc) =

198 (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'

199 then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc

200 else \<top>)" by (rule merge_def)

201 moreover {

202 fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"

203 with less have "s' <=_r \<phi>!pc'" by auto

204 also

205 from bounded pc s' have "pc' < length \<phi>" by (rule boundedD)

206 with s' suc_pc pc have "c!pc' = \<phi>!pc'" ..

207 hence "\<phi>!pc' = c!pc'" ..

208 finally have "s' <=_r c!pc'" .

209 } hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto

210 moreover

211 from pc have "Suc pc = length \<phi> \<or> Suc pc < length \<phi>" by auto

212 hence "map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc \<noteq> \<top>"

213 (is "?map ++_f _ \<noteq> _")

214 proof (rule disjE)

215 assume pc': "Suc pc = length \<phi>"

216 with cert have "c!Suc pc = \<bottom>" by (simp add: cert_okD2)

217 moreover

218 from pc' bounded pc

219 have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto)

220 hence "[(p',t') \<leftarrow> ?step.p'=pc+1] = []" by (blast intro: filter_False)

221 hence "?map = []" by simp

222 ultimately show ?thesis by (simp add: B_neq_T)

223 next

224 assume pc': "Suc pc < length \<phi>"

225 from pc' phi have "\<phi>!Suc pc \<in> A" by simp

226 moreover note cert_suc

227 moreover from stepA

228 have "set ?map \<subseteq> A" by auto

229 moreover

230 have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto

231 with less have "\<forall>s' \<in> set ?map. s' <=_r \<phi>!Suc pc" by auto

232 moreover

233 from pc' have "c!Suc pc <=_r \<phi>!Suc pc"

234 by (cases "c!Suc pc = \<bottom>") (auto dest: cert_approx)

235 ultimately

236 have "?map ++_f c!Suc pc <=_r \<phi>!Suc pc" by (rule pp_lub)

237 moreover

238 from pc' phi have "\<phi>!Suc pc \<noteq> \<top>" by simp

239 ultimately

240 show ?thesis by auto

241 qed

242 ultimately

243 have "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by simp

244 thus ?thesis by (simp add: wti)

245 qed

247 lemma (in lbvc) wti_less:

248 assumes stable: "stable r step \<phi> pc"

249 assumes suc_pc: "Suc pc < length \<phi>"

250 shows "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" (is "?wti <=_r _")

251 proof -

252 let ?step = "step pc (\<phi>!pc)"

254 from stable

255 have less: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def)

257 from suc_pc have pc: "pc < length \<phi>" by simp

258 with cert B_A have cert_suc: "c!Suc pc \<in> A" by (rule cert_okD3)

259 moreover

260 from phi pc have "\<phi>!pc \<in> A" by simp

261 with pres pc have stepA: "snd`set ?step \<subseteq> A" by - (rule pres_typeD2)

262 moreover

263 from stable pc have "?wti \<noteq> \<top>" by (rule stable_wti)

264 hence "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by (simp add: wti)

265 ultimately

266 have "merge c pc ?step (c!Suc pc) =

267 map snd [(p',t')\<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s)

268 hence "?wti = \<dots>" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti)

269 also {

270 from suc_pc phi have "\<phi>!Suc pc \<in> A" by simp

271 moreover note cert_suc

272 moreover from stepA have "set ?map \<subseteq> A" by auto

273 moreover

274 have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto

275 with less have "\<forall>s' \<in> set ?map. s' <=_r \<phi>!Suc pc" by auto

276 moreover

277 from suc_pc have "c!Suc pc <=_r \<phi>!Suc pc"

278 by (cases "c!Suc pc = \<bottom>") (auto dest: cert_approx)

279 ultimately

280 have "?sum <=_r \<phi>!Suc pc" by (rule pp_lub)

281 }

282 finally show ?thesis .

283 qed

285 lemma (in lbvc) stable_wtc:

286 assumes stable: "stable r step phi pc"

287 assumes pc: "pc < length \<phi>"

288 shows "wtc c pc (\<phi>!pc) \<noteq> \<top>"

289 proof -

290 from stable pc have wti: "wti c pc (\<phi>!pc) \<noteq> \<top>" by (rule stable_wti)

291 show ?thesis

292 proof (cases "c!pc = \<bottom>")

293 case True with wti show ?thesis by (simp add: wtc)

294 next

295 case False

296 with pc have "c!pc = \<phi>!pc" ..

297 with False wti show ?thesis by (simp add: wtc)

298 qed

299 qed

301 lemma (in lbvc) wtc_less:

302 assumes stable: "stable r step \<phi> pc"

303 assumes suc_pc: "Suc pc < length \<phi>"

304 shows "wtc c pc (\<phi>!pc) <=_r \<phi>!Suc pc" (is "?wtc <=_r _")

305 proof (cases "c!pc = \<bottom>")

306 case True

307 moreover from stable suc_pc have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc"

308 by (rule wti_less)

309 ultimately show ?thesis by (simp add: wtc)

310 next

311 case False

312 from suc_pc have pc: "pc < length \<phi>" by simp

313 with stable have "?wtc \<noteq> \<top>" by (rule stable_wtc)

314 with False have "?wtc = wti c pc (c!pc)"

315 by (unfold wtc) (simp split: split_if_asm)

316 also from pc False have "c!pc = \<phi>!pc" ..

317 finally have "?wtc = wti c pc (\<phi>!pc)" .

318 also from stable suc_pc have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less)

319 finally show ?thesis .

320 qed

323 lemma (in lbvc) wt_step_wtl_lemma:

324 assumes wt_step: "wt_step r \<top> step \<phi>"

325 shows "\<And>pc s. pc+length ls = length \<phi> \<Longrightarrow> s <=_r \<phi>!pc \<Longrightarrow> s \<in> A \<Longrightarrow> s\<noteq>\<top> \<Longrightarrow>

326 wtl ls c pc s \<noteq> \<top>"

327 (is "\<And>pc s. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?wtl ls pc s \<noteq> _")

328 proof (induct ls)

329 fix pc s assume "s\<noteq>\<top>" thus "?wtl [] pc s \<noteq> \<top>" by simp

330 next

331 fix pc s i ls

332 assume "\<And>pc s. pc+length ls=length \<phi> \<Longrightarrow> s <=_r \<phi>!pc \<Longrightarrow> s \<in> A \<Longrightarrow> s\<noteq>\<top> \<Longrightarrow>

333 ?wtl ls pc s \<noteq> \<top>"

334 moreover

335 assume pc_l: "pc + length (i#ls) = length \<phi>"

336 hence suc_pc_l: "Suc pc + length ls = length \<phi>" by simp

337 ultimately

338 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>" .

340 from pc_l obtain pc: "pc < length \<phi>" by simp

341 with wt_step have stable: "stable r step \<phi> pc" by (simp add: wt_step_def)

342 from this pc have wt_phi: "wtc c pc (\<phi>!pc) \<noteq> \<top>" by (rule stable_wtc)

343 assume s_phi: "s <=_r \<phi>!pc"

344 from phi pc have phi_pc: "\<phi>!pc \<in> A" by simp

345 assume s: "s \<in> A"

346 with s_phi pc phi_pc have wt_s_phi: "wtc c pc s <=_r wtc c pc (\<phi>!pc)" by (rule wtc_mono)

347 with wt_phi have wt_s: "wtc c pc s \<noteq> \<top>" by simp

348 moreover

349 assume s': "s \<noteq> \<top>"

350 ultimately

351 have "ls = [] \<Longrightarrow> ?wtl (i#ls) pc s \<noteq> \<top>" by simp

352 moreover {

353 assume "ls \<noteq> []"

354 with pc_l have suc_pc: "Suc pc < length \<phi>" by (auto simp add: neq_Nil_conv)

355 with stable have "wtc c pc (phi!pc) <=_r \<phi>!Suc pc" by (rule wtc_less)

356 with wt_s_phi have "wtc c pc s <=_r \<phi>!Suc pc" by (rule trans_r)

357 moreover

358 from cert suc_pc have "c!pc \<in> A" "c!(pc+1) \<in> A"

359 by (auto simp add: cert_ok_def)

360 from pres this s pc have "wtc c pc s \<in> A" by (rule wtc_pres)

361 ultimately

362 have "?wtl ls (Suc pc) (wtc c pc s) \<noteq> \<top>" using IH wt_s by blast

363 with s' wt_s have "?wtl (i#ls) pc s \<noteq> \<top>" by simp

364 }

365 ultimately show "?wtl (i#ls) pc s \<noteq> \<top>" by (cases ls) blast+

366 qed

369 theorem (in lbvc) wtl_complete:

370 assumes wt: "wt_step r \<top> step \<phi>"

371 and s: "s <=_r \<phi>!0" "s \<in> A" "s \<noteq> \<top>"

372 and len: "length ins = length phi"

373 shows "wtl ins c 0 s \<noteq> \<top>"

374 proof -

375 from len have "0+length ins = length phi" by simp

376 from wt this s show ?thesis by (rule wt_step_wtl_lemma)

377 qed

379 end