author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45605  a89b4bc311a5 
child 51703  f2e92fc0c8aa 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/AxSem.thy 
12854  2 
Author: David von Oheimb 
3 
*) 

4 

5 
header {* Axiomatic semantics of Java expressions and statements 

6 
(see also Eval.thy) 

7 
*} 

16417  8 
theory AxSem imports Evaln TypeSafe begin 
12854  9 

10 
text {* 

11 
design issues: 

12 
\begin{itemize} 

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

14 
takes the recursive depth needed to complete execution, enables 

15 
correctness proof 

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

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

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

19 
handling 

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

21 
(with result entry) 

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

23 
stack 

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

25 
this is also useful for conditional expressions and statements 

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

27 
states) 

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

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

30 
\end{itemize} 

31 

32 
restrictions: 

33 
\begin{itemize} 

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

35 
polymorphism) 

36 
\end{itemize} 

37 
*} 

38 

41778  39 
type_synonym res = vals {* result entry *} 
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

40 

af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

41 
abbreviation (input) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

42 
Val where "Val x == In1 x" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

43 

af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

44 
abbreviation (input) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

45 
Var where "Var x == In2 x" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

46 

af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

47 
abbreviation (input) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

48 
Vals where "Vals x == In3 x" 
12854  49 

50 
syntax 

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

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

12854  54 

55 
translations 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

56 
"\<lambda>Val:v . b" == "(\<lambda>v. b) \<circ> CONST the_In1" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

57 
"\<lambda>Var:v . b" == "(\<lambda>v. b) \<circ> CONST the_In2" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

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

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

60 
{* relation on result values, state and auxiliary variables *} 
41778  61 
type_synonym 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool" 
12854  62 
translations 
35431  63 
(type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool" 
12854  64 

37956  65 
definition 
66 
assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25) 

67 
where "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)" 

12854  68 

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

70 
apply (unfold assn_imp_def) 

71 
apply (rule HOL.refl) 

72 
done 

73 

74 

75 
section "assertion transformers" 

76 

77 
subsection "peekand" 

78 

37956  79 
definition 
80 
peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13) 

81 
where "(P \<and>. p) = (\<lambda>Y s Z. P Y s Z \<and> p s)" 

12854  82 

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

84 
apply (unfold peek_and_def) 

85 
apply (simp (no_asm)) 

86 
done 

87 

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

89 
apply (rule ext) 

90 
apply (rule ext) 

91 
apply (simp (no_asm)) 

92 
done 

93 

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

95 
apply (unfold peek_and_def) 

96 
apply (simp (no_asm)) 

97 
done 

98 

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

100 
apply (rule ext) 

101 
apply (rule ext) 

102 
apply (rule ext) 

103 
apply auto 

104 
done 

105 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

106 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

107 
Normal :: "'a assn \<Rightarrow> 'a assn" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

108 
where "Normal P == P \<and>. normal" 
12854  109 

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

111 
apply (rule ext) 

112 
apply (rule ext) 

113 
apply (rule ext) 

114 
apply auto 

115 
done 

116 

117 
subsection "assnsupd" 

118 

37956  119 
definition 
120 
assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13) 

121 
where "(P ;. f) = (\<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s)" 

12854  122 

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

124 
apply (unfold assn_supd_def) 

125 
apply (simp (no_asm)) 

126 
done 

127 

128 
subsection "supdassn" 

129 

37956  130 
definition 
131 
supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13) 

132 
where "(f .; P) = (\<lambda>Y s. P Y (f s))" 

12854  133 

134 

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

136 
apply (unfold supd_assn_def) 

137 
apply (simp (no_asm)) 

138 
done 

139 

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

141 
apply auto 

142 
done 

143 

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

145 
apply (auto simp del: split_paired_Ex) 

146 
done 

147 

148 
subsection "substres" 

149 

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

152 
where "P\<leftarrow>w = (\<lambda>Y. P w)" 

12854  153 

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

155 
apply (unfold subst_res_def) 

156 
apply (simp (no_asm)) 

157 
done 

158 

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

160 
apply (rule ext) 

161 
apply (simp (no_asm)) 

162 
done 

163 

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

165 
apply (rule ext) 

166 
apply (rule ext) 

167 
apply (simp (no_asm)) 

168 
done 

169 

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

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

172 
apply (rule ext) 

173 
by simp 

174 

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

