author  berghofe 
Mon, 11 Dec 2006 16:06:14 +0100  
changeset 21765  89275a3ed7be 
parent 20014  729a45534001 
child 23563  42f2f90b51a6 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/AxSem.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

4 
*) 

5 

6 
header {* Axiomatic semantics of Java expressions and statements 

7 
(see also Eval.thy) 

8 
*} 

9 

16417  10 
theory AxSem imports Evaln TypeSafe begin 
12854  11 

12 
text {* 

13 
design issues: 

14 
\begin{itemize} 

15 
\item a strong version of validity for triples with premises, namely one that 

16 
takes the recursive depth needed to complete execution, enables 

17 
correctness proof 

18 
\item auxiliary variables are handled firstclass (> Thomas Kleymann) 

19 
\item expressions not flattened to elementary assignments (as usual for 

20 
axiomatic semantics) but treated firstclass => explicit result value 

21 
handling 

22 
\item intermediate values not on triple, but on assertion level 

23 
(with result entry) 

24 
\item multiple results with semantical substitution mechnism not requiring a 

25 
stack 

26 
\item because of dynamic method binding, terms need to be dependent on state. 

27 
this is also useful for conditional expressions and statements 

28 
\item result values in triples exactly as in eval relation (also for xcpt 

29 
states) 

30 
\item validity: additional assumption of state conformance and welltypedness, 

31 
which is required for soundness and thus rule hazard required of completeness 

32 
\end{itemize} 

33 

34 
restrictions: 

35 
\begin{itemize} 

36 
\item all triples in a derivation are of the same type (due to weak 

37 
polymorphism) 

38 
\end{itemize} 

39 
*} 

40 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

41 
types res = vals {* result entry *} 
12854  42 
syntax 
43 
Val :: "val \<Rightarrow> res" 

44 
Var :: "var \<Rightarrow> res" 

45 
Vals :: "val list \<Rightarrow> res" 

46 
translations 

47 
"Val x" => "(In1 x)" 

48 
"Var x" => "(In2 x)" 

49 
"Vals x" => "(In3 x)" 

50 

51 
syntax 

52 
"Val_" :: "[pttrn] => pttrn" ("Val:_" [951] 950) 

53 
"Var_" :: "[pttrn] => pttrn" ("Var:_" [951] 950) 

54 
"Vals_" :: "[pttrn] => pttrn" ("Vals:_" [951] 950) 

55 

56 
translations 

57 
"\<lambda>Val:v . b" == "(\<lambda>v. b) \<circ> the_In1" 

58 
"\<lambda>Var:v . b" == "(\<lambda>v. b) \<circ> the_In2" 

59 
"\<lambda>Vals:v. b" == "(\<lambda>v. b) \<circ> the_In3" 

60 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

61 
{* relation on result values, state and auxiliary variables *} 
12854  62 
types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool" 
63 
translations 

64 
"res" <= (type) "AxSem.res" 

65 
"a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> a \<Rightarrow> bool" 

66 

67 
constdefs 

68 
assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25) 

69 
"P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z" 

70 

71 
lemma assn_imp_def2 [iff]: "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)" 

72 
apply (unfold assn_imp_def) 

73 
apply (rule HOL.refl) 

74 
done 

75 

76 

77 
section "assertion transformers" 

78 

79 
subsection "peekand" 

80 

81 
constdefs 

82 
peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13) 

83 
"P \<and>. p \<equiv> \<lambda>Y s Z. P Y s Z \<and> p s" 

84 

85 
lemma peek_and_def2 [simp]: "peek_and P p Y s = (\<lambda>Z. (P Y s Z \<and> p s))" 

86 
apply (unfold peek_and_def) 

87 
apply (simp (no_asm)) 

88 
done 

89 

90 
lemma peek_and_Not [simp]: "(P \<and>. (\<lambda>s. \<not> f s)) = (P \<and>. Not \<circ> f)" 

91 
apply (rule ext) 

92 
apply (rule ext) 

93 
apply (simp (no_asm)) 

94 
done 

95 

96 
lemma peek_and_and [simp]: "peek_and (peek_and P p) p = peek_and P p" 

97 
apply (unfold peek_and_def) 

98 
apply (simp (no_asm)) 

99 
done 

100 

101 
lemma peek_and_commut: "(P \<and>. p \<and>. q) = (P \<and>. q \<and>. p)" 

102 
apply (rule ext) 

103 
apply (rule ext) 

104 
apply (rule ext) 

105 
apply auto 

106 
done 

107 

108 
syntax 

109 
Normal :: "'a assn \<Rightarrow> 'a assn" 

110 
translations 

111 
"Normal P" == "P \<and>. normal" 

112 

113 
lemma peek_and_Normal [simp]: "peek_and (Normal P) p = Normal (peek_and P p)" 

114 
apply (rule ext) 

115 
apply (rule ext) 

116 
apply (rule ext) 

117 
apply auto 

118 
done 

119 

120 
subsection "assnsupd" 

121 

122 
constdefs 

123 
assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13) 

124 
"P ;. f \<equiv> \<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s" 

125 

126 
lemma assn_supd_def2 [simp]: "assn_supd P f Y s' Z = (\<exists>s. P Y s Z \<and> s' = f s)" 

127 
apply (unfold assn_supd_def) 

128 
apply (simp (no_asm)) 

129 
done 

130 

131 
subsection "supdassn" 

132 

133 
constdefs 

134 
supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13) 

135 
"f .; P \<equiv> \<lambda>Y s. P Y (f s)" 

136 

137 

138 
lemma supd_assn_def2 [simp]: "(f .; P) Y s = P Y (f s)" 

139 
apply (unfold supd_assn_def) 

140 
apply (simp (no_asm)) 

141 
done 

142 

143 
lemma supd_assn_supdD [elim]: "((f .; Q) ;. f) Y s Z \<Longrightarrow> Q Y s Z" 

144 
apply auto 

145 
done 

146 

147 
lemma supd_assn_supdI [elim]: "Q Y s Z \<Longrightarrow> (f .; (Q ;. f)) Y s Z" 

148 
apply (auto simp del: split_paired_Ex) 

149 
done 

150 

151 
subsection "substres" 

152 

153 
constdefs 

154 
subst_res :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<leftarrow>_" [60,61] 60) 

155 
"P\<leftarrow>w \<equiv> \<lambda>Y. P w" 

156 

157 
lemma subst_res_def2 [simp]: "(P\<leftarrow>w) Y = P w" 

158 
apply (unfold subst_res_def) 

159 
apply (simp (no_asm)) 

160 
done 

161 

162 
lemma subst_subst_res [simp]: "P\<leftarrow>w\<leftarrow>v = P\<leftarrow>w" 

163 
apply (rule ext) 

164 
apply (simp (no_asm)) 

165 
done 

166 

167 
lemma peek_and_subst_res [simp]: "(P \<and>. p)\<leftarrow>w = (P\<leftarrow>w \<and>. p)" 

168 
apply (rule ext) 

169 
apply (rule ext) 

170 
apply (simp (no_asm)) 

171 
done 

172 

173 
(*###Do not work for some strange (unification?) reason 

174 
lemma subst_res_Val_beta [simp]: "(\<lambda>Y. P (the_In1 Y))\<leftarrow>Val v = (\<lambda>Y. P v)" 

175 
apply (rule ext) 

176 
by simp 

177 

178 
lemma subst_res_Var_beta [simp]: "(\<lambda>Y. P (the_In2 Y))\<leftarrow>Var vf = (\<lambda>Y. P vf)"; 

179 
apply (rule ext) 

180 
by simp 

181 

182 
lemma subst_res_Vals_beta [simp]: "(\<lambda>Y. P (the_In3 Y))\<leftarrow>Vals vs = (\<lambda>Y. P vs)"; 

183 
apply (rule ext) 

184 
by simp 

185 
*) 

186 

187 
subsection "substBool" 

188 

189 
constdefs 

190 
subst_Bool :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<leftarrow>=_" [60,61] 60) 

