author  wenzelm 
Mon, 25 Feb 2002 20:48:14 +0100  
changeset 12937  0c4fd7529467 
parent 12925  99131847fb93 
child 13524  604d0f3622d6 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Example.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

12858  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
12854  5 
*) 
6 
header {* Example Bali program *} 

7 

8 
theory Example = Eval + WellForm: 

9 

10 
text {* 

11 
The following example Bali program includes: 

12 
\begin{itemize} 

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

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

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

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

17 
local assignment, local access, field assignment, type cast, 

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

19 
statement 

20 
\item instance creation and (default) static initialization 

21 
\end{itemize} 

22 
\begin{verbatim} 

23 
package java_lang 

24 

25 
public interface HasFoo { 

26 
public Base foo(Base z); 

27 
} 

28 

29 
public class Base implements HasFoo { 

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

31 
public HasFoo vee; 

32 
public Base foo(Base z) { 

33 
return z; 

34 
} 

35 
} 

36 

37 
public class Ext extends Base { 

38 
public int vee; 

39 
public Ext foo(Base z) { 

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

41 
return null; 

42 
} 

43 
} 

44 

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

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

48 
try {e.foo(null); } 

49 
catch(NullPointerException z) { 

50 
while(Ext.arr[2]) ; 

51 
} 

52 
} 

53 
} 

54 
\end{verbatim} 

55 
*} 

56 
declare widen.null [intro] 

57 

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

59 
apply (unfold wf_fdecl_def) 

60 
apply (simp (no_asm)) 

61 
done 

62 

63 
declare wf_fdecl_def2 [iff] 

64 

65 

66 
section "type and expression names" 

67 

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

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

72 

73 
consts 

74 

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

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

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

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

79 
to tnam, vname and label **) 

80 

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

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

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

84 

85 

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

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

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

89 

90 
syntax 

91 

92 
HasFoo :: qtname 

93 
Base :: qtname 

94 
Ext :: qtname 

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

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

98 
z :: ename 

99 
e :: ename 

100 
lab1:: label 

101 
translations 

102 

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

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

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

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

109 
"z" == "(vnam_ z_)" 

110 
"e" == "(vnam_ e_)" 

111 
"lab1" == "label_ lab1_" 

112 

113 

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

115 
by (simp add: Object_def) 

116 

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

118 
by (simp add: Object_def) 

119 

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

120 
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

121 
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

122 

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

125 

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

127 
by (simp add: SXcpt_def) 

128 

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

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

130 
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

131 

12854  132 
section "classes and interfaces" 
133 

134 
defs 

135 

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

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

138 

139 
consts 

140 

141 
foo :: mname 

142 

143 
constdefs 

144 

145 
foo_sig :: sig 

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

147 

148 
foo_mhead :: mhead 

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

150 

151 
constdefs 

152 

153 
Base_foo :: mdecl 

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

155 
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

156 

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

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

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

161 
mbody=\<lparr>lcls=[] 

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

162 
,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := 
12854  163 
Lit (Intg 1))\<rparr> 
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 

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

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

691 
"tprg\<turnstile>(Base,mdecl 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

692 
by (auto intro!: members.Immediate Base_declares_foo) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

693 

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

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

697 

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

698 
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

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

700 
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

701 

12854  702 
lemma Base_foo_permits_acc: 
703 
"tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_to S" 

704 
by ( simp add: permits_acc_def Base_foo_def) 

705 

706 
lemma Base_foo_accessible [simp]: 

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

708 
by (auto intro: accessible_fromR.Immediate 
12854  709 
Base_foo_member_of_Base Base_foo_permits_acc) 
710 

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

711 
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

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

713 
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

714 
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

715 
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

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

717 

12854  718 
lemma accmethd_Base [simp]: 
719 
"accmethd tprg S Base = methd tprg Base" 

720 
apply (simp add: accmethd_def) 

721 
apply (rule filter_tab_all_True) 

722 
apply (simp add: snd_special_simp fst_special_simp) 

723 
done 

724 

725 
lemma Ext_foo_permits_acc: 

726 
"tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_to S" 

727 
by ( simp add: permits_acc_def Ext_foo_def) 

728 

729 
lemma Ext_foo_accessible [simp]: 

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

731 
by (auto intro: accessible_fromR.Immediate 
12854  732 
Ext_foo_member_of_Ext Ext_foo_permits_acc) 
733 

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

734 
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

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

736 
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

737 
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

738 
apply (rule Ext_foo_permits_acc) 
12854  739 
done 
740 

741 
lemma Ext_foo_overrides_Base_foo: 

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

