author  wenzelm 
Sat, 17 Oct 2009 14:43:18 +0200  
changeset 32960  69916a850301 
parent 28524  644b62cf678f 
child 35067  af4c18c30593 
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 

24783  52 
"_Val" :: "[pttrn] => pttrn" ("Val:_" [951] 950) 
53 
"_Var" :: "[pttrn] => pttrn" ("Var:_" [951] 950) 

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

12854  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] 

24019  474 
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *} 
475 
declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *} 

12854  476 

23747  477 
inductive 
21765  478 
ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_\<turnstile>_" [61,58,58] 57) 
479 
and ax_deriv :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple \<Rightarrow> bool" ("_,_\<turnstile>_" [61,58,58] 57) 

480 
for G :: prog 

481 
where 

12854  482 

21765  483 
"G,A \<turnstile>t \<equiv> G,A\<turnstile>{t}" 
484 

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

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

12854  487 
G,A\<turnstile>insert t ts" 
488 

21765  489 
 asm: "ts\<subseteq>A \<Longrightarrow> G,A\<turnstile>ts" 
12854  490 

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

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

493 
G,A \<turnstile>ts" 

494 
*) 

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

21765  497 
 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  498 
(\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> 
499 
Q Y' s' Z )) 

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

501 

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

28524  504 
 Abrupt: "G,A\<turnstile>{P\<leftarrow>(undefined3 t) \<and>. Not \<circ> normal} t\<succ> {P}" 
12854  505 

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

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

21765  509 
 FVar: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Q}; 
12854  510 
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

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

21765  513 
 AVar: "\<lbrakk>G,A\<turnstile>{Normal P} e1\<succ> {Q}; 
12854  514 
\<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} e2\<succ> {\<lambda>Val:i:. avar G i a ..; R}\<rbrakk> \<Longrightarrow> 
515 
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

516 
{* expressions *} 
12854  517 

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

21765  521 
 NewA: "\<lbrakk>G,A\<turnstile>{Normal P} .init_comp_ty T. {Q}; G,A\<turnstile>{Q} e\<succ> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

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

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

528 

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

532 

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

21765  535 
 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

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

537 
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

538 

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

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

543 
{\<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

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

545 
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

546 

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

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

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

555 

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

559 

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

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

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

565 
l = locals (store s)) ;. 

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

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

568 
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

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

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

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

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

578 

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

579 
{* expression lists *} 
12854  580 

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

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

586 

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

587 
{* statements *} 
12854  588 

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

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

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

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

600 

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

604 
(* unfolding variant of Loop, not needed here 

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

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

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

608 
*) 

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

612 

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

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

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

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

622 

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

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

627 

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

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

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

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

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

636 

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

637 
 {* 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

638 
@{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

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

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

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

644 
 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

645 
(* 
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

646 
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

647 
*) 
12854  648 

649 
constdefs 

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

651 
"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)" 

652 

653 

654 
section "rules derived by induction" 

655 

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

657 
apply (unfold ax_valids_def) 

658 
apply fast 

659 
done 

660 

661 
(*if cut is available 

662 
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> 

663 
G,A\<turnstile>ts" 

664 
b y etac ax_derivs.cut 1; 

665 
b y eatac ax_derivs.asm 1 1; 

666 
qed "ax_thin"; 

667 
*) 

668 
lemma ax_thin [rule_format (no_asm)]: 

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

670 
apply (erule ax_derivs.induct) 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23747
diff
changeset

671 
apply (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])") 
12854  672 
apply (rule ax_derivs.empty) 
673 
apply (erule (1) ax_derivs.insert) 

674 
apply (fast intro: ax_derivs.asm) 

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

676 
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

677 
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

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

679 
prefer 18 (* Methd *) 
23563  680 
apply (rule ax_derivs.Methd, drule spec, erule mp, fast) 
681 
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))) *}) 

682 
apply auto 

12854  683 
done 
684 

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

686 
apply (erule ax_thin) 

687 
apply fast 

688 
done 

689 

690 
lemma subset_mtriples_iff: 

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

692 
apply (unfold mtriples_def) 

693 
apply (rule subset_image_iff) 

694 
done 

695 

696 
lemma weaken: 

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

698 
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

699 
(*42 subgoals*) 
12854  700 
apply (tactic "ALLGOALS strip_tac") 
701 
apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"), 

26342  702 
etac disjE, fast_tac (@{claset} addSIs [thm "ax_derivs.empty"])]))*}) 
12854  703 
apply (tactic "TRYALL hyp_subst_tac") 
704 
apply (simp, rule ax_derivs.empty) 

705 
apply (drule subset_insertD) 

706 
apply (blast intro: ax_derivs.insert) 

707 
apply (fast intro: ax_derivs.asm) 

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

709 
apply (fast intro: ax_derivs.weaken) 

710 
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

711 
(*37 subgoals*) 
12854  712 
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23747
diff
changeset