191 
"P\<leftarrow>=b \<equiv> \<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b)" 

192 

193 
lemma subst_Bool_def2 [simp]: 

194 
"(P\<leftarrow>=b) Y s Z = (\<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))" 

195 
apply (unfold subst_Bool_def) 

196 
apply (simp (no_asm)) 

197 
done 

198 

199 
lemma subst_Bool_the_BoolI: "P (Val b) s Z \<Longrightarrow> (P\<leftarrow>=the_Bool b) Y s Z" 

200 
apply auto 

201 
done 

202 

203 
subsection "peekres" 

204 

205 
constdefs 

206 
peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" 

207 
"peek_res Pf \<equiv> \<lambda>Y. Pf Y Y" 

208 

209 
syntax 

210 
"@peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_:. _" [0,3] 3) 

211 
translations 

212 
"\<lambda>w:. P" == "peek_res (\<lambda>w. P)" 

213 

214 
lemma peek_res_def2 [simp]: "peek_res P Y = P Y Y" 

215 
apply (unfold peek_res_def) 

216 
apply (simp (no_asm)) 

217 
done 

218 

219 
lemma peek_res_subst_res [simp]: "peek_res P\<leftarrow>w = P w\<leftarrow>w" 

220 
apply (rule ext) 

221 
apply (simp (no_asm)) 

222 
done 

223 

224 
(* unused *) 

225 
lemma peek_subst_res_allI: 

226 
"(\<And>a. T a (P (f a)\<leftarrow>f a)) \<Longrightarrow> \<forall>a. T a (peek_res P\<leftarrow>f a)" 

227 
apply (rule allI) 

228 
apply (simp (no_asm)) 

229 
apply fast 

230 
done 

231 

232 
subsection "ignres" 

233 

234 
constdefs 

235 
ign_res :: " 'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000) 

236 
"P\<down> \<equiv> \<lambda>Y s Z. \<exists>Y. P Y s Z" 

237 

238 
lemma ign_res_def2 [simp]: "P\<down> Y s Z = (\<exists>Y. P Y s Z)" 

239 
apply (unfold ign_res_def) 

240 
apply (simp (no_asm)) 

241 
done 

242 

243 
lemma ign_ign_res [simp]: "P\<down>\<down> = P\<down>" 

244 
apply (rule ext) 

245 
apply (rule ext) 

246 
apply (rule ext) 

247 
apply (simp (no_asm)) 

248 
done 

249 

250 
lemma ign_subst_res [simp]: "P\<down>\<leftarrow>w = P\<down>" 

251 
apply (rule ext) 

252 
apply (rule ext) 

253 
apply (rule ext) 

254 
apply (simp (no_asm)) 

255 
done 

256 

257 
lemma peek_and_ign_res [simp]: "(P \<and>. p)\<down> = (P\<down> \<and>. p)" 

258 
apply (rule ext) 

259 
apply (rule ext) 

260 
apply (rule ext) 

261 
apply (simp (no_asm)) 

262 
done 

263 

264 
subsection "peekst" 

265 

266 
constdefs 

267 
peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" 

268 
"peek_st P \<equiv> \<lambda>Y s. P (store s) Y s" 

269 

270 
syntax 

271 
"@peek_st" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_.. _" [0,3] 3) 

272 
translations 

273 
"\<lambda>s.. P" == "peek_st (\<lambda>s. P)" 

274 

275 
lemma peek_st_def2 [simp]: "(\<lambda>s.. Pf s) Y s = Pf (store s) Y s" 

276 
apply (unfold peek_st_def) 

277 
apply (simp (no_asm)) 

278 
done 

279 

280 
lemma peek_st_triv [simp]: "(\<lambda>s.. P) = P" 

281 
apply (rule ext) 

282 
apply (rule ext) 

283 
apply (simp (no_asm)) 

284 
done 

285 

286 
lemma peek_st_st [simp]: "(\<lambda>s.. \<lambda>s'.. P s s') = (\<lambda>s.. P s s)" 

287 
apply (rule ext) 

288 
apply (rule ext) 

289 
apply (simp (no_asm)) 

290 
done 

291 

292 
lemma peek_st_split [simp]: "(\<lambda>s.. \<lambda>Y s'. P s Y s') = (\<lambda>Y s. P (store s) Y s)" 

293 
apply (rule ext) 

294 
apply (rule ext) 

295 
apply (simp (no_asm)) 

296 
done 

297 

298 
lemma peek_st_subst_res [simp]: "(\<lambda>s.. P s)\<leftarrow>w = (\<lambda>s.. P s\<leftarrow>w)" 

299 
apply (rule ext) 

300 
apply (simp (no_asm)) 

301 
done 

302 

303 
lemma peek_st_Normal [simp]: "(\<lambda>s..(Normal (P s))) = Normal (\<lambda>s.. P s)" 

304 
apply (rule ext) 

305 
apply (rule ext) 

306 
apply (simp (no_asm)) 

307 
done 

308 

309 
subsection "ignreseq" 

310 

311 
constdefs 

312 
ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>=_" [60,61] 60) 

313 
"P\<down>=w \<equiv> \<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w)" 

314 

315 
lemma ign_res_eq_def2 [simp]: "(P\<down>=w) Y s Z = ((\<exists>Y. P Y s Z) \<and> Y=w)" 

316 
apply (unfold ign_res_eq_def) 

317 
apply auto 

318 
done 

319 

320 
lemma ign_ign_res_eq [simp]: "(P\<down>=w)\<down> = P\<down>" 

321 
apply (rule ext) 

322 
apply (rule ext) 

323 
apply (rule ext) 

324 
apply (simp (no_asm)) 

325 
done 

326 

327 
(* unused *) 

328 
lemma ign_res_eq_subst_res: "P\<down>=w\<leftarrow>w = P\<down>" 

329 
apply (rule ext) 

330 
apply (rule ext) 

331 
apply (rule ext) 

332 
apply (simp (no_asm)) 

333 
done 

334 

335 
(* unused *) 

336 
lemma subst_Bool_ign_res_eq: "((P\<leftarrow>=b)\<down>=x) Y s Z = ((P\<leftarrow>=b) Y s Z \<and> Y=x)" 

337 
apply (simp (no_asm)) 

338 
done 

339 

340 
subsection "RefVar" 

341 

342 
constdefs 

343 
RefVar :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn"(infixr "..;" 13) 

344 
"vf ..; P \<equiv> \<lambda>Y s. let (v,s') = vf s in P (Var v) s'" 

345 

346 
lemma RefVar_def2 [simp]: "(vf ..; P) Y s = 

347 
P (Var (fst (vf s))) (snd (vf s))" 

348 
apply (unfold RefVar_def Let_def) 

349 
apply (simp (no_asm) add: split_beta) 

350 
done 

351 

352 
subsection "allocation" 

353 

354 
constdefs 

355 
Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn" 

356 
"Alloc G otag P \<equiv> \<lambda>Y s Z. 

357 
\<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z" 

358 

359 
SXAlloc :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn" 

360 
"SXAlloc G P \<equiv> \<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z" 

361 

362 

363 
lemma Alloc_def2 [simp]: "Alloc G otag P Y s Z = 

364 
(\<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z)" 

365 
apply (unfold Alloc_def) 

366 
apply (simp (no_asm)) 

367 
done 

368 

369 
lemma SXAlloc_def2 [simp]: 

370 
"SXAlloc G P Y s Z = (\<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z)" 

371 
apply (unfold SXAlloc_def) 

372 
apply (simp (no_asm)) 

373 
done 

374 

375 
section "validity" 

376 

377 
constdefs 

378 
type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

379 
"type_ok G t s \<equiv> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

380 
\<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

381 
\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A ) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

382 
\<and> s\<Colon>\<preceq>(G,L)" 
12854  383 