743 
proof (rule overridesR.Direct, simp_all) 

744 
show "\<not> is_static Ext_foo" 

745 
by (simp add: member_is_static_simp Ext_foo_def) 

746 
show "\<not> is_static Base_foo" 

747 
by (simp add: member_is_static_simp Base_foo_def) 

748 
show "accmodi Ext_foo \<noteq> Private" 

749 
by (simp add: Ext_foo_def) 

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

751 
by (simp add: Ext_foo_def Base_foo_def) 

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

753 
by (auto intro: Ext_declares_foo) 

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

755 
by (auto intro: Base_declares_foo) 

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

757 
by (simp add: inheritable_in_def Base_foo_def) 

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

759 
by (simp add: Ext_foo_def Base_foo_def mhead_resTy_simp) 

760 
qed 

761 

762 
lemma accmethd_Ext [simp]: 

763 
"accmethd tprg S Ext = methd tprg Ext" 

764 
apply (simp add: accmethd_def) 

765 
apply (rule filter_tab_all_True) 

766 
apply (auto simp add: snd_special_simp fst_special_simp) 

767 
done 

768 

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

770 
by simp 

771 
lemma dynmethd_Ext_foo: 

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

773 
= Some (Ext,snd Ext_foo)" 

774 
proof  

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

776 
= Some (Base,snd Base_foo)" and 

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

778 
= Some (Ext,snd Ext_foo)" 

779 
by (auto simp add: Ext_foo_def Base_foo_def foo_sig_def) 

780 
with cls_Ext ws_tprg Ext_foo_overrides_Base_foo 

781 
show ?thesis 

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

783 
qed 

784 

785 
lemma Base_fields_accessible[simp]: 

786 
"accfield tprg S Base 

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

788 
apply (auto simp add: accfield_def expand_fun_eq Let_def 

789 
accessible_in_RefT_simp 

790 
is_public_def 

791 
BaseCl_def 

792 
permits_acc_def 

793 
declared_in_def 

794 
cdeclaredfield_def 

795 
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

796 
accessible_fromR.Immediate 
12854  797 
intro: members.Immediate) 
798 
done 

799 

800 

801 
lemma arr_member_of_Base: 

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

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

804 
member_of Base" 

805 
by (auto intro: members.Immediate 

806 
simp add: declared_in_def cdeclaredfield_def BaseCl_def) 

807 

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

808 
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

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

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

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

812 
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

813 

12854  814 
lemma arr_member_of_Ext: 
815 
"tprg\<turnstile>(Base, fdecl (arr, 

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

817 
member_of Ext" 

818 
apply (rule members.Inherited) 

819 
apply (simp add: inheritable_in_def) 

820 
apply (simp add: undeclared_in_def cdeclaredfield_def ExtCl_def) 

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

822 
done 

823 

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

824 
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

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

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

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

828 
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

829 

12854  830 
lemma Ext_fields_accessible[simp]: 
831 
"accfield tprg S Ext 

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

833 
apply (auto simp add: accfield_def expand_fun_eq Let_def 

834 
accessible_in_RefT_simp 

835 
is_public_def 

836 
BaseCl_def 

837 
ExtCl_def 

838 
permits_acc_def 

839 
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

840 
accessible_fromR.Immediate) 
12854  841 
apply (auto intro: members.Immediate arr_member_of_Ext 
842 
simp add: declared_in_def cdeclaredfield_def ExtCl_def) 

843 
done 

844 

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

845 
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

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

847 
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

848 
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

849 
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

850 
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

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

852 

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

853 
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

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

855 
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

856 
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

857 
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

858 
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

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

860 

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

863 
apply (simp add: is_acc_type_def accessible_in_RefT_simp) 

864 
done 

865 

866 
lemma PrimT_acc [simp]: 

867 
"is_acc_type tprg java_lang (PrimT t)" 

868 
apply (simp add: is_acc_type_def accessible_in_RefT_simp) 

869 
done 

870 

871 
lemma Object_acc [simp]: 

872 
"is_acc_class tprg java_lang Object" 

873 
apply (auto simp add: is_acc_class_def accessible_in_RefT_simp is_public_def) 

874 
done 

875 

876 

877 
section "wellformedness" 

878 

879 

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

881 
apply (unfold wf_idecl_def HasFooInt_def) 

882 
apply (auto intro!: wf_mheadI ws_idecl_HasFoo 

883 
simp add: foo_sig_def foo_mhead_def mhead_resTy_simp 

884 
member_is_static_simp ) 

885 
done 

886 

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

887 

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

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

892 
ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *} 

893 
lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros 

894 

