author  haftmann 
Fri, 17 Jun 2005 16:12:49 +0200  
changeset 16417  9bc16273c2d4 
parent 14981  e73f8140af78 
child 18447  da548623916a 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Example.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

4 
*) 

5 
header {* Example Bali program *} 

6 

16417  7 
theory Example imports Eval WellForm begin 
12854  8 

9 
text {* 

10 
The following example Bali program includes: 

11 
\begin{itemize} 

12 
\item class and interface declarations with inheritance, hiding of fields, 

13 
overriding of methods (with refined result type), array type, 

14 
\item method call (with dynamic binding), parameter access, return expressions, 

15 
\item expression statements, sequential composition, literal values, 

16 
local assignment, local access, field assignment, type cast, 

17 
\item exception generation and propagation, try and catch statement, throw 

18 
statement 

19 
\item instance creation and (default) static initialization 

20 
\end{itemize} 

21 
\begin{verbatim} 

22 
package java_lang 

23 

24 
public interface HasFoo { 

25 
public Base foo(Base z); 

26 
} 

27 

28 
public class Base implements HasFoo { 

29 
static boolean arr[] = new boolean[2]; 

30 
public HasFoo vee; 

31 
public Base foo(Base z) { 

32 
return z; 

33 
} 

34 
} 

35 

36 
public class Ext extends Base { 

37 
public int vee; 

38 
public Ext foo(Base z) { 

39 
((Ext)z).vee = 1; 

40 
return null; 

41 
} 

42 
} 

43 

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

44 
public class Main { 
12854  45 
public static void main(String args[]) throws Throwable { 
46 
Base e = new Ext(); 

47 
try {e.foo(null); } 

48 
catch(NullPointerException z) { 

49 
while(Ext.arr[2]) ; 

50 
} 

51 
} 

52 
} 

53 
\end{verbatim} 

54 
*} 

55 
declare widen.null [intro] 

56 

57 
lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))" 

58 
apply (unfold wf_fdecl_def) 

59 
apply (simp (no_asm)) 

60 
done 

61 

62 
declare wf_fdecl_def2 [iff] 

63 

64 

65 
section "type and expression names" 

66 

67 
(** unfortunately cannot simply instantiate tnam **) 

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

68 
datatype tnam_ = HasFoo_  Base_  Ext_  Main_ 
12854  69 
datatype vnam_ = arr_  vee_  z_  e_ 
70 
datatype label_ = lab1_ 

71 

72 
consts 

73 

74 
tnam_ :: "tnam_ \<Rightarrow> tnam" 

75 
vnam_ :: "vnam_ \<Rightarrow> vname" 

76 
label_:: "label_ \<Rightarrow> label" 

77 
axioms (** tnam_, vnam_ and label are intended to be isomorphic 

78 
to tnam, vname and label **) 

79 

80 
inj_tnam_ [simp]: "(tnam_ x = tnam_ y) = (x = y)" 

81 
inj_vnam_ [simp]: "(vnam_ x = vnam_ y) = (x = y)" 

82 
inj_label_ [simp]: "(label_ x = label_ y) = (x = y)" 

83 

84 

85 
surj_tnam_: "\<exists>m. n = tnam_ m" 

86 
surj_vnam_: "\<exists>m. n = vnam_ m" 

87 
surj_label_:" \<exists>m. n = label_ m" 

88 

89 
syntax 

90 

91 
HasFoo :: qtname 

92 
Base :: qtname 

93 
Ext :: qtname 

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

94 
Main :: qtname 
12854  95 
arr :: ename 
96 
vee :: ename 

97 
z :: ename 

98 
e :: ename 

99 
lab1:: label 

100 
translations 

101 

102 
"HasFoo" == "\<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>" 

103 
"Base" == "\<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>" 

104 
"Ext" == "\<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>" 

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

105 
"Main" == "\<lparr>pid=java_lang,tid=TName (tnam_ Main_)\<rparr>" 
12854  106 
"arr" == "(vnam_ arr_)" 
107 
"vee" == "(vnam_ vee_)" 

108 
"z" == "(vnam_ z_)" 

109 
"e" == "(vnam_ e_)" 

110 
"lab1" == "label_ lab1_" 

111 

112 

113 
lemma neq_Base_Object [simp]: "Base\<noteq>Object" 

114 
by (simp add: Object_def) 

115 

116 
lemma neq_Ext_Object [simp]: "Ext\<noteq>Object" 

117 
by (simp add: Object_def) 

118 

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

119 
lemma neq_Main_Object [simp]: "Main\<noteq>Object" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

121 

12854  122 
lemma neq_Base_SXcpt [simp]: "Base\<noteq>SXcpt xn" 
123 
by (simp add: SXcpt_def) 

124 

125 
lemma neq_Ext_SXcpt [simp]: "Ext\<noteq>SXcpt xn" 

126 
by (simp add: SXcpt_def) 

127 

13524  128 
lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn" 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

130 

12854  131 
section "classes and interfaces" 
132 

133 
defs 

134 

135 
Object_mdecls_def: "Object_mdecls \<equiv> []" 

136 
SXcpt_mdecls_def: "SXcpt_mdecls \<equiv> []" 

137 

138 
consts 

139 

140 
foo :: mname 

141 

142 
constdefs 

143 

144 
foo_sig :: sig 

145 
"foo_sig \<equiv> \<lparr>name=foo,parTs=[Class Base]\<rparr>" 

146 

147 
foo_mhead :: mhead 

148 
"foo_mhead \<equiv> \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>" 

149 

150 
constdefs 

151 

152 
Base_foo :: mdecl 

153 
"Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base, 

154 
mbody=\<lparr>lcls=[],stmt=Return (!!z)\<rparr>\<rparr>)" 

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

155 

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

156 
constdefs 
12854  157 
Ext_foo :: mdecl 
158 
"Ext_foo \<equiv> (foo_sig, 

159 
\<lparr>access=Public,static=False,pars=[z],resT=Class Ext, 

160 
mbody=\<lparr>lcls=[] 

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

161 
,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := 
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

162 
Lit (Intg 1)) ;; 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

163 
Return (Lit Null)\<rparr> 
12854  164 
\<rparr>)" 
165 

166 
constdefs 

167 

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

168 
arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

169 
"arr_viewed_from accC C \<equiv> {accC,Base,True}StatRef (ClassT C)..arr" 
12854  170 

171 
BaseCl :: class 

172 
"BaseCl \<equiv> \<lparr>access=Public, 

173 
cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>), 

174 
(vee, \<lparr>access=Public,static=False,type=Iface HasFoo \<rparr>)], 

175 
methods=[Base_foo], 

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

176 
init=Expr(arr_viewed_from Base Base 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

177 
:=New (PrimT Boolean)[Lit (Intg 2)]), 
12854  178 
super=Object, 
179 
superIfs=[HasFoo]\<rparr>" 

180 

181 
ExtCl :: class 

182 
"ExtCl \<equiv> \<lparr>access=Public, 

183 
cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)], 

184 
methods=[Ext_foo], 

185 
init=Skip, 

186 
super=Base, 

187 
superIfs=[]\<rparr>" 

188 

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

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

190 
"MainCl \<equiv> \<lparr>access=Public, 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

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

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

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

195 
superIfs=[]\<rparr>" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

196 
(* The "main" method is modeled seperately (see tprg) *) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

197 

12854  198 
constdefs 
199 

200 
HasFooInt :: iface 

201 
"HasFooInt \<equiv> \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>" 

202 

203 
Ifaces ::"idecl list" 

204 
"Ifaces \<equiv> [(HasFoo,HasFooInt)]" 

205 

206 
"Classes" ::"cdecl list" 

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