384 
datatype 'a triple = triple "('a assn)" "term" "('a assn)" (** should be 

385 
something like triple = \<forall>'a. triple ('a assn) term ('a assn) **) 

386 
("{(1_)}/ _>/ {(1_)}" [3,65,3]75) 

387 
types 'a triples = "'a triple set" 

388 

389 
syntax 

390 

391 
var_triple :: "['a assn, var ,'a assn] \<Rightarrow> 'a triple" 

392 
("{(1_)}/ _=>/ {(1_)}" [3,80,3] 75) 

393 
expr_triple :: "['a assn, expr ,'a assn] \<Rightarrow> 'a triple" 

394 
("{(1_)}/ _>/ {(1_)}" [3,80,3] 75) 

395 
exprs_triple :: "['a assn, expr list ,'a assn] \<Rightarrow> 'a triple" 

396 
("{(1_)}/ _#>/ {(1_)}" [3,65,3] 75) 

397 
stmt_triple :: "['a assn, stmt, 'a assn] \<Rightarrow> 'a triple" 

398 
("{(1_)}/ ._./ {(1_)}" [3,65,3] 75) 

399 

400 
syntax (xsymbols) 

401 

402 
triple :: "['a assn, term ,'a assn] \<Rightarrow> 'a triple" 

403 
("{(1_)}/ _\<succ>/ {(1_)}" [3,65,3] 75) 

404 
var_triple :: "['a assn, var ,'a assn] \<Rightarrow> 'a triple" 

405 
("{(1_)}/ _=\<succ>/ {(1_)}" [3,80,3] 75) 

406 
expr_triple :: "['a assn, expr ,'a assn] \<Rightarrow> 'a triple" 

407 
("{(1_)}/ _\<succ>/ {(1_)}" [3,80,3] 75) 

408 
exprs_triple :: "['a assn, expr list ,'a assn] \<Rightarrow> 'a triple" 

409 
("{(1_)}/ _\<doteq>\<succ>/ {(1_)}" [3,65,3] 75) 

410 

411 
translations 

412 
"{P} e\<succ> {Q}" == "{P} In1l e\<succ> {Q}" 

413 
"{P} e=\<succ> {Q}" == "{P} In2 e\<succ> {Q}" 

414 
"{P} e\<doteq>\<succ> {Q}" == "{P} In3 e\<succ> {Q}" 

415 
"{P} .c. {Q}" == "{P} In1r c\<succ> {Q}" 

416 

417 
lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})" 

13585  418 
apply (rule inj_onI) 
12854  419 
apply auto 
420 
done 

421 

422 
lemma triple_inj_eq: "({P} t\<succ> {Q} = {P'} t'\<succ> {Q'} ) = (P=P' \<and> t=t' \<and> Q=Q')" 

423 
apply auto 

424 
done 

425 

426 
constdefs 

427 
mtriples :: "('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<Rightarrow> 'sig \<Rightarrow> expr) \<Rightarrow> 

428 
('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<times> 'sig) set \<Rightarrow> 'a triples" 

429 
("{{(1_)}/ _\<succ>/ {(1_)}  _}"[3,65,3,65]75) 

430 
"{{P} tf\<succ> {Q}  ms} \<equiv> (\<lambda>(C,sig). {Normal(P C sig)} tf C sig\<succ> {Q C sig})`ms" 

431 

432 
consts 

433 

434 
triple_valid :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool" 

435 
( "_\<Turnstile>_:_" [61,0, 58] 57) 

436 
ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool" 

437 
("_,_\<Turnstile>_" [61,58,58] 57) 

438 

439 
syntax 

440 

441 
triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool" 

442 
( "_=_:_" [61,0, 58] 57) 

443 
ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool" 

444 
( "_,_=_" [61,58,58] 57) 

445 

446 
syntax (xsymbols) 

447 

448 
triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool" 

449 
( "_\<Turnstile>_:_" [61,0, 58] 57) 

450 
ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool" 

451 
( "_,_\<Turnstile>_" [61,58,58] 57) 

452 

453 
defs triple_valid_def: "G\<Turnstile>n:t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow> 

454 
\<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow> 

455 
(\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z)" 

456 
translations "G\<Turnstile>n:ts" == "Ball ts (triple_valid G n)" 

457 
defs ax_valids_def:"G,A\<Turnstile>ts \<equiv> \<forall>n. G\<Turnstile>n:A \<longrightarrow> G\<Turnstile>n:ts" 

458 
translations "G,A \<Turnstile>t" == "G,A\<Turnstile>{t}" 

459 

460 
lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} = 

461 
(\<forall>Y s Z. P Y s Z 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

462 
\<longrightarrow> (\<exists>L. (normal s \<longrightarrow> (\<exists> C T A. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

463 
\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<and> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

464 
s\<Colon>\<preceq>(G,L)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

465 
\<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow> Q Y' s' Z))" 
12854  466 
apply (unfold triple_valid_def type_ok_def) 
467 
apply (simp (no_asm)) 

468 
done 

469 

470 

471 
declare split_paired_All [simp del] split_paired_Ex [simp del] 

472 
declare split_if [split del] split_if_asm [split del] 

473 
option.split [split del] option.split_asm [split del] 

474 
ML_setup {* 

17876  475 
change_simpset (fn ss => ss delloop "split_all_tac"); 
476 
change_claset (fn cs => cs delSWrapper "split_all_tac"); 

12854  477 
*} 
478 

21765  479 
inductive2 
480 
ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_\<turnstile>_" [61,58,58] 57) 

481 
and ax_deriv :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple \<Rightarrow> bool" ("_,_\<turnstile>_" [61,58,58] 57) 

482 
for G :: prog 

483 
where 

12854  484 

21765  485 
"G,A \<turnstile>t \<equiv> G,A\<turnstile>{t}" 
486 

487 
 empty: " G,A\<turnstile>{}" 

488 
 insert:"\<lbrakk>G,A\<turnstile>t; G,A\<turnstile>ts\<rbrakk> \<Longrightarrow> 

12854  489 
G,A\<turnstile>insert t ts" 
490 

21765  491 
 asm: "ts\<subseteq>A \<Longrightarrow> G,A\<turnstile>ts" 
12854  492 

493 
(* could be added for convenience and efficiency, but is not necessary 

494 
cut: "\<lbrakk>G,A'\<turnstile>ts; G,A\<turnstile>A'\<rbrakk> \<Longrightarrow> 

495 
G,A \<turnstile>ts" 

496 
*) 

21765  497 
 weaken:"\<lbrakk>G,A\<turnstile>ts'; ts \<subseteq> ts'\<rbrakk> \<Longrightarrow> G,A\<turnstile>ts" 
12854  498 

21765  499 
 conseq:"\<forall>Y s Z . P Y s Z \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'. 
12854  500 
(\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> 
501 
Q Y' s' Z )) 

502 
\<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }" 

503 

21765  504 
 hazard:"G,A\<turnstile>{P \<and>. Not \<circ> type_ok G t} t\<succ> {Q}" 
12854  505 

21765  506 
 Abrupt: "G,A\<turnstile>{P\<leftarrow>(arbitrary3 t) \<and>. Not \<circ> normal} t\<succ> {P}" 
12854  507 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

508 
{* variables *} 
21765  509 
 LVar: " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}" 
12854  510 

21765  511 
 FVar: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Q}; 
12854  512 
G,A\<turnstile>{Q} e\<succ> {\<lambda>Val:a:. fvar C stat fn a ..; R}\<rbrakk> \<Longrightarrow> 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

513 
G,A\<turnstile>{Normal P} {accC,C,stat}e..fn=\<succ> {R}" 
12854  514 

21765  515 
 AVar: "\<lbrakk>G,A\<turnstile>{Normal P} e1\<succ> {Q}; 
12854  516 
\<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} e2\<succ> {\<lambda>Val:i:. avar G i a ..; R}\<rbrakk> \<Longrightarrow> 
517 
G,A\<turnstile>{Normal P} e1.[e2]=\<succ> {R}" 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

518 
{* expressions *} 
12854  519 

21765  520 
 NewC: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Alloc G (CInst C) Q}\<rbrakk> \<Longrightarrow> 
