author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 41778  5f79a9e42507 
child 55417  01fbfb60c33e 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/State.thy 
12854  2 
Author: David von Oheimb 
3 
*) 

4 
header {* State for evaluation of Java expressions and statements *} 

5 

33965  6 
theory State 
7 
imports DeclConcepts 

8 
begin 

12854  9 

10 
text {* 

11 
design issues: 

12 
\begin{itemize} 

13 
\item all kinds of objects (class instances, arrays, and class objects) 

14 
are handeled via a general object abstraction 

15 
\item the heap and the map for class objects are combined into a single table 

16 
@{text "(recall (loc, obj) table \<times> (qtname, obj) table ~= (loc + qtname, obj) table)"} 

17 
\end{itemize} 

18 
*} 

19 

20 
section "objects" 

21 

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:
13524
diff
changeset

22 
datatype obj_tag = {* tag for generic object *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31127
diff
changeset

23 
CInst qtname {* class instance *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31127
diff
changeset

24 
 Arr ty int {* array with component type and length *} 
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:
13524
diff
changeset

25 
{*  CStat qtname the tag is irrelevant for a class object, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31127
diff
changeset

26 
i.e. the static fields of a class, 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

27 
since its type is given already by the reference to 
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:
13524
diff
changeset

28 
it (see below) *} 
12854  29 

41778  30 
type_synonym vn = "fspec + int" {* variable name *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31127
diff
changeset

31 
record obj = 
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:
13524
diff
changeset

32 
tag :: "obj_tag" {* generalized object *} 
31127  33 
"values" :: "(vn, val) table" 
12854  34 

35 
translations 

35431  36 
(type) "fspec" <= (type) "vname \<times> qtname" 
37 
(type) "vn" <= (type) "fspec + int" 

38 
(type) "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>" 

39 
(type) "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>" 

12854  40 

37956  41 
definition 
42 
the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table" 

43 
where "the_Arr obj = (SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>)" 

12854  44 

45 
lemma the_Arr_Arr [simp]: "the_Arr (Some \<lparr>tag=Arr T k,values=cs\<rparr>) = (T,k,cs)" 

46 
apply (auto simp: the_Arr_def) 

47 
done 

48 

49 
lemma the_Arr_Arr1 [simp,intro,dest]: 

50 
"\<lbrakk>tag obj = Arr T k\<rbrakk> \<Longrightarrow> the_Arr (Some obj) = (T,k,values obj)" 

51 
apply (auto simp add: the_Arr_def) 

52 
done 

53 

37956  54 
definition 
55 
upd_obj :: "vn \<Rightarrow> val \<Rightarrow> obj \<Rightarrow> obj" 

56 
where "upd_obj n v = (\<lambda>obj. obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>)" 

12854  57 

58 
lemma upd_obj_def2 [simp]: 

59 
"upd_obj n v obj = obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>" 

60 
apply (auto simp: upd_obj_def) 

61 
done 

62 

37956  63 
definition 
64 
obj_ty :: "obj \<Rightarrow> ty" where 

65 
"obj_ty obj = (case tag obj of 

66 
CInst C \<Rightarrow> Class C 

67 
 Arr T k \<Rightarrow> T.[])" 

12854  68 

69 
lemma obj_ty_eq [intro!]: "obj_ty \<lparr>tag=oi,values=x\<rparr> = obj_ty \<lparr>tag=oi,values=y\<rparr>" 

70 
by (simp add: obj_ty_def) 

71 

72 

73 
lemma obj_ty_eq1 [intro!,dest]: 

74 
"tag obj = tag obj' \<Longrightarrow> obj_ty obj = obj_ty obj'" 

75 
by (simp add: obj_ty_def) 

76 

77 
lemma obj_ty_cong [simp]: 

78 
"obj_ty (obj \<lparr>values:=vs\<rparr>) = obj_ty obj" 

79 
by auto 

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:
13524
diff
changeset

80 

12854  81 
lemma obj_ty_CInst [simp]: 
82 
"obj_ty \<lparr>tag=CInst C,values=vs\<rparr> = Class C" 

83 
by (simp add: obj_ty_def) 

84 

85 
lemma obj_ty_CInst1 [simp,intro!,dest]: 

86 
"\<lbrakk>tag obj = CInst C\<rbrakk> \<Longrightarrow> obj_ty obj = Class C" 

87 
by (simp add: obj_ty_def) 

88 

89 
lemma obj_ty_Arr [simp]: 

90 
"obj_ty \<lparr>tag=Arr T i,values=vs\<rparr> = T.[]" 

91 
by (simp add: obj_ty_def) 

92 

93 
lemma obj_ty_Arr1 [simp,intro!,dest]: 

94 
"\<lbrakk>tag obj = Arr T i\<rbrakk> \<Longrightarrow> obj_ty obj = T.[]" 

95 
by (simp add: obj_ty_def) 

96 

97 
lemma obj_ty_widenD: 

98 
"G\<turnstile>obj_ty obj\<preceq>RefT t \<Longrightarrow> (\<exists>C. tag obj = CInst C) \<or> (\<exists>T k. tag obj = Arr T k)" 

99 
apply (unfold obj_ty_def) 

100 
apply (auto split add: obj_tag.split_asm) 

101 
done 

102 

37956  103 
definition 
104 
obj_class :: "obj \<Rightarrow> qtname" where 

105 
"obj_class obj = (case tag obj of 

106 
CInst C \<Rightarrow> C 

107 
 Arr T k \<Rightarrow> Object)" 

12854  108 

109 

110 
lemma obj_class_CInst [simp]: "obj_class \<lparr>tag=CInst C,values=vs\<rparr> = C" 

111 
by (auto simp: obj_class_def) 

112 

113 
lemma obj_class_CInst1 [simp,intro!,dest]: 

114 
"tag obj = CInst C \<Longrightarrow> obj_class obj = C" 

115 
by (auto simp: obj_class_def) 

116 

117 
lemma obj_class_Arr [simp]: "obj_class \<lparr>tag=Arr T k,values=vs\<rparr> = Object" 

118 
by (auto simp: obj_class_def) 

119 

120 
lemma obj_class_Arr1 [simp,intro!,dest]: 

121 
"tag obj = Arr T k \<Longrightarrow> obj_class obj = Object" 

122 
by (auto simp: obj_class_def) 

123 

124 
lemma obj_ty_obj_class: "G\<turnstile>obj_ty obj\<preceq> Class statC = G\<turnstile>obj_class obj \<preceq>\<^sub>C statC" 

125 
apply (case_tac "tag obj") 

126 
apply (auto simp add: obj_ty_def obj_class_def) 

127 
apply (case_tac "statC = Object") 

128 
apply (auto dest: widen_Array_Class) 

129 
done 

130 

131 
section "object references" 

132 

41778  133 
type_synonym oref = "loc + qtname" {* generalized object reference *} 
12854  134 
syntax 
135 
Heap :: "loc \<Rightarrow> oref" 

136 
Stat :: "qtname \<Rightarrow> oref" 

137 

138 
translations 

33965  139 
"Heap" => "CONST Inl" 
140 
"Stat" => "CONST Inr" 

35431  141 
(type) "oref" <= (type) "loc + qtname" 
12854  142 

37956  143 
definition 
144 
fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool) \<Rightarrow> (fspec, ty) table" where 