207 
"Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes" 
12854  208 

209 
lemmas table_classes_defs = 

210 
Classes_def standard_classes_def ObjectC_def SXcptC_def 

211 

212 
lemma table_ifaces [simp]: "table_of Ifaces = empty(HasFoo\<mapsto>HasFooInt)" 

213 
apply (unfold Ifaces_def) 

214 
apply (simp (no_asm)) 

215 
done 

216 

217 
lemma table_classes_Object [simp]: 

218 
"table_of Classes Object = Some \<lparr>access=Public,cfields=[] 

219 
,methods=Object_mdecls 

220 
,init=Skip,super=arbitrary,superIfs=[]\<rparr>" 

221 
apply (unfold table_classes_defs) 

222 
apply (simp (no_asm) add:Object_def) 

223 
done 

224 

225 
lemma table_classes_SXcpt [simp]: 

226 
"table_of Classes (SXcpt xn) 

227 
= Some \<lparr>access=Public,cfields=[],methods=SXcpt_mdecls, 

228 
init=Skip, 

229 
super=if xn = Throwable then Object else SXcpt Throwable, 

230 
superIfs=[]\<rparr>" 

231 
apply (unfold table_classes_defs) 

232 
apply (induct_tac xn) 

233 
apply (simp add: Object_def SXcpt_def)+ 

234 
done 

235 

236 
lemma table_classes_HasFoo [simp]: "table_of Classes HasFoo = None" 

237 
apply (unfold table_classes_defs) 

238 
apply (simp (no_asm) add: Object_def SXcpt_def) 

239 
done 

240 

241 
lemma table_classes_Base [simp]: "table_of Classes Base = Some BaseCl" 

242 
apply (unfold table_classes_defs ) 

243 
apply (simp (no_asm) add: Object_def SXcpt_def) 

244 
done 

245 

246 
lemma table_classes_Ext [simp]: "table_of Classes Ext = Some ExtCl" 

247 
apply (unfold table_classes_defs ) 

248 
apply (simp (no_asm) add: Object_def SXcpt_def) 

249 
done 

250 

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

251 
lemma table_classes_Main [simp]: "table_of Classes Main = Some MainCl" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

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

254 
done 
12854  255 

256 
section "program" 

257 

258 
syntax 

259 
tprg :: prog 

260 

261 
translations 

262 
"tprg" == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>" 

263 

264 
constdefs 

265 
test :: "(ty)list \<Rightarrow> stmt" 

266 
"test pTs \<equiv> e:==NewC Ext;; 

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

267 
\<spacespace> Try Expr({Main,ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null])) 
12854  268 
\<spacespace> Catch((SXcpt NullPointer) z) 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