12854  521 
G,A\<turnstile>{Normal P} NewC C\<succ> {Q}" 
522 

21765  523 
 NewA: "\<lbrakk>G,A\<turnstile>{Normal P} .init_comp_ty T. {Q}; G,A\<turnstile>{Q} e\<succ> 
12854  524 
{\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}\<rbrakk> \<Longrightarrow> 
525 
G,A\<turnstile>{Normal P} New T[e]\<succ> {R}" 

526 

21765  527 
 Cast: "\<lbrakk>G,A\<turnstile>{Normal P} e\<succ> {\<lambda>Val:v:. \<lambda>s.. 
12854  528 
abupd (raise_if (\<not>G,s\<turnstile>v fits T) ClassCast) .; Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow> 
529 
G,A\<turnstile>{Normal P} Cast T e\<succ> {Q}" 

530 

21765  531 
 Inst: "\<lbrakk>G,A\<turnstile>{Normal P} e\<succ> {\<lambda>Val:v:. \<lambda>s.. 
12854  532 
Q\<leftarrow>Val (Bool (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T))}\<rbrakk> \<Longrightarrow> 
533 
G,A\<turnstile>{Normal P} e InstOf T\<succ> {Q}" 

534 

21765  535 
 Lit: "G,A\<turnstile>{Normal (P\<leftarrow>Val v)} Lit v\<succ> {P}" 
12854  536 

21765  537 
 UnOp: "\<lbrakk>G,A\<turnstile>{Normal P} e\<succ> {\<lambda>Val:v:. Q\<leftarrow>Val (eval_unop unop v)}\<rbrakk> 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

538 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

539 
G,A\<turnstile>{Normal P} UnOp unop e\<succ> {Q}" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

540 

21765  541 
 BinOp: 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

542 
"\<lbrakk>G,A\<turnstile>{Normal P} e1\<succ> {Q}; 
13384  543 
\<forall>v1. G,A\<turnstile>{Q\<leftarrow>Val v1} 
544 
(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))\<succ> 

545 
{\<lambda>Val:v2:. R\<leftarrow>Val (eval_binop binop v1 v2)}\<rbrakk> 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

546 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

547 
G,A\<turnstile>{Normal P} BinOp binop e1 e2\<succ> {R}" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

548 

21765  549 
 Super:" G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Val (val_this s))} Super\<succ> {P}" 
12854  550 

21765  551 
 Acc: "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f):. Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow> 
12854  552 
G,A\<turnstile>{Normal P} Acc va\<succ> {Q}" 
553 

21765  554 
 Ass: "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {Q}; 
12854  555 
\<forall>vf. G,A\<turnstile>{Q\<leftarrow>Var vf} e\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R}\<rbrakk> \<Longrightarrow> 
556 
G,A\<turnstile>{Normal P} va:=e\<succ> {R}" 

557 

21765  558 
 Cond: "\<lbrakk>G,A \<turnstile>{Normal P} e0\<succ> {P'}; 
12854  559 
\<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} (if b then e1 else e2)\<succ> {Q}\<rbrakk> \<Longrightarrow> 
560 
G,A\<turnstile>{Normal P} e0 ? e1 : e2\<succ> {Q}" 

561 

21765  562 
 Call: 
12854  563 
"\<lbrakk>G,A\<turnstile>{Normal P} e\<succ> {Q}; \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {R a}; 
564 
\<forall>a vs invC declC l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>. 

565 
(\<lambda>s. declC=invocation_declclass G mode (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> \<and> 

566 
invC = invocation_class mode (store s) a statT \<and> 

567 
l = locals (store s)) ;. 

568 
init_lvars G declC \<lparr>name=mn,parTs=pTs\<rparr> mode a vs) \<and>. 

569 
(\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)} 

570 
Methd declC \<lparr>name=mn,parTs=pTs\<rparr>\<succ> {set_lvars l .; S}\<rbrakk> \<Longrightarrow> 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

571 
G,A\<turnstile>{Normal P} {accC,statT,mode}e\<cdot>mn({pTs}args)\<succ> {S}" 
12854  572 

21765  573 
 Methd:"\<lbrakk>G,A\<union> {{P} Methd\<succ> {Q}  ms} \<turnstile> {{P} body G\<succ> {Q}  ms}\<rbrakk> \<Longrightarrow> 
12854  574 
G,A\<turnstile>{{P} Methd\<succ> {Q}  ms}" 
575 

21765  576 
 Body: "\<lbrakk>G,A\<turnstile>{Normal P} .Init D. {Q}; 
12854  577 
G,A\<turnstile>{Q} .c. {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>(In1 (the (locals s Result)))}\<rbrakk> 
578 
\<Longrightarrow> 

579 
G,A\<turnstile>{Normal P} Body D c\<succ> {R}" 

580 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

581 
{* expression lists *} 
12854  582 

21765  583 
 Nil: "G,A\<turnstile>{Normal (P\<leftarrow>Vals [])} []\<doteq>\<succ> {P}" 
12854  584 

21765  585 
 Cons: "\<lbrakk>G,A\<turnstile>{Normal P} e\<succ> {Q}; 
12854  586 
\<forall>v. G,A\<turnstile>{Q\<leftarrow>Val v} es\<doteq>\<succ> {\<lambda>Vals:vs:. R\<leftarrow>Vals (v#vs)}\<rbrakk> \<Longrightarrow> 
587 
G,A\<turnstile>{Normal P} e#es\<doteq>\<succ> {R}" 

588 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

589 
{* statements *} 
12854  590 

21765  591 
 Skip: "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit>)} .Skip. {P}" 
12854  592 

21765  593 
 Expr: "\<lbrakk>G,A\<turnstile>{Normal P} e\<succ> {Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow> 
12854  594 
G,A\<turnstile>{Normal P} .Expr e. {Q}" 
595 

21765  596 
 Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb l) .; Q}\<rbrakk> \<Longrightarrow> 
12854  597 
G,A\<turnstile>{Normal P} .l\<bullet> c. {Q}" 
598 

21765  599 
 Comp: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q}; 
12854  600 
G,A\<turnstile>{Q} .c2. {R}\<rbrakk> \<Longrightarrow> 
601 
G,A\<turnstile>{Normal P} .c1;;c2. {R}" 

602 

21765  603 
 If: "\<lbrakk>G,A \<turnstile>{Normal P} e\<succ> {P'}; 
12854  604 
\<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c1 else c2). {Q}\<rbrakk> \<Longrightarrow> 
605 
G,A\<turnstile>{Normal P} .If(e) c1 Else c2. {Q}" 

606 
(* unfolding variant of Loop, not needed here 

607 
LoopU:"\<lbrakk>G,A \<turnstile>{Normal P} e\<succ> {P'}; 

608 
\<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c;;While(e) c else Skip).{Q}\<rbrakk> 

609 
\<Longrightarrow> G,A\<turnstile>{Normal P} .While(e) c. {Q}" 

610 
*) 

21765  611 
 Loop: "\<lbrakk>G,A\<turnstile>{P} e\<succ> {P'}; 