176 
apply (rule ext) 

177 
by simp 

178 

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

180 
apply (rule ext) 

181 
by simp 

182 
*) 

183 

184 
subsection "substBool" 

185 

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

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

12854  189 

190 
lemma subst_Bool_def2 [simp]: 

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

192 
apply (unfold subst_Bool_def) 

193 
apply (simp (no_asm)) 

194 
done 

195 

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

197 
apply auto 

198 
done 

199 

200 
subsection "peekres" 

201 

37956  202 
definition 
203 
peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" 

204 
where "peek_res Pf = (\<lambda>Y. Pf Y Y)" 

12854  205 

206 
syntax 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

207 
"_peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_:. _" [0,3] 3) 
12854  208 
translations 
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

209 
"\<lambda>w:. P" == "CONST peek_res (\<lambda>w. P)" 
12854  210 

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

212 
apply (unfold peek_res_def) 

213 
apply (simp (no_asm)) 

214 
done 

215 

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

217 
apply (rule ext) 

218 
apply (simp (no_asm)) 

219 
done 

220 

221 
(* unused *) 

222 
lemma peek_subst_res_allI: 

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

224 
apply (rule allI) 

225 
apply (simp (no_asm)) 

226 
apply fast 

227 
done 

228 

229 
subsection "ignres" 

230 

37956  231 
definition 
232 
ign_res :: "'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000) 

233 
where "P\<down> = (\<lambda>Y s Z. \<exists>Y. P Y s Z)" 

12854  234 

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

236 
apply (unfold ign_res_def) 

237 
apply (simp (no_asm)) 

238 
done 

239 

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

241 
apply (rule ext) 

242 
apply (rule ext) 

243 
apply (rule ext) 

244 
apply (simp (no_asm)) 

245 
done 

246 

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

248 
apply (rule ext) 

249 
apply (rule ext) 

250 
apply (rule ext) 

251 
apply (simp (no_asm)) 

252 
done 

253 

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

255 
apply (rule ext) 

256 
apply (rule ext) 

257 
apply (rule ext) 

258 
apply (simp (no_asm)) 

259 
done 

260 

261 
subsection "peekst" 

262 

37956  263 
definition 
264 
peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" 

265 
where "peek_st P = (\<lambda>Y s. P (store s) Y s)" 

12854  266 

267 
syntax 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

268 
"_peek_st" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_.. _" [0,3] 3) 
12854  269 
translations 
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

270 
"\<lambda>s.. P" == "CONST peek_st (\<lambda>s. P)" 
12854  271 

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

273 
apply (unfold peek_st_def) 

274 
apply (simp (no_asm)) 

275 
done 

276 

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

278 
apply (rule ext) 

279 
apply (rule ext) 

280 
apply (simp (no_asm)) 

281 
done 

282 

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

284 
apply (rule ext) 

285 
apply (rule ext) 

286 
apply (simp (no_asm)) 

287 
done 

288 

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

290 
apply (rule ext) 

291 
apply (rule ext) 

292 
apply (simp (no_asm)) 

293 
done 

294 

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

296 
apply (rule ext) 

297 
apply (simp (no_asm)) 

298 
done 

299 

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

301 
apply (rule ext) 

302 
apply (rule ext) 

303 
apply (simp (no_asm)) 

304 
done 

305 

306 
subsection "ignreseq" 

307 

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

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

12854  311 

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

313 
apply (unfold ign_res_eq_def) 

314 
apply auto 

315 
done 

316 

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

318 
apply (rule ext) 

319 
apply (rule ext) 

320 
apply (rule ext) 

321 
apply (simp (no_asm)) 

322 
done 

323 

324 
(* unused *) 

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

326 
apply (rule ext) 

327 
apply (rule ext) 

328 
apply (rule ext) 

329 
apply (simp (no_asm)) 

330 
done 

331 

332 
(* unused *) 

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

334 
apply (simp (no_asm)) 

335 
done 

336 

337 
subsection "RefVar" 

338 

37956  339 
definition 
340 
RefVar :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr "..;" 13) 

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

12854  342 

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

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

345 
apply (unfold RefVar_def Let_def) 

346 
apply (simp (no_asm) add: split_beta) 

347 
done 

348 

349 
subsection "allocation" 

350 

37956  351 
definition 
352 
Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn" 

353 
where "Alloc G otag P = (\<lambda>Y s Z. \<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z)" 