269 
(lab1\<bullet> While(Acc 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

270 
(Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip)" 
12854  271 

272 

273 
section "wellstructuredness" 

274 

275 
lemma not_Object_subcls_any [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ \<Longrightarrow> R" 

276 
apply (auto dest!: tranclD subcls1D) 

277 
done 

278 

279 
lemma not_Throwable_subcls_SXcpt [elim!]: 

280 
"(SXcpt Throwable, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R" 

281 
apply (auto dest!: tranclD subcls1D) 

282 
apply (simp add: Object_def SXcpt_def) 

283 
done 

284 

285 
lemma not_SXcpt_n_subcls_SXcpt_n [elim!]: 

286 
"(SXcpt xn, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R" 

287 
apply (auto dest!: tranclD subcls1D) 

288 
apply (drule rtranclD) 

289 
apply auto 

290 
done 

291 

292 
lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+ \<Longrightarrow> R" 

293 
apply (auto dest!: tranclD subcls1D simp add: BaseCl_def) 

294 
done 

295 

296 
lemma not_TName_n_subcls_TName_n [rule_format (no_asm), elim!]: 

297 
"(\<lparr>pid=java_lang,tid=TName tn\<rparr>, \<lparr>pid=java_lang,tid=TName tn\<rparr>) 

298 
\<in> (subcls1 tprg)^+ \<longrightarrow> R" 

299 
apply (rule_tac n1 = "tn" in surj_tnam_ [THEN exE]) 

300 
apply (erule ssubst) 

301 
apply (rule tnam_.induct) 

302 
apply safe 

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

303 
apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def MainCl_def) 
12854  304 
apply (drule rtranclD) 
305 
apply auto 

306 
done 

307 

308 

309 
lemma ws_idecl_HasFoo: "ws_idecl tprg HasFoo []" 

310 
apply (unfold ws_idecl_def) 

311 
apply (simp (no_asm)) 

312 
done 

313 

314 
lemma ws_cdecl_Object: "ws_cdecl tprg Object any" 

315 
apply (unfold ws_cdecl_def) 

316 
apply auto 

317 
done 

318 

319 
lemma ws_cdecl_Throwable: "ws_cdecl tprg (SXcpt Throwable) Object" 

320 
apply (unfold ws_cdecl_def) 

321 
apply auto 

322 
done 

323 

324 
lemma ws_cdecl_SXcpt: "ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)" 

325 
apply (unfold ws_cdecl_def) 

326 
apply auto 

327 
done 

328 

329 
lemma ws_cdecl_Base: "ws_cdecl tprg Base Object" 

330 
apply (unfold ws_cdecl_def) 

331 
apply auto 

332 
done 

333 

334 
lemma ws_cdecl_Ext: "ws_cdecl tprg Ext Base" 

335 
apply (unfold ws_cdecl_def) 

336 
apply auto 

337 
done 

338 

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

339 
lemma ws_cdecl_Main: "ws_cdecl tprg Main Object" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

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

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

343 

12854  344 
lemmas ws_cdecls = ws_cdecl_SXcpt ws_cdecl_Object ws_cdecl_Throwable 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

345 
ws_cdecl_Base ws_cdecl_Ext ws_cdecl_Main 
12854  346 

347 
declare not_Object_subcls_any [rule del] 

348 
not_Throwable_subcls_SXcpt [rule del] 

349 
not_SXcpt_n_subcls_SXcpt_n [rule del] 

350 
not_Base_subcls_Ext [rule del] not_TName_n_subcls_TName_n [rule del] 

351 

352 
lemma ws_idecl_all: 

353 
"G=tprg \<Longrightarrow> (\<forall>(I,i)\<in>set Ifaces. ws_idecl G I (isuperIfs i))" 

354 
apply (simp (no_asm) add: Ifaces_def HasFooInt_def) 

355 
apply (auto intro!: ws_idecl_HasFoo) 

356 
done 

357 

358 
lemma ws_cdecl_all: "G=tprg \<Longrightarrow> (\<forall>(C,c)\<in>set Classes. ws_cdecl G C (super c))" 

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

359 
apply (simp (no_asm) add: Classes_def BaseCl_def ExtCl_def MainCl_def) 
12854  360 
apply (auto intro!: ws_cdecls simp add: standard_classes_def ObjectC_def 
361 
SXcptC_def) 

362 
done 

363 

364 
lemma ws_tprg: "ws_prog tprg" 

365 
apply (unfold ws_prog_def) 

366 
apply (auto intro!: ws_idecl_all ws_cdecl_all) 

367 
done 

368 

369 

370 
section "misc program properties (independent of wellstructuredness)" 

371 

372 
lemma single_iface [simp]: "is_iface tprg I = (I = HasFoo)" 

373 
apply (unfold Ifaces_def) 

374 
apply (simp (no_asm)) 

375 
done 

376 

377 
lemma empty_subint1 [simp]: "subint1 tprg = {}" 

378 
apply (unfold subint1_def Ifaces_def HasFooInt_def) 

379 
apply auto 

380 
done 

381 

382 
lemma unique_ifaces: "unique Ifaces" 

383 
apply (unfold Ifaces_def) 

384 
apply (simp (no_asm)) 

385 
done 

386 

387 
lemma unique_classes: "unique Classes" 

388 
apply (unfold table_classes_defs ) 

389 
apply (simp ) 

390 
done 

391 

392 
lemma SXcpt_subcls_Throwable [simp]: "tprg\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable" 

393 
apply (rule SXcpt_subcls_Throwable_lemma) 

394 
apply auto 

395 
done 

396 

397 
lemma Ext_subclseq_Base [simp]: "tprg\<turnstile>Ext \<preceq>\<^sub>C Base" 

398 
apply (rule subcls_direct1) 

399 
apply (simp (no_asm) add: ExtCl_def) 

400 
apply (simp add: Object_def) 

401 
apply (simp (no_asm)) 

402 
done 

403 

404 
lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext \<prec>\<^sub>C Base" 

405 
apply (rule subcls_direct2) 

406 
apply (simp (no_asm) add: ExtCl_def) 

407 
apply (simp add: Object_def) 

408 
apply (simp (no_asm)) 

409 
done 

410 

411 

412 

413 
section "fields and method lookup" 

414 

415 
lemma fields_tprg_Object [simp]: "DeclConcepts.fields tprg Object = []" 

416 
by (rule ws_tprg [THEN fields_emptyI], force+) 

417 

418 
lemma fields_tprg_Throwable [simp]: 

419 
"DeclConcepts.fields tprg (SXcpt Throwable) = []" 

420 
by (rule ws_tprg [THEN fields_emptyI], force+) 

421 

422 
lemma fields_tprg_SXcpt [simp]: "DeclConcepts.fields tprg (SXcpt xn) = []" 

423 
apply (case_tac "xn = Throwable") 

424 
apply (simp (no_asm_simp)) 

425 
by (rule ws_tprg [THEN fields_emptyI], force+) 

426 

427 
lemmas fields_rec_ = fields_rec [OF _ ws_tprg] 

428 

429 
lemma fields_Base [simp]: 

430 
"DeclConcepts.fields tprg Base 

431 
= [((arr,Base), \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>), 

432 
((vee,Base), \<lparr>access=Public,static=False,type=Iface HasFoo \<rparr>)]" 

433 
apply (subst fields_rec_) 

434 
apply (auto simp add: BaseCl_def) 

435 
done 

436 

437 
lemma fields_Ext [simp]: 

438 
"DeclConcepts.fields tprg Ext 

439 
= [((vee,Ext), \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)] 

440 
@ DeclConcepts.fields tprg Base" 

441 
apply (rule trans) 

442 
apply (rule fields_rec_) 

443 
apply (auto simp add: ExtCl_def Object_def) 

444 
done 

445 

446 
lemmas imethds_rec_ = imethds_rec [OF _ ws_tprg] 

447 
lemmas methd_rec_ = methd_rec [OF _ ws_tprg] 

448 

449 
lemma imethds_HasFoo [simp]: 

450 
"imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))" 

451 
apply (rule trans) 

452 
apply (rule imethds_rec_) 

453 
apply (auto simp add: HasFooInt_def) 

454 
done 

455 

456 
lemma methd_tprg_Object [simp]: "methd tprg Object = empty" 

457 
apply (subst methd_rec_) 

458 
apply (auto simp add: Object_mdecls_def) 

459 
done 

460 

461 
lemma methd_Base [simp]: 

462 
"methd tprg Base = table_of [(\<lambda>(s,m). (s, Base, m)) Base_foo]" 

463 
apply (rule trans) 

464 
apply (rule methd_rec_) 

465 
apply (auto simp add: BaseCl_def) 

466 
done 

467 

468 
lemma memberid_Base_foo_simp [simp]: 

469 
"memberid (mdecl Base_foo) = mid foo_sig" 

470 
by (simp add: Base_foo_def) 

471 

472 
lemma memberid_Ext_foo_simp [simp]: 

473 
"memberid (mdecl Ext_foo) = mid foo_sig" 

474 
by (simp add: Ext_foo_def) 

475 

476 
lemma Base_declares_foo: 

477 
"tprg\<turnstile>mdecl Base_foo declared_in Base" 

478 
by (auto simp add: declared_in_def cdeclaredmethd_def BaseCl_def Base_foo_def) 

479 

480 
lemma foo_sig_not_undeclared_in_Base: 

481 
"\<not> tprg\<turnstile>mid foo_sig undeclared_in Base" 

482 
proof  

483 
from Base_declares_foo 

484 
show ?thesis 

485 
by (auto dest!: declared_not_undeclared ) 

486 
qed 

487 

488 
lemma Ext_declares_foo: 

489 
"tprg\<turnstile>mdecl Ext_foo declared_in Ext" 

490 
by (auto simp add: declared_in_def cdeclaredmethd_def ExtCl_def Ext_foo_def) 

491 

492 
lemma foo_sig_not_undeclared_in_Ext: 

493 
"\<not> tprg\<turnstile>mid foo_sig undeclared_in Ext" 

494 
proof  

495 
from Ext_declares_foo 

496 
show ?thesis 

497 
by (auto dest!: declared_not_undeclared ) 

498 
qed 

499 

500 
lemma Base_foo_not_inherited_in_Ext: 

501 
"\<not> tprg \<turnstile> Ext inherits (Base,mdecl Base_foo)" 

502 
by (auto simp add: inherits_def foo_sig_not_undeclared_in_Ext) 

503 

504 
lemma Ext_method_inheritance: 

505 
"filter_tab (\<lambda>sig m. tprg \<turnstile> Ext inherits method sig m) 

506 
(empty(fst ((\<lambda>(s, m). (s, Base, m)) Base_foo)\<mapsto> 

507 
snd ((\<lambda>(s, m). (s, Base, m)) Base_foo))) 

508 
= empty" 

509 
proof  

510 
from Base_foo_not_inherited_in_Ext 

511 
show ?thesis 

512 
by (auto intro: filter_tab_all_False simp add: Base_foo_def) 

513 
qed 

514 

515 

516 
lemma methd_Ext [simp]: "methd tprg Ext = 

517 
table_of [(\<lambda>(s,m). (s, Ext, m)) Ext_foo]" 

518 
apply (rule trans) 

519 
apply (rule methd_rec_) 

520 
apply (auto simp add: ExtCl_def Object_def Ext_method_inheritance) 

521 
done 

522 

523 
section "accessibility" 

524 

525 
lemma classesDefined: 

526 
"\<lbrakk>class tprg C = Some c; C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class tprg (super c) = Some sc" 

527 
apply (auto simp add: Classes_def standard_classes_def 

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

528 
BaseCl_def ExtCl_def MainCl_def 
12854  529 
SXcptC_def ObjectC_def) 
530 
done 

531 

532 
lemma superclassesBase [simp]: "superclasses tprg Base={Object}" 

533 
proof  

534 
have ws: "ws_prog tprg" by (rule ws_tprg) 

535 
then show ?thesis 

536 
by (auto simp add: superclasses_rec BaseCl_def) 

537 
qed 

538 

539 
lemma superclassesExt [simp]: "superclasses tprg Ext={Base,Object}" 

540 
proof  

541 
have ws: "ws_prog tprg" by (rule ws_tprg) 

542 
then show ?thesis 

543 
by (auto simp add: superclasses_rec ExtCl_def BaseCl_def) 

544 
qed 

545 

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

546 
lemma superclassesMain [simp]: "superclasses tprg Main={Object}" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

548 
have ws: "ws_prog tprg" by (rule ws_tprg) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

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

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

552 

12854  553 
lemma HasFoo_accessible[simp]:"tprg\<turnstile>(Iface HasFoo) accessible_in P" 
554 
by (simp add: accessible_in_RefT_simp is_public_def HasFooInt_def) 

555 

556 
lemma HasFoo_is_acc_iface[simp]: "is_acc_iface tprg P HasFoo" 

557 
by (simp add: is_acc_iface_def) 

558 

559 
lemma HasFoo_is_acc_type[simp]: "is_acc_type tprg P (Iface HasFoo)" 

560 
by (simp add: is_acc_type_def) 

561 

562 
lemma Base_accessible[simp]:"tprg\<turnstile>(Class Base) accessible_in P" 

563 
by (simp add: accessible_in_RefT_simp is_public_def BaseCl_def) 

564 

565 
lemma Base_is_acc_class[simp]: "is_acc_class tprg P Base" 

566 
by (simp add: is_acc_class_def) 

567 

568 
lemma Base_is_acc_type[simp]: "is_acc_type tprg P (Class Base)" 

569 
by (simp add: is_acc_type_def) 

570 

571 
lemma Ext_accessible[simp]:"tprg\<turnstile>(Class Ext) accessible_in P" 

572 
by (simp add: accessible_in_RefT_simp is_public_def ExtCl_def) 

573 

574 
lemma Ext_is_acc_class[simp]: "is_acc_class tprg P Ext" 

575 
by (simp add: is_acc_class_def) 

576 

577 
lemma Ext_is_acc_type[simp]: "is_acc_type tprg P (Class Ext)" 

578 
by (simp add: is_acc_type_def) 

579 

580 
lemma accmethd_tprg_Object [simp]: "accmethd tprg S Object = empty" 

581 
apply (unfold accmethd_def) 

582 
apply (simp) 

583 
done 

584 

585 
lemma snd_special_simp: "snd ((\<lambda>(s, m). (s, a, m)) x) = (a,snd x)" 

586 
by (cases x) (auto) 

587 

588 
lemma fst_special_simp: "fst ((\<lambda>(s, m). (s, a, m)) x) = fst x" 

589 
by (cases x) (auto) 

590 

591 
lemma foo_sig_undeclared_in_Object: 

592 
"tprg\<turnstile>mid foo_sig undeclared_in Object" 

593 
by (auto simp add: undeclared_in_def cdeclaredmethd_def Object_mdecls_def) 

594 

595 
lemma unique_sig_Base_foo: 

596 
"tprg\<turnstile> mdecl (sig, snd Base_foo) declared_in Base \<Longrightarrow> sig=foo_sig" 

597 
by (auto simp add: declared_in_def cdeclaredmethd_def 

598 
Base_foo_def BaseCl_def) 

599 

600 
lemma Base_foo_no_override: 

601 
"tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides old \<Longrightarrow> P" 

602 
apply (drule overrides_commonD) 

603 
apply (clarsimp) 

604 
apply (frule subclsEval) 

605 
apply (rule ws_tprg) 

606 
apply (simp) 

607 
apply (rule classesDefined) 

608 
apply assumption+ 

609 
apply (frule unique_sig_Base_foo) 

610 
apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object 

611 
dest: unique_sig_Base_foo) 

612 
done 

613 

614 
lemma Base_foo_no_stat_override: 

615 
"tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides\<^sub>S old \<Longrightarrow> P" 

616 
apply (drule stat_overrides_commonD) 

617 
apply (clarsimp) 

618 
apply (frule subclsEval) 

619 
apply (rule ws_tprg) 

620 
apply (simp) 

621 
apply (rule classesDefined) 

622 
apply assumption+ 

623 
apply (frule unique_sig_Base_foo) 

624 
apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object 

625 
dest: unique_sig_Base_foo) 