895 
lemma wf_Base_foo: "wf_mdecl tprg Base Base_foo" 

896 
apply (unfold Base_foo_defs ) 

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

898 
simp add: mhead_resTy_simp) 

899 
done 

900 

901 
lemma wf_Ext_foo: "wf_mdecl tprg Ext Ext_foo" 

902 
apply (unfold Ext_foo_defs ) 

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

904 
simp add: mhead_resTy_simp ) 

905 
apply (rule wt.Cast) 

906 
prefer 2 

907 
apply simp 

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

909 
apply (auto intro!: wtIs) 

910 
done 

911 

912 
declare mhead_resTy_simp [simp add] 

913 
declare member_is_static_simp [simp add] 

914 

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

916 
apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def) 

917 
apply (auto intro!: wf_Base_foo) 

918 
apply (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_def) 

919 
apply (auto intro!: wtIs) 

920 
apply (auto simp add: Base_foo_defs entails_def Let_def) 

921 
apply (insert Base_foo_no_stat_override, simp add: Base_foo_def,blast)+ 

922 
apply (insert Base_foo_no_hide , simp add: Base_foo_def,blast) 

923 
done 

924 

925 

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

927 
apply (unfold wf_cdecl_def ExtCl_def) 

928 
apply (auto intro!: wf_Ext_foo ws_cdecl_Ext) 

929 
apply (auto simp add: entails_def snd_special_simp) 

930 
apply (insert Ext_foo_stat_override) 

931 
apply (force simp add: qmdecl_def Ext_foo_def Base_foo_def) 

932 
apply (force simp add: qmdecl_def Ext_foo_def Base_foo_def) 

933 
apply (force simp add: qmdecl_def Ext_foo_def Base_foo_def) 

934 
apply (insert Ext_foo_no_hide) 

935 
apply (simp_all add: qmdecl_def) 

936 
apply blast+ 

937 
done 

938 

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

939 
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

940 
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

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

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

943 

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

946 
apply (simp (no_asm_simp)) 

947 
apply (rule wf_HasFoo) 

948 
done 

949 

950 
lemma wf_cdecl_all_standard_classes: 

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

952 
apply (unfold standard_classes_def Let_def 

953 
ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def) 

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

955 
apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def) 

956 
apply (auto simp add: Object_def Classes_def standard_classes_def 

957 
SXcptC_def SXcpt_def) 

958 
done 

959 

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

961 
apply (simp (no_asm) add: Classes_def) 

962 
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

963 
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

964 
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

965 
apply (rule wf_MainC [THEN conjI]) 
12854  966 
apply (rule wf_cdecl_all_standard_classes) 
967 
done 

968 

969 
theorem wf_tprg: "wf_prog tprg" 

970 
apply (unfold wf_prog_def Let_def) 

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

972 
apply (rule conjI) 

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

974 
apply (rule conjI) 

975 
apply (simp add: Object_mdecls_def) 

976 
apply safe 

977 
apply (cut_tac xn_cases_old) (* FIXME (insert xn_cases) *) 

978 
apply (simp (no_asm_simp) add: Classes_def standard_classes_def) 

979 
apply (insert wf_idecl_all) 

980 
apply (insert wf_cdecl_all) 

981 
apply auto 

982 
done 

983 

984 

985 
section "max spec" 

986 

987 
lemma appl_methds_Base_foo: 

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

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

990 
,[Class Base])}" 

991 
apply (unfold appl_methds_def) 

992 
apply (simp (no_asm)) 

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

994 
apply (auto simp add: cmheads_def Base_foo_defs) 

995 
done 

996 

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

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

999 
, [Class Base])}" 

1000 
apply (unfold max_spec_def) 

1001 
apply (simp (no_asm) add: appl_methds_Base_foo) 

1002 
apply auto 

1003 
done 

1004 

1005 

1006 
section "welltypedness" 

1007 

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

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

1011 
apply (rule wtIs (* ;; *)) 

1012 
apply (rule wtIs (* Ass *)) 

1013 
apply (rule wtIs (* NewC *)) 

1014 
apply (rule wtIs (* LVar *)) 

1015 
apply (simp) 

1016 
apply (simp) 

1017 
apply (simp) 

1018 
apply (rule wtIs (* NewC *)) 

1019 
apply (simp) 

1020 
apply (simp) 

1021 
apply (rule wtIs (* Try *)) 

1022 
prefer 4 

1023 
apply (simp) 

1024 
defer 

1025 
apply (rule wtIs (* Expr *)) 

1026 
apply (rule wtIs (* Call *)) 

1027 
apply (rule wtIs (* Acc *)) 