12854  612 
G,A\<turnstile>{Normal (P'\<leftarrow>=True)} .c. {abupd (absorb (Cont l)) .; P}\<rbrakk> \<Longrightarrow> 
613 
G,A\<turnstile>{P} .l\<bullet> While(e) c. {(P'\<leftarrow>=False)\<down>=\<diamondsuit>}" 

614 

21765  615 
 Jmp: "G,A\<turnstile>{Normal (abupd (\<lambda>a. (Some (Jump j))) .; P\<leftarrow>\<diamondsuit>)} .Jmp j. {P}" 
12854  616 

21765  617 
 Throw:"\<lbrakk>G,A\<turnstile>{Normal P} e\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow> 
12854  618 
G,A\<turnstile>{Normal P} .Throw e. {Q}" 
619 

21765  620 
 Try: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {SXAlloc G Q}; 
12854  621 
G,A\<turnstile>{Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn} .c2. {R}; 
622 
(Q \<and>. (\<lambda>s. \<not>G,s\<turnstile>catch C)) \<Rightarrow> R\<rbrakk> \<Longrightarrow> 

623 
G,A\<turnstile>{Normal P} .Try c1 Catch(C vn) c2. {R}" 

624 

21765  625 
 Fin: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q}; 
12854  626 
\<forall>x. G,A\<turnstile>{Q \<and>. (\<lambda>s. x = fst s) ;. abupd (\<lambda>x. None)} 
627 
.c2. {abupd (abrupt_if (x\<noteq>None) x) .; R}\<rbrakk> \<Longrightarrow> 

628 
G,A\<turnstile>{Normal P} .c1 Finally c2. {R}" 

629 

21765  630 
 Done: "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P}" 
12854  631 

21765  632 
 Init: "\<lbrakk>the (class G C) = c; 
12854  633 
G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))} 
634 
.(if C = Object then Skip else Init (super c)). {Q}; 

635 
\<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty} 

636 
.init c. {set_lvars l .; R}\<rbrakk> \<Longrightarrow> 

637 
G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}" 

638 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

639 
 {* Some dummy rules for the intermediate terms @{text Callee}, 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

640 
@{text InsInitE}, @{text InsInitV}, @{text FinA} only used by the smallstep 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

641 
semantics. 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

642 
*} 
21765  643 
 InsInitV: " G,A\<turnstile>{Normal P} InsInitV c v=\<succ> {Q}" 
644 
 InsInitE: " G,A\<turnstile>{Normal P} InsInitE c e\<succ> {Q}" 

645 
 Callee: " G,A\<turnstile>{Normal P} Callee l e\<succ> {Q}" 

646 
 FinA: " G,A\<turnstile>{Normal P} .FinA a c. {Q}" 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

647 
(* 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

648 
axioms 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

649 
*) 
12854  650 

651 
constdefs 

652 
adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" 

653 
"adapt_pre P Q Q'\<equiv>\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z)" 

654 

655 

656 
section "rules derived by induction" 

657 

658 
lemma cut_valid: "\<lbrakk>G,A'\<Turnstile>ts; G,A\<Turnstile>A'\<rbrakk> \<Longrightarrow> G,A\<Turnstile>ts" 

659 
apply (unfold ax_valids_def) 

660 
apply fast 

661 
done 

662 

663 
(*if cut is available 

664 
Goal "\<lbrakk>G,A'\<turnstile>ts; A' \<subseteq> A; \<forall>P Q t. {P} t\<succ> {Q} \<in> A' \<longrightarrow> (\<exists>T. (G,L)\<turnstile>t\<Colon>T) \<rbrakk> \<Longrightarrow> 

665 
G,A\<turnstile>ts" 

666 
b y etac ax_derivs.cut 1; 

667 
b y eatac ax_derivs.asm 1 1; 

668 
qed "ax_thin"; 

669 
*) 

670 
lemma ax_thin [rule_format (no_asm)]: 

671 
"G,(A'::'a triple set)\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A\<turnstile>ts" 

672 
apply (erule ax_derivs.induct) 

673 
apply (tactic "ALLGOALS(EVERY'[Clarify_tac,REPEAT o smp_tac 1])") 

674 
apply (rule ax_derivs.empty) 

675 
apply (erule (1) ax_derivs.insert) 

676 
apply (fast intro: ax_derivs.asm) 

677 
(*apply (fast intro: ax_derivs.cut) *) 

678 
apply (fast intro: ax_derivs.weaken) 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

679 
apply (rule ax_derivs.conseq, intro strip, tactic "smp_tac 3 1",clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

680 
(* 37 subgoals *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

681 
prefer 18 (* Methd *) 
12854  682 
apply (rule ax_derivs.Methd, drule spec, erule mp, fast) 
683 
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 

684 
THEN_ALL_NEW Blast_tac) *}) 

685 
apply (erule ax_derivs.Call) 

686 
apply clarify 

687 
apply blast 

688 

689 
apply (rule allI)+ 

690 
apply (drule spec)+ 

691 
apply blast 

692 
done 

693 

694 
lemma ax_thin_insert: "G,(A::'a triple set)\<turnstile>(t::'a triple) \<Longrightarrow> G,insert x A\<turnstile>t" 

695 
apply (erule ax_thin) 

696 
apply fast 

697 
done 

698 

699 
lemma subset_mtriples_iff: 

700 
"ts \<subseteq> {{P} mb\<succ> {Q}  ms} = (\<exists>ms'. ms'\<subseteq>ms \<and> ts = {{P} mb\<succ> {Q}  ms'})" 

701 
apply (unfold mtriples_def) 

702 
apply (rule subset_image_iff) 

703 
done 

704 

705 
lemma weaken: 

706 
"G,(A::'a triple set)\<turnstile>(ts'::'a triple set) \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A\<turnstile>ts" 

707 
apply (erule ax_derivs.induct) 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

708 
(*42 subgoals*) 
12854  709 
apply (tactic "ALLGOALS strip_tac") 
710 
apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"), 

711 
etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*}) 

712 
apply (tactic "TRYALL hyp_subst_tac") 

713 
apply (simp, rule ax_derivs.empty) 

714 
apply (drule subset_insertD) 

715 
apply (blast intro: ax_derivs.insert) 

716 
apply (fast intro: ax_derivs.asm) 

717 
(*apply (blast intro: ax_derivs.cut) *) 

718 
apply (fast intro: ax_derivs.weaken) 

719 
apply (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *)) 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

720 
(*37 subgoals*) 
12854  721 
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
722 
THEN_ALL_NEW Fast_tac) *}) 

723 
(*1 subgoal*) 

724 
apply (clarsimp simp add: subset_mtriples_iff) 

725 
apply (rule ax_derivs.Methd) 

726 
apply (drule spec) 

727 
apply (erule impE) 

728 
apply (rule exI) 

729 
apply (erule conjI) 

730 
apply (rule HOL.refl) 

731 
oops (* dead end, Methd is to blame *) 

732 

733 

734 
section "rules derived from conseq" 

735 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

736 
text {* In the following rules we often have to give some type annotations like: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

737 
@{term "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q}"}. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

738 
Given only the term above without annotations, Isabelle would infer a more 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

739 
general type were we could have 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

740 
different types of auxiliary variables in the assumption set (@{term A}) and 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

741 
in the triple itself (@{term P} and @{term Q}). But 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

742 
@{text "ax_derivs.Methd"} enforces the same type in the inductive definition of 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

743 
the derivation. So we have to restrict the types to be able to apply the 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

744 
rules. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

745 
*} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

746 
lemma conseq12: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'}; 
12854  747 
\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> 
748 
Q Y' s' Z)\<rbrakk> 

749 
\<Longrightarrow> G,A\<turnstile>{P ::'a assn} t\<succ> {Q }" 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

750 
apply (rule ax_derivs.conseq) 
12854  751 
apply clarsimp 
752 
apply blast 

753 
done 

754 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

755 
 {* Nice variant, since it is so symmetric we might be able to memorise it. *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

756 
lemma conseq12': "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'}; \<forall>s Y' s'. 
12854  757 
(\<forall>Y Z. P' Y s Z \<longrightarrow> Q' Y' s' Z) \<longrightarrow> 
758 
(\<forall>Y Z. P Y s Z \<longrightarrow> Q Y' s' Z)\<rbrakk> 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

759 
\<Longrightarrow> G,A\<turnstile>{P::'a assn } t\<succ> {Q }" 
12854  760 
apply (erule conseq12) 
761 
apply fast 

762 
done 

763 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

764 
lemma conseq12_from_conseq12': "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'}; 
12854  765 
\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> 
766 
Q Y' s' Z)\<rbrakk> 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

767 
\<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q }" 
12854  768 
apply (erule conseq12') 
769 
apply blast 

770 
done 

771 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

772 
lemma conseq1: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q}; P \<Rightarrow> P'\<rbrakk> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