12854  354 

37956  355 
definition 
356 
SXAlloc :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn" 

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

12854  358 

359 

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

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

362 
apply (unfold Alloc_def) 

363 
apply (simp (no_asm)) 

364 
done 

365 

366 
lemma SXAlloc_def2 [simp]: 

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

368 
apply (unfold SXAlloc_def) 

369 
apply (simp (no_asm)) 

370 
done 

371 

372 
section "validity" 

373 

37956  374 
definition 
375 
type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" where 

376 
"type_ok G t s = 

377 
(\<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 

378 
\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A ) 

379 
\<and> s\<Colon>\<preceq>(G,L))" 

12854  380 

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

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

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

41778  384 
type_synonym 'a triples = "'a triple set" 
12854  385 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

386 
abbreviation 
12854  387 
var_triple :: "['a assn, var ,'a assn] \<Rightarrow> 'a triple" 
388 
("{(1_)}/ _=>/ {(1_)}" [3,80,3] 75) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

389 
where "{P} e=> {Q} == {P} In2 e> {Q}" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

390 

af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

391 
abbreviation 
12854  392 
expr_triple :: "['a assn, expr ,'a assn] \<Rightarrow> 'a triple" 
393 
("{(1_)}/ _>/ {(1_)}" [3,80,3] 75) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

394 
where "{P} e> {Q} == {P} In1l e> {Q}" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

395 

af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

396 
abbreviation 
12854  397 
exprs_triple :: "['a assn, expr list ,'a assn] \<Rightarrow> 'a triple" 
398 
("{(1_)}/ _#>/ {(1_)}" [3,65,3] 75) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

399 
where "{P} e#> {Q} == {P} In3 e> {Q}" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

400 

af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

401 
abbreviation 
12854  402 
stmt_triple :: "['a assn, stmt, 'a assn] \<Rightarrow> 'a triple" 
403 
("{(1_)}/ ._./ {(1_)}" [3,65,3] 75) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

404 
where "{P} .c. {Q} == {P} In1r c> {Q}" 
12854  405 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

406 
notation (xsymbols) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

407 
triple ("{(1_)}/ _\<succ>/ {(1_)}" [3,65,3] 75) and 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

408 
var_triple ("{(1_)}/ _=\<succ>/ {(1_)}" [3,80,3] 75) and 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

409 
expr_triple ("{(1_)}/ _\<succ>/ {(1_)}" [3,80,3] 75) and 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

410 
exprs_triple ("{(1_)}/ _\<doteq>\<succ>/ {(1_)}" [3,65,3] 75) 
12854  411 

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

13585  413 
apply (rule inj_onI) 
12854  414 
apply auto 
415 
done 

416 

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

418 
apply auto 

419 
done 

420 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

421 
definition mtriples :: "('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<Rightarrow> 'sig \<Rightarrow> expr) \<Rightarrow> 
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

422 
('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<times> 'sig) set \<Rightarrow> 'a triples" ("{{(1_)}/ _\<succ>/ {(1_)}  _}"[3,65,3,65]75) where 
37956  423 
"{{P} tf\<succ> {Q}  ms} = (\<lambda>(C,sig). {Normal(P C sig)} tf C sig\<succ> {Q C sig})`ms" 
12854  424 

37956  425 
definition 
426 
triple_valid :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool" ("_\<Turnstile>_:_" [61,0, 58] 57) 

427 
where 

428 
"G\<Turnstile>n:t = 

429 
(case t of {P} t\<succ> {Q} \<Rightarrow> 

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

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

12854  432 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

433 
abbreviation 
37956  434 
triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool" ( "_=_:_" [61,0, 58] 57) 
435 
where "G=n:ts == Ball ts (triple_valid G n)" 

436 

437 
notation (xsymbols) 

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

439 

440 

441 
definition 

442 
ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_\<Turnstile>_" [61,58,58] 57) 

443 
where "(G,A\<Turnstile>ts) = (\<forall>n. G\<Turnstile>n:A \<longrightarrow> G\<Turnstile>n:ts)" 

12854  444 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

445 
abbreviation 
37956  446 
ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool" ( "_,_=_" [61,58,58] 57) 
447 
where "G,A =t == G,A\<Turnstile>{t}" 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

448 

af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

449 
notation (xsymbols) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

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

452 

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

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

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

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

457 
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

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

461 
done 

462 

463 

464 
declare split_paired_All [simp del] split_paired_Ex [simp del] 

465 
declare split_if [split del] split_if_asm [split del] 

466 
option.split [split del] option.split_asm [split del] 

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

12854  469 

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

473 
for G :: prog 

474 
where 

12854  475 

21765  476 
"G,A \<turnstile>t \<equiv> G,A\<turnstile>{t}" 
477 

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

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

12854  480 
G,A\<turnstile>insert t ts" 
481 

21765  482 
 asm: "ts\<subseteq>A \<Longrightarrow> G,A\<turnstile>ts" 
12854  483 

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

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

486 
G,A \<turnstile>ts" 

487 
*) 

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