145 
"fields_table G C P = 

146 
Option.map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))" 

12854  147 

148 
lemma fields_table_SomeI: 

149 
"\<lbrakk>table_of (DeclConcepts.fields G C) n = Some f; P n f\<rbrakk> 

150 
\<Longrightarrow> fields_table G C P n = Some (type f)" 

151 
apply (unfold fields_table_def) 

152 
apply clarsimp 

153 
apply (rule exI) 

154 
apply (rule conjI) 

155 
apply (erule map_of_filter_in) 

156 
apply assumption 

157 
apply simp 

158 
done 

159 

160 
(* unused *) 

161 
lemma fields_table_SomeD': "fields_table G C P fn = Some T \<Longrightarrow> 

162 
\<exists>f. (fn,f)\<in>set(DeclConcepts.fields G C) \<and> type f = T" 

163 
apply (unfold fields_table_def) 

164 
apply clarsimp 

165 
apply (drule map_of_SomeD) 

166 
apply auto 

167 
done 

168 

169 
lemma fields_table_SomeD: 

170 
"\<lbrakk>fields_table G C P fn = Some T; unique (DeclConcepts.fields G C)\<rbrakk> \<Longrightarrow> 

171 
\<exists>f. table_of (DeclConcepts.fields G C) fn = Some f \<and> type f = T" 

172 
apply (unfold fields_table_def) 

173 
apply clarsimp 

174 
apply (rule exI) 

175 
apply (rule conjI) 

176 
apply (erule table_of_filter_unique_SomeD) 

177 
apply assumption 

178 
apply simp 

179 
done 

180 

37956  181 
definition 
182 
in_bounds :: "int \<Rightarrow> int \<Rightarrow> bool" ("(_/ in'_bounds _)" [50, 51] 50) 

183 
where "i in_bounds k = (0 \<le> i \<and> i < k)" 

12854  184 

37956  185 
definition 
186 
arr_comps :: "'a \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a option" 

187 
where "arr_comps T k = (\<lambda>i. if i in_bounds k then Some T else None)" 

12854  188 

37956  189 
definition 
190 
var_tys :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> (vn, ty) table" where 

191 
"var_tys G oi r = 