1028 
apply (rule wtIs (* LVar *)) 

1029 
apply (simp) 

1030 
apply (simp) 

1031 
apply (rule wtIs (* Cons *)) 

1032 
apply (rule wtIs (* Lit *)) 

1033 
apply (simp) 

1034 
apply (rule wtIs (* Nil *)) 

1035 
apply (simp) 

1036 
apply (rule max_spec_Base_foo) 

1037 
apply (simp) 

1038 
apply (simp) 

1039 
apply (simp) 

1040 
apply (simp) 

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

1041 
apply (simp) 
12854  1042 
apply (rule wtIs (* While *)) 
1043 
apply (rule wtIs (* Acc *)) 

1044 
apply (rule wtIs (* AVar *)) 

1045 
apply (rule wtIs (* Acc *)) 

1046 
apply (rule wtIs (* FVar *)) 

1047 
apply (rule wtIs (* StatRef *)) 

1048 
apply (simp) 

1049 
apply (simp) 

1050 
apply (simp ) 

1051 
apply (simp) 

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

1052 
apply (simp) 
12854  1053 
apply (rule wtIs (* LVar *)) 
1054 
apply (simp) 

1055 
apply (rule wtIs (* Skip *)) 

1056 
done 

1057 

1058 

1059 
section "execution" 

1060 

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

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

1063 
apply (frule atleast_free_SucD) 

1064 
apply (drule atleast_free_Suc [THEN iffD1]) 

1065 
apply clarsimp 

1066 
apply (frule new_Addr_SomeI) 

1067 
apply force 

1068 
done 

1069 

1070 
declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp] 

1071 
declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp] 

1072 
declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp] 

1073 
Base_foo_defs [simp] 

1074 