21765  490 
 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  491 
(\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> 
492 
Q Y' s' Z )) 

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

494 

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

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

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

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

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

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

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

509 
{* expressions *} 
12854  510 

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

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

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

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

521 

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

525 

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

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

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

530 
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

531 

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

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

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

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

538 
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

539 

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

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

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

548 

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

552 

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

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

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

558 
l = locals (store s)) ;. 

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

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

561 
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

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

21765  564 
 Methd:"\<lbrakk>G,A\<union> {{P} Methd\<succ> {Q}  ms} \<turnstile> {{P} body G\<succ> {Q}  ms}\<rbrakk> \<Longrightarrow> 
12854  565 
G,A\<turnstile>{{P} Methd\<succ> {Q}  ms}" 
566 

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

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

571 

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

572 
{* expression lists *} 
12854  573 

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

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

579 

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

580 
{* statements *} 
12854  581 

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

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

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

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

593 

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

597 
(* unfolding variant of Loop, not needed here 

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

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

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

601 
*) 

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

605 

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

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

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

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

615 

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

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

620 

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

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

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

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

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

629 

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

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

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

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

633 
*} 
21765  634 
 InsInitV: " G,A\<turnstile>{Normal P} InsInitV c v=\<succ> {Q}" 
635 
 InsInitE: " G,A\<turnstile>{Normal P} InsInitE c e\<succ> {Q}" 

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

637 
 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

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

639 
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

640 
*) 
12854  641 

37956  642 
definition 
643 
adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" 

644 
where "adapt_pre P Q Q' = (\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z))" 

12854  645 

646 

647 
section "rules derived by induction" 

648 

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

650 
apply (unfold ax_valids_def) 

651 
apply fast 

652 
done 

653 

654 
(*if cut is available 

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

656 
G,A\<turnstile>ts" 

657 
b y etac ax_derivs.cut 1; 

658 
b y eatac ax_derivs.asm 1 1; 

659 
qed "ax_thin"; 

660 
*) 

661 
lemma ax_thin [rule_format (no_asm)]: 

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

663 
apply (erule ax_derivs.induct) 

42793  664 
apply (tactic "ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])") 
12854  665 
apply (rule ax_derivs.empty) 
666 
apply (erule (1) ax_derivs.insert) 

667 
apply (fast intro: ax_derivs.asm) 

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

669 
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

670 
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

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

672 
prefer 18 (* Methd *) 
23563  673 
apply (rule ax_derivs.Methd, drule spec, erule mp, fast) 
39159  674 
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros})) *}) 
23563  675 
apply auto 
12854  676 
done 
677 

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

679 
apply (erule ax_thin) 

680 
apply fast 

681 
done 

682 

683 
lemma subset_mtriples_iff: 

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

685 
apply (unfold mtriples_def) 

686 
apply (rule subset_image_iff) 

687 
done 

688 

689 
lemma weaken: 

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

691 
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

692 
(*42 subgoals*) 
12854  693 
apply (tactic "ALLGOALS strip_tac") 
39159  694 
apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD}, 
42793  695 
etac disjE, fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*}) 
12854  696 
apply (tactic "TRYALL hyp_subst_tac") 
697 
apply (simp, rule ax_derivs.empty) 

698 
apply (drule subset_insertD) 

699 
apply (blast intro: ax_derivs.insert) 

700 
apply (fast intro: ax_derivs.asm) 

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

702 
apply (fast intro: ax_derivs.weaken) 

703 
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

704 
(*37 subgoals*) 
39159  705 
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros}) 
42793  706 
THEN_ALL_NEW fast_tac @{context}) *}) 
12854  707 
(*1 subgoal*) 
708 
apply (clarsimp simp add: subset_mtriples_iff) 