192 
(case r of 

12854  193 
Heap a \<Rightarrow> (case oi of 
194 
CInst C \<Rightarrow> fields_table G C (\<lambda>n f. \<not>static f) (+) empty 

195 
 Arr T k \<Rightarrow> empty (+) arr_comps T k) 

196 
 Stat C \<Rightarrow> fields_table G C (\<lambda>fn f. declclassf fn = C \<and> static f) 

37956  197 
(+) empty)" 
12854  198 

199 
lemma var_tys_Some_eq: 

200 
"var_tys G oi r n = Some T 

201 
= (case r of 

202 
Inl a \<Rightarrow> (case oi of 

203 
CInst C \<Rightarrow> (\<exists>nt. n = Inl nt \<and> fields_table G C (\<lambda>n f. 

204 
\<not>static f) nt = Some T) 

205 
 Arr t k \<Rightarrow> (\<exists> i. n = Inr i \<and> i in_bounds k \<and> t = T)) 

206 
 Inr C \<Rightarrow> (\<exists>nt. n = Inl nt \<and> 

207 
fields_table G C (\<lambda>fn f. declclassf fn = C \<and> static f) nt 

208 
= Some T))" 

209 
apply (unfold var_tys_def arr_comps_def) 

210 
apply (force split add: sum.split_asm sum.split obj_tag.split) 

211 
done 

212 

213 

214 
section "stores" 

215 

41778  216 
type_synonym globs {* global variables: heap and static variables *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31127
diff
changeset

217 
= "(oref , obj) table" 
41778  218 
type_synonym heap 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31127
diff
changeset

219 
= "(loc , obj) table" 
41778  220 
(* type_synonym locals 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31127
diff
changeset

221 
= "(lname, val) table" *) (* defined in Value.thy local variables *) 
12854  222 

223 
translations 

35431  224 
(type) "globs" <= (type) "(oref , obj) table" 
225 
(type) "heap" <= (type) "(loc , obj) table" 

226 
(* (type) "locals" <= (type) "(lname, val) table" *) 

12854  227 

228 
datatype st = (* pure state, i.e. contents of all variables *) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31127
diff
changeset

229 
st globs locals 
12854  230 

231 
subsection "access" 

232 

37956  233 
definition 
234 
globs :: "st \<Rightarrow> globs" 

235 
where "globs = st_case (\<lambda>g l. g)" 

12854  236 

37956  237 
definition 
238 
locals :: "st \<Rightarrow> locals" 

239 
where "locals = st_case (\<lambda>g l. l)" 

12854  240 

37956  241 
definition heap :: "st \<Rightarrow> heap" where 
242 
"heap s = globs s \<circ> Heap" 

12854  243 

244 

245 
lemma globs_def2 [simp]: " globs (st g l) = g" 

246 
by (simp add: globs_def) 

247 

248 
lemma locals_def2 [simp]: "locals (st g l) = l" 

249 
by (simp add: locals_def) 

250 

251 
lemma heap_def2 [simp]: "heap s a=globs s (Heap a)" 

252 
by (simp add: heap_def) 

253 

254 

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

255 
abbreviation val_this :: "st \<Rightarrow> val" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

256 
where "val_this s == the (locals s This)" 
12854  257 

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

258 
abbreviation lookup_obj :: "st \<Rightarrow> val \<Rightarrow> obj" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

259 
where "lookup_obj s a' == the (heap s (the_Addr a'))" 
12854  260 

261 
subsection "memory allocation" 

262 

37956  263 
definition 
264 
new_Addr :: "heap \<Rightarrow> loc option" where 

265 
"new_Addr h = (if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None))" 

12854  266 

267 
lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None" 

18576  268 
apply (auto simp add: new_Addr_def) 
18447  269 
apply (erule someI) 
12854  270 
done 
271 

272 
lemma new_AddrD2: "new_Addr h = Some a \<Longrightarrow> \<forall>b. h b \<noteq> None \<longrightarrow> b \<noteq> a" 

273 
apply (drule new_AddrD) 

274 
apply auto 

275 
done 

276 

277 
lemma new_Addr_SomeI: "h a = None \<Longrightarrow> \<exists>b. new_Addr h = Some b \<and> h b = None" 

18576  278 
apply (simp add: new_Addr_def) 
18447  279 
apply (fast intro: someI2) 
12854  280 
done 
281 

282 

283 
subsection "initialization" 

284 

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

285 
abbreviation init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

286 
where "init_vals vs == Option.map default_val \<circ> vs" 
12854  287 

288 
lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty" 

289 
apply (unfold arr_comps_def in_bounds_def) 

290 
apply (rule ext) 

291 
apply auto 

292 
done 

293 

294 
lemma init_arr_comps_step [simp]: 

295 
"0 < j \<Longrightarrow> init_vals (arr_comps T j ) = 

296 
init_vals (arr_comps T (j  1))(j  1\<mapsto>default_val T)" 

297 
apply (unfold arr_comps_def in_bounds_def) 

298 
apply (rule ext) 

299 
apply auto 

300 
done 

301 

302 
subsection "update" 

303 

37956  304 
definition 
305 
gupd :: "oref \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st" ("gupd'(_\<mapsto>_')" [10, 10] 1000) 

306 
where "gupd r obj = st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)" 

12854  307 

37956  308 
definition 
309 
lupd :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" ("lupd'(_\<mapsto>_')" [10, 10] 1000) 