626 
done 

627 

628 

629 
lemma Base_foo_no_hide: 

630 
"tprg,sig\<turnstile>(Base,(snd Base_foo)) hides old \<Longrightarrow> P" 

631 
by (auto dest: hidesD simp add: Base_foo_def member_is_static_simp) 

632 

633 
lemma Ext_foo_no_hide: 

634 
"tprg,sig\<turnstile>(Ext,(snd Ext_foo)) hides old \<Longrightarrow> P" 

635 
by (auto dest: hidesD simp add: Ext_foo_def member_is_static_simp) 

636 

637 
lemma unique_sig_Ext_foo: 

638 
"tprg\<turnstile> mdecl (sig, snd Ext_foo) declared_in Ext \<Longrightarrow> sig=foo_sig" 

639 
by (auto simp add: declared_in_def cdeclaredmethd_def 

640 
Ext_foo_def ExtCl_def) 

641 

642 
lemma Ext_foo_override: 

643 
"tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides old 

644 
\<Longrightarrow> old = (Base,(snd Base_foo))" 

645 
apply (drule overrides_commonD) 

646 
apply (clarsimp) 

647 
apply (frule subclsEval) 

648 
apply (rule ws_tprg) 

649 
apply (simp) 

650 
apply (rule classesDefined) 

651 
apply assumption+ 

652 
apply (frule unique_sig_Ext_foo) 

653 
apply (case_tac "old") 

654 
apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 

655 
apply (auto simp add: ExtCl_def Ext_foo_def 

656 
BaseCl_def Base_foo_def Object_mdecls_def 

657 
split_paired_all 

658 
member_is_static_simp 

659 
dest: declared_not_undeclared unique_declaration) 

660 
done 

661 

662 
lemma Ext_foo_stat_override: 

663 
"tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides\<^sub>S old 

664 
\<Longrightarrow> old = (Base,(snd Base_foo))" 

665 
apply (drule stat_overrides_commonD) 

666 
apply (clarsimp) 

667 
apply (frule subclsEval) 

668 
apply (rule ws_tprg) 

669 
apply (simp) 

670 
apply (rule classesDefined) 

671 
apply assumption+ 

672 
apply (frule unique_sig_Ext_foo) 

673 
apply (case_tac "old") 

674 
apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 

675 
apply (auto simp add: ExtCl_def Ext_foo_def 

676 
BaseCl_def Base_foo_def Object_mdecls_def 

677 
split_paired_all 

678 
member_is_static_simp 

679 
dest: declared_not_undeclared unique_declaration) 

680 
done 

681 

682 
lemma Base_foo_member_of_Base: 

683 
"tprg\<turnstile>(Base,mdecl Base_foo) member_of Base" 

684 
by (auto intro!: members.Immediate Base_declares_foo) 

685 

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

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

687 
"tprg\<turnstile>(Base,mdecl Base_foo) member_in Base" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

688 
by (rule member_of_to_member_in [OF Base_foo_member_of_Base]) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

689 

12854  690 
lemma Ext_foo_member_of_Ext: 
691 
"tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext" 

692 
by (auto intro!: members.Immediate Ext_declares_foo) 

693 

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

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

695 
"tprg\<turnstile>(Ext,mdecl Ext_foo) member_in Ext" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

696 
by (rule member_of_to_member_in [OF Ext_foo_member_of_Ext]) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

697 

12854  698 
lemma Base_foo_permits_acc: 
14030  699 
"tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_from S" 
12854  700 
by ( simp add: permits_acc_def Base_foo_def) 
701 

702 
lemma Base_foo_accessible [simp]: 

703 
"tprg\<turnstile>(Base,mdecl Base_foo) of Base accessible_from S" 

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

704 
by (auto intro: accessible_fromR.Immediate 
12854  705 
Base_foo_member_of_Base Base_foo_permits_acc) 
706 

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

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

708 
"tprg\<turnstile>(Base,mdecl Base_foo) in Base dyn_accessible_from S" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

709 
apply (rule dyn_accessible_fromR.Immediate) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

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

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

713 