773 
\<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q}" 
12854  774 
apply (erule conseq12) 
775 
apply blast 

776 
done 

777 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

778 
lemma conseq2: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q'}; Q' \<Rightarrow> Q\<rbrakk> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

779 
\<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q}" 
12854  780 
apply (erule conseq12) 
781 
apply blast 

782 
done 

783 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

784 
lemma ax_escape: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

785 
"\<lbrakk>\<forall>Y s Z. P Y s Z 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

786 
\<longrightarrow> G,(A::'a triple set)\<turnstile>{\<lambda>Y' s' (Z'::'a). (Y',s') = (Y,s)} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

787 
t\<succ> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

788 
{\<lambda>Y s Z'. Q Y s Z} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

789 
\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q::'a assn}" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

790 
apply (rule ax_derivs.conseq) 
12854  791 
apply force 
792 
done 

793 

794 
(* unused *) 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

795 
lemma ax_constant: "\<lbrakk> C \<Longrightarrow> G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q}\<rbrakk> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

796 
\<Longrightarrow> G,A\<turnstile>{\<lambda>Y s Z. C \<and> P Y s Z} t\<succ> {Q}" 
12854  797 
apply (rule ax_escape (* unused *)) 
798 
apply clarify 

799 
apply (rule conseq12) 

800 
apply fast 

801 
apply auto 

802 
done 

803 
(*alternative (more direct) proof: 

804 
apply (rule ax_derivs.conseq) *)(* unused *)(* 

805 
apply (fast) 

806 
*) 

807 

808 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

809 
lemma ax_impossible [intro]: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

810 
"G,(A::'a triple set)\<turnstile>{\<lambda>Y s Z. False} t\<succ> {Q::'a assn}" 
12854  811 
apply (rule ax_escape) 
812 
apply clarify 

813 
done 

814 

815 
(* unused *) 

816 
lemma ax_nochange_lemma: "\<lbrakk>P Y s; All (op = w)\<rbrakk> \<Longrightarrow> P w s" 

817 
apply auto 

818 
done 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

819 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

820 
lemma ax_nochange: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

821 
"G,(A::(res \<times> state) triple set)\<turnstile>{\<lambda>Y s Z. (Y,s)=Z} t\<succ> {\<lambda>Y s Z. (Y,s)=Z} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

822 
\<Longrightarrow> G,A\<turnstile>{P::(res \<times> state) assn} t\<succ> {P}" 
12854  823 
apply (erule conseq12) 
824 
apply auto 

825 
apply (erule (1) ax_nochange_lemma) 

826 
done 

827 

828 
(* unused *) 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

829 
lemma ax_trivial: "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {\<lambda>Y s Z. True}" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

830 
apply (rule ax_derivs.conseq(* unused *)) 
12854  831 
apply auto 
832 
done 

833 

834 
(* unused *) 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

835 
lemma ax_disj: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

836 
"\<lbrakk>G,(A::'a triple set)\<turnstile>{P1::'a assn} t\<succ> {Q1}; G,A\<turnstile>{P2::'a assn} t\<succ> {Q2}\<rbrakk> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

837 
\<Longrightarrow> G,A\<turnstile>{\<lambda>Y s Z. P1 Y s Z \<or> P2 Y s Z} t\<succ> {\<lambda>Y s Z. Q1 Y s Z \<or> Q2 Y s Z}" 
12854  838 
apply (rule ax_escape (* unused *)) 
839 
apply safe 

840 
apply (erule conseq12, fast)+ 

841 
done 

842 

843 
(* unused *) 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

844 
lemma ax_supd_shuffle: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

845 
"(\<exists>Q. G,(A::'a triple set)\<turnstile>{P::'a assn} .c1. {Q} \<and> G,A\<turnstile>{Q ;. f} .c2. {R}) = 
12854  846 
(\<exists>Q'. G,A\<turnstile>{P} .c1. {f .; Q'} \<and> G,A\<turnstile>{Q'} .c2. {R})" 
847 
apply (best elim!: conseq1 conseq2) 

848 
done 

849 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

850 
lemma ax_cases: " 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

851 
\<lbrakk>G,(A::'a triple set)\<turnstile>{P \<and>. C} t\<succ> {Q::'a assn}; 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

852 
G,A\<turnstile>{P \<and>. Not \<circ> C} t\<succ> {Q}\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}" 
12854  853 
apply (unfold peek_and_def) 
854 
apply (rule ax_escape) 

855 
apply clarify 

856 
apply (case_tac "C s") 

857 
apply (erule conseq12, force)+ 

858 
done 

859 
(*alternative (more direct) proof: 

860 
apply (rule rtac ax_derivs.conseq) *)(* unused *)(* 

861 
apply clarify 

862 
apply (case_tac "C s") 

863 
apply force+ 

864 
*) 

865 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

866 
lemma ax_adapt: "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

867 
\<Longrightarrow> G,A\<turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}" 
12854  868 
apply (unfold adapt_pre_def) 
869 
apply (erule conseq12) 

870 
apply fast 

871 
done 

872 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

873 
lemma adapt_pre_adapts: "G,(A::'a triple set)\<Turnstile>{P::'a assn} t\<succ> {Q} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

874 
\<longrightarrow> G,A\<Turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}" 
12854  875 
apply (unfold adapt_pre_def) 
876 
apply (simp add: ax_valids_def triple_valid_def2) 

877 
apply fast 

878 
done 

879 

880 

881 
lemma adapt_pre_weakest: 

882 
"\<forall>G (A::'a triple set) t. G,A\<Turnstile>{P} t\<succ> {Q} \<longrightarrow> G,A\<Turnstile>{P'} t\<succ> {Q'} \<Longrightarrow> 

883 
P' \<Rightarrow> adapt_pre P Q (Q'::'a assn)" 

884 
apply (unfold adapt_pre_def) 

885 
apply (drule spec) 

886 
apply (drule_tac x = "{}" in spec) 

887 
apply (drule_tac x = "In1r Skip" in spec) 

888 
apply (simp add: ax_valids_def triple_valid_def2) 

889 
oops 

890 

891 
lemma peek_and_forget1_Normal: 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

892 
"G,(A::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

893 
\<Longrightarrow> G,A\<turnstile>{Normal (P \<and>. p)} t\<succ> {Q}" 
12854  894 
apply (erule conseq1) 
895 
apply (simp (no_asm)) 

896 
done 

897 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

898 
lemma peek_and_forget1: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

899 
"G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

900 
\<Longrightarrow> G,A\<turnstile>{P \<and>. p} t\<succ> {Q}" 
12854  901 
apply (erule conseq1) 
902 
apply (simp (no_asm)) 

903 
done 

904 

905 
lemmas ax_NormalD = peek_and_forget1 [of _ _ _ _ _ normal] 

906 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

907 
lemma peek_and_forget2: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

908 
"G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q \<and>. p} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

909 
\<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}" 
12854  910 
apply (erule conseq2) 
911 
apply (simp (no_asm)) 

912 
done 

913 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

914 
lemma ax_subst_Val_allI: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

915 
"\<forall>v. G,(A::'a triple set)\<turnstile>{(P' v )\<leftarrow>Val v} t\<succ> {(Q v)::'a assn} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

916 
\<Longrightarrow> \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In1 w))\<leftarrow>Val v} t\<succ> {Q v}" 
12854  917 
apply (force elim!: conseq1) 
918 
done 

919 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

920 
lemma ax_subst_Var_allI: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

921 
"\<forall>v. G,(A::'a triple set)\<turnstile>{(P' v )\<leftarrow>Var v} t\<succ> {(Q v)::'a assn} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

922 
\<Longrightarrow> \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In2 w))\<leftarrow>Var v} t\<succ> {Q v}" 
12854  923 
apply (force elim!: conseq1) 
924 
done 

925 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

926 
lemma ax_subst_Vals_allI: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

927 
"(\<forall>v. G,(A::'a triple set)\<turnstile>{( P' v )\<leftarrow>Vals v} t\<succ> {(Q v)::'a assn}) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

