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

src/HOL/MicroJava/BV/LBVComplete.thy

author | webertj |

Mon Mar 07 19:30:53 2005 +0100 (2005-03-07) | |

changeset 15584 | 3478bb4f93ff |

parent 15425 | 6356d2523f73 |

child 16417 | 9bc16273c2d4 |

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

refute_params: default value itself=1 added (for type classes)

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 = LBVSpec + Typing_Framework:

11 constdefs

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

13 "is_target step phi pc' \<equiv>

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

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

17 "make_cert step phi B \<equiv>

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

20 constdefs

21 list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"

22 "list_ex P xs \<equiv> \<exists>x \<in> set xs. P x"

24 lemma [code]: "list_ex P [] = False" by (simp add: list_ex_def)

25 lemma [code]: "list_ex P (x#xs) = (P x \<or> list_ex P xs)" by (simp add: list_ex_def)

27 lemma [code]:

28 "is_target step phi pc' =

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

30 apply (simp add: list_ex_def is_target_def set_mem_eq)

31 apply force

32 done

34 locale (open) lbvc = lbv +

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

36 fixes c :: "'a list"

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

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

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

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

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

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

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

48 proof (unfold cert_ok_def, intro strip conjI)

49 note [simp] = make_cert_def cert_def nth_append

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

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

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

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

56 qed

58 lemmas [simp del] = split_paired_Ex

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

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

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

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

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

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

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

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

71 by (auto simp add: cert_def make_cert_def nth_append)

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

75 "x <=_r \<top>"

76 by (insert top) simp

79 lemma (in lbv) merge_mono:

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

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

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

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

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

85 proof-

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

87 moreover {

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

89 from x ss1 have "?s1 =

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

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

92 else \<top>)"

93 by (rule merge_def)

94 with merge obtain

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

96 (is "?app ss1") and

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

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

99 by (simp split: split_if_asm)

100 from app less

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

102 moreover {

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

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

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

106 moreover

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

108 from x map1

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

110 by clarify (rule pp_ub1)

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

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

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

114 moreover

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

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

117 moreover

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

119 ultimately

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

121 }

122 moreover

123 from x ss2 have

124 "?s2 =

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

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

127 else \<top>)"

128 by (rule merge_def)

129 ultimately have ?thesis by simp

130 }

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

132 qed

135 lemma (in lbvc) wti_mono:

136 assumes less: "s2 <=_r s1"

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

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

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

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

141 proof -

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

143 moreover

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

145 moreover

146 from pres s1 pc

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

148 moreover

149 from pres s2 pc

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

151 ultimately

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

153 qed

155 lemma (in lbvc) wtc_mono:

156 assumes less: "s2 <=_r s1"

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

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

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

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

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

162 case True

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

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

165 next

166 case False

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

168 moreover {

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

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

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

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

173 }

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

175 qed

178 lemma (in lbv) top_le_conv [simp]:

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

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

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

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

184 by (cases "x = T") auto

187 lemma (in lbvc) stable_wti:

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

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

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

191 proof -

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

193 from stable

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

196 from cert pc

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

198 moreover

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

200 with pres pc

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

202 ultimately

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

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

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

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

207 moreover {

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

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

210 also

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

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

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

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

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

216 moreover

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

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

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

220 proof (rule disjE)

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

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

223 moreover

224 from pc' bounded pc

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

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

227 hence "?map = []" by simp

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

229 next

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

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

232 moreover note cert_suc

233 moreover from stepA

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

235 moreover

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

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

238 moreover

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

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

241 ultimately

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

243 moreover

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

245 ultimately

246 show ?thesis by auto

247 qed

248 ultimately

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

250 thus ?thesis by (simp add: wti)

251 qed

253 lemma (in lbvc) wti_less:

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

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

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

257 proof -

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

260 from stable

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

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

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

265 moreover

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

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

268 moreover

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

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

271 ultimately

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

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

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

275 also {

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

277 moreover note cert_suc

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

279 moreover

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

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

282 moreover

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

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

285 ultimately

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

287 }

288 finally show ?thesis .

289 qed

291 lemma (in lbvc) stable_wtc:

292 assumes stable: "stable r step phi pc"

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

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

295 proof -

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

297 show ?thesis

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

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

300 next

301 case False

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

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

304 qed

305 qed

307 lemma (in lbvc) wtc_less:

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

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

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

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

312 case True

313 moreover have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less)

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

315 next

316 case False

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

318 hence "?wtc \<noteq> \<top>" by - (rule stable_wtc)

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

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

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

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

323 also have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less)

324 finally show ?thesis .

325 qed

328 lemma (in lbvc) wt_step_wtl_lemma:

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

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

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

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

333 proof (induct ls)

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

335 next

336 fix pc s i ls

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

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

339 moreover

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

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

342 ultimately

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

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

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

347 moreover

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

349 ultimately

350 have wt_phi: "wtc c pc (\<phi>!pc) \<noteq> \<top>" by - (rule stable_wtc)

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

353 moreover

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

355 ultimately

356 have wt_s_phi: "wtc c pc s <=_r wtc c pc (\<phi>!pc)" using s_phi by - (rule wtc_mono)

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

358 moreover

359 assume s: "s \<noteq> \<top>"

360 ultimately

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

362 moreover {

363 assume "ls \<noteq> []"

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

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

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

367 moreover

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

369 by (auto simp add: cert_ok_def)

370 with pres have "wtc c pc s \<in> A" by (rule wtc_pres)

371 ultimately

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

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

374 }

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

376 qed

379 theorem (in lbvc) wtl_complete:

380 assumes "wt_step r \<top> step \<phi>"

381 assumes "s <=_r \<phi>!0" and "s \<in> A" and "s \<noteq> \<top>" and "length ins = length phi"

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

383 proof -

384 have "0+length ins = length phi" by simp

385 thus ?thesis by - (rule wt_step_wtl_lemma)

386 qed

389 end