310 
where "lupd vn v = st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))" 

12854  311 

37956  312 
definition 
313 
upd_gobj :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" 

314 
where "upd_gobj r n v = st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)" 

12854  315 

37956  316 
definition 
317 
set_locals :: "locals \<Rightarrow> st \<Rightarrow> st" 

318 
where "set_locals l = st_case (\<lambda>g l'. st g l)" 

30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
28524
diff
changeset

319 

37956  320 
definition 
321 
init_obj :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st" 

322 
where "init_obj G oi r = gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)" 

12854  323 

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

324 
abbreviation 
12854  325 
init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st" 
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

326 
where "init_class_obj G C == init_obj G undefined (Inr C)" 
12854  327 

328 
lemma gupd_def2 [simp]: "gupd(r\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l" 

329 
apply (unfold gupd_def) 

330 
apply (simp (no_asm)) 

331 
done 

332 

333 
lemma lupd_def2 [simp]: "lupd(vn\<mapsto>v) (st g l) = st g (l(vn\<mapsto>v))" 

334 
apply (unfold lupd_def) 

335 
apply (simp (no_asm)) 

336 
done 

337 

338 
lemma globs_gupd [simp]: "globs (gupd(r\<mapsto>obj) s) = globs s(r\<mapsto>obj)" 

339 
apply (induct "s") 

340 
by (simp add: gupd_def) 

341 

342 
lemma globs_lupd [simp]: "globs (lupd(vn\<mapsto>v ) s) = globs s" 

343 
apply (induct "s") 

344 
by (simp add: lupd_def) 

345 

346 
lemma locals_gupd [simp]: "locals (gupd(r\<mapsto>obj) s) = locals s" 

347 
apply (induct "s") 

348 
by (simp add: gupd_def) 

349 

350 
lemma locals_lupd [simp]: "locals (lupd(vn\<mapsto>v ) s) = locals s(vn\<mapsto>v )" 

351 
apply (induct "s") 

352 
by (simp add: lupd_def) 

353 

354 
lemma globs_upd_gobj_new [rule_format (no_asm), simp]: 

355 
"globs s r = None \<longrightarrow> globs (upd_gobj r n v s) = globs s" 

356 
apply (unfold upd_gobj_def) 

357 
apply (induct "s") 

358 
apply auto 

359 
done 

360 

361 
lemma globs_upd_gobj_upd [rule_format (no_asm), simp]: 

362 
"globs s r=Some obj\<longrightarrow> globs (upd_gobj r n v s) = globs s(r\<mapsto>upd_obj n v obj)" 

363 
apply (unfold upd_gobj_def) 

364 
apply (induct "s") 

365 
apply auto 

366 
done 

367 

368 
lemma locals_upd_gobj [simp]: "locals (upd_gobj r n v s) = locals s" 

369 
apply (induct "s") 

370 
by (simp add: upd_gobj_def) 

371 

372 

373 
lemma globs_init_obj [simp]: "globs (init_obj G oi r s) t = 

374 
(if t=r then Some \<lparr>tag=oi,values=init_vals (var_tys G oi r)\<rparr> else globs s t)" 

375 
apply (unfold init_obj_def) 

376 
apply (simp (no_asm)) 

377 
done 

378 

379 
lemma locals_init_obj [simp]: "locals (init_obj G oi r s) = locals s" 

380 
by (simp add: init_obj_def) 

381 

382 
lemma surjective_st [simp]: "st (globs s) (locals s) = s" 

383 
apply (induct "s") 

384 
by auto 

385 

386 
lemma surjective_st_init_obj: 

387 
"st (globs (init_obj G oi r s)) (locals s) = init_obj G oi r s" 

388 
apply (subst locals_init_obj [THEN sym]) 

389 
apply (rule surjective_st) 

390 
done 

391 

392 
lemma heap_heap_upd [simp]: 

393 
"heap (st (g(Inl a\<mapsto>obj)) l) = heap (st g l)(a\<mapsto>obj)" 

394 
apply (rule ext) 

395 
apply (simp (no_asm)) 

396 
done 

397 
lemma heap_stat_upd [simp]: "heap (st (g(Inr C\<mapsto>obj)) l) = heap (st g l)" 

398 
apply (rule ext) 

399 
apply (simp (no_asm)) 

400 
done 

401 
lemma heap_local_upd [simp]: "heap (st g (l(vn\<mapsto>v))) = heap (st g l)" 

402 
apply (rule ext) 

403 
apply (simp (no_asm)) 

404 
done 

405 