928 
\<Longrightarrow> \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In3 w))\<leftarrow>Vals v} t\<succ> {Q v}" 
12854  929 
apply (force elim!: conseq1) 
930 
done 

931 

932 

933 
section "alternative axioms" 

934 

935 
lemma ax_Lit2: 

936 
"G,(A::'a triple set)\<turnstile>{Normal P::'a assn} Lit v\<succ> {Normal (P\<down>=Val v)}" 

937 
apply (rule ax_derivs.Lit [THEN conseq1]) 

938 
apply force 

939 
done 

940 
lemma ax_Lit2_test_complete: 

941 
"G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val v)::'a assn} Lit v\<succ> {P}" 

942 
apply (rule ax_Lit2 [THEN conseq2]) 

943 
apply force 

944 
done 

945 

946 
lemma ax_LVar2: "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} LVar vn=\<succ> {Normal (\<lambda>s.. P\<down>=Var (lvar vn s))}" 

947 
apply (rule ax_derivs.LVar [THEN conseq1]) 

948 
apply force 

949 
done 

950 

951 
lemma ax_Super2: "G,(A::'a triple set)\<turnstile> 

952 
{Normal P::'a assn} Super\<succ> {Normal (\<lambda>s.. P\<down>=Val (val_this s))}" 

953 
apply (rule ax_derivs.Super [THEN conseq1]) 

954 
apply force 

955 
done 

956 

957 
lemma ax_Nil2: 

958 
"G,(A::'a triple set)\<turnstile>{Normal P::'a assn} []\<doteq>\<succ> {Normal (P\<down>=Vals [])}" 

959 
apply (rule ax_derivs.Nil [THEN conseq1]) 

960 
apply force 

961 
done 

962 

963 

964 
section "misc derived structural rules" 

965 

966 
(* unused *) 

967 
lemma ax_finite_mtriples_lemma: "\<lbrakk>F \<subseteq> ms; finite ms; \<forall>(C,sig)\<in>ms. 

968 
G,(A::'a triple set)\<turnstile>{Normal (P C sig)::'a assn} mb C sig\<succ> {Q C sig}\<rbrakk> \<Longrightarrow> 

969 
G,A\<turnstile>{{P} mb\<succ> {Q}  F}" 

970 
apply (frule (1) finite_subset) 

971 
apply (erule make_imp) 

972 
apply (erule thin_rl) 

973 
apply (erule finite_induct) 

974 
apply (unfold mtriples_def) 

975 
apply (clarsimp intro!: ax_derivs.empty ax_derivs.insert)+ 

976 
apply force 

977 
done 

978 
lemmas ax_finite_mtriples = ax_finite_mtriples_lemma [OF subset_refl] 

979 

980 
lemma ax_derivs_insertD: 

981 
"G,(A::'a triple set)\<turnstile>insert (t::'a triple) ts \<Longrightarrow> G,A\<turnstile>t \<and> G,A\<turnstile>ts" 

982 
apply (fast intro: ax_derivs.weaken) 

983 
done 

984 

985 
lemma ax_methods_spec: 

986 
"\<lbrakk>G,(A::'a triple set)\<turnstile>split f ` ms; (C,sig) \<in> ms\<rbrakk>\<Longrightarrow> G,A\<turnstile>((f C sig)::'a triple)" 

987 
apply (erule ax_derivs.weaken) 

988 
apply (force del: image_eqI intro: rev_image_eqI) 

989 
done 

990 

991 
(* this version is used to avoid using the cut rule *) 

992 
lemma ax_finite_pointwise_lemma [rule_format]: "\<lbrakk>F \<subseteq> ms; finite ms\<rbrakk> \<Longrightarrow> 

993 
((\<forall>(C,sig)\<in>F. G,(A::'a triple set)\<turnstile>(f C sig::'a triple)) \<longrightarrow> (\<forall>(C,sig)\<in>ms. G,A\<turnstile>(g C sig::'a triple))) \<longrightarrow> 

994 
G,A\<turnstile>split f ` F \<longrightarrow> G,A\<turnstile>split g ` F" 

995 
apply (frule (1) finite_subset) 

996 
apply (erule make_imp) 

997 
apply (erule thin_rl) 

998 
apply (erule finite_induct) 

999 
apply clarsimp+ 

1000 
apply (drule ax_derivs_insertD) 

1001 
apply (rule ax_derivs.insert) 

1002 
apply (simp (no_asm_simp) only: split_tupled_all) 

1003 
apply (auto elim: ax_methods_spec) 

1004 
done 

1005 
lemmas ax_finite_pointwise = ax_finite_pointwise_lemma [OF subset_refl] 

1006 

1007 
lemma ax_no_hazard: 

1008 
"G,(A::'a triple set)\<turnstile>{P \<and>. type_ok G t} t\<succ> {Q::'a assn} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}" 

1009 
apply (erule ax_cases) 

1010 
apply (rule ax_derivs.hazard [THEN conseq1]) 

1011 
apply force 

1012 
done 

1013 

1014 
lemma ax_free_wt: 

1015 
"(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 

1016 
\<longrightarrow> G,(A::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} \<Longrightarrow> 

1017 
G,A\<turnstile>{Normal P} t\<succ> {Q}" 

1018 
apply (rule ax_no_hazard) 

1019 
apply (rule ax_escape) 

1020 
apply clarify 

1021 
apply (erule mp [THEN conseq12]) 

1022 
apply (auto simp add: type_ok_def) 

1023 
done 

1024 

1025 
ML {* 

1026 
bind_thms ("ax_Abrupts", sum3_instantiate (thm "ax_derivs.Abrupt")) 

1027 
*} 

1028 
declare ax_Abrupts [intro!] 

1029 

21765  1030 
lemmas ax_Normal_cases = ax_cases [of _ _ _ normal] 
12854  1031 

1032 
lemma ax_Skip [intro!]: "G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit>} .Skip. {P::'a assn}" 

1033 
apply (rule ax_Normal_cases) 

1034 
apply (rule ax_derivs.Skip) 

1035 
apply fast 

1036 
done 

1037 
lemmas ax_SkipI = ax_Skip [THEN conseq1, standard] 

1038 

1039 

1040 
section "derived rules for methd call" 

1041 

1042 
lemma ax_Call_known_DynT: 

1043 
"\<lbrakk>G\<turnstile>IntVir\<rightarrow>C\<preceq>statT; 

1044 
\<forall>a vs l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;. 

1045 
init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> IntVir a vs)} 

1046 
Methd C \<lparr>name=mn,parTs=pTs\<rparr>\<succ> {set_lvars l .; S}; 

1047 
\<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> 

1048 
{R a \<and>. (\<lambda>s. C = obj_class (the (heap (store s) (the_Addr a))) \<and> 

1049 
C = invocation_declclass 

1050 
G IntVir (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> )}; 

1051 
G,(A::'a triple set)\<turnstile>{Normal P} e\<succ> {Q::'a assn}\<rbrakk> 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1052 
\<Longrightarrow> G,A\<turnstile>{Normal P} {accC,statT,IntVir}e\<cdot>mn({pTs}args)\<succ> {S}" 
12854  1053 
apply (erule ax_derivs.Call) 
1054 
apply safe 

1055 
apply (erule spec) 

1056 
apply (rule ax_escape, clarsimp) 

1057 
apply (drule spec, drule spec, drule spec,erule conseq12) 

1058 
apply force 

1059 
done 

1060 

1061 

1062 
lemma ax_Call_Static: 

1063 
"\<lbrakk>\<forall>a vs l. G,A\<turnstile>{R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;. 

1064 
init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> Static any_Addr vs} 

1065 
Methd C \<lparr>name=mn,parTs=pTs\<rparr>\<succ> {set_lvars l .; S}; 

1066 
G,A\<turnstile>{Normal P} e\<succ> {Q}; 

1067 
\<forall> a. G,(A::'a triple set)\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {(R::val \<Rightarrow> 'a assn) a 

1068 
\<and>. (\<lambda> s. C=invocation_declclass 

1069 
G Static (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr>)} 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1070 
\<rbrakk> \<Longrightarrow> G,A\<turnstile>{Normal P} {accC,statT,Static}e\<cdot>mn({pTs}args)\<succ> {S}" 
12854  1071 
apply (erule ax_derivs.Call) 
1072 
apply safe 

1073 
apply (erule spec) 

1074 
apply (rule ax_escape, clarsimp) 

1075 
apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl) 

1076 
apply (drule spec,drule spec,drule spec, erule conseq12) 

20014  1077 
apply (force simp add: init_lvars_def Let_def) 
12854  1078 
done 
1079 

1080 
lemma ax_Methd1: 

1081 
"\<lbrakk>G,A\<union>{{P} Methd\<succ> {Q}  ms}\<turnstile> {{P} body G\<succ> {Q}  ms}; (C,sig)\<in> ms\<rbrakk> \<Longrightarrow> 

1082 
G,A\<turnstile>{Normal (P C sig)} Methd C sig\<succ> {Q C sig}" 

1083 
apply (drule ax_derivs.Methd) 

1084 
apply (unfold mtriples_def) 

1085 
apply (erule (1) ax_methods_spec) 

1086 
done 

1087 

1088 
lemma ax_MethdN: 

1089 
"G,insert({Normal P} Methd C sig\<succ> {Q}) A\<turnstile> 

1090 
{Normal P} body G C sig\<succ> {Q} \<Longrightarrow> 

1091 
G,A\<turnstile>{Normal P} Methd C sig\<succ> {Q}" 

1092 
apply (rule ax_Methd1) 

1093 
apply (rule_tac [2] singletonI) 

1094 
apply (unfold mtriples_def) 

1095 
apply clarsimp 

1096 
done 

1097 

1098 
lemma ax_StatRef: 

1099 
"G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val Null)} StatRef rt\<succ> {P::'a assn}" 

1100 
apply (rule ax_derivs.Cast) 

1101 
apply (rule ax_Lit2 [THEN conseq2]) 

1102 
apply clarsimp 

1103 
done 

1104 

1105 
section "rules derived from Init and Done" 

1106 

1107 
lemma ax_InitS: "\<lbrakk>the (class G C) = c; C \<noteq> Object; 

1108 
\<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty} 