1075 
ML {* bind_thms ("eval_intros", map 

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

1077 
addsimps [thm "lvar_def"]) o 

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

1079 
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros 

1080 

1081 
consts 

1082 
a :: loc 

1083 
b :: loc 

1084 
c :: loc 

1085 

1086 
syntax 

1087 

1088 
tprg :: prog 

1089 

1090 
obj_a :: obj 

1091 
obj_b :: obj 

1092 
obj_c :: obj 

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

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

1095 
globs1 :: globs 

1096 
globs2 :: globs 

1097 
globs3 :: globs 

1098 
globs8 :: globs 

1099 
locs3 :: locals 

1100 
locs4 :: locals 

1101 
locs8 :: locals 

1102 
s0 :: state 

1103 
s0' :: state 

1104 
s9' :: state 

1105 
s1 :: state 

1106 
s1' :: state 

1107 
s2 :: state 

1108 
s2' :: state 

1109 
s3 :: state 

1110 
s3' :: state 

1111 
s4 :: state 

1112 
s4' :: state 

1113 
s6' :: state 

1114 
s7' :: state 

1115 
s8 :: state 

1116 
s8' :: state 

1117 

1118 
translations 

1119 

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

1121 

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

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

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

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

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

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

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

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

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

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

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

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

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

1135 
(Inl a\<mapsto>obj_a) 

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

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

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

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

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

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

1142 
"s0" == " st empty empty" 

1143 
"s0'" == " Norm s0" 

1144 
"s1" == " st globs1 empty" 

1145 
"s1'" == " Norm s1" 

1146 
"s2" == " st globs2 empty" 

1147 
"s2'" == " Norm s2" 

1148 
"s3" == " st globs3 locs3 " 

1149 
"s3'" == " Norm s3" 

1150 
"s4" == " st globs3 locs4" 

1151 
"s4'" == " Norm s4" 

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

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

1154 
"s8" == " st globs8 locs8" 

1155 
"s8'" == " Norm s8" 

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

1157 

1158 

1159 
syntax "four"::nat 

1160 
"tree"::nat 

1161 
"two" ::nat 

1162 
"one" ::nat 

1163 
translations 

1164 
"one" == "Suc 0" 

1165 
"two" == "Suc one" 

1166 
"tree" == "Suc two" 

1167 
"four" == "Suc tree" 

1168 

1169 
declare Pair_eq [simp del] 

1170 
lemma exec_test: 

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

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

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

1174 
atleast_free (heap s0) four \<Longrightarrow> 

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

1176 
apply (unfold test_def arr_viewed_from_def) 

1177 
(* ?s9' = s9' *) 

1178 
apply (simp (no_asm_use)) 

1179 
apply (drule (1) alloc_one,clarsimp) 

1180 
apply (rule eval_Is (* ;; *)) 

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

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

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

1184 
apply (rule eval_Is (* Expr *)) 

1185 
apply (rule eval_Is (* Ass *)) 

1186 
apply (rule eval_Is (* LVar *)) 

1187 
apply (rule eval_Is (* NewC *)) 

1188 
(* begin init Ext *) 

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

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

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

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

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

1194 
apply (simp) 

1195 
apply (rule conjI) 

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

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

1198 
apply (simp add: arr_viewed_from_def) 

1199 
apply (rule conjI) 

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

1201 
apply (simp) 

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

1203 
apply (rule HOL.refl) 

1204 
apply (simp) 

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

1206 
apply (rule eval_Is (* Expr *)) 

1207 
apply (rule eval_Is (* Ass *)) 

1208 
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

1209 
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

1210 
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

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

1212 
apply (simp add: check_field_access_def Let_def) 
12854  1213 
apply (rule eval_Is (* NewA *)) 
1214 
apply (simp) 

1215 
apply (rule eval_Is (* Lit *)) 

1216 
apply (simp) 

1217 
apply (rule halloc.New) 

1218 
apply (simp (no_asm_simp)) 

1219 
apply (drule atleast_free_weaken,rotate_tac 1,drule atleast_free_weaken) 

1220 
apply (simp (no_asm_simp)) 

1221 
apply (simp add: upd_gobj_def) 

1222 
(* end init Ext *) 

1223 
apply (rule halloc.New) 

1224 
apply (drule alloc_one) 

1225 
prefer 2 apply fast 

1226 
apply (simp (no_asm_simp)) 

1227 
apply (drule atleast_free_weaken) 

1228 
apply force 

1229 
apply (simp) 

1230 
apply (drule alloc_one) 

1231 
apply (simp (no_asm_simp)) 

1232 
apply clarsimp 

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

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

1235 
apply (simp (no_asm_use)) 

1236 
apply (rule eval_Is (* Try *)) 

1237 
apply (rule eval_Is (* Expr *)) 

1238 
(* begin method call *) 

1239 
apply (rule eval_Is (* Call *)) 

1240 
apply (rule eval_Is (* Acc *)) 

1241 
apply (rule eval_Is (* LVar *)) 

1242 
apply (rule eval_Is (* Cons *)) 

1243 
apply (rule eval_Is (* Lit *)) 

1244 
apply (rule eval_Is (* Nil *)) 

1245 
apply (simp) 

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

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

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

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

1249 
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

1250 
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

1251 
apply (rule Ext_foo_dyn_accessible) 
12854  1252 
apply (rule eval_Is (* Methd *)) 
1253 
apply (simp add: body_def Let_def) 

1254 
apply (rule eval_Is (* Body *)) 

1255 
apply (rule init_done, simp) 

1256 
apply (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo) 

1257 
apply (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo) 

1258 
apply (rule eval_Is (* Expr *)) 

1259 
apply (rule eval_Is (* Ass *)) 

1260 
apply (rule eval_Is (* FVar *)) 

1261 
apply (rule init_done, simp) 

1262 
apply (rule eval_Is (* Cast *)) 

1263 
apply (rule eval_Is (* Acc *)) 

1264 
apply (rule eval_Is (* LVar *)) 

1265 
apply (simp) 

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

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

1267 
apply (simp add: check_field_access_def Let_def) 
12854  1268 
apply (rule eval_Is (* XcptE *)) 
1269 
apply (simp) 

1270 
(* end method call *) 

1271 
apply (rule sxalloc.intros) 

1272 
apply (rule halloc.New) 

1273 
apply (erule alloc_one [THEN conjunct1]) 

1274 
apply (simp (no_asm_simp)) 

1275 
apply (simp (no_asm_simp)) 

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

1277 
apply (drule alloc_one [THEN conjunct1]) 

1278 
apply (simp (no_asm_simp)) 

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

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

1281 
apply simp 

1282 
apply (rule eval_Is (* While *)) 

1283 
apply (rule eval_Is (* Acc *)) 

1284 
apply (rule eval_Is (* AVar *)) 

1285 
apply (rule eval_Is (* Acc *)) 

1286 
apply (rule eval_Is (* FVar *)) 

1287 
apply (rule init_done, simp) 

1288 
apply (rule eval_Is (* StatRef *)) 

1289 
apply (simp) 

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

1290 
apply (simp add: check_field_access_def Let_def) 
12854  1291 
apply (rule eval_Is (* Lit *)) 
1292 
apply (simp (no_asm_simp)) 

1293 
apply (auto simp add: in_bounds_def) 

1294 
done 

1295 
declare Pair_eq [simp] 

1296 

1297 
end 