709 
apply (rule ax_derivs.Methd) 

710 
apply (drule spec) 

711 
apply (erule impE) 

712 
apply (rule exI) 

713 
apply (erule conjI) 

714 
apply (rule HOL.refl) 

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

716 

717 

718 
section "rules derived from conseq" 

719 

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

720 
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

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

722 
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

723 
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

724 
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

725 
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

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

727 
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

728 
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

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

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

734 
apply (rule ax_derivs.conseq) 
12854  735 
apply clarsimp 
736 
apply blast 

737 
done 

738 

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

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

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

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

746 
done 

747 

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

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

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

754 
done 

755 

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

756 
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

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

760 
done 

761 

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

762 
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

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

766 
done 

767 

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

768 
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

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

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

771 
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

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

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

774 
apply (rule ax_derivs.conseq) 
12854  775 
apply force 
776 
done 

777 

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

779 
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

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

783 
apply (rule conseq12) 

784 
apply fast 

785 
apply auto 

786 
done 

787 
(*alternative (more direct) proof: 

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

789 
apply (fast) 

790 
*) 

791 

792 

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

793 
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

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

797 
done 

798 

799 
(* unused *) 

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

801 
apply auto 

802 
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

803 

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

804 
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

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

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

809 
apply (erule (1) ax_nochange_lemma) 

810 
done 

811 

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

813 
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

814 
apply (rule ax_derivs.conseq(* unused *)) 
12854  815 
apply auto 
816 
done 

817 

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

819 
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

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

821 
\<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  822 
apply (rule ax_escape (* unused *)) 
823 
apply safe 

824 
apply (erule conseq12, fast)+ 

825 
done 

826 

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

828 
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

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

832 
done 

833 

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

834 
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

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

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

839 
apply clarify 

840 
apply (case_tac "C s") 

841 
apply (erule conseq12, force)+ 

842 
done 

843 
(*alternative (more direct) proof: 

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

845 
apply clarify 

846 
apply (case_tac "C s") 

847 
apply force+ 

848 
*) 

849 

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

850 
lemma ax_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

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

854 
apply fast 

855 
done 

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

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

861 
apply fast 

862 
done 

863 

864 

865 
lemma adapt_pre_weakest: 

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

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

868 
apply (unfold adapt_pre_def) 

869 
apply (drule spec) 

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

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

872 
apply (simp add: ax_valids_def triple_valid_def2) 

873 
oops 

874 

875 
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

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

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

880 
done 

881 

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

882 
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

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

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

887 
done 

888 

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

890 

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

891 
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

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

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

896 
done 

897 

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

898 
lemma 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

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

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

903 

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

904 
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

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

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

909 

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

910 
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

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

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

915 

916 

917 
section "alternative axioms" 

918 

919 
lemma ax_Lit2: 

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

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

922 
apply force 

923 
done 

924 
lemma ax_Lit2_test_complete: 

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

926 
apply (rule ax_Lit2 [THEN conseq2]) 

927 
apply force 

928 
done 

929 

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

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

932 
apply force 

933 
done 

934 

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

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

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

938 
apply force 

939 
done 

940 

941 
lemma ax_Nil2: 

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

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

944 
apply force 

945 
done 

946 

947 

948 
section "misc derived structural rules" 

949 

950 
(* unused *) 

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

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

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

954 
apply (frule (1) finite_subset) 

24038  955 
apply (erule rev_mp) 
12854  956 
apply (erule thin_rl) 
957 
apply (erule finite_induct) 

958 
apply (unfold mtriples_def) 

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

960 
apply force 

961 
done 

962 
lemmas ax_finite_mtriples = ax_finite_mtriples_lemma [OF subset_refl] 

963 

964 
lemma ax_derivs_insertD: 

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

966 
apply (fast intro: ax_derivs.weaken) 

967 
done 

968 

969 
lemma ax_methods_spec: 

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

971 
apply (erule ax_derivs.weaken) 

972 
apply (force del: image_eqI intro: rev_image_eqI) 

973 
done 

974 

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

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

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

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

979 
apply (frule (1) finite_subset) 

24038  980 
apply (erule rev_mp) 
12854  981 
apply (erule thin_rl) 
982 
apply (erule finite_induct) 

983 
apply clarsimp+ 

984 
apply (drule ax_derivs_insertD) 