12854  714 
lemma accmethd_Base [simp]: 
715 
"accmethd tprg S Base = methd tprg Base" 

716 
apply (simp add: accmethd_def) 

717 
apply (rule filter_tab_all_True) 

718 
apply (simp add: snd_special_simp fst_special_simp) 

719 
done 

720 

721 
lemma Ext_foo_permits_acc: 

14030  722 
"tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_from S" 
12854  723 
by ( simp add: permits_acc_def Ext_foo_def) 
724 

725 
lemma Ext_foo_accessible [simp]: 

726 
"tprg\<turnstile>(Ext,mdecl Ext_foo) of Ext accessible_from S" 

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

727 
by (auto intro: accessible_fromR.Immediate 
12854  728 
Ext_foo_member_of_Ext Ext_foo_permits_acc) 
729 

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

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

731 
"tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from S" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

732 
apply (rule dyn_accessible_fromR.Immediate) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

734 
apply (rule Ext_foo_permits_acc) 
12854  735 
done 
736 

737 
lemma Ext_foo_overrides_Base_foo: 

738 
"tprg\<turnstile>(Ext,Ext_foo) overrides (Base,Base_foo)" 

739 
proof (rule overridesR.Direct, simp_all) 

740 
show "\<not> is_static Ext_foo" 

741 
by (simp add: member_is_static_simp Ext_foo_def) 

742 
show "\<not> is_static Base_foo" 

743 
by (simp add: member_is_static_simp Base_foo_def) 

744 
show "accmodi Ext_foo \<noteq> Private" 

745 
by (simp add: Ext_foo_def) 

746 
show "msig (Ext, Ext_foo) = msig (Base, Base_foo)" 

747 
by (simp add: Ext_foo_def Base_foo_def) 

748 
show "tprg\<turnstile>mdecl Ext_foo declared_in Ext" 

749 
by (auto intro: Ext_declares_foo) 

750 
show "tprg\<turnstile>mdecl Base_foo declared_in Base" 

751 
by (auto intro: Base_declares_foo) 

752 
show "tprg \<turnstile>(Base, mdecl Base_foo) inheritable_in java_lang" 

753 
by (simp add: inheritable_in_def Base_foo_def) 

754 
show "tprg\<turnstile>resTy Ext_foo\<preceq>resTy Base_foo" 

755 
by (simp add: Ext_foo_def Base_foo_def mhead_resTy_simp) 

756 
qed 

757 

758 
lemma accmethd_Ext [simp]: 

759 
"accmethd tprg S Ext = methd tprg Ext" 

760 
apply (simp add: accmethd_def) 

761 
apply (rule filter_tab_all_True) 

762 
apply (auto simp add: snd_special_simp fst_special_simp) 

763 
done 

764 

765 
lemma cls_Ext: "class tprg Ext = Some ExtCl" 

766 
by simp 

767 
lemma dynmethd_Ext_foo: 

768 
"dynmethd tprg Base Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 

769 
= Some (Ext,snd Ext_foo)" 

770 
proof  

771 
have "methd tprg Base \<lparr>name = foo, parTs = [Class Base]\<rparr> 

772 
= Some (Base,snd Base_foo)" and 

773 
"methd tprg Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 

774 
= Some (Ext,snd Ext_foo)" 

775 
by (auto simp add: Ext_foo_def Base_foo_def foo_sig_def) 

776 
with cls_Ext ws_tprg Ext_foo_overrides_Base_foo 

777 
show ?thesis 

778 
by (auto simp add: dynmethd_rec simp add: Ext_foo_def Base_foo_def) 

779 
qed 

780 

781 
lemma Base_fields_accessible[simp]: 

782 
"accfield tprg S Base 

783 
= table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))" 

784 
apply (auto simp add: accfield_def expand_fun_eq Let_def 

785 
accessible_in_RefT_simp 

786 
is_public_def 

787 
BaseCl_def 

788 
permits_acc_def 

789 
declared_in_def 

790 
cdeclaredfield_def 

791 
intro!: filter_tab_all_True_Some filter_tab_None 

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

792 
accessible_fromR.Immediate 
12854  793 
intro: members.Immediate) 
794 
done 

795 

796 

797 
lemma arr_member_of_Base: 

798 
"tprg\<turnstile>(Base, fdecl (arr, 

799 
\<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>)) 

800 
member_of Base" 

801 
by (auto intro: members.Immediate 

802 
simp add: declared_in_def cdeclaredfield_def BaseCl_def) 

803 

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

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

805 
"tprg\<turnstile>(Base, fdecl (arr, 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

806 
\<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>)) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

808 
by (rule member_of_to_member_in [OF arr_member_of_Base]) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

809 

12854  810 
lemma arr_member_of_Ext: 
811 
"tprg\<turnstile>(Base, fdecl (arr, 

812 
\<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>)) 

813 
member_of Ext" 

814 
apply (rule members.Inherited) 

815 
apply (simp add: inheritable_in_def) 

816 
apply (simp add: undeclared_in_def cdeclaredfield_def ExtCl_def) 

817 
apply (auto intro: arr_member_of_Base simp add: subcls1_def ExtCl_def) 

818 
done 

819 

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

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

821 
"tprg\<turnstile>(Base, fdecl (arr, 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

822 
\<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>)) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

824 
by (rule member_of_to_member_in [OF arr_member_of_Ext]) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

825 

12854  826 
lemma Ext_fields_accessible[simp]: 
827 
"accfield tprg S Ext 

828 
= table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))" 

829 
apply (auto simp add: accfield_def expand_fun_eq Let_def 

830 
accessible_in_RefT_simp 

831 
is_public_def 

832 
BaseCl_def 

833 
ExtCl_def 

834 
permits_acc_def 

835 
intro!: filter_tab_all_True_Some filter_tab_None 

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

836 
accessible_fromR.Immediate) 
12854  837 
apply (auto intro: members.Immediate arr_member_of_Ext 
838 
simp add: declared_in_def cdeclaredfield_def ExtCl_def) 

839 
done 

840 

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

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

842 
"tprg\<turnstile>(Base, fdecl (arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>)) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

844 
apply (rule dyn_accessible_fromR.Immediate) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

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

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

848 

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

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

850 
"tprg\<turnstile>(Base, fdecl (arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>)) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

852 
apply (rule dyn_accessible_fromR.Immediate) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

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

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

856 

12854  857 
lemma array_of_PrimT_acc [simp]: 
858 
"is_acc_type tprg java_lang (PrimT t.[])" 

859 
apply (simp add: is_acc_type_def accessible_in_RefT_simp) 

860 
done 

861 

862 
lemma PrimT_acc [simp]: 

863 
"is_acc_type tprg java_lang (PrimT t)" 

864 
apply (simp add: is_acc_type_def accessible_in_RefT_simp) 

865 
done 

866 

867 
lemma Object_acc [simp]: 

868 
"is_acc_class tprg java_lang Object" 

869 
apply (auto simp add: is_acc_class_def accessible_in_RefT_simp is_public_def) 

870 
done 

871 

872 

873 
section "wellformedness" 

874 

875 

876 
lemma wf_HasFoo: "wf_idecl tprg (HasFoo, HasFooInt)" 

877 
apply (unfold wf_idecl_def HasFooInt_def) 

878 
apply (auto intro!: wf_mheadI ws_idecl_HasFoo 

879 
simp add: foo_sig_def foo_mhead_def mhead_resTy_simp 

880 
member_is_static_simp ) 

881 
done 

882 

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

883 

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

884 
declare member_is_static_simp [simp] 
12854  885 
declare wt.Skip [rule del] wt.Init [rule del] 
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

886 
ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

887 
lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

888 
lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

889 

12854  890 
lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def 
891 
lemmas Ext_foo_defs = Ext_foo_def foo_sig_def 

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