1109 
.init c. {set_lvars l .; R}; 

1110 
G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))} 

1111 
.Init (super c). {Q}\<rbrakk> \<Longrightarrow> 

1112 
G,(A::'a triple set)\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R::'a assn}" 

1113 
apply (erule ax_derivs.Init) 

1114 
apply (simp (no_asm_simp)) 

1115 
apply assumption 

1116 
done 

1117 

1118 
lemma ax_Init_Skip_lemma: 

1119 
"\<forall>l. G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit> \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars l'} 

1120 
.Skip. {(set_lvars l .; P)::'a assn}" 

1121 
apply (rule allI) 

1122 
apply (rule ax_SkipI) 

1123 
apply clarsimp 

1124 
done 

1125 

1126 
lemma ax_triv_InitS: "\<lbrakk>the (class G C) = c;init c = Skip; C \<noteq> Object; 

1127 
P\<leftarrow>\<diamondsuit> \<Rightarrow> (supd (init_class_obj G C) .; P); 

1128 
G,A\<turnstile>{Normal (P \<and>. initd C)} .Init (super c). {(P \<and>. initd C)\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow> 

1129 
G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init C. {(P \<and>. initd C)::'a assn}" 

1130 
apply (rule_tac C = "initd C" in ax_cases) 

1131 
apply (rule conseq1, rule ax_derivs.Done, clarsimp) 

1132 
apply (simp (no_asm)) 

1133 
apply (erule (1) ax_InitS) 

1134 
apply simp 

1135 
apply (rule ax_Init_Skip_lemma) 

1136 
apply (erule conseq1) 

1137 
apply force 

1138 
done 

1139 

1140 
lemma ax_Init_Object: "wf_prog G \<Longrightarrow> G,(A::'a triple set)\<turnstile> 

1141 
{Normal ((supd (init_class_obj G Object) .; P\<leftarrow>\<diamondsuit>) \<and>. Not \<circ> initd Object)} 

1142 
.Init Object. {(P \<and>. initd Object)::'a assn}" 

1143 
apply (rule ax_derivs.Init) 

1144 
apply (drule class_Object, force) 

1145 
apply (simp_all (no_asm)) 

1146 
apply (rule_tac [2] ax_Init_Skip_lemma) 

1147 
apply (rule ax_SkipI, force) 

1148 
done 

1149 

1150 
lemma ax_triv_Init_Object: "\<lbrakk>wf_prog G; 

1151 
(P::'a assn) \<Rightarrow> (supd (init_class_obj G Object) .; P)\<rbrakk> \<Longrightarrow> 

1152 
G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init Object. {P \<and>. initd Object}" 

1153 
apply (rule_tac C = "initd Object" in ax_cases) 

1154 
apply (rule conseq1, rule ax_derivs.Done, clarsimp) 

1155 
apply (erule ax_Init_Object [THEN conseq1]) 

1156 
apply force 

1157 
done 

1158 

1159 

1160 
section "introduction rules for Alloc and SXAlloc" 

1161 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1162 
lemma ax_SXAlloc_Normal: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1163 
"G,(A::'a triple set)\<turnstile>{P::'a assn} .c. {Normal Q} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1164 
\<Longrightarrow> G,A\<turnstile>{P} .c. {SXAlloc G Q}" 
12854  1165 
apply (erule conseq2) 
1166 
apply (clarsimp elim!: sxalloc_elim_cases simp add: split_tupled_all) 

1167 
done 

1168 

1169 
lemma ax_Alloc: 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1170 
"G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1171 
{Normal (\<lambda>Y (x,s) Z. (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1172 
Q (Val (Addr a)) (Norm(init_obj G (CInst C) (Heap a) s)) Z)) \<and>. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1173 
heap_free (Suc (Suc 0))} 
12854  1174 
\<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Alloc G (CInst C) Q}" 
1175 
apply (erule conseq2) 

1176 
apply (auto elim!: halloc_elim_cases) 

1177 
done 

1178 

1179 
lemma ax_Alloc_Arr: 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1180 
"G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1181 
{\<lambda>Val:i:. Normal (\<lambda>Y (x,s) Z. \<not>the_Intg i<0 \<and> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1182 
(\<forall>a. new_Addr (heap s) = Some a \<longrightarrow> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1183 
Q (Val (Addr a)) (Norm (init_obj G (Arr T (the_Intg i)) (Heap a) s)) Z)) \<and>. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1184 
heap_free (Suc (Suc 0))} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1185 
\<Longrightarrow> 
12854  1186 
G,A\<turnstile>{P} t\<succ> {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T(the_Intg i)) Q}" 
1187 
apply (erule conseq2) 

1188 
apply (auto elim!: halloc_elim_cases) 

1189 
done 

1190 

1191 
lemma ax_SXAlloc_catch_SXcpt: 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1192 
"\<lbrakk>G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1193 
{(\<lambda>Y (x,s) Z. x=Some (Xcpt (Std xn)) \<and> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1194 
(\<forall>a. new_Addr (heap s) = Some a \<longrightarrow> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1195 
Q Y (Some (Xcpt (Loc a)),init_obj G (CInst (SXcpt xn)) (Heap a) s) Z)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1196 
\<and>. heap_free (Suc (Suc 0))}\<rbrakk> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1197 
\<Longrightarrow> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1198 
G,A\<turnstile>{P} t\<succ> {SXAlloc G (\<lambda>Y s Z. Q Y s Z \<and> G,s\<turnstile>catch SXcpt xn)}" 
12854  1199 
apply (erule conseq2) 
1200 
apply (auto elim!: sxalloc_elim_cases halloc_elim_cases) 

1201 
done 

1202 

1203 
end 