985 
apply (rule ax_derivs.insert) 

986 
apply (simp (no_asm_simp) only: split_tupled_all) 

987 
apply (auto elim: ax_methods_spec) 

988 
done 

989 
lemmas ax_finite_pointwise = ax_finite_pointwise_lemma [OF subset_refl] 

990 

991 
lemma ax_no_hazard: 

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

993 
apply (erule ax_cases) 

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

995 
apply force 

996 
done 

997 

998 
lemma ax_free_wt: 

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

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

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

1002 
apply (rule ax_no_hazard) 

1003 
apply (rule ax_escape) 

1004 
apply clarify 

1005 
apply (erule mp [THEN conseq12]) 

1006 
apply (auto simp add: type_ok_def) 

1007 
done 

1008 

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

21765  1012 
lemmas ax_Normal_cases = ax_cases [of _ _ _ normal] 
12854  1013 

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

1015 
apply (rule ax_Normal_cases) 

1016 
apply (rule ax_derivs.Skip) 

1017 
apply fast 

1018 
done 

45605  1019 
lemmas ax_SkipI = ax_Skip [THEN conseq1] 
12854  1020 

1021 

1022 
section "derived rules for methd call" 

1023 

1024 
lemma ax_Call_known_DynT: 

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

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

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

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

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

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

1031 
C = invocation_declclass 

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

1033 
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

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

1037 
apply (erule spec) 

1038 
apply (rule ax_escape, clarsimp) 

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

1040 
apply force 

1041 
done 

1042 

1043 

1044 
lemma ax_Call_Static: 

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

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

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

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

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

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

1051 
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

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

1055 
apply (erule spec) 

1056 
apply (rule ax_escape, clarsimp) 

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

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

20014  1059 
apply (force simp add: init_lvars_def Let_def) 
12854  1060 
done 
1061 

1062 
lemma ax_Methd1: 

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

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

1065 
apply (drule ax_derivs.Methd) 

1066 
apply (unfold mtriples_def) 

1067 
apply (erule (1) ax_methods_spec) 

1068 
done 

1069 

1070 
lemma ax_MethdN: 

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

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

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

1074 
apply (rule ax_Methd1) 

1075 
apply (rule_tac [2] singletonI) 

1076 
apply (unfold mtriples_def) 

1077 
apply clarsimp 

1078 
done 

1079 

1080 
lemma ax_StatRef: 

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

1082 
apply (rule ax_derivs.Cast) 

1083 
apply (rule ax_Lit2 [THEN conseq2]) 

1084 
apply clarsimp 

1085 
done 

1086 

1087 
section "rules derived from Init and Done" 

1088 

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

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

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

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

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

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

1095 
apply (erule ax_derivs.Init) 

1096 
apply (simp (no_asm_simp)) 

1097 
apply assumption 

1098 
done 

1099 

1100 
lemma ax_Init_Skip_lemma: 

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

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

1103 
apply (rule allI) 

1104 
apply (rule ax_SkipI) 

1105 
apply clarsimp 

1106 
done 

1107 

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

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

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

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

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

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

1114 
apply (simp (no_asm)) 

1115 
apply (erule (1) ax_InitS) 

1116 
apply simp 

1117 
apply (rule ax_Init_Skip_lemma) 

1118 
apply (erule conseq1) 

1119 
apply force 

1120 
done 

1121 

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

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

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

1125 
apply (rule ax_derivs.Init) 

1126 
apply (drule class_Object, force) 

1127 
apply (simp_all (no_asm)) 

1128 
apply (rule_tac [2] ax_Init_Skip_lemma) 

1129 
apply (rule ax_SkipI, force) 

1130 
done 

1131 

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

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

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

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

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

1137 
apply (erule ax_Init_Object [THEN conseq1]) 

1138 
apply force 

1139 
done 

1140 

1141 

1142 
section "introduction rules for Alloc and SXAlloc" 

1143 

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

1144 
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

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

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

1149 
done 

1150 

1151 
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

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

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

1154 
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

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

1158 
apply (auto elim!: halloc_elim_cases) 

1159 
done 

1160 

1161 
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

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

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

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

1165 
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

1166 
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

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

1170 
apply (auto elim!: halloc_elim_cases) 

1171 
done 

1172 

1173 
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

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

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

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

1177 
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

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

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

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

1183 
done 

1184 

1185 
end 