406 
lemma heap_gupd_Heap [simp]: "heap (gupd(Heap a\<mapsto>obj) s) = heap s(a\<mapsto>obj)" 

407 
apply (rule ext) 

408 
apply (simp (no_asm)) 

409 
done 

410 
lemma heap_gupd_Stat [simp]: "heap (gupd(Stat C\<mapsto>obj) s) = heap s" 

411 
apply (rule ext) 

412 
apply (simp (no_asm)) 

413 
done 

414 
lemma heap_lupd [simp]: "heap (lupd(vn\<mapsto>v) s) = heap s" 

415 
apply (rule ext) 

416 
apply (simp (no_asm)) 

417 
done 

418 

419 
lemma heap_upd_gobj_Stat [simp]: "heap (upd_gobj (Stat C) n v s) = heap s" 

420 
apply (rule ext) 

421 
apply (simp (no_asm)) 

422 
apply (case_tac "globs s (Stat C)") 

423 
apply auto 

424 
done 

425 

426 
lemma set_locals_def2 [simp]: "set_locals l (st g l') = st g l" 

427 
apply (unfold set_locals_def) 

428 
apply (simp (no_asm)) 

429 
done 

430 

431 
lemma set_locals_id [simp]: "set_locals (locals s) s = s" 

432 
apply (unfold set_locals_def) 

433 
apply (induct_tac "s") 

434 
apply (simp (no_asm)) 

435 
done 

436 

437 
lemma set_set_locals [simp]: "set_locals l (set_locals l' s) = set_locals l s" 

438 
apply (unfold set_locals_def) 

439 
apply (induct_tac "s") 

440 
apply (simp (no_asm)) 

441 
done 

442 

443 
lemma locals_set_locals [simp]: "locals (set_locals l s) = l" 

444 
apply (unfold set_locals_def) 

445 
apply (induct_tac "s") 

446 
apply (simp (no_asm)) 

447 
done 

448 

449 
lemma globs_set_locals [simp]: "globs (set_locals l s) = globs s" 

450 
apply (unfold set_locals_def) 

451 
apply (induct_tac "s") 

452 
apply (simp (no_asm)) 

453 
done 

454 

455 
lemma heap_set_locals [simp]: "heap (set_locals l s) = heap s" 

456 
apply (unfold heap_def) 

457 
apply (induct_tac "s") 

458 
apply (simp (no_asm)) 

459 
done 

460 

461 

462 
section "abrupt completion" 

463 

464 

465 

37956  466 
primrec the_Xcpt :: "abrupt \<Rightarrow> xcpt" 
467 
where "the_Xcpt (Xcpt x) = x" 

12854  468 

37956  469 
primrec the_Jump :: "abrupt => jump" 
470 
where "the_Jump (Jump j) = j" 

12854  471 

37956  472 
primrec the_Loc :: "xcpt \<Rightarrow> loc" 
473 
where "the_Loc (Loc a) = a" 

12854  474 

37956  475 
primrec the_Std :: "xcpt \<Rightarrow> xname" 
476 
where "the_Std (Std x) = x" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31127
diff
changeset

477 

12854  478 

37956  479 
definition 
480 
abrupt_if :: "bool \<Rightarrow> abopt \<Rightarrow> abopt \<Rightarrow> abopt" 

481 
where "abrupt_if c x' x = (if c \<and> (x = None) then x' else x)" 

12854  482 

483 
lemma abrupt_if_True_None [simp]: "abrupt_if True x None = x" 

484 
by (simp add: abrupt_if_def) 

485 

486 
lemma abrupt_if_True_not_None [simp]: "x \<noteq> None \<Longrightarrow> abrupt_if True x y \<noteq> None" 

487 
by (simp add: abrupt_if_def) 

488 

489 
lemma abrupt_if_False [simp]: "abrupt_if False x y = y" 

490 
by (simp add: abrupt_if_def) 

491 

492 
lemma abrupt_if_Some [simp]: "abrupt_if c x (Some y) = Some y" 

493 
by (simp add: abrupt_if_def) 

494 

495 
lemma abrupt_if_not_None [simp]: "y \<noteq> None \<Longrightarrow> abrupt_if c x y = y" 

496 
apply (simp add: abrupt_if_def) 

497 
by auto 

498 

499 

500 
lemma split_abrupt_if: 

501 
"P (abrupt_if c x' x) = 