713 
THEN_ALL_NEW fast_tac @{claset}) *}) 
12854  714 
(*1 subgoal*) 
715 
apply (clarsimp simp add: subset_mtriples_iff) 

716 
apply (rule ax_derivs.Methd) 

717 
apply (drule spec) 

718 
apply (erule impE) 

719 
apply (rule exI) 

720 
apply (erule conjI) 

721 
apply (rule HOL.refl) 

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

723 

724 

725 
section "rules derived from conseq" 

726 

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

727 
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

728 
@{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

729 
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

730 
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

731 
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

732 
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

733 
@{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

734 
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

735 
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

736 
*} 
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 
lemma conseq12: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'}; 
12854  738 
\<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> 
739 
Q Y' s' Z)\<rbrakk> 

740 
\<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

741 
apply (rule ax_derivs.conseq) 
12854  742 
apply clarsimp 
743 
apply blast 

744 
done 

745 

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

746 
 {* 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

747 
lemma conseq12': "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'}; \<forall>s Y' s'. 
12854  748 
(\<forall>Y Z. P' Y s Z \<longrightarrow> Q' Y' s' Z) \<longrightarrow> 
749 
(\<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

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

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 
lemma conseq12_from_conseq12': "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'}; 
12854  756 
\<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> 
757 
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

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

761 
done 

762 

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

763 
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

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

767 
done 

768 

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

769 
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

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

773 
done 

774 

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

775 
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

776 
"\<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

777 
\<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

778 
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