892 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

893 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

894 

12854  895 

896 
lemma wf_Base_foo: "wf_mdecl tprg Base Base_foo" 

897 
apply (unfold Base_foo_defs ) 

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

898 
apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs 
12854  899 
simp add: mhead_resTy_simp) 
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

900 
(* for definite assignment *) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

901 
apply (rule exI) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

902 
apply (simp add: parameters_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

903 
apply (rule conjI) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

904 
apply (rule da.Comp) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

905 
apply (rule da.Expr) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

906 
apply (rule da.AssLVar) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

907 
apply (rule da.AccLVar) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

908 
apply (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

909 
apply (rule assigned.select_convs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

910 
apply (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

911 
apply (rule assigned.select_convs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

912 
apply (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

913 
apply (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

914 
apply (rule da.Jmp) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

915 
apply (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

916 
apply (rule assigned.select_convs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

917 
apply (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

918 
apply (rule assigned.select_convs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

919 
apply (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

920 
apply (simp) 
12854  921 
done 
922 

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

923 

12854  924 
lemma wf_Ext_foo: "wf_mdecl tprg Ext Ext_foo" 
925 
apply (unfold Ext_foo_defs ) 

926 
apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs 

927 
simp add: mhead_resTy_simp ) 

928 
apply (rule wt.Cast) 

929 
prefer 2 

930 
apply simp 

931 
apply (rule_tac [2] narrow.subcls [THEN cast.narrow]) 

932 
apply (auto intro!: wtIs) 

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

933 
(* for definite assignment *) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

934 
apply (rule exI) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

935 
apply (simp add: parameters_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

936 
apply (rule conjI) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

937 
apply (rule da.Comp) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

938 
apply (rule da.Expr) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

939 
apply (rule da.Ass) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

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

941 
apply (rule da.FVar) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

942 
apply (rule da.Cast) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

943 
apply (rule da.AccLVar) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

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

945 
apply (rule assigned.select_convs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

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

947 
apply (rule da_Lit) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

948 
apply (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

949 
apply (rule da.Comp) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

950 
apply (rule da.Expr) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

951 
apply (rule da.AssLVar) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

952 
apply (rule da.Lit) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

953 
apply (rule assigned.select_convs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

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

955 
apply (rule da.Jmp) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

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

957 
apply (rule assigned.select_convs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

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

959 
apply (rule assigned.select_convs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

960 
apply (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

961 
apply (rule assigned.select_convs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

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

963 
apply simp 
12854  964 
done 
965 

966 
declare mhead_resTy_simp [simp add] 

967 
declare member_is_static_simp [simp add] 

968 

969 
lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)" 

970 
apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def) 

971 
apply (auto intro!: wf_Base_foo) 

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

972 
apply (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_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

973 
apply (auto intro!: wtIs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

974 
(* for definite assignment *) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

975 
apply (rule exI) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

976 
apply (rule da.Expr) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

977 
apply (rule da.Ass) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

978 
apply (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

979 
apply (rule da.FVar) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

980 
apply (rule da.Cast) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

981 
apply (rule da_Lit) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

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

983 
apply (rule da.NewA) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

984 
apply (rule da.Lit) 
12854  985 
apply (auto simp add: Base_foo_defs entails_def Let_def) 
986 
apply (insert Base_foo_no_stat_override, simp add: Base_foo_def,blast)+ 

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

987 
apply (insert Base_foo_no_hide , simp add: Base_foo_def,blast) 
12854  988 
done 
989 

990 

991 
lemma wf_ExtC: "wf_cdecl tprg (Ext,ExtCl)" 

992 
apply (unfold wf_cdecl_def ExtCl_def) 

993 
apply (auto intro!: wf_Ext_foo ws_cdecl_Ext) 

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

994 
apply (auto simp add: entails_def snd_special_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

995 
apply (insert Ext_foo_stat_override) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

996 
apply (rule exI,rule da.Skip) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

997 
apply (force simp add: qmdecl_def Ext_foo_def Base_foo_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

998 
apply (force simp add: qmdecl_def Ext_foo_def Base_foo_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

999 
apply (force simp add: qmdecl_def Ext_foo_def Base_foo_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

1000 
apply (insert Ext_foo_no_hide) 
12854  1001 
apply (simp_all add: qmdecl_def) 
1002 
apply blast+ 

1003 
done 

1004 

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

1005 
lemma wf_MainC: "wf_cdecl tprg (Main,MainCl)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

1006 
apply (unfold wf_cdecl_def MainCl_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

1007 
apply (auto intro: ws_cdecl_Main) 
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

1008 
apply (rule exI,rule da.Skip) 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

1010 

12854  1011 
lemma wf_idecl_all: "p=tprg \<Longrightarrow> Ball (set Ifaces) (wf_idecl p)" 
1012 
apply (simp (no_asm) add: Ifaces_def) 

1013 
apply (simp (no_asm_simp)) 

1014 
apply (rule wf_HasFoo) 

1015 
done 

1016 

1017 
lemma wf_cdecl_all_standard_classes: 

1018 
"Ball (set standard_classes) (wf_cdecl tprg)" 

1019 
apply (unfold standard_classes_def Let_def 

1020 
ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def) 

1021 
apply (simp (no_asm) add: wf_cdecl_def ws_cdecls) 

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

1022 
apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_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

1023 
intro: da.Skip) 
12854  1024 
apply (auto simp add: Object_def Classes_def standard_classes_def 
1025 
SXcptC_def SXcpt_def) 

1026 
done 

1027 

1028 
lemma wf_cdecl_all: "p=tprg \<Longrightarrow> Ball (set Classes) (wf_cdecl p)" 

1029 
apply (simp (no_asm) add: Classes_def) 

1030 
apply (simp (no_asm_simp)) 

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

1031 
apply (rule wf_BaseC [THEN conjI]) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

1032 
apply (rule wf_ExtC [THEN conjI]) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

1033 
apply (rule wf_MainC [THEN conjI]) 
12854  1034 
apply (rule wf_cdecl_all_standard_classes) 
1035 
done 

1036 

1037 
theorem wf_tprg: "wf_prog tprg" 

1038 
apply (unfold wf_prog_def Let_def) 

1039 
apply (simp (no_asm) add: unique_ifaces unique_classes) 

1040 
apply (rule conjI) 

1041 
apply ((simp (no_asm) add: Classes_def standard_classes_def)) 

1042 
apply (rule conjI) 

1043 
apply (simp add: Object_mdecls_def) 

1044 
apply safe 

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

1045 
apply (cut_tac xn_cases) 
12854  1046 
apply (simp (no_asm_simp) add: Classes_def standard_classes_def) 
1047 
apply (insert wf_idecl_all) 

1048 
apply (insert wf_cdecl_all) 

1049 
apply auto 

1050 
done 

1051 

1052 
section "max spec" 

1053 

1054 
lemma appl_methds_Base_foo: 

1055 
"appl_methds tprg S (ClassT Base) \<lparr>name=foo, parTs=[NT]\<rparr> = 

1056 
{((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>) 

1057 
,[Class Base])}" 

1058 
apply (unfold appl_methds_def) 

1059 
apply (simp (no_asm)) 

1060 
apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base") 

1061 
apply (auto simp add: cmheads_def Base_foo_defs) 

1062 
done 

1063 

1064 
lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = 

1065 
{((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>) 

1066 
, [Class Base])}" 

1067 
apply (unfold max_spec_def) 

1068 
apply (simp (no_asm) add: appl_methds_Base_foo) 

1069 
apply auto 

1070 
done 

1071 

1072 
section "welltypedness" 

1073 

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

1074 
lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>" 
12854  1075 
apply (unfold test_def arr_viewed_from_def) 
1076 
(* ?pTs = [Class Base] *) 

1077 
apply (rule wtIs (* ;; *)) 

1078 
apply (rule wtIs (* Ass *)) 

1079 
apply (rule wtIs (* NewC *)) 

1080 
apply (rule wtIs (* LVar *)) 

1081 
apply (simp) 

1082 
apply (simp) 

1083 
apply (simp) 

1084 
apply (rule wtIs (* NewC *)) 

1085 
apply (simp) 

1086 
apply (simp) 

1087 
apply (rule wtIs (* Try *)) 

1088 
prefer 4 

1089 
apply (simp) 

1090 
defer 

1091 
apply (rule wtIs (* Expr *)) 

1092 
apply (rule wtIs (* Call *)) 

1093 
apply (rule wtIs (* Acc *)) 

1094 
apply (rule wtIs (* LVar *)) 

1095 
apply (simp) 

1096 
apply (simp) 

1097 
apply (rule wtIs (* Cons *)) 

1098 
apply (rule wtIs (* Lit *)) 

1099 
apply (simp) 

1100 
apply (rule wtIs (* Nil *)) 

1101 
apply (simp) 

1102 
apply (rule max_spec_Base_foo) 

1103 
apply (simp) 

1104 
apply (simp) 

1105 
apply (simp) 

1106 
apply (simp) 

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

1107 
apply (simp) 
12854  1108 
apply (rule wtIs (* While *)) 
1109 
apply (rule wtIs (* Acc *)) 

1110 
apply (rule wtIs (* AVar *)) 

1111 
apply (rule wtIs (* Acc *)) 

1112 
apply (rule wtIs (* FVar *)) 

1113 
apply (rule wtIs (* StatRef *)) 

1114 
apply (simp) 

1115 
apply (simp) 

1116 
apply (simp ) 

1117 
apply (simp) 

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

1118 
apply (simp) 
12854  1119 
apply (rule wtIs (* LVar *)) 
1120 
apply (simp) 

1121 
apply (rule wtIs (* Skip *)) 

1122 
done 

1123 

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

1124 
section "definite assignment" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1125 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1126 
lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1127 
\<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1128 
apply (unfold test_def arr_viewed_from_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

1129 
apply (rule da.Comp) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1130 
apply (rule da.Expr) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1131 
apply (rule da.AssLVar) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1132 
apply (rule da.NewC) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1133 
apply (rule assigned.select_convs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1134 
apply (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

1135 
apply (rule da.Try) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1136 
apply (rule da.Expr) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1137 
apply (rule da.Call) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1138 
apply (rule da.AccLVar) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1139 
apply (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

1140 
apply (rule assigned.select_convs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1141 
apply (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

1142 
apply (rule da.Cons) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1143 
apply (rule da.Lit) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1144 
apply (rule da.Nil) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1145 
apply (rule da.Loop) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1146 
apply (rule da.Acc) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1147 
apply (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

1148 
apply (rule da.AVar) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1149 
apply (rule da.Acc) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

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

1151 
apply (rule da.FVar) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1152 
apply (rule da.Cast) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1153 
apply (rule da.Lit) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1154 
apply (rule da.Lit) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1155 
apply (rule da_Skip) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1156 
apply (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

1157 
apply (simp,rule assigned.select_convs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1158 
apply (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

1159 
apply (simp,rule assigned.select_convs) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1160 
apply (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

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

1162 
apply blast 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

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

1164 
apply (simp add: intersect_ts_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

1165 
done 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1166 

12854  1167 

1168 
section "execution" 

1169 

1170 
lemma alloc_one: "\<And>a obj. \<lbrakk>the (new_Addr h) = a; atleast_free h (Suc n)\<rbrakk> \<Longrightarrow> 

1171 
new_Addr h = Some a \<and> atleast_free (h(a\<mapsto>obj)) n" 

1172 
apply (frule atleast_free_SucD) 

1173 
apply (drule atleast_free_Suc [THEN iffD1]) 

1174 
apply clarsimp 

1175 
apply (frule new_Addr_SomeI) 

1176 
apply force 

1177 
done 

1178 

1179 
declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp] 

1180 
declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp] 

1181 
declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp] 

1182 
Base_foo_defs [simp] 

1183 

1184 
ML {* bind_thms ("eval_intros", map 

1185 
(simplify (simpset() delsimps [thm "Skip_eq"] 

1186 
addsimps [thm "lvar_def"]) o 

1187 
rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *} 

1188 
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros 

1189 

1190 
consts 

1191 
a :: loc 

1192 
b :: loc 

1193 
c :: loc 

1194 

1195 
syntax 

1196 

1197 
tprg :: prog 

1198 

1199 
obj_a :: obj 

1200 
obj_b :: obj 

1201 
obj_c :: obj 

1202 
arr_N :: "(vn, val) table" 

1203 
arr_a :: "(vn, val) table" 

1204 
globs1 :: globs 

1205 
globs2 :: globs 

1206 
globs3 :: globs 

1207 
globs8 :: globs 

1208 
locs3 :: locals 

1209 
locs4 :: locals 

1210 
locs8 :: locals 

1211 
s0 :: state 

1212 
s0' :: state 

1213 
s9' :: state 

1214 
s1 :: state 

1215 
s1' :: state 

1216 
s2 :: state 

1217 
s2' :: state 

1218 
s3 :: state 

1219 
s3' :: state 

1220 
s4 :: state 

1221 
s4' :: state 

1222 
s6' :: state 

1223 
s7' :: state 

1224 
s8 :: state 

1225 
s8' :: state 

1226 

1227 
translations 

1228 

1229 
"tprg" == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>" 

1230 

1231 
"obj_a" <= "\<lparr>tag=Arr (PrimT Boolean) two 

1232 
,values=empty(Inr 0\<mapsto>Bool False)(Inr one\<mapsto>Bool False)\<rparr>" 

1233 
"obj_b" <= "\<lparr>tag=CInst Ext 

1234 
,values=(empty(Inl (vee, Base)\<mapsto>Null ) 

1235 
(Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>" 

1236 
"obj_c" == "\<lparr>tag=CInst (SXcpt NullPointer),values=empty\<rparr>" 

1237 
"arr_N" == "empty(Inl (arr, Base)\<mapsto>Null)" 

1238 
"arr_a" == "empty(Inl (arr, Base)\<mapsto>Addr a)" 

1239 
"globs1" == "empty(Inr Ext \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>) 

1240 
(Inr Base \<mapsto>\<lparr>tag=arbitrary, values=arr_N\<rparr>) 

1241 
(Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)" 

1242 
"globs2" == "empty(Inr Ext \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>) 

1243 
(Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>) 

1244 
(Inl a\<mapsto>obj_a) 

1245 
(Inr Base \<mapsto>\<lparr>tag=arbitrary, values=arr_a\<rparr>)" 

1246 
"globs3" == "globs2(Inl b\<mapsto>obj_b)" 

1247 
"globs8" == "globs3(Inl c\<mapsto>obj_c)" 

1248 
"locs3" == "empty(VName e\<mapsto>Addr b)" 

1249 
"locs4" == "empty(VName z\<mapsto>Null)(Inr()\<mapsto>Addr b)" 

1250 
"locs8" == "locs3(VName z\<mapsto>Addr c)" 

1251 
"s0" == " st empty empty" 

1252 
"s0'" == " Norm s0" 

1253 
"s1" == " st globs1 empty" 

1254 
"s1'" == " Norm s1" 

1255 
"s2" == " st globs2 empty" 

1256 
"s2'" == " Norm s2" 

1257 
"s3" == " st globs3 locs3 " 

1258 
"s3'" == " Norm s3" 

1259 
"s4" == " st globs3 locs4" 

1260 
"s4'" == " Norm s4" 

1261 
"s6'" == "(Some (Xcpt (Std NullPointer)), s4)" 

1262 
"s7'" == "(Some (Xcpt (Std NullPointer)), s3)" 

1263 
"s8" == " st globs8 locs8" 

1264 
"s8'" == " Norm s8" 

1265 
"s9'" == "(Some (Xcpt (Std IndOutBound)), s8)" 

1266 

1267 

1268 
syntax "four"::nat 

1269 
"tree"::nat 

1270 
"two" ::nat 

1271 
"one" ::nat 

1272 
translations 

1273 
"one" == "Suc 0" 

1274 
"two" == "Suc one" 

1275 
"tree" == "Suc two" 

1276 
"four" == "Suc tree" 

1277 

1278 
declare Pair_eq [simp del] 

1279 
lemma exec_test: 

1280 
"\<lbrakk>the (new_Addr (heap s1)) = a; 

1281 
the (new_Addr (heap ?s2)) = b; 

1282 
the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow> 

1283 
atleast_free (heap s0) four \<Longrightarrow> 

1284 
tprg\<turnstile>s0' \<midarrow>test [Class Base]\<rightarrow> ?s9'" 

1285 
apply (unfold test_def arr_viewed_from_def) 

1286 
(* ?s9' = s9' *) 

1287 
apply (simp (no_asm_use)) 

1288 
apply (drule (1) alloc_one,clarsimp) 

1289 
apply (rule eval_Is (* ;; *)) 

1290 
apply (erule_tac V = "the (new_Addr ?h) = c" in thin_rl) 

1291 
apply (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl) 

1292 
apply (erule_tac [2] V = "atleast_free ?h four" in thin_rl) 

1293 
apply (rule eval_Is (* Expr *)) 

1294 
apply (rule eval_Is (* Ass *)) 

1295 
apply (rule eval_Is (* LVar *)) 

1296 
apply (rule eval_Is (* NewC *)) 

1297 
(* begin init Ext *) 

1298 
apply (erule_tac V = "the (new_Addr ?h) = b" in thin_rl) 

1299 
apply (erule_tac V = "atleast_free ?h tree" in thin_rl) 

1300 
apply (erule_tac [2] V = "atleast_free ?h four" in thin_rl) 

1301 
apply (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl) 

1302 
apply (rule eval_Is (* Init Ext *)) 

1303 
apply (simp) 

1304 
apply (rule conjI) 

1305 
prefer 2 apply (rule conjI HOL.refl)+ 

1306 
apply (rule eval_Is (* Init Base *)) 

1307 
apply (simp add: arr_viewed_from_def) 

1308 
apply (rule conjI) 

1309 
apply (rule eval_Is (* Init Object *)) 

1310 
apply (simp) 

1311 
apply (rule conjI, rule HOL.refl)+ 

1312 
apply (rule HOL.refl) 

1313 
apply (simp) 

1314 
apply (rule conjI, rule_tac [2] HOL.refl) 

1315 
apply (rule eval_Is (* Expr *)) 

1316 
apply (rule eval_Is (* Ass *)) 

1317 
apply (rule eval_Is (* FVar *)) 

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

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

1319 
apply (rule eval_Is (* StatRef *)) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

1321 
apply (simp add: check_field_access_def Let_def) 
12854  1322 
apply (rule eval_Is (* NewA *)) 
1323 
apply (simp) 

1324 
apply (rule eval_Is (* Lit *)) 

1325 
apply (simp) 

1326 
apply (rule halloc.New) 

1327 
apply (simp (no_asm_simp)) 

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

1328 
apply (drule atleast_free_weaken,drule atleast_free_weaken) 
12854  1329 
apply (simp (no_asm_simp)) 
1330 
apply (simp add: upd_gobj_def) 

1331 
(* end init Ext *) 

1332 
apply (rule halloc.New) 

1333 
apply (drule alloc_one) 

1334 
prefer 2 apply fast 

1335 
apply (simp (no_asm_simp)) 

1336 
apply (drule atleast_free_weaken) 

1337 
apply force 

1338 
apply (simp) 

1339 
apply (drule alloc_one) 

1340 
apply (simp (no_asm_simp)) 

1341 
apply clarsimp 

1342 
apply (erule_tac V = "atleast_free ?h tree" in thin_rl) 

1343 
apply (drule_tac x = "a" in new_AddrD2 [THEN spec]) 

1344 
apply (simp (no_asm_use)) 

1345 
apply (rule eval_Is (* Try *)) 

1346 
apply (rule eval_Is (* Expr *)) 

1347 
(* begin method call *) 

1348 
apply (rule eval_Is (* Call *)) 

1349 
apply (rule eval_Is (* Acc *)) 

1350 
apply (rule eval_Is (* LVar *)) 

1351 
apply (rule eval_Is (* Cons *)) 

1352 
apply (rule eval_Is (* Lit *)) 

1353 
apply (rule eval_Is (* Nil *)) 

1354 
apply (simp) 

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

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

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

1357 
"tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from Main") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

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

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

1360 
apply (rule Ext_foo_dyn_accessible) 
12854  1361 
apply (rule eval_Is (* Methd *)) 
1362 
apply (simp add: body_def Let_def) 

1363 
apply (rule eval_Is (* Body *)) 

1364 
apply (rule init_done, simp) 

1365 
apply (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo) 

1366 
apply (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo) 

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

1367 
apply (rule eval_Is (* Comp *)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1368 
apply (rule eval_Is (* Expr *)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1369 
apply (rule eval_Is (* Ass *)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1370 
apply (rule eval_Is (* FVar *)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1371 
apply (rule init_done, 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

1372 
apply (rule eval_Is (* Cast *)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1373 
apply (rule eval_Is (* Acc *)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1374 
apply (rule eval_Is (* LVar *)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1375 
apply (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

1376 
apply (simp split del: split_if) 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

1377 
apply (simp add: check_field_access_def Let_def) 
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

1378 
apply (rule eval_Is (* XcptE *)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1379 
apply (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

1380 
apply (rule conjI) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

1381 
apply (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

1382 
apply (rule eval_Is (* Comp *)) 
12854  1383 
apply (simp) 
1384 
(* end method call *) 

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

1385 
apply simp 
12854  1386 
apply (rule sxalloc.intros) 
1387 
apply (rule halloc.New) 

1388 
apply (erule alloc_one [THEN conjunct1]) 

1389 
apply (simp (no_asm_simp)) 

1390 
apply (simp (no_asm_simp)) 

1391 
apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if) 

1392 
apply (drule alloc_one [THEN conjunct1]) 

1393 
apply (simp (no_asm_simp)) 

1394 
apply (erule_tac V = "atleast_free ?h two" in thin_rl) 

1395 
apply (drule_tac x = "a" in new_AddrD2 [THEN spec]) 

1396 
apply simp 

1397 
apply (rule eval_Is (* While *)) 

1398 
apply (rule eval_Is (* Acc *)) 

1399 
apply (rule eval_Is (* AVar *)) 

1400 
apply (rule eval_Is (* Acc *)) 

1401 
apply (rule eval_Is (* FVar *)) 

1402 
apply (rule init_done, simp) 

1403 
apply (rule eval_Is (* StatRef *)) 

1404 
apply (simp) 

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

1405 
apply (simp add: check_field_access_def Let_def) 
12854  1406 
apply (rule eval_Is (* Lit *)) 
1407 
apply (simp (no_asm_simp)) 

1408 
apply (auto simp add: in_bounds_def) 

1409 
done 

1410 
declare Pair_eq [simp] 