502 
((c \<and> x = None \<longrightarrow> P x') \<and> (\<not> (c \<and> x = None) \<longrightarrow> P x))" 

503 
apply (unfold abrupt_if_def) 

504 
apply (split split_if) 

505 
apply auto 

506 
done 

507 

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

508 
abbreviation raise_if :: "bool \<Rightarrow> xname \<Rightarrow> abopt \<Rightarrow> abopt" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

509 
where "raise_if c xn == abrupt_if c (Some (Xcpt (Std xn)))" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

510 

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

511 
abbreviation np :: "val \<Rightarrow> abopt \<Rightarrow> abopt" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

512 
where "np v == raise_if (v = Null) NullPointer" 
12854  513 

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

514 
abbreviation check_neg :: "val \<Rightarrow> abopt \<Rightarrow> abopt" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

515 
where "check_neg i' == raise_if (the_Intg i'<0) NegArrSize" 
12854  516 

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

517 
abbreviation error_if :: "bool \<Rightarrow> error \<Rightarrow> abopt \<Rightarrow> abopt" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

518 
where "error_if c e == abrupt_if c (Some (Error e))" 
12854  519 

520 
lemma raise_if_None [simp]: "(raise_if c x y = None) = (\<not>c \<and> y = None)" 

521 
apply (simp add: abrupt_if_def) 

522 
by auto 

523 
declare raise_if_None [THEN iffD1, dest!] 

524 

525 
lemma if_raise_if_None [simp]: 

526 
"((if b then y else raise_if c x y) = None) = ((c \<longrightarrow> b) \<and> y = None)" 

527 
apply (simp add: abrupt_if_def) 

528 
apply auto 

529 
done 

530 

531 
lemma raise_if_SomeD [dest!]: 

532 
"raise_if c x y = Some z \<Longrightarrow> c \<and> z=(Xcpt (Std x)) \<and> y=None \<or> (y=Some z)" 

533 
apply (case_tac y) 

534 
apply (case_tac c) 

535 
apply (simp add: abrupt_if_def) 

536 
apply (simp add: abrupt_if_def) 

537 
apply auto 

538 
done 

539 

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

540 
lemma error_if_None [simp]: "(error_if c e y = None) = (\<not>c \<and> y = None)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

541 
apply (simp add: abrupt_if_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

542 
by auto 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

543 
declare error_if_None [THEN iffD1, dest!] 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

544 

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

545 
lemma if_error_if_None [simp]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

546 
"((if b then y else error_if c e y) = None) = ((c \<longrightarrow> b) \<and> y = None)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

547 
apply (simp add: abrupt_if_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

548 
apply auto 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

550 

13524  551 
lemma error_if_SomeD [dest!]: 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

552 
"error_if c e y = Some z \<Longrightarrow> c \<and> z=(Error e) \<and> y=None \<or> (y=Some z)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

553 
apply (case_tac y) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

554 
apply (case_tac c) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

555 
apply (simp add: abrupt_if_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

556 
apply (simp add: abrupt_if_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

557 
apply auto 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

559 

37956  560 
definition 
561 
absorb :: "jump \<Rightarrow> abopt \<Rightarrow> abopt" 

562 
where "absorb j a = (if a=Some (Jump j) then None else a)" 

12854  563 

564 
lemma absorb_SomeD [dest!]: "absorb j a = Some x \<Longrightarrow> a = Some x" 

565 
by (auto simp add: absorb_def) 

566 

567 
lemma absorb_same [simp]: "absorb j (Some (Jump j)) = None" 

568 
by (auto simp add: absorb_def) 

569 

570 
lemma absorb_other [simp]: "a \<noteq> Some (Jump j) \<Longrightarrow> absorb j a = a" 

571 
by (auto simp add: absorb_def) 

572 

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:
13524
diff
changeset

573 
lemma absorb_Some_NoneD: "absorb j (Some abr) = None \<Longrightarrow> abr = Jump j" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

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

575 

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

576 
lemma absorb_Some_JumpD: "absorb j s = Some (Jump j') \<Longrightarrow> j'\<noteq>j" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

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

578 

12854  579 

580 
section "full program state" 

581 

41778  582 
type_synonym 
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:
13524
diff
changeset

583 
state = "abopt \<times> st" {* state including abruption information *} 
12854  584 

585 
translations 

35431  586 
(type) "abopt" <= (type) "abrupt option" 
587 
(type) "state" <= (type) "abopt \<times> st" 

12854  588 

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

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

590 
Norm :: "st \<Rightarrow> state" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

591 
where "Norm s == (None, s)" 
12854  592 

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

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

594 
abrupt :: "state \<Rightarrow> abopt" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

595 
where "abrupt == fst" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

596 

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

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

598 
store :: "state \<Rightarrow> st" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

599 
where "store == snd" 
12854  600 

601 
lemma single_stateE: "\<forall>Z. Z = (s::state) \<Longrightarrow> False" 

602 
apply (erule_tac x = "(Some k,y)" in all_dupE) 

603 
apply (erule_tac x = "(None,y)" in allE) 

604 
apply clarify 

605 
done 

606 

607 
lemma state_not_single: "All (op = (x::state)) \<Longrightarrow> R" 

608 
apply (drule_tac x = "(if abrupt x = None then Some ?x else None,?y)" in spec) 

609 
apply clarsimp 

610 
done 

611 

37956  612 
definition 
613 
normal :: "state \<Rightarrow> bool" 

614 
where "normal = (\<lambda>s. abrupt s = None)" 

12854  615 

616 
lemma normal_def2 [simp]: "normal s = (abrupt s = None)" 

617 
apply (unfold normal_def) 

618 
apply (simp (no_asm)) 

619 
done 

620 

37956  621 
definition 
622 
heap_free :: "nat \<Rightarrow> state \<Rightarrow> bool" 

623 
where "heap_free n = (\<lambda>s. atleast_free (heap (store s)) n)" 

12854  624 

625 
lemma heap_free_def2 [simp]: "heap_free n s = atleast_free (heap (store s)) n" 

626 
apply (unfold heap_free_def) 

627 
apply simp 

628 
done 

629 

630 
subsection "update" 

631 

37956  632 
definition 
633 
abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state" 

40607  634 
where "abupd f = map_pair f id" 
12854  635 

37956  636 
definition 
637 
supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state" 

40607  638 
where "supd = map_pair id" 
12854  639 

640 
lemma abupd_def2 [simp]: "abupd f (x,s) = (f x,s)" 

641 
by (simp add: abupd_def) 

642 

643 
lemma abupd_abrupt_if_False [simp]: "\<And> s. abupd (abrupt_if False xo) s = s" 

644 
by simp 

645 

646 
lemma supd_def2 [simp]: "supd f (x,s) = (x,f s)" 

647 
by (simp add: supd_def) 

648 

649 
lemma supd_lupd [simp]: 

650 
"\<And> s. supd (lupd vn v ) s = (abrupt s,lupd vn v (store s))" 

651 
apply (simp (no_asm_simp) only: split_tupled_all) 

652 
apply (simp (no_asm)) 

653 
done 

654 

655 

656 
lemma supd_gupd [simp]: 

657 
"\<And> s. supd (gupd r obj) s = (abrupt s,gupd r obj (store s))" 

658 
apply (simp (no_asm_simp) only: split_tupled_all) 

659 
apply (simp (no_asm)) 

660 
done 

661 

662 
lemma supd_init_obj [simp]: 

663 
"supd (init_obj G oi r) s = (abrupt s,init_obj G oi r (store s))" 

664 
apply (unfold init_obj_def) 

665 
apply (simp (no_asm)) 

666 
done 

667 

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:
13524
diff
changeset

668 
lemma abupd_store_invariant [simp]: "store (abupd f s) = store 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:
13524
diff
changeset

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

670 

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

671 
lemma supd_abrupt_invariant [simp]: "abrupt (supd f s) = abrupt 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:
13524
diff
changeset

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

673 

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

674 
abbreviation set_lvars :: "locals \<Rightarrow> state \<Rightarrow> state" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

675 
where "set_lvars l == supd (set_locals l)" 
12854  676 

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

677 
abbreviation restore_lvars :: "state \<Rightarrow> state \<Rightarrow> state" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

678 
where "restore_lvars s' s == set_lvars (locals (store s')) s" 
12854  679 

680 
lemma set_set_lvars [simp]: "\<And> s. set_lvars l (set_lvars l' s) = set_lvars l s" 

681 
apply (simp (no_asm_simp) only: split_tupled_all) 

682 
apply (simp (no_asm)) 

683 
done 

684 

685 
lemma set_lvars_id [simp]: "\<And> s. set_lvars (locals (store s)) s = s" 

686 
apply (simp (no_asm_simp) only: split_tupled_all) 

687 
apply (simp (no_asm)) 

688 
done 

689 

690 
section "initialisation test" 

691 

37956  692 
definition 
693 
inited :: "qtname \<Rightarrow> globs \<Rightarrow> bool" 

694 
where "inited C g = (g (Stat C) \<noteq> None)" 

12854  695 

37956  696 
definition 
697 
initd :: "qtname \<Rightarrow> state \<Rightarrow> bool" 

698 
where "initd C = inited C \<circ> globs \<circ> store" 

12854  699 

700 
lemma not_inited_empty [simp]: "\<not>inited C empty" 

701 
apply (unfold inited_def) 

702 
apply (simp (no_asm)) 

703 
done 

704 

705 
lemma inited_gupdate [simp]: "inited C (g(r\<mapsto>obj)) = (inited C g \<or> r = Stat C)" 

706 
apply (unfold inited_def) 

707 
apply (auto split add: st.split) 

708 
done 

709 

710 
lemma inited_init_class_obj [intro!]: "inited C (globs (init_class_obj G C s))" 

711 
apply (unfold inited_def) 

712 
apply (simp (no_asm)) 

713 
done 

714 

715 
lemma not_initedD: "\<not> inited C g \<Longrightarrow> g (Stat C) = None" 

716 
apply (unfold inited_def) 

717 
apply (erule notnotD) 

718 
done 

719 

720 
lemma initedD: "inited C g \<Longrightarrow> \<exists> obj. g (Stat C) = Some obj" 

721 
apply (unfold inited_def) 

722 
apply auto 

723 
done 

724 

725 
lemma initd_def2 [simp]: "initd C s = inited C (globs (store s))" 

726 
apply (unfold initd_def) 

727 
apply (simp (no_asm)) 

728 
done 

729 

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

730 
section {* @{text error_free} *} 
37956  731 

732 
definition 

733 
error_free :: "state \<Rightarrow> bool" 

734 
where "error_free s = (\<not> (\<exists> err. abrupt s = Some (Error err)))" 

12854  735 

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

736 
lemma error_free_Norm [simp,intro]: "error_free (Norm s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

737 
by (simp add: error_free_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

738 

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

739 
lemma error_free_normal [simp,intro]: "normal s \<Longrightarrow> error_free s" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

740 
by (simp add: error_free_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

741 

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

742 
lemma error_free_Xcpt [simp]: "error_free (Some (Xcpt x),s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

743 
by (simp add: error_free_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

744 

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

745 
lemma error_free_Jump [simp,intro]: "error_free (Some (Jump j),s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

746 
by (simp add: error_free_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

747 

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

748 
lemma error_free_Error [simp]: "error_free (Some (Error e),s) = False" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

749 
by (simp add: error_free_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

750 

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

751 
lemma error_free_Some [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

752 
"\<not> (\<exists> err. x=Error err) \<Longrightarrow> error_free ((Some x),s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

753 
by (auto simp add: error_free_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

754 

13524  755 
lemma error_free_abupd_absorb [simp,intro]: 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

756 
"error_free s \<Longrightarrow> error_free (abupd (absorb j) s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

757 
by (cases s) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

758 
(auto simp add: error_free_def absorb_def 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

759 
split: split_if_asm) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

760 

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

761 
lemma error_free_absorb [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

762 
"error_free (a,s) \<Longrightarrow> error_free (absorb j a, s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

763 
by (auto simp add: error_free_def absorb_def 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

764 
split: split_if_asm) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

765 

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

766 
lemma error_free_abrupt_if [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

767 
"\<lbrakk>error_free s; \<not> (\<exists> err. x=Error err)\<rbrakk> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

768 
\<Longrightarrow> error_free (abupd (abrupt_if p (Some x)) s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

769 
by (cases s) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

770 
(auto simp add: abrupt_if_def 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

771 
split: split_if) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

772 

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

773 
lemma error_free_abrupt_if1 [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

774 
"\<lbrakk>error_free (a,s); \<not> (\<exists> err. x=Error err)\<rbrakk> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

775 
\<Longrightarrow> error_free (abrupt_if p (Some x) a, s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

776 
by (auto simp add: abrupt_if_def 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

777 
split: split_if) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

778 

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

779 
lemma error_free_abrupt_if_Xcpt [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

780 
"error_free s 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

781 
\<Longrightarrow> error_free (abupd (abrupt_if p (Some (Xcpt x))) s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

782 
by simp 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

783 

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

784 
lemma error_free_abrupt_if_Xcpt1 [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

785 
"error_free (a,s) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

786 
\<Longrightarrow> error_free (abrupt_if p (Some (Xcpt x)) a, s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

787 
by simp 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

788 

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

789 
lemma error_free_abrupt_if_Jump [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

790 
"error_free s 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

791 
\<Longrightarrow> error_free (abupd (abrupt_if p (Some (Jump j))) s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

792 
by simp 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

793 

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

794 
lemma error_free_abrupt_if_Jump1 [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

795 
"error_free (a,s) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

796 
\<Longrightarrow> error_free (abrupt_if p (Some (Jump j)) a, s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

797 
by simp 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

798 

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

799 
lemma error_free_raise_if [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

800 
"error_free s \<Longrightarrow> error_free (abupd (raise_if p x) s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

801 
by simp 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

802 

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

803 
lemma error_free_raise_if1 [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

804 
"error_free (a,s) \<Longrightarrow> error_free ((raise_if p x a), s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

805 
by simp 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

806 

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

807 
lemma error_free_supd [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

808 
"error_free s \<Longrightarrow> error_free (supd f s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

809 
by (cases s) (simp add: error_free_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

810 

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

811 
lemma error_free_supd1 [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

812 
"error_free (a,s) \<Longrightarrow> error_free (a,f s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

813 
by (simp add: error_free_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

814 

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

815 
lemma error_free_set_lvars [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

816 
"error_free s \<Longrightarrow> error_free ((set_lvars l) s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

817 
by (cases s) simp 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

818 

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

819 
lemma error_free_set_locals [simp,intro]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

820 
"error_free (x, s) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

821 
\<Longrightarrow> error_free (x, set_locals l s')" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

822 
by (simp add: error_free_def) 
12854  823 

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:
13524
diff
changeset

824 

12854  825 
end 
826 