779 
{\<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

780 
\<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

781 
apply (rule ax_derivs.conseq) 
12854  782 
apply force 
783 
done 

784 

785 
(* 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

786 
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

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

790 
apply (rule conseq12) 

791 
apply fast 

792 
apply auto 

793 
done 

794 
(*alternative (more direct) proof: 

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

796 
apply (fast) 

797 
*) 

798 

799 

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

800 
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

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

804 
done 

805 

806 
(* unused *) 

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

808 
apply auto 

809 
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

810 

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

811 
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

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

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

816 
apply (erule (1) ax_nochange_lemma) 

817 
done 

818 

819 
(* 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

820 
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

821 
apply (rule ax_derivs.conseq(* unused *)) 
12854  822 
apply auto 
823 
done 

824 

825 
(* 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

826 
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

827 
"\<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

828 
\<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  829 
apply (rule ax_escape (* unused *)) 
830 
apply safe 

831 
apply (erule conseq12, fast)+ 

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_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

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

839 
done 

840 

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

841 
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

842 
\<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

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

846 
apply clarify 

847 
apply (case_tac "C s") 

848 
apply (erule conseq12, force)+ 

849 
done 

850 
(*alternative (more direct) proof: 

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

852 
apply clarify 

853 
apply (case_tac "C s") 

854 
apply force+ 

855 
*) 

856 

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

857 
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

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

861 
apply fast 

862 
done 

863 

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

864 
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

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

868 
apply fast 

869 
done 

870 

871 

872 
lemma adapt_pre_weakest: 

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

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

875 
apply (unfold adapt_pre_def) 

876 
apply (drule spec) 

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

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

879 
apply (simp add: ax_valids_def triple_valid_def2) 

880 
oops 

881 

882 
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

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

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

887 
done 

888 

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

889 
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

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

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

894 
done 

895 

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

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_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

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

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

903 
done 

904 

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

905 
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

906 
"\<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

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

910 

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

911 
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

912 
"\<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

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

916 

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

917 
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

918 
"(\<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

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

922 

923 

924 
section "alternative axioms" 

925 

926 
lemma ax_Lit2: 

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

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

929 
apply force 

930 
done 

931 
lemma ax_Lit2_test_complete: 

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

933 
apply (rule ax_Lit2 [THEN conseq2]) 

934 
apply force 

935 
done 

936 

937 
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))}" 

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

939 
apply force 

940 
done 

941 

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

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

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

945 
apply force 

946 
done 

947 

948 
lemma ax_Nil2: 

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

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

951 
apply force 

952 
done 

953 

954 

955 
section "misc derived structural rules" 

956 

957 
(* unused *) 

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

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

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

961 
apply (frule (1) finite_subset) 

24038  962 
apply (erule rev_mp) 
12854  963 
apply (erule thin_rl) 
964 
apply (erule finite_induct) 

965 
apply (unfold mtriples_def) 

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

967 
apply force 

968 
done 

969 
lemmas ax_finite_mtriples = ax_finite_mtriples_lemma [OF subset_refl] 

970 

971 
lemma ax_derivs_insertD: 

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

973 
apply (fast intro: ax_derivs.weaken) 

974 
done 

975 

976 
lemma ax_methods_spec: 

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

978 
apply (erule ax_derivs.weaken) 

979 
apply (force del: image_eqI intro: rev_image_eqI) 

980 
done 

981 

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

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

984 
((\<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> 

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

986 
apply (frule (1) finite_subset) 

24038  987 
apply (erule rev_mp) 
12854  988 
apply (erule thin_rl) 
989 
apply (erule finite_induct) 

990 
apply clarsimp+ 

991 
apply (drule ax_derivs_insertD) 

992 
apply (rule ax_derivs.insert) 

993 
apply (simp (no_asm_simp) only: split_tupled_all) 

994 
apply (auto elim: ax_methods_spec) 

995 
done 

996 
lemmas ax_finite_pointwise = ax_finite_pointwise_lemma [OF subset_refl] 

997 

998 
lemma ax_no_hazard: 

999 
"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}" 

1000 
apply (erule ax_cases) 

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

1002 
apply force 

1003 
done 

1004 

1005 
lemma ax_free_wt: 

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

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

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

1009 
apply (rule ax_no_hazard) 

1010 
apply (rule ax_escape) 

1011 
apply clarify 

1012 
apply (erule mp [THEN conseq12]) 

1013 
apply (auto simp add: type_ok_def) 

1014 
done 

1015 

27226  1016 
ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *} 
12854  1017 
declare ax_Abrupts [intro!] 
1018 

21765  1019 
lemmas ax_Normal_cases = ax_cases [of _ _ _ normal] 
12854  1020 

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

1022 
apply (rule ax_Normal_cases) 

1023 
apply (rule ax_derivs.Skip) 

1024 
apply fast 

1025 
done 

1026 
lemmas ax_SkipI = ax_Skip [THEN conseq1, standard] 

1027 

1028 

1029 
section "derived rules for methd call" 

1030 

1031 
lemma ax_Call_known_DynT: 

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

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

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

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

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

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

1038 
C = invocation_declclass 

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

1040 
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

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

1044 
apply (erule spec) 

1045 
apply (rule ax_escape, clarsimp) 

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

1047 
apply force 

1048 
done 

1049 

1050 

1051 
lemma ax_Call_Static: 

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

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

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

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

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

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

1058 
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

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

1062 
apply (erule spec) 

1063 
apply (rule ax_escape, clarsimp) 

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

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

20014  1066 
apply (force simp add: init_lvars_def Let_def) 
12854  1067 
done 
1068 

1069 
lemma ax_Methd1: 

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

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

1072 
apply (drule ax_derivs.Methd) 

1073 
apply (unfold mtriples_def) 

1074 
apply (erule (1) ax_methods_spec) 

1075 
done 

1076 

1077 
lemma ax_MethdN: 

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

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

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

1081 
apply (rule ax_Methd1) 

1082 
apply (rule_tac [2] singletonI) 

1083 
apply (unfold mtriples_def) 

1084 
apply clarsimp 

1085 
done 

1086 

1087 
lemma ax_StatRef: 

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

1089 
apply (rule ax_derivs.Cast) 

1090 
apply (rule ax_Lit2 [THEN conseq2]) 

1091 
apply clarsimp 

1092 
done 

1093 

1094 
section "rules derived from Init and Done" 

1095 

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

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

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

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

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

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

1102 
apply (erule ax_derivs.Init) 

1103 
apply (simp (no_asm_simp)) 

1104 
apply assumption 

1105 
done 

1106 

1107 
lemma ax_Init_Skip_lemma: 

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

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

1110 
apply (rule allI) 

1111 
apply (rule ax_SkipI) 

1112 
apply clarsimp 

1113 
done 

1114 

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

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

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

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

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

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

1121 
apply (simp (no_asm)) 

1122 
apply (erule (1) ax_InitS) 

1123 
apply simp 

1124 
apply (rule ax_Init_Skip_lemma) 

1125 
apply (erule conseq1) 

1126 
apply force 

1127 
done 

1128 

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

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

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

1132 
apply (rule ax_derivs.Init) 

1133 
apply (drule class_Object, force) 

1134 
apply (simp_all (no_asm)) 

1135 
apply (rule_tac [2] ax_Init_Skip_lemma) 

1136 
apply (rule ax_SkipI, force) 

1137 
done 

1138 

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

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

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

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

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

1144 
apply (erule ax_Init_Object [THEN conseq1]) 

1145 
apply force 

1146 
done 

1147 

1148 

1149 
section "introduction rules for Alloc and SXAlloc" 

1150 

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

1151 
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

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

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

1156 
done 

1157 

1158 
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

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

1160 
{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

1161 
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

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

1165 
apply (auto elim!: halloc_elim_cases) 

1166 
done 

1167 

1168 
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

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

1170 
{\<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

1171 
(\<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 (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

1173 
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

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

1177 
apply (auto elim!: halloc_elim_cases) 

1178 
done 

1179 

1180 
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

1181 
"\<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

1182 
{(\<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

1183 
(\<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

1184 
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

1185 
\<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

1186 
\<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

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

1190 
done 

1191 

1192 
end 